diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-29 13:49:51 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-29 13:50:08 -0500 |
commit | fa5df1aad69f8ad62686b9418070a1baf74b4a77 (patch) | |
tree | ad780365050498223b2a3fceb703556713cb49d0 /src/theory/quantifiers_engine.h | |
parent | 599329b76da2e95f18479a19c1bbbc3e3228b100 (diff) |
Add quantifiers options related to model and master equality engine.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5d7c25cde..bb38e5e4a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -165,6 +165,8 @@ private: //this information is reset during check context::CDO< bool > d_conflict_c; /** has added lemma this round */ bool d_hasAddedLemma; + /** whether to use model equality engine */ + bool d_useModelEe; private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; @@ -306,9 +308,9 @@ private: bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); -public: /** flush lemmas */ void flushLemmas(); +public: /** get instantiation */ Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); /** get instantiation */ @@ -366,9 +368,13 @@ public: void eqNotifyPostMerge(TNode t1, TNode t2); void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); /** get the master equality engine */ - eq::EqualityEngine* getMasterEqualityEngine() ; + eq::EqualityEngine* getMasterEqualityEngine(); + /** get the active equality engine */ + eq::EqualityEngine* getActiveEqualityEngine(); /** debug print equality engine */ void debugPrintEqualityEngine( const char * c ); + /** get internal representative */ + Node getInternalRepresentative( Node a, Node q, int index ); public: /** print instantiations */ void printInstantiations( std::ostream& out ); @@ -402,6 +408,7 @@ public: IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; IntStat d_inst_duplicate_ent; + IntStat d_inst_duplicate_model_true; IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers; |