[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 5bec41e2b27a31de7bb62d5d66e3df1be2037837..0f8ad8e694df4fcba085847822511b349428e005 100644 (file)
--- 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 8f6d9d3b7759d8ffa12eaf0dace4647a238b4101..0172c0845823cb060a4399056fa3c9d1965434fb 100644 (file)
--- 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 be0815668e982ef9ba03c27a626a7128fbd3a3ec..39fa83311dc235494496a1dd097b745347fa2cef 100644 (file)
--- 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 (file)
index 0000000..b21c3f1
--- /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)