From 1f4b954a2cc7667a56a3007fa75c125fba93ed23 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Mar 2017 14:45:21 -0600
Subject: Eliminate Boolean term conversion. Generalizes removeITE pass to
 remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as
 theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

---
 src/prop/cnf_stream.cpp | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

(limited to 'src/prop')

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index f2401041e..bc819801b 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -242,7 +242,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
   bool preRegister = false;
 
   // Is this a variable add it to the list
-  if (node.isVar()) {
+  if (node.isVar() && node.getKind()!=BOOLEAN_TERM_VARIABLE) {
     d_booleanVariables.push_back(node);
   } else {
     theoryLiteral = true;
@@ -389,7 +389,7 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 
 SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   Assert(!hasLiteral(iffNode), "Atom already mapped!");
-  Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
+  Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!");
   Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
   Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
@@ -488,9 +488,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     case ITE:
       nodeLit = handleIte(node);
       break;
-    case IFF:
-      nodeLit = handleIff(node);
-      break;
     case IMPLIES:
       nodeLit = handleImplies(node);
       break;
@@ -502,8 +499,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
       break;
     case EQUAL:
       if(node[0].getType().isBoolean()) {
-        // normally this is an IFF, but EQUAL is possible with pseudobooleans
-        nodeLit = handleIff(node[0].iffNode(node[1]));
+        nodeLit = handleIff(node);
       } else {
         nodeLit = convertAtom(node);
       }
@@ -722,9 +718,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   case OR:
     convertAndAssertOr(node, negated);
     break;
-  case IFF:
-    convertAndAssertIff(node, negated);
-    break;
   case XOR:
     convertAndAssertXor(node, negated);
     break;
@@ -737,6 +730,11 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   case NOT:
     convertAndAssert(node[0], !negated);
     break;
+  case EQUAL:
+    if( node[0].getType().isBoolean() ){
+      convertAndAssertIff(node, negated);
+      break;
+    }
   default:
   {
     Node nnode = node;
-- 
cgit v1.2.3