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/proof_rule.cpp | |
| 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/proof_rule.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 2 |
1 files changed, 2 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 "?"; |