More optimization of QCF. Fixed InstMatchTrie for caching instantiations. Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.

14 files changed, 1206 insertions, 1047 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index ebe587765..8428069aa 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -158,7 +158,10 @@ void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) {
   set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n );
 }
 
-/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
+
+
+
+/*
 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
     int i_index = imtio ? imtio->d_order[index] : index;
@@ -167,7 +170,6 @@ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m,
   }
 }
 
-/** exists match */
 bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
   if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
     return true;
@@ -227,49 +229,96 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, b
     return false;
   }
 }
+*/
 
 
 
-/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
-void CDInstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ){
-  if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
+
+bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ){
+  if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
+    return false;
+  }else{
     int i_index = imtio ? imtio->d_order[index] : index;
     Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
-    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
     if( it!=d_data.end() ){
-      it->second->addInstMatch2( qe, f, m, c, index+1, imtio );
+      return it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
     }else{
-      CDInstMatchTrie* imt = new CDInstMatchTrie( c );
-      d_data[n] = imt;
-      imt->d_valid = true;
-      imt->addInstMatch2( qe, f, m, c, index+1, imtio );
+
+      /*
+      //check if m is an instance of another instantiation if modInst is true
+      if( modInst ){
+        if( !n.isNull() ){
+          Node nl;
+          std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
+          if( itm!=d_data.end() ){
+            if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+              return false;
+            }
+          }
+        }
+      }
+      */
+      /*
+      if( modEq ){
+        //check modulo equality if any other instantiation match exists
+        if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+          eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                   qe->getEqualityQuery()->getEngine() );
+          while( !eqc.isFinished() ){
+            Node en = (*eqc);
+            if( en!=n ){
+              std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
+              if( itc!=d_data.end() ){
+                if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+                  return false;
+                }
+              }
+            }
+            ++eqc;
+          }
+        }
+      }
+      */
+      if( !onlyExist ){
+        d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+      }
+      return true;
     }
   }
 }
 
+
+
 /** exists match */
-bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
-  if( !d_valid ){
-    return false;
-  }else if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
+bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
+  if( !d_valid.get() ){
+    if( onlyExist ){
+      return false;
+    }else{
+      d_valid.set( true );
+    }
+  }
+  if( index==(int)f[0].getNumChildren() ){
     return true;
   }else{
-    int i_index = imtio ? imtio->d_order[index] : index;
-    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
-    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
-    if( it!=d_data.end() ){
-      if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
-        return true;
+    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, index ) );
+    if( onlyExist ){
+      std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+      if( it!=d_data.end() ){
+        if( !it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
+          return false;
+        }
       }
     }
     //check if m is an instance of another instantiation if modInst is true
     if( modInst ){
       if( !n.isNull() ){
         Node nl;
-        it = d_data.find( nl );
-        if( it!=d_data.end() ){
-          if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
-            return true;
+        std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
+        if( itm!=d_data.end() ){
+          if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
+            return false;
           }
         }
       }
@@ -284,8 +333,8 @@ bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch
           if( en!=n ){
             std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
             if( itc!=d_data.end() ){
-              if( itc->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
-                return true;
+              if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
+                return false;
               }
             }
           }
@@ -293,24 +342,22 @@ bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch
         }
       }
     }
+    if( !onlyExist ){
+      std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+      CDInstMatchTrie* imt;
+      if( it!=d_data.end() ){
+        imt = it->second;
+        it->second->d_valid.set( true );
+      }else{
+        imt = new CDInstMatchTrie( c );
+        d_data[n] = imt;
+      }
+      return imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
+    }
     return false;
   }
 }
 
-bool CDInstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
-  return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
-}
-
-bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, Context* c, bool modEq, bool modInst, ImtIndexOrder* imtio ){
-  if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
-    addInstMatch2( qe, f, m, c, 0, imtio );
-    return true;
-  }else{
-    return false;
-  }
-}
-
-
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 72447fd66..2cf33bc8e 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -119,11 +119,6 @@ public:
   public:
     std::vector< int > d_order;
   };/* class InstMatchTrie ImtIndexOrder */
-private:
-  /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
-  void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio );
-  /** exists match */
-  bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 public:
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
@@ -136,16 +131,20 @@ public:
         modInst is if we return true if m is an instance of a match that exists
    */
   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                        bool modInst = false, ImtIndexOrder* imtio = NULL );
+                        bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
+    return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+  }
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                     bool modInst = false, ImtIndexOrder* imtio = NULL );
+                     bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 };/* class InstMatchTrie */
 
 
+#if 0
+
 /** trie for InstMatch objects */
 class CDInstMatchTrie {
 public:
@@ -181,6 +180,37 @@ public:
                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 };/* class CDInstMatchTrie */
 
+#else
+
+
+/** trie for InstMatch objects */
+class CDInstMatchTrie {
+public:
+  /** the data */
+  std::map< Node, CDInstMatchTrie* > d_data;
+  /** is valid */
+  context::CDO< bool > d_valid;
+public:
+  CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
+  ~CDInstMatchTrie(){}
+public:
+  /** return true if m exists in this trie
+        modEq is if we check modulo equality
+        modInst is if we return true if m is an instance of a match that exists
+   */
+  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+                        bool modInst = false, int index = 0 ) {
+    return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+  }
+  /** add match m for quantifier f, take into account equalities if modEq = true,
+      if imtio is non-null, this is the order to add to trie
+      return true if successful
+  */
+  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+                     bool modInst = false, int index = 0, bool onlyExist = false );
+};/* class CDInstMatchTrie */
+
+
 class InstMatchTrieOrdered{
 private:
   InstMatchTrie::ImtIndexOrder* d_imtio;
@@ -202,6 +232,9 @@ public:
   }
 };/* class InstMatchTrieOrdered */
 
+#endif
+
+
 }/* CVC4::theory::inst namespace */
 
 typedef CVC4::theory::inst::InstMatch InstMatch;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 9acdf6152..6a9327967 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/relevant_domain.h"
 
 using namespace std;
 using namespace CVC4;
@@ -60,6 +61,8 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
     return STATUS_UNFINISHED;
   }else if( e==1 ){
     d_counter[f]++;
+      Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
+
     Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;
     //Notice() << "Try user-provided patterns..." << std::endl;
     for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
@@ -150,6 +153,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
           Trace("no-trigger") << "Could not find trigger for " << f << std::endl;
         }
       }
+      Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
 
       //if( e==4 ){
       //  d_processed_trigger.clear();
@@ -250,7 +254,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
   if( !patTerms.empty() ){
     Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
     //sort terms based on relevance
-    if( d_rlv_strategy==RELEVANCE_DEFAULT ){
+    if( options::relevantTriggers() ){
       sortQuantifiersForSymbol sqfs;
       sqfs.d_qe = d_quantEngine;
       //sort based on # occurrences (this will cause Trigger to select rarer symbols)
@@ -317,12 +321,16 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
         if( index<(int)patTerms.size() ){
           //Notice() << "check add additional" << std::endl;
           //check if similar patterns exist, and if so, add them additionally
-          int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+          int nqfs_curr = 0;
+          if( options::relevantTriggers() ){
+            nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+          }
           index++;
           bool success = true;
           while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
             success = false;
-            if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
+            if( !options::relevantTriggers() ||
+                d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
               d_single_trigger_gen[ patTerms[index] ] = true;
               Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
                                                  options::smartTriggers() );
@@ -342,20 +350,6 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     }
   }
 }
-/*
-InstStrategyAutoGenTriggers::Statistics::Statistics():
-  d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
-  d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-  StatisticsRegistry::registerStat(&d_instantiations_min);
-}
-
-InstStrategyAutoGenTriggers::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-  StatisticsRegistry::unregisterStat(&d_instantiations_min);
-}
-*/
 
 void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
 }
@@ -364,26 +358,55 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
   if( e<5 ){
     return STATUS_UNFINISHED;
   }else{
+    //first, try from relevant domain
+    Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
+    bool success;
+    ///*  TODO: add back
+    RelevantDomain * rd = d_quantEngine->getRelevantDomain();
+    if( rd ){
+      rd->compute();
+      std::vector< unsigned > childIndex;
+      int index = 0;
+      do {
+        while( index>=0 && index<(int)f[0].getNumChildren() ){
+          if( index==(int)childIndex.size() ){
+            childIndex.push_back( -1 );
+          }else{
+            Assert( index==(int)(childIndex.size())-1 );
+            if( (childIndex[index]+1)<rd->getRDomain( f, index )->d_terms.size() ){
+              childIndex[index]++;
+              index++;
+            }else{
+              childIndex.pop_back();
+              index--;
+            }
+          }
+        }
+        success = index>=0;
+        if( success ){
+          index--;
+          //try instantiation
+          InstMatch m;
+          for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+            m.set( d_quantEngine, f, i, rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+          }
+          if( d_quantEngine->addInstantiation( f, m, true, false, false ) ){
+            ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+            return STATUS_UNKNOWN;
+          }
+        }
+      }while( success );
+    }
+    //*/
+
     if( d_guessed.find( f )==d_guessed.end() ){
+      Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
       d_guessed[f] = true;
-      Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
       InstMatch m;
       if( d_quantEngine->addInstantiation( f, m ) ){
         ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
-        //d_quantEngine->d_hasInstantiated[f] = true;
       }
     }
     return STATUS_UNKNOWN;
   }
 }
-/*
-InstStrategyFreeVariable::Statistics::Statistics():
-  d_instantiations("InstStrategyGuess::Instantiations", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyFreeVariable::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index c73186dbb..24470c58b 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -65,8 +65,6 @@ public:
 private:
   /** trigger generation strategy */
   int d_tr_strategy;
-  /** relevance strategy */
-  int d_rlv_strategy;
   /** regeneration */
   bool d_regenerate;
   int d_regenerate_frequency;
@@ -92,8 +90,8 @@ public:
   /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
       rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
       rgfr is the frequency at which triggers are generated */
-  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :
-      InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){
+  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt,  int rgfr = -1 ) :
+      InstStrategy( qe ), d_tr_strategy( tstrt ), d_generate_additional( false ){
     setRegenerateFrequency( rgfr );
   }
   ~InstStrategyAutoGenTriggers(){}
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index c19172b3b..41198c1f4 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -48,8 +48,7 @@ void InstantiationEngine::finishInit(){
     }else{
       d_isup = NULL;
     }
-    int rlv = options::relevantTriggers() ? InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT : InstStrategyAutoGenTriggers::RELEVANCE_NONE;
-    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, rlv, 3 );
+    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 );
     i_ag->setGenerateAdditional( true );
     addInstStrategy( i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
@@ -250,8 +249,10 @@ void InstantiationEngine::check( Theory::Effort e ){
         Debug("quantifiers") << "  Active : " << n << ", no ce assigned." << std::endl;
       }
       Debug("quantifiers-relevance")  << "Quantifier : " << n << std::endl;
-      Debug("quantifiers-relevance")  << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
-      Debug("quantifiers") << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
+      if( options::relevantTriggers() ){
+        Debug("quantifiers-relevance")  << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
+        Debug("quantifiers") << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
+      }
       Trace("inst-engine-debug") << "Process : " << n << " " << d_quant_active[n] << std::endl;
     }
     if( quantActive ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 9e3e77c8e..ef4e67a68 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -50,12 +50,6 @@ QuantifiersModule( qe ){
     Trace("model-engine-debug") << "...make default model builder." << std::endl;
     d_builder = new QModelBuilderDefault( c, qe );
   }
-
-  if( options::fmfRelevantDomain() ){
-    d_rel_dom = new RelevantDomain( qe, qe->getModel() );
-  }else{
-    d_rel_dom = NULL;
-  }
 }
 
 void ModelEngine::check( Theory::Effort e ){
@@ -192,10 +186,6 @@ int ModelEngine::checkModel(){
       }
     }
   }
-  //relevant domain?
-  if( d_rel_dom ){
-    d_rel_dom->compute();
-  }
 
   d_triedLemmas = 0;
   d_addedLemmas = 0;
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index ba54d7ba4..cf770a7b9 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -20,7 +20,6 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/model_builder.h"
 #include "theory/theory_model.h"
-#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
@@ -32,8 +31,6 @@ class ModelEngine : public QuantifiersModule
 private:
   /** builder class */
   QModelBuilder* d_builder;
-private:    //analysis of current model:
-  RelevantDomain* d_rel_dom;
 private:
   //options
   bool optOneQuantPerRound();
@@ -52,8 +49,6 @@ private:
 public:
   ModelEngine( context::Context* c, QuantifiersEngine* qe );
   ~ModelEngine(){}
-  //get relevant domain
-  RelevantDomain * getRelevantDomain() { return d_rel_dom; }
   //get the builder
   QModelBuilder* getModelBuilder() { return d_builder; }
 public:
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 00d3cf234..8962104e1 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -103,8 +103,6 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
-option fmfRelevantDomain --fmf-relevant-domain bool :default false
- use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
 option fmfInstGen /--disable-fmf-inst-gen bool :default true
  disable Inst-Gen instantiation techniques for finite model finding
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 198ec3bbf..665ae5329 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -68,665 +68,8 @@ void QcfNodeIndex::debugPrint( const char * c, int t ) {
   }

 }

 

-QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :

-QuantifiersModule( qe ),

-d_c( c ),

-d_conflict( c, false ),

-d_qassert( c ) {

-  d_fid_count = 0;

-  d_true = NodeManager::currentNM()->mkConst<bool>(true);

-  d_false = NodeManager::currentNM()->mkConst<bool>(false);

-}

-

-Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {

-  if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){

-    index = 0;

-    return n;

-  }else if( isHandledUfTerm( n ) ){

-    /*

-    std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );

-    if( it==d_op_node.end() ){

-      std::vector< Node > children;

-      children.push_back( n.getOperator() );

-      for( unsigned i=0; i<n.getNumChildren(); i++ ){

-        children.push_back( getFv( n[i].getType() ) );

-      }

-      Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );

-      d_op_node[n.getOperator()] = nn;

-      return nn;

-    }else{

-      return it->second;

-    }*/

-    index = 1;

-    return n.getOperator();

-  }else{

-    return Node::null();

-  }

-}

-

-Node QuantConflictFind::mkEqNode( Node a, Node b ) {

-  if( a.getType().isBoolean() ){

-    return a.iffNode( b );

-  }else{

-    return a.eqNode( b );

-  }

-}

-

-//-------------------------------------------------- registration

-

-void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {

-  //qcf->d_node = n;

-  bool recurse = true;

-  if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){

-    if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

-      //literals

-

-      /*

-        if( n.getKind()==APPLY_UF || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){

-          for( unsigned i=0; i<n.getNumChildren(); i++ ){

-            flatten( q, n[i] );

-          }

-        }else if( n.getKind()==EQUAL ){

-          for( unsigned i=0; i<n.getNumChildren(); i++ ){

-            for( unsigned j=0; j<n[i].getNumChildren(); j++ ){

-              flatten( q, n[i][j] );

-            }

-          }

-        }

-

-        */

-

-      if( n.getKind()==APPLY_UF ){

-        flatten( q, n );

-      }else if( n.getKind()==EQUAL ){

-        for( unsigned i=0; i<n.getNumChildren(); i++ ){

-          flatten( q, n[i] );

-        }

-      }

-

-    }else{

-      Trace("qcf-qregister") << "    RegisterGroundLit : " << n;

-    }

-    recurse = false;

-  }

-  if( recurse ){

-    for( unsigned i=0; i<n.getNumChildren(); i++ ){

-      bool newHasPol;

-      bool newPol;

-      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );

-      //QcfNode * qcfc = new QcfNode( d_c );

-      //qcfc->d_parent = qcf;

-      //qcf->d_child[i] = qcfc;

-      registerNode( q, n[i], newHasPol, newPol );

-    }

-  }

-}

-

-void QuantConflictFind::flatten( Node q, Node n ) {

-  if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){

-    if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){

-      //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;

-      d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();

-      d_qinfo[q].d_vars.push_back( n );

-    }

-    for( unsigned i=0; i<n.getNumChildren(); i++ ){

-      flatten( q, n[i] );

-    }

-  }

-}

-

-void QuantConflictFind::registerQuantifier( Node q ) {

-  d_quants.push_back( q );

-  d_quant_id[q] = d_quants.size();

-  Trace("qcf-qregister") << "Register ";

-  debugPrintQuant( "qcf-qregister", q );

-  Trace("qcf-qregister") << " : " << q << std::endl;

-

-  //register the variables

-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

-    d_qinfo[q].d_var_num[q[0][i]] = i;

-    d_qinfo[q].d_vars.push_back( q[0][i] );

-  }

-

-  //make QcfNode structure

-  Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;

-  //d_qinfo[q].d_cf = new QcfNode( d_c );

-  registerNode( q, q[1], true, true );

-

-  //debug print

-  Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;

-  Trace("qcf-qregister") << "    ";

-  debugPrintQuantBody( "qcf-qregister", q, q[1] );

-  Trace("qcf-qregister") << std::endl;

-  if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){

-    Trace("qcf-qregister") << "  with additional constraints : " << std::endl;

-    for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){

-      Trace("qcf-qregister") << "    ?x" << j << " = ";

-      debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );

-      Trace("qcf-qregister") << std::endl;

-    }

-  }

-

-  Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;

-  d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );

-

-  for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){

-    d_qinfo[q].d_var_mg[j] = new MatchGen( this, q, d_qinfo[q].d_vars[j], false, true );

-    if( !d_qinfo[q].d_var_mg[j]->isValid() ){

-      d_qinfo[q].d_mg->setInvalid();

-      break;

-    }

-  }

-

-  Trace("qcf-qregister") << "Done registering quantifier." << std::endl;

-}

-

-int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {

-  int ret = 0;

-  if( n.getKind()==EQUAL ){

-    Node n1 = evaluateTerm( n[0] );

-    Node n2 = evaluateTerm( n[1] );

-    Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;

-    if( areEqual( n1, n2 ) ){

-      ret = 1;

-    }else if( areDisequal( n1, n2 ) ){

-      ret = -1;

-    }

-    //else if( d_effort>QuantConflictFind::effort_conflict ){

-    //  ret = -1;

-    //}

-  }else if( n.getKind()==APPLY_UF ){  //predicate

-    Node nn = evaluateTerm( n );

-    Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;

-    if( areEqual( nn, d_true ) ){

-      ret = 1;

-    }else if( areEqual( nn, d_false ) ){

-      ret = -1;

-    }

-    //else if( d_effort>QuantConflictFind::effort_conflict ){

-    //  ret = -1;

-    //}

-  }else if( n.getKind()==NOT ){

-    return -evaluate( n[0] );

-  }else if( n.getKind()==ITE ){

-    int cev1 = evaluate( n[0] );

-    int cevc[2] = { 0, 0 };

-    for( unsigned i=0; i<2; i++ ){

-      if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){

-        cevc[i] = evaluate( n[i+1] );

-        if( cev1!=0 ){

-          ret = cevc[i];

-          break;

-        }else if( cevc[i]==0 ){

-          break;

-        }

-      }

-    }

-    if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){

-      ret = cevc[0];

-    }

-  }else if( n.getKind()==IFF ){

-    int cev1 = evaluate( n[0] );

-    if( cev1!=0 ){

-      int cev2 = evaluate( n[1] );

-      if( cev2!=0 ){

-        ret = cev1==cev2 ? 1 : -1;

-      }

-    }

-

-  }else{

-    int ssval = 0;

-    if( n.getKind()==OR ){

-      ssval = 1;

-    }else if( n.getKind()==AND ){

-      ssval = -1;

-    }

-    bool isUnk = false;

-    for( unsigned i=0; i<n.getNumChildren(); i++ ){

-      int cev = evaluate( n[i] );

-      if( cev==ssval ){

-        ret = ssval;

-        break;

-      }else if( cev==0 ){

-        isUnk = true;

-      }

-    }

-    if( ret==0 && !isUnk ){

-      ret = -ssval;

-    }

-  }

-  Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;

-  return ret;

-}

-

-bool QuantConflictFind::isPropagationSet() {

-  return !d_prop_eq[0].isNull();

-}

-

-bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {

-  //if( d_effort==QuantConflictFind::effort_prop_deq ){

-  //  return n1==n2 || !areDisequal( n1, n2 );

-  //}else{

-  return n1==n2;

-  //}

-}

-

-bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {

-  //if( d_effort==QuantConflictFind::effort_conflict ){

-  //  return areDisequal( n1, n2 );

-  //}else{

-  return n1!=n2;

-  //}

-}

-

-//-------------------------------------------------- handling assertions / eqc

-

-void QuantConflictFind::assertNode( Node q ) {

-  Trace("qcf-proc") << "QCF : assertQuantifier : ";

-  debugPrintQuant("qcf-proc", q);

-  Trace("qcf-proc") << std::endl;

-  d_qassert.push_back( q );

-  //set the eqRegistries that this depends on to true

-  //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){

-  //  it->first->d_active.set( true );

-  //}

-}

 

-eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {

-  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();

-  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();

-}

-bool QuantConflictFind::areEqual( Node n1, Node n2 ) {

-  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );

-}

-bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {

-  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );

-}

-Node QuantConflictFind::getRepresentative( Node n ) {

-  if( getEqualityEngine()->hasTerm( n ) ){

-    return getEqualityEngine()->getRepresentative( n );

-  }else{

-    return n;

-  }

-}

-Node QuantConflictFind::evaluateTerm( Node n ) {

-  if( isHandledUfTerm( n ) ){

-    Node nn;

-    if( getEqualityEngine()->hasTerm( n ) ){

-      computeArgReps( n );

-      nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );

-    }else{

-      std::vector< TNode > args;

-      for( unsigned i=0; i<n.getNumChildren(); i++ ){

-        Node c = evaluateTerm( n[i] );

-        args.push_back( c );

-      }

-      nn = d_uf_terms[n.getOperator()].existsTerm( n, args );

-    }

-    if( !nn.isNull() ){

-      Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;

-      return getRepresentative( nn );

-    }else{

-      Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;

-      return n;

-    }

-  }

-  return getRepresentative( n );

-}

-

-/*

-QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {

-  std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );

-  if( it2==d_eqc_info.end() ){

-    if( doCreate ){

-      EqcInfo * eqci = new EqcInfo( d_c );

-      d_eqc_info[n] = eqci;

-      return eqci;

-    }else{

-      return NULL;

-    }

-  }

-  return it2->second;

-}

-*/

-

-QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {

-  std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );

-  if( itut==d_eqc_uf_terms.end() ){

-    return NULL;

-  }else{

-    if( eqc.isNull() ){

-      return &itut->second;

-    }else{

-      std::map< TNode, QcfNodeIndex >::iterator itute = itut->second.d_children.find( eqc );

-      if( itute!=itut->second.d_children.end() ){

-        return &itute->second;

-      }else{

-        return NULL;

-      }

-    }

-  }

-}

-

-QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {

-  std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );

-  if( itut!=d_uf_terms.end() ){

-    return &itut->second;

-  }else{

-    return NULL;

-  }

-}

-

-/** new node */

-void QuantConflictFind::newEqClass( Node n ) {

-  //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;

-  //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;

-}

-

-/** merge */

-void QuantConflictFind::merge( Node a, Node b ) {

-  /*

-  if( b.getKind()==EQUAL ){

-    if( a==d_true ){

-      //will merge anyways

-      //merge( b[0], b[1] );

-    }else if( a==d_false ){

-      assertDisequal( b[0], b[1] );

-    }

-  }else{

-    Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;

-    EqcInfo * eqc_b = getEqcInfo( b, false );

-    EqcInfo * eqc_a = NULL;

-    if( eqc_b ){

-      eqc_a = getEqcInfo( a );

-      //move disequalities of b into a

-      for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){

-        if( (*it).second ){

-          Node n = (*it).first;

-          EqcInfo * eqc_n = getEqcInfo( n, false );

-          Assert( eqc_n );

-          if( !eqc_n->isDisequal( a ) ){

-            Assert( !eqc_a->isDisequal( n ) );

-            eqc_n->setDisequal( a );

-            eqc_a->setDisequal( n );

-            //setEqual( eqc_a, eqc_b, a, n, false );

-          }

-          eqc_n->setDisequal( b, false );

-        }

-      }

-      ////move all previous EqcRegistry's regarding equalities within b

-      //for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){

-      //  if( (*it).second ){

-      //    eqc_a->d_rel_eqr_e[(*it).first] = true;

-      //  }

-      //}

-    }

-    //process new equalities

-    //setEqual( eqc_a, eqc_b, a, b, true );

-    Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;

-  }

-  */

-}

-

-/** assert disequal */

-void QuantConflictFind::assertDisequal( Node a, Node b ) {

-  /*

-  a = getRepresentative( a );

-  b = getRepresentative( b );

-  Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;

-  EqcInfo * eqc_a = getEqcInfo( a );

-  EqcInfo * eqc_b = getEqcInfo( b );

-  if( !eqc_a->isDisequal( b ) ){

-    Assert( !eqc_b->isDisequal( a ) );

-    eqc_b->setDisequal( a );

-    eqc_a->setDisequal( b );

-    //setEqual( eqc_a, eqc_b, a, b, false );

-  }

-  Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;

-  */

-}

-

-//-------------------------------------------------- check function

-

-/** check */

-void QuantConflictFind::check( Theory::Effort level ) {

-  Trace("qcf-check") << "QCF : check : " << level << std::endl;

-  if( d_conflict ){

-    Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;

-    if( level>=Theory::EFFORT_FULL ){

-      Assert( false );

-    }

-  }else{

-    int addedLemmas = 0;

-    if( d_performCheck ){

-      ++(d_statistics.d_inst_rounds);

-      double clSet = 0;

-      if( Trace.isOn("qcf-engine") ){

-        clSet = double(clock())/double(CLOCKS_PER_SEC);

-        Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;

-      }

-      Trace("qcf-check") << "Compute relevant equalities..." << std::endl;

-      computeRelevantEqr();

-

-      if( Trace.isOn("qcf-debug") ){

-        Trace("qcf-debug") << std::endl;

-        debugPrint("qcf-debug");

-        Trace("qcf-debug") << std::endl;

-      }

-      short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;

-      for( short e = effort_conflict; e<=end_e; e++ ){

-        d_effort = e;

-        if( e == effort_prop_eq ){

-          for( unsigned i=0; i<2; i++ ){

-            d_prop_eq[i] = Node::null();

-          }

-        }

-        Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;

-        for( unsigned j=0; j<d_qassert.size(); j++ ){

-          Node q = d_qassert[j];

-          Trace("qcf-check") << "Check quantified formula ";

-          debugPrintQuant("qcf-check", q);

-          Trace("qcf-check") << " : " << q << "..." << std::endl;

-

-          Assert( d_qinfo.find( q )!=d_qinfo.end() );

-          if( d_qinfo[q].d_mg->isValid() ){

-            d_qinfo[q].reset_round( this );

-            //try to make a matches making the body false

-            d_qinfo[q].d_mg->reset( this, false, q );

-            while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){

-

-              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;

-              d_qinfo[q].debugPrintMatch("qcf-check");

-              Trace("qcf-check") << std::endl;

-

-              if( !d_qinfo[q].isMatchSpurious( this ) ){

-                std::vector< int > assigned;

-                if( d_qinfo[q].completeMatch( this, q, assigned ) ){

-                  InstMatch m;

-                  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

-                    //Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );

-                    int repVar = d_qinfo[q].getCurrentRepVar( i );

-                    Node cv;

-                    std::map< int, Node >::iterator itmt = d_qinfo[q].d_match_term.find( repVar );

-                    if( itmt!=d_qinfo[q].d_match_term.end() ){

-                      cv = itmt->second;

-                    }else{

-                      cv = d_qinfo[q].d_match[repVar];

-                    }

-

-

-                    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;

-                    m.set( d_quantEngine, q, i, cv );

-                  }

-                  if( Debug.isOn("qcf-check-inst") ){

-                    //if( e==effort_conflict ){

-                    Node inst = d_quantEngine->getInstantiation( q, m );

-                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

-                    Assert( evaluate( inst )!=1 );

-                    Assert( evaluate( inst )==-1 || e>effort_conflict );

-                    //}

-                  }

-                  if( d_quantEngine->addInstantiation( q, m ) ){

-                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;

-                    ++addedLemmas;

-                    if( e==effort_conflict ){

-                      d_conflict.set( true );

-                      ++(d_statistics.d_conflict_inst);

-                      break;

-                    }else if( e==effort_prop_eq ){

-                      ++(d_statistics.d_prop_inst);

-                    }

-                  }else{

-                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

-                    Assert( false );

-                  }

-                  //clean up assigned

-                  for( unsigned i=0; i<assigned.size(); i++ ){

-                    d_qinfo[q].d_match.erase( assigned[i] );

-                  }

-                }else{

-                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

-                }

-              }else{

-                Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;

-              }

-            }

-          }

-          if( d_conflict ){

-            break;

-          }

-        }

-        if( addedLemmas>0 ){

-          d_quantEngine->flushLemmas();

-          break;

-        }

-      }

-      if( Trace.isOn("qcf-engine") ){

-        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);

-        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);

-        if( addedLemmas>0 ){

-          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );

-          Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;

-        }

-        Trace("qcf-engine") << std::endl;

-      }

-    }

-    Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;

-  }

-}

-

-bool QuantConflictFind::needsCheck( Theory::Effort level ) {

-  d_performCheck = false;

-  if( !d_conflict ){

-    if( level==Theory::EFFORT_LAST_CALL ){

-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;

-    }else if( level==Theory::EFFORT_FULL ){

-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;

-    }else if( level==Theory::EFFORT_STANDARD ){

-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;

-    }

-  }

-  return d_performCheck;

-}

-

-void QuantConflictFind::computeRelevantEqr() {

-  d_uf_terms.clear();

-  d_eqc_uf_terms.clear();

-  d_eqcs.clear();

-  d_arg_reps.clear();

-  double clSet = 0;

-  if( Trace.isOn("qcf-opt") ){

-    clSet = double(clock())/double(CLOCKS_PER_SEC);

-  }

-

-  long nTermst = 0;

-  long nTerms = 0;

-  long nEqc = 0;

-

-  //which nodes are irrelevant for disequality matches

-  std::map< TNode, bool > irrelevant_dnode;

-  //now, store matches

-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );

-  while( !eqcs_i.isFinished() ){

-    nEqc++;

-    Node r = (*eqcs_i);

-    d_eqcs[r.getType()].push_back( r );

-    //EqcInfo * eqcir = getEqcInfo( r, false );

-    //get relevant nodes that we are disequal from

-    /*

-    std::vector< Node > deqc;

-    if( eqcir ){

-      for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){

-        if( (*it).second ){

-          //Node rd = (*it).first;

-          //if( rd!=getRepresentative( rd ) ){

-          //  std::cout << "Bad rep!" << std::endl;

-          //  exit( 0 );

-          //}

-          deqc.push_back( (*it).first );

-        }

-      }

-    }

-    */

-    //process disequalities

-    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

-    while( !eqc_i.isFinished() ){

-      TNode n = (*eqc_i);

-      if( n.getKind()!=EQUAL ){

-        nTermst++;

-        //node_to_rep[n] = r;

-        //if( n.getNumChildren()>0 ){

-        //  if( n.getKind()!=APPLY_UF ){

-        //    std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;

-        //  }

-        //}

-

-        bool isRedundant;

-        std::map< TNode, std::vector< TNode > >::iterator it_na;

-        TNode fn;

-        if( isHandledUfTerm( n ) ){

-          computeArgReps( n );

-          it_na = d_arg_reps.find( n );

-          Assert( it_na!=d_arg_reps.end() );

-          Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );

-          isRedundant = (nadd!=n);

-          d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );

-          if( !isRedundant ){

-            int jindex;

-            fn = getFunction( n, jindex );

-          }

-        }else{

-          isRedundant = false;

-        }

-        nTerms += isRedundant ? 0 : 1;

-      }

-      ++eqc_i;

-    }

-    //process_eqc[r] = true;

-    ++eqcs_i;

-  }

-  if( Trace.isOn("qcf-opt") ){

-    double clSet2 = double(clock())/double(CLOCKS_PER_SEC);

-    Trace("qcf-opt") << "Compute rel eqc : " << std::endl;

-    Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;

-    Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;

-    Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;

-  }

-}

-

-void QuantConflictFind::computeArgReps( TNode n ) {

-  if( d_arg_reps.find( n )==d_arg_reps.end() ){

-    Assert( isHandledUfTerm( n ) );

-    for( unsigned j=0; j<n.getNumChildren(); j++ ){

-      d_arg_reps[n].push_back( getRepresentative( n[j] ) );

-    }

-  }

-}

-bool QuantConflictFind::isHandledUfTerm( TNode n ) {

-  return n.getKind()==APPLY_UF;

-}

-

-void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {

+void QuantInfo::reset_round( QuantConflictFind * p ) {

   d_match.clear();

   d_match_term.clear();

   d_curr_var_deq.clear();

@@ -758,8 +101,8 @@ void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {
   }

 }

 

-int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {

-  std::map< int, Node >::iterator it = d_match.find( v );

+int QuantInfo::getCurrentRepVar( int v ) {

+  std::map< int, TNode >::iterator it = d_match.find( v );

   if( it!=d_match.end() ){

     int vn = getVarNum( it->second );

     if( vn!=-1 ){

@@ -772,12 +115,12 @@ int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {
   return v;

 }

 

-Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) {

+TNode QuantInfo::getCurrentValue( TNode n ) {

   int v = getVarNum( n );

   if( v==-1 ){

     return n;

   }else{

-    std::map< int, Node >::iterator it = d_match.find( v );

+    std::map< int, TNode >::iterator it = d_match.find( v );

     if( it==d_match.end() ){

       return n;

     }else{

@@ -787,24 +130,27 @@ Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) {
   }

 }

 

-bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n, bool chDiseq ) {

+bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {

   //check disequalities

-  for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){

-    Node cv = getCurrentValue( it->first );

-    Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;

-    if( cv==n ){

-      return false;

-    }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){

-      //they must actually be disequal if we are looking for conflicts

-      if( !p->areDisequal( n, cv ) ){

+  std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );

+  if( itd!=d_curr_var_deq.end() ){

+    for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){

+      Node cv = getCurrentValue( it->first );

+      Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;

+      if( cv==n ){

         return false;

+      }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){

+        //they must actually be disequal if we are looking for conflicts

+        if( !p->areDisequal( n, cv ) ){

+          return false;

+        }

       }

     }

   }

   return true;

 }

 

-int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, bool polarity ) {

+int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ) {

   v = getCurrentRepVar( v );

   int vn = getVarNum( n );

   vn = vn==-1 ? -1 : getCurrentRepVar( vn );

@@ -812,7 +158,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
   return addConstraint( p, v, n, vn, polarity, false );

 }

 

-int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove ) {

+int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ) {

   //for handling equalities between variables, and disequalities involving variables

   Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";

   Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;

@@ -824,16 +170,16 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
       if( doRemove ){

         if( vn!=-1 ){

           //if set to this in the opposite direction, clean up opposite instead

-          std::map< int, Node >::iterator itmn = d_match.find( vn );

+          std::map< int, TNode >::iterator itmn = d_match.find( vn );

           if( itmn!=d_match.end() && itmn->second==d_vars[v] ){

             return addConstraint( p, vn, d_vars[v], v, true, true );

           }else{

             //unsetting variables equal

-            std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( vn );

+            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );

             if( itd!=d_curr_var_deq.end() ){

               //remove disequalities owned by this

-              std::vector< Node > remDeq;

-              for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){

+              std::vector< TNode > remDeq;

+              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){

                 if( it->second==v ){

                   remDeq.push_back( it->first );

                 }

@@ -847,11 +193,11 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
         d_match.erase( v );

         return 1;

       }else{

-        std::map< int, Node >::iterator itm = d_match.find( v );

+        std::map< int, TNode >::iterator itm = d_match.find( v );

 

         if( vn!=-1 ){

           Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;

-          std::map< int, Node >::iterator itmn = d_match.find( vn );

+          std::map< int, TNode >::iterator itmn = d_match.find( vn );

           if( itm==d_match.end() ){

             //setting variables equal

             bool alreadySet = false;

@@ -861,9 +207,9 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
             }

 

             //copy or check disequalities

-            std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( v );

+            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );

             if( itd!=d_curr_var_deq.end() ){

-              for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){

+              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){

                 Node dv = getCurrentValue( it->first );

                 if( !alreadySet ){

                   if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){

@@ -925,9 +271,9 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
       }else{

         if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){

           //check if it respects equality

-          std::map< int, Node >::iterator itm = d_match.find( v );

+          std::map< int, TNode >::iterator itm = d_match.find( v );

           if( itm!=d_match.end() ){

-            Node nv = getCurrentValue( n );

+            TNode nv = getCurrentValue( n );

             if( !p->areMatchDisequal( nv, itm->second ) ){

               Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;

               return -1;

@@ -945,32 +291,28 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
   }

 }

 

-bool QuantConflictFind::QuantInfo::isConstrainedVar( int v ) {

-  //if( options::qcfMode()==QCF_CONFLICT_ONLY ){

-  //  return true;

-  //}else{

-    if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){

-      return true;

-    }else{

-      Node vv = getVar( v );

-      for( std::map< int, Node >::iterator it = d_match.begin(); it != d_match.end(); ++it ){

-        if( it->second==vv ){

-          return true;

-        }

+bool QuantInfo::isConstrainedVar( int v ) {

+  if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){

+    return true;

+  }else{

+    Node vv = getVar( v );

+    for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){

+      if( it->second==vv ){

+        return true;

       }

-      for( std::map< int, std::map< Node, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){

-        for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){

-          if( it2->first==vv ){

-            return true;

-          }

+    }

+    for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){

+      for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){

+        if( it2->first==vv ){

+          return true;

         }

       }

-      return false;

     }

-  //}

+    return false;

+  }

 }

 

-bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node n ) {

+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {

   if( getCurrentCanBeEqual( p, v, n ) ){

     Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " <<  d_curr_var_deq[v].size() << " disequalities" << std::endl;

     d_match[v] = n;

@@ -980,9 +322,9 @@ bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node
   }

 }

 

-bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {

+bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {

   for( int i=0; i<getNumVars(); i++ ){

-    std::map< int, Node >::iterator it = d_match.find( i );

+    std::map< int, TNode >::iterator it = d_match.find( i );

     if( it!=d_match.end() ){

       if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){

         return true;

@@ -992,7 +334,7 @@ bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   return false;

 }

 

-bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned ) {

+bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned ) {

   //assign values for variables that were unassigned (usually not necessary, but handles corner cases)

   Trace("qcf-check") << std::endl;

   std::vector< int > unassigned[2];

@@ -1023,7 +365,7 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q,
               if( !isConstrainedVar( unassigned[r][index] ) ){

                 eqc_count.push_back( -1 );

               }else{

-                d_var_mg[ unassigned[r][index] ]->reset( p, true, q );

+                d_var_mg[ unassigned[r][index] ]->reset( p, true, this );

                 eqc_count.push_back( 0 );

               }

             }else{

@@ -1034,7 +376,7 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q,
               if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){

                 Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl;

                 index++;

-              }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){

+              }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, this ) ){

                 Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl;

                 index++;

               }else{

@@ -1098,7 +440,7 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q,
   }

 }

 

-void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {

+void QuantInfo::debugPrintMatch( const char * c ) {

   for( int i=0; i<getNumVars(); i++ ){

     Trace(c) << "  " << d_vars[i] << " -> ";

     if( d_match.find( i )!=d_match.end() ){

@@ -1108,7 +450,7 @@ void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {
     }

     if( !d_curr_var_deq[i].empty() ){

       Trace(c) << ", DEQ{ ";

-      for( std::map< Node, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){

+      for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){

         Trace(c) << it->first << " ";

       }

       Trace(c) << "}";

@@ -1119,14 +461,14 @@ void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {
 

 /*

 struct MatchGenSort {

-  QuantConflictFind::MatchGen * d_mg;

+  MatchGen * d_mg;

   bool operator() (int i,int j) {

     return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;

   }

 };

 */

 

-QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){

+MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){

   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;

   std::vector< Node > qni_apps;

   d_qni_size = 0;

@@ -1231,11 +573,11 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
 }

 

 

-void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {

+void MatchGen::reset_round( QuantConflictFind * p ) {

   for( unsigned i=0; i<d_children.size(); i++ ){

     d_children[i].reset_round( p );

   }

-  for( std::map< int, Node >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){

+  for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){

     d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );

   }

   if( d_type==typ_ground ){

@@ -1254,7 +596,7 @@ void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {
   }

 }

 

-void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q ) {

+void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {

   d_tgt = d_type_not ? !tgt : tgt;

   Debug("qcf-match") << "     Reset for : " << d_n << ", type : ";

   debugPrintType( "qcf-match", d_type );

@@ -1265,7 +607,9 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
   d_child_counter = -1;

 

   //set up processing matches

-  if( d_type==typ_ground ){

+  if( d_type==typ_invalid ){

+    //d_child_counter = 0;

+  }else if( d_type==typ_ground ){

     if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){

       d_child_counter = 0;

     }

@@ -1282,22 +626,30 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
     Node nn[2];

     int vn[2];

     if( d_type==typ_pred ){

-      nn[0] = p->d_qinfo[q].getCurrentValue( d_n );

-      vn[0] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[0] ) );

+      nn[0] = qi->getCurrentValue( d_n );

+      vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );

       nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );

       vn[1] = -1;

       d_tgt = true;

     }else{

       for( unsigned i=0; i<2; i++ ){

-        nn[i] = p->d_qinfo[q].getCurrentValue( d_n[i] );

-        vn[i] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[i] ) );

+        nn[i] = qi->getCurrentValue( d_n[i] );

+        vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );

       }

     }

     bool success;

     if( vn[0]==-1 && vn[1]==-1 ){

       Debug("qcf-match-debug") << "       reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;

       //just compare values

-      success = d_tgt ? p->areMatchEqual( nn[0], nn[1] ) : p->areMatchDisequal( nn[0], nn[1] );

+      if( d_tgt ){

+        success = p->areMatchEqual( nn[0], nn[1] );

+      }else{

+        if( p->d_effort==QuantConflictFind::effort_conflict ){

+          success = p->areDisequal( nn[0], nn[1] );

+        }else{

+          success = p->areMatchDisequal( nn[0], nn[1] );

+        }

+      }

     }else{

       //otherwise, add a constraint to a variable

       if( vn[1]!=-1 && vn[0]==-1 ){

@@ -1310,7 +662,7 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
       }

       Debug("qcf-match-debug") << "       reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;

       //add some constraint

-      int addc = p->d_qinfo[q].addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );

+      int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );

       success = addc!=-1;

       //if successful and non-redundant, store that we need to cleanup this

       if( addc==1 ){

@@ -1334,18 +686,18 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q
     }else{

       //reset the first child to d_tgt

       d_child_counter = 0;

-      getChild( d_child_counter )->reset( p, d_tgt, q );

+      getChild( d_child_counter )->reset( p, d_tgt, qi );

     }

   }

   d_binding = false;

   Debug("qcf-match") << "     reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;

 }

 

-bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) {

+bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {

   Debug("qcf-match") << "     Get next match for : " << d_n << ", type = ";

   debugPrintType( "qcf-match", d_type );

   Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;

-  if( d_type==typ_ground ){

+  if( d_type==typ_invalid || d_type==typ_ground ){

     if( d_child_counter==0 ){

       d_child_counter = -1;

       return true;

@@ -1359,7 +711,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
       bool doReset = false;

       bool doFail = false;

       if( !d_binding ){

-        if( doMatching( p, q ) ){

+        if( doMatching( p, qi ) ){

           Debug("qcf-match-debug") << "     - Matching succeeded" << std::endl;

           d_binding = true;

           d_binding_it = d_qni_bound.begin();

@@ -1383,14 +735,14 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
           std::map< int, MatchGen * >::iterator itm;

           if( !doFail ){

             Debug("qcf-match-debug") << "       check variable " << d_binding_it->second << std::endl;

-            itm = p->d_qinfo[q].d_var_mg.find( d_binding_it->second );

+            itm = qi->d_var_mg.find( d_binding_it->second );

           }

-          if( doFail || ( d_binding_it->first!=0 && itm!=p->d_qinfo[q].d_var_mg.end() ) ){

+          if( doFail || ( d_binding_it->first!=0 && itm!=qi->d_var_mg.end() ) ){

             Debug("qcf-match-debug") << "       we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;

             if( doReset ){

-              itm->second->reset( p, true, q );

+              itm->second->reset( p, true, qi );

             }

-            if( doFail || !itm->second->getNextMatch( p, q ) ){

+            if( doFail || !itm->second->getNextMatch( p, qi ) ){

               do {

                 if( d_binding_it==d_qni_bound.begin() ){

                   Debug("qcf-match-debug") << "       failed." << std::endl;

@@ -1399,7 +751,7 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
                   Debug("qcf-match-debug") << "       decrement..." << std::endl;

                   --d_binding_it;

                 }

-              }while( success && ( d_binding_it->first==0 || p->d_qinfo[q].d_var_mg.find( d_binding_it->second )==p->d_qinfo[q].d_var_mg.end() ) );

+              }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );

               doReset = false;

               doFail = false;

             }else{

@@ -1426,12 +778,12 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
     //if not successful, clean up the variables you bound

     if( !success ){

       if( d_type==typ_eq || d_type==typ_pred ){

-        for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){

+        for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){

           if( !it->second.isNull() ){

             Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;

             std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );

             int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;

-            p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true );

+            qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );

           }

         }

         d_qni_bound_cons.clear();

@@ -1441,9 +793,9 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
         //clean up the match : remove equalities/disequalities

         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){

           Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;

-          Assert( it->second<p->d_qinfo[q].getNumVars() );

-          p->d_qinfo[q].d_match.erase( it->second );

-          p->d_qinfo[q].d_match_term.erase( it->second );

+          Assert( it->second<qi->getNumVars() );

+          qi->d_match.erase( it->second );

+          qi->d_match_term.erase( it->second );

         }

         d_qni_bound.clear();

       }

@@ -1458,11 +810,11 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
         if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){

           if( (d_n.getKind()==AND)==d_tgt ){

             //all children must match simultaneously

-            if( getChild( d_child_counter )->getNextMatch( p, q ) ){

+            if( getChild( d_child_counter )->getNextMatch( p, qi ) ){

               if( d_child_counter<(int)(getNumChildren()-1) ){

                 d_child_counter++;

                 Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << std::endl;

-                getChild( d_child_counter )->reset( p, d_tgt, q );

+                getChild( d_child_counter )->reset( p, d_tgt, qi );

               }else{

                 success = true;

               }

@@ -1471,11 +823,11 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
             }

           }else{

             //one child must match

-            if( !getChild( d_child_counter )->getNextMatch( p, q ) ){

+            if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){

               if( d_child_counter<(int)(getNumChildren()-1) ){

                 d_child_counter++;

                 Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;

-                getChild( d_child_counter )->reset( p, d_tgt, q );

+                getChild( d_child_counter )->reset( p, d_tgt, qi );

               }else{

                 d_child_counter = -1;

               }

@@ -1486,20 +838,20 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
         }else if( d_n.getKind()==IFF ){

           //construct match based on both children

           if( d_child_counter%2==0 ){

-            if( getChild( 0 )->getNextMatch( p, q ) ){

+            if( getChild( 0 )->getNextMatch( p, qi ) ){

               d_child_counter++;

-              getChild( 1 )->reset( p, d_child_counter==1, q );

+              getChild( 1 )->reset( p, d_child_counter==1, qi );

             }else{

               if( d_child_counter==0 ){

                 d_child_counter = 2;

-                getChild( 0 )->reset( p, !d_tgt, q );

+                getChild( 0 )->reset( p, !d_tgt, qi );

               }else{

                 d_child_counter = -1;

               }

             }

           }

           if( d_child_counter%2==1 ){

-            if( getChild( 1 )->getNextMatch( p, q ) ){

+            if( getChild( 1 )->getNextMatch( p, qi ) ){

               success = true;

             }else{

               d_child_counter--;

@@ -1508,21 +860,21 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
         }else if( d_n.getKind()==ITE ){

           if( d_child_counter%2==0 ){

             int index1 = d_child_counter==4 ? 1 : 0;

-            if( getChild( index1 )->getNextMatch( p, q ) ){

+            if( getChild( index1 )->getNextMatch( p, qi ) ){

               d_child_counter++;

-              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, q );

+              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, qi );

             }else{

               if( d_child_counter==4 ){

                 d_child_counter = -1;

               }else{

                 d_child_counter +=2;

-                getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, q );

+                getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );

               }

             }

           }

           if( d_child_counter%2==1 ){

             int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);

-            if( getChild( index2 )->getNextMatch( p, q ) ){

+            if( getChild( index2 )->getNextMatch( p, qi ) ){

               success = true;

             }else{

               d_child_counter--;

@@ -1538,12 +890,13 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
   return false;

 }

 

-bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {

+bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {

   if( !d_qn.empty() ){

     if( d_qn[0]==NULL ){

       d_qn.clear();

       return true;

     }else{

+      Assert( d_type==typ_var );

       Assert( d_qni_size>0 );

       bool invalidMatch;

       do {

@@ -1556,11 +909,11 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
           std::map< int, int >::iterator itv = d_qni_var_num.find( index );

           if( itv!=d_qni_var_num.end() ){

             //get the representative variable this variable is equal to

-            int repVar = p->d_qinfo[q].getCurrentRepVar( itv->second );

+            int repVar = qi->getCurrentRepVar( itv->second );

             Debug("qcf-match-debug") << "       Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;

             //get the value the rep variable

-            std::map< int, Node >::iterator itm = p->d_qinfo[q].d_match.find( repVar );

-            if( itm!=p->d_qinfo[q].d_match.end() ){

+            std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );

+            if( itm!=qi->d_match.end() ){

               val = itm->second;

               Assert( !val.isNull() );

               Debug("qcf-match-debug") << "       Variable is already bound to " << val << std::endl;

@@ -1571,7 +924,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
               if( it != d_qn[index]->d_children.end() ) {

                 d_qni.push_back( it );

                 //set the match

-                if( p->d_qinfo[q].setMatch( p, d_qni_bound[index], it->first ) ){

+                if( qi->setMatch( p, d_qni_bound[index], it->first ) ){

                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;

                   if( d_qn.size()<d_qni_size ){

                     d_qn.push_back( &it->second );

@@ -1616,7 +969,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
             d_qni[index]++;

             if( d_qni[index]!=d_qn[index]->d_children.end() ){

               success = true;

-              if( p->d_qinfo[q].setMatch( p, itb->second, d_qni[index]->first ) ){

+              if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){

                 Debug("qcf-match-debug") << "       Bind next variable" << std::endl;

                 if( d_qn.size()<d_qni_size ){

                   d_qn.push_back( &d_qni[index]->second );

@@ -1643,14 +996,14 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
         //Debug("qcf-match-debug") << "       We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;

         Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );

         Node t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;

-        Debug("qcf-match-debug") << "       We matched " << t << std::endl;

+        Debug("qcf-match-debug") << "       " << d_n << " matched " << t << std::endl;

         //set the match terms

         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){

-          if( it->second<(int)q[0].getNumChildren() ){   //if it is an actual variable, we are interested in knowing the actual term

-            Assert( it->first>0 );

-            Assert( p->d_qinfo[q].d_match.find( it->second )!=p->d_qinfo[q].d_match.end() );

-            Assert( p->areEqual( t[it->first-1], p->d_qinfo[q].d_match[ it->second ] ) );

-            p->d_qinfo[q].d_match_term[it->second] = t[it->first-1];

+          Debug("qcf-match-debug") << "       position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;

+          if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){   //if it is an actual variable, we are interested in knowing the actual term

+            Assert( qi->d_match.find( it->second )!=qi->d_match.end() );

+            Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );

+            qi->d_match_term[it->second] = t[it->first-1];

           }

         }

       }

@@ -1659,7 +1012,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {
   return !d_qn.empty();

 }

 

-void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {

+void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {

   if( isTrace ){

     switch( typ ){

     case typ_invalid: Trace(c) << "invalid";break;

@@ -1683,12 +1036,679 @@ void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, boo
   }

 }

 

-void QuantConflictFind::MatchGen::setInvalid() {

+void MatchGen::setInvalid() {

   d_type = typ_invalid;

   d_children.clear();

 }

 

 

+

+QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :

+QuantifiersModule( qe ),

+d_c( c ),

+d_conflict( c, false ),

+d_qassert( c ) {

+  d_fid_count = 0;

+  d_true = NodeManager::currentNM()->mkConst<bool>(true);

+  d_false = NodeManager::currentNM()->mkConst<bool>(false);

+}

+

+Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {

+  if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){

+    index = 0;

+    return n;

+  }else if( isHandledUfTerm( n ) ){

+    /*

+    std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );

+    if( it==d_op_node.end() ){

+      std::vector< Node > children;

+      children.push_back( n.getOperator() );

+      for( unsigned i=0; i<n.getNumChildren(); i++ ){

+        children.push_back( getFv( n[i].getType() ) );

+      }

+      Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );

+      d_op_node[n.getOperator()] = nn;

+      return nn;

+    }else{

+      return it->second;

+    }*/

+    index = 1;

+    return n.getOperator();

+  }else{

+    return Node::null();

+  }

+}

+

+Node QuantConflictFind::mkEqNode( Node a, Node b ) {

+  if( a.getType().isBoolean() ){

+    return a.iffNode( b );

+  }else{

+    return a.eqNode( b );

+  }

+}

+

+//-------------------------------------------------- registration

+

+void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {

+  if( n.getKind()==FORALL ){

+    //do nothing

+  }else{

+    //qcf->d_node = n;

+    bool recurse = true;

+    if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){

+      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

+        //literals

+

+        /*

+          if( n.getKind()==APPLY_UF || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){

+            for( unsigned i=0; i<n.getNumChildren(); i++ ){

+              flatten( q, n[i] );

+            }

+          }else if( n.getKind()==EQUAL ){

+            for( unsigned i=0; i<n.getNumChildren(); i++ ){

+              for( unsigned j=0; j<n[i].getNumChildren(); j++ ){

+                flatten( q, n[i][j] );

+              }

+            }

+          }

+

+          */

+

+        if( n.getKind()==APPLY_UF ){

+          flatten( q, n );

+        }else if( n.getKind()==EQUAL ){

+          for( unsigned i=0; i<n.getNumChildren(); i++ ){

+            flatten( q, n[i] );

+          }

+        }

+

+      }else{

+        Trace("qcf-qregister") << "    RegisterGroundLit : " << n;

+      }

+      recurse = false;

+    }

+    if( recurse ){

+      for( unsigned i=0; i<n.getNumChildren(); i++ ){

+        bool newHasPol;

+        bool newPol;

+        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );

+        //QcfNode * qcfc = new QcfNode( d_c );

+        //qcfc->d_parent = qcf;

+        //qcf->d_child[i] = qcfc;

+        registerNode( q, n[i], newHasPol, newPol );

+      }

+    }

+  }

+}

+

+void QuantConflictFind::flatten( Node q, Node n ) {

+  if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){

+    if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){

+      //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;

+      d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();

+      d_qinfo[q].d_vars.push_back( n );

+    }

+    for( unsigned i=0; i<n.getNumChildren(); i++ ){

+      flatten( q, n[i] );

+    }

+  }

+}

+

+void QuantConflictFind::registerQuantifier( Node q ) {

+  d_quants.push_back( q );

+  d_quant_id[q] = d_quants.size();

+  d_qinfo[q].d_q = q;

+  Trace("qcf-qregister") << "Register ";

+  debugPrintQuant( "qcf-qregister", q );

+  Trace("qcf-qregister") << " : " << q << std::endl;

+

+  //register the variables

+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

+    d_qinfo[q].d_var_num[q[0][i]] = i;

+    d_qinfo[q].d_vars.push_back( q[0][i] );

+  }

+

+  //make QcfNode structure

+  Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;

+  //d_qinfo[q].d_cf = new QcfNode( d_c );

+  registerNode( q, q[1], true, true );

+

+  //debug print

+  Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;

+  Trace("qcf-qregister") << "    ";

+  debugPrintQuantBody( "qcf-qregister", q, q[1] );

+  Trace("qcf-qregister") << std::endl;

+  if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){

+    Trace("qcf-qregister") << "  with additional constraints : " << std::endl;

+    for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){

+      Trace("qcf-qregister") << "    ?x" << j << " = ";

+      debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );

+      Trace("qcf-qregister") << std::endl;

+    }

+  }

+

+  Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;

+  d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );

+

+  for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){

+    d_qinfo[q].d_var_mg[j] = new MatchGen( this, q, d_qinfo[q].d_vars[j], false, true );

+    if( !d_qinfo[q].d_var_mg[j]->isValid() ){

+      d_qinfo[q].d_mg->setInvalid();

+      break;

+    }

+  }

+

+  Trace("qcf-qregister") << "Done registering quantifier." << std::endl;

+}

+

+int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {

+  int ret = 0;

+  if( n.getKind()==EQUAL ){

+    Node n1 = evaluateTerm( n[0] );

+    Node n2 = evaluateTerm( n[1] );

+    Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;

+    if( areEqual( n1, n2 ) ){

+      ret = 1;

+    }else if( areDisequal( n1, n2 ) ){

+      ret = -1;

+    }

+    //else if( d_effort>QuantConflictFind::effort_conflict ){

+    //  ret = -1;

+    //}

+  }else if( n.getKind()==APPLY_UF ){  //predicate

+    Node nn = evaluateTerm( n );

+    Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;

+    if( areEqual( nn, d_true ) ){

+      ret = 1;

+    }else if( areEqual( nn, d_false ) ){

+      ret = -1;

+    }

+    //else if( d_effort>QuantConflictFind::effort_conflict ){

+    //  ret = -1;

+    //}

+  }else if( n.getKind()==NOT ){

+    return -evaluate( n[0] );

+  }else if( n.getKind()==ITE ){

+    int cev1 = evaluate( n[0] );

+    int cevc[2] = { 0, 0 };

+    for( unsigned i=0; i<2; i++ ){

+      if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){

+        cevc[i] = evaluate( n[i+1] );

+        if( cev1!=0 ){

+          ret = cevc[i];

+          break;

+        }else if( cevc[i]==0 ){

+          break;

+        }

+      }

+    }

+    if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){

+      ret = cevc[0];

+    }

+  }else if( n.getKind()==IFF ){

+    int cev1 = evaluate( n[0] );

+    if( cev1!=0 ){

+      int cev2 = evaluate( n[1] );

+      if( cev2!=0 ){

+        ret = cev1==cev2 ? 1 : -1;

+      }

+    }

+

+  }else{

+    int ssval = 0;

+    if( n.getKind()==OR ){

+      ssval = 1;

+    }else if( n.getKind()==AND ){

+      ssval = -1;

+    }

+    bool isUnk = false;

+    for( unsigned i=0; i<n.getNumChildren(); i++ ){

+      int cev = evaluate( n[i] );

+      if( cev==ssval ){

+        ret = ssval;

+        break;

+      }else if( cev==0 ){

+        isUnk = true;

+      }

+    }

+    if( ret==0 && !isUnk ){

+      ret = -ssval;

+    }

+  }

+  Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;

+  return ret;

+}

+

+bool QuantConflictFind::isPropagationSet() {

+  return !d_prop_eq[0].isNull();

+}

+

+bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {

+  //if( d_effort==QuantConflictFind::effort_prop_deq ){

+  //  return n1==n2 || !areDisequal( n1, n2 );

+  //}else{

+  return n1==n2;

+  //}

+}

+

+bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {

+  //if( d_effort==QuantConflictFind::effort_conflict ){

+  //  return areDisequal( n1, n2 );

+  //}else{

+  return n1!=n2;

+  //}

+}

+

+//-------------------------------------------------- handling assertions / eqc

+

+void QuantConflictFind::assertNode( Node q ) {

+  Trace("qcf-proc") << "QCF : assertQuantifier : ";

+  debugPrintQuant("qcf-proc", q);

+  Trace("qcf-proc") << std::endl;

+  d_qassert.push_back( q );

+  //set the eqRegistries that this depends on to true

+  //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){

+  //  it->first->d_active.set( true );

+  //}

+}

+

+eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {

+  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();

+  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();

+}

+bool QuantConflictFind::areEqual( Node n1, Node n2 ) {

+  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );

+}

+bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {

+  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );

+}

+Node QuantConflictFind::getRepresentative( Node n ) {

+  if( getEqualityEngine()->hasTerm( n ) ){

+    return getEqualityEngine()->getRepresentative( n );

+  }else{

+    return n;

+  }

+}

+Node QuantConflictFind::evaluateTerm( Node n ) {

+  if( isHandledUfTerm( n ) ){

+    Node nn;

+    if( getEqualityEngine()->hasTerm( n ) ){

+      computeArgReps( n );

+      nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );

+    }else{

+      std::vector< TNode > args;

+      for( unsigned i=0; i<n.getNumChildren(); i++ ){

+        Node c = evaluateTerm( n[i] );

+        args.push_back( c );

+      }

+      nn = d_uf_terms[n.getOperator()].existsTerm( n, args );

+    }

+    if( !nn.isNull() ){

+      Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;

+      return getRepresentative( nn );

+    }else{

+      Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;

+      return n;

+    }

+  }

+  return getRepresentative( n );

+}

+

+/*

+QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {

+  std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );

+  if( it2==d_eqc_info.end() ){

+    if( doCreate ){

+      EqcInfo * eqci = new EqcInfo( d_c );

+      d_eqc_info[n] = eqci;

+      return eqci;

+    }else{

+      return NULL;

+    }

+  }

+  return it2->second;

+}

+*/

+

+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {

+  std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );

+  if( itut==d_eqc_uf_terms.end() ){

+    return NULL;

+  }else{

+    if( eqc.isNull() ){

+      return &itut->second;

+    }else{

+      std::map< TNode, QcfNodeIndex >::iterator itute = itut->second.d_children.find( eqc );

+      if( itute!=itut->second.d_children.end() ){

+        return &itute->second;

+      }else{

+        return NULL;

+      }

+    }

+  }

+}

+

+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {

+  std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );

+  if( itut!=d_uf_terms.end() ){

+    return &itut->second;

+  }else{

+    return NULL;

+  }

+}

+

+/** new node */

+void QuantConflictFind::newEqClass( Node n ) {

+  //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;

+  //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;

+}

+

+/** merge */

+void QuantConflictFind::merge( Node a, Node b ) {

+  /*

+  if( b.getKind()==EQUAL ){

+    if( a==d_true ){

+      //will merge anyways

+      //merge( b[0], b[1] );

+    }else if( a==d_false ){

+      assertDisequal( b[0], b[1] );

+    }

+  }else{

+    Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;

+    EqcInfo * eqc_b = getEqcInfo( b, false );

+    EqcInfo * eqc_a = NULL;

+    if( eqc_b ){

+      eqc_a = getEqcInfo( a );

+      //move disequalities of b into a

+      for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){

+        if( (*it).second ){

+          Node n = (*it).first;

+          EqcInfo * eqc_n = getEqcInfo( n, false );

+          Assert( eqc_n );

+          if( !eqc_n->isDisequal( a ) ){

+            Assert( !eqc_a->isDisequal( n ) );

+            eqc_n->setDisequal( a );

+            eqc_a->setDisequal( n );

+            //setEqual( eqc_a, eqc_b, a, n, false );

+          }

+          eqc_n->setDisequal( b, false );

+        }

+      }

+      ////move all previous EqcRegistry's regarding equalities within b

+      //for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){

+      //  if( (*it).second ){

+      //    eqc_a->d_rel_eqr_e[(*it).first] = true;

+      //  }

+      //}

+    }

+    //process new equalities

+    //setEqual( eqc_a, eqc_b, a, b, true );

+    Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;

+  }

+  */

+}

+

+/** assert disequal */

+void QuantConflictFind::assertDisequal( Node a, Node b ) {

+  /*

+  a = getRepresentative( a );

+  b = getRepresentative( b );

+  Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;

+  EqcInfo * eqc_a = getEqcInfo( a );

+  EqcInfo * eqc_b = getEqcInfo( b );

+  if( !eqc_a->isDisequal( b ) ){

+    Assert( !eqc_b->isDisequal( a ) );

+    eqc_b->setDisequal( a );

+    eqc_a->setDisequal( b );

+    //setEqual( eqc_a, eqc_b, a, b, false );

+  }

+  Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;

+  */

+}

+

+//-------------------------------------------------- check function

+

+/** check */

+void QuantConflictFind::check( Theory::Effort level ) {

+  Trace("qcf-check") << "QCF : check : " << level << std::endl;

+  if( d_conflict ){

+    Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;

+    if( level>=Theory::EFFORT_FULL ){

+      Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;

+      //Assert( false );

+    }

+  }else{

+    int addedLemmas = 0;

+    if( d_performCheck ){

+      ++(d_statistics.d_inst_rounds);

+      double clSet = 0;

+      if( Trace.isOn("qcf-engine") ){

+        clSet = double(clock())/double(CLOCKS_PER_SEC);

+        Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;

+      }

+      Trace("qcf-check") << "Compute relevant equalities..." << std::endl;

+      computeRelevantEqr();

+

+      if( Trace.isOn("qcf-debug") ){

+        Trace("qcf-debug") << std::endl;

+        debugPrint("qcf-debug");

+        Trace("qcf-debug") << std::endl;

+      }

+      short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;

+      for( short e = effort_conflict; e<=end_e; e++ ){

+        d_effort = e;

+        if( e == effort_prop_eq ){

+          for( unsigned i=0; i<2; i++ ){

+            d_prop_eq[i] = Node::null();

+          }

+        }

+        Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;

+        for( unsigned j=0; j<d_qassert.size(); j++ ){

+          Node q = d_qassert[j];

+          QuantInfo * qi = &d_qinfo[q];

+          Trace("qcf-check") << "Check quantified formula ";

+          debugPrintQuant("qcf-check", q);

+          Trace("qcf-check") << " : " << q << "..." << std::endl;

+

+          Assert( d_qinfo.find( q )!=d_qinfo.end() );

+          if( qi->d_mg->isValid() ){

+            qi->reset_round( this );

+            //try to make a matches making the body false

+            qi->d_mg->reset( this, false, qi );

+            while( qi->d_mg->getNextMatch( this, qi ) ){

+

+              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;

+              qi->debugPrintMatch("qcf-check");

+              Trace("qcf-check") << std::endl;

+

+              if( !qi->isMatchSpurious( this ) ){

+                std::vector< int > assigned;

+                if( qi->completeMatch( this, assigned ) ){

+                  InstMatch m;

+                  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

+                    //Node cv = qi->getCurrentValue( qi->d_match[i] );

+                    int repVar = qi->getCurrentRepVar( i );

+                    Node cv;

+                    std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );

+                    if( itmt!=qi->d_match_term.end() ){

+                      cv = itmt->second;

+                    }else{

+                      cv = qi->d_match[repVar];

+                    }

+

+

+                    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;

+                    m.set( d_quantEngine, q, i, cv );

+                  }

+                  if( Debug.isOn("qcf-check-inst") ){

+                    //if( e==effort_conflict ){

+                    Node inst = d_quantEngine->getInstantiation( q, m );

+                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

+                    Assert( evaluate( inst )!=1 );

+                    Assert( evaluate( inst )==-1 || e>effort_conflict );

+                    //}

+                  }

+                  if( d_quantEngine->addInstantiation( q, m ) ){

+                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;

+                    ++addedLemmas;

+                    if( e==effort_conflict ){

+                      d_conflict.set( true );

+                      ++(d_statistics.d_conflict_inst);

+                      break;

+                    }else if( e==effort_prop_eq ){

+                      ++(d_statistics.d_prop_inst);

+                    }

+                  }else{

+                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

+                    //Assert( false );

+                  }

+                  //clean up assigned

+                  for( unsigned i=0; i<assigned.size(); i++ ){

+                    qi->d_match.erase( assigned[i] );

+                  }

+                }else{

+                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

+                }

+              }else{

+                Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;

+              }

+            }

+          }

+          if( d_conflict ){

+            break;

+          }

+        }

+        if( addedLemmas>0 ){

+          d_quantEngine->flushLemmas();

+          break;

+        }

+      }

+      if( Trace.isOn("qcf-engine") ){

+        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);

+        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);

+        if( addedLemmas>0 ){

+          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );

+          Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;

+        }

+        Trace("qcf-engine") << std::endl;

+      }

+    }

+    Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;

+  }

+}

+

+bool QuantConflictFind::needsCheck( Theory::Effort level ) {

+  d_performCheck = false;

+  if( !d_conflict ){

+    if( level==Theory::EFFORT_LAST_CALL ){

+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;

+    }else if( level==Theory::EFFORT_FULL ){

+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;

+    }else if( level==Theory::EFFORT_STANDARD ){

+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;

+    }

+  }

+  return d_performCheck;

+}

+

+void QuantConflictFind::computeRelevantEqr() {

+  d_uf_terms.clear();

+  d_eqc_uf_terms.clear();

+  d_eqcs.clear();

+  d_arg_reps.clear();

+  double clSet = 0;

+  if( Trace.isOn("qcf-opt") ){

+    clSet = double(clock())/double(CLOCKS_PER_SEC);

+  }

+

+  long nTermst = 0;

+  long nTerms = 0;

+  long nEqc = 0;

+

+  //which nodes are irrelevant for disequality matches

+  std::map< TNode, bool > irrelevant_dnode;

+  //now, store matches

+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );

+  while( !eqcs_i.isFinished() ){

+    nEqc++;

+    Node r = (*eqcs_i);

+    d_eqcs[r.getType()].push_back( r );

+    //EqcInfo * eqcir = getEqcInfo( r, false );

+    //get relevant nodes that we are disequal from

+    /*

+    std::vector< Node > deqc;

+    if( eqcir ){

+      for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){

+        if( (*it).second ){

+          //Node rd = (*it).first;

+          //if( rd!=getRepresentative( rd ) ){

+          //  std::cout << "Bad rep!" << std::endl;

+          //  exit( 0 );

+          //}

+          deqc.push_back( (*it).first );

+        }

+      }

+    }

+    */

+    //process disequalities

+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

+    while( !eqc_i.isFinished() ){

+      TNode n = (*eqc_i);

+      if( n.getKind()!=EQUAL ){

+        nTermst++;

+        //node_to_rep[n] = r;

+        //if( n.getNumChildren()>0 ){

+        //  if( n.getKind()!=APPLY_UF ){

+        //    std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;

+        //  }

+        //}

+

+        bool isRedundant;

+        std::map< TNode, std::vector< TNode > >::iterator it_na;

+        TNode fn;

+        if( isHandledUfTerm( n ) ){

+          computeArgReps( n );

+          it_na = d_arg_reps.find( n );

+          Assert( it_na!=d_arg_reps.end() );

+          Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );

+          isRedundant = (nadd!=n);

+          d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );

+          if( !isRedundant ){

+            int jindex;

+            fn = getFunction( n, jindex );

+          }

+        }else{

+          isRedundant = false;

+        }

+        nTerms += isRedundant ? 0 : 1;

+      }

+      ++eqc_i;

+    }

+    //process_eqc[r] = true;

+    ++eqcs_i;

+  }

+  if( Trace.isOn("qcf-opt") ){

+    double clSet2 = double(clock())/double(CLOCKS_PER_SEC);

+    Trace("qcf-opt") << "Compute rel eqc : " << std::endl;

+    Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;

+    Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;

+    Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;

+  }

+}

+

+void QuantConflictFind::computeArgReps( TNode n ) {

+  if( d_arg_reps.find( n )==d_arg_reps.end() ){

+    Assert( isHandledUfTerm( n ) );

+    for( unsigned j=0; j<n.getNumChildren(); j++ ){

+      d_arg_reps[n].push_back( getRepresentative( n[j] ) );

+    }

+  }

+}

+bool QuantConflictFind::isHandledUfTerm( TNode n ) {

+  return n.getKind()==APPLY_UF;

+}

+

+

 //-------------------------------------------------- debugging

 

 

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index d8fe1e808..5ba7684ef 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -38,9 +38,99 @@ public:
   Node addTerm( TNode n, std::vector< TNode >& reps, int index = 0 );

 };

 

+class QuantInfo;

+

+//match generator

+class MatchGen {

+private:

+  //current children information

+  int d_child_counter;

+  //children of this object

+  //std::vector< int > d_children_order;

+  unsigned getNumChildren() { return d_children.size(); }

+  //MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }

+  MatchGen * getChild( int i ) { return &d_children[i]; }

+  //current matching information

+  std::vector< QcfNodeIndex * > d_qn;

+  std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni;

+  bool doMatching( QuantConflictFind * p, QuantInfo * qi );

+  //for matching : each index is either a variable or a ground term

+  unsigned d_qni_size;

+  std::map< int, int > d_qni_var_num;

+  std::map< int, TNode > d_qni_gterm;

+  std::map< int, TNode > d_qni_gterm_rep;

+  std::map< int, int > d_qni_bound;

+  std::map< int, TNode > d_qni_bound_cons;

+  std::map< int, int > d_qni_bound_cons_var;

+  std::map< int, int >::iterator d_binding_it;

+  bool d_binding;

+  //int getVarBindingVar();

+  std::map< int, Node > d_ground_eval;

+public:

+  //type of the match generator

+  enum {

+    typ_invalid,

+    typ_ground,

+    typ_pred,

+    typ_eq,

+    typ_formula,

+    typ_var,

+    typ_top,

+  };

+  void debugPrintType( const char * c, short typ, bool isTrace = false );

+public:

+  MatchGen() : d_type( typ_invalid ){}

+  MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false );

+  bool d_tgt;

+  Node d_n;

+  std::vector< MatchGen > d_children;

+  short d_type;

+  bool d_type_not;

+  void reset_round( QuantConflictFind * p );

+  void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );

+  bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );

+  bool isValid() { return d_type!=typ_invalid; }

+  void setInvalid();

+};

+

+//info for quantifiers

+class QuantInfo {

+public:

+  QuantInfo() : d_mg( NULL ) {}

+  std::vector< TNode > d_vars;

+  std::map< TNode, int > d_var_num;

+  //std::map< EqRegistry *, bool > d_rel_eqr;

+  std::map< int, std::vector< Node > > d_var_constraint[2];

+  int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }

+  bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }

+  int getNumVars() { return (int)d_vars.size(); }

+  TNode getVar( int i ) { return d_vars[i]; }

+  MatchGen * d_mg;

+  Node d_q;

+  std::map< int, MatchGen * > d_var_mg;

+  void reset_round( QuantConflictFind * p );

+public:

+  //current constraints

+  std::map< int, TNode > d_match;

+  std::map< int, TNode > d_match_term;

+  std::map< int, std::map< TNode, int > > d_curr_var_deq;

+  int getCurrentRepVar( int v );

+  TNode getCurrentValue( TNode n );

+  bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );

+  int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );

+  int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );

+  bool setMatch( QuantConflictFind * p, int v, TNode n );

+  bool isMatchSpurious( QuantConflictFind * p );

+  bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned );

+  void debugPrintMatch( const char * c );

+  bool isConstrainedVar( int v );

+};

+

 class QuantConflictFind : public QuantifiersModule

 {

   friend class QcfNodeIndex;

+  friend class MatchGen;

+  friend class QuantInfo;

   typedef context::CDChunkList<Node> NodeList;

   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;

 private:

@@ -62,93 +152,9 @@ public:  //for ground terms
 private:

   Node evaluateTerm( Node n );

   int evaluate( Node n, bool pref = false, bool hasPref = false );

-public:  //for quantifiers

-  //match generator

-  class MatchGen {

-  private:

-    //current children information

-    int d_child_counter;

-    //children of this object

-    //std::vector< int > d_children_order;

-    unsigned getNumChildren() { return d_children.size(); }

-    //MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }

-    MatchGen * getChild( int i ) { return &d_children[i]; }

-    //current matching information

-    std::vector< QcfNodeIndex * > d_qn;

-    std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni;

-    bool doMatching( QuantConflictFind * p, Node q );

-    //for matching : each index is either a variable or a ground term

-    unsigned d_qni_size;

-    std::map< int, int > d_qni_var_num;

-    std::map< int, Node > d_qni_gterm;

-    std::map< int, Node > d_qni_gterm_rep;

-    std::map< int, int > d_qni_bound;

-    std::map< int, Node > d_qni_bound_cons;

-    std::map< int, int > d_qni_bound_cons_var;

-    std::map< int, int >::iterator d_binding_it;

-    bool d_binding;

-    //int getVarBindingVar();

-    std::map< int, Node > d_ground_eval;

-  public:

-    //type of the match generator

-    enum {

-      typ_invalid,

-      typ_ground,

-      typ_pred,

-      typ_eq,

-      typ_formula,

-      typ_var,

-      typ_top,

-    };

-    void debugPrintType( const char * c, short typ, bool isTrace = false );

-  public:

-    MatchGen() : d_type( typ_invalid ){}

-    MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false );

-    bool d_tgt;

-    Node d_n;

-    std::vector< MatchGen > d_children;

-    short d_type;

-    bool d_type_not;

-    void reset_round( QuantConflictFind * p );

-    void reset( QuantConflictFind * p, bool tgt, Node q );

-    bool getNextMatch( QuantConflictFind * p, Node q );

-    bool isValid() { return d_type!=typ_invalid; }

-    void setInvalid();

-  };

 private:

   //currently asserted quantifiers

   NodeList d_qassert;

-  //info for quantifiers

-  class QuantInfo {

-  public:

-    QuantInfo() : d_mg( NULL ) {}

-    std::vector< Node > d_vars;

-    std::map< Node, int > d_var_num;

-    //std::map< EqRegistry *, bool > d_rel_eqr;

-    std::map< int, std::vector< Node > > d_var_constraint[2];

-    int getVarNum( Node v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }

-    bool isVar( Node v ) { return d_var_num.find( v )!=d_var_num.end(); }

-    int getNumVars() { return (int)d_vars.size(); }

-    Node getVar( int i ) { return d_vars[i]; }

-    MatchGen * d_mg;

-    std::map< int, MatchGen * > d_var_mg;

-    void reset_round( QuantConflictFind * p );

-  public:

-    //current constraints

-    std::map< int, Node > d_match;

-    std::map< int, Node > d_match_term;

-    std::map< int, std::map< Node, int > > d_curr_var_deq;

-    int getCurrentRepVar( int v );

-    Node getCurrentValue( Node n );

-    bool getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n, bool chDiseq = false );

-    int addConstraint( QuantConflictFind * p, int v, Node n, bool polarity );

-    int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove );

-    bool setMatch( QuantConflictFind * p, int v, Node n );

-    bool isMatchSpurious( QuantConflictFind * p );

-    bool completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned );

-    void debugPrintMatch( const char * c );

-    bool isConstrainedVar( int v );

-  };

   std::map< Node, QuantInfo > d_qinfo;

 private:  //for equivalence classes

   eq::EqualityEngine * getEqualityEngine();

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index b079ae75c..33d658e0a 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -70,7 +70,7 @@ void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) {
 
 
 RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){
-
+   d_is_computed = false;
 }
 
 RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) {
@@ -82,52 +82,59 @@ RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) {
   return d_rel_doms[n][i]->getParent();
 }
 
+void RelevantDomain::reset(){
+  d_is_computed = false;
+}
+
 void RelevantDomain::compute(){
-  for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
-    for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-      it2->second->reset();
+  if( !d_is_computed ){
+    d_is_computed = true;
+    for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
+      for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        it2->second->reset();
+      }
+    }
+    for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
+      Node f = d_model->getAssertedQuantifier( i );
+      Node icf = d_qe->getTermDatabase()->getInstConstantBody( f );
+      Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
+      computeRelevantDomain( icf, true, true );
     }
-  }
-  for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_model->getAssertedQuantifier( i );
-    Node icf = d_qe->getTermDatabase()->getInstConstantBody( f );
-    Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
-    computeRelevantDomain( icf, true, true );
-  }
 
-  Trace("rel-dom-debug") << "account for ground terms" << std::endl;
-  for( std::map< Node, std::vector< Node > >::iterator it = d_model->d_uf_terms.begin(); it != d_model->d_uf_terms.end(); ++it ){
-    Node op = it->first;
-    for( unsigned i=0; i<it->second.size(); i++ ){
-      Node n = it->second[i];
-      //if it is a non-redundant term
-      if( !n.getAttribute(NoMatchAttribute()) ){
-        for( unsigned j=0; j<n.getNumChildren(); j++ ){
-          RDomain * rf = getRDomain( op, j );
-          rf->addTerm( n[j] );
+    Trace("rel-dom-debug") << "account for ground terms" << std::endl;
+    TermDb * db = d_qe->getTermDatabase();
+    for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
+      Node op = it->first;
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node n = it->second[i];
+        //if it is a non-redundant term
+        if( !n.getAttribute(NoMatchAttribute()) ){
+          for( unsigned j=0; j<n.getNumChildren(); j++ ){
+            RDomain * rf = getRDomain( op, j );
+            rf->addTerm( n[j] );
+          }
         }
       }
     }
-  }
-  //print debug
-  for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
-    Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;
-    for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-      Trace("rel-dom") << "   " << it2->first << " : ";
-      RDomain * r = it2->second;
-      RDomain * rp = r->getParent();
-      if( r==rp ){
-        r->removeRedundantTerms( d_model );
-        for( unsigned i=0; i<r->d_terms.size(); i++ ){
-          Trace("rel-dom") << r->d_terms[i] << " ";
+    //print debug
+    for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
+      Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;
+      for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        Trace("rel-dom") << "   " << it2->first << " : ";
+        RDomain * r = it2->second;
+        RDomain * rp = r->getParent();
+        if( r==rp ){
+          r->removeRedundantTerms( d_model );
+          for( unsigned i=0; i<r->d_terms.size(); i++ ){
+            Trace("rel-dom") << r->d_terms[i] << " ";
+          }
+        }else{
+          Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";
         }
-      }else{
-        Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";
+        Trace("rel-dom") << std::endl;
       }
-      Trace("rel-dom") << std::endl;
     }
   }
-
 }
 
 void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index c4345f828..0f5afcadd 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -42,16 +42,18 @@ private:
   std::map< Node, std::map< int, RDomain * > > d_rel_doms;
   std::map< RDomain *, Node > d_rn_map;
   std::map< RDomain *, int > d_ri_map;
-  RDomain * getRDomain( Node n, int i );
   QuantifiersEngine* d_qe;
   FirstOrderModel* d_model;
   void computeRelevantDomain( Node n, bool hasPol, bool pol );
+  bool d_is_computed;
 public:
   RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
   virtual ~RelevantDomain(){}
+  void reset();
   //compute the relevant domain
   void compute();
 
+  RDomain * getRDomain( Node n, int i );
   Node getRelevantTerm( Node f, int i, Node r );
 };/* class RelevantDomain */
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 001d8b2b6..111aa9ac5 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,6 +30,7 @@
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
+#include "theory/quantifiers/relevant_domain.h"
 #include "theory/uf/options.h"
 
 using namespace std;
@@ -41,7 +42,6 @@ using namespace CVC4::theory::inst;
 
 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
 d_te( te ),
-d_quant_rel( false ),
 d_lemmas_produced_c(u){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
@@ -51,6 +51,7 @@ d_lemmas_produced_c(u){
   d_hasAddedLemma = false;
 
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
+
   //the model object
   if( options::mbqiMode()==quantifiers::MBQI_FMC ||
       options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
@@ -60,6 +61,16 @@ d_lemmas_produced_c(u){
   }else{
     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }
+  if( !options::finiteModelFind() ){
+    d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
+  }else{
+    d_rel_dom = NULL;
+  }
+  if( options::relevantTriggers() ){
+    d_quant_rel = new QuantRelevance( false );
+  }else{
+    d_quant_rel = NULL;
+  }
 
   //add quantifiers modules
   if( options::quantConflictFind() ){
@@ -161,6 +172,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
     d_hasAddedLemma = false;
     d_term_db->reset( e );
     d_eq_query->reset();
+    if( d_rel_dom ){
+      d_rel_dom->reset();
+    }
     if( e==Theory::EFFORT_LAST_CALL ){
       //if effort is last call, try to minimize model first
       if( options::finiteModelFind() ){
@@ -209,7 +223,9 @@ void QuantifiersEngine::registerQuantifier( Node f ){
     //make instantiation constants for f
     d_term_db->makeInstantiationConstantsFor( f );
     //register with quantifier relevance
-    d_quant_rel.registerQuantifier( f );
+    if( d_quant_rel ){
+      d_quant_rel->registerQuantifier( f );
+    }
     //register with each module
     for( int i=0; i<(int)d_modules.size(); i++ ){
       d_modules[i]->registerQuantifier( f );
@@ -264,9 +280,11 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
     d_eem->newTerms( added );
   }
   //added contains also the Node that just have been asserted in this branch
-  for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
-    if( !withinQuant ){
-      d_quant_rel.setRelevance( i->getOperator(), 0 );
+  if( d_quant_rel ){
+    for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
+      if( !withinQuant ){
+        d_quant_rel->setRelevance( i->getOperator(), 0 );
+      }
     }
   }
 }
@@ -414,9 +432,17 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
 }
 
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
-  if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
-    if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){
-      return true;
+  if( options::incrementalSolving() ){
+    if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
+      if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
+        return true;
+      }
+    }
+  }else{
+    if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
+      if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+        return true;
+      }
     }
   }
   //also check model engine (it may contain instantiations internally)
@@ -461,19 +487,27 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
     }
   }
   //check for duplication modulo equality
-  inst::CDInstMatchTrie* imt;
-  std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_inst_match_trie.find( f );
-  if( it!=d_inst_match_trie.end() ){
-    imt = it->second;
+  bool alreadyExists = false;
+  ///*
+  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+  if( options::incrementalSolving() ){
+    inst::CDInstMatchTrie* imt;
+    std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
+    if( it!=d_c_inst_match_trie.end() ){
+      imt = it->second;
+    }else{
+      imt = new CDInstMatchTrie( getUserContext() );
+      d_c_inst_match_trie[f] = imt;
+    }
+    alreadyExists = !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst );
   }else{
-    imt = new CDInstMatchTrie( getUserContext() );
-    d_inst_match_trie[f] = imt;
+    alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst );
   }
-  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
-  if( !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
-    Trace("inst-add-debug") << " -> Already exists." << std::endl;
-    ++(d_statistics.d_inst_duplicate);
-    return false;
+  //*/
+  if( alreadyExists ){
+      Trace("inst-add-debug") << " -> Already exists." << std::endl;
+      ++(d_statistics.d_inst_duplicate_eq);
+      return false;
   }
   Trace("inst-add-debug") << "compute terms" << std::endl;
   //compute the vector of terms for the instantiation
@@ -681,47 +715,46 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
     if( d_int_rep.find( r )==d_int_rep.end() ){
       //find best selection for representative
       Node r_best;
-      if( options::fmfRelevantDomain() && !f.isNull() ){
-        Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
-        r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r );
-        Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
-      }else{
-        std::vector< Node > eqc;
-        getEquivalenceClass( r, eqc );
-        Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
-        for( unsigned i=0; i<eqc.size(); i++ ){
-          if( i>0 ) Trace("internal-rep-select") << ", ";
-          Trace("internal-rep-select") << eqc[i];
-        }
-        Trace("internal-rep-select")  << " } " << std::endl;
-        int r_best_score = -1;
-        for( size_t i=0; i<eqc.size(); i++ ){
-          //if cbqi is active, do not choose instantiation constant terms
-          if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
-            int score = getRepScore( eqc[i], f, index );
-            //score prefers earliest use of this term as a representative
-            if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
-              r_best = eqc[i];
-              r_best_score = score;
-            }
-		      }
-        }
-        if( r_best.isNull() ){
-          if( !f.isNull() ){
-            Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
-            r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
-          }else{
-            r_best = a;
+      //if( options::fmfRelevantDomain() && !f.isNull() ){
+      //  Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
+      //  r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
+      //  Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
+      //}
+      std::vector< Node > eqc;
+      getEquivalenceClass( r, eqc );
+      Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
+      for( unsigned i=0; i<eqc.size(); i++ ){
+        if( i>0 ) Trace("internal-rep-select") << ", ";
+        Trace("internal-rep-select") << eqc[i];
+      }
+      Trace("internal-rep-select")  << " } " << std::endl;
+      int r_best_score = -1;
+      for( size_t i=0; i<eqc.size(); i++ ){
+        //if cbqi is active, do not choose instantiation constant terms
+        if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
+          int score = getRepScore( eqc[i], f, index );
+          //score prefers earliest use of this term as a representative
+          if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
+            r_best = eqc[i];
+            r_best_score = score;
           }
-		    }
-        //now, make sure that no other member of the class is an instance
-        r_best = getInstance( r_best, eqc );
-        //store that this representative was chosen at this point
-        if( d_rep_score.find( r_best )==d_rep_score.end() ){
-          d_rep_score[ r_best ] = d_reset_count;
         }
-        Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
       }
+      if( r_best.isNull() ){
+        if( !f.isNull() ){
+          Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
+          r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+        }else{
+          r_best = a;
+        }
+      }
+      //now, make sure that no other member of the class is an instance
+      r_best = getInstance( r_best, eqc );
+      //store that this representative was chosen at this point
+      if( d_rep_score.find( r_best )==d_rep_score.end() ){
+        d_rep_score[ r_best ] = d_reset_count;
+      }
+      Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
       d_int_rep[r] = r_best;
       if( r_best!=a ){
         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index ee7e6e6d8..9d341194f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -68,6 +68,7 @@ namespace quantifiers {
   class BoundedIntegers;
   class QuantConflictFind;
   class RewriteEngine;
+  class RelevantDomain;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -95,7 +96,9 @@ private:
   /** equality query class */
   EqualityQueryQuantifiersEngine* d_eq_query;
   /** for computing relevance of quantifiers */
-  QuantRelevance d_quant_rel;
+  QuantRelevance * d_quant_rel;
+  /** relevant domain */
+  quantifiers::RelevantDomain* d_rel_dom;
   /** phase requirements for each quantifier for each instantiation literal */
   std::map< Node, QuantPhaseReq* > d_phase_reqs;
   /** efficient e-matcher */
@@ -121,7 +124,8 @@ private:
   /** has added lemma this round */
   bool d_hasAddedLemma;
   /** list of all instantiations produced for each quantifier */
-  std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie;
+  std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
+  std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
   /** term database */
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
@@ -158,8 +162,10 @@ public:
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
   Valuation& getValuation();
+  /** get relevant domain */
+  quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
   /** get quantifier relevance */
-  QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; }
+  QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
   /** get phase requirement information */
   QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
   /** get phase requirement terms */