Adding rudimentary ITE handling in CnfStream

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9abea4fcdea5f9571b16596a7a787a043d48934d..2330327060e8a0c579b64e3ce73e2b6adbcce3da 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -306,6 +306,46 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   return iteLit;
 }
 
+Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
+  /* Our main goal here is to tease out any ITE's sitting under a theory operator. */
+  Node rewrite;
+  NodeManager *nodeManager = NodeManager::currentNM();
+  if(nodeManager->getAttribute(node, IteRewriteAttr(), rewrite)) {
+    return rewrite.isNull() ? Node(node) : rewrite;
+  }
+
+  if(node.getKind() == ITE) {
+    Assert( node.getNumChildren() == 3 );
+    Node skolem = nodeManager->mkVar(node.getType());
+    Node newAssertion =
+        nodeManager->mkNode(
+            ITE,
+            node[0],
+            nodeManager->mkNode(EQUAL, skolem, node[1]),
+            nodeManager->mkNode(EQUAL, skolem, node[2]));
+    nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
+    convertAndAssert( newAssertion );
+    return skolem;
+  } else {
+    std::vector<Node> newChildren;
+    bool somethingChanged = false;
+    for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+      Node newChild = handleNonAtomicNode(*it);
+      somethingChanged |= (newChild != *it);
+      newChildren.push_back(newChild);
+    }
+
+    if(somethingChanged) {
+      rewrite = nodeManager->mkNode(node.getKind(), newChildren);
+      nodeManager->setAttribute(node, IteRewriteAttr(), rewrite);
+      return rewrite;
+    } else {
+      nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
+      return node;
+    }
+  }
+}
+
 SatLiteral TseitinCnfStream::toCNF(TNode node) {
 
   // If the node has already been translated, return the previous translation
@@ -335,7 +375,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
   case AND:
     return handleAnd(node);
   default:
-    Unreachable();
+    return handleAtom(handleNonAtomicNode(node));
   }
 }
 

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 6e4eaf047c66d0d3175fad8dea4fd980f522fbfd..ae4582d6f746b28f2799fb5ba399410cf5c8dc82 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -202,6 +202,10 @@ private:
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
 
+  struct IteRewriteTag {};
+  typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
+  Node handleNonAtomicNode(TNode node);
+
   /**
    * Transforms the node into CNF recursively.
    * @param node the formula to transform

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d87ff05411ac4dbd254bd677d2a527d0fb505db2..521fd7feb58e5a6aa29d8eafd7fc3c80b5e71afe 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -12,6 +12,8 @@ TESTS =       \
        simple2.smt \
        simple.smt \
        simple-uf.smt \
+       ite.smt2 \
+       ite2.smt2 \
        bug32.cvc \
        hole6.cvc \
        logops.01.cvc \

diff --git a/test/regress/regress0/ite.smt2 b/test/regress/regress0/ite.smt2
new file mode 100644 (file)
index 0000000..0e17166
--- /dev/null
+++ b/test/regress/regress0/ite.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (not (= x (ite true x y))))
+(check-sat)

diff --git a/test/regress/regress0/ite2.smt2 b/test/regress/regress0/ite2.smt2
new file mode 100644 (file)
index 0000000..ada9453
--- /dev/null
+++ b/test/regress/regress0/ite2.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LRA)
+(set-info :status sat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (not (= x (ite true y x))))
+(check-sat)