From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 18 Sep 2020 16:32:47 +0000 (-0300)
Subject: [proof-new] Proof utilities for normalizing clauses at the Node level (#5089)
X-Git-Tag: cvc5-1.0.0~2837
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e040d5e9e9d8c01138b4b961a1118b7342735d87;p=cvc5.git

[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)

Extends Theory Proof Step Buffer. These utilities are used so that we can account for the fact that Minisat silenly does these transformations on added clauses.
---

diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp
index 8a518b49a..97936011b 100644
--- a/src/theory/theory_proof_step_buffer.cpp
+++ b/src/theory/theory_proof_step_buffer.cpp
@@ -90,5 +90,119 @@ Node TheoryProofStepBuffer::applyPredElim(Node src,
   return srcRew;
 }
 
+Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
+{
+  if (n.getKind() != kind::OR)
+  {
+    return elimDoubleNegLit(n);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> children{n.begin(), n.end()};
+  std::vector<Node> childrenEqs;
+  // eliminate double neg for each lit. Do it first because it may expose
+  // duplicates
+  bool hasDoubleNeg = false;
+  for (unsigned i = 0; i < children.size(); ++i)
+  {
+    if (children[i].getKind() == kind::NOT
+        && children[i][0].getKind() == kind::NOT)
+    {
+      hasDoubleNeg = true;
+      childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
+      addStep(PfRule::MACRO_SR_PRED_INTRO,
+              {},
+              {childrenEqs.back()},
+              childrenEqs.back());
+      // update child
+      children[i] = children[i][0][0];
+    }
+    else
+    {
+      childrenEqs.push_back(children[i].eqNode(children[i]));
+      addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back());
+    }
+  }
+  if (hasDoubleNeg)
+  {
+    Node oldn = n;
+    n = nm->mkNode(kind::OR, children);
+    // Create a congruence step to justify replacement of each doubly negated
+    // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
+    // from the old clause to the new one, which, under the standard rewriter,
+    // may not hold. An example is
+    //
+    //   ---------------------------------------------------------------------
+    //   (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
+    //
+    // which fails due to factoring not happening after flattening.
+    //
+    // Using congruence only the
+    //
+    //  ------------------ MACRO_SR_PRED_INTRO
+    //  (not (not t)) = t
+    //
+    // steps are added, which, since double negation is eliminated in a
+    // pre-rewrite in the Boolean rewriter, will always hold under the
+    // standard rewriter.
+    Node congEq = oldn.eqNode(n);
+    addStep(PfRule::CONG,
+            childrenEqs,
+            {ProofRuleChecker::mkKindNode(kind::OR)},
+            congEq);
+    // add an equality resolution step to derive normalize clause
+    addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
+  }
+  children.clear();
+  // remove duplicates while keeping the order of children
+  std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+  unsigned size = n.getNumChildren();
+  for (unsigned i = 0; i < size; ++i)
+  {
+    if (clauseSet.count(n[i]))
+    {
+      continue;
+    }
+    children.push_back(n[i]);
+    clauseSet.insert(n[i]);
+  }
+  // if factoring changed
+  if (children.size() < size)
+  {
+    Node factored = children.empty()
+                        ? nm->mkConst<bool>(false)
+                        : children.size() == 1 ? children[0]
+                                               : nm->mkNode(kind::OR, children);
+    // don't overwrite what already has a proof step to avoid cycles
+    addStep(PfRule::FACTORING, {n}, {}, factored);
+    n = factored;
+  }
+  // nothing to order
+  if (children.size() < 2)
+  {
+    return n;
+  }
+  // order
+  std::sort(children.begin(), children.end());
+  Node ordered = nm->mkNode(kind::OR, children);
+  // if ordering changed
+  if (ordered != n)
+  {
+    // don't overwrite what already has a proof step to avoid cycles
+    addStep(PfRule::REORDERING, {n}, {ordered}, ordered);
+  }
+  return ordered;
+}
+
+Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
+{
+  // eliminate double neg
+  if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
+  {
+    addStep(PfRule::MACRO_SR_PRED_TRANSFORM, {n}, {n[0][0]}, n[0][0]);
+    return n[0][0];
+  }
+  return n;
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h
index 55b4ee1c0..554d7656a 100644
--- a/src/theory/theory_proof_step_buffer.h
+++ b/src/theory/theory_proof_step_buffer.h
@@ -73,6 +73,29 @@ class TheoryProofStepBuffer : public ProofStepBuffer
                      MethodId ids = MethodId::SB_DEFAULT,
                      MethodId idr = MethodId::RW_REWRITE);
   //---------------------------- end utilities builtin proof rules
+
+  //---------------------------- utility methods for normalizing clauses
+  /**
+   * Normalizes a non-unit clause (an OR node) according to factoring and
+   * reordering, i.e. removes duplicates and reorders literals (according to
+   * node ids). Moreover it eliminates double negations, which can be done also
+   * for unit clauses (a arbitrary Boolean node). All normalization steps are
+   * tracked via proof steps added to this proof step buffer.
+   *
+   * @param n the clause to be normalized
+   * @return the normalized clause node
+   */
+  Node factorReorderElimDoubleNeg(Node n);
+
+  /**
+   * Eliminates double negation of a literal if it has the form
+   *  (not (not t))
+   * If the elimination happens, a step is added to this proof step buffer.
+   *
+   * @param n the node to have the top-level double negation eliminated
+   * @return the normalized clause node
+   */
+  Node elimDoubleNegLit(Node n);
 };
 
 }  // namespace theory