From 4303a1f7fe7691c9f9eeea4b079a7b77387fdf2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 May 2023 09:33:29 +0100 Subject: [PATCH] added div/mod handling Signed-off-by: Nikolaj Bjorner --- src/math/lp/int_solver.cpp | 33 +++++++++++++++++++++------------ src/smt/theory_arith_aux.h | 4 +++- src/smt/theory_arith_core.h | 2 ++ src/smt/theory_arith_int.h | 13 ++++++++++--- src/smt/theory_lra.cpp | 37 ++++++++++++++++++++++++++++++++----- 5 files changed, 68 insertions(+), 21 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 48015471c..099d97f6c 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -49,8 +49,13 @@ namespace lp { continue; patch_nbasic_column(v); } + unsigned num_fixed = 0; + for (unsigned v = 0; v < num; v++) + if (lia.is_fixed(v)) + ++num_fixed; + lp_assert(lia.is_feasible()); - verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << "\n"; + verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n"; //lra.display(verbose_stream()); //exit(0); if (!lia.has_inf_int()) { @@ -72,16 +77,6 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) { bool val_is_int = lia.value_is_int(j); - const auto & A = lra.A_r(); - if (!m_is_one) { - verbose_stream() << "divisor: " << m << "\n"; - lia.display_column(verbose_stream(), j); - for (auto c : A.column(j)) { - unsigned row_index = c.var(); - lia.display_row(verbose_stream(), A.m_rows[row_index]); - verbose_stream() << "\n"; - } - } // check whether value of j is already a multiple of m. if (val_is_int && (m_is_one || (val.x / m).is_int())) { @@ -92,6 +87,19 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) { return; } +#if 0 + const auto & A = lra.A_r(); + if (!m_is_one) { + // lia.display_column(verbose_stream(), j); + for (auto c : A.column(j)) { + continue; + unsigned row_index = c.var(); + lia.display_row(verbose_stream(), A.m_rows[row_index]); + verbose_stream() << "\n"; + } + } +#endif + TRACE("patch_int", tout << "TARGET j" << j << " -> ["; if (inf_l) tout << "-oo"; else tout << l; @@ -126,6 +134,7 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) { lra.set_value_for_nbasic_column(j, l); } else { + verbose_stream() << "fail: " << j << " " << m << "\n"; --m_patch_success; ++m_patch_fail; TRACE("patch_int", tout << "not patching " << l << "\n";); @@ -354,7 +363,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) { // this function assumes that all basic columns dependend on j are feasible bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) { - if (lrac.m_r_heading[j] >= 0) // the basic var + if (lrac.m_r_heading[j] >= 0 || is_fixed(j)) // basic or fixed var return false; TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 5d31f0657..4b244ca88 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -2059,7 +2059,9 @@ namespace smt { bool inf_l, inf_u; inf_numeral l, u; numeral m; - get_freedom_interval(v, inf_l, l, inf_u, u, m); + if (!get_freedom_interval(v, inf_l, l, inf_u, u, m)) + return false; + if (inf_l && inf_u) { inf_numeral new_val = inf_numeral(m_random() % (RANGE + 1)); set_value(v, new_val); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 0eddd1273..513ce6851 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1567,6 +1567,8 @@ namespace smt { m_liberal_final_check = true; m_changed_assignment = false; final_check_status result = final_check_core(); + //display(verbose_stream()); + //exit(0); if (result != FC_DONE) return result; if (!m_changed_assignment) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 911cd2eca..e28113863 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -908,15 +908,21 @@ namespace smt { inf_numeral l, u; numeral m; unsigned num_patched = 0, num_not_patched = 0; - unsigned num_one = 0, num_divides = 0; + unsigned num_one = 0, num_divides = 0, num_fixed = 0; + + for (theory_var v = 0; v < num; v++) + if (is_fixed(v)) + ++num_fixed; + for (theory_var v = 0; v < num; v++) { - if (!is_non_base(v)) + if (!is_non_base(v) || is_fixed(v)) continue; get_freedom_interval(v, inf_l, l, inf_u, u, m); if (m.is_one() && get_value(v).is_int()) { num_one++; continue; } + // check whether value of v is already a multiple of m. if ((get_value(v).get_rational() / m).is_int()) { num_divides++; @@ -952,6 +958,7 @@ namespace smt { } if (!inf_l && !inf_u && l > u) { ++num_not_patched; + verbose_stream() << "fail: " << v << " " << m << "\n"; continue; // cannot patch } ++num_patched; @@ -963,7 +970,7 @@ namespace smt { set_value(v, inf_numeral(0)); } SASSERT(m_to_patch.empty()); - verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << "\n"; + verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << " fixed " << num_fixed << "\n"; //display(verbose_stream()); //exit(0); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9f94df354..9b5a13c22 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -449,6 +449,29 @@ class theory_lra::imp { return v; } + theory_var internalize_mod(app* n) { + TRACE("arith", tout << "internalizing...\n" << mk_pp(n, m) << "\n";); + rational r(1); + theory_var s = mk_binary_op(n); + if (!a.is_numeral(n->get_arg(1), r) || r.is_zero()) + found_underspecified(n); + if (!ctx().relevancy()) + mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1)); + return s; + + } + + theory_var mk_binary_op(app * n) { + SASSERT(n->get_num_args() == 2); + if (ctx().e_internalized(n)) + return mk_var(n); + ctx().internalize(n->get_arg(0), false); + ctx().internalize(n->get_arg(1), false); + enode* e = mk_enode(n); + return mk_var(n); + } + + /** * \brief Internalize the given term and return an alias for it. * Return null_theory_var if the term was not implemented by the theory yet. @@ -472,16 +495,18 @@ class theory_lra::imp { return internalize_numeral(n, val); else if (a.is_mul(n)) return internalize_mul1(n); - else if (a.is_arith_expr(n)) + else if (a.is_mod(n)) + return internalize_mod(n); + else if (a.is_idiv(n)) + return internalize_mod(n); + else if (a.is_arith_expr(n)) { + verbose_stream() << "nyi " << mk_pp(n, m) << "\n"; NOT_IMPLEMENTED_YET(); + } #if 0 else if (a.is_div(n)) return internalize_div(n); - else if (a.is_idiv(n)) - return internalize_idiv(n); - else if (a.is_mod(n)) - return internalize_mod(n); else if (a.is_rem(n)) return internalize_rem(n); else if (a.is_to_real(n)) @@ -1919,6 +1944,8 @@ public: m_changed_assignment = false; ctx().push_trail(value_trail(m_final_check_idx)); final_check_status result = final_check_core(); + //display(verbose_stream()); + //exit(0); if (result != FC_DONE) return result; if (!m_changed_assignment)