diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-20 12:36:10 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-20 12:36:10 -0600 |
| commit | c710665ee3f1bd28f0329d6f8428fcbeedd5d372 (patch) | |
| tree | a6d85eeeb8cb6663bb163716f4bc6052a743f5e3 /src/theory/arith/arith_rewriter.cpp | |
| parent | 018ff661d60cfc4801a2178fdb4f91181a8a69ee (diff) | |
Transcendental functions check model (#1443)
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 72f9cdf4a..b47cb1e60 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -381,8 +381,15 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { case kind::SINE: if(t[0].getKind() == kind::CONST_RATIONAL){ const Rational& rat = t[0].getConst<Rational>(); + NodeManager* nm = NodeManager::currentNM(); if(rat.sgn() == 0){ - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(0))); + return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(0))); + } + else if (rat.sgn() == -1) + { + Node ret = + nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, nm->mkConst(-rat))); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); } }else{ // get the factor of PI in the argument |