summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-11-14 23:49:07 +0000
committerTim King <taking@cs.nyu.edu>2012-11-14 23:49:07 +0000
commit19abe15ccc1e310ae3f726b351b0023670ba7962 (patch)
tree66848c129df4493ab068885fcb0efcad53c5d5e5
parent8a672c060d2b3946c542c82bd6ca8f89892216ee (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.cpp2
-rw-r--r--src/printer/cvc/cvc_printer.cpp8
-rw-r--r--src/theory/model.cpp2
-rw-r--r--test/regress/regress0/Makefile.am3
-rw-r--r--test/regress/regress0/print_lambda.cvc10
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;
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback