diff options
Diffstat (limited to 'src/theory/arith/constraint.cpp')
| -rw-r--r-- | src/theory/arith/constraint.cpp | 126 |
1 files changed, 109 insertions, 17 deletions
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<Rational>(-1), nm->mkConst<Rational>(1)}); + auto botPf = d_database->d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)}); + std::vector<Node> 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<Node>& out, ConstraintP a, ConstraintP b){ +void ConstraintDatabase::proveOr(std::vector<TrustNode>& 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<Rational>(-1 * sndSign), + nm->mkConst<Rational>(sndSign)})}, + {nm->mkConst(false)}); + std::vector<Node> 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<TrustNode>& 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<Node>& out, ConstraintP a, ConstraintP b){ +void ConstraintDatabase::mutuallyExclusive(std::vector<TrustNode>& 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<Node>& out, ArithVar v) const{ +void ConstraintDatabase::outputUnateInequalityLemmas( + std::vector<TrustNode>& 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<Node>& out, Ari } } -void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& out, ArithVar v) const{ - +void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<TrustNode>& out, + ArithVar v) const +{ vector<ConstraintP> equalities; SortedConstraintMap& scm = getVariableSCM(v); @@ -2123,13 +2211,17 @@ void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& out, Arith } } -void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& lemmas) const{ +void ConstraintDatabase::outputUnateEqualityLemmas( + std::vector<TrustNode>& lemmas) const +{ for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ outputUnateEqualityLemmas(lemmas, v); } } -void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas) const{ +void ConstraintDatabase::outputUnateInequalityLemmas( + std::vector<TrustNode>& lemmas) const +{ for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ outputUnateInequalityLemmas(lemmas, v); } |