From 8bb85b0f1664f6d03bcbf3997533140204c29251 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 19 May 2021 18:16:12 -0700 Subject: [PATCH] Expand arith's farkas lemma rule as a macro (#6577) reflects that it is a macro, which we will eliminate --- src/expr/proof_rule.cpp | 4 +- src/expr/proof_rule.h | 3 +- src/smt/proof_post_processor.cpp | 52 +++++++++++++++++++++++ src/theory/arith/congruence_manager.cpp | 2 +- src/theory/arith/constraint.cpp | 10 ++--- src/theory/arith/proof_checker.cpp | 23 +++++++--- src/theory/arith/theory_arith_private.cpp | 7 ++- 7 files changed, 80 insertions(+), 21 deletions(-) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index fbeaea729..02323b606 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -196,7 +196,9 @@ const char* toString(PfRule id) case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ"; case PfRule::STRING_TRUST: return "STRING_TRUST"; //================================================= Arith rules - case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS"; + case PfRule::MACRO_ARITH_SCALE_SUM_UB: + return "ARITH_SCALE_SUM_UPPER_BOUNDS"; + case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB"; case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 4730df652..cfab15614 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1124,8 +1124,7 @@ enum class PfRule : uint32_t // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n // * const_n) - ARITH_SCALE_SUM_UPPER_BOUNDS, - + MACRO_ARITH_SCALE_SUM_UB, // ======== Sum Upper Bounds // Children: (P1, ... , Pn) // where each Pi has form (>getChecker()}; + + // Scale all children, accumulating + std::vector scaledRels; + for (size_t i = 0; i < children.size(); ++i) + { + TNode child = children[i]; + TNode scalar = args[i]; + bool isPos = scalar.getConst() > 0; + Node scalarCmp = + nm->mkNode(isPos ? GT : LT, scalar, nm->mkConst(Rational(0))); + // (= scalarCmp true) + Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp}); + Assert(!scalarCmpOrTrue.isNull()); + // scalarCmp + steps.addStep(PfRule::TRUE_ELIM, {scalarCmpOrTrue}, {}, scalarCmp); + // (and scalarCmp relation) + Node scalarCmpAndRel = + steps.tryStep(PfRule::AND_INTRO, {scalarCmp, child}, {}); + Assert(!scalarCmpAndRel.isNull()); + // (=> (and scalarCmp relation) scaled) + Node impl = + steps.tryStep(isPos ? PfRule::ARITH_MULT_POS : PfRule::ARITH_MULT_NEG, + {}, + {scalar, child}); + Assert(!impl.isNull()); + // scaled + Node scaled = + steps.tryStep(PfRule::MODUS_PONENS, {scalarCmpAndRel, impl}, {}); + Assert(!scaled.isNull()); + scaledRels.emplace_back(scaled); + } + + Node sumBounds = steps.tryStep(PfRule::ARITH_SUM_UB, scaledRels, {}); + cdp->addSteps(steps); + Debug("macro::arith") << "Expansion done. Proved: " << sumBounds + << std::endl; + return sumBounds; + } // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS? diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 23bdb20f6..3d5e7270b 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -311,7 +311,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){ const auto isZeroPf = d_pnm->mkAssume(isZero); const auto nm = NodeManager::currentNM(); const auto sumPf = d_pnm->mkNode( - PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, + PfRule::MACRO_ARITH_SCALE_SUM_UB, {isZeroPf, pf}, // Trick for getting correct, opposing signs. {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))}); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index fc2506f84..15dfe4791 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -1092,7 +1092,7 @@ TrustNode Constraint::split() 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, + PfRule::MACRO_ARITH_SCALE_SUM_UB, {gtPf, ltPf}, {nm->mkConst(-1), nm->mkConst(1)}); auto botPf = d_database->d_pnm->mkNode( @@ -1779,10 +1779,8 @@ std::shared_ptr Constraint::externalExplain( } // Apply the scaled-sum rule. - std::shared_ptr sumPf = - pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, - farkasChildren, - farkasCoeffs); + std::shared_ptr sumPf = pnm->mkNode( + PfRule::MACRO_ARITH_SCALE_SUM_UB, farkasChildren, farkasCoeffs); // Provable rewrite the result auto botPf = pnm->mkNode( @@ -2081,7 +2079,7 @@ void ConstraintDatabase::proveOr(std::vector& out, 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, + {d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB, {pf_neg_la, pf_neg_lb}, {nm->mkConst(-1 * sndSign), nm->mkConst(sndSign)})}, diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 535d6b090..4e25ae76b 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -30,7 +30,7 @@ namespace arith { void ArithProofRuleChecker::registerTo(ProofChecker* pc) { - pc->registerChecker(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, this); + pc->registerChecker(PfRule::MACRO_ARITH_SCALE_SUM_UB, this); pc->registerChecker(PfRule::ARITH_SUM_UB, this); pc->registerChecker(PfRule::ARITH_TRICHOTOMY, this); pc->registerChecker(PfRule::INT_TIGHT_UB, this); @@ -141,21 +141,30 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, rightSum.constructNode()); return r; } - case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: + case PfRule::MACRO_ARITH_SCALE_SUM_UB: { + //================================================= Arithmetic rules + // ======== Adding Inequalities + // Note: an ArithLiteral is a term of the form (>< poly const) + // where + // >< is >=, >, ==, <, <=, or not(== ...). + // poly is a polynomial + // const is a rational constant + // Children: (P1:l1, ..., Pn:ln) // where each li is an ArithLiteral // not(= ...) is dis-allowed! // // Arguments: (k1, ..., kn), non-zero reals // --------------------- - // Conclusion: (>< (* k t1) (* k t2)) + // Conclusion: (>< t1 t2) // where >< is the fusion of the combination of the >< is always one of <, <= NB: this implies // that lower bounds must have negative ki, // and upper bounds must have positive ki. - // t1 is the sum of the polynomials. - // t2 is the sum of the constants. + // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * + // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + + // k_n * const_n) Assert(children.size() == args.size()); if (children.size() < 2) { @@ -234,9 +243,9 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, } } leftSum << nm->mkNode( - Kind::MULT, children[i][0], nm->mkConst(scalar)); + Kind::MULT, nm->mkConst(scalar), children[i][0]); rightSum << nm->mkNode( - Kind::MULT, children[i][1], nm->mkConst(scalar)); + Kind::MULT, nm->mkConst(scalar), children[i][1]); } Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ, leftSum.constructNode(), diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index a4a5ad229..911954a5a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1460,7 +1460,7 @@ TrustNode TheoryArithPrivate::dioCutting() Pf pfLt = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pfNotGeq}, {lt}); Pf pfSum = - d_pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, + d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB, {pfGt, pfLt}, {nm->mkConst(-1), nm->mkConst(1)}); Pf pfBot = d_pnm->mkNode( @@ -4547,9 +4547,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C [nm](const Rational& r) { return nm->mkConst(r); }); // Prove bottom. - auto sumPf = d_pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, - conflictPfs, - farkasCoefficients); + auto sumPf = d_pnm->mkNode( + PfRule::MACRO_ARITH_SCALE_SUM_UB, conflictPfs, farkasCoefficients); auto botPf = d_pnm->mkNode( PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)}); -- 2.30.2