diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-23 17:51:53 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-23 17:51:53 +0100 |
| commit | b4c832ab30dafe048334c6e47642aa12619357ef (patch) | |
| tree | b37829eb546c49fd2921a3bd841db12e6f066408 /src/expr | |
| parent | 7a695fd7c29af97dbcc363eb277ffeae1617cffe (diff) | |
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.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof_rule.cpp | 2 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 16 |
2 files changed, 18 insertions, 0 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) |