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.

1 files changed, 7 insertions, 9 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 32a7c247d..cc60d8c07 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -24,7 +24,7 @@
 namespace CVC4 {
 
 inline static Node eqNode(TNode n1, TNode n2) {
-  return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
+  return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
 }
 
 // congrence matching term helper
@@ -640,7 +640,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       //       b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
       //       and use it to determine which option we need.
 
-      if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+      if(n2.getKind() == kind::EQUAL) {
         if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
           // We are in a sequence of identical equalities
 
@@ -701,8 +701,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                   nodeAfterEqualitySequence = nodeAfterEqualitySequence[0];
                 }
 
-                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL ||
-                       nodeAfterEqualitySequence.getKind() == kind::IFF);
+                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
 
                 if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
 
@@ -747,7 +746,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n";
       if(tb == 1) {
         Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
-        Debug("mgdx") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n";
+        Debug("mgdx") << (n2.getKind() == kind::EQUAL) << "\n";
 
         if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
           Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
@@ -784,8 +783,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         ss << "(trans _ _ _ _ ";
       }
 
-      if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) &&
-         (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF))
+      if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL))
         // Both elements of the transitivity rule are equalities/iffs
       {
         if(n1[0] == n2[0]) {
@@ -824,7 +822,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
           Unreachable();
         }
         Debug("mgd") << "++ trans proof[" << i << "], now have " << n1 << std::endl;
-      } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) {
+      } else if(n1.getKind() == kind::EQUAL) {
         // n1 is an equality/iff, but n2 is a predicate
         if(n1[0] == n2) {
           n1 = n1[1];
@@ -836,7 +834,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         } else {
           Unreachable();
         }
-      } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+      } else if(n2.getKind() == kind::EQUAL) {
         // n2 is an equality/iff, but n1 is a predicate
         if(n2[0] == n1) {
           n1 = n2[1];