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

prepare for integer intervals

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-23 15:33:48 -08:00
parent 98c9fa7faf
commit fad428381a
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/nlsat/nlsat_evaluator.cpp
View file

@ -593,7 +593,8 @@ namespace nlsat {
return result; return result;
} }
interval_set_ref infeasible_intervals(root_atom * a, bool neg, clause const* cls) { interval_set_ref infeasible_intervals(root_atom * a, bool is_int, bool neg, clause const* cls) {
(void) is_int;
atom::kind k = a->get_kind(); atom::kind k = a->get_kind();
unsigned i = a->i(); unsigned i = a->i();
SASSERT(i > 0); SASSERT(i > 0);
@ -664,8 +665,8 @@ namespace nlsat {
return result; return result;
} }
interval_set_ref infeasible_intervals(atom * a, bool neg, clause const* cls) { interval_set_ref infeasible_intervals(atom * a, bool is_int, bool neg, clause const* cls) {
return a->is_ineq_atom() ? infeasible_intervals(to_ineq_atom(a), neg, cls) : infeasible_intervals(to_root_atom(a), neg, cls); return a->is_ineq_atom() ? infeasible_intervals(to_ineq_atom(a), is_int, neg, cls) : infeasible_intervals(to_root_atom(a), is_int, neg, cls);
} }
}; };

4
src/nlsat/nlsat_explain.cpp
View file

@ -1439,7 +1439,7 @@ namespace nlsat {
literal l = core[i]; literal l = core[i];
atom * a = m_atoms[l.var()]; atom * a = m_atoms[l.var()];
SASSERT(a != 0); SASSERT(a != 0);
interval_set_ref inf = m_evaluator.infeasible_intervals(a, l.sign(), nullptr); interval_set_ref inf = m_evaluator.infeasible_intervals(a, m_solver.is_int(a->max_var()), l.sign(), nullptr);
r = ism.mk_union(inf, r); r = ism.mk_union(inf, r);
if (ism.is_full(r)) { if (ism.is_full(r)) {
// Done // Done
@ -1458,7 +1458,7 @@ namespace nlsat {
literal l = todo[i]; literal l = todo[i];
atom * a = m_atoms[l.var()]; atom * a = m_atoms[l.var()];
SASSERT(a != 0); SASSERT(a != 0);
interval_set_ref inf = m_evaluator.infeasible_intervals(a, l.sign(), nullptr); interval_set_ref inf = m_evaluator.infeasible_intervals(a, m_solver.is_int(a->max_var()), l.sign(), nullptr);
r = ism.mk_union(inf, r); r = ism.mk_union(inf, r);
if (ism.is_full(r)) { if (ism.is_full(r)) {
// literal l must be in the core // literal l must be in the core