cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation

10 files changed, 84 insertions, 49 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 36f265c30..4a89a4dd3 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -91,7 +91,7 @@ void InstMatch::debugPrint( const char* c ){
   //  Debug( c ) << std::endl;
   //}
 }
-
+/*
 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
     Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
@@ -113,13 +113,15 @@ void InstMatch::makeInternal( QuantifiersEngine* qe ){
     }
   }
 }
-
+*/
 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-    d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
-    if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
-      d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+    if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
+      d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
     }
+    //if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
+    //  d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+    //}
   }
 }
 
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 426adc02d..43c0d26c7 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -55,9 +55,9 @@ public:
   /** is complete? */
   bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
   /** make complete */
-  void makeComplete( Node f, QuantifiersEngine* qe );
+  //void makeComplete( Node f, QuantifiersEngine* qe );
   /** make internal: ensure that no term in d_map contains instantiation constants */
-  void makeInternal( QuantifiersEngine* qe );
+  //void makeInternal( QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
   /** get value */
@@ -96,7 +96,8 @@ public:
     //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
     Assert( !var.isNull() );
     Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-            var.getType() == n.getType() );
+            //var.getType() == n.getType()
+            n.getType().isSubtypeOf( var.getType() ) );
     d_map[var] = n;
   }
   size_t size(){ return d_map.size(); }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 027ac67eb..8d935a323 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
+QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
 
 }
 
@@ -67,7 +67,12 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl;
   //reset the quantifiers engine
   Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
-  d_quantEngine->resetInstantiationRound( effort );
+  //reset the instantiators
+  for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
+    if( d_quantEngine->getInstantiator( i ) ){
+      d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort );
+    }
+  }
   //iterate over an internal effort level e
   int e = 0;
   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
@@ -125,22 +130,26 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   }
 }
 
-void InstantiationEngine::check( Theory::Effort e ){
+bool InstantiationEngine::needsCheck( Theory::Effort e ){
   if( e==Theory::EFFORT_FULL ){
     d_ierCounter++;
   }
   //determine if we should perform check, based on instWhenMode
-  bool performCheck = false;
+  d_performCheck = false;
   if( options::instWhenMode()==INST_WHEN_FULL ){
-    performCheck = ( e >= Theory::EFFORT_FULL );
+    d_performCheck = ( e >= Theory::EFFORT_FULL );
   }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+    d_performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
-    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
+    d_performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{
-    performCheck = true;
+    d_performCheck = true;
   }
-  if( performCheck ){
+  return d_performCheck;
+}
+
+void InstantiationEngine::check( Theory::Effort e ){
+  if( d_performCheck ){
     Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl;
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 6d995097a..b3bbbce4a 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -34,6 +34,7 @@ private:
   bool d_setIncomplete;
   /** inst round counter */
   int d_ierCounter;
+  bool d_performCheck;
   /** whether each quantifier is active */
   std::map< Node, bool > d_quant_active;
   /** whether we have added cbqi lemma */
@@ -62,6 +63,7 @@ public:
   InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
   ~InstantiationEngine(){}
 
+  bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
   void assertNode( Node f );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index f2e195d2e..8b34a3a12 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -33,20 +33,20 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-bool TermArgBasisTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
+bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
   if( argIndex<(int)n.getNumChildren() ){
     Node r;
     if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
       r = n[ argIndex ];
     }else{
-      r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
+      r = fm->getRepresentative( n[ argIndex ] );
     }
     std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
     if( it==d_data.end() ){
-      d_data[r].addTerm2( qe, n, argIndex+1 );
+      d_data[r].addTerm2( fm, n, argIndex+1 );
       return true;
     }else{
-      return it->second.addTerm2( qe, n, argIndex+1 );
+      return it->second.addTerm2( fm, n, argIndex+1 );
     }
   }else{
     return false;
@@ -99,6 +99,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
         }
       }
     }
+    //END FOR DEBUGGING
   }else{
     d_curr_model = fm;
     d_addedLemmas = 0;
@@ -162,6 +163,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
               if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){
                 break;
               }
+            }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+              d_numQuantSat++;
             }
           }
           Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
@@ -267,7 +270,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
       if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
         if( !n.getAttribute(BasisNoMatchAttribute()) ){
           //need to consider if it is not congruent modulo model basis
-          if( !tabt.addTerm( d_qe, n ) ){
+          if( !tabt.addTerm( fm, n ) ){
              BasisNoMatchAttribute bnma;
              n.setAttribute(bnma,true);
           }
@@ -311,7 +314,7 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
 }
 
 bool ModelEngineBuilder::optExhInstNonInstGenQuant(){
-  return true;
+  return options::fmfNewInstGen();
 }
 
 void ModelEngineBuilder::setEffort( int effort ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index d0348dff8..7331daf8e 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -23,6 +23,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 
 /** Attribute true for nodes that should not be used when considered for inst-gen basis */
 struct BasisNoMatchAttributeId {};
@@ -35,17 +36,14 @@ typedef expr::Attribute< BasisNoMatchAttributeId,
 
 class TermArgBasisTrie {
 private:
-  bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
+  bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
 public:
   /** the data */
   std::map< Node, TermArgBasisTrie > d_data;
 public:
-  bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
+  bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); }
 };/* class TermArgBasisTrie */
 
-
-namespace quantifiers {
-
 /** model builder class
   *  This class is capable of building candidate models based on the current quantified formulas
   *  that are asserted.  Use:
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 40a61f7c5..87f842862 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -52,21 +52,19 @@ void ModelEngine::check( Theory::Effort e ){
     FirstOrderModel* fm = d_quantEngine->getModel();
     //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
     int addedLemmas = 0;
-    Trace("model-engine") << "---Model Engine Round---" << std::endl;
+    //quantifiers are initialized, we begin an instantiation round
+    double clSet = 0;
+    if( Trace.isOn("model-engine") ){
+      clSet = double(clock())/double(CLOCKS_PER_SEC);
+    }
+    ++(d_statistics.d_inst_rounds);
     //two effort levels: first try exhaustive instantiation without axioms, then with.
     int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
     for( int effort=startEffort; effort<2; effort++ ){
       // for effort = 0, we only instantiate non-axioms
       // for effort = 1, we instantiate everything
       if( addedLemmas==0 ){
-        //quantifiers are initialized, we begin an instantiation round
-        double clSet = 0;
-        if( Trace.isOn("model-engine") ){
-          clSet = double(clock())/double(CLOCKS_PER_SEC);
-        }
-        ++(d_statistics.d_inst_rounds);
-        //reset the quantifiers engine
-        d_quantEngine->resetInstantiationRound( e );
+        Trace("model-engine") << "---Model Engine Round---" << std::endl;
         //initialize the model
         Trace("model-engine-debug") << "Build model..." << std::endl;
         d_builder->setEffort( effort );
@@ -91,10 +89,6 @@ void ModelEngine::check( Theory::Effort e ){
           //check quantifiers that inst-gen didn't apply to
           addedLemmas += checkModel( check_model_no_inst_gen );
         }
-        if( Trace.isOn("model-engine") ){
-          double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-          Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
-        }
       }
       if( addedLemmas==0 ){
         //if we have not added lemmas yet and axiomInstMode=trust, then we are done
@@ -107,6 +101,10 @@ void ModelEngine::check( Theory::Effort e ){
         }
       }
     }
+    if( Trace.isOn("model-engine") ){
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+    }
     if( addedLemmas==0 ){
       Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
       //CVC4 will answer SAT or unknown
@@ -155,6 +153,19 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){
 #endif
 }
 
+bool containsNN( Node n, Node nc ){
+  if( n==nc ){
+    return true;
+  }else{
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( containsNN( n[i], nc ) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
 int ModelEngine::checkModel( int checkOption ){
   int addedLemmas = 0;
   FirstOrderModel* fm = d_quantEngine->getModel();
@@ -169,6 +180,17 @@ int ModelEngine::checkModel( int checkOption ){
           Trace("model-engine-debug") << it->second[i] << "  ";
         }
         Trace("model-engine-debug") << std::endl;
+        for( size_t i=0; i<it->second.size(); i++ ){
+          std::vector< Node > eqc;
+          d_quantEngine->getEqualityQuery()->getEquivalenceClass( it->second[i], eqc );
+          Trace("model-engine-debug-eqc") << "      " << it->second[i] << " : { ";
+          for( size_t j=0; j<eqc.size(); j++ ){
+            if( it->second[i]!=eqc[j] && containsNN( it->second[i], eqc[j] ) ){
+              Trace("model-engine-debug-eqc") << eqc[j] << " ";
+            }
+          }
+          Trace("model-engine-debug-eqc") << "}" << std::endl;
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 724c76e82..5802a05cd 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -61,9 +61,12 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false
 option userPatternsQuant /--ignore-user-patterns bool :default true
  ignore user-provided patterns for quantifier instantiation
 
-option flipDecision --enable-flip-decision/ bool :default false
+option flipDecision --flip-decision/ bool :default false
  turns on flip decision heuristic
 
+option internalReps --disable-quant-internal-reps/ bool :default true
+ disables instantiating with representatives chosen by quantifiers engine
+
 option finiteModelFind --finite-model-find bool :default false
  use finite model finding heuristic for quantifier instantiation
 
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 18aaab01f..bb6855c47 100755
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -77,6 +77,8 @@ class EqualityQuery {
 public:

   EqualityQuery(){}

   virtual ~EqualityQuery(){};

+  /** reset */

+  virtual void reset() = 0;

   /** contains term */

   virtual bool hasTerm( Node a ) = 0;

   /** get the representative of the equivalence class of a */

@@ -85,11 +87,6 @@ public:
   virtual bool areEqual( Node a, Node b ) = 0;

   /** returns true is a and b are disequal in the current context */

   virtual bool areDisequal( Node a, Node b ) = 0;

-  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.

-      If cbqi is active, this will return a term in the equivalence class of "a" that does

-      not contain instantiation constants, if such a term exists.

-   */

-  virtual Node getInternalRepresentative( Node a ) = 0;

   /** get the equality engine associated with this query */

   virtual eq::EqualityEngine* getEngine() = 0;

   /** get the equivalence class of a */

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 493b9e931..d637fa25f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -144,7 +144,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
            computeModelBasisArgAttribute( n );
            if( !n.getAttribute(NoMatchAttribute()) ){
              if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
-               //only set no match if not a model basis argument term
                NoMatchAttribute nma;
                n.setAttribute(nma,true);
                congruentCount++;
@@ -171,7 +170,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
          if( !en.getAttribute(NoMatchAttribute()) ){
            Node op = en.getOperator();
            if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
-             //only set no match if not a model basis argument term
              NoMatchAttribute nma;
              en.setAttribute(nma,true);
              congruentCount++;