diff options
| -rw-r--r-- | src/theory/theory_proof_step_buffer.cpp | 114 | ||||
| -rw-r--r-- | src/theory/theory_proof_step_buffer.h | 23 |
2 files changed, 137 insertions, 0 deletions
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 |