summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_rewriter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r--src/theory/arith/arith_rewriter.cpp109
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback