diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-23 17:17:45 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-23 17:17:45 +0100 |
commit | 7a695fd7c29af97dbcc363eb277ffeae1617cffe (patch) | |
tree | ae3ae02313dadfb126b9c76ded8aadc3e743120f /src/expr | |
parent | c2311f97441befbf10e80ab597455b3ab8ccc10c (diff) |
(proof-new) Add proof generator for CAD solver (#5964)
This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/proof_rule.cpp | 2 | ||||
-rw-r--r-- | src/expr/proof_rule.h | 35 |
2 files changed, 37 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 85463d2d9..bead7397a 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -188,6 +188,8 @@ const char* toString(PfRule id) return "ARITH_TRANS_SINE_APPROX_BELOW_NEG"; case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS: return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; + case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; + case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 917db4088..d42175fab 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1277,6 +1277,41 @@ enum class PfRule : uint32_t // secant of p from l to u. ARITH_TRANS_SINE_APPROX_BELOW_POS, + // ================ CAD Lemmas + // We use IRP for IndexedRootPredicate. + // + // A formula "Interval" describes that a variable (xn is none is given) is + // within a particular interval whose bounds are given as IRPs. It is either + // an open interval or a point interval: + // (IRP k poly) < xn < (IRP k poly) + // xn == (IRP k poly) + // + // A formula "Cell" describes a portion + // of the real space in the following form: + // Interval(x1) and Interval(x2) and ... + // We implicitly assume a Cell to go up to n-1 (and can be empty). + // + // A formula "Covering" is a set of Intervals, implying that xn can be in + // neither of these intervals. To be a covering (of the real line), the union + // of these intervals should be the real numbers. + // ======== CAD direct conflict + // Children (Cell, A) + // --------------------- + // Conclusion: (false) + // A direct interval is generated from an assumption A (in variables x1...xn) + // over a Cell (in variables x1...xn). It derives that A evaluates to false + // over the Cell. In the actual algorithm, it means that xn can not be in the + // topmost interval of the Cell. + ARITH_NL_CAD_DIRECT, + // ======== CAD recursive interval + // Children (Cell, Covering) + // --------------------- + // Conclusion: (false) + // A recursive interval is generated from a Covering (for xn) over a Cell + // (in variables x1...xn-1). It generates the conclusion that no xn exists + // that extends the Cell and satisfies all assumptions. + ARITH_NL_CAD_RECURSIVE, + //================================================= Unknown rule UNKNOWN, }; |