Add quantifiers options related to model and master equality engine.

9 files changed, 17 insertions, 20 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 7c9a6196f..17c8e0300 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -284,7 +284,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
       TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
       if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
-          nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
+          nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
           //don't consider this if already the instantiation is ineligible
           if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){
             nh = Node::null();
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 703dc6928..7ce299864 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -711,6 +711,7 @@ void CegInstantiator::processAssertions() {
   d_curr_eqc.clear();
   d_curr_type_eqc.clear();
 
+  // must use master equality engine to avoid value instantiations
   eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
   //to eliminate identified illegal terms
   std::map< Node, Node > aux_subs;
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 28b92cc5e..6457de145 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -91,7 +91,7 @@ bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
 
 /** get the equality engine associated with this query */
 eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
-  return d_qe->getMasterEqualityEngine();
+  return d_qe->getActiveEqualityEngine();
 }
 
 /** get the equivalence class of a */
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index ada28c084..09ed99735 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -143,7 +143,7 @@ void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) {
 
 void LtePartialInst::reset() {
   d_reps.clear();
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   while( !eqcs_i.isFinished() ){
     TNode r = (*eqcs_i);
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f529a9a27..2faf13f1a 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -155,7 +155,7 @@ int ModelEngine::checkModel(){
   //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
   //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
 
-  //for debugging
+  //for debugging, setup
   for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
        it != fm->d_rep_set.d_type_reps.end(); ++it ){
     if( it->first.isSort() ){
@@ -167,7 +167,7 @@ int ModelEngine::checkModel(){
       Trace("model-engine-debug") << std::endl;
       Trace("model-engine-debug") << "   Term reps : ";
       for( size_t i=0; i<it->second.size(); i++ ){
-        Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
+        Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 );
         Trace("model-engine-debug") << r << " ";
       }
       Trace("model-engine-debug") << std::endl;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 163c576f7..8fecaa78d 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -29,7 +29,7 @@ unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
 }
 
 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
-  return d_quantEngine->getMasterEqualityEngine();
+  return d_quantEngine->getActiveEqualityEngine();
 }
 
 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 28423259b..4f58f7a2e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -204,7 +204,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
 
 void TermDb::computeArgReps( TNode n ) {
   if( d_arg_reps.find( n )==d_arg_reps.end() ){
-    eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+    eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
     for( unsigned j=0; j<n.getNumChildren(); j++ ){
       TNode r = ee->hasTerm( n[j] ) ? ee->getRepresentative( n[j] ) : n[j];
       d_arg_reps[n].push_back( r );
@@ -215,7 +215,7 @@ void TermDb::computeArgReps( TNode n ) {
 void TermDb::computeUfEqcTerms( TNode f ) {
   if( d_func_map_eqc_trie.find( f )==d_func_map_eqc_trie.end() ){
     d_func_map_eqc_trie[f].clear();
-    eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+    eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
     for( unsigned i=0; i<d_op_map[f].size(); i++ ){
       TNode n = d_op_map[f][i];
       if( hasTermCurrent( n ) ){
@@ -234,7 +234,7 @@ void TermDb::computeUfTerms( TNode f ) {
     d_op_nonred_count[ f ] = 0;
     std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
     if( it!=d_op_map.end() ){
-      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+      eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
       Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
       unsigned congruentCount = 0;
       unsigned nonCongruentCount = 0;
@@ -307,7 +307,8 @@ void TermDb::computeUfTerms( TNode f ) {
 
 bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
   computeUfTerms( f );
-  Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r );
+  Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || 
+          d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r );
   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
   if( it != d_func_map_rel_dom.end() ){
     std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
@@ -578,7 +579,7 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   if( !useMode ){
     return d_has_map.find( n )!=d_has_map.end();
   }else{
-    //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
+    //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
     if( options::termDbMode()==TERM_DB_ALL ){
       return true;
     }else if( options::termDbMode()==TERM_DB_RELEVANT ){
@@ -630,7 +631,7 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
     std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
     if( it==d_term_elig_eqc.end() ){
       Node h;
-      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+      eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
       while( h.isNull() && !eqc_i.isFinished() ){
         TNode n = (*eqc_i);
@@ -680,7 +681,7 @@ bool TermDb::reset( Theory::Effort effort ){
   d_func_map_rel_dom.clear();
   d_consistent_ee = true;
 
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
   //compute has map
   if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
     d_has_map.clear();
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 94a11a09e..4d3e584b4 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -35,8 +35,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
-  d_masterEqualityEngine(0)
+    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
 {
   d_numInstantiations = 0;
   d_baseDecLevel = -1;
@@ -55,7 +54,7 @@ TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
 void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_masterEqualityEngine = eq;
+
 }
 
 void TheoryQuantifiers::addSharedTerm(TNode t) {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index f52381011..462dcb339 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -44,9 +44,6 @@ private:
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
-
-  eq::EqualityEngine* d_masterEqualityEngine;
-
 private:
   void computeCareGraph();
 
@@ -69,7 +66,6 @@ public:
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
-  eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
   bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
 private:
   void assertUniversal( Node n );