From 6a6630bf6fa4b68c6a483b767be4c696da8fd0bd Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 7 Nov 2014 16:16:57 -0500
Subject: Corrected fix for missing case in model postprocessor (resolves bug
 #595).

---
 src/smt/model_postprocessor.cpp | 46 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

(limited to 'src/smt/model_postprocessor.cpp')

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index dd9d0a78c..7c2742ce4 100644
--- 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;
@@ -235,6 +244,43 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     Debug("boolean-terms") << "model-post: " << current << endl
                            << "- returning " << n << endl;
     d_nodes[current] = n;
+  } else if(current.getKind() == kind::LAMBDA) {
+    // 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());
+      if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        TNode op = current.getOperator();
+        Node realOp;
+        if(op.getAttribute(BooleanTermAttr(), realOp)) {
+          nb << realOp;
+        } else {
+          nb << op;
+        }
+      }
+      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;
+    }
   } else {
     Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
     // rewrite to self
-- 
cgit v1.2.3