diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-07 09:12:59 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-07 09:12:59 -0600 |
commit | 0533b9009d23a39bcc78ef85d6e98b62ef304351 (patch) | |
tree | e32b823d509e1c9b54dfe4230d075b8396f48b9c /src/theory/arith/arith_rewriter.cpp | |
parent | 82066be04ce068b59b24526fbc8c9b4188503cae (diff) |
Add remaining transcendental functions (#1551)
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 109 |
1 files changed, 80 insertions, 29 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index b862e7604..a9761ade4 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -107,7 +107,15 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::SINE: case kind::COSINE: case kind::TANGENT: - return preRewriteTranscendental(t); + case kind::COSECANT: + case kind::SECANT: + case kind::COTANGENT: + case kind::ARCSINE: + case kind::ARCCOSINE: + case kind::ARCTANGENT: + case kind::ARCCOSECANT: + case kind::ARCSECANT: + case kind::ARCCOTANGENT: return preRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); @@ -163,7 +171,15 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::SINE: case kind::COSINE: case kind::TANGENT: - return postRewriteTranscendental(t); + case kind::COSECANT: + case kind::SECANT: + case kind::COTANGENT: + case kind::ARCSINE: + case kind::ARCCOSINE: + case kind::ARCTANGENT: + case kind::ARCCOSECANT: + case kind::ARCSECANT: + case kind::ARCCOTANGENT: return postRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); @@ -360,28 +376,30 @@ RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t) { RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { Trace("arith-tf-rewrite") << "Rewrite transcendental function : " << t << std::endl; + NodeManager* nm = NodeManager::currentNM(); switch( t.getKind() ){ case kind::EXPONENTIAL: { if(t[0].getKind() == kind::CONST_RATIONAL){ - Node one = NodeManager::currentNM()->mkConst(Rational(1)); + Node one = nm->mkConst(Rational(1)); if(t[0].getConst<Rational>().sgn()>=0 && t[0].getType().isInteger() && t[0]!=one){ - return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::POW, NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, one ), t[0])); + return RewriteResponse( + REWRITE_AGAIN, + nm->mkNode(kind::POW, nm->mkNode(kind::EXPONENTIAL, one), t[0])); }else{ return RewriteResponse(REWRITE_DONE, t); } }else if(t[0].getKind() == kind::PLUS ){ std::vector<Node> product; for( unsigned i=0; i<t[0].getNumChildren(); i++ ){ - product.push_back( NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, t[0][i] ) ); + product.push_back(nm->mkNode(kind::EXPONENTIAL, t[0][i])); } - return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::MULT, product)); + return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::MULT, product)); } } break; 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, nm->mkConst(Rational(0))); } @@ -433,26 +451,29 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { if (r_abs > rone) { //add/substract 2*pi beyond scope - Node ra_div_two = NodeManager::currentNM()->mkNode( + Node ra_div_two = nm->mkNode( kind::INTS_DIVISION, mkRationalNode(r_abs + rone), ntwo); Node new_pi_factor; if( r.sgn()==1 ){ - new_pi_factor = NodeManager::currentNM()->mkNode( kind::MINUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) ); + new_pi_factor = + nm->mkNode(kind::MINUS, + pi_factor, + nm->mkNode(kind::MULT, ntwo, ra_div_two)); }else{ Assert( r.sgn()==-1 ); - new_pi_factor = NodeManager::currentNM()->mkNode( kind::PLUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) ); + new_pi_factor = + nm->mkNode(kind::PLUS, + pi_factor, + nm->mkNode(kind::MULT, ntwo, ra_div_two)); } - Node new_arg = - NodeManager::currentNM()->mkNode(kind::MULT, new_pi_factor, pi); + Node new_arg = nm->mkNode(kind::MULT, new_pi_factor, pi); if (!rem.isNull()) { - new_arg = - NodeManager::currentNM()->mkNode(kind::PLUS, new_arg, rem); + new_arg = nm->mkNode(kind::PLUS, new_arg, rem); } // sin( 2*n*PI + x ) = sin( x ) - return RewriteResponse( - REWRITE_AGAIN_FULL, - NodeManager::currentNM()->mkNode(kind::SINE, new_arg)); + return RewriteResponse(REWRITE_AGAIN_FULL, + nm->mkNode(kind::SINE, new_arg)); } else if (r_abs == rone) { @@ -465,9 +486,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { { return RewriteResponse( REWRITE_AGAIN_FULL, - NodeManager::currentNM()->mkNode( - kind::UMINUS, - NodeManager::currentNM()->mkNode(kind::SINE, rem))); + nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, rem))); } } else if (rem.isNull()) @@ -498,16 +517,48 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { } break; case kind::COSINE: { - return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode( kind::SINE, - NodeManager::currentNM()->mkNode( kind::MINUS, - NodeManager::currentNM()->mkNode( kind::MULT, - NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ), - NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI ) ), - t[0] ) ) ); - } break; + return RewriteResponse( + REWRITE_AGAIN_FULL, + nm->mkNode(kind::SINE, + nm->mkNode(kind::MINUS, + nm->mkNode(kind::MULT, + nm->mkConst(Rational(1) / Rational(2)), + mkPi()), + t[0]))); + } + break; case kind::TANGENT: - return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode(kind::DIVISION, NodeManager::currentNM()->mkNode( kind::SINE, t[0] ), - NodeManager::currentNM()->mkNode( kind::COSINE, t[0] ) )); + { + return RewriteResponse(REWRITE_AGAIN_FULL, + nm->mkNode(kind::DIVISION, + nm->mkNode(kind::SINE, t[0]), + nm->mkNode(kind::COSINE, t[0]))); + } + break; + case kind::COSECANT: + { + return RewriteResponse(REWRITE_AGAIN_FULL, + nm->mkNode(kind::DIVISION, + mkRationalNode(Rational(1)), + nm->mkNode(kind::SINE, t[0]))); + } + break; + case kind::SECANT: + { + return RewriteResponse(REWRITE_AGAIN_FULL, + nm->mkNode(kind::DIVISION, + mkRationalNode(Rational(1)), + nm->mkNode(kind::COSINE, t[0]))); + } + break; + case kind::COTANGENT: + { + return RewriteResponse(REWRITE_AGAIN_FULL, + nm->mkNode(kind::DIVISION, + nm->mkNode(kind::COSINE, t[0]), + nm->mkNode(kind::SINE, t[0]))); + } + break; default: break; } |