diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-31 06:06:39 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-31 08:06:39 -0600 |
commit | b77641f3db3d868536549deb0fc7851ff07b5e88 (patch) | |
tree | 3377181222efba76be911604e8f179d3c90d7cb9 /src/theory/arith | |
parent | a456ef81b15e2f8612cd41a31ad811af35f47846 (diff) |
Fix arithmetic rewriter for exponential (#3688)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a1264c612..d8dd2cf58 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -390,12 +390,18 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { }else{ return RewriteResponse(REWRITE_DONE, t); } - }else if(t[0].getKind() == kind::PLUS ){ + } + else if (t[0].getKind() == kind::PLUS) + { std::vector<Node> product; - for( unsigned i=0; i<t[0].getNumChildren(); i++ ){ - product.push_back(nm->mkNode(kind::EXPONENTIAL, t[0][i])); + for (const Node tc : t[0]) + { + product.push_back(nm->mkNode(kind::EXPONENTIAL, tc)); } - return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::MULT, product)); + // We need to do a full rewrite here, since we can get exponentials of + // constants, e.g. when we are rewriting exp(2 + x) + return RewriteResponse(REWRITE_AGAIN_FULL, + nm->mkNode(kind::MULT, product)); } } break; |