mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixes for #6590

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-15 15:11:44 -08:00
parent c1ecc49021
commit 7c08e53e94
2 changed files with 17 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -79,6 +79,7 @@ am().set(rval, am_value(r));
namespace nla { namespace nla {
lbool powers::check(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) { lbool powers::check(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
TRACE("nla", tout << r << " == " << x << "^" << y << "\n");
if (x == null_lpvar || y == null_lpvar || r == null_lpvar) if (x == null_lpvar || y == null_lpvar || r == null_lpvar)
return l_undef; return l_undef;
if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(r)) if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(r))
@ -145,17 +146,24 @@ namespace nla {
auto r2val = power(xval, yval.get_unsigned()); auto r2val = power(xval, yval.get_unsigned());
if (rval == r2val) if (rval == r2val)
return l_true; return l_true;
if (xval > 0 && r2val < rval) { if (c.random() % 2 == 0) {
SASSERT(yval > 0); new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0");
lemma |= ineq(x, llc::NE, xval);
lemma |= ineq(y, llc::NE, yval);
lemma |= ineq(r, llc::EQ, r2val);
return l_false;
}
if (yval > 0 && r2val > rval) {
new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0"); new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0");
lemma |= ineq(x, llc::LT, xval); lemma |= ineq(x, llc::LT, xval);
lemma |= ineq(y, llc::LT, yval); lemma |= ineq(y, llc::LT, yval);
lemma |= ineq(r, llc::GE, r2val); lemma |= ineq(r, llc::GE, r2val);
return l_false; return l_false;
} }
if (xval > 0 && r2val < rval) { if (r2val < rval) {
new_lemma lemma(c, "x >= x0 > 0, y <= y0 => r <= x0^y0"); new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0");
lemma |= ineq(x, llc::LT, xval); lemma |= ineq(x, llc::LE, rational::zero());
lemma |= ineq(x, llc::GT, xval);
lemma |= ineq(y, llc::GT, yval); lemma |= ineq(y, llc::GT, yval);
lemma |= ineq(r, llc::LE, r2val); lemma |= ineq(r, llc::LE, r2val);
return l_false; return l_false;

8
src/smt/theory_lra.cpp
View file

@ -814,12 +814,13 @@ class theory_lra::imp {
} }
lpvar get_lpvar(expr* e) { lpvar get_lpvar(expr* e) {
return get_lpvar(get_enode(e)); theory_var v = mk_var(e);
m_solver->register_existing_terms();
return register_theory_var_in_lar_solver(v);
} }
lpvar get_lpvar(enode* n) { lpvar get_lpvar(enode* n) {
ensure_column(n); return get_lpvar(n->get_expr());
return n ? get_lpvar(n->get_th_var(get_id())) : lp::null_lpvar;
} }
lpvar get_lpvar(theory_var v) const { lpvar get_lpvar(theory_var v) const {
@ -1674,7 +1675,6 @@ public:
for (expr* e : m_not_handled) { for (expr* e : m_not_handled) {
if (!ctx().is_relevant(e)) if (!ctx().is_relevant(e))
continue; continue;
st = FC_DONE;
switch (eval_unsupported(e)) { switch (eval_unsupported(e)) {
case FC_CONTINUE: case FC_CONTINUE:
st = FC_CONTINUE; st = FC_CONTINUE;