mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

adding placeholder for refining power of 2

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-20 14:37:05 -08:00
parent 0f4f32c5d0
commit 4e6d498a60
1 changed files with 42 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/smt/theory_lra.cpp
View file

@ -1556,6 +1556,33 @@ public:
return !m_asserted_atoms.empty();
}
final_check_status eval_power(expr* e) {
return FC_GIVEUP;
expr* x, * y;
VERIFY(a.is_power(e, x, y));
enode* xn = get_enode(x);
enode* yn = get_enode(y);
if (!xn || !yn)
return FC_GIVEUP;
rational valx, valy, valn;
bool vx = get_value(xn, valx);
bool vy = get_value(yn, valy);
enode* n = get_enode(e);
bool vn = get_value(n, valn);
verbose_stream() << vx << " " << valx << " " << vy << " " << valy << "\n";
verbose_stream() << vn << " " << valn << "\n";
// add tangent lemmas for power:
// valx > 0 valy > 0 => n >= rational_floor(valx^valy)
// establish equality using algebraic numerals
return FC_GIVEUP;
}
final_check_status eval_unsupported(expr* e) {
if (a.is_power(e))
return eval_power(e);
return FC_GIVEUP;
}
final_check_status final_check_eh() {
if (propagate_core())
return FC_CONTINUE;
@ -1607,10 +1634,21 @@ public:
for (expr* e : m_not_handled) {
if (!ctx().is_relevant(e))
continue;
(void) e; // just in case TRACE() is a no-op
TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";);
st = FC_GIVEUP;
}
st = FC_DONE;
switch (eval_unsupported(e)) {
case FC_CONTINUE:
st = FC_CONTINUE;
break;
case FC_GIVEUP:
if (st != FC_CONTINUE)
st = FC_GIVEUP;
break;
default:
break;
}
if (st == FC_CONTINUE)
break;
}
return st;
case l_false:
get_infeasibility_explanation_and_set_conflict();