From 16215e6e021c0fb24a6237126e17c89485dfc012 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 21 Mar 2013 14:04:35 -0400
Subject: [PATCH] Some model and printing fixes for defined functions in input.

---
 src/parser/smt2/Smt2.g            |  4 ++--
 src/printer/ast/ast_printer.cpp   |  2 +-
 src/printer/cvc/cvc_printer.cpp   |  2 +-
 src/printer/smt2/smt2_printer.cpp |  2 +-
 src/smt/smt_engine.cpp            | 12 +++++++++++-
 test/unit/expr/type_node_white.h  |  2 +-
 6 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1ee288aa4..a390cf452 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -267,7 +267,7 @@ command returns [CVC4::Command* cmd = NULL]
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
           ++i) {
-        terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+        terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
       }
     }
     term[expr, expr2]
@@ -479,7 +479,7 @@ extendedCommand[CVC4::Command*& cmd]
               sortedVarNames.begin(), iend = sortedVarNames.end();
             i != iend;
             ++i) {
-          terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+          terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
         }
       }
       term[e,e2]
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 3239d5b85..42fe7801d 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -144,10 +144,10 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
      tryToStream<DeclareFunctionCommand>(out, c) ||
-     tryToStream<DefineFunctionCommand>(out, c) ||
      tryToStream<DeclareTypeCommand>(out, c) ||
      tryToStream<DefineTypeCommand>(out, c) ||
      tryToStream<DefineNamedFunctionCommand>(out, c) ||
+     tryToStream<DefineFunctionCommand>(out, c) ||
      tryToStream<SimplifyCommand>(out, c) ||
      tryToStream<GetValueCommand>(out, c) ||
      tryToStream<GetModelCommand>(out, c) ||
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 0206c4252..2cfeaafc1 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -764,10 +764,10 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
      tryToStream<DeclareFunctionCommand>(out, c) ||
-     tryToStream<DefineFunctionCommand>(out, c) ||
      tryToStream<DeclareTypeCommand>(out, c) ||
      tryToStream<DefineTypeCommand>(out, c) ||
      tryToStream<DefineNamedFunctionCommand>(out, c) ||
+     tryToStream<DefineFunctionCommand>(out, c) ||
      tryToStream<SimplifyCommand>(out, c) ||
      tryToStream<GetValueCommand>(out, c) ||
      tryToStream<GetModelCommand>(out, c) ||
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ef4fd5fea..50cab3f53 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -506,10 +506,10 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<QuitCommand>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
      tryToStream<DeclareFunctionCommand>(out, c) ||
-     tryToStream<DefineFunctionCommand>(out, c) ||
      tryToStream<DeclareTypeCommand>(out, c) ||
      tryToStream<DefineTypeCommand>(out, c) ||
      tryToStream<DefineNamedFunctionCommand>(out, c) ||
+     tryToStream<DefineFunctionCommand>(out, c) ||
      tryToStream<SimplifyCommand>(out, c) ||
      tryToStream<GetValueCommand>(out, c) ||
      tryToStream<GetModelCommand>(out, c) ||
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5a4c1ca58..e98bffc1e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1169,6 +1169,16 @@ void SmtEngine::defineFunction(Expr func,
                                const std::vector<Expr>& formals,
                                Expr formula) {
   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
+  for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
+    if((*i).getKind() != kind::BOUND_VARIABLE) {
+      stringstream ss;
+      ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
+         << "definition of function " << func << ", formal\n"
+         << "  " << *i << "\n"
+         << "has kind " << (*i).getKind();
+      throw TypeCheckingException(func, ss.str());
+    }
+  }
   if(Dump.isOn("declarations")) {
     stringstream ss;
     ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
@@ -1285,7 +1295,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
     if(i != d_smt.d_definedFunctions->end()) {
       // replacement must be closed
       if((*i).second.getFormals().size() > 0) {
-        //throw TypeCheckingException(n.toExpr(), string("Defined function requires arguments: `") + n.toString() + "'");
+        return d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula());
       }
       // don't bother putting in the cache
       return (*i).second.getFormula();
diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 86f0b192d..97dc1a696 100644
--- a/test/unit/expr/type_node_white.h
+++ b/test/unit/expr/type_node_white.h
@@ -61,7 +61,7 @@ public:
     TypeNode bvType = d_nm->mkBitVectorType(32);
     TypeNode subrangeType = d_nm->mkSubrangeType(SubrangeBounds(Integer(1), Integer(10)));
 
-    Node x = d_nm->mkVar("x", realType);
+    Node x = d_nm->mkBoundVar("x", realType);
     Node xPos = d_nm->mkNode(GT, x, d_nm->mkConst(Rational(0)));
     TypeNode funtype = d_nm->mkFunctionType(integerType, booleanType);
     Node lambda = d_nm->mkVar("lambda", funtype);
-- 
2.30.2