From c71ec272d5ef58bfa147507bdbb370f2e288d154 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 24 Feb 2013 16:37:46 -0600 Subject: added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts --- src/theory/quantifiers_engine.h | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'src/theory/quantifiers_engine.h') 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 */ -- cgit v1.2.3