From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 13 Jul 2021 18:38:23 +0000 (-0300)
Subject: [rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)
X-Git-Tag: cvc5-1.0.0~1497
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=912be5c60f194c3b0d52c1d06a1339fb6cb13a9c;p=cvc5.git

[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)

Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.
---

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 5bec41e2b..0f8ad8e69 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -336,6 +336,10 @@ void SatProofManager::explainLit(SatLiteral lit,
   Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
   Node litNode = getClauseNode(lit);
   Trace("sat-proof") << " [" << litNode << "]\n";
+  // Note that if we had two literals for (= a b) and (= b a) and we had already
+  // a proof for (= a b) this test would return true for (= b a), which could
+  // lead to open proof. However we should never have two literals like this in
+  // the SAT solver since they'd be rewritten to the same one
   if (d_resChainPg.hasProofFor(litNode))
   {
     Trace("sat-proof") << "SatProofManager::explainLit: already justified "
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 8f6d9d3b7..0172c0845 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -36,7 +36,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
  * flattenNode looks for children of same kind, and if found merges
  * them into the parent.
  *
- * It simultaneously handles a couple of other optimizations: 
+ * It simultaneously handles a couple of other optimizations:
  * - trivialNode - if found during exploration, return that node itself
  *    (like in case of OR, if "true" is found, makes sense to replace
  *     whole formula with "true")
@@ -287,7 +287,13 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
         }
       }
     }
-    break;
+    // sort
+    if (n[0].getId() > n[1].getId())
+    {
+      return RewriteResponse(REWRITE_AGAIN,
+                             nodeManager->mkNode(kind::EQUAL, n[1], n[0]));
+    }
+    return RewriteResponse(REWRITE_DONE, n);
   }
   case kind::XOR: {
     // rewrite simple cases of XOR
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index be0815668..39fa83311 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -828,6 +828,7 @@ set(regress_0_tests
   regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc
   regress0/proofs/issue277-circuit-propagator.smt2
+  regress0/proofs/open-pf-if-unordered-iff.smt2
   regress0/proofs/scope.smt2
   regress0/proofs/trust-subs-eq-open.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
diff --git a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
new file mode 100644
index 000000000..b21c3f142
--- /dev/null
+++ b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const __ (_ BitVec 3))
+(declare-const ___ (_ BitVec 3))
+(assert (= (_ bv0 64) (bvand (_ bv1 64) ((_ zero_extend 32) ((_ zero_extend 16) ((_ zero_extend 8) ((_ zero_extend 4) ((_ zero_extend 1) __))))))))
+(assert (bvule __ ___))
+(assert (= (_ bv0 64) (bvand (_ bv1 64) (bvadd (_ bv1 64) ((_ zero_extend 32) ((_ zero_extend 16) ((_ zero_extend 8) ((_ zero_extend 4) ((_ zero_extend 1) ___)))))))))
+(assert (bvule ___ __))
+(check-sat)