Fix arithmetic rewriter for exponential (#3688)

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a1264c6125eb9667895faa33b27dc7d687ace7c5..d8dd2cf58238bd2b161181679036efc2c787d98c 100644 (file)
--- 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 d5414364af6c7993192b82babe0b06ede2d77868..e49af0a83a0bcf007d6a4c269db923524326166a 100644 (file)
--- 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 (file)
index 0000000..0ce6dc8
--- /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 0e71fe9111d8b6d45913c44cf20db93436e3fbb3..0460759bc585faad315b028577d67776e4b7f576 100644 (file)
--- 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));
   }
 };