From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 9 Dec 2020 05:38:15 +0000 (+0100)
Subject: Split initial exp lemma into separate lemmas. (#5622)
X-Git-Tag: cvc5-1.0.0~2470
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1eac626e6c23dca3a3bb92e0a62289aecb61fc02;p=cvc5.git

Split initial exp lemma into separate lemmas. (#5622)

This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas.
---

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 243fa251b..cbed48a2a 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -69,26 +69,37 @@ void ExponentialSolver::checkInitialRefine()
       if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end())
       {
         d_tf_initial_refine[t] = true;
-        Node lem;
-        // ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) <
-        // 1 ) ^ ( x <= 0 V exp( x ) > x + 1 )
-        lem = nm->mkNode(
-            Kind::AND,
-            nm->mkNode(Kind::GT, t, d_data->d_zero),
-            nm->mkNode(Kind::EQUAL,
-                       t[0].eqNode(d_data->d_zero),
-                       t.eqNode(d_data->d_one)),
-            nm->mkNode(Kind::EQUAL,
-                       nm->mkNode(Kind::LT, t[0], d_data->d_zero),
-                       nm->mkNode(Kind::LT, t, d_data->d_one)),
-            nm->mkNode(
-                Kind::OR,
-                nm->mkNode(Kind::LEQ, t[0], d_data->d_zero),
-                nm->mkNode(
-                    Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one))));
-        if (!lem.isNull())
         {
-          d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_INIT_REFINE);
+          // exp is always positive: exp(t) > 0
+          Node lem = nm->mkNode(Kind::GT, t, d_data->d_zero);
+          d_data->d_im.addPendingArithLemma(
+              lem, InferenceId::NL_T_INIT_REFINE, nullptr);
+        }
+        {
+          // exp at zero: (t = 0) <=> (exp(t) = 1)
+          Node lem = nm->mkNode(Kind::EQUAL,
+                                t[0].eqNode(d_data->d_zero),
+                                t.eqNode(d_data->d_one));
+          d_data->d_im.addPendingArithLemma(
+              lem, InferenceId::NL_T_INIT_REFINE, nullptr);
+        }
+        {
+          // exp on negative values: (t < 0) <=> (exp(t) < 1)
+          Node lem = nm->mkNode(Kind::EQUAL,
+                                nm->mkNode(Kind::LT, t[0], d_data->d_zero),
+                                nm->mkNode(Kind::LT, t, d_data->d_one));
+          d_data->d_im.addPendingArithLemma(
+              lem, InferenceId::NL_T_INIT_REFINE, nullptr);
+        }
+        {
+          // exp on positive values: (t <= 0) or (exp(t) > t+1)
+          Node lem = nm->mkNode(
+              Kind::OR,
+              nm->mkNode(Kind::LEQ, t[0], d_data->d_zero),
+              nm->mkNode(
+                  Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one)));
+          d_data->d_im.addPendingArithLemma(
+              lem, InferenceId::NL_T_INIT_REFINE, nullptr);
         }
       }
     }