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 | |
| parent | a456ef81b15e2f8612cd41a31ad811af35f47846 (diff) | |
Fix arithmetic rewriter for exponential (#3688)
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 14 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/issue3683.smt2 | 5 | ||||
| -rw-r--r-- | test/unit/theory/theory_arith_white.h | 6 |
4 files changed, 22 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; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d5414364a..e49af0a83 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -28,6 +28,7 @@ set(regress_0_tests regress0/arith/issue1399.smt2 regress0/arith/issue3412.smt2 regress0/arith/issue3413.smt2 + regress0/arith/issue3683.smt2 regress0/arith/ite-lift.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc diff --git a/test/regress/regress0/arith/issue3683.smt2 b/test/regress/regress0/arith/issue3683.smt2 new file mode 100644 index 000000000..0ce6dc89d --- /dev/null +++ b/test/regress/regress0/arith/issue3683.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(declare-fun a () Real) +(assert (= (+ 2 (exp (+ 2 a))) 0)) +(set-info :status unsat) +(check-sat) diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 0e71fe911..0460759bc 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -294,6 +294,7 @@ public: void testIntNormalForm() { Node x = d_nm->mkVar(*d_intType); + Node xr = d_nm->mkVar(*d_realType); Node c0 = d_nm->mkConst<Rational>(d_zero); Node c1 = d_nm->mkConst<Rational>(d_one); Node c2 = d_nm->mkConst<Rational>(Rational(2)); @@ -327,5 +328,10 @@ public: // (abs x) --> (abs x) Node absX = d_nm->mkNode(ABS, x); TS_ASSERT_EQUALS(Rewriter::rewrite(absX), absX); + + // (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1)) + Node t = d_nm->mkNode(EXPONENTIAL, d_nm->mkNode(PLUS, c2, xr)).eqNode(c0); + TS_ASSERT_EQUALS(Rewriter::rewrite(Rewriter::rewrite(t)), + Rewriter::rewrite(t)); } }; |