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.

4 files changed, 38 insertions, 34 deletions

diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 25529f1c8..b41cd9715 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -220,18 +220,19 @@ void translate_to_isat(const map<Expr, unsigned>& variables, const Expr& asserti
         cout << " -> ";
         translate_to_isat(variables, assertion[1]);
         cout << ")";
-        break;
-      case kind::IFF:
-        cout << "(";
-        translate_to_isat(variables, assertion[0]);
-        cout << " <-> ";
-        translate_to_isat(variables, assertion[1]);
-        cout << ")";
-        break;            
+        break;          
       case kind::EQUAL:
-        op = "=";
-        theory = true;
-	break;
+        if( assertion[0].getType().isBoolean() ){
+          cout << "(";
+          translate_to_isat(variables, assertion[0]);
+          cout << " <-> ";
+          translate_to_isat(variables, assertion[1]);
+          cout << ")";
+        }else{
+          op = "=";
+          theory = true;
+        }
+	      break;
       case kind::LT:
         op = "<";
         theory = true;
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index f261705d5..c593cf72c 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -214,18 +214,19 @@ void translate_to_mathematica(const map<Expr, unsigned>& variables, const Expr&
         cout << ",";
         translate_to_mathematica(variables, assertion[1]);
         cout << "]";
-        break;
-      case kind::IFF:
+        break;         
+      case kind::EQUAL:
+      if( assertion[0].getType().isBoolean() ){
         cout << "Equivalent[";
         translate_to_mathematica(variables, assertion[0]);
         cout << ",";
         translate_to_mathematica(variables, assertion[1]);
         cout << "]";
-        break;            
-      case kind::EQUAL:
+      }else{
         op = "==";
         theory = true;
-	break;
+      }
+	      break;
       case kind::LT:
         op = "<";
         theory = true;
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index 800c02164..30b0afbbb 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -219,14 +219,15 @@ void translate_to_qepcad(const std::map<Expr, unsigned>& variables,
         op = "==>";
         binary =  true;
         break;
-      case kind::IFF:
-        op = "<==>";
-        binary =  true;
-        break;
       case kind::EQUAL:
-        op = "=";
-        theory =  true;
-	break;
+        if( assertion[0].getType().isBoolean() ){
+          op = "<==>";
+          binary =  true;
+        }else{
+          op = "=";
+          theory =  true;
+        }
+	      break;
       case kind::LT:
         op = "<";
         theory =  true;
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index eb85186be..53241413f 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -228,18 +228,19 @@ void translate_to_redlog(const map<Expr, unsigned>& variables, const Expr& asser
         cout << " impl ";
         translate_to_redlog(variables, assertion[1]);
         cout << ")";
-        break;
-      case kind::IFF:
-        cout << "(";
-        translate_to_redlog(variables, assertion[0]);
-        cout << " equiv ";
-        translate_to_redlog(variables, assertion[1]);
-        cout << ")";
-        break;            
+        break;          
       case kind::EQUAL:
-        op = "=";
-        theory = true;
-	break;
+        if( assertion[0].getType().isBoolean() ){
+          cout << "(";
+          translate_to_redlog(variables, assertion[0]);
+          cout << " equiv ";
+          translate_to_redlog(variables, assertion[1]);
+          cout << ")";
+        }else{
+          op = "=";
+          theory = true;
+        }
+	      break;
       case kind::LT:
         op = "<";
         theory = true;