diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2020-12-09 06:38:15 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-08 23:38:15 -0600 |
| commit | 1eac626e6c23dca3a3bb92e0a62289aecb61fc02 (patch) | |
| tree | 0501228cac7e2dac226b42cfb9a635b2d9fd8685 | |
| parent | 6fdac54fe0153bb17eca1c01eb5bd45b9418c596 (diff) | |
Split initial exp lemma into separate lemmas. (#5622)
This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas.
| -rw-r--r-- | src/theory/arith/nl/transcendental/exponential_solver.cpp | 49 |
1 files 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); } } } |