From b77641f3db3d868536549deb0fc7851ff07b5e88 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 31 Jan 2020 06:06:39 -0800
Subject: [PATCH] Fix arithmetic rewriter for exponential (#3688)

---
 src/theory/arith/arith_rewriter.cpp        | 14 ++++++++++----
 test/regress/CMakeLists.txt                |  1 +
 test/regress/regress0/arith/issue3683.smt2 |  5 +++++
 test/unit/theory/theory_arith_white.h      |  6 ++++++
 4 files changed, 22 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/arith/issue3683.smt2

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));
   }
 };
-- 
2.30.2