From b4c832ab30dafe048334c6e47642aa12619357ef Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 23 Feb 2021 17:51:53 +0100 Subject: [PATCH] Add proof for monomial bounds check (#5965) This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors. --- src/expr/proof_rule.cpp | 2 + src/expr/proof_rule.h | 16 ++++++++ .../arith/nl/ext/monomial_bounds_check.cpp | 15 +++++-- src/theory/arith/nl/ext/proof_checker.cpp | 41 ++++++++++++++++++- 4 files changed, 70 insertions(+), 4 deletions(-) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index bead7397a..cc5613057 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -159,6 +159,8 @@ const char* toString(PfRule id) case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; case PfRule::INT_TRUST: return "INT_TRUST"; + case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS"; + case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG"; case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index d42175fab..bf6f1d6ae 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1092,6 +1092,22 @@ enum class PfRule : uint32_t // Conclusion: (Q) INT_TRUST, + //======== Multiplication with positive factor + // Children: none + // Arguments: (m, orig, lhs, rel, rhs) + // --------------------- + // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs))) + // Where orig is the origin that implies (rel lhs rhs) and rel is a relation + // symbol. + ARITH_MULT_POS, + //======== Multiplication with negative factor + // Children: none + // Arguments: (m, orig, (rel lhs rhs)) + // --------------------- + // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs))) + // Where orig is the origin that implies (rel lhs rhs) and rel is a relation + // symbol and rel_inv the inverted relation symbol. + ARITH_MULT_NEG, //======== Multiplication tangent plane // Children: none // Arguments: (t, x, y, a, b, sgn) diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 46b1c991e..5ae898bd2 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -317,11 +317,20 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, Trace("nl-ext-bound-lemma") << "*** Bound inference lemma : " << iblem << " (pre-rewrite : " << pr_iblem << ")" << std::endl; - // Trace("nl-ext-bound-lemma") << " intro new - // monomials = " << introNewTerms << std::endl; + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep( + iblem, + mmv_sign == 1 ? PfRule::ARITH_MULT_POS + : PfRule::ARITH_MULT_NEG, + {}, + {mult, d_ci_exp[x][coeff][rhs], nm->mkNode(type, t, rhs)}); + } d_data->d_im.addPendingLemma(iblem, InferenceId::ARITH_NL_INFER_BOUNDS_NT, - nullptr, + proof, introNewTerms); } } diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index 8c594f1df..a0c5d2021 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -27,6 +27,8 @@ namespace nl { void ExtProofRuleChecker::registerTo(ProofChecker* pc) { + pc->registerChecker(PfRule::ARITH_MULT_POS, this); + pc->registerChecker(PfRule::ARITH_MULT_NEG, this); pc->registerChecker(PfRule::ARITH_MULT_TANGENT, this); } @@ -45,7 +47,44 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, { Trace("nl-ext-checker") << "\t" << c << std::endl; } - if (id == PfRule::ARITH_MULT_TANGENT) + if (id == PfRule::ARITH_MULT_POS) + { + Assert(children.empty()); + Assert(args.size() == 3); + Node mult = args[0]; + Node orig = args[1]; + Kind rel = args[2].getKind(); + Assert(rel == Kind::EQUAL || rel == Kind::DISTINCT || rel == Kind::LT + || rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ); + Node lhs = args[2][0]; + Node rhs = args[2][1]; + return Rewriter::rewrite(nm->mkNode( + Kind::IMPLIES, + nm->mkAnd(std::vector{nm->mkNode(Kind::GT, mult, zero), orig}), + nm->mkNode(rel, + nm->mkNode(Kind::MULT, mult, lhs), + nm->mkNode(Kind::MULT, mult, rhs)))); + } + else if (id == PfRule::ARITH_MULT_NEG) + { + Assert(children.empty()); + Assert(args.size() == 3); + Node mult = args[0]; + Node orig = args[1]; + Kind rel = args[2].getKind(); + Assert(rel == Kind::EQUAL || rel == Kind::DISTINCT || rel == Kind::LT + || rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ); + Kind rel_inv = (rel == Kind::DISTINCT ? rel : reverseRelationKind(rel)); + Node lhs = args[2][0]; + Node rhs = args[2][1]; + return Rewriter::rewrite(nm->mkNode( + Kind::IMPLIES, + nm->mkAnd(std::vector{nm->mkNode(Kind::LT, mult, zero), orig}), + nm->mkNode(rel_inv, + nm->mkNode(Kind::MULT, mult, lhs), + nm->mkNode(Kind::MULT, mult, rhs)))); + } + else if (id == PfRule::ARITH_MULT_TANGENT) { Assert(children.empty()); Assert(args.size() == 6); -- 2.30.2