diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-06-28 05:51:31 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-28 07:51:31 -0500 |
commit | cb68fa0f7b096bf086a7c7189e40805253ef1acf (patch) | |
tree | 029c0d18cd3e9b0c722c852bb2d88255832e675d /src/expr | |
parent | fa833542f0e96187b3a02c4e15ec33ba45428b62 (diff) |
Proof Rules and Checker for Arithmetic (#4665)
This PR introduces proof rules for arithmetic and their checker.
The code is dead, since these rules are never used.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/proof_rule.cpp | 7 | ||||
-rw-r--r-- | src/expr/proof_rule.h | 64 |
2 files changed, 71 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index f736efed9..d00f1658b 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -90,6 +90,13 @@ const char* toString(PfRule id) case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; case PfRule::SKOLEMIZE: return "SKOLEMIZE"; case PfRule::INSTANTIATE: return "INSTANTIATE"; + //================================================= Arith rules + case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS"; + 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"; + case PfRule::INT_TRUST: return "INT_TRUST"; + case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index d6e5b6f4b..ec589a16e 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -507,6 +507,70 @@ enum class PfRule : uint32_t // sigma maps x1 ... xn to t1 ... tn. INSTANTIATE, + // ======== Adding Inequalities + // Note: an ArithLiteral is a term of the form (>< poly const) + // where + // >< is >=, >, ==, <, <=, or not(== ...). + // poly is a polynomial + // const is a rational constant + + // Children: (P1:l1, ..., Pn:ln) + // where each li is an ArithLiteral + // not(= ...) is dis-allowed! + // + // Arguments: (k1, ..., kn), non-zero reals + // --------------------- + // Conclusion: (>< (* k t1) (* k t2)) + // where >< is the fusion of the combination of the ><i, (flipping each it + // its ki is negative). >< is always one of <, <= + // NB: this implies that lower bounds must have negative ki, + // and upper bounds must have positive ki. + // t1 is the sum of the polynomials. + // t2 is the sum of the constants. + ARITH_SCALE_SUM_UPPER_BOUNDS, + + // ======== Tightening Strict Integer Upper Bounds + // Children: (P:(< i c)) + // where i has integer type. + // Arguments: none + // --------------------- + // Conclusion: (<= i greatestIntLessThan(c)}) + INT_TIGHT_UB, + + // ======== Tightening Strict Integer Lower Bounds + // Children: (P:(> i c)) + // where i has integer type. + // Arguments: none + // --------------------- + // Conclusion: (>= i leastIntGreaterThan(c)}) + INT_TIGHT_LB, + + // ======== Trichotomy of the reals + // Children: (A B) + // Arguments: (C) + // --------------------- + // Conclusion: (C), + // where (not A) (not B) and C + // are (> x c) (< x c) and (= x c) + // in some order + // note that "not" here denotes arithmetic negation, flipping + // >= to <, etc. + ARITH_TRICHOTOMY, + + // ======== Arithmetic operator elimination + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: arith::OperatorElim::getAxiomFor(t) + ARITH_OP_ELIM_AXIOM, + + // ======== Int Trust + // Children: (P1 ... Pn) + // Arguments: (Q) + // --------------------- + // Conclusion: (Q) + INT_TRUST, + //================================================= Unknown rule UNKNOWN, }; |