Fix symmetric proof issue for ITE in circuit propagator (#7452)

This PR goes back to #7446 and implements a proper fix that handles both symmetrical cases.

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index 3b1e40667684c90b250c88e1c3354cc8621e11c1..fa48f7638e7020221579da5bbc3a77d6cf4a86fc 100644 (file)
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -396,8 +396,10 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
   }
   if (d_parentAssignment)
   {
-    return mkResolution(
-        mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], true);
+    return mkResolution(mkProof(c == 0 ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2,
+                                {assume(d_parent)}),
+                        d_parent[c + 1],
+                        true);
   }
   return mkResolution(
       mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}),

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fe7c3fdaf2339122b0b8f31d5b17c363d07455d5..1ed42dd77c52078e0d52a8dc41d628dc3425fd74 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -835,7 +835,8 @@ set(regress_0_tests
   regress0/preprocess/preprocess_14.cvc.smt2
   regress0/preprocess/preprocess_15.cvc.smt2
   regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
-  regress0/preprocess/proj-issue305-circuit-prop-ite.smt2
+  regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2
+  regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2
   regress0/print_define_fun_internal.smt2
   regress0/print_lambda.cvc.smt2
   regress0/print_model.cvc.smt2

diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2
new file mode 100644 (file)
index 0000000..6760bdf
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-const x Bool)
+(declare-const y Bool)
+(declare-const z Bool)
+(assert y)
+(assert (not z))
+(assert (ite x y z))
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2
new file mode 100644 (file)
index 0000000..fcb2605
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert c)
+(assert (not b))
+(assert (ite a b c))
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2
deleted file mode 100644 (file)
index 6760bdf..0000000
--- a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; EXPECT: sat
-(set-logic ALL)
-(set-option :check-proofs true)
-(declare-const x Bool)
-(declare-const y Bool)
-(declare-const z Bool)
-(assert y)
-(assert (not z))
-(assert (ite x y z))
-(check-sat)
\ No newline at end of file