diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-12-21 18:16:53 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-21 11:16:53 -0600 |
commit | 0c2a43ab616c3670f3077758defcaa1f61cbe291 (patch) | |
tree | 83cf86aa5cdd2ea0af07a980ebca0cd4af072f83 /src/expr/proof_rule.cpp | |
parent | 708c5a14bca031100b05000ddae65a9828d76da0 (diff) |
Add proof for sine shift lemmas. (#5710)
This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.
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 22459edd4..24cfa0091 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -160,6 +160,7 @@ const char* toString(PfRule id) case PfRule::INT_TRUST: return "INT_TRUST"; case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; + case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; |