From 1b94d43a8bab976e42fc05f41f371a3f806927e2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jan 2024 08:52:56 -0800 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_evaluator.cpp | 13 ++++++------- src/nlsat/nlsat_evaluator.h | 2 +- src/nlsat/nlsat_explain.cpp | 4 ++-- src/nlsat/nlsat_solver.cpp | 8 ++++---- 4 files changed, 13 insertions(+), 14 deletions(-) diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index f95a80b56..1f93737dc 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -488,7 +488,7 @@ namespace nlsat { return sign; } - interval_set_ref infeasible_intervals(ineq_atom * a, bool is_int, bool neg, clause const* cls) { + interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) { sign_table & table = m_sign_table_tmp; table.reset(); TRACE("nlsat_evaluator", m_solver.display(tout, *a) << "\n";); @@ -593,8 +593,7 @@ namespace nlsat { return result; } - interval_set_ref infeasible_intervals(root_atom * a, bool is_int, bool neg, clause const* cls) { - (void) is_int; + interval_set_ref infeasible_intervals(root_atom * a, bool neg, clause const* cls) { atom::kind k = a->get_kind(); unsigned i = a->i(); SASSERT(i > 0); @@ -665,8 +664,8 @@ namespace nlsat { return result; } - 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); + 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); } }; @@ -686,8 +685,8 @@ namespace nlsat { return m_imp->eval(a, neg); } - interval_set_ref evaluator::infeasible_intervals(atom * a, bool is_int, bool neg, clause const* cls) { - return m_imp->infeasible_intervals(a, is_int, neg, cls); + interval_set_ref evaluator::infeasible_intervals(atom * a, bool neg, clause const* cls) { + return m_imp->infeasible_intervals(a, neg, cls); } void evaluator::push() { diff --git a/src/nlsat/nlsat_evaluator.h b/src/nlsat/nlsat_evaluator.h index 9f9b346dd..d2db3f41a 100644 --- a/src/nlsat/nlsat_evaluator.h +++ b/src/nlsat/nlsat_evaluator.h @@ -51,7 +51,7 @@ namespace nlsat { Let x be a->max_var(). Then, the resultant set specifies which values of x falsify the given literal. */ - interval_set_ref infeasible_intervals(atom * a, bool is_int, bool neg, clause const* cls); + interval_set_ref infeasible_intervals(atom * a, bool neg, clause const* cls); void push(); void pop(unsigned num_scopes); diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index ef5745fe4..0b76a14ef 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, m_solver.is_int(a->max_var()), l.sign(), nullptr); + interval_set_ref inf = m_evaluator.infeasible_intervals(a, 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, m_solver.is_int(a->max_var()), l.sign(), nullptr); + interval_set_ref inf = m_evaluator.infeasible_intervals(a, l.sign(), nullptr); r = ism.mk_union(inf, r); if (ism.is_full(r)) { // literal l must be in the core diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ef7afda91..16b28c246 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -827,7 +827,7 @@ namespace nlsat { // need to translate Boolean variables and literals scoped_bool_vars tr(checker); for (var x = 0; x < m_is_int.size(); ++x) { - checker.register_var(x, m_is_int[x]); + checker.register_var(x, is_int(x)); } bool_var bv = 0; tr.push_back(bv); @@ -1357,7 +1357,7 @@ namespace nlsat { atom * a = m_atoms[b]; SASSERT(a != nullptr); interval_set_ref curr_set(m_ism); - curr_set = m_evaluator.infeasible_intervals(a, is_int(m_xk), l.sign(), &cls); + curr_set = m_evaluator.infeasible_intervals(a, 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"; display(tout, cls) << "\n";); if (m_ism.is_empty(curr_set)) { @@ -1470,7 +1470,7 @@ namespace nlsat { void select_witness() { scoped_anum w(m_am); SASSERT(!m_ism.is_full(m_infeasible[m_xk])); - m_ism.peek_in_complement(m_infeasible[m_xk], m_is_int[m_xk], w, m_randomize); + m_ism.peek_in_complement(m_infeasible[m_xk], is_int(m_xk), w, m_randomize); TRACE("nlsat", tout << "infeasible intervals: "; m_ism.display(tout, m_infeasible[m_xk]); tout << "\n"; tout << "assigning "; m_display_var(tout, m_xk) << "(x" << m_xk << ") -> " << w << "\n";); @@ -1576,7 +1576,7 @@ namespace nlsat { vector> bounds; for (var x = 0; x < num_vars(); x++) { - if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { + if (is_int(x) && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { scoped_anum v(m_am), vlo(m_am); v = m_assignment.value(x); rational lo;