diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2021-05-19 18:16:12 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-20 01:16:12 +0000 |
| commit | 8bb85b0f1664f6d03bcbf3997533140204c29251 (patch) | |
| tree | 4979d8adedcf00d55706b5b6967a7f5bf3cddcaa /src/expr | |
| parent | 12770db5ef8a0a86dd264311955e105a78ae0b29 (diff) | |
Expand arith's farkas lemma rule as a macro (#6577)
reflects that it is a macro, which we will eliminate
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof_rule.cpp | 4 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 3 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index fbeaea729..02323b606 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -196,7 +196,9 @@ const char* toString(PfRule id) case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ"; case PfRule::STRING_TRUST: return "STRING_TRUST"; //================================================= Arith rules - case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS"; + case PfRule::MACRO_ARITH_SCALE_SUM_UB: + return "ARITH_SCALE_SUM_UPPER_BOUNDS"; + case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB"; case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 4730df652..cfab15614 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1124,8 +1124,7 @@ enum class PfRule : uint32_t // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n // * const_n) - ARITH_SCALE_SUM_UPPER_BOUNDS, - + MACRO_ARITH_SCALE_SUM_UB, // ======== Sum Upper Bounds // Children: (P1, ... , Pn) // where each Pi has form (><i, Li, Ri) |