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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index cc5613057..d29aca6ea 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -159,6 +159,7 @@ 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_SIGN: return "ARITH_MULT_SIGN"; 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"; |