mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

reshuffle pre-conditions for powers

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-25 13:51:19 -08:00
parent e41dd91893
commit 8be43ca68b
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/lp/nla_powers.cpp
View file

@ -83,6 +83,8 @@ namespace nla {
return l_undef;
core& c = m_core;
if (c.use_nra_model())
return l_undef;
auto xval = c.val(x);
auto yval = c.val(y);
@ -90,7 +92,6 @@ namespace nla {
lemmas.reset();
if (xval != 0 && yval == 0 && rval != 1) {
new_lemma lemma(c, "x != 0 => x^0 = 1");
lemma |= ineq(x, llc::EQ, rational::zero());
@ -99,7 +100,7 @@ namespace nla {
return l_false;
}
if (xval == 0 && yval > 0 && rval != 0) {
if (xval == 0 && yval != 0 && rval != 0) {
new_lemma lemma(c, "y != 0 => 0^y = 0");
lemma |= ineq(x, llc::NE, rational::zero());
lemma |= ineq(y, llc::EQ, rational::zero());
@ -107,14 +108,14 @@ namespace nla {
return l_false;
}
if (xval > 0 && rval < 0 && rval <= 0) {
if (xval > 0 && rval <= 0) {
new_lemma lemma(c, "x > 0 => x^y > 0");
lemma |= ineq(x, llc::LE, rational::zero());
lemma |= ineq(r, llc::GT, rational::zero());
return l_false;
}
if (xval > 1 && rval >= 1 && yval < 0) {
if (xval > 1 && yval < 0 && rval >= 1) {
new_lemma lemma(c, "x > 1, y < 0 => x^y < 1");
lemma |= ineq(x, llc::LE, rational::one());
lemma |= ineq(y, llc::GE, rational::zero());
@ -122,7 +123,7 @@ namespace nla {
return l_false;
}
if (xval > 1 && rval <= 1 && yval > 0) {
if (xval > 1 && yval > 0 && rval <= 1) {
new_lemma lemma(c, "x > 1, y > 0 => x^y > 1");
lemma |= ineq(x, llc::LE, rational::one());
lemma |= ineq(y, llc::LE, rational::zero());