From 611c14844d84558e2705be8a4ebe11d37715441a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Mar 2020 16:05:13 +0100 Subject: [PATCH] fix #3194, remove euclidean solver Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 3 +- src/CMakeLists.txt | 1 - src/math/euclid/CMakeLists.txt | 6 - src/math/euclid/README | 2 - src/math/euclid/euclidean_solver.cpp | 862 ------------------------- src/math/euclid/euclidean_solver.h | 102 --- src/smt/CMakeLists.txt | 1 - src/smt/params/smt_params_helper.pyg | 1 - src/smt/params/theory_arith_params.cpp | 2 - src/smt/params/theory_arith_params.h | 5 +- src/smt/theory_arith.h | 6 +- src/smt/theory_arith_int.h | 333 ---------- 12 files changed, 5 insertions(+), 1319 deletions(-) delete mode 100644 src/math/euclid/CMakeLists.txt delete mode 100644 src/math/euclid/README delete mode 100644 src/math/euclid/euclidean_solver.cpp delete mode 100644 src/math/euclid/euclidean_solver.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index dc43dd9ee..d3da0cf37 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -34,7 +34,6 @@ def init_project_def(): add_lib('tactic', ['ast', 'model']) add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution') add_lib('parser_util', ['ast'], 'parsers/util') - add_lib('euclid', ['util'], 'math/euclid') add_lib('proofs', ['rewriter', 'util'], 'ast/proofs') add_lib('solver', ['model', 'tactic', 'proofs']) add_lib('cmd_context', ['solver', 'rewriter']) @@ -52,7 +51,7 @@ def init_project_def(): add_lib('smt_params', ['ast', 'rewriter', 'pattern', 'bit_blaster'], 'smt/params') add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', - 'substitution', 'grobner', 'euclid', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp']) + 'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp']) add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e1ca4984e..46d0411e6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -54,7 +54,6 @@ add_subdirectory(math/grobner) add_subdirectory(sat) add_subdirectory(nlsat) add_subdirectory(math/lp) -add_subdirectory(math/euclid) add_subdirectory(tactic/core) add_subdirectory(math/subpaving/tactic) add_subdirectory(tactic/aig) diff --git a/src/math/euclid/CMakeLists.txt b/src/math/euclid/CMakeLists.txt deleted file mode 100644 index a72f02b28..000000000 --- a/src/math/euclid/CMakeLists.txt +++ /dev/null @@ -1,6 +0,0 @@ -z3_add_component(euclid - SOURCES - euclidean_solver.cpp - COMPONENT_DEPENDENCIES - util -) diff --git a/src/math/euclid/README b/src/math/euclid/README deleted file mode 100644 index 17d408fc9..000000000 --- a/src/math/euclid/README +++ /dev/null @@ -1,2 +0,0 @@ -Basic Euclidean solver for linear integer equations. -This solver generates "explanations". diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp deleted file mode 100644 index 96586a1d6..000000000 --- a/src/math/euclid/euclidean_solver.cpp +++ /dev/null @@ -1,862 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - euclidean_solver.cpp - -Abstract: - - Euclidean Solver with support for explanations. - -Author: - - Leonardo de Moura (leonardo) 2011-07-08. - -Revision History: - ---*/ -#include "math/euclid/euclidean_solver.h" -#include "util/numeral_buffer.h" -#include "util/heap.h" - -struct euclidean_solver::imp { - typedef unsigned var; - typedef unsigned justification; - typedef unsynch_mpq_manager numeral_manager; - typedef numeral_buffer mpz_buffer; - typedef numeral_buffer mpq_buffer; - typedef svector justification_vector; - static const justification null_justification = UINT_MAX; -#define null_var UINT_MAX -#define null_eq_idx UINT_MAX - typedef svector var_vector; - typedef svector mpz_vector; - typedef svector mpq_vector; - - struct elim_order_lt { - unsigned_vector & m_solved; - elim_order_lt(unsigned_vector & s):m_solved(s) {} - bool operator()(var x1, var x2) const { return m_solved[x1] < m_solved[x2]; } - }; - - typedef heap var_queue; // queue used for scheduling variables for applying substitution. - - static unsigned pos(unsigned_vector const & xs, unsigned x_i) { - if (xs.empty()) - return UINT_MAX; - int low = 0; - int high = xs.size() - 1; - while (true) { - int mid = low + ((high - low) / 2); - var x_mid = xs[mid]; - if (x_i > x_mid) { - low = mid + 1; - if (low > high) - return UINT_MAX; - } - else if (x_i < x_mid) { - high = mid - 1; - if (low > high) - return UINT_MAX; - } - else { - return mid; - } - } - } - - - /** - Equation as[0]*xs[0] + ... + as[n-1]*xs[n-1] + c = 0 with justification bs[0]*js[0] + ... + bs[m-1]*js[m-1] - */ - struct equation { - mpz_vector m_as; - var_vector m_xs; - mpz m_c; - // justification - mpq_vector m_bs; - justification_vector m_js; - - unsigned size() const { return m_xs.size(); } - unsigned js_size() const { return m_js.size(); } - var x(unsigned i) const { return m_xs[i]; } - var & x(unsigned i) { return m_xs[i]; } - mpz const & a(unsigned i) const { return m_as[i]; } - mpz & a(unsigned i) { return m_as[i]; } - mpz const & c() const { return m_c; } - mpz & c() { return m_c; } - var j(unsigned i) const { return m_js[i]; } - var & j(unsigned i) { return m_js[i]; } - mpq const & b(unsigned i) const { return m_bs[i]; } - mpq & b(unsigned i) { return m_bs[i]; } - - unsigned pos_x(unsigned x_i) const { return pos(m_xs, x_i); } - }; - - typedef ptr_vector equations; - typedef svector occs; - - numeral_manager * m_manager; - bool m_owns_m; - - equations m_equations; - equations m_solution; - - svector m_parameter; - unsigned_vector m_solved; // null_eq_idx if var is not solved, otherwise the position in m_solution - vector m_occs; // occurrences of the variable in m_equations. - - unsigned m_inconsistent; // null_eq_idx if not inconsistent, otherwise it is the index of an unsatisfiable equality in m_equations. - unsigned m_next_justification; - mpz_buffer m_decompose_buffer; - mpz_buffer m_as_buffer; - mpq_buffer m_bs_buffer; - - var_vector m_tmp_xs; - mpz_buffer m_tmp_as; - mpq_buffer m_tmp_bs; - - var_vector m_norm_xs_vector; - mpz_vector m_norm_as_vector; - mpq_vector m_norm_bs_vector; - - var_queue m_var_queue; - - // next candidate - unsigned m_next_eq; - var m_next_x; - mpz m_next_a; - bool m_next_pos_a; - - numeral_manager & m() const { return *m_manager; } - - bool solved(var x) const { return m_solved[x] != null_eq_idx; } - - template - void sort_core(svector & as, unsigned_vector & xs, numeral_buffer & buffer) { - std::sort(xs.begin(), xs.end()); - unsigned num = as.size(); - for (unsigned i = 0; i < num; i++) { - m().swap(as[i], buffer[xs[i]]); - } - unsigned j = 0; - for (unsigned i = 0; i < num; ++i) { - if (i > 0 && xs[j] == xs[i]) { - m().add(as[j], as[i], as[j]); - continue; - } - if (i != j) { - xs[j] = xs[i]; - m().set(as[j], as[i]); - } - ++j; - } - xs.shrink(j); - as.shrink(j); - } - - template - void sort(svector & as, unsigned_vector & xs, numeral_buffer & buffer) { - unsigned num = as.size(); - for (unsigned i = 0; i < num; i++) { - m().set(buffer[xs[i]], as[i]); - } - sort_core(as, xs, buffer); - } - - equation * mk_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, unsigned num_js, mpq const * bs, justification const * js, - bool sort = true) { - equation * new_eq = alloc(equation); - for (unsigned i = 0; i < num; i++) { - m().set(m_as_buffer[xs[i]], as[i]); - new_eq->m_as.push_back(mpz()); - new_eq->m_xs.push_back(xs[i]); - } - sort_core(new_eq->m_as, new_eq->m_xs, m_as_buffer); - m().set(new_eq->m_c, c); - for (unsigned i = 0; i < num_js; i++) { - m().set(m_bs_buffer[js[i]], bs[i]); - new_eq->m_bs.push_back(mpq()); - new_eq->m_js.push_back(js[i]); - } - if (sort) - sort_core(new_eq->m_bs, new_eq->m_js, m_bs_buffer); - return new_eq; - } - - template - void div(svector & as, mpz const & g) { - unsigned n = as.size(); - for (unsigned i = 0; i < n; i++) - m().div(as[i], g, as[i]); - } - - void normalize_eq(unsigned eq_idx) { - if (inconsistent()) - return; - equation & eq = *(m_equations[eq_idx]); - TRACE("euclidean_solver", tout << "normalizing:\n"; display(tout, eq); tout << "\n";); - unsigned num = eq.size(); - if (num == 0) { - // c == 0 inconsistency - if (!m().is_zero(eq.c())) { - TRACE("euclidean_solver", tout << "c = 0 inconsistency detected\n";); - m_inconsistent = eq_idx; - } - else { - del_eq(&eq); - m_equations[eq_idx] = 0; - } - return; - } - - mpz g; - mpz a; - m().set(g, eq.a(0)); - m().abs(g); - for (unsigned i = 1; i < num; i++) { - if (m().is_one(g)) - break; - m().set(a, eq.a(i)); - m().abs(a); - m().gcd(g, a, g); - } - if (m().is_one(g)) - return; - if (!m().divides(g, eq.c())) { - // g does not divide c - TRACE("euclidean_solver", tout << "gcd inconsistency detected\n";); - m_inconsistent = eq_idx; - return; - } - div(eq.m_as, g); - div(eq.m_bs, g); - m().del(g); - m().del(a); - TRACE("euclidean_solver", tout << "after normalization:\n"; display(tout, eq); tout << "\n";); - } - - bool is_better(mpz const & a, var x, unsigned eq_sz) { - SASSERT(m().is_pos(a)); - if (m_next_x == null_var) - return true; - if (m().lt(a, m_next_a)) - return true; - if (m().lt(m_next_a, a)) - return false; - if (m_occs[x].size() < m_occs[m_next_x].size()) - return true; - if (m_occs[x].size() > m_occs[m_next_x].size()) - return false; - return eq_sz < m_equations[m_next_eq]->size(); - } - - void updt_next_candidate(unsigned eq_idx) { - if (!m_equations[eq_idx]) - return; - mpz abs_a; - equation const & eq = *(m_equations[eq_idx]); - unsigned num = eq.size(); - for (unsigned i = 0; i < num; i++) { - mpz const & a = eq.a(i); - m().set(abs_a, a); - m().abs(abs_a); - if (is_better(abs_a, eq.x(i), num)) { - m().set(m_next_a, abs_a); - m_next_x = eq.x(i); - m_next_eq = eq_idx; - m_next_pos_a = m().is_pos(a); - } - } - m().del(abs_a); - } - - /** - \brief Select next variable to be eliminated. - Return false if there is not variable to eliminate. - - The result is in - m_next_x variable to be eliminated - m_next_eq id of the equation containing x - m_next_a absolute value of the coefficient of x in eq. - m_next_pos_a true if the coefficient of x is positive in eq. - */ - bool select_next_var() { - while (!m_equations.empty() && m_equations.back() == 0) - m_equations.pop_back(); - if (m_equations.empty()) - return false; - SASSERT(!m_equations.empty() && m_equations.back() != 0); - m_next_x = null_var; - unsigned eq_idx = m_equations.size(); - while (eq_idx > 0) { - --eq_idx; - updt_next_candidate(eq_idx); - // stop as soon as possible - // TODO: use heuristics - if (m_next_x != null_var && m().is_one(m_next_a)) - return true; - } - CTRACE("euclidean_solver_bug", m_next_x == null_var, display(tout);); - SASSERT(m_next_x != null_var); - return true; - } - - template - void del_nums(svector & as) { - unsigned sz = as.size(); - for (unsigned i = 0; i < sz; i++) - m().del(as[i]); - as.reset(); - } - - void del_eq(equation * eq) { - m().del(eq->c()); - del_nums(eq->m_as); - del_nums(eq->m_bs); - dealloc(eq); - } - - void del_equations(equations & eqs) { - unsigned sz = eqs.size(); - for (unsigned i = 0; i < sz; i++) { - if (eqs[i]) - del_eq(eqs[i]); - } - } - - /** - \brief Store the "solved" variables in xs into m_var_queue. - */ - void schedule_var_subst(unsigned num, var const * xs) { - for (unsigned i = 0; i < num; i++) { - if (solved(xs[i])) - m_var_queue.insert(xs[i]); - } - } - - void schedule_var_subst(var_vector const & xs) { - schedule_var_subst(xs.size(), xs.c_ptr()); - } - - /** - \brief Store as1*xs1 + k*as2*xs2 into new_as*new_xs - - If UpdateOcc == true, - Then, - 1) for each variable x occurring in xs2 but not in xs1: - - eq_idx is added to m_occs[x] - 2) for each variable that occurs in xs1 and xs2 and the resultant coefficient is zero, - - eq_idx is removed from m_occs[x] IF x != except_var - - If UpdateQueue == true - Then, - 1) for each variable x occurring in xs2 but not in xs1: - - if x is solved, then x is inserted into m_var_queue - 2) for each variable that occurs in xs1 and xs2 and the resultant coefficient is zero, - - if x is solved, then x is removed from m_var_queue - - */ - template - void addmul(svector const & as1, var_vector const & xs1, - mpz const & k, svector const & as2, var_vector const & xs2, - numeral_buffer & new_as, var_vector & new_xs, - unsigned eq_idx = null_eq_idx, var except_var = null_var) { - Numeral new_a; - SASSERT(as1.size() == xs1.size()); - SASSERT(as2.size() == xs2.size()); - new_as.reset(); - new_xs.reset(); - unsigned sz1 = xs1.size(); - unsigned sz2 = xs2.size(); - unsigned i1 = 0; - unsigned i2 = 0; - while (true) { - if (i1 == sz1) { - // copy remaining entries from as2*xs2 - while (i2 < sz2) { - var x2 = xs2[i2]; - if (UpdateOcc) - m_occs[x2].push_back(eq_idx); - if (UpdateQueue && solved(x2)) - m_var_queue.insert(x2); - new_as.push_back(Numeral()); - m().mul(k, as2[i2], new_as.back()); - new_xs.push_back(x2); - i2++; - } - break; - } - if (i2 == sz2) { - // copy remaining entries from as1*xs1 - while (i1 < sz1) { - new_as.push_back(as1[i1]); - new_xs.push_back(xs1[i1]); - i1++; - } - break; - } - var x1 = xs1[i1]; - var x2 = xs2[i2]; - if (x1 < x2) { - new_as.push_back(as1[i1]); - new_xs.push_back(xs1[i1]); - i1++; - } - else if (x1 > x2) { - if (UpdateOcc) - m_occs[x2].push_back(eq_idx); - if (UpdateQueue && solved(x2)) - m_var_queue.insert(x2); - new_as.push_back(Numeral()); - m().mul(k, as2[i2], new_as.back()); - new_xs.push_back(x2); - i2++; - } - else { - m().addmul(as1[i1], k, as2[i2], new_a); - TRACE("euclidean_solver_add_mul", tout << "i1: " << i1 << ", i2: " << i2 << " new_a: " << m().to_string(new_a) << "\n"; - tout << "as1: " << m().to_string(as1[i1]) << ", k: " << m().to_string(k) << ", as2: " << m().to_string(as2[i2]) << "\n";); - if (m().is_zero(new_a)) { - // variable was canceled - if (UpdateOcc && x1 != except_var) - m_occs[x1].erase(eq_idx); - if (UpdateQueue && solved(x1) && m_var_queue.contains(x1)) - m_var_queue.erase(x1); - } - else { - new_as.push_back(new_a); - new_xs.push_back(x1); - } - i1++; - i2++; - } - } - m().del(new_a); - } - - template - void apply_solution(var x, mpz_vector & as, var_vector & xs, mpz & c, mpq_vector & bs, justification_vector & js, - unsigned eq_idx = null_eq_idx, var except_var = null_var) { - SASSERT(solved(x)); - unsigned idx = pos(xs, x); - if (idx == UINT_MAX) - return; - mpz const & a1 = as[idx]; - - SASSERT(!m().is_zero(a1)); - equation const & eq2 = *(m_solution[m_solved[x]]); - TRACE("euclidean_solver_apply", - tout << "applying: " << m().to_string(a1) << " * "; display(tout, eq2); tout << "\n"; - tout << "index: " << idx << "\n"; - for (unsigned i = 0; i < xs.size(); i++) tout << m().to_string(as[i]) << "*x" << xs[i] << " "; tout << "\n";); - SASSERT(eq2.pos_x(x) != UINT_MAX); - SASSERT(m().is_minus_one(eq2.a(eq2.pos_x(x)))); - addmul(as, xs, a1, eq2.m_as, eq2.m_xs, m_tmp_as, m_tmp_xs, eq_idx, except_var); - m().addmul(c, a1, eq2.m_c, c); - m_tmp_as.swap(as); - m_tmp_xs.swap(xs); - SASSERT(as.size() == xs.size()); - TRACE("euclidean_solver_apply", for (unsigned i = 0; i < xs.size(); i++) tout << m().to_string(as[i]) << "*x" << xs[i] << " "; tout << "\n";); - addmul(bs, js, a1, eq2.m_bs, eq2.m_js, m_tmp_bs, m_tmp_xs); - m_tmp_bs.swap(bs); - m_tmp_xs.swap(js); - SASSERT(pos(xs, x) == UINT_MAX); - } - - void apply_solution(mpz_vector & as, var_vector & xs, mpz & c, mpq_vector & bs, justification_vector & js) { - m_var_queue.reset(); - schedule_var_subst(xs); - while (!m_var_queue.empty()) { - var x = m_var_queue.erase_min(); - apply_solution(x, as, xs, c, bs, js); - } - } - - void apply_solution(equation & eq) { - apply_solution(eq.m_as, eq.m_xs, eq.m_c, eq.m_bs, eq.m_js); - } - - void display(std::ostream & out, equation const & eq) const { - unsigned num = eq.js_size(); - for (unsigned i = 0; i < num; i ++) { - if (i > 0) out << " "; - out << m().to_string(eq.b(i)) << "*j" << eq.j(i); - } - if (num > 0) out << " "; - out << "|= "; - num = eq.size(); - for (unsigned i = 0; i < num; i++) { - out << m().to_string(eq.a(i)) << "*x" << eq.x(i) << " + "; - } - out << m().to_string(eq.c()) << " = 0"; - } - - void display(std::ostream & out, equations const & eqs) const { - unsigned num = eqs.size(); - for (unsigned i = 0; i < num; i++) { - if (eqs[i]) { - display(out, *(eqs[i])); - out << "\n"; - } - } - } - - void display(std::ostream & out) const { - if (inconsistent()) { - out << "inconsistent: "; - display(out, *(m_equations[m_inconsistent])); - out << "\n"; - } - out << "solution set:\n"; - display(out, m_solution); - out << "todo:\n"; - display(out, m_equations); - } - - void add_occs(unsigned eq_idx) { - equation const & eq = *(m_equations[eq_idx]); - unsigned sz = eq.size(); - for (unsigned i = 0; i < sz; i++) - m_occs[eq.x(i)].push_back(eq_idx); - } - - imp(numeral_manager * m): - m_manager(m == nullptr ? alloc(numeral_manager) : m), - m_owns_m(m == nullptr), - m_decompose_buffer(*m_manager), - m_as_buffer(*m_manager), - m_bs_buffer(*m_manager), - m_tmp_as(*m_manager), - m_tmp_bs(*m_manager), - m_var_queue(16, elim_order_lt(m_solved)) { - m_inconsistent = null_eq_idx; - m_next_justification = 0; - m_next_x = null_var; - m_next_eq = null_eq_idx; - } - - ~imp() { - m().del(m_next_a); - del_equations(m_equations); - del_equations(m_solution); - if (m_owns_m) - dealloc(m_manager); - } - - var mk_var(bool parameter) { - var x = m_solved.size(); - m_parameter.push_back(parameter); - m_solved.push_back(null_eq_idx); - m_occs.push_back(occs()); - m_as_buffer.push_back(mpz()); - m_var_queue.reserve(x+1); - return x; - } - - justification mk_justification() { - justification r = m_next_justification; - m_bs_buffer.push_back(mpq()); - m_next_justification++; - return r; - } - - void assert_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, justification j) { - if (inconsistent()) - return; - equation * eq; - if (j == null_justification) { - eq = mk_eq(num, as, xs, c, 0, nullptr, nullptr); - } - else { - mpq one(1); - eq = mk_eq(num, as, xs, c, 1, &one, &j); - } - TRACE("euclidean_solver", tout << "new-eq:\n"; display(tout, *eq); tout << "\n";); - unsigned eq_idx = m_equations.size(); - m_equations.push_back(eq); - apply_solution(*eq); - normalize_eq(eq_idx); - add_occs(eq_idx); - TRACE("euclidean_solver", tout << "asserted:\n"; display(tout, *eq); tout << "\n";); - } - - justification_vector const & get_justification() const { - SASSERT(inconsistent()); - return m_equations[m_inconsistent]->m_js; - } - - template - void neg_coeffs(svector & as) { - unsigned sz = as.size(); - for (unsigned i = 0; i < sz; i++) { - m().neg(as[i]); - } - } - - void substitute_most_recent_solution(var x) { - SASSERT(!m_solution.empty()); - TRACE("euclidean_solver", tout << "applying solution for x" << x << "\n"; - display(tout, *(m_solution.back())); tout << "\n";); - occs & use_list = m_occs[x]; - occs::iterator it = use_list.begin(); - occs::iterator end = use_list.end(); - for (; it != end; ++it) { - unsigned eq_idx = *it; - // remark we don't want to update the use_list of x while we are traversing it. - equation & eq2 = *(m_equations[eq_idx]); - TRACE("euclidean_solver", tout << "eq before substituting x" << x << "\n"; display(tout, eq2); tout << "\n";); - apply_solution(x, eq2.m_as, eq2.m_xs, eq2.m_c, eq2.m_bs, eq2.m_js, eq_idx, x); - TRACE("euclidean_solver", tout << "eq after substituting x" << x << "\n"; display(tout, eq2); tout << "\n";); - normalize_eq(eq_idx); - if (inconsistent()) - break; - } - use_list.reset(); - } - - void elim_unit() { - SASSERT(m().is_one(m_next_a)); - equation & eq = *(m_equations[m_next_eq]); - TRACE("euclidean_solver", tout << "eliminating equation with unit coefficient:\n"; display(tout, eq); tout << "\n";); - if (m_next_pos_a) { - // neg coeffs... to make sure that m_next_x is -1 - neg_coeffs(eq.m_as); - neg_coeffs(eq.m_bs); - m().neg(eq.m_c); - } - unsigned sz = eq.size(); - for (unsigned i = 0; i < sz; i++) { - m_occs[eq.x(i)].erase(m_next_eq); - } - m_solved[m_next_x] = m_solution.size(); - m_solution.push_back(&eq); - m_equations[m_next_eq] = 0; - substitute_most_recent_solution(m_next_x); - } - - void decompose(bool pos_a, mpz const & abs_a, mpz const & a_i, mpz & new_a_i, mpz & r_i) { - mpz abs_a_i; - bool pos_a_i = m().is_pos(a_i); - m().set(abs_a_i, a_i); - if (!pos_a_i) - m().neg(abs_a_i); - bool new_pos_a_i = pos_a_i; - if (pos_a) - new_pos_a_i = !new_pos_a_i; - m().div(abs_a_i, abs_a, new_a_i); - if (m().divides(abs_a, a_i)) { - m().reset(r_i); - } - else { - if (pos_a_i) - m().submul(a_i, abs_a, new_a_i, r_i); - else - m().addmul(a_i, abs_a, new_a_i, r_i); - } - if (!new_pos_a_i) - m().neg(new_a_i); - m().del(abs_a_i); - } - - void decompose_and_elim() { - m_tmp_xs.reset(); - mpz_buffer & buffer = m_decompose_buffer; - buffer.reset(); - var p = mk_var(true); - mpz new_a_i; - equation & eq = *(m_equations[m_next_eq]); - TRACE("euclidean_solver", tout << "decomposing equation for x" << m_next_x << "\n"; display(tout, eq); tout << "\n";); - unsigned sz = eq.size(); - unsigned j = 0; - for (unsigned i = 0; i < sz; i++) { - var x_i = eq.x(i); - if (x_i == m_next_x) { - m().set(new_a_i, -1); - buffer.push_back(new_a_i); - m_tmp_xs.push_back(m_next_x); - m_occs[x_i].erase(m_next_eq); - } - else { - decompose(m_next_pos_a, m_next_a, eq.a(i), new_a_i, eq.m_as[j]); - buffer.push_back(new_a_i); - m_tmp_xs.push_back(x_i); - if (m().is_zero(eq.m_as[j])) { - m_occs[x_i].erase(m_next_eq); - } - else { - eq.m_xs[j] = x_i; - j++; - } - } - } - SASSERT(j < sz); - // add parameter: p to new equality, and m_next_pos_a * m_next_a * p to current eq - m().set(new_a_i, 1); - buffer.push_back(new_a_i); - m_tmp_xs.push_back(p); - m().set(eq.m_as[j], m_next_a); - if (!m_next_pos_a) - m().neg(eq.m_as[j]); - eq.m_xs[j] = p; - j++; - unsigned new_sz = j; - // shrink current eq - for (; j < sz; j++) - m().del(eq.m_as[j]); - eq.m_as.shrink(new_sz); - eq.m_xs.shrink(new_sz); - // adjust c - mpz new_c; - decompose(m_next_pos_a, m_next_a, eq.m_c, new_c, eq.m_c); - // create auxiliary equation - equation * new_eq = mk_eq(m_tmp_xs.size(), buffer.c_ptr(), m_tmp_xs.c_ptr(), new_c, 0, nullptr, nullptr, false); - // new_eq doesn't need to normalized, since it has unit coefficients - TRACE("euclidean_solver", tout << "decomposition: new parameter x" << p << " aux eq:\n"; - display(tout, *new_eq); tout << "\n"; - display(tout, eq); tout << "\n"; - tout << "next_x " << m_next_x << "\n";); - m_solved[m_next_x] = m_solution.size(); - m_solution.push_back(new_eq); - substitute_most_recent_solution(m_next_x); - m().del(new_a_i); - m().del(new_c); - } - - bool solve() { - if (inconsistent()) return false; - TRACE("euclidean_solver", tout << "solving...\n"; display(tout);); - while (select_next_var()) { - CTRACE("euclidean_solver_bug", m_next_x == null_var, display(tout);); - TRACE("euclidean_solver", tout << "eliminating x" << m_next_x << "\n";); - if (m().is_one(m_next_a) || m().is_minus_one(m_next_a)) - elim_unit(); - else - decompose_and_elim(); - TRACE("euclidean_solver", display(tout);); - if (inconsistent()) return false; - } - return true; - } - - bool inconsistent() const { - return m_inconsistent != null_eq_idx; - } - - bool is_parameter(var x) const { - return m_parameter[x]; - } - - void normalize(unsigned num, mpz const * as, var const * xs, mpz const & c, mpz & a_prime, mpz & c_prime, justification_vector & js) { - TRACE("euclidean_solver", tout << "before applying solution set\n"; - for (unsigned i = 0; i < num; i++) { - tout << m().to_string(as[i]) << "*x" << xs[i] << " "; - } - tout << "\n";); - - m_norm_xs_vector.reset(); - m_norm_as_vector.reset(); - for (unsigned i = 0; i < num; i++) { - m_norm_xs_vector.push_back(xs[i]); - m_norm_as_vector.push_back(mpz()); - m().set(m_norm_as_vector.back(), as[i]); - } - sort(m_norm_as_vector, m_norm_xs_vector, m_as_buffer); - DEBUG_CODE(for (unsigned i = 1; i < m_norm_xs_vector.size(); ++i) SASSERT(m_norm_xs_vector[i - 1] != m_norm_xs_vector[i]);); - m_norm_bs_vector.reset(); - js.reset(); - m().set(c_prime, c); - apply_solution(m_norm_as_vector, m_norm_xs_vector, c_prime, m_norm_bs_vector, js); - TRACE("euclidean_solver", tout << "after applying solution set\n"; - for (unsigned i = 0; i < m_norm_as_vector.size(); i++) { - tout << m().to_string(m_norm_as_vector[i]) << "*x" << m_norm_xs_vector[i] << " "; - } - tout << "\n";); - // compute gcd of the result m_norm_as_vector - if (m_norm_as_vector.empty()) { - m().set(a_prime, 0); - } - else { - mpz a; - m().set(a_prime, m_norm_as_vector[0]); - m().abs(a_prime); - unsigned sz = m_norm_as_vector.size(); - for (unsigned i = 1; i < sz; i++) { - if (m().is_one(a_prime)) - break; - m().set(a, m_norm_as_vector[i]); - m().abs(a); - m().gcd(a_prime, a, a_prime); - } - m().del(a); - } - // REMARK: m_norm_bs_vector contains the linear combination of the justifications. It may be useful if we - // decided (one day) to generate detailed proofs for this step. - del_nums(m_norm_as_vector); - del_nums(m_norm_bs_vector); - } - - -}; - -euclidean_solver::euclidean_solver(numeral_manager * m): - m_imp(alloc(imp, m)) { -} - -euclidean_solver::~euclidean_solver() { - dealloc(m_imp); -} - -euclidean_solver::numeral_manager & euclidean_solver::m() const { - return m_imp->m(); -} - -void euclidean_solver::reset() { - numeral_manager * m = m_imp->m_manager; - bool owns_m = m_imp->m_owns_m; - m_imp->m_owns_m = false; - dealloc(m_imp); - m_imp = alloc(imp, m); - m_imp->m_owns_m = owns_m; -} - -euclidean_solver::var euclidean_solver::mk_var() { - return m_imp->mk_var(false); -} - -euclidean_solver::justification euclidean_solver::mk_justification() { - return m_imp->mk_justification(); -} - -void euclidean_solver::assert_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, justification j) { - m_imp->assert_eq(num, as, xs, c, j); -} - -bool euclidean_solver::solve() { - return m_imp->solve(); -} - -euclidean_solver::justification_vector const & euclidean_solver::get_justification() const { - return m_imp->get_justification(); -} - -bool euclidean_solver::inconsistent() const { - return m_imp->inconsistent(); -} - -bool euclidean_solver::is_parameter(var x) const { - return m_imp->is_parameter(x); -} - -void euclidean_solver::normalize(unsigned num, mpz const * as, var const * xs, mpz const & c, mpz & a_prime, mpz & c_prime, - justification_vector & js) { - return m_imp->normalize(num, as, xs, c, a_prime, c_prime, js); -} - - -void euclidean_solver::display(std::ostream & out) const { - m_imp->display(out); -} - - diff --git a/src/math/euclid/euclidean_solver.h b/src/math/euclid/euclidean_solver.h deleted file mode 100644 index 74d0d7fa4..000000000 --- a/src/math/euclid/euclidean_solver.h +++ /dev/null @@ -1,102 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - euclidean_solver.h - -Abstract: - - Euclidean Solver with support for explanations. - -Author: - - Leonardo de Moura (leonardo) 2011-07-08. - -Revision History: - ---*/ -#ifndef EUCLIDEAN_SOLVER_H_ -#define EUCLIDEAN_SOLVER_H_ - -#include "util/mpq.h" -#include "util/vector.h" - -class euclidean_solver { - struct imp; - imp * m_imp; -public: - typedef unsigned var; - typedef unsigned justification; - typedef unsynch_mpq_manager numeral_manager; - typedef svector justification_vector; - static const justification null_justification = UINT_MAX; - - /** - \brief If m == 0, then the solver will create its own numeral manager. - */ - euclidean_solver(numeral_manager * m); - - ~euclidean_solver(); - - numeral_manager & m() const; - - /** - \brief Reset the state of the euclidean solver. - */ - void reset(); - - /** - \brief Creates a integer variable. - */ - var mk_var(); - - /** - \brief Creates a fresh justification id. - */ - justification mk_justification(); - - /** - \brief Asserts an equation of the form as[0]*xs[0] + ... + as[num-1]*xs[num-1] + c = 0 with justification j. - - The numerals must be created using the numeral_manager m(). - */ - void assert_eq(unsigned num, mpz const * as, var const * xs, mpz const & c, justification j = null_justification); - - /** - \brief Solve the current set of equations. Return false if it is inconsistent. - */ - bool solve(); - - /** - \brief Return a set of justifications (proof) for the inconsitency. - - \pre inconsistent() - */ - justification_vector const & get_justification() const; - - bool inconsistent() const; - - /** - \brief Return true if the variable is a "parameter" created by the Euclidean solver. - */ - bool is_parameter(var x) const; - - /** - Given a linear polynomial as[0]*xs[0] + ... + as[num-1]*xs[num-1] + c and the current solution set, - It applies the solution set to produce a polynomial of the for a_prime * p + c_prime, where - a_prime * p represents a linear polynomial where the coefficient of every monomial is a multiple of - a_prime. - - The justification is stored in js. - Note that, this function does not return the actual p. - - The numerals must be created using the numeral_manager m(). - */ - void normalize(unsigned num, mpz const * as, var const * xs, mpz const & c, mpz & a_prime, mpz & c_prime, justification_vector & js); - - - void display(std::ostream & out) const; -}; - -#endif diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index e08b55e30..b29270e0a 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -77,7 +77,6 @@ z3_add_component(smt COMPONENT_DEPENDENCIES bit_blaster cmd_context - euclid fpa grobner nlsat diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 22b252985..c08323726 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -59,7 +59,6 @@ def_module_params(module_name='smt', ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), - ('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'), ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 0918c9423..22de881fa 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -29,7 +29,6 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_nl_arith_gb = p.arith_nl_gb(); m_nl_arith_branching = p.arith_nl_branching(); m_nl_arith_rounds = p.arith_nl_rounds(); - m_arith_euclidean_solver = p.arith_euclidean_solver(); m_arith_propagate_eqs = p.arith_propagate_eqs(); m_arith_branch_cut_ratio = p.arith_branch_cut_ratio(); m_arith_int_eq_branching = p.arith_int_eq_branch(); @@ -93,5 +92,4 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_max_degree); DISPLAY_PARAM(m_nl_arith_branching); DISPLAY_PARAM(m_nl_arith_rounds); - DISPLAY_PARAM(m_arith_euclidean_solver); } diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index fe7cc6060..675cfce52 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -106,8 +106,6 @@ struct theory_arith_params { bool m_nl_arith_branching; unsigned m_nl_arith_rounds; - // euclidean solver for tighting bounds - bool m_arith_euclidean_solver; theory_arith_params(params_ref const & p = params_ref()): @@ -155,8 +153,7 @@ struct theory_arith_params { m_nl_arith_gb_perturbate(true), m_nl_arith_max_degree(6), m_nl_arith_branching(true), - m_nl_arith_rounds(1024), - m_arith_euclidean_solver(false) { + m_nl_arith_rounds(1024) { updt_params(p); } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index dc30c99a0..ee1b99312 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -853,9 +853,9 @@ namespace smt { bool max_min_infeasible_int_vars(); void patch_int_infeasible_vars(); void fix_non_base_vars(); - unsynch_mpq_manager m_es_num_manager; // manager for euclidean solver. - struct euclidean_solver_bridge; - bool apply_euclidean_solver(); +// unsynch_mpq_manager m_es_num_manager; // manager for euclidean solver. +// struct euclidean_solver_bridge; +// bool apply_euclidean_solver(); final_check_status check_int_feasibility(); // ----------------------------------- diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index edf22b76c..d46fa4350 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -23,7 +23,6 @@ Revision History: #include "ast/ast_ll_pp.h" #include "ast/well_sorted.h" #include "ast/ast_smt2_pp.h" -#include "math/euclid/euclidean_solver.h" namespace smt { @@ -964,335 +963,6 @@ namespace smt { failed(); } - template - struct theory_arith::euclidean_solver_bridge { - typedef numeral_buffer mpz_buffer; - theory_arith & t; - euclidean_solver m_solver; - unsigned_vector m_tv2v; // theory var to euclidean solver var - svector m_j2v; // justification to theory var - - // aux fields - unsigned_vector m_xs; - mpz_buffer m_as; - unsigned_vector m_js; - - typedef euclidean_solver::var evar; - typedef euclidean_solver::justification ejustification; - euclidean_solver_bridge(theory_arith & _t):t(_t), m_solver(&t.m_es_num_manager), m_as(m_solver.m()) {} - - evar mk_var(theory_var v) { - m_tv2v.reserve(v+1, UINT_MAX); - if (m_tv2v[v] == UINT_MAX) - m_tv2v[v] = m_solver.mk_var(); - return m_tv2v[v]; - } - - /** - \brief Given a monomial, retrieve its coefficient and the power product - That is, mon = a * pp - */ - void get_monomial(expr * mon, rational & a, expr * & pp) { - expr * a_expr; - if (t.m_util.is_mul(mon, a_expr, pp) && t.m_util.is_numeral(a_expr, a)) - return; - a = rational(1); - pp = mon; - } - - /** - \brief Return the theory var associated with the given power product. - */ - theory_var get_theory_var(expr * pp) { - context & ctx = t.get_context(); - if (ctx.e_internalized(pp)) { - enode * e = ctx.get_enode(pp); - if (t.is_attached_to_var(e)) - return e->get_th_var(t.get_id()); - } - return null_theory_var; - } - - /** - \brief Create an euclidean_solver variable for the given - power product, if it has a theory variable associated with - it. - */ - evar mk_var(expr * pp) { - theory_var v = get_theory_var(pp); - if (v == null_theory_var) - return UINT_MAX; - return mk_var(v); - } - - /** - \brief Return the euclidean_solver variable associated with the given - power product. Return UINT_MAX, if it doesn't have one. - */ - evar get_var(expr * pp) { - theory_var v = get_theory_var(pp); - if (v == null_theory_var || v >= static_cast(m_tv2v.size())) - return UINT_MAX; - return m_tv2v[v]; - } - - void assert_eqs() { - // traverse definitions looking for equalities - mpz c, a; - mpz one; - euclidean_solver::numeral_manager & m = m_solver.m(); - m.set(one, 1); - mpz_buffer & as = m_as; - unsigned_vector & xs = m_xs; - int num = t.get_num_vars(); - for (theory_var v = 0; v < num; v++) { - if (!t.is_fixed(v)) - continue; - if (!t.is_int(v)) - continue; // only integer variables - expr * n = t.get_enode(v)->get_owner(); - if (t.m_util.is_numeral(n)) - continue; // skip stupid equality c - c = 0 - inf_numeral const & val = t.get_value(v); - rational num = val.get_rational().to_rational(); - SASSERT(num.is_int()); - num.neg(); - m.set(c, num.to_mpq().numerator()); - ejustification j = m_solver.mk_justification(); - m_j2v.reserve(j+1, null_theory_var); - m_j2v[j] = v; - as.reset(); - xs.reset(); - bool failed = false; - unsigned num_args; - expr * const * args; - if (t.m_util.is_add(n)) { - num_args = to_app(n)->get_num_args(); - args = to_app(n)->get_args(); - } - else { - num_args = 1; - args = &n; - } - for (unsigned i = 0; i < num_args; i++) { - expr * arg = args[i]; - expr * pp; - rational a_val; - get_monomial(arg, a_val, pp); - if (!a_val.is_int()) { - failed = true; - break; - } - evar x = mk_var(pp); - if (x == UINT_MAX) { - failed = true; - break; - } - m.set(a, a_val.to_mpq().numerator()); - as.push_back(a); - xs.push_back(x); - } - if (!failed) { - m_solver.assert_eq(as.size(), as.c_ptr(), xs.c_ptr(), c, j); - TRACE("euclidean_solver", tout << "add definition: v" << v << " := " << mk_ismt2_pp(n, t.get_manager()) << "\n";); - } - else { - TRACE("euclidean_solver", tout << "failed for:\n" << mk_ismt2_pp(n, t.get_manager()) << "\n";); - } - } - m.del(a); - m.del(c); - m.del(one); - } - - void mk_bound(theory_var v, rational k, bool lower, bound * old_bound, unsigned_vector const & js) { - derived_bound * new_bound = alloc(derived_bound, v, inf_numeral(k), lower ? B_LOWER : B_UPPER); - t.m_tmp_lit_set.reset(); - t.m_tmp_eq_set.reset(); - if (old_bound != nullptr) { - t.accumulate_justification(*old_bound, *new_bound, numeral(0) /* refine for proof gen */, t.m_tmp_lit_set, t.m_tmp_eq_set); - } - unsigned_vector::const_iterator it = js.begin(); - unsigned_vector::const_iterator end = js.end(); - for (; it != end; ++it) { - ejustification j = *it; - theory_var fixed_v = m_j2v[j]; - SASSERT(fixed_v != null_theory_var); - t.accumulate_justification(*(t.lower(fixed_v)), *new_bound, numeral(0) /* refine for proof gen */, t.m_tmp_lit_set, t.m_tmp_eq_set); - t.accumulate_justification(*(t.upper(fixed_v)), *new_bound, numeral(0) /* refine for proof gen */, t.m_tmp_lit_set, t.m_tmp_eq_set); - } - t.m_bounds_to_delete.push_back(new_bound); - t.m_asserted_bounds.push_back(new_bound); - } - - void mk_lower(theory_var v, rational k, bound * old_bound, unsigned_vector const & js) { - mk_bound(v, k, true, old_bound, js); - } - - void mk_upper(theory_var v, rational k, bound * old_bound, unsigned_vector const & js) { - mk_bound(v, k, false, old_bound, js); - } - - bool tight_bounds(theory_var v) { - SASSERT(!t.is_fixed(v)); - euclidean_solver::numeral_manager & m = m_solver.m(); - expr * n = t.get_enode(v)->get_owner(); - SASSERT(!t.m_util.is_numeral(n)); // should not be a numeral since v is not fixed. - bool propagated = false; - mpz a; - mpz c; - rational g; // gcd of the coefficients of the variables that are not in m_solver - rational c2; - bool init_g = false; - mpz_buffer & as = m_as; - unsigned_vector & xs = m_xs; - as.reset(); - xs.reset(); - - unsigned num_args; - expr * const * args; - if (t.m_util.is_add(n)) { - num_args = to_app(n)->get_num_args(); - args = to_app(n)->get_args(); - } - else { - num_args = 1; - args = &n; - } - for (unsigned j = 0; j < num_args; j++) { - expr * arg = args[j]; - expr * pp; - rational a_val; - get_monomial(arg, a_val, pp); - if (!a_val.is_int()) - goto cleanup; - evar x = get_var(pp); - if (x == UINT_MAX) { - a_val = abs(a_val); - if (init_g) - g = gcd(g, a_val); - else - g = a_val; - init_g = true; - if (g.is_one()) - goto cleanup; // gcd of the coeffs is one. - } - else { - m.set(a, a_val.to_mpq().numerator()); - as.push_back(a); - xs.push_back(x); - } - } - m_js.reset(); - m_solver.normalize(as.size(), as.c_ptr(), xs.c_ptr(), c, a, c, m_js); - if (init_g) { - if (!m.is_zero(a)) - g = gcd(g, rational(a)); - } - else { - g = rational(a); - } - TRACE("euclidean_solver", tout << "tightening " << mk_ismt2_pp(t.get_enode(v)->get_owner(), t.get_manager()) << "\n"; - tout << "g: " << g << ", a: " << m.to_string(a) << ", c: " << m.to_string(c) << "\n"; - t.display_var(tout, v);); - if (g.is_one()) - goto cleanup; - CTRACE("euclidean_solver_zero", g.is_zero(), tout << "tightening " << mk_ismt2_pp(t.get_enode(v)->get_owner(), t.get_manager()) << "\n"; - tout << "g: " << g << ", a: " << m.to_string(a) << ", c: " << m.to_string(c) << "\n"; - t.display(tout); - tout << "------------\nSolver state:\n"; - m_solver.display(tout);); - if (g.is_zero()) { - // The definition of v is equal to (0 + c). - // That is, v is fixed at c. - // The justification is just m_js, the existing bounds of v are not needed for justifying the new bounds for v. - c2 = rational(c); - TRACE("euclidean_solver_new", tout << "new fixed: " << c2 << "\n";); - propagated = true; - mk_lower(v, c2, nullptr, m_js); - mk_upper(v, c2, nullptr, m_js); - } - else { - TRACE("euclidean_solver", tout << "inequality can be tightned, since all coefficients are multiple of: " << g << "\n";); - // Let l and u be the current lower and upper bounds. - // Then, the following new bounds can be generated: - // - // l' := g*ceil((l - c)/g) + c - // u' := g*floor((l - c)/g) + c - bound * l = t.lower(v); - bound * u = t.upper(v); - c2 = rational(c); - if (l != nullptr) { - rational l_old = l->get_value().get_rational().to_rational(); - rational l_new = g*ceil((l_old - c2)/g) + c2; - TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n"; - tout << "c: " << c2 << " ceil((l_old - c2)/g): " << (ceil((l_old - c2)/g)) << "\n";); - if (l_new > l_old) { - propagated = true; - mk_lower(v, l_new, l, m_js); - } - } - if (u != nullptr) { - rational u_old = u->get_value().get_rational().to_rational(); - rational u_new = g*floor((u_old - c2)/g) + c2; - TRACE("euclidean_solver_new", tout << "new upper: " << u_new << " old: " << u_old << "\n";); - if (u_new < u_old) { - propagated = true; - mk_upper(v, u_new, u, m_js); - } - } - } - cleanup: - m.del(a); - m.del(c); - return propagated; - } - - bool tight_bounds() { - bool propagated = false; - context & ctx = t.get_context(); - // try to apply solution set to every definition - int num = t.get_num_vars(); - for (theory_var v = 0; v < num; v++) { - if (t.is_fixed(v)) - continue; // skip equations... - if (!t.is_int(v)) - continue; // skip non integer definitions... - if (t.lower(v) == nullptr && t.upper(v) == nullptr) - continue; // there is nothing to be tightned - if (tight_bounds(v)) - propagated = true; - if (ctx.inconsistent()) - break; - } - return propagated; - } - - bool operator()() { - TRACE("euclidean_solver", t.display(tout);); - assert_eqs(); - m_solver.solve(); - if (m_solver.inconsistent()) { - // TODO: set conflict - TRACE("euclidean_solver_conflict", tout << "conflict detected...\n"; m_solver.display(tout);); - return false; - } - return tight_bounds(); - } - }; - - - template - bool theory_arith::apply_euclidean_solver() { - TRACE("euclidean_solver", tout << "executing euclidean solver...\n";); - euclidean_solver_bridge esb(*this); - if (esb()) { - propagate_core(); - return true; - } - return false; - } - /** \brief Return FC_DONE if the assignment is int feasible. Otherwise, apply GCD test, branch and bound and Gomory Cuts. @@ -1341,9 +1011,6 @@ namespace smt { if (!gcd_test()) return FC_CONTINUE; - - if (m_params.m_arith_euclidean_solver) - apply_euclidean_solver(); if (get_context().inconsistent()) return FC_CONTINUE;