diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index fa8a51d1f..9f520f420 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -214,6 +214,7 @@ public: rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false ); + /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; public: /** statistics class */ @@ -266,7 +267,7 @@ private: /** pointer to theory engine */ QuantifiersEngine* d_qe; /** internal representatives */ - std::map< Node, Node > d_int_rep; + std::map< int, std::map< Node, Node > > d_int_rep; /** rep score */ std::map< Node, int > d_rep_score; /** reset count */ @@ -275,7 +276,9 @@ private: /** node contains */ Node getInstance( Node n, std::vector< Node >& eqc ); /** get score */ - int getRepScore( Node n ); + int getRepScore( Node n, Node f, int index ); + /** choose rep based on sort inference */ + bool optInternalRepSortInference(); public: EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){} ~EqualityQueryQuantifiersEngine(){} @@ -292,7 +295,7 @@ public: If cbqi is active, this will return a term in the equivalence class of "a" that does not contain instantiation constants, if such a term exists. */ - Node getInternalRepresentative( Node a ); + Node getInternalRepresentative( Node a, Node f, int index ); }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory namespace */ |