diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_state.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_state.h | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 76baab7ca..d45938f98 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -17,6 +17,7 @@ #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H +#include "theory/theory.h" #include "theory/theory_state.h" namespace CVC4 { @@ -31,6 +32,44 @@ class QuantifiersState : public TheoryState public: QuantifiersState(context::Context* c, context::UserContext* u, Valuation val); ~QuantifiersState() {} + /** + * Increment the instantiation counters, called once at the beginning of when + * we perform a check with quantifiers engine for the given effort. + */ + void incrementInstRoundCounters(Theory::Effort e); + /** + * Get whether we need to check at effort e based on the inst-when mode. This + * option determines the policy of quantifier instantiation and theory + * combination, e.g. does it run before, after, or interleaved with theory + * combination. This is based on the state of the counters maintained by this + * class. + */ + bool getInstWhenNeedsCheck(Theory::Effort e) const; + /** Get the number of instantiation rounds performed in this SAT context */ + uint64_t getInstRoundDepth() const; + /** Get the total number of instantiation rounds performed */ + uint64_t getInstRounds() const; + /** debug print equality engine on trace c */ + void debugPrintEqualityEngine(const char* c) const; + + private: + /** The number of instantiation rounds in this SAT context */ + context::CDO<uint64_t> d_ierCounterc; + /** The number of total instantiation rounds (full effort) */ + uint64_t d_ierCounter; + /** The number of total instantiation rounds (last call effort) */ + uint64_t d_ierCounterLc; + /** + * A counter to remember the last value of d_ierCounterLc where we a + * full effort check. This is used for interleaving theory combination + * and quantifier instantiation rounds. + */ + uint64_t d_ierCounterLastLc; + /** + * The number of instantiation rounds we run for each call to theory + * combination. + */ + uint64_t d_instWhenPhase; }; } // namespace quantifiers |