From 1eac626e6c23dca3a3bb92e0a62289aecb61fc02 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 9 Dec 2020 06:38:15 +0100 Subject: [PATCH] Split initial exp lemma into separate lemmas. (#5622) This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas. --- .../nl/transcendental/exponential_solver.cpp | 49 ++++++++++++------- 1 file changed, 30 insertions(+), 19 deletions(-) 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); } } } -- 2.30.2