More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fmf mbqi=gen-ev for interpreted operators.

5 files changed, 33 insertions, 50 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d2e83702f..c7c82b2d8 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -912,7 +912,8 @@ smt25Command[CVC4::Command*& cmd]
           }
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }
-        Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED);
+        Expr func = PARSER_STATE->mkVar(fname, t);
+        static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t));
         std::vector< Expr > f_app;
         f_app.push_back( func );
         PARSER_STATE->pushScope(true);
@@ -958,7 +959,8 @@ smt25Command[CVC4::Command*& cmd]
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }
         sortedVarNames.clear();
-        Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED);
+        Expr func = PARSER_STATE->mkVar(fname, t);
+        static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t));
         funcs.push_back( func );
       }
       RPAREN_TOK
@@ -1079,6 +1081,7 @@ extendedCommand[CVC4::Command*& cmd]
         }
         Expr func = PARSER_STATE->mkVar(name, t);
         static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t));
+        sorts.clear();
       }
     )+
     RPAREN_TOK
@@ -1098,6 +1101,7 @@ extendedCommand[CVC4::Command*& cmd]
         }
         Expr func = PARSER_STATE->mkVar(name, t);
         static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t));
+        sorts.clear();
       }
     )+
     RPAREN_TOK
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 88464bb9a..50b04123c 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -169,10 +169,10 @@ void FirstOrderModelIG::processInitializeModelForTerm( Node n ){
       TypeNode tn = op.getType();
       tn = tn[ (int)tn.getNumChildren()-1 ];
       //only generate models for predicates and functions with uninterpreted range types
-      if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){
+      //if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){
         d_uf_model_tree[ op ] = uf::UfModelTree( op );
         d_uf_model_gen[ op ].clear();
-      }
+      //}
     }
   }
   /*
@@ -355,42 +355,9 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri
     }
   }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 );
-        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];
-        }
-      }
-      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 );
-#endif
-    }else{
-      //default term evaluate : evaluate all children, recreate the value
-      val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
-    }
+    //default term evaluate : evaluate all children, recreate the value
+    val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
+    Trace("fmf-eval-debug") << "Evaluate term, value from " << n << " is " << val << std::endl;
     if( !val.isNull() ){
       bool setVal = false;
       //custom ways of evaluating terms
@@ -405,8 +372,10 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri
           makeEvalUfModel( n );
           //now, consult the model
           if( d_eval_uf_use_default[n] ){
+            Trace("fmf-eval-debug") << "get default" << std::endl;
             val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex );
           }else{
+            Trace("fmf-eval-debug") << "get uf model" << std::endl;
             val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex );
           }
           //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
@@ -422,22 +391,20 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri
             }
           }
           setVal = true;
+        }else{
+          Trace("fmf-eval-debug") << "No model." << std::endl;
         }
-      }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 );
+        if( !val.isConst() ){
+          return Node::null();
         }
       }
       Trace("fmf-eval-debug") << "Evaluate term " << n << " = ";
       printRepresentativeDebug( "fmf-eval-debug", val );
-      Trace("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
+      Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl;
     }
   }
   return val;
@@ -448,6 +415,7 @@ Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector<
   if( n.getNumChildren()==0 ){
     return n;
   }else{
+    bool isInterp = n.getKind()!=APPLY_UF;
     //first we must evaluate the arguments
     std::vector< Node > children;
     if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
@@ -461,10 +429,15 @@ Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector<
         depIndex = ri->getNumTerms()-1;
         return nn;
       }else{
-        children.push_back( nn );
         if( childDepIndex[i]>depIndex ){
           depIndex = childDepIndex[i];
         }
+        if( isInterp ){
+          if( !nn.isConst() ) {
+            nn = getRepresentative( nn );
+          }
+        }
+        children.push_back( nn );
       }
     }
     //recreate the value
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 591034ffc..6e73b37a7 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -77,7 +77,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       Trace("model-engine-debug") << "Check model..." << std::endl;
       d_incomplete_check = false;
       //print debug
-      Debug("fmf-model-complete") << std::endl;
+      Trace("fmf-model-complete") << std::endl;
       debugPrint("fmf-model-complete");
       //successfully built an acceptable model, now check it
       addedLemmas += checkModel();
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 9003ef636..6bd6280ae 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -67,7 +67,8 @@ SMT2_TESTS = \
 	hung13sdk_output1.smt2 \
 	hung10_itesdk_output2.smt2 \
 	hung10_itesdk_output1.smt2 \
-	hung13sdk_output2.smt2
+	hung13sdk_output2.smt2 \
+	declare-funs.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
diff --git a/test/regress/regress0/declare-funs.smt2 b/test/regress/regress0/declare-funs.smt2
new file mode 100644
index 000000000..9cbbd8f73
--- /dev/null
+++ b/test/regress/regress0/declare-funs.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(set-info :status sat)
+(declare-funs ((f Int) (g Int)))
+(assert (= f g))
+(check-sat)
\ No newline at end of file