throttle the branching in dio

Signed-off-by: Lev Nachmanson <[email protected]>

src/math/lp/dioph_eq.cpp

@@ -77,9 +77,12 @@ namespace lp {
         unsigned size() const {return static_cast<unsigned>(m_map.size());}
 
         void erase_val(unsigned b) {
-            SASSERT(contains(m_rev_map, b) && contains(m_map, m_rev_map[b]));
-            unsigned key = m_rev_map[b];
-            m_rev_map.erase(b);
+            VERIFY(contains(m_rev_map, b) && contains(m_map, m_rev_map[b]));
+            auto it = m_rev_map.find(b);
+            if (it == m_rev_map.end()) return;
+            unsigned key = it->second;
+            m_rev_map.erase(it);
+            VERIFY(has_key(key));
             m_map.erase(key);
         }
         bool has_val(unsigned b) const {
@@ -123,7 +126,7 @@ namespace lp {
         }
         unsigned operator[](unsigned i) const {
             auto it = m_map.find(i);
-            SASSERT(it != m_map.end());
+            VERIFY(it != m_map.end());
             return it->second;
         }
     };
@@ -151,10 +154,10 @@ namespace lp {
         }
 
         void erase_by_second_key(unsigned b) {
-            SASSERT(m_bij.has_val(b));
+            VERIFY(m_bij.has_val(b));
             m_bij.erase_val(b);
             auto it = m_data.find(b);
-            SASSERT(it != m_data.end());
+            VERIFY(it != m_data.end());
             m_data.erase(it);
         }
 
@@ -169,7 +172,7 @@ namespace lp {
         // Get the data by 'b' directly
         const T& get_by_val(unsigned b) const {
             auto it = m_data.find(b);
-            SASSERT(it != m_data.end());
+            VERIFY(it != m_data.end());
             return it->second;
         }
     };
@@ -351,7 +354,7 @@ namespace lp {
 
             const mpq& operator[](unsigned j) const {
                 SASSERT(j >= 0 && j < m_index.size());
-                SASSERT(m_index[j] >= 0 && m_index[j] < m_data.size());
+                SASSERT(m_index[j] >= 0 && m_index[j] < (int)m_data.size());
                 return m_data[m_index[j]].coeff();
             }
 
@@ -470,8 +473,8 @@ namespace lp {
 
 
         unsigned m_conflict_index = -1;  // the row index of the conflict
-        unsigned m_max_number_of_iterations = 100;
-        unsigned m_number_of_iterations;
+        unsigned m_max_of_branching_iterations = 0;
+        unsigned m_number_of_branching_calls;
         struct branch {
             unsigned m_j = UINT_MAX;
             mpq m_rs;
@@ -1084,7 +1087,7 @@ namespace lp {
             m_conflict_index = -1;
             m_infeas_explanation.clear();
             lia.get_term().clear();
-            m_number_of_iterations = 0;
+            m_number_of_branching_calls = 0;
             m_branch_stack.clear();
             m_lra_level = 0;
 
@@ -1182,11 +1185,6 @@ namespace lp {
                 return true;
             }
             // c_g is not integral
-            if (lra.stats().m_dio_calls %
-                lra.settings().dio_branch_from_proof_period() ==
-                0 &&
-                !has_fresh_var(ei))
-                prepare_lia_branch_report(ei, e, g, c_g);
             return false;
         }
 
@@ -1738,8 +1736,8 @@ namespace lp {
         lia_move branching_on_undef() {
             m_explanation_of_branches.clear();
             bool need_create_branch = true;
-            m_number_of_iterations = 0;
-            while (++m_number_of_iterations < m_max_number_of_iterations) {
+            m_number_of_branching_calls = 0;
+            while (++m_number_of_branching_calls < m_max_of_branching_iterations) {
                 lra.stats().m_dio_branch_iterations++;
                 if (need_create_branch) {
                     if (!push_branch()) {
@@ -1954,12 +1952,14 @@ namespace lp {
             if (ret == lia_move::branch || ret == lia_move::conflict)
                 return ret;
             SASSERT(ret == lia_move::undef);
-            ret = branching_on_undef();
+            if (lra.stats().m_dio_calls % lra.settings().dio_branching_period() == 0) {
+                ret = branching_on_undef();
+            }
             if (ret == lia_move::sat || ret == lia_move::conflict) {
                 return ret;
             }
             SASSERT(ret == lia_move::undef);
-            m_max_number_of_iterations = (unsigned)m_max_number_of_iterations/2;
+            m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations/2;
 
             return lia_move::undef;
         }
@@ -1979,8 +1979,7 @@ namespace lp {
             mpq t;
             for (const auto& p : m_e_matrix.m_rows[ei]) {
                 t = abs(p.coeff());
-                if (first || t < ahk ||
-                    (t == ahk && p.var() < k)) {  // the last condition is for debug
+                if (first || t < ahk) {
                     ahk = t;
                     k_sign = p.coeff().is_pos() ? 1 : -1;
                     k = p.var();
@@ -2092,11 +2091,10 @@ namespace lp {
 
                 mpq coeff = m_e_matrix.get_val(c);
                 TRACE("dioph_eq", tout << "before pivot entry :"; print_entry(c.var(), tout) << std::endl;);
-                unsigned c_row = c.var();
                 m_e_matrix.pivot_term_to_row_given_cell(t, c, j, j_sign);
                 TRACE("dioph_eq", tout << "after pivoting c_row:";
-                      print_entry(c_row, tout););
-                SASSERT(entry_invariant(c_row));
+                      print_entry(c.var(), tout););
+                SASSERT(entry_invariant(c.var()));
                 cell_to_process--;
             }
             SASSERT(is_eliminated_from_f(j));

src/math/lp/lp_settings.cpp

@@ -33,5 +33,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     m_simplex_strategy = static_cast<lp::simplex_strategy_enum>(p.arith_simplex_strategy());
     m_nlsat_delay = p.arith_nl_delay();
     m_dio_eqs = p.arith_lp_dio_eqs();
-    m_dio_branch_from_proof_period = p.arith_lp_dio_branch_from_proof_period();
+    m_dio_branching_period = p.arith_lp_dio_branching_period();
 }

src/math/lp/lp_settings.h

@@ -253,7 +253,7 @@ struct lp_settings {
     bool             m_dio_eqs = false;
     bool             m_dio_enable_gomory_cuts = true;
     bool             m_dio_enable_hnf_cuts = true;
-    unsigned         m_dio_branch_from_proof_period = 100; // report rarely
+    unsigned         m_dio_branching_period = 100; //  do branching rarere
 
 public:
     bool print_external_var_name() const { return m_print_external_var_name; }
@@ -263,9 +263,9 @@ struct lp_settings {
     unsigned random_next() { return m_rand(); }
     unsigned random_next(unsigned u ) { return m_rand(u); }
     bool dio_eqs() { return m_dio_eqs; }
-    bool dio_enable_gomory_cuts() { return m_dio_eqs && m_dio_enable_gomory_cuts; }
-    bool dio_enable_hnf_cuts() { return m_dio_eqs && m_dio_enable_hnf_cuts; }
-    unsigned dio_branch_from_proof_period() { return m_dio_branch_from_proof_period; }
+    bool dio_enable_gomory_cuts() const { return m_dio_eqs && m_dio_enable_gomory_cuts; }
+    bool dio_enable_hnf_cuts() const { return m_dio_eqs && m_dio_enable_hnf_cuts; }
+    unsigned dio_branching_period() const { return m_dio_branching_period; }
     void set_random_seed(unsigned s) { m_rand.set_seed(s); }
 
     bool bound_progation() const { 

src/math/lp/static_matrix_def.h

@@ -166,6 +166,7 @@ namespace lp {
             SASSERT(!is_zero(iv.coeff()));
             int j_offs = m_work_vector_of_row_offsets[j];
             if (j_offs == -1) { // it is a new element
+                add_columns_up_to(j);
                 T alv = alpha * iv.coeff();
                 add_new_element(ii, j, alv);
             }

src/smt/params/smt_params_helper.pyg

@@ -58,7 +58,7 @@ def_module_params(module_name='smt',
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('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.lp.dio_eqs', BOOL, True, 'use Diophantine equalities'),
-                          ('arith.lp.dio_branch_from_proof_period', UINT, 100, 'Period of creating a branch instead of a cut'),
+                          ('arith.lp.dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
                           ('arith.lp.dio_cuts_enable_gomory', BOOL, True, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),                          
                           ('arith.lp.dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),                          
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),