mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-13 14:40:55 +00:00
Code Activity

prepare for handling integer intervals

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-23 15:29:11 -08:00
parent 36453c5949
commit 98c9fa7faf
4 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_evaluator.cpp
View file

@ -488,7 +488,7 @@ namespace nlsat {
return sign; return sign;
} }
interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) { interval_set_ref infeasible_intervals(ineq_atom * a, bool is_int, bool neg, clause const* cls) {
sign_table & table = m_sign_table_tmp; sign_table & table = m_sign_table_tmp;
table.reset(); table.reset();
TRACE("nlsat_evaluator", m_solver.display(tout, *a) << "\n";); TRACE("nlsat_evaluator", m_solver.display(tout, *a) << "\n";);
@ -685,8 +685,8 @@ namespace nlsat {
return m_imp->eval(a, neg); return m_imp->eval(a, neg);
} }
interval_set_ref evaluator::infeasible_intervals(atom * a, bool neg, clause const* cls) { interval_set_ref evaluator::infeasible_intervals(atom * a, bool is_int, bool neg, clause const* cls) {
return m_imp->infeasible_intervals(a, neg, cls); return m_imp->infeasible_intervals(a, is_int, neg, cls);
} }
void evaluator::push() { void evaluator::push() {

2
src/nlsat/nlsat_evaluator.h
View file

@ -51,7 +51,7 @@ namespace nlsat {
Let x be a->max_var(). Then, the resultant set specifies which Let x be a->max_var(). Then, the resultant set specifies which
values of x falsify the given literal. values of x falsify the given literal.
*/ */
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);
void push(); void push();
void pop(unsigned num_scopes); void pop(unsigned num_scopes);

5
src/nlsat/nlsat_interval_set.cpp
View file

@ -695,12 +695,11 @@ namespace nlsat {
scoped_mpq _w(m_am.qm()); scoped_mpq _w(m_am.qm());
m_am.qm().set(_w, num, den); m_am.qm().set(_w, num, den);
m_am.set(w, _w); m_am.set(w, _w);
return;
} }
else { else {
m_am.set(w, 0); m_am.set(w, 0);
return;
} }
return;
} }
unsigned n = 0; unsigned n = 0;
@ -741,7 +740,7 @@ namespace nlsat {
for (unsigned i = 1; i < num; i++) { for (unsigned i = 1; i < num; i++) {
if (s->m_intervals[i-1].m_upper_open && s->m_intervals[i].m_lower_open) { if (s->m_intervals[i-1].m_upper_open && s->m_intervals[i].m_lower_open) {
SASSERT(m_am.eq(s->m_intervals[i-1].m_upper, s->m_intervals[i].m_lower)); // otherwise we would have found it in the previous step SASSERT(m_am.eq(s->m_intervals[i-1].m_upper, s->m_intervals[i].m_lower)); // otherwise we would have found it in the previous step
if (m_am.is_rational(s->m_intervals[i-1].m_upper)) { if (m_am.is_rational(s->m_intervals[i-1].m_upper)) {
m_am.set(w, s->m_intervals[i-1].m_upper); m_am.set(w, s->m_intervals[i-1].m_upper);
return; return;
} }

7
src/nlsat/nlsat_solver.cpp
View file

@ -486,7 +486,7 @@ namespace nlsat {
SASSERT(x == num_vars()); SASSERT(x == num_vars());
m_is_int. push_back(is_int); m_is_int. push_back(is_int);
m_watches. push_back(clause_vector()); m_watches. push_back(clause_vector());
m_infeasible.push_back(0); m_infeasible.push_back(nullptr);
m_var2eq. push_back(nullptr); m_var2eq. push_back(nullptr);
m_perm. push_back(x); m_perm. push_back(x);
m_inv_perm. push_back(x); m_inv_perm. push_back(x);
@ -1006,7 +1006,8 @@ namespace nlsat {
} }
void undo_set_updt(interval_set * old_set) { void undo_set_updt(interval_set * old_set) {
if (m_xk == null_var) return; if (m_xk == null_var)
return;
var x = m_xk; var x = m_xk;
if (x < m_infeasible.size()) { if (x < m_infeasible.size()) {
m_ism.dec_ref(m_infeasible[x]); m_ism.dec_ref(m_infeasible[x]);
@ -1356,7 +1357,7 @@ namespace nlsat {
atom * a = m_atoms[b]; atom * a = m_atoms[b];
SASSERT(a != nullptr); SASSERT(a != nullptr);
interval_set_ref curr_set(m_ism); interval_set_ref curr_set(m_ism);
curr_set = m_evaluator.infeasible_intervals(a, l.sign(), &cls); curr_set = m_evaluator.infeasible_intervals(a, is_int(m_xk), l.sign(), &cls);
TRACE("nlsat_inf_set", tout << "infeasible set for literal: "; display(tout, l); tout << "\n"; m_ism.display(tout, curr_set); tout << "\n"; TRACE("nlsat_inf_set", tout << "infeasible set for literal: "; display(tout, l); tout << "\n"; m_ism.display(tout, curr_set); tout << "\n";
display(tout, cls) << "\n";); display(tout, cls) << "\n";);
if (m_ism.is_empty(curr_set)) { if (m_ism.is_empty(curr_set)) {