From: Alex Ozdemir Date: Wed, 14 Oct 2020 04:15:25 +0000 (-0700) Subject: (proof-new) Prove lemmas in Constraint (#5254) X-Git-Tag: cvc5-1.0.0~2715 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9be90e37556d0654d7b7565ba6a62ba46eb44ccd;p=cvc5.git (proof-new) Prove lemmas in Constraint (#5254) Includes: T/F splitting lemmas for any arith constraint Unate lemmas produced early on The hard part is proving the unate lemmas. In general, they are all implied by 2-constraint farkas proofs, so we ultimately map them all down to proveOr, which constructs that proof. make check was happy with this change. Hopefully the CI agrees :). --- diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index a08122295..b0be108f7 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -1062,7 +1062,8 @@ bool Constraint::contextDependentDataIsSet() const{ return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory(); } -Node Constraint::split(){ +TrustNode Constraint::split() +{ Assert(isEquality() || isDisequality()); bool isEq = isEquality(); @@ -1076,15 +1077,48 @@ Node Constraint::split(){ TNode rhs = eqNode[1]; Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs; + Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; + Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs; Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode; + TrustNode trustedLemma; + if (options::proofNew()) + { + // Farkas proof that this works. + auto nm = NodeManager::currentNM(); + auto nLeqPf = d_database->d_pnm->mkAssume(leqNode.negate()); + auto gtPf = d_database->d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {nLeqPf}, {gtNode}); + auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate()); + auto ltPf = d_database->d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {nGeqPf}, {ltNode}); + auto sumPf = d_database->d_pnm->mkNode( + PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, + {gtPf, ltPf}, + {nm->mkConst(-1), nm->mkConst(1)}); + auto botPf = d_database->d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)}); + std::vector a = {leqNode.negate(), geqNode.negate()}; + auto notAndNotPf = d_database->d_pnm->mkScope(botPf, a); + // No need to ensure that the expected node aggrees with `a` because we are + // not providing an expected node. + auto orNotNotPf = + d_database->d_pnm->mkNode(PfRule::NOT_AND, {notAndNotPf}, {}); + auto orPf = d_database->d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {orNotNotPf}, {lemma}); + trustedLemma = d_database->d_pfGen->mkTrustNode(lemma, orPf); + } + else + { + trustedLemma = TrustNode::mkTrustLemma(lemma); + } eq->d_database->pushSplitWatch(eq); diseq->d_database->pushSplitWatch(diseq); - return lemma; + return trustedLemma; } bool ConstraintDatabase::hasLiteral(TNode literal) const { @@ -2026,30 +2060,83 @@ Node Constraint::getProofLiteral() const return neg ? posLit.negate() : posLit; } -void implies(std::vector& out, ConstraintP a, ConstraintP b){ +void ConstraintDatabase::proveOr(std::vector& out, + ConstraintP a, + ConstraintP b, + bool negateSecond) const +{ + Node la = a->getLiteral(); + Node lb = b->getLiteral(); + Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la); + if (options::proofNew()) + { + Assert(b->getNegation()->getType() != ConstraintType::Disequality); + auto nm = NodeManager::currentNM(); + auto pf_neg_la = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {d_pnm->mkAssume(la.negate())}, + {a->getNegation()->getProofLiteral()}); + auto pf_neg_lb = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {d_pnm->mkAssume(lb.negate())}, + {b->getNegation()->getProofLiteral()}); + int sndSign = negateSecond ? -1 : 1; + auto bot_pf = + d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {d_pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, + {pf_neg_la, pf_neg_lb}, + {nm->mkConst(-1 * sndSign), + nm->mkConst(sndSign)})}, + {nm->mkConst(false)}); + std::vector as; + std::transform(orN.begin(), orN.end(), std::back_inserter(as), [](Node n) { + return n.negate(); + }); + // No need to ensure that the expected node aggrees with `as` because we + // are not providing an expected node. + auto pf = d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, + {d_pnm->mkNode(PfRule::NOT_AND, {d_pnm->mkScope(bot_pf, as)}, {})}, + {orN}); + out.push_back(d_pfGen->mkTrustNode(orN, pf)); + } + else + { + out.push_back(TrustNode::mkTrustLemma(orN)); + } +} + +void ConstraintDatabase::implies(std::vector& out, + ConstraintP a, + ConstraintP b) const +{ Node la = a->getLiteral(); Node lb = b->getLiteral(); Node neg_la = (la.getKind() == kind::NOT)? la[0] : la.notNode(); Assert(lb != neg_la); - Node orderOr = (lb < neg_la) ? lb.orNode(neg_la) : neg_la.orNode(lb); - out.push_back(orderOr); + Assert(b->getNegation()->getType() == ConstraintType::LowerBound + || b->getNegation()->getType() == ConstraintType::UpperBound); + proveOr(out, + a->getNegation(), + b, + b->getNegation()->getType() == ConstraintType::LowerBound); } -void mutuallyExclusive(std::vector& out, ConstraintP a, ConstraintP b){ +void ConstraintDatabase::mutuallyExclusive(std::vector& out, + ConstraintP a, + ConstraintP b) const +{ Node la = a->getLiteral(); Node lb = b->getLiteral(); - Node neg_la = (la.getKind() == kind::NOT)? la[0] : la.notNode(); - Node neg_lb = (lb.getKind() == kind::NOT)? lb[0] : lb.notNode(); - - Assert(neg_la != neg_lb); - Node orderOr = (neg_la < neg_lb) ? neg_la.orNode(neg_lb) : neg_lb.orNode(neg_la); - out.push_back(orderOr); + Node neg_la = la.negate(); + Node neg_lb = lb.negate(); + proveOr(out, a->getNegation(), b->getNegation(), true); } -void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& out, ArithVar v) const{ +void ConstraintDatabase::outputUnateInequalityLemmas( + std::vector& out, ArithVar v) const +{ SortedConstraintMap& scm = getVariableSCM(v); SortedConstraintMapConstIterator scm_iter = scm.begin(); SortedConstraintMapConstIterator scm_end = scm.end(); @@ -2070,8 +2157,9 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& out, Ari } } -void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& out, ArithVar v) const{ - +void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& out, + ArithVar v) const +{ vector equalities; SortedConstraintMap& scm = getVariableSCM(v); @@ -2123,13 +2211,17 @@ void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& out, Arith } } -void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& lemmas) const{ +void ConstraintDatabase::outputUnateEqualityLemmas( + std::vector& lemmas) const +{ for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ outputUnateEqualityLemmas(lemmas, v); } } -void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& lemmas) const{ +void ConstraintDatabase::outputUnateInequalityLemmas( + std::vector& lemmas) const +{ for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ outputUnateInequalityLemmas(lemmas, v); } diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 02bc3c988..952879182 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -411,7 +411,7 @@ class Constraint { * Returns a lemma that is assumed to be true for the rest of the user context. * Constraint must be an equality or disequality. */ - Node split(); + TrustNode split(); bool canBePropagated() const { return d_canBePropagated; @@ -1191,14 +1191,39 @@ private: void deleteConstraintAndNegation(ConstraintP c); + /** Given constraints `a` and `b` such that `a OR b` by unate reasoning, + * adds a TrustNode to `out` which proves `a OR b` as a lemma. + * + * Example: `x <= 5` OR `5 <= x`. + */ + void proveOr(std::vector& out, + ConstraintP a, + ConstraintP b, + bool negateSecond) const; + /** Given constraints `a` and `b` such that `a` implies `b` by unate + * reasoning, adds a TrustNode to `out` which proves `-a OR b` as a lemma. + * + * Example: `x >= 5` -> `x >= 4`. + */ + void implies(std::vector& out, ConstraintP a, ConstraintP b) const; + /** Given constraints `a` and `b` such that `not(a AND b)` by unate reasoning, + * adds a TrustNode to `out` which proves `-a OR -b` as a lemma. + * + * Example: `x >= 4` -> `x <= 3`. + */ + void mutuallyExclusive(std::vector& out, + ConstraintP a, + ConstraintP b) const; + /** * Outputs a minimal set of unate implications onto the vector for the variable. * This outputs lemmas of the general forms * (= p c) implies (<= p d) for c < d, or * (= p c) implies (not (= p d)) for c != d. */ - void outputUnateEqualityLemmas(std::vector& lemmas) const; - void outputUnateEqualityLemmas(std::vector& lemmas, ArithVar v) const; + void outputUnateEqualityLemmas(std::vector& lemmas) const; + void outputUnateEqualityLemmas(std::vector& lemmas, + ArithVar v) const; /** * Outputs a minimal set of unate implications onto the vector for the variable. @@ -1206,9 +1231,9 @@ private: * If ineqs is true, this outputs lemmas of the general form * (<= p c) implies (<= p d) for c < d. */ - void outputUnateInequalityLemmas(std::vector& lemmas) const; - void outputUnateInequalityLemmas(std::vector& lemmas, ArithVar v) const; - + void outputUnateInequalityLemmas(std::vector& lemmas) const; + void outputUnateInequalityLemmas(std::vector& lemmas, + ArithVar v) const; void unatePropLowerBound(ConstraintP curr, ConstraintP prev); void unatePropUpperBound(ConstraintP curr, ConstraintP prev); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 3abd9495e..119be6307 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1063,7 +1063,7 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){ if(!split && c_i == d_partialModel.getAssignment(x_i)){ Debug("arith::eq") << "lemma now! " << constraint << endl; - outputLemma(constraint->split()); + outputTrustedLemma(constraint->split()); return false; }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ Debug("arith::eq") << "can drop as less than lb" << constraint << endl; @@ -1918,6 +1918,12 @@ void TheoryArithPrivate::outputConflicts(){ } } +void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma) +{ + Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl; + (d_containing.d_out)->lemma(lemma.getNode()); +} + void TheoryArithPrivate::outputLemma(TNode lem) { Debug("arith::channel") << "Arith lemma: " << lem << std::endl; (d_containing.d_out)->lemma(lem); @@ -3728,11 +3734,12 @@ bool TheoryArithPrivate::splitDisequalities(){ Debug("arith::lemma") << "Splitting on " << front << endl; Debug("arith::lemma") << "LHS value = " << lhsValue << endl; Debug("arith::lemma") << "RHS value = " << rhsValue << endl; - Node lemma = front->split(); + TrustNode lemma = front->split(); ++(d_statistics.d_statDisequalitySplits); - Debug("arith::lemma") << "Now " << Rewriter::rewrite(lemma) << endl; - outputLemma(lemma); + Debug("arith::lemma") + << "Now " << Rewriter::rewrite(lemma.getNode()) << endl; + outputTrustedLemma(lemma); //cout << "Now " << Rewriter::rewrite(lemma) << endl; splitSomething = true; }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){ @@ -4158,7 +4165,7 @@ void TheoryArithPrivate::presolve(){ callCount = callCount + 1; } - vector lemmas; + vector lemmas; if(!options::incrementalSolving()) { switch(options::arithUnateLemmaMode()){ case options::ArithUnateLemmaMode::NO: break; @@ -4176,11 +4183,11 @@ void TheoryArithPrivate::presolve(){ } } - vector::const_iterator i = lemmas.begin(), i_end = lemmas.end(); + vector::const_iterator i = lemmas.begin(), i_end = lemmas.end(); for(; i != i_end; ++i){ - Node lem = *i; + TrustNode lem = *i; Debug("arith::oldprop") << " lemma lemma duck " <