Api (#7097)

* rename ul_pair to column Signed-off-by: Lev Nachmanson <[email protected]> * t Signed-off-by: Lev Nachmanson <[email protected]> * simple test passed * remove an assert * relax an assertion * remove an obsolete function Signed-off-by: Lev Nachmanson <[email protected]> * access a term by the term column * remove the column index from colunm.h * remove an unused method * remove debug code * fix the build of lp_tst Signed-off-by: Lev Nachmanson <[email protected]> --------- Signed-off-by: Lev Nachmanson <[email protected]> Co-authored-by: Lev Nachmanson <[email protected]>
Z3Prover · Jan 25, 2024 · bdb9106 · bdb9106
1 parent 1335466
commit bdb9106
Show file tree

Hide file tree

Showing 45 changed files with 587 additions and 973 deletions.
diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
@@ -291,7 +291,6 @@ public :
             int bound_sign = (is_lower_bound ? 1 : -1);
             int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
 
-            SASSERT(!tv::is_term(bound_j));
             u_dependency* ret = nullptr;
             for (auto const& r : lar->get_row(row_index)) {
                 unsigned j = r.var();

diff --git a/src/math/lp/ul_pair.h → src/math/lp/column.h b/src/math/lp/ul_pair.h → src/math/lp/column.h
@@ -37,17 +37,19 @@ inline std::ostream& operator<<(std::ostream& out, lconstraint_kind k) {
     return out << "??";
 }
 
-inline bool compare(const std::pair<mpq, var_index> & a, const std::pair<mpq, var_index> & b) {
+inline bool compare(const std::pair<mpq, lpvar> & a, const std::pair<mpq, lpvar> & b) {
     return a.second < b.second;
 }
-
-class ul_pair {
+class lar_term; // forward definition
+class column {
     u_dependency* m_lower_bound_witness = nullptr;
     u_dependency* m_upper_bound_witness = nullptr;
     bool          m_associated_with_row = false;  
+    lpvar         m_j; //the column index
+    lar_term*     m_term = nullptr;
 public:
-    // TODO - seems more straight-forward to just expose ul_pair as a struct with direct access to attributes.
-    
+    lar_term*  term() const { return m_term; }
+
     u_dependency*& lower_bound_witness() { return m_lower_bound_witness; }
     u_dependency* lower_bound_witness() const { return m_lower_bound_witness; }
     u_dependency*& upper_bound_witness() { return m_upper_bound_witness; }
@@ -56,20 +58,21 @@ class ul_pair {
     // equality is used by stackedvector operations.
     // this appears to be a low level reason
 
-    bool operator!=(const ul_pair & p) const {
+    bool operator!=(const column & p) const {
         return !(*this == p);
     }
 
-    bool operator==(const ul_pair & p) const {
+    bool operator==(const column & p) const {
         return m_lower_bound_witness == p.m_lower_bound_witness
             && m_upper_bound_witness == p.m_upper_bound_witness 
             && m_associated_with_row == p.m_associated_with_row;
     }
-    // empty constructor
-    ul_pair() {}
+    column()  = delete;
+    column(bool) = delete;
 
-    ul_pair(bool associated_with_row) :
-        m_associated_with_row(associated_with_row) {}
+
+    column(bool associated_with_row, lar_term* term) :
+        m_associated_with_row(associated_with_row), m_term(term) {}
 
     bool associated_with_row() const { return m_associated_with_row; }
 };

diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
@@ -536,7 +536,7 @@ bool emonics::invariant() const {
             do {
                 auto const& m = m_monics[c->m_index];
                 bool found = false;
-                for (lp::var_index w : m.rvars()) {
+                for (lp::lpvar w : m.rvars()) {
                     auto w1 = m_ve.find(w);
                     found |= v1.var() == w1.var();
                 }

diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h
@@ -109,7 +109,7 @@ class general_matrix {
         auto & row = m_data[adjust_row(i)];
         lp_assert(row_is_initialized_correctly(row));
         for (lp::lar_term::ival p : c) {
-            unsigned j = adjust_column(column_fix(p.column().index()));
+            unsigned j = adjust_column(column_fix(p.j()));
             row[j] = sign * p.coeff();
         }
     }

diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
@@ -156,7 +156,7 @@ struct create_cut {
 
     template <typename T>
     void dump_coeff(std::ostream & out, const T& c) const {
-        dump_coeff_val(out << "(* ", c.coeff()) << " " << var_name(c.column().index()) << ")";
+        dump_coeff_val(out << "(* ", c.coeff()) << " " << var_name(c.j()) << ")";
     }
 
     std::ostream& dump_row_coefficients(std::ostream & out) const {
@@ -183,9 +183,8 @@ struct create_cut {
         for (const auto & p : m_row) 
             dump_declaration(out, p.var());
         for (lar_term::ival p : m_t) {
-            auto t = lia.lra.column2tv(p.column());
-            if (t.is_term()) 
-                dump_declaration(out, t.id());            
+            if (lia.lra.column_has_term(p.j()))
+                dump_declaration(out, p.j());            
         }
     }
 
@@ -491,9 +490,8 @@ struct create_cut {
             return all_of(t, [&](auto ci) { return ci.coeff().is_small(); });
         };
         auto add_cut = [&](const lar_term& t, const mpq& k, u_dependency * dep) {
-            lp::lpvar term_index = lra.add_term(t.coeffs_as_vector(), UINT_MAX);
-            term_index = lra.map_term_index_to_column_index(term_index);
-            lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::GE,  k, dep); 
+            lp::lpvar j = lra.add_term(t.coeffs_as_vector(), UINT_MAX);
+            lra.update_column_type_and_bound(j, lp::lconstraint_kind::GE,  k, dep); 
         };
         auto _check_feasible = [&](void) {
             lra.find_feasible_solution();

diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp
@@ -20,7 +20,7 @@ namespace lp  {
         lra(lia.lra),
         m_settings(lia.settings()),
         m_abs_max(zero_of_type<mpq>()),
-        m_var_register(false) {}
+        m_var_register() {}
 
     bool hnf_cutter::is_full() const {
         return
@@ -50,7 +50,7 @@ namespace lp  {
         m_constraints_for_explanation.push_back(ci);
 
         for (lar_term::ival p : *t) {
-            m_var_register.add_var(p.column().index(), true); // hnf only deals with integral variables for now
+            m_var_register.add_var(p.j(), true); // hnf only deals with integral variables for now
             mpq t = abs(ceil(p.coeff()));
             if (t > m_abs_max)
                 m_abs_max = t;
@@ -227,12 +227,12 @@ branch y_i >= ceil(y0_i) is impossible.
 
     svector<unsigned> hnf_cutter::vars() const { return m_var_register.vars(); }
 
-    void hnf_cutter::try_add_term_to_A_for_hnf(tv const &i) {
+    void hnf_cutter::try_add_term_to_A_for_hnf(lpvar j) {
         mpq rs;
-        const lar_term& t = lra.get_term(i);
+        const lar_term& t = lra.get_term(j);
         u_dependency* dep;
         bool upper_bound;
-        if (!is_full() && lra.get_equality_and_right_side_for_term_on_current_x(i, rs, dep, upper_bound)) {
+        if (!is_full() && lra.get_equality_and_right_side_for_term_on_current_x(j, rs, dep, upper_bound)) {
             add_term(&t, rs, dep, upper_bound);
         }
     }
@@ -243,8 +243,8 @@ branch y_i >= ceil(y0_i) is impossible.
 
     bool hnf_cutter::init_terms_for_hnf_cut() {
         clear();
-        for (unsigned i = 0; i < lra.terms().size() && !is_full(); i++) 
-            try_add_term_to_A_for_hnf(tv::term(i));
+        for (const lar_term* t:  lra.terms()) 
+            try_add_term_to_A_for_hnf(t->j());
         return hnf_has_var_with_non_integral_value();
     }
 

diff --git a/src/math/lp/hnf_cutter.h b/src/math/lp/hnf_cutter.h
@@ -50,7 +50,7 @@ class hnf_cutter {
 private:
     bool init_terms_for_hnf_cut();
     bool hnf_has_var_with_non_integral_value() const;
-    void try_add_term_to_A_for_hnf(tv const& i);
+    void try_add_term_to_A_for_hnf(lpvar);
 
     unsigned terms_count() const { return m_terms.size();  }
     const mpq & abs_max() const { return m_abs_max; }

diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
@@ -34,7 +34,7 @@ lia_move int_branch::create_branch_on_column(int j) {
     lia.m_t.clear();
 
     lp_assert(j != -1);
-    lia.m_t.add_monomial(mpq(1), lra.column_to_reported_index(j));
+    lia.m_t.add_monomial(mpq(1), j);
     if (lia.is_free(j)) {
         lia.m_upper = lia.random() % 2;
         lia.m_k = mpq(0);

diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp
@@ -55,21 +55,21 @@ namespace lp {
         lia.settings().stats().m_cube_success++;
         return lia_move::sat;
     }
-
+// i is the column index having the term
     bool int_cube::tighten_term_for_cube(unsigned i) {
-        if (!lra.term_is_used_as_row(i))
+        if (!lra.column_associated_with_row(i))
             return true;
-        const lar_term* t = lra.terms()[i];
-        impq delta = get_cube_delta_for_term(*t);
-        TRACE("cube", lra.print_term_as_indices(*t, tout); tout << ", delta = " << delta << "\n";);
+        const lar_term& t = lra.get_term(i);
+        impq delta = get_cube_delta_for_term(t);
+        TRACE("cube", lra.print_term_as_indices(t, tout); tout << ", delta = " << delta << "\n";);
         if (is_zero(delta))
             return true;
-        return lra.tighten_term_bounds_by_delta(tv::term(i), delta);
+        return lra.tighten_term_bounds_by_delta(i, delta);
     }
 
     bool int_cube::tighten_terms_for_cube() {
-        for (unsigned i = 0; i < lra.terms().size(); i++)
-            if (!tighten_term_for_cube(i)) {
+        for (const lar_term* t: lra.terms())
+            if (!tighten_term_for_cube(t->j())) {
                 TRACE("cube", tout << "cannot tighten";);
                 return false;
             }
@@ -86,7 +86,7 @@ namespace lp {
             bool seen_minus = false;
             bool seen_plus = false;
             for(lar_term::ival p : t) {
-                if (!lia.column_is_int(p.column()))
+                if (!lia.column_is_int(p.j()))
                     goto usual_delta;
                 const mpq & c = p.coeff();
                 if (c == one_of_type<mpq>()) {
@@ -104,7 +104,7 @@ namespace lp {
     usual_delta:
         mpq delta = zero_of_type<mpq>();
         for (lar_term::ival p : t)
-            if (lia.column_is_int(p.column()))
+            if (lia.column_is_int(p.j()))
                 delta += abs(p.coeff());
 
         delta *= mpq(1, 2);

diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
@@ -228,7 +228,7 @@ namespace lp {
 
     bool int_solver::cut_indices_are_columns() const {
         for (lar_term::ival p : m_t) {
-            if (p.column().index() >= lra.A_r().column_count())
+            if (p.j() >= lra.A_r().column_count())
                 return false;
         }
         return true;
@@ -271,7 +271,7 @@ namespace lp {
         return lra.settings();
     }
 
-    bool int_solver::column_is_int(column_index const& j) const {
+    bool int_solver::column_is_int(lpvar j) const {
         return lra.column_is_int(j);
     }
 
@@ -296,7 +296,7 @@ namespace lp {
     }
 
     bool int_solver::is_term(unsigned j) const {
-        return lra.column_corresponds_to_term(j);
+        return lra.column_has_term(j);
     }
 
     unsigned int_solver::column_count() const  {

diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
@@ -83,7 +83,7 @@ class int_solver {
     bool is_real(unsigned j) const;
     const impq & lower_bound(unsigned j) const;
     const impq & upper_bound(unsigned j) const;
-    bool column_is_int(column_index const& j) const;
+    bool column_is_int(lpvar j) const;
     const impq & get_value(unsigned j) const;
     bool at_lower(unsigned j) const;
     bool at_upper(unsigned j) const;

diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h
@@ -16,7 +16,7 @@ Copyright (c) 2017 Microsoft Corporation
 #include "util/region.h"
 #include "util/stacked_value.h"
 #include "math/lp/lp_utils.h"
-#include "math/lp/ul_pair.h"
+#include "math/lp/column.h"
 #include "math/lp/lar_term.h"
 #include "math/lp/column_namer.h"
 namespace lp {
@@ -46,7 +46,7 @@ class lar_base_constraint {
 
    public:
 
-    virtual vector<std::pair<mpq, var_index>> coeffs() const = 0;
+    virtual vector<std::pair<mpq, lpvar>> coeffs() const = 0;
     lar_base_constraint(unsigned j, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) :
         m_kind(kind), m_right_side(right_side), m_active(false), m_j(j), m_dep(dep) {}
     virtual ~lar_base_constraint() = default;
@@ -69,8 +69,8 @@ class lar_var_constraint: public lar_base_constraint {
     lar_var_constraint(unsigned j, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) : 
         lar_base_constraint(j, kind, dep, right_side) {}
 
-    vector<std::pair<mpq, var_index>> coeffs() const override {
-        vector<std::pair<mpq, var_index>> ret;
+    vector<std::pair<mpq, lpvar>> coeffs() const override {
+        vector<std::pair<mpq, lpvar>> ret;
         ret.push_back(std::make_pair(one_of_type<mpq>(), column()));
         return ret;
     }
@@ -84,7 +84,7 @@ class lar_term_constraint: public lar_base_constraint {
     lar_term_constraint(unsigned j, const lar_term* t, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) : 
         lar_base_constraint(j, kind, dep, right_side), m_term(t) {}
 
-    vector<std::pair<mpq, var_index>> coeffs() const override { return m_term->coeffs_as_vector(); }
+    vector<std::pair<mpq, lpvar>> coeffs() const override { return m_term->coeffs_as_vector(); }
     unsigned size() const override { return m_term->size();}
 };
 
@@ -168,7 +168,7 @@ class constraint_set {
         m_region.pop_scope(k);
     }
 
-    constraint_index add_var_constraint(var_index j, lconstraint_kind k, mpq const& rhs) {
+    constraint_index add_var_constraint(lpvar j, lconstraint_kind k, mpq const& rhs) {
         return add(new (m_region) lar_var_constraint(j, k, mk_dep(), rhs));
     }