Merge 36a0006f59 into 81f10912ae

src/math/lp/CMakeLists.txt

@@ -43,6 +43,8 @@ z3_add_component(lp
     polynomial
     nlsat
     smt_params
+  PYG_FILES
+    lp_params_helper.pyg
 )
 
 include_directories(${src_SOURCE_DIR})

src/math/lp/dioph_eq.cpp

@@ -343,7 +343,10 @@ namespace lp {
             return out;
         }
 
-        bool m_has_non_integral_term = false;
+        // the maximal size of the term to try to tighten the bounds:
+        // if the size of the term is large than the chances are that the GCD of the coefficients is one
+        unsigned m_tighten_size_max = 10;
+        bool m_some_terms_are_ignored = false;
         std_vector<mpq> m_sum_of_fixed;
         // we have to use m_var_register because of the fresh variables: otherwise they clash with the existing lar_solver column indices
         var_register m_var_register;
@@ -360,8 +363,9 @@ namespace lp {
         // set S - iterate over bijection m_k2s
         mpq m_c;  // the constant of the equation
         struct term_with_index {
-            // The invariant is that m_index[m_data[k].var()] = k, for each 0 <= k < m_data.size(),
-            // and m_index[j] = -1, or m_tmp[m_index[j]].var() = j, for every 0 <= j < m_index.size().
+            // The invariant is
+            // 1)  m_index[m_data[k].var()] = k, for each 0 <= k < m_data.size(), and
+            // 2)  m_index[j] = -1, or m_data[m_index[j]].var() = j, for every 0 <= j < m_index.size().
             // For example m_data = [(coeff, 5), (coeff, 3)]
             // then m_index = [-1,-1, -1, 1, -1, 0, -1, ....].
             std_vector<iv> m_data;
@@ -375,6 +379,8 @@ namespace lp {
                 return r;
             }
 
+            auto size() const { return m_data.size(); }
+            
             bool has(unsigned k) const {
                 return k < m_index.size() && m_index[k] >= 0;
             }
@@ -498,9 +504,9 @@ namespace lp {
         std::unordered_map<unsigned, std_vector<unsigned>> m_row2fresh_defs;
 
         indexed_uint_set m_changed_rows;
-        // m_changed_columns are the columns that just became fixed, or those that just stopped being fixed.
+        // m_changed_f_columns are the columns that just became fixed, or those that just stopped being fixed.
         // If such a column appears in an entry it has to be recalculated.
-        indexed_uint_set m_changed_columns;
+        indexed_uint_set m_changed_f_columns;
         indexed_uint_set m_changed_terms; // represented by term columns
         indexed_uint_set m_terms_to_tighten; // represented by term columns
         // m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j
@@ -596,34 +602,61 @@ namespace lp {
         };
 
         struct protected_queue {
-            std::queue<unsigned> m_q;
-            indexed_uint_set m_in_q;
+            std::list<unsigned> m_q;
+            std::unordered_map<unsigned, std::list<unsigned>::iterator> m_positions;
+
             bool empty() const {
                 return m_q.empty();
             }
 
             unsigned size() const {
-                return (unsigned)m_q.size();
+                return static_cast<unsigned>(m_q.size());
             }
 
             void push(unsigned j) {
-                if (m_in_q.contains(j)) return;
-                m_in_q.insert(j);
-                m_q.push(j);
+                if (m_positions.find(j) != m_positions.end()) return;
+                m_q.push_back(j);
+                m_positions[j] = std::prev(m_q.end());
             }
 
             unsigned pop_front() {
                 unsigned j = m_q.front();
-                m_q.pop();
-                SASSERT(m_in_q.contains(j));
-                m_in_q.remove(j);
+                m_q.pop_front();
+                m_positions.erase(j);
                 return j;
             }
 
+            void remove(unsigned j) {
+                auto it = m_positions.find(j);
+                if (it != m_positions.end()) {
+                    m_q.erase(it->second);
+                    m_positions.erase(it);
+                }
+                SASSERT(invariant());
+            }
+
+            bool contains(unsigned j) const {
+                return m_positions.find(j) != m_positions.end();
+            }
+
             void reset() {
-                while (!m_q.empty())
-                    m_q.pop();
-                m_in_q.reset();
+                m_q.clear();
+                m_positions.clear();
+            }
+            // Invariant method to ensure m_q and m_positions are aligned
+            bool invariant() const {
+                if (m_q.size() != m_positions.size())
+                    return false;
+
+                for (auto it = m_q.begin(); it != m_q.end(); ++it) {
+                    auto pos_it = m_positions.find(*it);
+                    if (pos_it == m_positions.end())
+                        return false;
+                    if (pos_it->second != it)
+                        return false;
+                }
+
+                return true;
             }
         };
 
@@ -743,28 +776,36 @@ namespace lp {
 
         void add_changed_column(unsigned j) {
             TRACE("dio", lra.print_column_info(j, tout););
-            m_changed_columns.insert(j);
+            m_changed_f_columns.insert(j);
         }
         std_vector<const lar_term*> m_added_terms;
         std::unordered_set<const lar_term*> m_active_terms;
         std_vector<variable_branch_stats> m_branch_stats;
         std_vector<branch> m_branch_stack;
         std_vector<constraint_index> m_explanation_of_branches;
+        // it is a non-const function : it can set m_some_terms_are_ignored to true
+        bool term_has_big_number(const lar_term& t) {
+            for (const auto& p : t) {
+                if (p.coeff().is_big() || (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big())) {
+                    m_some_terms_are_ignored = true;
+                    return true;
+                }
+            }
+            return false;
+        }
+
+        bool ignore_big_nums() const { return lra.settings().dio_ignore_big_nums(); }
+
+        // we add all terms, even those with big numbers, but we might choose to non process the latter.
         void add_term_callback(const lar_term* t) {
             unsigned j = t->j();
             TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;);
             if (!lra.column_is_int(j)) {
                 TRACE("dio", tout << "ignored a non-integral column" << std::endl;);
-                m_has_non_integral_term = true;
+                m_some_terms_are_ignored = true;
                 return;
             }
-
             CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;);
-
-            if (!lia.column_is_int(t->j())) {
-                TRACE("dio", tout << "not all vars are integrall\n";);
-                return;
-            }
             m_added_terms.push_back(t);
             mark_term_change(t->j());
             auto undo = undo_add_term(*this, t);
@@ -784,7 +825,7 @@ namespace lp {
             if (!lra.column_is_fixed(j))
                 return;
             TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout););
-            m_changed_columns.insert(j);
+            m_changed_f_columns.insert(j);
             lra.trail().push(undo_fixed_column(*this, j));
         }
 
@@ -812,7 +853,7 @@ namespace lp {
         }
 
         void register_columns_to_term(const lar_term& t) {
-            TRACE("dio_reg", tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;);
+            CTRACE("dio_reg", t.j() == 1337, tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;);
             for (const auto& p : t.ext_coeffs()) {
                 auto it = m_columns_to_terms.find(p.var());
                 TRACE("dio_reg", tout << "register p.var():" << p.var() << "->" << t.j() << std::endl;);
@@ -854,7 +895,7 @@ namespace lp {
             }
             subs_entry(entry_index);
             SASSERT(entry_invariant(entry_index));
-            TRACE("dio", print_entry(entry_index, tout) << std::endl;);
+            TRACE("dio_entry", print_entry(entry_index, tout) << std::endl;);
         }
         void subs_entry(unsigned ei) {
             if (ei >= m_e_matrix.row_count()) return;
@@ -965,7 +1006,7 @@ namespace lp {
         }
 
         void find_changed_terms_and_more_changed_rows() {
-            for (unsigned j : m_changed_columns) {
+            for (unsigned j : m_changed_f_columns) {
                 const auto it = m_columns_to_terms.find(j);
                 if (it != m_columns_to_terms.end())
                     for (unsigned k : it->second) {
@@ -1013,15 +1054,28 @@ namespace lp {
             }
         }
 
-        void process_changed_columns(std_vector<unsigned> &f_vector) {
+        // this is a non-const function - it can set m_some_terms_are_ignored to true
+        bool is_big_term_or_no_term(unsigned j) {
+            return
+                j >= lra.column_count()
+                ||
+                !lra.column_has_term(j)
+                ||
+                (ignore_big_nums() && term_has_big_number(lra.get_term(j)));
+        }
+ 
+// Processes columns that have changed due to variables becoming fixed/unfixed or terms being updated.
+// It identifies affected terms and rows, recalculates entries, removes irrelevant fresh definitions,
+// and ensures substituted variables are properly eliminated from changed F entries, m_e_matrix.
+// The function maintains internal consistency of data structures after these updates.
+     void process_m_changed_f_columns(std_vector<unsigned> &f_vector) {
             find_changed_terms_and_more_changed_rows();
             for (unsigned j: m_changed_terms) {
-                m_terms_to_tighten.insert(j);
-                if (j < m_l_matrix.column_count()) {
-                    for (const auto& cs : m_l_matrix.column(j)) {
-                        m_changed_rows.insert(cs.var());
-                    }
-                }
+                if (!is_big_term_or_no_term(j))
+                    m_terms_to_tighten.insert(j);
+                if (j < m_l_matrix.column_count())
+                    for (const auto& cs : m_l_matrix.column(j)) 
+                        m_changed_rows.insert(cs.var());                
             }
 
             // find more entries to recalculate
@@ -1031,39 +1085,34 @@ namespace lp {
                 if (it == m_row2fresh_defs.end()) continue;
                 for (unsigned xt : it->second) {
                     SASSERT(var_is_fresh(xt));
-                    for (const auto& p : m_e_matrix.m_columns[xt]) {
+                    for (const auto& p : m_e_matrix.m_columns[xt])
                         more_changed_rows.push_back(p.var());
-                    }
                 }
             }
 
-            for (unsigned ei : more_changed_rows) {
+            for (unsigned ei : more_changed_rows)
                 m_changed_rows.insert(ei);
-            }
-
+            
             for (unsigned ei : m_changed_rows) {
                 if (ei >= m_e_matrix.row_count())
                     continue;
                 if (belongs_to_s(ei))
                     f_vector.push_back(ei);
+
                 recalculate_entry(ei);
                 
                 if (m_e_matrix.m_columns.back().size() == 0) {
                     m_e_matrix.m_columns.pop_back();
                     m_var_register.shrink(m_e_matrix.column_count());
                 }
-                if (m_l_matrix.m_columns.back().size() == 0) {
+                if (m_l_matrix.m_columns.back().size() == 0)
                     m_l_matrix.m_columns.pop_back();
-                }
             }
-
             remove_irrelevant_fresh_defs();
-
             eliminate_substituted_in_changed_rows();
-            m_changed_columns.reset();
+            m_changed_f_columns.reset();
             m_changed_rows.reset();
             m_changed_terms.reset();
-            SASSERT(entries_are_ok());
         }
 
         int get_sign_in_e_row(unsigned ei, unsigned j) const {
@@ -1131,7 +1180,7 @@ namespace lp {
             m_lra_level = 0;
             reset_conflict();
 
-            process_changed_columns(f_vector);
+            process_m_changed_f_columns(f_vector);
             for (const lar_term* t : m_added_terms) {
                 m_active_terms.insert(t);
                 f_vector.push_back(m_e_matrix.row_count()); // going to add a row in fill_entry
@@ -1295,6 +1344,59 @@ namespace lp {
         bool is_substituted_by_fresh(unsigned k) const {
             return m_fresh_k2xt_terms.has_key(k);
         }
+
+        // find a variable in q, not neccessarily at the beginning of the queue, that when substituted would create the minimal
+        // number of non-zeroes
+        unsigned find_var_to_substitute_on_espace(protected_queue& q) {
+            // go over all q elements j
+            // say j is substituted by entry ei = m_k2s[j]
+            // count the number of variables i in m_e_matrix[ei] that m_espace does not contain i,
+            // and choose ei where this number is minimal
+            
+            unsigned best_var = UINT_MAX;
+            size_t min_new_vars = std::numeric_limits<size_t>::max();
+            unsigned num_candidates = 0;
+            std::vector<unsigned> to_remove;
+            for (unsigned j : q.m_q) {
+                size_t new_vars = 0;
+                if (!m_espace.has(j)) {
+                    to_remove.push_back(j);
+                    continue;
+                }
+                if (m_k2s.has_key(j)) {
+                    unsigned ei = m_k2s[j]; // entry index for substitution
+                    for (const auto& p : m_e_matrix.m_rows[ei])
+                        if (p.var() != j && !m_espace.has(p.var()))
+                            ++new_vars;
+                }
+                else if (m_fresh_k2xt_terms.has_key(j)) {
+                    const lar_term& fresh_term = m_fresh_k2xt_terms.get_by_key(j).first;
+                    for (const auto& p : fresh_term)
+                        if (p.var() != j && !m_espace.has(p.var()))
+                            ++new_vars;
+                }
+                if (new_vars < min_new_vars) {
+                    min_new_vars = new_vars;
+                    best_var = j;
+                    num_candidates = 1;
+                }
+                else if (new_vars == min_new_vars) {
+                    ++num_candidates;
+                    if ((lra.settings().random_next() % num_candidates) == 0)
+                        best_var = j;
+                }
+            }
+
+            if (best_var != UINT_MAX)
+                q.remove(best_var);
+
+            for (unsigned j: to_remove)
+                q.remove(j);
+            
+            
+            return best_var;
+        }
+        
         // The term giving the substitution is in form (+-)x_k + sum {a_i*x_i} + c = 0.
         // We substitute x_k in t by (+-)coeff*(sum {a_i*x_i} + c), where coeff is
         // the coefficient of x_k in t.
@@ -1303,11 +1405,11 @@ namespace lp {
             auto r = tighten_on_espace(j);
             if (r == lia_move::conflict)
                 return lia_move::conflict;
-            unsigned k = q.pop_front();
-            if (!m_espace.has(k))
-                return lia_move::undef;            
+            unsigned k = find_var_to_substitute_on_espace(q);
+            if (k == UINT_MAX)
+                return lia_move::undef;
+            SASSERT(m_espace.has(k));
             // we might substitute with a term from S or a fresh term
-
             SASSERT(can_substitute(k));
             lia_move ret;
             if (is_substituted_by_fresh(k)) 
@@ -1385,7 +1487,7 @@ namespace lp {
         
         lia_move subs_with_S_and_fresh(protected_queue& q, unsigned j) {
             lia_move r = lia_move::undef;
-            while (!q.empty() && r != lia_move::conflict) {
+            while (!q.empty() && r != lia_move::conflict && m_espace.size() <= m_tighten_size_max) {
                 lia_move ret = subs_front_with_S_and_fresh(q, j);
                 r = join(ret, r);
             }
@@ -1436,8 +1538,13 @@ namespace lp {
                   // print_bounds(tout);
             );
             for (unsigned j : sorted_changed_terms) {
-                m_terms_to_tighten.remove(j);
+                if (is_big_term_or_no_term(j)) {
+                    m_terms_to_tighten.remove(j);
+                    continue;
+                }
                 auto ret = tighten_bounds_for_term_column(j);
+                m_terms_to_tighten.remove(j);
+                                
                 r = join(ret, r);
                 if (r == lia_move::conflict)
                     break;
@@ -1459,25 +1566,37 @@ namespace lp {
 
         // We will have lar_t, and let j is lar_t.j(), the term column. 
         // In the m_espace we have lar_t. The result of open_ml((1*j)) is lar_t - (1, j).
-        // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j()) 
-        void init_substitutions(const lar_term& lar_t, protected_queue& q) {
+        // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j())
+        // return false iff seen a big number and dio_ignore_big_nums() is true
+        bool init_substitutions(const lar_term& lar_t, protected_queue& q) {
             m_espace.clear();
             m_c = mpq(0);
             m_lspace.clear();
             m_lspace.add(mpq(1), lar_t.j());
+            bool ret = true;
             SASSERT(get_extended_term_value(lar_t).is_zero());
             for (const auto& p : lar_t) {
                 if (is_fixed(p.j())) {
-                    m_c += p.coeff() * lia.lower_bound(p.j()).x;
+                    const mpq& b = lia.lower_bound(p.j()).x;
+                    if (ignore_big_nums() && b.is_big()) {
+                        ret = false;
+                        break;
+                    }
+                    m_c += p.coeff() * b;
                 }
                 else {
                     unsigned lj = lar_solver_to_local(p.j());
+                    if (ignore_big_nums() && p.coeff().is_big()) {
+                        ret = false;
+                        break;
+                    }
                     m_espace.add(p.coeff(), lj);;
                     if (can_substitute(lj))
                         q.push(lj);
                 }
             }
             SASSERT(subs_invariant(lar_t.j()));
+            return ret;
         }
 
         unsigned lar_solver_to_local(unsigned j) const {
@@ -1499,8 +1618,6 @@ namespace lp {
         
         lia_move tighten_on_espace(unsigned j) {
             mpq g = gcd_of_coeffs(m_espace.m_data, true);
-            TRACE("dio", tout << "after process_q_with_S\nt:";  print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
-            
             if (g.is_one())
                 return lia_move::undef;
             if (g.is_zero()) {
@@ -1517,7 +1634,7 @@ namespace lp {
             auto r = tighten_bounds_for_non_trivial_gcd(g, j, true);
             if (r == lia_move::undef)
                 r = tighten_bounds_for_non_trivial_gcd(g, j, false);
-            if (r == lia_move::undef && m_changed_columns.contains(j))
+            if (r == lia_move::undef && m_changed_f_columns.contains(j))
                 r = lia_move::continue_with_check;            
             return r;
         }
@@ -1533,12 +1650,13 @@ namespace lp {
         lia_move tighten_bounds_for_term_column(unsigned j) {
             // q is the queue of variables that can be substituted in term_to_tighten
             protected_queue q;
-            TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl;
+            TRACE("dio", tout << "j:" << j << " , initial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl;
                   for( const auto& p : lra.get_term(j).ext_coeffs()) {
                       lra.print_column_info(p.var(), tout);
                   }
                 );
-            init_substitutions(lra.get_term(j), q);
+            if (!init_substitutions(lra.get_term(j), q))
+                return lia_move::undef;
          
             TRACE("dio", tout << "t:";
                   tout << "m_espace:";
@@ -1687,30 +1805,23 @@ namespace lp {
             mpq rs;
             bool is_strict = false;
             u_dependency* b_dep = nullptr;
-            SASSERT(!g.is_zero());
+            SASSERT(!g.is_zero() && !g.is_one());
 
             if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) {
-                TRACE("dio", 
-                      tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":"
-                      << rs << std::endl;);
+                TRACE("dio", tout << "x" << j << (is_upper? " <= ":" >= ") << rs << std::endl;);
                 mpq rs_g = (rs - m_c) % g;
-                if (rs_g.is_neg()) {
+                if (rs_g.is_neg())
                     rs_g += g;
-                }
-                if (! (!rs_g.is_neg() && rs_g.is_int())) {
-                    std::cout << "rs:" << rs << "\n";
-                    std::cout << "m_c:" << m_c << "\n";
-                    std::cout << "g:" << g << "\n";
-                    std::cout << "rs_g:" << rs_g << "\n";
-                }
-                SASSERT(rs_g.is_int());
+                
+                SASSERT(rs_g.is_int() && !rs_g.is_neg());
+
                 TRACE("dio", tout << "(rs - m_c) % g:" << rs_g << std::endl;);
                 if (!rs_g.is_zero()) {
                     if (tighten_bound_kind(g, j, rs, rs_g, is_upper))
                         return lia_move::conflict;
-                } else {
-                    TRACE("dio", tout << "no improvement in the bound\n";);
                 }
+                else 
+                    TRACE("dio", tout << "rs_g is zero: no improvement in the bound\n";);
             }
             return lia_move::undef;
         }
@@ -1773,10 +1884,7 @@ namespace lp {
             for (const auto& p: fixed_part_of_the_term) {
                 SASSERT(is_fixed(p.var()));                
                 if (p.coeff().is_int() && (p.coeff() % g).is_zero()) {
-                    // we can skip this dependency
-                    // because the monomial p.coeff()*p.var() is 0 modulo g, and it does not matter that p.var() is fixed.
-                    // We could have added  p.coeff()*p.var() to g*t_, substructed the value of  p.coeff()*p.var() from m_c and
-                    // still get the same result.
+                    // we can skip this dependency as explained above
                     TRACE("dio", tout << "skipped dep:\n"; print_deps(tout, lra.get_bound_constraint_witnesses_for_column(p.var())););
                     continue;
                 }
@@ -1788,7 +1896,6 @@ namespace lp {
             if (lra.settings().get_cancel_flag())
                 return false;
             lra.update_column_type_and_bound(j, kind, bound, dep);
-
             lp_status st = lra.find_feasible_solution();
             if (is_sat(st) || st == lp::lp_status::CANCELLED)
                 return false;
@@ -1852,7 +1959,7 @@ namespace lp {
                     return lia_move::undef;
                 if (r == lia_move::conflict || r == lia_move::undef) 
                     break;
-                SASSERT(m_changed_columns.size() == 0);
+                SASSERT(m_changed_f_columns.size() == 0);
             }
             while (f_vector.size());
 
@@ -2180,11 +2287,12 @@ namespace lp {
         bool is_in_sync() const {
             for (unsigned j = 0; j < m_e_matrix.column_count(); j++) {
                 unsigned external_j = m_var_register.local_to_external(j);
-                if (external_j == UINT_MAX) continue;
-                if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size()) {
-                    // It is OK to have an empty column in m_e_matrix.
+                if (external_j == UINT_MAX)
+                    continue;
+                if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size()) 
                     return false;
-                }
+                // It is OK to have an empty column in m_e_matrix.
+
             }
 
             for (unsigned ei = 0; ei < m_e_matrix.row_count(); ei++) {
@@ -2219,6 +2327,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;
         }
 
@@ -2692,8 +2802,8 @@ namespace lp {
         // needed for the template bound_analyzer_on_row.h
         const lar_solver& lp() const { return lra; }
         lar_solver& lp() {return lra;}
-        bool has_non_integral_term() const {
-            return m_has_non_integral_term;
+        bool some_terms_are_ignored() const {
+            return m_some_terms_are_ignored;
         }
     };
     // Constructor definition
@@ -2712,8 +2822,8 @@ namespace lp {
         m_imp->explain(ex);
     }
 
-    bool dioph_eq::has_non_integral_term() const {
-        return m_imp->has_non_integral_term();
+    bool dioph_eq::some_terms_are_ignored() const {
+        return m_imp->some_terms_are_ignored();
     }
     
 

src/math/lp/dioph_eq.h

@@ -30,6 +30,6 @@ namespace lp {
         ~dioph_eq();
         lia_move check();
         void explain(lp::explanation&);
-        bool has_non_integral_term() const;
+        bool some_terms_are_ignored() const;
     };
 }

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 {
@@ -187,20 +185,19 @@ namespace lp {
         }
 
         bool should_gomory_cut() {
-            bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() ||
-                                      m_dio.has_non_integral_term();
-
+            bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() ||
+                                      m_dio.some_terms_are_ignored();
             return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
         }
 
         bool should_solve_dioph_eq() {
-            return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0;
+            return lia.settings().dio() && (m_number_of_calls % settings().dio_calls_period() == 0);
         }
 
         // HNF
 
         bool should_hnf_cut() {
-            return (!settings().dio_eqs() || settings().dio_enable_hnf_cuts())
+            return (!settings().dio() || settings().dio_enable_hnf_cuts())
                 && settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0;
         }
         
@@ -226,7 +223,7 @@ namespace lp {
         
             lia_move r = lia_move::undef;
 
-            if (m_gcd.should_apply())
+            if (m_gcd.should_apply() || (settings().dio() && m_dio.some_terms_are_ignored()))
                 r = m_gcd();
 
             check_return_helper pc(lra);

src/math/lp/lp_params_helper.pyg

@@ -0,0 +1,13 @@
+def_module_params(module_name='lp',
+                  class_name='lp_params_helper',
+                  description='linear programming parameters',
+                  export=True,
+                  params=(('dio', BOOL, False, 'use Diophantine equalities'),
+                          ('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
+                          ('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, 4, 'Period of calling the Diophantine handler in the final_check()'),
+                          ('dio_run_gcd', BOOL, True, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),                          
+                         ))
+                         

src/math/lp/lp_settings.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#include "math/lp/lp_params_helper.hpp"
 #include <memory>
 #include "util/vector.h"
 #include "smt/params/smt_params_helper.hpp"
@@ -25,6 +26,7 @@ template bool lp::vectors_are_equal<lp::mpq>(vector<lp::mpq > const&, vector<lp:
 
 void lp::lp_settings::updt_params(params_ref const& _p) {
     smt_params_helper p(_p);
+    lp_params_helper lp_p(_p);
     m_enable_hnf = p.arith_enable_hnf();
     m_propagate_eqs = p.arith_propagate_eqs();
     print_statistics = p.arith_print_stats();
@@ -32,9 +34,12 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     report_frequency = p.arith_rep_freq();
     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_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory();
-    m_dio_enable_hnf_cuts = p.arith_lp_dio_cuts_enable_hnf();
-    m_dio_branching_period = p.arith_lp_dio_branching_period();
+    m_dio = lp_p.dio();
+    m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
+    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();
+    m_dio_run_gcd = lp_p.dio_run_gcd();
 }

src/math/lp/lp_settings.h

@@ -218,8 +218,12 @@ public:
     void updt_params(params_ref const& p);
     bool enable_hnf() const { return m_enable_hnf; }
     unsigned nlsat_delay() const { return m_nlsat_delay; }
-    bool int_run_gcd_test() const { return m_int_run_gcd_test; }
-    bool& int_run_gcd_test() { return m_int_run_gcd_test; }
+    bool int_run_gcd_test() const {
+        if (!m_dio)
+            return m_int_run_gcd_test;
+        return m_dio_run_gcd;
+    }
+    void set_run_gcd_test(bool v) { m_int_run_gcd_test = v; }
     unsigned      reps_in_scaler = 20;
     int           c_partial_pivoting = 10; // this is the constant c from page 410
     unsigned      depth_of_rook_search = 4;
@@ -243,7 +247,6 @@ public:
     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;
@@ -255,23 +258,30 @@ private:
     bool             m_enable_hnf = true;
     bool             m_print_external_var_name = false;
     bool             m_propagate_eqs = false;
-    bool             m_dio_eqs = false;
+    bool             m_dio = false;
     bool             m_dio_enable_gomory_cuts = false;
     bool             m_dio_enable_hnf_cuts = true;
     unsigned         m_dio_branching_period = 100; //  do branching rarely
     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 = 4;
+    bool             m_dio_run_gcd = true;
 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; }
     void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period;  }
     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() 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; }
+    bool dio() { return m_dio; }
+    bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; }
+    bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; }
+    bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; }
     unsigned dio_branching_period() const { return m_dio_branching_period; }
+    bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; }
     void set_random_seed(unsigned s) { m_rand.set_seed(s); }
     unsigned dio_report_branch_with_term_tigthening_period() const { return m_dio_report_branch_with_term_tigthening_period; }
     bool bound_progation() const { 

src/sat/smt/arith_solver.cpp

@@ -35,7 +35,7 @@ namespace arith {
         lp().updt_params(ctx.s().params());
         lp().settings().set_resource_limit(m_resource_limit);
         lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode();
-        lp().settings().int_run_gcd_test() = get_config().m_arith_gcd_test;
+        lp().settings().set_run_gcd_test(get_config().m_arith_gcd_test);
         lp().settings().set_random_seed(get_config().m_random_seed);
         
         m_lia = alloc(lp::int_solver, *m_solver.get());

src/smt/params/smt_params_helper.pyg

@@ -57,10 +57,6 @@ def_module_params(module_name='smt',
                           ('bv.solver', UINT, 0, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'),
                           ('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, False, 'use Diophantine equalities'),
-                          ('arith.lp.dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
-                          ('arith.lp.dio_cuts_enable_gomory', BOOL, False, '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'),
                           ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),
                           ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),

src/smt/theory_lra.cpp

@@ -871,7 +871,7 @@ public:
         unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
         lp().set_cut_strategy(branch_cut_ratio);
         
-        lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
+        lp().settings().set_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());
     }