add parameter m_dio_calls_period

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

Author: levnach

Diff for: src/math/lp/dioph_eq.cpp

@@ -2333,6 +2333,8 @@ namespace lp {
                 ret = branching_on_undef();
 
             m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations / 2;
+            if (ret == lia_move::undef)
+                lra.settings().dio_calls_period() *= 2;
             return ret;
         }
 

Diff for: src/math/lp/int_solver.cpp

@@ -41,7 +41,6 @@ namespace lp {
         mpq                 m_k;               // the right side of the cut
         hnf_cutter          m_hnf_cutter;
         unsigned            m_hnf_cut_period;
-        unsigned            m_dioph_eq_period;
         dioph_eq            m_dio;  
         int_gcd_test        m_gcd;
 
@@ -51,7 +50,6 @@ namespace lp {
 
         imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_dio(lia), m_gcd(lia) {
             m_hnf_cut_period = settings().hnf_cut_period();
-            m_dioph_eq_period = settings().m_dioph_eq_period;
         } 
 
         bool has_lower(unsigned j) const {
@@ -193,7 +191,7 @@ namespace lp {
         }
 
         bool should_solve_dioph_eq() {
-            return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0;
+            return lia.settings().dio_eqs() && (m_number_of_calls % settings().dio_calls_period() == 0);
         }
 
         // HNF

Diff for: src/math/lp/lp_params_helper.pyg

@@ -7,5 +7,6 @@ def_module_params(module_name='lp',
                           ('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
                           ('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
                           ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
+                          ('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
                          ))
 

Diff for: src/math/lp/lp_settings.cpp

@@ -39,4 +39,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();
     m_dio_branching_period = lp_p.dio_branching_period();m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
     m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums();
+    m_dio_calls_period = lp_p.dio_calls_period();
 }

Diff for: src/math/lp/lp_settings.h

@@ -243,7 +243,6 @@ struct lp_settings {
     unsigned         column_number_threshold_for_using_lu_in_lar_solver = 4000;
     unsigned         m_int_gomory_cut_period = 4;
     unsigned         m_int_find_cube_period = 4;
-    unsigned         m_dioph_eq_period = 1;
 private:
     unsigned         m_hnf_cut_period = 4;
     bool             m_int_run_gcd_test = true;
@@ -262,8 +261,11 @@ struct lp_settings {
     unsigned         m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening
     bool             m_dump_bound_lemmas = false;
     bool             m_dio_ignore_big_nums = false;
+    unsigned         m_dio_calls_period = 1;
 
 public:
+    unsigned dio_calls_period() const { return m_dio_calls_period; }
+    unsigned & dio_calls_period() { return m_dio_calls_period; }
     bool print_external_var_name() const { return m_print_external_var_name; }
     bool propagate_eqs() const { return m_propagate_eqs;}
     unsigned hnf_cut_period() const { return m_hnf_cut_period; }