diff options
author | Tim King <taking@cs.nyu.edu> | 2014-03-05 12:04:03 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-03-05 12:12:36 -0500 |
commit | df554608cc47684be08d8be7c427027b7c5e8eb2 (patch) | |
tree | b884d51b8a6ebe8841af04b09132430908e204f8 /src/theory/arith | |
parent | 7062bbe7ed2ad5d0b0a94badd624808d7dc91bb2 (diff) |
Improving support for POW in arithmetic. Resolves bug 549.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index f72537965..e1cab0356 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -121,11 +121,14 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); + case kind::POW: + return RewriteResponse(REWRITE_DONE, t); default: Unhandled(k); } } } + RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ if(t.isConst()){ return rewriteConstant(t); @@ -182,6 +185,33 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ //Unimplemented("IS_INTEGER, nonconstant"); //return rewriteIsInteger(t); return RewriteResponse(REWRITE_DONE, t); + case kind::POW: + { + if(t[1].getKind() == kind::CONST_RATIONAL){ + const Rational& exp = t[1].getConst<Rational>(); + TNode base = t[0]; + if(exp.sgn() == 0){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1))); + }else if(exp.sgn() > 0 && exp.isIntegral()){ + Integer num = exp.getNumerator(); + NodeBuilder<> nb(kind::MULT); + Integer one(1); + for(Integer i(0); i < num; i = i + one){ + nb << base; + } + Assert(nb.getNumChildren() > 0); + Node mult = nb; + return RewriteResponse(REWRITE_AGAIN, mult); + } + } + + // Todo improve the exception thrown + std::stringstream ss; + ss << "The POW(^) operator can only be used with a natural number "; + ss << "in the exponent. Exception occured in:" << std::endl; + ss << " " << t; + throw Exception(ss.str()); + } default: Unreachable(); } |