fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 24, 2024 · 1b94d43 · 1b94d43
1 parent fad4283
commit 1b94d43
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 14 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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<std::pair<var, rational>> 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;