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.

8 files changed, 68 insertions, 48 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index b7ed0b2ec..0f0c14eb2 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_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
@@ -429,7 +429,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
       //       we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
       //       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
 
@@ -487,8 +487,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
               } else {
                 // We have a "next node". Use it to guide us.
 
-                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL ||
-                       nodeAfterEqualitySequence.getKind() == kind::IFF);
+                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
 
                 if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
 
@@ -533,7 +532,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
       Debug("pf::arith") << "\ndoing trans proof, got n2 " << n2 << "\n";
       if(tb == 1) {
         Debug("pf::arith") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
-        Debug("pf::arith") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n";
+        Debug("pf::arith") << (n2.getKind() == kind::EQUAL) << "\n";
 
         if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
           Debug("pf::arith") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
@@ -549,8 +548,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
       }
       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]) {
@@ -580,7 +578,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
           Unreachable();
         }
         Debug("pf::arith") << "++ 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];
@@ -591,7 +589,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
         } 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];
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];
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index cbe54ff4b..926dae9fd 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -412,7 +412,7 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) {
 }
 
 void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) {
-  std::string op = utils::toLFSCKind(term.getKind());
+  std::string op = utils::toLFSCKindTerm(term);
   std::ostringstream paren;
   std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : "";
   unsigned size = term.getKind() == kind::BITVECTOR_CONCAT? utils::getSize(term) :
@@ -431,7 +431,7 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Pr
 
 void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) {
   os <<"(";
-  os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
+  os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
   os << " ";
   d_proofEngine->printBoundTerm(term[0], os, map);
   os <<")";
@@ -439,7 +439,7 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const P
 
 void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) {
   os <<"(";
-  os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" ";
+  os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" ";
   os << " ";
   d_proofEngine->printBoundTerm(term[0], os, map);
   os << " ";
@@ -449,7 +449,7 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const Proof
 
 void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) {
   os <<"(";
-  os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
+  os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
   os <<" ";
   if (term.getKind() == kind::BITVECTOR_REPEAT) {
     unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
@@ -872,7 +872,7 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool
   case kind::EQUAL: {
     Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
 
-    os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind());
+    os << "(bv_bbl_" << utils::toLFSCKindTerm(atom);
 
     if (swap) {os << "_swap";}
 
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index b58ade35e..69b613f28 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -596,16 +596,16 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
         os << ")";
       }
     }
-  }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){
+  }else if( base_assertion.getKind()==kind::XOR || ( base_assertion.getKind()==kind::EQUAL && base_assertion[0].getType().isBoolean() ) ){
     //eliminate negation
     int num_nots_2 = 0;
     int num_nots_1 = 0;
     Kind k;
     if( !base_pol ){
-      if( base_assertion.getKind()==kind::IFF ){
+      if( base_assertion.getKind()==kind::EQUAL ){
         num_nots_2 = 1;
       }
-      k = kind::IFF;
+      k = kind::EQUAL;
     }else{
       k = base_assertion.getKind();
     }
@@ -623,7 +623,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
         if( i==0 ){
           //figure out which way to elim
           elimNum = child_pol==childPol[child_base] ? 2 : 1;
-          if( (elimNum==2)==(k==kind::IFF) ){
+          if( (elimNum==2)==(k==kind::EQUAL) ){
             num_nots_2++;
           }
           if( elimNum==1 ){
@@ -651,9 +651,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
         os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
       }
       Assert( elimNum!=0 );
-      os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
+      os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
       if( !base_pol ){
-        os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
+        os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
       }else{
         os_base_n << os_base.str();
       }
diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp
index fe0d42242..3ace236b5 100644
--- a/src/proof/proof_utils.cpp
+++ b/src/proof/proof_utils.cpp
@@ -41,7 +41,6 @@ std::string toLFSCKind(Kind kind) {
   case kind::AND: return "and";
   case kind::XOR: return "xor";
   case kind::EQUAL: return "=";
-  case kind::IFF: return "iff";
   case kind::IMPLIES: return "impl";
   case kind::NOT: return "not";
 
@@ -123,5 +122,18 @@ std::string toLFSCKind(Kind kind) {
   }
 }
 
+std::string toLFSCKindTerm(Expr node) {
+  Kind k = node.getKind();
+  if( k==kind::EQUAL ){
+    if( node[0].getType().isBoolean() ){
+      return "iff";
+    }else{
+      return "=";
+    }
+  }else{
+    return toLFSCKind( k );
+  }
+}
+
 } /* namespace CVC4::utils */
 } /* namespace CVC4 */
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index b172217d8..a7590451d 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -88,6 +88,7 @@ typedef std::vector<LetOrderElement> Bindings;
 namespace utils {
 
 std::string toLFSCKind(Kind kind);
+std::string toLFSCKindTerm(Expr node);
 
 inline unsigned getExtractHigh(Expr node) {
   return node.getOperator().getConst<BitVectorExtract>().high;
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 1912dbada..156c90e47 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -856,9 +856,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
 
   case kind::EQUAL:
     os << "(";
-    os << "= ";
-    printSort(term[0].getType(), os);
-    os << " ";
+    if( term[0].getType().isBoolean() ){
+      os << "iff ";
+    }else{
+      os << "= ";
+      printSort(term[0].getType(), os);
+      os << " ";
+    }
     printBoundTerm(term[0], os, map);
     os << " ";
     printBoundTerm(term[1], os, map);
@@ -912,6 +916,12 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
     // LFSC doesn't allow declarations with variable numbers of
     // arguments, so we have to flatten chained operators, like =.
     Kind op = term.getOperator().getConst<Chain>().getOperator();
+    std::string op_str;
+    if( op==kind::EQUAL && term[0].getType().isBoolean() ){
+      op_str = "iff";
+    }else{
+      op_str = utils::toLFSCKind(op);
+    }
     size_t n = term.getNumChildren();
     std::ostringstream paren;
     for(size_t i = 1; i < n; ++i) {
@@ -919,7 +929,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
         os << "(" << utils::toLFSCKind(kind::AND) << " ";
         paren << ")";
       }
-      os << "(" << utils::toLFSCKind(op) << " ";
+      os << "(" << op_str << " ";
       printBoundTerm(term[i - 1], os, map);
       os << " ";
       printBoundTerm(term[i], os, map);
@@ -1096,7 +1106,6 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
     // If letification is off or there were 2 children, same treatment as the other cases.
     // (No break is intentional).
   case kind::XOR:
-  case kind::IFF:
   case kind::IMPLIES:
   case kind::NOT:
     // print the Boolean operators
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 27f351102..41262051c 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_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
@@ -472,7 +472,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       //       we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
       //       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
 
@@ -530,8 +530,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
               } else {
                 // We have a "next node". Use it to guide us.
 
-                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL ||
-                       nodeAfterEqualitySequence.getKind() == kind::IFF);
+                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
 
                 if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
 
@@ -576,7 +575,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       Debug("pf::uf") << "\ndoing trans proof, got n2 " << n2 << "\n";
       if(tb == 1) {
         Debug("pf::uf") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
-        Debug("pf::uf") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n";
+        Debug("pf::uf") << (n2.getKind() == kind::EQUAL) << "\n";
 
         if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
           Debug("pf::uf") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
@@ -592,8 +591,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       }
       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]) {
@@ -623,24 +621,24 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
           Unreachable();
         }
         Debug("pf::uf") << "++ 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].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n1[1].eqNode(NodeManager::currentNM()->mkConst(true));
           ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
         } else if(n1[1] == n2) {
-          n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n1[0].eqNode(NodeManager::currentNM()->mkConst(true));
           ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
         } 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].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n2[1].eqNode(NodeManager::currentNM()->mkConst(true));
           ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
         } else if(n2[1] == n1) {
-          n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n2[0].eqNode(NodeManager::currentNM()->mkConst(true));
           ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
         } else {
           Unreachable();
@@ -707,6 +705,10 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
     os << term;
     return;
   }
+  if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+    os << "(p_app " << term << ")";
+    return;
+  }
 
   Assert (term.getKind() == kind::APPLY_UF);
   d_proofEngine->treatBoolsAsFormulas(false);