Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC printer...

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index a469c6fc7b2fda4ce40aaf63857fd3b776cea6f5..ef386f57e7283e1ee965324716c0feb2cb4b111e 100644 (file)
--- 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 4fc94947bba24bacc3a36a6ea15dd57a613d6887..14347ff8e72bfd96ef278a308b94914c06083685 100644 (file)
--- 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 0e1d90a7478f3207b9caee2cfc26f53a179ba142..72352f6d3c65e1b809318b39f45a0347771539d6 100644 (file)
--- 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 13c9f36c1aee421a43c95f506e6b670c0a657dea..4789b0a5548c4b916a03e0f3ebeb292b58fe306d 100644 (file)
--- 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 (file)
index 0000000..dca97e1
--- /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;
+