diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-10 21:48:13 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-10 20:48:13 +0000 |
| commit | bd52deb7434b1b08a122db4513972644c11fc4aa (patch) | |
| tree | 44cd11cde22fe7f20a281c8d9092de219547c6fb /src/expr | |
| parent | 27fb04bc96999e101b45458c549345e864e085e9 (diff) | |
Improve arithmetic proofs (#6106)
The proof rules for ARITH_MULT_POS and ARITH_MULT_NEG were complex than necessary in that they incorporated a rewriting step. This PR removes rewriting from these rules, making them cleaner and easier to understand.
The proof now applies these simpler rule and uses MACRO_SR_PRED_TRANSFORM to prove the lemma that is actually added.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof_rule.h | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 909f7b7cd..2759a3c9e 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1108,19 +1108,17 @@ enum class PfRule : uint32_t ARITH_MULT_SIGN, //======== Multiplication with positive factor // Children: none - // Arguments: (m, orig, lhs, rel, rhs) + // Arguments: (m, (rel lhs 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. + // Where rel is a relation symbol. ARITH_MULT_POS, //======== Multiplication with negative factor // Children: none - // Arguments: (m, orig, (rel lhs rhs)) + // Arguments: (m, (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. + // Where rel is a relation symbol and rel_inv the inverted relation symbol. ARITH_MULT_NEG, //======== Multiplication tangent plane // Children: none |