diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 8169c78fb..29381a309 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -104,12 +104,13 @@ private: std::vector< Node > d_quants; /** list of all lemmas produced */ std::map< Node, bool > d_lemmas_produced; + BoolMap d_lemmas_produced_c; /** lemmas waiting */ std::vector< Node > d_lemmas_waiting; /** has added lemma this round */ bool d_hasAddedLemma; /** list of all instantiations produced for each quantifier */ - std::map< Node, inst::InstMatchTrie > d_inst_match_trie; + std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie; /** term database */ quantifiers::TermDb* d_term_db; /** all triggers will be stored in this trie */ @@ -121,7 +122,7 @@ private: private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: - QuantifiersEngine(context::Context* c, TheoryEngine* te); + QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); /** get instantiator for id */ //Instantiator* getInstantiator( theory::TheoryId id ); @@ -136,6 +137,8 @@ public: quantifiers::ModelEngine* getModelEngine() { return d_model_engine; } /** get default sat context for quantifiers engine */ context::Context* getSatContext(); + /** get default sat context for quantifiers engine */ + context::Context* getUserContext(); /** get default output channel for the quantifiers engine */ OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ |