isolate constraints in a constraint_set

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/lar_constraints.h

@@ -158,7 +158,8 @@ public:
     // TBD: would like to make this opaque
     // and expose just active constraints
     // constraints need not be active.
-    unsigned size() const { return m_constraints.size(); }
+    bool valid_index(constraint_index ci) const { return ci < m_constraints.size(); }
+//    unsigned size() const { return m_constraints.size(); }
     vector<lar_base_constraint*>::const_iterator begin() const { return m_constraints.begin(); }
     vector<lar_base_constraint*>::const_iterator end() const { return m_constraints.end(); }
 

src/math/lp/lar_solver.cpp

@@ -1053,7 +1053,7 @@ bool lar_solver::the_left_sides_sum_to_zero(const vector<std::pair<mpq, unsigned
     for (auto & it : evidence) {
         mpq coeff = it.first;
         constraint_index con_ind = it.second;
-        lp_assert(con_ind < m_constraints.size());
+        lp_assert(m_constraints.valid_index(con_ind));
         register_in_map(coeff_map, m_constraints[con_ind], coeff);
     }
 
@@ -1107,7 +1107,7 @@ mpq lar_solver::sum_of_right_sides_of_explanation(explanation& exp) const {
     for (auto & it : exp) {
         mpq coeff = it.first;
         constraint_index con_ind = it.second;
-        lp_assert(con_ind < m_constraints.size());
+        lp_assert(m_constraints.valid_index(con_ind));
         ret += (m_constraints[con_ind].m_right_side - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff;
     }
     return ret;
@@ -1201,7 +1201,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
         const ul_pair & ul = m_columns_to_ul_pairs[j];
 
         constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.lower_bound_witness();
-        lp_assert(bound_constr_i < m_constraints.size());
+        lp_assert(m_constraints.valid_index(bound_constr_i));
         exp.push_justification(bound_constr_i, coeff);
     } 
 }
@@ -1830,7 +1830,7 @@ constraint_index lar_solver::add_constraint_from_term_and_create_new_column_row(
     add_row_from_term_no_constraint(term, term_j);
     unsigned j = A_r().column_count() - 1;
     constraint_index ci = m_constraints.add_term_constraint(term, kind, right_side);    
-    update_column_type_and_bound(j, kind, right_side, m_constraints.size());
+    update_column_type_and_bound(j, kind, right_side, ci);
     lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
     return ci;
 }

src/math/lp/lar_solver.h

@@ -92,10 +92,6 @@ public:
     var_register                                        m_term_register;
     stacked_vector<ul_pair>                             m_columns_to_ul_pairs;
     constraint_set                                      m_constraints;
-#if 0
-    vector<lar_base_constraint*>                        m_constraints;
-    stacked_value<unsigned>                             m_constraint_count;
-#endif
     // the set of column indices j such that bounds have changed for j
     int_set                                             m_columns_with_changed_bound;
     int_set                                             m_rows_with_changed_bounds;
@@ -115,16 +111,10 @@ public:
     unsigned terms_start_index() const { return m_terms_start_index; }
     const vector<lar_term*> & terms() const { return m_terms; }
     lar_term const& term(unsigned i) const { return *m_terms[i]; }
-    constraint_set const& constraints() const {
-        return m_constraints;
-    }
-    void set_int_solver(int_solver * int_slv) {
-        m_int_solver = int_slv;
-    }
-    int_solver * get_int_solver() {
-        return m_int_solver;
-    }
-    const lar_base_constraint& get_constraint(unsigned ci) const { return m_constraints[ci]; }
+    constraint_set const& constraints() const { return m_constraints; }
+    void set_int_solver(int_solver * int_slv) { m_int_solver = int_slv; }
+    int_solver * get_int_solver() { return m_int_solver; }
+
     ////////////////// methods ////////////////////////////////
     static_matrix<mpq, numeric_pair<mpq>> & A_r();
     static_matrix<mpq, numeric_pair<mpq>> const & A_r() const;
@@ -354,12 +344,10 @@ public:
 
     void prepare_costs_for_r_solver(const lar_term & term);
     
-    bool maximize_term_on_corrected_r_solver(lar_term & term,
-                                             impq &term_max);    
+    bool maximize_term_on_corrected_r_solver(lar_term & term, impq &term_max);    
     // starting from a given feasible state look for the maximum of the term
     // return true if found and false if unbounded
-    lp_status maximize_term(unsigned j_or_term,
-                            impq &term_max);
+    lp_status maximize_term(unsigned j_or_term, impq &term_max);
     
 
     

src/math/lp/nla_core.cpp

@@ -995,7 +995,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
         }
     }
     for (const auto& p : current_expl()) {
-        const auto& c = m_lar_solver.get_constraint(p.second);
+        const auto& c = m_lar_solver.constraints()[p.second];
         for (const auto& r : c.coeffs()) {
             insert_j(r.second);
         }

src/math/lp/nra_solver.cpp

@@ -92,8 +92,11 @@ typedef nla::variable_map_type variable_map_type;
             vector<nlsat::assumption, false> core;
 
             // add linear inequalities from lra_solver
-            for (unsigned i = 0; i < s.constraints().size(); ++i) {
+            unsigned i = 0;
+            for (auto const* c : s.constraints()) {
+                (void)c;
                 add_constraint(i);
+                ++i;
             }
 
             // add polynomial definitions.