diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-14 23:49:07 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-14 23:49:07 +0000 |
commit | 19abe15ccc1e310ae3f726b351b0023670ba7962 (patch) | |
tree | 66848c129df4493ab068885fcb0efcad53c5d5e5 | |
parent | 8a672c060d2b3946c542c82bd6ca8f89892216ee (diff) |
Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
-rw-r--r-- | src/parser/parser.cpp | 2 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 8 | ||||
-rw-r--r-- | src/theory/model.cpp | 2 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/print_lambda.cvc | 10 |
5 files changed, 20 insertions, 5 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index a469c6fc7..ef386f57e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -164,7 +164,7 @@ Parser::mkFunction(const std::string& name, const Type& type, Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) { stringstream name; - name << prefix << ':' << ++d_anonymousFunctionCount; + name << prefix << "_anon_" << ++d_anonymousFunctionCount; return mkFunction(name.str(), type); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 4fc94947b..14347ff8e 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -212,8 +212,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo // no-op break; case kind::LAMBDA: - op << "LAMBDA"; - opType = PREFIX; + out << "(LAMBDA"; + toStream(out, n[0], depth, types, true); + out << ": "; + toStream(out, n[1], depth, types, true); + out << ")"; + return; break; case kind::APPLY: toStream(op, n.getOperator(), depth, types, true); diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 0e1d90a74..72352f6d3 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -744,7 +744,7 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) } ufmt.setDefaultValue( m, default_v ); ufmt.simplify(); - Node val = ufmt.getFunctionValue( "$x" ); + Node val = ufmt.getFunctionValue( "_ufmt_" ); Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl; m->d_uf_models[n] = val; //ufmt.debugPrint( std::cout, m ); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 13c9f36c1..4789b0a55 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -90,7 +90,8 @@ CVC_TESTS = \ wiki.20.cvc \ wiki.21.cvc \ simplification_bug3.cvc \ - queries0.cvc + queries0.cvc \ + print_lambda.cvc # Regression tests for TPTP inputs TPTP_TESTS = \ diff --git a/test/regress/regress0/print_lambda.cvc b/test/regress/regress0/print_lambda.cvc new file mode 100644 index 000000000..dca97e167 --- /dev/null +++ b/test/regress/regress0/print_lambda.cvc @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-models +; EXPECT: sat +; EXPECT: f : (INT) -> INT = (LAMBDA(_ufmt_1:INT): 0); +; EXIT: 10 + +f : INT -> INT; +ASSERT f(1) = 0; +CHECKSAT; +COUNTEREXAMPLE; + |