diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-23 19:31:28 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-23 12:31:28 -0600 |
| commit | f956c6b5cf9a4d836ebcd99ef57558b9b11f4d29 (patch) | |
| tree | e2fdba4a57678e56b90beab4913f5db129ee0a76 /src/expr/proof_rule.h | |
| parent | 1e58294a927f8c3067ea0feaad0d891f82f42ebe (diff) | |
Add proof for mult sign lemma (#5966)
This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.
Diffstat (limited to 'src/expr/proof_rule.h')
| -rw-r--r-- | src/expr/proof_rule.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index bf6f1d6ae..76c2d0958 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1092,6 +1092,18 @@ enum class PfRule : uint32_t // Conclusion: (Q) INT_TRUST, + //======== Multiplication sign inference + // Children: none + // Arguments: (f1, ..., fk, m) + // --------------------- + // Conclusion: (=> (and f1 ... fk) (~ m 0)) + // Where f1, ..., fk are variables compared to zero (less, greater or not + // equal), m is a monomial from these variables, and ~ is the comparison (less + // or greater) that results from the signs of the variables. All variables + // with even exponent in m should be given as not equal to zero while all + // variables with odd exponent in m should be given as less or greater than + // zero. + ARITH_MULT_SIGN, //======== Multiplication with positive factor // Children: none // Arguments: (m, orig, lhs, rel, rhs) |