GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_split.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_split.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief dynamic quantifiers splitting
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANT_SPLIT_H
18
#define CVC4__THEORY__QUANT_SPLIT_H
19
20
#include "context/cdo.h"
21
#include "theory/quantifiers/quant_module.h"
22
23
namespace CVC4 {
24
namespace theory {
25
26
class QuantifiersEngine;
27
28
namespace quantifiers {
29
30
/** Quantifiers dynamic splitting
31
 *
32
 * This module identifies quantified formulas that should be "split", e.g.
33
 * based on datatype constructor case splitting.
34
 *
35
 * An example of a quantified formula that we may split is the following. Let:
36
 *   optionPair := mkPair( U, U ) | none
37
 * where U is an uninterpreted sort. The quantified formula:
38
 *   forall x : optionPair. P( x )
39
 * may be "split" via the lemma:
40
 *   forall x : optionPair. P( x ) <=>
41
 *   ( forall xy : U. P( mkPair( x, y ) ) OR P( none ) )
42
 *
43
 * Notice that such splitting may lead to exponential behavior, say if we
44
 * quantify over 32 variables of type optionPair above gives 2^32 disjuncts.
45
 * This class is used to compute this splitting dynamically, by splitting
46
 * one variable per quantified formula at a time.
47
 */
48
10006
class QuantDSplit : public QuantifiersModule {
49
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
50
51
 public:
52
  QuantDSplit(QuantifiersEngine* qe,
53
              QuantifiersState& qs,
54
              QuantifiersInferenceManager& qim,
55
              QuantifiersRegistry& qr);
56
  /** determine whether this quantified formula will be reduced */
57
  void checkOwnership(Node q) override;
58
  /* whether this module needs to check this round */
59
  bool needsCheck(Theory::Effort e) override;
60
  /* Call during quantifier engine's check */
61
  void check(Theory::Effort e, QEffort quant_e) override;
62
  /** check complete for */
63
  bool checkCompleteFor(Node q) override;
64
  /** Identify this module (for debugging, dynamic configuration, etc..) */
65
57645
  std::string identify() const override { return "QuantDSplit"; }
66
67
 private:
68
  /** list of relevant quantifiers asserted in the current context */
69
  std::map<Node, int> d_quant_to_reduce;
70
  /** whether we have instantiated quantified formulas */
71
  NodeSet d_added_split;
72
};
73
74
}
75
}
76
}
77
78
#endif