Eliminate Boolean ITE within terms, fixes 2947 (#2949)

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index ff17c562217da6d8209d893483715c5607a168a5..f610cc7df5fdfbf3471b5cbbc56f68488b37c4f6 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -84,9 +84,13 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   TypeNode nodeType = node.getType();
   Node skolem;
   Node newAssertion;
-  if(node.getKind() == kind::ITE) {
-    // If an ITE, replace it
-    if (!nodeType.isBoolean() && (!inQuant || !expr::hasBoundVar(node)))
+  // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled
+  // in the "non-variable Boolean term within term" case below.
+  if (node.getKind() == kind::ITE && !nodeType.isBoolean())
+  {
+    // Here, we eliminate the ITE if we are not Boolean and if we do not contain
+    // a bound variable.
+    if (!inQuant || !expr::hasBoundVar(node))
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
@@ -163,13 +167,15 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
            && inTerm
            && !inQuant)
   {
-    // if a non-variable Boolean term, replace it
+    // if a non-variable Boolean term within another term, replace it
     skolem = getSkolemForNode(node);
     if (skolem.isNull())
     {
       // Make the skolem to represent the Boolean term
-      // skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable
-      // introduced due to Boolean term removal");
+      // Skolems introduced for Boolean formulas appearing in terms have a
+      // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled
+      // properly in theory combination. We must use this kind here instead of a
+      // generic skolem.
       skolem = nodeManager->mkBooleanTermVariable();
       d_skolem_cache.insert(node, skolem);
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 64da9ec61f5d380e6916fb9c090ebbc4b4b1323a..687dfc6f205841b40f67d9aabceaf2a5e21dac66 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -933,6 +933,7 @@ set(regress_0_tests
   regress0/uf/euf_simp12.smt
   regress0/uf/euf_simp13.smt
   regress0/uf/iso_brn001.smt
+  regress0/uf/issue2947.smt2
   regress0/uf/pred.smt
   regress0/uf/simple.01.cvc
   regress0/uf/simple.02.cvc

diff --git a/test/regress/regress0/uf/issue2947.smt2 b/test/regress/regress0/uf/issue2947.smt2
new file mode 100644 (file)
index 0000000..6bb60b9
--- /dev/null
+++ b/test/regress/regress0/uf/issue2947.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-fun f (Bool) Bool)
+(assert
+  (not (f true))
+)
+(assert
+  (f (ite (f true) true (f false)))
+)
+(check-sat)
+(exit)