From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 21 Oct 2021 19:10:26 +0000 (-0700)
Subject: Fix symmetric proof issue for ITE in circuit propagator (#7452)
X-Git-Tag: cvc5-1.0.0~1013
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f3bf9af12eb6af487e61c585fa9639f1d1485220;p=cvc5.git

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 3b1e40667..fa48f7638 100644
--- 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 fe7c3fdaf..1ed42dd77 100644
--- 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
index 000000000..6760bdf4d
--- /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
index 000000000..fcb26054e
--- /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
index 6760bdf4d..000000000
--- 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