diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
| -rw-r--r-- | src/printer/ast/ast_printer.cpp | 2 | ||||
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 2 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 12 | ||||
| -rw-r--r-- | 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); |