From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 21 Mar 2013 18:04:35 +0000 (-0400)
Subject: Some model and printing fixes for defined functions in input.
X-Git-Tag: cvc5-1.0.0~7376^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16215e6e021c0fb24a6237126e17c89485dfc012;p=cvc5.git

Some model and printing fixes for defined functions in input.
---

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