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 /src | |
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.
Diffstat (limited to 'src')
-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 |
3 files changed, 8 insertions, 4 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 ); |