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, 8 insertions, 3 deletions

diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 1f68fb787..41099552d 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -366,8 +366,13 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) {
     return false;
   }else{
     Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
-    Assert( ak!=NOT );
-    return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+    if( ak==EQUAL ){
+      Node atom = n.getKind() ? n[0] : n;
+      return !atom[0].getType().isBoolean();
+    }else{
+      Assert( ak!=NOT );
+      return ak!=AND && ak!=OR && ak!=ITE;
+    }
   }
 }
 
@@ -466,7 +471,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s
                 addArgument( c, args, watch, is_watch );
                 abort_i = i;
                 break;
-              }else if( k==kind::AND || k==kind::OR || k==kind::ITE || k==IFF ){
+              }else if( k==kind::AND || k==kind::OR || k==kind::ITE || ( k==EQUAL && n[0].getType().isBoolean() ) ){
                 Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl;
                 if( ( k==kind::AND || k==kind::OR  ) && c.getKind()==k ){
                   //flatten