merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

4 files changed, 18 insertions, 14 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 55e10724b..bbeee4f7f 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -922,9 +922,9 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
             }
           } else {
             Debug("parser") << "  " << *i << " not declared" << std::endl;
-            PARSER_STATE->mkVar(*i, t);
+            Expr func = PARSER_STATE->mkVar(*i, t);
             if(topLevel) {
-              Command* decl = new DeclareFunctionCommand(*i, t);
+              Command* decl = new DeclareFunctionCommand(*i, func, t);
               seq->addCommand(decl);
             }
           }
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index d44f7abcb..429adee0a 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -470,8 +470,8 @@ functionDeclaration[CVC4::Command*& smt_command]
       } else {
         t = EXPR_MANAGER->mkFunctionType(sorts);
       }
-      PARSER_STATE->mkVar(name, t);
-      smt_command = new DeclareFunctionCommand(name, t);
+      Expr func = PARSER_STATE->mkVar(name, t);
+      smt_command = new DeclareFunctionCommand(name, func, t);
     }
   ;
 
@@ -490,8 +490,8 @@ predicateDeclaration[CVC4::Command*& smt_command]
       } else {
         t = EXPR_MANAGER->mkPredicateType(p_sorts);
       }
-      PARSER_STATE->mkVar(name, t);
-      smt_command = new DeclareFunctionCommand(name, t);
+      Expr func = PARSER_STATE->mkVar(name, t);
+      smt_command = new DeclareFunctionCommand(name, func, t);
     }
   ;
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 84d75ceac..577438d37 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -240,8 +240,8 @@ command returns [CVC4::Command* cmd = NULL]
       if( sorts.size() > 0 ) {
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
-      PARSER_STATE->mkVar(name, t);
-      $cmd = new DeclareFunctionCommand(name, t); }
+      Expr func = PARSER_STATE->mkVar(name, t);
+      $cmd = new DeclareFunctionCommand(name, func, t); }
   | /* function definition */
     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -383,6 +383,9 @@ extendedCommand[CVC4::Command*& cmd]
     LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK
     { PARSER_STATE->popScope();
       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+  | /* get model */
+    GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { cmd = new GetModelCommand; }      
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
       { std::stringstream ss;
@@ -1063,6 +1066,7 @@ POP_TOK : 'pop';
 
 // extended commands
 DECLARE_DATATYPES_TOK : 'declare-datatypes';
+GET_MODEL_TOK : 'get-model';
 ECHO_TOK : 'echo';
 
 // attributes
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index e6231920d..ae4ad4e7f 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -70,11 +70,11 @@ public:
       //Conversion from rational to unsorted
       t = em->mkFunctionType(em->realType(), d_unsorted);
       d_rtu_op = em->mkVar("$$rtu",t);
-      preemptCommand(new DeclareFunctionCommand("$$rtu", t));
+      preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
       //Conversion from unsorted to rational
       t = em->mkFunctionType(d_unsorted, em->realType());
       d_utr_op = em->mkVar("$$utr",t);
-      preemptCommand(new DeclareFunctionCommand("$$utur", t));
+      preemptCommand(new DeclareFunctionCommand("$$utur", d_utr_op, t));
     }
     // Add the inverse in order to show that over the elements that
     // appear in the problem there is a bijection between unsorted and
@@ -98,11 +98,11 @@ public:
       //Conversion from string to unsorted
       t = em->mkFunctionType(em->stringType(), d_unsorted);
       d_stu_op = em->mkVar("$$stu",t);
-      preemptCommand(new DeclareFunctionCommand("$$stu", t));
+      preemptCommand(new DeclareFunctionCommand("$$stu", d_stu_op, t));
       //Conversion from unsorted to string
       t = em->mkFunctionType(d_unsorted, em->stringType());
       d_uts_op = em->mkVar("$$uts",t);
-      preemptCommand(new DeclareFunctionCommand("$$uts", t));
+      preemptCommand(new DeclareFunctionCommand("$$uts", d_uts_op, t));
     }
     // Add the inverse in order to show that over the elements that
     // appear in the problem there is a bijection between unsorted and
@@ -185,7 +185,7 @@ inline void Tptp::makeApplication(Expr & expr, std::string & name,
     } else {
       Type t = term ? d_unsorted : getExprManager()->booleanType();
       expr = mkVar(name,t,true); //levelZero
-      preemptCommand(new DeclareFunctionCommand(name, t));
+      preemptCommand(new DeclareFunctionCommand(name, expr, t));
     }
   } else { // Its an application
     if(isDeclared(name)){ //already appeared
@@ -195,7 +195,7 @@ inline void Tptp::makeApplication(Expr & expr, std::string & name,
       Type t = term ? d_unsorted : getExprManager()->booleanType();
       t = getExprManager()->mkFunctionType(sorts, t);
       expr = mkVar(name,t,true); //levelZero
-      preemptCommand(new DeclareFunctionCommand(name, t));
+      preemptCommand(new DeclareFunctionCommand(name, expr, t));
     }
     expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args);
   }