diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-20 12:53:12 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-20 10:53:12 -0800 |
commit | 05a2414a2742ee0c7e5af40ac9c725cb49d1f196 (patch) | |
tree | 8392f1b56aedc1a9ea107790cf7741af64b6607f /src/theory/arith/arith_rewriter.cpp | |
parent | 4ef569cfd91bccabb6e704dcc4ecd55a9fa0a8ea (diff) |
Minor fixes and additions for transcendental functions (#1612)
Also adds parsing support for PI in smt2 with syntax "real.pi".
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a9761ade4..355aa7b0f 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -115,7 +115,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::ARCTANGENT: case kind::ARCCOSECANT: case kind::ARCSECANT: - case kind::ARCCOTANGENT: return preRewriteTranscendental(t); + case kind::ARCCOTANGENT: + case kind::SQRT: return preRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); @@ -179,7 +180,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::ARCTANGENT: case kind::ARCCOSECANT: case kind::ARCSECANT: - case kind::ARCCOTANGENT: return postRewriteTranscendental(t); + case kind::ARCCOTANGENT: + case kind::SQRT: return postRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); |