From 19abe15ccc1e310ae3f726b351b0023670ba7962 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 14 Nov 2012 23:49:07 +0000
Subject: [PATCH] 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.

---
 src/parser/parser.cpp                  |  2 +-
 src/printer/cvc/cvc_printer.cpp        |  8 ++++++--
 src/theory/model.cpp                   |  2 +-
 test/regress/regress0/Makefile.am      |  3 ++-
 test/regress/regress0/print_lambda.cvc | 10 ++++++++++
 5 files changed, 20 insertions(+), 5 deletions(-)
 create mode 100644 test/regress/regress0/print_lambda.cvc

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;
+
-- 
2.30.2