Fix proof for xor in circuit propagator (#7525)

This PR fixes another double negation issue in the circuit propagator.
Fixes cvc5/cvc5-projects#332.

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index e462414d1aa7d1d1153c9c264c309a0e3469f727..1ec8f7b67ca228b160e3031c94e13bda5e019b69 100644 (file)
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -206,11 +206,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated,
         parent[1],
         false));
   }
-  return mkResolution(
-      mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1,
-              {assume(negated ? parent.notNode() : Node(parent))}),
-      parent[1],
-      true);
+  return mkNot(
+      mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1,
+                           {assume(negated ? parent.notNode() : Node(parent))}),
+                   parent[1],
+                   true));
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2430eb13f9f7b9f9f59633cf80b3e63ada534e2c..8b8a6a926d28f2df84969cc927ac1a077b7a6fc5 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -846,6 +846,7 @@ set(regress_0_tests
   regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2
   regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2
   regress0/preprocess/proj-issue309-circuit-prop-ite.smt2
+  regress0/preprocess/proj-issue332-circuit-prop-xor.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-issue332-circuit-prop-xor.smt2 b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2
new file mode 100644 (file)
index 0000000..841e739
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-const x Real)
+(declare-const x4 Real)
+(declare-const x8 Bool)
+(assert (<= x4 x))
+(assert (not (xor (> x4 x) x8)))
+(check-sat)