From fad428381a3e8e448e096e57d27b59a464660afe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jan 2024 15:33:48 -0800 Subject: [PATCH] prepare for integer intervals --- src/nlsat/nlsat_evaluator.cpp | 7 ++++--- src/nlsat/nlsat_explain.cpp | 4 ++-- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 1d55db9cb78..f95a80b56fe 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -593,7 +593,8 @@ namespace nlsat { 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(); unsigned i = a->i(); SASSERT(i > 0); @@ -664,8 +665,8 @@ namespace nlsat { return result; } - interval_set_ref infeasible_intervals(atom * a, 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); + 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), is_int, neg, cls) : infeasible_intervals(to_root_atom(a), is_int, neg, cls); } }; diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 0b76a14efb1..ef5745fe40a 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1439,7 +1439,7 @@ namespace nlsat { literal l = core[i]; atom * a = m_atoms[l.var()]; 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); if (ism.is_full(r)) { // Done @@ -1458,7 +1458,7 @@ namespace nlsat { literal l = todo[i]; atom * a = m_atoms[l.var()]; 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); if (ism.is_full(r)) { // literal l must be in the core