Fix missing case in model postprocessor (resolves bug #595).

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index dd9d0a78caa4ac81ef1c3881ac00089fb5c73bd9..c0c865b9849056548647acc1d88180769683b144 100644 (file)
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -27,6 +27,15 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     // good to go, we have the right type
     return n;
   }
+  if(n.getKind() == kind::LAMBDA) {
+    Assert(asType.isFunction());
+    Node rhs = rewriteAs(n[1], asType[1]);
+    Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs);
+    Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl;
+    Debug("boolean-terms") << "need type " << asType << endl;
+    Assert(out.getType() == asType);
+    return out;
+  }
   if(!n.isConst()) {
     // we don't handle non-const right now
     return n;
@@ -236,8 +245,32 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
                            << "- returning " << n << endl;
     d_nodes[current] = n;
   } else {
-    Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
-    // rewrite to self
-    d_nodes[current] = Node::null();
+    // rewrite based on children
+    bool self = true;
+    for(size_t i = 0; i < current.getNumChildren(); ++i) {
+      Assert(d_nodes.find(current[i]) != d_nodes.end());
+      if(!d_nodes[current[i]].isNull()) {
+        self = false;
+        break;
+      }
+    }
+    if(self) {
+      Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
+      // rewrite to self
+      d_nodes[current] = Node::null();
+    } else {
+      // rewrite based on children
+      NodeBuilder<> nb(current.getKind());
+      for(size_t i = 0; i < current.getNumChildren(); ++i) {
+        Assert(d_nodes.find(current[i]) != d_nodes.end());
+        TNode rw = d_nodes[current[i]];
+        if(rw.isNull()) {
+          rw = current[i];
+        }
+        nb << rw;
+      }
+      d_nodes[current] = nb;
+      Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << endl;
+    }
   }
 }/* ModelPostprocessor::visit() */

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dcfc526eca3fbb9dd8799be6a1b9d1274103c29c..ea52f43a7fa97a1d16388f69c6ad6a969a82ab94 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3417,6 +3417,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   ModelPostprocessor mpost;
   NodeVisitor<ModelPostprocessor> visitor;
+  Debug("boolean-terms") << "postproc: visit " << node << endl;
   Node value = visitor.run(mpost, node);
   Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
   Node realValue = mpost.rewriteAs(value, expectedType);

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index c0ee0f2bb6d3e3d443a14a1d32a23dac0ff43db1..15888fbcea3049295fd9212f5ea343f6338c7087 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -166,7 +166,8 @@ BUG_TESTS = \
        bug576a.smt2 \
        bug578.smt2 \
        bug585.cvc \
-       bug586.cvc
+       bug586.cvc \
+       bug595.cvc
 
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/bug595.cvc b/test/regress/regress0/bug595.cvc
new file mode 100644 (file)
index 0000000..c11cfb6
--- /dev/null
+++ b/test/regress/regress0/bug595.cvc
@@ -0,0 +1,7 @@
+% EXPECT: sat
+
+f : INT -> [# i:INT, b:INT #];
+a : INT;
+ASSERT f(a) /= (# i := 0, b := 0 #);
+
+CHECKSAT;