Fix issues with double negation in circuit propagator (#6669)

This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index 6c4e0f96b5f246c614d1998cd151d45cc19f9083..ed4f81cb316e6f8f3e187ea14ed81a2a4243fcaf 100644 (file)
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -169,11 +169,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y,
   {
     return nullptr;
   }
-  return mkResolution(
+  return mkNot(mkResolution(
       mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
               {assume(parent.notNode())}),
       parent[1],
-      !y);
+      !y));
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
@@ -183,11 +183,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
   {
     return nullptr;
   }
-  return mkResolution(
+  return mkNot(mkResolution(
       mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
               {assume(parent.notNode())}),
       parent[0],
-      !x);
+      !x));
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 39f1985b018c1db1c785fc20bc9fc7fd67f1128d..3adb3ebbbcdf1b56bf94f3dae085391ba80f32ba 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -800,6 +800,7 @@ set(regress_0_tests
   regress0/printer/let_shadowing.smt2
   regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc
+  regress0/proofs/issue277-circuit-propagator.smt2
   regress0/proofs/scope.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2

diff --git a/test/regress/regress0/proofs/issue277-circuit-propagator.smt2 b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2
new file mode 100644 (file)
index 0000000..f0815e8
--- /dev/null
+++ b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2
@@ -0,0 +1,47 @@
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_UF)
+(set-option :produce-proofs true)
+(set-option :incremental true)
+(declare-fun p () Bool)
+(declare-fun q () Bool)
+
+(push)
+(assert (not (= p (not q))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not q) p)))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not p) (not (not q)))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not q)) (not p))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not p)) (not (not (not q))))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not (not q))) (not (not p)))))
+(assert p)
+(check-sat)
+(pop)
\ No newline at end of file