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);
   }