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, 13 insertions, 1 deletions

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 */