From b9b8676beefc3008b85e5dce77b8540e839fd94f Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Fri, 14 May 2010 03:02:40 +0000
Subject: [PATCH] Adding rudimentary ITE handling in CnfStream

---
 src/prop/cnf_stream.cpp           | 42 ++++++++++++++++++++++++++++++-
 src/prop/cnf_stream.h             |  4 +++
 test/regress/regress0/Makefile.am |  2 ++
 test/regress/regress0/ite.smt2    |  6 +++++
 test/regress/regress0/ite2.smt2   |  6 +++++
 5 files changed, 59 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/ite.smt2
 create mode 100644 test/regress/regress0/ite2.smt2

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9abea4fcd..233032706 100644
--- 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 6e4eaf047..ae4582d6f 100644
--- 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 d87ff0541..521fd7feb 100644
--- 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
index 000000000..0e171666f
--- /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
index 000000000..ada94531d
--- /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)
-- 
2.30.2