minor fix for mbqi in finite model finding

5 files changed, 128 insertions, 154 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index bd9e6aefa..4a3ddc9ca 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -604,6 +604,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 
 Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps)
 {
+  Trace("tembn") << "Normalize " << r << std::endl;
   std::map<Node, Node>::iterator itMap = constantReps.find(r);
   if (itMap != constantReps.end()) {
     return (*itMap).second;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index e0723f432..33dcdd533 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -252,124 +252,118 @@ int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
 
 Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
   //Message() << "Eval term " << n << std::endl;
-  if( !n.hasAttribute(InstConstantAttribute()) ){
-    //if evaluating a ground term, just consult the standard getValue functionality
-    depIndex = -1;
-    return getValue( n );
-  }else{
-    Node val;
-    depIndex = ri->getNumTerms()-1;
-    //check the type of n
-    if( n.getKind()==INST_CONSTANT ){
-      int v = n.getAttribute(InstVarNumAttribute());
-      depIndex = ri->d_var_order[ v ];
-      val = ri->getTerm( v );
-    }else if( n.getKind()==ITE ){
-      int depIndex1, depIndex2;
-      int eval = evaluate( n[0], depIndex1, ri );
-      if( eval==0 ){
-        //evaluate children to see if they are the same
-        Node val1 = evaluateTerm( n[ 1 ], depIndex1, ri );
-        Node val2 = evaluateTerm( n[ 2 ], depIndex2, ri );
-        if( val1==val2 ){
-          val = val1;
-          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-        }else{
-          return Node::null();
-        }
-      }else{
-        val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2, ri );
+  Node val;
+  depIndex = ri->getNumTerms()-1;
+  //check the type of n
+  if( n.getKind()==INST_CONSTANT ){
+    int v = n.getAttribute(InstVarNumAttribute());
+    depIndex = ri->d_var_order[ v ];
+    val = ri->getTerm( v );
+  }else if( n.getKind()==ITE ){
+    int depIndex1, depIndex2;
+    int eval = evaluate( n[0], depIndex1, ri );
+    if( eval==0 ){
+      //evaluate children to see if they are the same
+      Node val1 = evaluateTerm( n[ 1 ], depIndex1, ri );
+      Node val2 = evaluateTerm( n[ 2 ], depIndex2, ri );
+      if( val1==val2 ){
+        val = val1;
         depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+      }else{
+        return Node::null();
       }
     }else{
-      std::vector< int > children_depIndex;
-      //for select, pre-process read over writes
-      if( n.getKind()==SELECT ){
+      val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2, ri );
+      depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+    }
+  }else{
+    std::vector< int > children_depIndex;
+    //for select, pre-process read over writes
+    if( n.getKind()==SELECT ){
 #if 0
-        //std::cout << "Evaluate " << n << std::endl;
-        Node sel = evaluateTerm( n[1], depIndex, ri );
-        if( sel.isNull() ){
-          depIndex = ri->getNumTerms()-1;
-          return Node::null();
-        }
-        Node arr = getRepresentative( n[0] );
-        //if( n[0]!=getRepresentative( n[0] ) ){
-        //  std::cout << n[0] << " is " << getRepresentative( n[0] ) << std::endl;
-        //}
-        int tempIndex;
-        int eval = 1;
-        while( arr.getKind()==STORE && eval!=0 ){
-          eval = evaluate( sel.eqNode( arr[1] ), tempIndex, ri );
+      //std::cout << "Evaluate " << n << std::endl;
+      Node sel = evaluateTerm( n[1], depIndex, ri );
+      if( sel.isNull() ){
+        depIndex = ri->getNumTerms()-1;
+        return Node::null();
+      }
+      Node arr = getRepresentative( n[0] );
+      //if( n[0]!=getRepresentative( n[0] ) ){
+      //  std::cout << n[0] << " is " << getRepresentative( n[0] ) << std::endl;
+      //}
+      int tempIndex;
+      int eval = 1;
+      while( arr.getKind()==STORE && eval!=0 ){
+        eval = evaluate( sel.eqNode( arr[1] ), tempIndex, ri );
+        depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+        if( eval==1 ){
+          val = evaluateTerm( arr[2], tempIndex, ri );
           depIndex = tempIndex > depIndex ? tempIndex : depIndex;
-          if( eval==1 ){
-            val = evaluateTerm( arr[2], tempIndex, ri );
-            depIndex = tempIndex > depIndex ? tempIndex : depIndex;
-            return val;
-          }else if( eval==-1 ){
-            arr = arr[0];
-          }
+          return val;
+        }else if( eval==-1 ){
+          arr = arr[0];
         }
-        arr = evaluateTerm( arr, tempIndex, ri );
-        depIndex = tempIndex > depIndex ? tempIndex : depIndex;
-        val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
+      }
+      arr = evaluateTerm( arr, tempIndex, ri );
+      depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+      val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
 #else
-        val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
+      val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
 #endif
-      }else{
-        //default term evaluate : evaluate all children, recreate the value
-        val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
-      }
-      if( !val.isNull() ){
-        bool setVal = false;
-        //custom ways of evaluating terms
-        if( n.getKind()==APPLY_UF ){
-          Node op = n.getOperator();
+    }else{
+      //default term evaluate : evaluate all children, recreate the value
+      val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
+    }
+    if( !val.isNull() ){
+      bool setVal = false;
+      //custom ways of evaluating terms
+      if( n.getKind()==APPLY_UF ){
+        Node op = n.getOperator();
+        //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+        //if it is a defined UF, then consult the interpretation
+        if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
+          ++d_eval_uf_terms;
+          int argDepIndex = 0;
+          //make the term model specifically for n
+          makeEvalUfModel( n );
+          //now, consult the model
+          if( d_eval_uf_use_default[n] ){
+            val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex );
+          }else{
+            val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex );
+          }
           //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
-          //if it is a defined UF, then consult the interpretation
-          if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
-            ++d_eval_uf_terms;
-            int argDepIndex = 0;
-            //make the term model specifically for n
-            makeEvalUfModel( n );
-            //now, consult the model
-            if( d_eval_uf_use_default[n] ){
-              val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex );
-            }else{
-              val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex );
-            }
-            //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
-            //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
-            Assert( !val.isNull() );
-            //recalculate the depIndex
-            depIndex = -1;
-            for( int i=0; i<argDepIndex; i++ ){
-              int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
-              Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
-              if( children_depIndex[index]>depIndex ){
-                depIndex = children_depIndex[index];
-              }
+          //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
+          Assert( !val.isNull() );
+          //recalculate the depIndex
+          depIndex = -1;
+          for( int i=0; i<argDepIndex; i++ ){
+            int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
+            Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
+            if( children_depIndex[index]>depIndex ){
+              depIndex = children_depIndex[index];
             }
-            setVal = true;
           }
-        }else if( n.getKind()==SELECT ){
-          //we are free to interpret this term however we want
+          setVal = true;
         }
-        //if not set already, rewrite and consult model for interpretation
-        if( !setVal ){
-          val = Rewriter::rewrite( val );
-          if( val.getMetaKind()!=kind::metakind::CONSTANT ){
-            //FIXME: we cannot do this until we trust all theories collectModelInfo!
-            //val = getInterpretedValue( val );
-            //val = getRepresentative( val );
-          }
+      }else if( n.getKind()==SELECT ){
+        //we are free to interpret this term however we want
+      }
+      //if not set already, rewrite and consult model for interpretation
+      if( !setVal ){
+        val = Rewriter::rewrite( val );
+        if( val.getMetaKind()!=kind::metakind::CONSTANT ){
+          //FIXME: we cannot do this until we trust all theories collectModelInfo!
+          //val = getInterpretedValue( val );
+          //val = getRepresentative( val );
         }
-        Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
-        printRepresentativeDebug( "fmf-eval-debug", val );
-        Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
       }
+      Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
+      printRepresentativeDebug( "fmf-eval-debug", val );
+      Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
     }
-    return val;
   }
+  return val;
 }
 
 Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 8eac4da95..805d27008 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -302,32 +302,6 @@ int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
   //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
   //  effectively acting as partial instantiations instead of pointwise instantiations.
   if( !d_quant_selection_lit[f].isNull() ){
-#if 0
-    bool phase = d_quant_selection_lit[f].getKind()!=NOT;
-    Node lit = d_quant_selection_lit[f].getKind()==NOT ? d_quant_selection_lit[f][0] : d_quant_selection_lit[f];
-    Assert( lit.hasAttribute(InstConstantAttribute()) );
-    for( size_t i=0; i<d_quant_selection_lit_terms[f].size(); i++ ){
-      Node n1 = d_quant_selection_lit_terms[f][i];
-      Node op = d_quant_selection_lit_terms[f][i].getOperator();
-      //check all other selection literals involving "op"
-      for( size_t i=0; i<d_op_selection_terms[op].size(); i++ ){
-        Node n2 = d_op_selection_terms[op][i];
-        Node n2_lit = d_term_selection_lit[ n2 ];
-        if( n2_lit!=d_quant_selection_lit[f] ){
-          //match n1 and n2
-        }
-      }
-      if( addedLemmas==0 ){
-        //check all ground terms involving "op"
-        for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
-          Node n2 = fm->d_uf_terms[op][i];
-          if( n1!=n2 ){
-            //match n1 and n2
-          }
-        }
-      }
-    }
-#else
     Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
     for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
       bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
@@ -369,7 +343,6 @@ int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
         addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
       }
     }
-#endif
   }
   return addedLemmas;
 }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index b5a9ee74c..d9d6b8b0b 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -26,8 +26,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 
-//#define ME_PRINT_WARNINGS
-
 #define EVAL_FAIL_SKIP_MULTIPLE
 
 using namespace std;
@@ -157,6 +155,14 @@ bool ModelEngine::optOneQuantPerRound(){
   return options::fmfOneQuantPerRound();
 }
 
+bool ModelEngine::optExhInstEvalSkipMultiple(){
+#ifdef EVAL_FAIL_SKIP_MULTIPLE
+  return true;
+#else
+  return false;
+#endif
+}
+
 int ModelEngine::initializeQuantifier( Node f ){
   if( d_quant_init.find( f )==d_quant_init.end() ){
     d_quant_init[f] = true;
@@ -233,13 +239,13 @@ void ModelEngine::checkModel( int& addedLemmas ){
   for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
     Node f = fm->getAssertedQuantifier( i );
     addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
-#ifdef ME_PRINT_WARNINGS
-    if( addedLemmas>10000 ){
-      Debug("fmf-exit") << std::endl;
-      debugPrint("fmf-exit");
-      exit( 0 );
+    if( Trace.isOn("model-engine-warn") ){
+      if( addedLemmas>10000 ){
+        Debug("fmf-exit") << std::endl;
+        debugPrint("fmf-exit");
+        exit( 0 );
+      }
     }
-#endif
     if( optOneQuantPerRound() && addedLemmas>0 ){
       break;
     }
@@ -261,6 +267,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
   d_totalLemmas += totalInst;
   //if we need to consider this quantifier on this iteration
   if( d_builder.isQuantifierActive( f ) ){
+    //debug printing
     Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
     if( useRelInstDomain ){
       Trace("rel-dom") << "Relevant domain : " << std::endl;
@@ -272,14 +279,14 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
         Trace("rel-dom") << std::endl;
       }
     }
-    int tests = 0;
-    int triedLemmas = 0;
     Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
       Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
     }
     Debug("inst-fmf-ei") << std::endl;
+
+    //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
     riter.setQuantifier( f );
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
@@ -289,6 +296,8 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
       riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
     }
     d_quantEngine->getModel()->resetEvaluate();
+    int tests = 0;
+    int triedLemmas = 0;
     while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
       d_testLemmas++;
       int eval = 0;
@@ -324,21 +333,19 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
         //add as instantiation
         if( d_quantEngine->addInstantiation( f, m ) ){
           addedLemmas++;
-#ifdef EVAL_FAIL_SKIP_MULTIPLE
-          if( eval==-1 ){
+          //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+          if( eval==-1 && optExhInstEvalSkipMultiple() ){
             riter.increment2( depIndex );
           }else{
             riter.increment();
           }
-#else
-          riter.increment();
-#endif
         }else{
-          Debug("ajr-temp") << "* Failed Add instantiation " << m << std::endl;
+          Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
           riter.increment();
         }
       }
     }
+    //print debugging information
     d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
     d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
     d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
@@ -354,17 +361,15 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
     Debug("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
     Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
     Debug("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
-#ifdef ME_PRINT_WARNINGS
     if( addedLemmas>1000 ){
-      Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl;
-      Notice() << "   Inst Total: " << totalInst << std::endl;
-      Notice() << "   Inst Relevant: " << totalRelevant << std::endl;
-      Notice() << "   Inst Tried: " << triedLemmas << std::endl;
-      Notice() << "   Inst Added: " << addedLemmas << std::endl;
-      Notice() << "   # Tests: " << tests << std::endl;
-      Notice() << std::endl;
+      Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+      Trace("model-engine-warn") << "   Inst Total: " << totalInst << std::endl;
+      Trace("model-engine-warn") << "   Inst Relevant: " << relevantInst << std::endl;
+      Trace("model-engine-warn") << "   Inst Tried: " << triedLemmas << std::endl;
+      Trace("model-engine-warn") << "   Inst Added: " << addedLemmas << std::endl;
+      Trace("model-engine-warn") << "   # Tests: " << tests << std::endl;
+      Trace("model-engine-warn") << std::endl;
     }
-#endif
   }
   return addedLemmas;
 }
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index a292eb5f8..7a5954e5c 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -47,6 +47,7 @@ private:
   bool optOneInstPerQuantRound();
   bool optUseRelevantDomain();
   bool optOneQuantPerRound();
+  bool optExhInstEvalSkipMultiple();
 private:
   //initialize quantifiers, return number of lemmas produced
   int initializeQuantifier( Node f );