debug cheap_eqs

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/bound_analyzer_on_row.h

@@ -330,7 +330,9 @@ private:
     }
 
     void analyze_eq() {
-        m_bp.try_create_eq(m_row_index);
+        if (m_bp.lp().settings().cheap_eqs()) {
+            m_bp.try_create_eq(m_row_index);
+        }
     }
 
 };

src/math/lp/int_gcd_test.cpp

@@ -26,7 +26,7 @@ namespace lp {
 
     bool int_gcd_test::should_apply() {
 
-        if (!lia.settings().m_int_run_gcd_test)
+        if (!lia.settings().int_run_gcd_test())
             return false;
 #if 1
         return true;

src/math/lp/int_solver.cpp

@@ -152,9 +152,6 @@ lia_move int_solver::check(lp::explanation * e) {
 
     check_return_helper pc(lra);
 
-    if (settings().m_int_pivot_fixed_vars_from_basis)
-        lra.pivot_fixed_vars_from_basis();
-
     ++m_number_of_calls;
     if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher();
     if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)();
@@ -271,7 +268,7 @@ bool int_solver::should_gomory_cut() {
 }
 
 bool int_solver::should_hnf_cut() {
-    return settings().m_enable_hnf && m_number_of_calls % m_hnf_cut_period == 0;
+    return settings().enable_hnf() && m_number_of_calls % m_hnf_cut_period == 0;
 }
 
 lia_move int_solver::hnf_cut() {

src/math/lp/lar_solver.cpp

@@ -767,7 +767,7 @@ void lar_solver::solve_with_core_solver() {
         update_x_and_inf_costs_for_columns_with_changed_bounds();
     m_mpq_lar_core_solver.solve();
     set_status(m_mpq_lar_core_solver.m_r_solver.get_status());
-    lp_assert((((m_settings.m_counter_for_debug++) % 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold());
+    lp_assert((((lp_settings::ddd++) % 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold());
 }
 
     
@@ -1188,7 +1188,7 @@ std::string lar_solver::get_variable_name(var_index j) const {
     if (!s.empty()) {
         return s;
     }
-    if (m_settings.m_print_external_var_name) {
+    if (m_settings.print_external_var_name()) {
         return std::string("j") + T_to_string(m_var_register.local_to_external(j));
     }
     else {

src/math/lp/lp_bound_propagator.h

@@ -62,12 +62,20 @@ class lp_bound_propagator {
     hashtable<unsigned, u_hash, u_eq>         m_visited_rows;
     hashtable<unsigned, u_hash, u_eq>         m_visited_columns;
     vector<vertex>                            m_vertices;
-    map<impq, lpvar, obj_hash<impq>, impq_eq> m_offsets_to_verts;
+    map<impq, lpvar, obj_hash<impq>, impq_eq> m_offset_to_verts;
     // these maps map a column index to the corresponding index in ibounds
     std::unordered_map<unsigned, unsigned>    m_improved_lower_bounds;
     std::unordered_map<unsigned, unsigned>    m_improved_upper_bounds;
     T&                                        m_imp;
     impq                                      m_zero;
+    typedef std::pair<unsigned, unsigned> upair;
+    struct uphash {
+        unsigned operator()(const upair& p) const { return combine_hash(p.first, p.second); }
+    };
+    struct upeq {
+        unsigned operator()(const upair& p, const upair& q) const { return p == q; }
+    };
+    hashtable<upair, uphash, upeq>  m_reported_pairs; // contain the pairs of columns (first < second)
 public:
     vector<implied_bound> m_ibounds;
     lp_bound_propagator(T& imp): m_imp(imp), m_zero(impq(0)) {}
@@ -154,7 +162,7 @@ public:
     bool is_offset_row(unsigned row_index,
                        unsigned & x_index,
                        lpvar & y_index,
-                       impq& offset) const {
+                       impq& offset) {
         x_index = y_index = UINT_MAX;
         const auto & row = lp().get_row(row_index);
         for (unsigned k = 0; k < row.size(); k++) {
@@ -176,27 +184,31 @@ public:
                 continue;
             offset += c.coeff() * lp().get_lower_bound(c.var());
         }
+        if (offset.is_zero()) {
+            lp::explanation ex;
+            explain_fixed_in_row(row_index, ex);
+            add_eq_on_columns(ex, row[x_index].var(), row[y_index].var());
+        }
         return true;
     }    
     
     void check_for_eq_and_add_to_offset_table(const vertex& v) {
         unsigned k; // the other vertex index
-        if (m_offsets_to_verts.find(v.offset(), k)) {
+        if (m_offset_to_verts.find(v.offset(), k)) {
-            if (k != v.id())
+            if (column(m_vertices[k]) != column(v))
                 report_eq(k, v.id());
         } else {
             TRACE("cheap_eq", tout << "registered offset " << v.offset() << " to " << v.id() << "\n";);
-            m_offsets_to_verts.insert(v.offset(), v.id());
+            m_offset_to_verts.insert(v.offset(), v.id());
         }
             
     }
 
     void clear_for_eq() {
-        // todo: do not clear the first two?
+        //        m_visited_rows.reset();
-        m_visited_rows.reset();
+        //        m_visited_columns.reset();
-        m_visited_columns.reset();
         m_vertices.reset();
-        m_offsets_to_verts.reset();
+        m_offset_to_verts.reset();
     }
 
     // we have v_i and v_j, indices of vertices at the same offsets
@@ -204,42 +216,40 @@ public:
         SASSERT(v_i != v_j);
         TRACE("cheap_eq", tout << "v_i = " << v_i << ", v_j = " << v_j << "\nu = ";
               m_vertices[v_i].print(tout) << "\nv = "; m_vertices[v_j].print(tout) <<"\n";);
+        
         svector<unsigned> path;
         find_path_on_tree(path, v_i, v_j);
         TRACE("cheap_eq", tout << "path = \n";
-              display_row_of_vertex(v_i, tout);
               for (unsigned k : path) {
                   display_row_of_vertex(k, tout);
-              }
+              });
-              display_row_of_vertex(v_j, tout);
+        lp::explanation exp = get_explanation_from_path(path);
-              );
+        add_eq_on_columns(exp, column(m_vertices[v_i]), column(m_vertices[v_j]));
-        lp::explanation exp = get_explanation_from_path(v_i, path, v_j);
+    }
-        lpvar v_i_col = get_column(m_vertices[v_i]);
+
-        lpvar v_j_col = get_column(m_vertices[v_j]);
+    void add_eq_on_columns(const explanation& exp, lpvar v_i_col, lpvar v_j_col) {
+        SASSERT(v_i_col != v_j_col);
         if (lp().column_is_int(v_i_col) != lp().column_is_int(v_j_col))
             return;
+        upair p = v_i_col < v_j_col? upair(v_i_col, v_j_col) :upair(v_j_col, v_i_col);
+        if (m_reported_pairs.contains(p))
+            return;
+        m_reported_pairs.insert(p);
         unsigned i_e = lp().column_to_reported_index(v_i_col);
         unsigned j_e = lp().column_to_reported_index(v_j_col);
+        TRACE("cheap_eq", tout << "reporting eq " << i_e << ", " << j_e << "\n";);
         m_imp.add_eq(i_e, j_e, exp);        
     }
     
-    explanation get_explanation_from_path(unsigned v_i,
+    explanation get_explanation_from_path(const svector<unsigned>& path) const {
-                                          const svector<unsigned>& path,
-                                          unsigned v_j) const {
         explanation ex;
-        unsigned row = m_vertices[v_i].row();
+        unsigned prev_row = UINT_MAX;
-        unsigned prev_row = row;
-        explain_fixed_in_row(row, ex);
         for (unsigned k : path) {
-            row = m_vertices[k].row();
+            unsigned row = m_vertices[k].row();
             if (row == prev_row)
                 continue;
-            prev_row = row;
+            explain_fixed_in_row(prev_row = row, ex);
-            explain_fixed_in_row(row, ex);
         }
-        row = m_vertices[v_j].row();
-        if (prev_row != row)
-            explain_fixed_in_row(row, ex);
         return ex;
     }
 
@@ -259,10 +269,12 @@ public:
         m_vertices[k].print(out);
         return lp().get_int_solver()->display_row_info(out,m_vertices[k].row() );
     }
-    // the path will not include the start and the end
+
     void find_path_on_tree(svector<unsigned> & path, unsigned u_i, unsigned v_i) const {
         const vertex* u = &m_vertices[u_i];
         const vertex* v = &m_vertices[v_i];
+        path.push_back(u->id());
+        path.push_back(v->id());
         // equalize the levels
         while (u->level() > v->level()) {
             u = &m_vertices[u->parent()];
@@ -326,11 +338,13 @@ public:
         }
         return out;
     }
-    lpvar get_column(const vertex& v) const {
+    lpvar column(const vertex& v) const {
         return lp().get_row(v.row())[v.index_in_row()].var();
     }
 
     void try_create_eq(unsigned row_index) {        
+        if (m_visited_rows.contains(row_index))
+            return;
         TRACE("cheap_eq", tout << "row_index = " << row_index << "\n";);
         clear_for_eq();
         unsigned x_index, y_index;
@@ -350,7 +364,7 @@ public:
     }
         
     void go_over_vertex_column(vertex & v) {
-        lpvar j = get_column(v);
+        lpvar j = column(v);
         if (m_visited_columns.contains(j))
             return;
         m_visited_columns.insert(j);

src/math/lp/lp_settings.h

@@ -142,6 +142,10 @@ private:
     random_gen                m_rand;
 
 public:
+    bool enable_hnf() const { return m_enable_hnf; }
+    bool& enable_hnf() { return m_enable_hnf; } 
+    bool int_run_gcd_test() const { return m_int_run_gcd_test; }
+    bool& int_run_gcd_test() { return m_int_run_gcd_test; }
     unsigned      reps_in_scaler;
     // when the absolute value of an element is less than pivot_epsilon
     // in pivoting, we treat it as a zero
@@ -194,18 +198,19 @@ public:
     unsigned         m_int_find_cube_period;
 private:
     unsigned         m_hnf_cut_period;
-public:
     bool             m_int_run_gcd_test;
-    bool             m_int_pivot_fixed_vars_from_basis;
+public:
     unsigned         limit_on_rows_for_hnf_cutter;
     unsigned         limit_on_columns_for_hnf_cutter;
+private:
     bool             m_enable_hnf;
     bool             m_print_external_var_name;
-#ifdef Z3DEBUG
+    bool             m_cheap_eqs;
-    unsigned         m_counter_for_debug;
+public:
-#endif
+    bool print_external_var_name() const { return m_print_external_var_name; }
-
+    bool& print_external_var_name() { return m_print_external_var_name; }
-
+    bool cheap_eqs() const { return m_cheap_eqs;}
+    bool& cheap_eqs() { return m_cheap_eqs;}
     unsigned hnf_cut_period() const { return m_hnf_cut_period; }
     void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period;  }
     unsigned random_next() { return m_rand(); }
@@ -267,14 +272,11 @@ public:
                     m_int_find_cube_period(4),
                     m_hnf_cut_period(4),
                     m_int_run_gcd_test(true),
-                    m_int_pivot_fixed_vars_from_basis(false),
                     limit_on_rows_for_hnf_cutter(75),
                     limit_on_columns_for_hnf_cutter(150),
                     m_enable_hnf(true),
                     m_print_external_var_name(false)
-#ifdef Z3DEBUG
+                    
-                  , m_counter_for_debug(0)
-#endif
     {}
 
     void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }

src/math/lp/lp_solver_def.h

@@ -29,7 +29,7 @@ template <typename T, typename X> column_info<T> * lp_solver<T, X>::get_or_creat
 
 template <typename T, typename X>
 std::string lp_solver<T, X>::get_variable_name(unsigned j) const { // j here is the core solver index
-    if (!m_settings.m_print_external_var_name)
+    if (!m_settings.print_external_var_name())
         return std::string("j")+T_to_string(j);
     auto it = this->m_core_solver_columns_to_external_columns.find(j);
     if (it == this->m_core_solver_columns_to_external_columns.end())

src/math/lp/nla_core.cpp

@@ -171,7 +171,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
     bool first = true;
     for (lpvar v : m) {
         if (!first) out << "*"; else first = false;
-        if (lp_settings().m_print_external_var_name)
+        if (lp_settings().print_external_var_name())
             out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")";
         else
             out << "(j" << v << " = " << val(v) << ")";
@@ -217,7 +217,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
 }
 
 std::ostream& core::print_monic(const monic& m, std::ostream& out) const {
-    if (lp_settings().m_print_external_var_name)
+    if (lp_settings().print_external_var_name())
         out << "([" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
     else 
         out << "(j" << m.var() << " = " << val(m.var()) << " = ";

src/smt/params/smt_params_helper.pyg

@@ -41,6 +41,7 @@ def_module_params(module_name='smt',
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
+                          ('arith.cheap_eqs', BOOL, True, 'true for extracting cheap equalities'),
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
                           ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'),

src/smt/theory_lra.cpp

@@ -344,8 +344,8 @@ class theory_lra::imp {
         lp().settings().set_resource_limit(m_resource_limit);
         lp().settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lpar.arith_simplex_strategy());
         lp().settings().bound_propagation() = BP_NONE != propagation_mode();
-        lp().settings().m_enable_hnf = lpar.arith_enable_hnf();
+        lp().settings().enable_hnf() = lpar.arith_enable_hnf();
-        lp().settings().m_print_external_var_name = lpar.arith_print_ext_var_names();
+        lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names();
         lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows());
         lp().settings().report_frequency = lpar.arith_rep_freq();
         lp().settings().print_statistics = lpar.arith_print_stats();
@@ -354,7 +354,7 @@ class theory_lra::imp {
         unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
         lp().set_cut_strategy(branch_cut_ratio);
         
-        lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
+        lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
         lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
         m_lia = alloc(lp::int_solver, *m_solver.get());
         get_one(true);
@@ -985,17 +985,18 @@ public:
         lp().settings().set_resource_limit(m_resource_limit);
         lp().settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lpar.arith_simplex_strategy());
         lp().settings().bound_propagation() = BP_NONE != propagation_mode();
-        lp().settings().m_enable_hnf = lpar.arith_enable_hnf();
+        lp().settings().enable_hnf() = lpar.arith_enable_hnf();
-        lp().settings().m_print_external_var_name = lpar.arith_print_ext_var_names();
+        lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names();
         lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows());
         lp().settings().report_frequency = lpar.arith_rep_freq();
         lp().settings().print_statistics = lpar.arith_print_stats();
+        lp().settings().cheap_eqs() = lpar.arith_cheap_eqs();
 
         // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
         unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
         lp().set_cut_strategy(branch_cut_ratio);
         
-        lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
+        lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
         lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
         m_lia = alloc(lp::int_solver, *m_solver.get());
         get_one(true);