Merge branch 'master' of https://github.com/z3prover/z3

src/math/lp/int_solver.cpp

@@ -358,14 +358,14 @@ int_solver::int_solver(lar_solver& lar_slv) :
 // this will allow to enable and disable tracking of the pivot rows
 struct check_return_helper {
     lar_solver&      lra;
-    bool             m_track_pivoted_rows;
+    bool             m_track_touched_rows;
     check_return_helper(lar_solver& ls) :
         lra(ls),
-        m_track_pivoted_rows(lra.get_track_pivoted_rows()) {
+        m_track_touched_rows(lra.touched_rows_are_tracked()) {
-        lra.set_track_pivoted_rows(false);
+        lra.track_touched_rows(false);
     }
     ~check_return_helper() {
-        lra.set_track_pivoted_rows(m_track_pivoted_rows);
+        lra.track_touched_rows(m_track_touched_rows);
     }
 };
 

src/math/lp/lar_solver.cpp

@@ -16,7 +16,7 @@ namespace lp {
 
     void lar_solver::updt_params(params_ref const& _p) {
         smt_params_helper p(_p);
-        set_track_pivoted_rows(p.arith_bprop_on_pivoted_rows());
+        track_touched_rows(p.arith_bprop_on_pivoted_rows());
         set_cut_strategy(p.arith_branch_cut_ratio());
         m_settings.updt_params(_p);
     }
@@ -28,12 +28,14 @@ namespace lp {
         m_term_register(true),
         m_constraints(*this) {}
 
-    void lar_solver::set_track_pivoted_rows(bool v) {
+    // start or ends tracking the rows that were changed by solve()
-        m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v ? (&m_rows_with_changed_bounds) : nullptr;
+    void lar_solver::track_touched_rows(bool v) {
+        m_mpq_lar_core_solver.m_r_solver.m_touched_rows = v ? (&m_touched_rows) : nullptr;
     }
-
+   
-    bool lar_solver::get_track_pivoted_rows() const {
+    // returns true iff the solver tracks the rows that were changed by solve()    
-        return m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows != nullptr;
+    bool lar_solver::touched_rows_are_tracked() const {
+        return m_mpq_lar_core_solver.m_r_solver.m_touched_rows != nullptr;
     }
 
     lar_solver::~lar_solver() {
@@ -271,11 +273,11 @@ namespace lp {
         clean_popped_elements(n, m_incorrect_columns);
 
         for (auto rid : m_row_bounds_to_replay)
-            insert_row_with_changed_bounds(rid);
+            add_touched_row(rid);
         m_row_bounds_to_replay.reset();
 
         unsigned m = A_r().row_count();
-        clean_popped_elements(m, m_rows_with_changed_bounds);
+        clean_popped_elements(m, m_touched_rows);
         clean_inf_heap_of_r_solver_after_pop();
         lp_assert(
             m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
@@ -616,17 +618,11 @@ namespace lp {
                 left_side.push_back(std::make_pair(c, v));        
     }
 
-    void lar_solver::insert_row_with_changed_bounds(unsigned rid) {
+    void lar_solver::add_touched_row(unsigned rid) {
-        m_rows_with_changed_bounds.insert(rid);
+        m_touched_rows.insert(rid);
-    }
-
-
-
-    void lar_solver::detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j) {
-        for (auto& rc : m_mpq_lar_core_solver.m_r_A.m_columns[j])
-            insert_row_with_changed_bounds(rc.var());
     }
 
+   
     
     bool lar_solver::use_tableau_costs() const {
         return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
@@ -697,9 +693,9 @@ namespace lp {
 
     void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) {
         if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) 
-            insert_row_with_changed_bounds(m_mpq_lar_core_solver.m_r_heading[j]);
+            add_touched_row(m_mpq_lar_core_solver.m_r_heading[j]);
         else 
-            detect_rows_of_bound_change_column_for_nbasic_column_tableau(j);        
+            add_column_rows_to_touched_rows(j);        
     }
 
     void lar_solver::detect_rows_with_changed_bounds() {
@@ -1170,10 +1166,10 @@ namespace lp {
         ru.update();
     }
 
-    void lar_solver::mark_rows_for_bound_prop(lpvar j) {
+    void lar_solver::add_column_rows_to_touched_rows(lpvar j) {
-        auto& column = A_r().m_columns[j];
+        const auto& column = A_r().m_columns[j];
         for (auto const& r : column) 
-            insert_row_with_changed_bounds(r.var());        
+            add_touched_row(r.var());        
     }
 
     void lar_solver::pop() {
@@ -1457,8 +1453,7 @@ namespace lp {
             A_r().add_row();
             m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size());
             m_mpq_lar_core_solver.m_r_basis.push_back(j);
-            if (m_settings.bound_propagation())
+            add_touched_row(A_r().row_count() - 1);
-                insert_row_with_changed_bounds(A_r().row_count() - 1);
         }
         else {
             m_mpq_lar_core_solver.m_r_heading.push_back(-static_cast<int>(m_mpq_lar_core_solver.m_r_nbasis.size()) - 1);
@@ -1545,8 +1540,7 @@ namespace lp {
         var_index ret = tv::mask_term(adjusted_term_index);
         if (!coeffs.empty()) {
             add_row_from_term_no_constraint(m_terms.back(), ret);
-            if (m_settings.bound_propagation())
+            add_touched_row(A_r().row_count() - 1);
-                insert_row_with_changed_bounds(A_r().row_count() - 1);
         }
         lp_assert(m_var_register.size() == A_r().column_count());
         if (m_need_register_terms) 
@@ -1594,7 +1588,7 @@ namespace lp {
         m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
         increase_by_one_columns_with_changed_bounds();
         m_incorrect_columns.increase_size_by_one();
-        m_rows_with_changed_bounds.increase_size_by_one();
+        m_touched_rows.increase_size_by_one();
         add_new_var_to_core_fields_for_mpq(true);
         
     }
@@ -1745,23 +1739,20 @@ namespace lp {
             update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
         TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j)?"feas":"non-feas") << ", and " << (this->column_is_bounded(j)? "bounded":"non-bounded") << std::endl;);    
     }
-    // clang-format on
     void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) {
         m_columns_with_changed_bounds.insert(j);
         TRACE("lar_solver", tout << "column " << j << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
     }
-    // clang-format off
     void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
-        lconstraint_kind kind,
+                                                                 lconstraint_kind kind,
-        const mpq& right_side,
+                                                                 const mpq& right_side,
-        constraint_index constr_index,
+                                                                 constraint_index constr_index,
-        unsigned& equal_to_j) {
+                                                                 unsigned& equal_to_j) {
         update_column_type_and_bound(j, kind, right_side, constr_index);
         equal_to_j = null_lpvar;
         if (column_is_fixed(j)) {
             register_in_fixed_var_table(j, equal_to_j);
         }
-
     }
 
     constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq& right_side) {

src/math/lp/lar_solver.h

@@ -86,7 +86,7 @@ class lar_solver : public column_namer {
     constraint_set m_constraints;
     // the set of column indices j such that bounds have changed for j
     u_set m_columns_with_changed_bounds;
-    u_set m_rows_with_changed_bounds;
+    u_set m_touched_rows;
     unsigned_vector m_row_bounds_to_replay;
 
     u_set m_basic_columns_with_changed_cost;
@@ -190,14 +190,12 @@ class lar_solver : public column_namer {
     void substitute_terms_in_linear_expression(const vector<std::pair<mpq, var_index>>& left_side_with_terms,
                                                vector<std::pair<mpq, var_index>>& left_side) const;
 
-    void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j);
     bool use_tableau_costs() const;
     bool tableau_with_costs() const;
     bool costs_are_used() const;
     void change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair<mpq>& delta);
     void update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j);
-    unsigned num_changed_bounds() const { return m_rows_with_changed_bounds.size(); }
+    void add_touched_row(unsigned rid);
-    void insert_row_with_changed_bounds(unsigned rid);
     void detect_rows_with_changed_bounds_for_column(unsigned j);
     void detect_rows_with_changed_bounds();
 
@@ -328,11 +326,11 @@ class lar_solver : public column_namer {
     void activate_check_on_equal(constraint_index, var_index&);
     void activate(constraint_index);
     void random_update(unsigned sz, var_index const* vars);
-    void mark_rows_for_bound_prop(lpvar j);
+    void add_column_rows_to_touched_rows(lpvar j);
     template <typename T>
     void propagate_bounds_for_touched_rows(lp_bound_propagator<T>& bp) {
         unsigned num_prop = 0;
-        for (unsigned i : m_rows_with_changed_bounds) {
+        for (unsigned i : m_touched_rows) {
             num_prop += calculate_implied_bounds_for_row(i, bp);
             if (settings().get_cancel_flag())
                 return;
@@ -342,7 +340,7 @@ class lar_solver : public column_namer {
         // and add fixed columns this way
         if (settings().propagate_eqs()) {
             bp.clear_for_eq();
-            for (unsigned i : m_rows_with_changed_bounds) {
+            for (unsigned i : m_touched_rows) {
                 unsigned offset_eqs = stats().m_offset_eqs;
                 bp.cheap_eq_tree(i);
                 if (settings().get_cancel_flag())
@@ -351,13 +349,13 @@ class lar_solver : public column_namer {
                     m_row_bounds_to_replay.push_back(i);
             }
         }
-        m_rows_with_changed_bounds.clear();
+        m_touched_rows.clear();
     }
 
     template <typename T>
     void check_missed_propagations(lp_bound_propagator<T>& bp) {
         for (unsigned i = 0; i < A_r().row_count(); i++)
-            if (!m_rows_with_changed_bounds.contains(i))
+            if (!m_touched_rows.contains(i))
                 if (0 < calculate_implied_bounds_for_row(i, bp)) {
                     verbose_stream() << i << ": " << get_row(i) << "\n";
                 }
@@ -612,8 +610,8 @@ class lar_solver : public column_namer {
     bool term_is_used_as_row(unsigned term) const;
     bool tighten_term_bounds_by_delta(tv const& t, const impq&);
     lar_solver();
-    void set_track_pivoted_rows(bool v);
+    void track_touched_rows(bool v);
-    bool get_track_pivoted_rows() const;
+    bool touched_rows_are_tracked() const;
     ~lar_solver() override;
     const vector<impq>& r_x() const { return m_mpq_lar_core_solver.m_r_x; }
     bool column_is_int(unsigned j) const;

src/math/lp/lp_core_solver_base.h

@@ -91,7 +91,8 @@ public:
     unsigned              m_basis_sort_counter;
     vector<unsigned>      m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving
     bool                  m_tracing_basis_changes;
-    u_set*                m_pivoted_rows;
+    // these rows are changed by adding to them a multiple of the pivot row
+    u_set*                m_touched_rows;
     bool                  m_look_for_feasible_solution_only;
 
     void start_tracing_basis_changes() {

src/math/lp/lp_core_solver_base_def.h

@@ -58,7 +58,7 @@ lp_core_solver_base(static_matrix<T, X> & A,
     m_upper_bounds(upper_bound_values),
     m_basis_sort_counter(0),
     m_tracing_basis_changes(false),
-    m_pivoted_rows(nullptr),
+    m_touched_rows(nullptr),
     m_look_for_feasible_solution_only(false) {
     lp_assert(bounds_for_boxed_are_set_correctly());    
     init();
@@ -324,8 +324,8 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
         if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
             return false;
         }
-        if (m_pivoted_rows!= nullptr)
+        if (m_touched_rows!= nullptr)
-            m_pivoted_rows->insert(c.var());
+            m_touched_rows->insert(c.var());
     }
 
     if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)

src/sat/smt/arith_solver.cpp

@@ -396,7 +396,7 @@ namespace arith {
             propagate_eqs(b.tv(), ci, k, b, value.get_rational());
 #if 0
         if (propagation_mode() != BP_NONE)
-            lp().mark_rows_for_bound_prop(b.tv().id());
+            lp().add_column_rows_to_touched_rows(b.tv().id());
 #endif
 
     }

src/smt/theory_arith.h

@@ -788,7 +788,7 @@ namespace smt {
         //
         // -----------------------------------
         void mark_row_for_bound_prop(unsigned r1);
-        void mark_rows_for_bound_prop(theory_var v);
+        void add_column_rows_to_touched_rows(theory_var v);
         void is_row_useful_for_bound_prop(row const & r, int & lower_idx, int & upper_idx) const;
         unsigned imply_bound_for_monomial(row const & r, int idx, bool lower);
         unsigned imply_bound_for_all_monomials(row const & r, bool lower);

src/smt/theory_arith_core.h

@@ -2486,7 +2486,7 @@ namespace smt {
         set_bound(b, false);
 
         if (propagation_mode() != bound_prop_mode::BP_NONE)
-            mark_rows_for_bound_prop(v);
+            add_column_rows_to_touched_rows(v);
 
         return true;
     }
@@ -2534,7 +2534,7 @@ namespace smt {
         set_bound(b, true);
 
         if (propagation_mode() != bound_prop_mode::BP_NONE)
-            mark_rows_for_bound_prop(v);
+            add_column_rows_to_touched_rows(v);
 
         return true;
     }
@@ -2603,7 +2603,7 @@ namespace smt {
        \brief Mark all rows that contain v for bound propagation.
     */
     template<typename Ext>
-    void theory_arith<Ext>::mark_rows_for_bound_prop(theory_var v) {
+    void theory_arith<Ext>::add_column_rows_to_touched_rows(theory_var v) {
         for (col_entry const& ce : m_columns[v]) {
             if (!ce.is_dead())
                 mark_row_for_bound_prop(ce.m_row_id);

src/smt/theory_lra.cpp

@@ -2989,7 +2989,7 @@ public:
         }
 #if 0
         if (should_propagate())
-            lp().mark_rows_for_bound_prop(b.tv().id());
+            lp().add_column_rows_to_touched_rows(b.tv().id());
 #endif
     }