From fc23a498c4da724746263f25432f639de2b5c213 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 4 Dec 2023 15:06:50 -1000 Subject: [PATCH 01/33] a simple version of choosing a column for gomory cut --- src/math/lp/gomory.cpp | 64 ++--------------------- src/math/lp/gomory.h | 4 +- src/math/lp/int_branch.cpp | 2 +- src/math/lp/int_solver.cpp | 104 +++++++++++++++++++++++++++---------- src/math/lp/int_solver.h | 7 +-- src/math/lp/lar_solver.h | 5 ++ 6 files changed, 90 insertions(+), 96 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 406b2a290..5c38a8c7f 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -409,73 +409,15 @@ lia_move gomory::cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_ create_cut cc(t, k, ex, basic_inf_int_j, row, lia); return cc.cut(); } - -bool gomory::is_gomory_cut_target(const row_strip& row) { - // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed). - unsigned j; - for (const auto & p : row) { - j = p.var(); - if (!lia.is_base(j) && (!lia.at_bound(j) || !is_zero(lia.get_value(j).y))) { - TRACE("gomory_cut", tout << "row is not gomory cut target:\n"; - lia.display_column(tout, j); - tout << "infinitesimal: " << !is_zero(lia.get_value(j).y) << "\n";); - return false; - } - } - return true; -} - -int gomory::find_basic_var() { - unsigned n = 0; - int result = -1; - unsigned min_row_size = UINT_MAX; - -#if 1 - result = lia.select_int_infeasible_var(true); - - if (result == -1) - return result; - - TRACE("gomory_cut", tout << "row: " << result << "\n"); - const row_strip& row = lra.get_row(lia.row_of_basic_column(result)); - if (is_gomory_cut_target(row)) - return result; - result = -1; - - UNREACHABLE(); -#endif - - for (unsigned j : lra.r_basis()) { - if (!lia.column_is_int_inf(j)) - continue; - const row_strip& row = lra.get_row(lia.row_of_basic_column(j)); - TRACE("gomory_cut", tout << "try j" << j << "\n"); - if (!is_gomory_cut_target(row)) - continue; - IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j))); - // Prefer smaller row size - if (min_row_size == UINT_MAX || - 2*row.size() < min_row_size || - (4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) { - result = j; - n = 1; - min_row_size = std::min(min_row_size, row.size()); - } - } - return result; -} -lia_move gomory::operator()() { - int j = find_basic_var(); - if (j == -1) - return lia_move::undef; +lia_move gomory::get_cut(lpvar j) { unsigned r = lia.row_of_basic_column(j); const row_strip& row = lra.get_row(r); SASSERT(lra.row_is_correct(r)); - SASSERT(is_gomory_cut_target(row)); + SASSERT(lia.is_gomory_cut_target(j)); lia.m_upper = false; lia.m_cut_vars.push_back(j); - return cut(lia.m_t, lia.m_k, lia.m_ex, j, row); + return cut(lia.m_t, lia.m_k, lia.m_ex, j, row); } diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h index 68e42feb9..cdb21a0c3 100644 --- a/src/math/lp/gomory.h +++ b/src/math/lp/gomory.h @@ -27,11 +27,9 @@ namespace lp { class gomory { class int_solver& lia; class lar_solver& lra; - int find_basic_var(); - bool is_gomory_cut_target(const row_strip& row); lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row); public: gomory(int_solver& lia); - lia_move operator()(); + lia_move get_cut(lpvar j); }; } diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 2137dfd82..1a998e92a 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -53,7 +53,7 @@ lia_move int_branch::create_branch_on_column(int j) { int int_branch::find_inf_int_base_column() { #if 1 - return lia.select_int_infeasible_var(false); + return lia.select_int_infeasible_var(); #endif int result = -1; diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index c324af5b6..f760755a2 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -198,15 +198,9 @@ namespace lp { if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds(); if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut(); - std::function gomory_fn = [&]() { return gomory(*this)(); }; - m_cut_vars.reset(); -#if 0 - if (r == lia_move::undef && should_gomory_cut()) r = gomory(*this)(); -#else + std::function gomory_fn = [&](lpvar j) { return gomory(*this).get_cut(j); }; if (r == lia_move::undef && should_gomory_cut()) r = local_cut(2, gomory_fn); - -#endif - m_cut_vars.reset(); + if (r == lia_move::undef) r = int_branch(*this)(); if (settings().get_cancel_flag()) r = lia_move::undef; return r; @@ -635,7 +629,7 @@ namespace lp { } - int int_solver::select_int_infeasible_var(bool check_bounded) { + int int_solver::select_int_infeasible_var() { int r_small_box = -1; int r_small_value = -1; int r_any_value = -1; @@ -648,18 +642,6 @@ namespace lp { lar_core_solver & lcs = lra.m_mpq_lar_core_solver; unsigned prev_usage = 0; - auto check_bounded_fn = [&](unsigned j) { - if (!check_bounded) - return true; - auto const& row = lra.get_row(row_of_basic_column(j)); - for (const auto & p : row) { - unsigned j = p.var(); - if (!is_base(j) && (!at_bound(j) || !is_zero(get_value(j).y))) - return false; - } - return true; - }; - auto add_column = [&](bool improved, int& result, unsigned& n, unsigned j) { if (result == -1) result = j; @@ -670,9 +652,7 @@ namespace lp { for (unsigned j : lra.r_basis()) { if (!column_is_int_inf(j)) continue; - if (!check_bounded_fn(j)) - continue; - if (m_cut_vars.contains(j)) + if (m_cut_vars.contains(j)) continue; SASSERT(!is_fixed(j)); @@ -849,19 +829,71 @@ namespace lp { #endif } + // return the minimal distance from the column value to an integer + mpq get_gomory_score(const int_solver& lia, lpvar j) { + const mpq& val = lia.get_value(j).x; + auto l = val - floor(val); + if (l <= mpq(1, 2)) + return l; + return mpq(1) - l; + } + unsigned_vector int_solver::gomory_select_int_infeasible_vars(unsigned num_cuts) { + SASSERT(m_cut_vars.size() == 0&& num_cuts >= 0); + + std::list sorted_vars; + std::unordered_map score; + for (lpvar j : lra.r_basis()) { + if (!column_is_int_inf(j) || !is_gomory_cut_target(j)) + continue; + SASSERT(!is_fixed(j)); + sorted_vars.push_back(j); + score[j] = get_gomory_score(*this, j); + } + // prefer the columns with the values close to integers + sorted_vars.sort([&](lpvar j, lpvar k) { + auto diff = score[j] - score[k]; + if (diff.is_neg()) + return true; + if (diff.is_pos()) + return false; + return lra.usage_in_terms(j) > lra.usage_in_terms(k); + }); + unsigned_vector ret; + unsigned n = static_cast(sorted_vars.size()); - lia_move int_solver::local_cut(unsigned num_cuts, std::function& cut_fn) { + while (num_cuts-- && n > 0) { + unsigned k = random() % n; + + double k_ratio = k / (double) n; + k_ratio *= k_ratio*k_ratio; // square k_ratio to make it smaller + k = static_cast(std::floor(k_ratio * n)); + // these operations move k to the beginning of the indices range + SASSERT(0 <= k && k < n); + auto it = sorted_vars.begin(); + while(k--) it++; + ret.push_back(*it); + sorted_vars.erase(it); + n--; + } + return ret; + } + + lia_move int_solver::local_cut(unsigned num_cuts, std::function& cut_fn) { + struct ex { explanation m_ex; lar_term m_term; mpq m_k; bool m_is_upper; }; + unsigned_vector columns_for_cuts = gomory_select_int_infeasible_vars(num_cuts); + vector cuts; - for (unsigned i = 0; i < num_cuts && has_inf_int(); ++i) { + + for (unsigned j : columns_for_cuts) { m_ex->clear(); m_t.clear(); m_k.reset(); - auto r = cut_fn(); + auto r = cut_fn(j); if (r != lia_move::cut) - break; + continue; cuts.push_back({ *m_ex, m_t, m_k, is_upper() }); if (settings().get_cancel_flag()) return lia_move::undef; @@ -938,6 +970,22 @@ namespace lp { return lia_move::undef; } + bool int_solver::is_gomory_cut_target(lpvar k) { + SASSERT(is_base(k)); + // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed). + const row_strip& row = lra.get_row(row_of_basic_column(k)); + unsigned j; + for (const auto & p : row) { + j = p.var(); + if ( k != j && (!at_bound(j) || !is_zero(get_value(j).y))) { + TRACE("gomory_cut", tout << "row is not gomory cut target:\n"; + display_column(tout, j); + tout << "infinitesimal: " << !is_zero(get_value(j).y) << "\n";); + return false; + } + } + return true; + } } diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 0832bd45e..feeb96986 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -111,7 +111,7 @@ private: bool has_upper(unsigned j) const; unsigned row_of_basic_column(unsigned j) const; bool cut_indices_are_columns() const; - lia_move local_cut(unsigned num_cuts, std::function& cut_fn); + lia_move local_cut(unsigned num_cuts, std::function& cut_fn); public: std::ostream& display_column(std::ostream & out, unsigned j) const; @@ -132,7 +132,8 @@ public: bool all_columns_are_bounded() const; lia_move hnf_cut(); - int select_int_infeasible_var(bool check_bounded); - + int select_int_infeasible_var(); + unsigned_vector gomory_select_int_infeasible_vars(unsigned num_cuts); + bool is_gomory_cut_target(lpvar); }; } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index d01a42680..a01a66a38 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -532,6 +532,11 @@ public: inline const impq& get_lower_bound(column_index j) const { return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j]; } + + inline mpq bound_span_x(column_index j) const { + return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j].x - m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j].x; + } + bool has_lower_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const; bool has_upper_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const; bool has_value(var_index var, mpq& value) const; From 4d1d067d42c3ea9d2928448b39695389c0e38552 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Dec 2023 13:34:35 -0800 Subject: [PATCH 02/33] fix divergence reported by Guido Martinez --- src/math/lp/emonics.cpp | 15 +++++++++++++++ src/math/lp/emonics.h | 1 + src/math/lp/monic.h | 3 +++ src/math/lp/nla_core.cpp | 3 +++ 4 files changed, 22 insertions(+) diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index 9a9e4566b..5d0e664f2 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -611,4 +611,19 @@ void emonics::set_propagated(monic const& m) { m_u_f_stack.push(set_unpropagated(*this, m.var())); } +void emonics::set_bound_propagated(monic const& m) { + struct set_bound_unpropagated : public trail { + emonics& em; + unsigned var; + public: + set_bound_unpropagated(emonics& em, unsigned var): em(em), var(var) {} + void undo() override { + em[var].set_bound_propagated(false); + } + }; + SASSERT(!m.is_bound_propagated()); + (*this)[m.var()].set_bound_propagated(true); + m_u_f_stack.push(set_bound_unpropagated(*this, m.var())); +} + } diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h index fe0b19117..55086515d 100644 --- a/src/math/lp/emonics.h +++ b/src/math/lp/emonics.h @@ -143,6 +143,7 @@ public: void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} void set_propagated(monic const& m); + void set_bound_propagated(monic const& m); // this method is required by union_find trail_stack & get_trail_stack() { return m_u_f_stack; } diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h index d981b2042..19137cd31 100644 --- a/src/math/lp/monic.h +++ b/src/math/lp/monic.h @@ -59,6 +59,7 @@ class monic: public mon_eq { bool m_rsign; mutable unsigned m_visited; bool m_propagated = false; + bool m_bound_propagated = false; public: // constructors monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): @@ -77,6 +78,8 @@ public: void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); } void set_propagated(bool p) { m_propagated = p; } bool is_propagated() const { return m_propagated; } + void set_bound_propagated(bool p) { m_bound_propagated = p; } + bool is_bound_propagated() const { return m_bound_propagated; } svector::const_iterator begin() const { return vars().begin(); } svector::const_iterator end() const { return vars().end(); } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 96f1b4a30..f36fab52e 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1517,6 +1517,9 @@ void core::add_bounds() { for (lpvar j : m.vars()) { if (!var_is_free(j)) continue; + if (m.is_bound_propagated()) + continue; + m_emons.set_bound_propagated(m); // split the free variable (j <= 0, or j > 0), and return m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); TRACE("nla_solver", print_ineq(m_literals.back(), tout) << "\n"); From 6cd619d377d829a81249cef93279afebcd945b44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 11:39:55 -0800 Subject: [PATCH 03/33] kludge to fixup osver in python for Mac Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index a20ff53a3..54992156f 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -313,6 +313,8 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv: osver = RELEASE_METADATA[3] if osver.count('.') > 1: osver = '.'.join(osver.split('.')[:2]) + if osver.startswith("11"): + osver = "11_0" if arch == 'x64': plat_name ='macosx_%s_x86_64' % osver.replace('.', '_') elif arch == 'arm64': From 8e26c2af17f33439b20c90fc865152de67cfb2df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 13:05:21 -0800 Subject: [PATCH 04/33] fix #7049 Signed-off-by: Nikolaj Bjorner --- src/ast/polymorphism_inst.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp index 4da83ee10..aa9b1e5fe 100644 --- a/src/ast/polymorphism_inst.cpp +++ b/src/ast/polymorphism_inst.cpp @@ -94,7 +94,10 @@ namespace polymorphism { t.push(value_trail(m_decl_qhead)); for (; m_decl_qhead < num_decls; ++m_decl_qhead) { func_decl* p = m_decl_queue.get(m_decl_qhead); - for (expr* e : m_occurs[m.poly_root(p)]) + func_decl* r = m.poly_root(p); + if (!m_occurs.contains(r)) + continue; + for (expr* e : m_occurs[r]) instantiate(p, e, instances); } } From 7e716f7cfe75b7da51167b0c4545c3506760351c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 13:12:05 -0800 Subject: [PATCH 05/33] try fix suggested in #7041 Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index a9f2676a7..aa4c50adf 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,3 +1,6 @@ [build-system] requires = ["setuptools>=46.4.0", "wheel", "cmake"] build-backend = "setuptools.build_meta" + +[project] +dependencies = ["importlib-resources" ] \ No newline at end of file From 6282f402550e53766f28ed9354772209b93cb098 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 14:57:45 -0800 Subject: [PATCH 06/33] try add name to project Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index aa4c50adf..4c199fb26 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -3,4 +3,5 @@ requires = ["setuptools>=46.4.0", "wheel", "cmake"] build-backend = "setuptools.build_meta" [project] -dependencies = ["importlib-resources" ] \ No newline at end of file +name = "z3-solver" +dependencies = ["importlib-resources", ] \ No newline at end of file From 4123405d176fb49e8e304a70405ae55448bc8ee4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 15:50:09 -0800 Subject: [PATCH 07/33] add version Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index 4c199fb26..2f441d000 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -4,4 +4,5 @@ build-backend = "setuptools.build_meta" [project] name = "z3-solver" +version = "4" dependencies = ["importlib-resources", ] \ No newline at end of file From 575538d32580a7d0b2ef8f721a817abfd6e8afc6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 18:38:29 -0800 Subject: [PATCH 08/33] follow error message to put dependencies in setup args Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 5 ----- src/api/python/setup.py | 1 + 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index 2f441d000..a9f2676a7 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,8 +1,3 @@ [build-system] requires = ["setuptools>=46.4.0", "wheel", "cmake"] build-backend = "setuptools.build_meta" - -[project] -name = "z3-solver" -version = "4" -dependencies = ["importlib-resources", ] \ No newline at end of file diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 54992156f..325fb4230 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -341,6 +341,7 @@ setup( license='MIT License', keywords=['z3', 'smt', 'sat', 'prover', 'theorem'], packages=['z3'], + install_requires = ['importlib-resources'], include_package_data=True, package_data={ 'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')] From e580c384b89c89f6536cc3e2e6a72471b0139bbe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Dec 2023 12:46:06 -0800 Subject: [PATCH 09/33] import updates to rational from polysat Signed-off-by: Nikolaj Bjorner --- src/util/mpq.cpp | 6 ++++++ src/util/mpq.h | 8 ++++++++ src/util/mpz.cpp | 13 +++++++++++++ src/util/mpz.h | 7 +++++++ src/util/rational.h | 27 ++++++++++++++++++++++++++- 5 files changed, 60 insertions(+), 1 deletion(-) diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index 324750cfa..f90843e36 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -316,6 +316,12 @@ unsigned mpq_manager::prev_power_of_two(mpq const & a) { return prev_power_of_two(_tmp); } +template +unsigned mpq_manager::next_power_of_two(mpq const & a) { + _scoped_numeral > _tmp(*this); + ceil(a, _tmp); + return next_power_of_two(_tmp); +} template template diff --git a/src/util/mpq.h b/src/util/mpq.h index e254ade69..1bdf8f31b 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -848,6 +848,14 @@ public: unsigned prev_power_of_two(mpz const & a) { return mpz_manager::prev_power_of_two(a); } unsigned prev_power_of_two(mpq const & a); + /** + \brief Return the smallest k s.t. a <= 2^k. + + \remark Return 0 if a is not positive. + */ + unsigned next_power_of_two(mpz const & a) { return mpz_manager::next_power_of_two(a); } + unsigned next_power_of_two(mpq const & a); + bool is_int_perfect_square(mpq const & a, mpq & r) { SASSERT(is_int(a)); reset_denominator(r); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index c3ba30161..296b4426e 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -2288,6 +2288,19 @@ unsigned mpz_manager::bitsize(mpz const & a) { return mlog2(a) + 1; } +template +unsigned mpz_manager::next_power_of_two(mpz const & a) { + if (is_nonpos(a)) + return 0; + if (is_one(a)) + return 0; + unsigned shift; + if (is_power_of_two(a, shift)) + return shift; + else + return log2(a) + 1; +} + template bool mpz_manager::is_perfect_square(mpz const & a, mpz & root) { if (is_neg(a)) diff --git a/src/util/mpz.h b/src/util/mpz.h index a1bb19395..bb1141ea7 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -692,6 +692,13 @@ public: \remark Return 0 if a is not positive. */ unsigned prev_power_of_two(mpz const & a) { return log2(a); } + + /** + \brief Return the smallest k s.t. a <= 2^k. + + \remark Return 0 if a is not positive. + */ + unsigned next_power_of_two(mpz const & a); /** \brief Return true if a^{1/n} is an integer, and store the result in a. diff --git a/src/util/rational.h b/src/util/rational.h index f47fddefe..88a0552ba 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -55,7 +55,7 @@ public: explicit rational(double z) { UNREACHABLE(); } explicit rational(char const * v) { m().set(m_val, v); } - + explicit rational(unsigned const * v, unsigned sz) { m().set(m_val, sz, v); } struct i64 {}; @@ -489,6 +489,18 @@ public: return get_num_digits(rational(10)); } + /** + * \brief Return the biggest k s.t. 2^k <= a. + * \remark Return 0 if a is not positive. + */ + unsigned prev_power_of_two() const { return m().prev_power_of_two(m_val); } + + /** + * \brief Return the smallest k s.t. a <= 2^k. + * \remark Return 0 if a is not positive. + */ + unsigned next_power_of_two() const { return m().next_power_of_two(m_val); } + bool get_bit(unsigned index) const { return m().get_bit(m_val, index); } @@ -501,6 +513,15 @@ public: return k; } + /** Number of trailing zeros in an N-bit representation */ + unsigned parity(unsigned num_bits) const { + SASSERT(!is_neg()); + SASSERT(*this < rational::power_of_two(num_bits)); + if (is_zero()) + return num_bits; + return trailing_zeros(); + } + static bool limit_denominator(rational &num, rational const& limit); }; @@ -649,3 +670,7 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val); return result; } + +inline void swap(rational& r1, rational& r2) { + r1.swap(r2); +} From 70d4f32ffd56b2508bb2c2ae8bc37a8452561d5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Dec 2023 13:00:43 -0800 Subject: [PATCH 10/33] port updates from poly/polysat Signed-off-by: Nikolaj Bjorner --- src/util/dlist.h | 10 ++++++++++ src/util/var_queue.h | 2 ++ 2 files changed, 12 insertions(+) diff --git a/src/util/dlist.h b/src/util/dlist.h index e5c95b8cf..07aefa97e 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -223,6 +223,16 @@ public: } }; +template +class dll_elements { + T const* m_list; +public: + dll_elements(T const* list) : m_list(list) {} + dll_iterator begin() const { return dll_iterator::mk_begin(m_list); } + dll_iterator end() const { return dll_iterator::mk_end(m_list); } +}; + + template < typename T , typename U = std::enable_if_t, T>> // should only match if T actually inherits from dll_base > diff --git a/src/util/var_queue.h b/src/util/var_queue.h index 9807e5ac2..0af4de3b8 100644 --- a/src/util/var_queue.h +++ b/src/util/var_queue.h @@ -68,6 +68,8 @@ public: void reset() { m_queue.reset(); } + + bool contains(var v) const { return m_queue.contains(v); } bool empty() const { return m_queue.empty(); } From 91837c3aeeafb5a0d1c4a7e3225f572f99d17e39 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 10:22:35 -0800 Subject: [PATCH 11/33] try adding readme again Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index ef41051d8..8e67bd65e 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -149,7 +149,7 @@ class Env: unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) mk_icon(self.source_root) -# mk_readme(self.source_root) + mk_readme(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) def main(): From 5732c3c98031e51eb803839b637f5aba4aed25a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 11:11:37 -0800 Subject: [PATCH 12/33] add readme under content Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 8e67bd65e..fe06bdba2 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -91,7 +91,7 @@ def mk_icon(source_root): def mk_readme(source_root): mk_dir("out/content") - shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/README.md") + shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") @@ -112,6 +112,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg + content/README>md https://github.com/Z3Prover/z3 MIT @@ -121,6 +122,9 @@ Linux Dependencies: + + + """.format(version, repo, branch, commit, arch) print(contents) sym = "sym." if symbols else "" From 5fc039d6ea60e12bb319fa01c4b76e9818949596 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 12:33:29 -0800 Subject: [PATCH 13/33] nuget spec: does this work? Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index fe06bdba2..5e6d3e039 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -88,9 +88,6 @@ def mk_targets(source_root): def mk_icon(source_root): mk_dir("out/content") shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg") - -def mk_readme(source_root): - mk_dir("out/content") shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") @@ -124,6 +121,7 @@ Linux Dependencies: + """.format(version, repo, branch, commit, arch) print(contents) @@ -153,7 +151,6 @@ class Env: unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) mk_icon(self.source_root) - mk_readme(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) def main(): From 0f4e96ac5d76bbf860ee80a6d0943e0a5589db1b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 20:50:32 -0800 Subject: [PATCH 14/33] fix character Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 5e6d3e039..d3f402773 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -109,7 +109,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - content/README>md + content/README.md https://github.com/Z3Prover/z3 MIT From 3ebec56880ec7e1b55993ea80ef44a71d2dbf3d8 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Thu, 14 Dec 2023 00:36:41 +0700 Subject: [PATCH 15/33] tptr.h: Include `` once rather than twice. (#7051) --- src/util/tptr.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/tptr.h b/src/util/tptr.h index 50e9417fe..37b6f64fe 100644 --- a/src/util/tptr.h +++ b/src/util/tptr.h @@ -21,7 +21,6 @@ Revision History: #include #include "util/machine.h" -#include #define TAG_SHIFT PTR_ALIGNMENT #define ALIGNMENT_VALUE (1 << PTR_ALIGNMENT) From 8293be859f0b8eb4c2b818f245c912864e79bde0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Dec 2023 02:05:33 +0000 Subject: [PATCH 16/33] Disable Python compilation cache during build (#7052) * Disable Python compilation cache during build * Fix var name --- scripts/mk_util.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0728c2cb7..90271321b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2994,9 +2994,16 @@ def cp_z3py_to_build(): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) + # We do not want a second copy of the compiled files in the system-wide cache, + # so we disable it temporarily. This is an issue with recent versions of MacOS + # where XCode's Python has a cache, but the build scripts don't have access to + # it (e.g. during OPAM package installation). + pycache_prefix_before = sys.pycache_prefix + sys.pycache_prefix = None # Compile Z3Py files if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") + sys.pycache_prefix = pycache_prefix_before if is_verbose: print("Generated python bytecode") # Copy sources to build From 995b40865b868511f8e627b7728c07b9d35520c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 18:44:11 -0800 Subject: [PATCH 17/33] remove readme reference, add arm64 build to nightly Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 7 +----- scripts/nightly.yaml | 46 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 47 insertions(+), 6 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index d3f402773..58251c6f8 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -88,7 +88,7 @@ def mk_targets(source_root): def mk_icon(source_root): mk_dir("out/content") shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg") - shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") +# shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") @@ -109,7 +109,6 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - content/README.md https://github.com/Z3Prover/z3 MIT @@ -119,10 +118,6 @@ Linux Dependencies: - - - - """.format(version, repo, branch, commit, arch) print(contents) sym = "sym." if symbols else "" diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 2b1b4ca3d..ad7f19a9c 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -233,6 +233,47 @@ stages: symbolServerType: TeamServices detailedLog: true +- job: "WindowsArm64" + displayName: "Windows" + pool: + vmImage: "windows-latest" + variables: + arch: "amd64_arm64" + steps: + - script: md build + - script: | + cd build + call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch) + cmake $(bindings) -G "NMake Makefiles" ../ + nmake + cd .. + - task: CopyFiles@2 + inputs: + sourceFolder: build + contents: '*.zip' + targetFolder: $(Build.ArtifactStagingDirectory) + - task: PublishPipelineArtifact@1 + inputs: + targetPath: $(Build.ArtifactStagingDirectory) + artifactName: 'WindowsArm64' + - task: CopyFiles@2 + displayName: 'Collect Symbols' + inputs: + sourceFolder: build + contents: '**/*.pdb' + targetFolder: '$(Build.ArtifactStagingDirectory)/symbols' + # Publish symbol archive to match nuget package + # Index your source code and publish symbols to a file share or Azure Artifacts symbol server + - task: PublishSymbols@2 + inputs: + symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols' + searchPattern: '**/*.pdb' + indexSources: false # Github not supported + publishSymbols: true + symbolServerType: TeamServices + detailedLog: true + + - stage: Package jobs: - job: NuGet64 @@ -534,6 +575,11 @@ stages: inputs: artifactName: 'Windows32' targetPath: tmp + - task: DownloadPipelineArtifact@2 + displayName: "Download windowsArm64" + inputs: + artifactName: 'WindowsArm64' + targetPath: tmp - task: DownloadPipelineArtifact@2 displayName: "Download windows64" inputs: From c20b8cb9788bc445600c637e763c9c37e0fb6c57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 18:46:20 -0800 Subject: [PATCH 18/33] nightly Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index ad7f19a9c..4de95339c 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -233,13 +233,13 @@ stages: symbolServerType: TeamServices detailedLog: true -- job: "WindowsArm64" - displayName: "Windows" - pool: - vmImage: "windows-latest" - variables: - arch: "amd64_arm64" - steps: + - job: "WindowsArm64" + displayName: "Windows" + pool: + vmImage: "windows-latest" + variables: + arch: "amd64_arm64" + steps: - script: md build - script: | cd build From b40e3015efe5092e072a85cc41770e3a946e06ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 19:25:18 -0800 Subject: [PATCH 19/33] fix #7053 --- src/opt/opt_solver.cpp | 4 ++-- src/smt/theory_arith_pp.h | 6 ++++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index ee91b06a4..955025fd9 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -52,7 +52,7 @@ namespace opt { if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { m_params.m_relevancy_lvl = 0; } - m_params.m_arith_auto_config_simplex = false; + m_params.m_arith_auto_config_simplex = true; m_params.m_threads = 1; // need to interact with the solver that created model so can't have threads // m_params.m_auto_config = false; } @@ -67,7 +67,7 @@ namespace opt { m_dump_benchmarks = p.dump_benchmarks(); m_params.updt_params(_p); m_context.updt_params(_p); - m_params.m_arith_auto_config_simplex = false; + m_params.m_arith_auto_config_simplex = true; } solver* opt_solver::translate(ast_manager& m, params_ref const& p) { diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index b0d43bc00..edc640d86 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -83,9 +83,11 @@ namespace smt { template void theory_arith::display_row(std::ostream & out, row const & r, bool compact) const { - + if (static_cast(r.get_base_var()) >= m_columns.size()) + return; column const & c = m_columns[r.get_base_var()]; - out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : "; + if (c.size() > 0) + out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : "; bool first = true; for (auto const& e : r) { if (!e.is_dead()) { From f7d9a5ba935163ddefd3e1883878556d713d6fee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 19:32:00 -0800 Subject: [PATCH 20/33] Revert "Disable Python compilation cache during build (#7052)" (#7054) This reverts commit 8293be859f0b8eb4c2b818f245c912864e79bde0. --- scripts/mk_util.py | 7 ------- 1 file changed, 7 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 90271321b..0728c2cb7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2994,16 +2994,9 @@ def cp_z3py_to_build(): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) - # We do not want a second copy of the compiled files in the system-wide cache, - # so we disable it temporarily. This is an issue with recent versions of MacOS - # where XCode's Python has a cache, but the build scripts don't have access to - # it (e.g. during OPAM package installation). - pycache_prefix_before = sys.pycache_prefix - sys.pycache_prefix = None # Compile Z3Py files if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") - sys.pycache_prefix = pycache_prefix_before if is_verbose: print("Generated python bytecode") # Copy sources to build From 7c2e4f2f9c546ee0b8ed241c7ea85a903b2b7c38 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 20:43:17 -0800 Subject: [PATCH 21/33] fiddle with what gets added to win-arm64 Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 4de95339c..0f5337654 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -234,11 +234,12 @@ stages: detailedLog: true - job: "WindowsArm64" - displayName: "Windows" + displayName: "WindowsArm64" pool: vmImage: "windows-latest" variables: arch: "amd64_arm64" + bindings: "-DCMAKE_BUILD_TYPE=RelWithDebInfo" steps: - script: md build - script: | @@ -250,7 +251,7 @@ stages: - task: CopyFiles@2 inputs: sourceFolder: build - contents: '*.zip' + contents: '*z3*.*' targetFolder: $(Build.ArtifactStagingDirectory) - task: PublishPipelineArtifact@1 inputs: From a2b490baa6f092be60d9797e7ddbeabe37b2671f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Dec 2023 15:26:52 +0000 Subject: [PATCH 22/33] Disable Python compilation cache during build (#7057) * Disable Python compilation cache during build * More pythonic check for none --- scripts/mk_util.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0728c2cb7..014b0e40f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2994,9 +2994,19 @@ def cp_z3py_to_build(): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) + # We do not want a second copy of the compiled files in the system-wide cache, + # so we disable it temporarily. This is an issue with recent versions of MacOS + # where XCode's Python has a cache, but the build scripts don't have access to + # it (e.g. during OPAM package installation). + have_cache = hasattr(sys, 'pycache_prefix') and sys.pycache_prefix is not None + if have_cache: + pycache_prefix_before = sys.pycache_prefix + sys.pycache_prefix = None # Compile Z3Py files if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") + if have_cache: + sys.pycache_prefix = pycache_prefix_before if is_verbose: print("Generated python bytecode") # Copy sources to build From e90a84450859038ce5c97d51dca833de03f19ae6 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 15 Dec 2023 15:44:57 +0700 Subject: [PATCH 23/33] Use `override` more. (#7059) --- src/ast/simplifiers/dependent_expr_state.h | 16 ++++++++-------- src/ast/simplifiers/model_reconstruction_trail.h | 2 +- src/math/lp/lar_solver.cpp | 2 +- src/solver/simplifier_solver.cpp | 2 +- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 165cbbce0..e187f19c6 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -105,14 +105,14 @@ public: class default_dependent_expr_state : public dependent_expr_state { public: default_dependent_expr_state(ast_manager& m): dependent_expr_state(m) {} - virtual unsigned qtail() const { return 0; } - virtual dependent_expr const& operator[](unsigned i) { throw default_exception("unexpected access"); } - virtual void update(unsigned i, dependent_expr const& j) { throw default_exception("unexpected update"); } - virtual void add(dependent_expr const& j) { throw default_exception("unexpected addition"); } - virtual bool inconsistent() { return false; } - virtual model_reconstruction_trail& model_trail() { throw default_exception("unexpected access to model reconstruction"); } - virtual bool updated() { return false; } - virtual void reset_updated() {} + unsigned qtail() const override { return 0; } + dependent_expr const& operator[](unsigned i) override { throw default_exception("unexpected access"); } + void update(unsigned i, dependent_expr const& j) override { throw default_exception("unexpected update"); } + void add(dependent_expr const& j) override { throw default_exception("unexpected addition"); } + bool inconsistent() override { return false; } + model_reconstruction_trail& model_trail() override { throw default_exception("unexpected access to model reconstruction"); } + bool updated() override { return false; } + void reset_updated() override {} }; diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index 79a38401a..c2d8b0001 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -90,7 +90,7 @@ class model_reconstruction_trail { struct undo_model_var : public trail { model_reconstruction_trail& s; undo_model_var(model_reconstruction_trail& s) : s(s) {} - virtual void undo() { + void undo() override { s.m_model_vars.mark(s.m_model_vars_trail.back(), false); s.m_model_vars_trail.pop_back(); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 15d03fb86..a55edfe35 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1490,7 +1490,7 @@ namespace lp { struct lar_solver::undo_add_column : public trail { lar_solver& s; undo_add_column(lar_solver& s) : s(s) {} - virtual void undo() { + void undo() override { s.remove_last_column_from_tableau(); s.m_columns_to_ul_pairs.pop_back(); unsigned j = s.m_columns_to_ul_pairs.size(); diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 712c42f45..7debe6bc0 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -39,7 +39,7 @@ class simplifier_solver : public solver { bool m_updated = false; dep_expr_state(simplifier_solver& s) :dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {} ~dep_expr_state() override {} - virtual unsigned qtail() const override { return s.m_fmls.size(); } + unsigned qtail() const override { return s.m_fmls.size(); } dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; } void update(unsigned i, dependent_expr const& j) override { SASSERT(j.fml()); From 2e83352d425f8fc8b357a48ae536fafb4edc6417 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 15 Dec 2023 16:34:27 +0000 Subject: [PATCH 24/33] Fix bug in fp.round_to_integral (#7060) --- src/ast/fpa/fpa2bv_converter.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 4267a6eed..25a0e77ad 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2189,7 +2189,13 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & renorm_delta = m.mk_ite(m_bv_util.mk_ule(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2); SASSERT(m_bv_util.get_bv_size(renorm_delta) == ebits + 2); res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta); - res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta)); + if (sbits >= ebits+2) + res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta)); + else { + // should not overflow because renorm_delta is logarithmic to the size of the leading zero bits + res_sig = m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(ebits+2-sbits, res_sig), renorm_delta); + res_sig = m_bv_util.mk_extract(sbits-1, 0, res_sig); + } dbg_decouple("fpa2bv_r2i_renorm_delta", renorm_delta); dbg_decouple("fpa2bv_r2i_sig_lz", sig_lz); dbg_decouple("fpa2bv_r2i_sig_lz_capped", sig_lz_capped); From 0520558fc0e18979d79935c3630ad5bde09a1dae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 08:53:58 -0800 Subject: [PATCH 25/33] port updated pdd from polysat Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 160 +++++++++++++++++++++++++----------- src/math/dd/dd_pdd.h | 180 +++++++++++++++++++++++++---------------- 2 files changed, 222 insertions(+), 118 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 970eb991f..55156c53a 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -113,11 +113,34 @@ namespace dd { pdd pdd_manager::add(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_add_op), this); } pdd pdd_manager::zero() { return pdd(zero_pdd, this); } pdd pdd_manager::one() { return pdd(one_pdd, this); } - - pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { return p + q - (p*q); } - pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) { if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; } - pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { pdd q(mk_val(x)); if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; } - pdd pdd_manager::mk_not(pdd const& p) { return 1 - p; } + + // NOTE: bit-wise AND cannot be expressed in mod2N_e semantics with the existing operations. + pdd pdd_manager::mk_and(pdd const& p, pdd const& q) { + VERIFY(m_semantics == mod2_e || m_semantics == zero_one_vars_e); + return p * q; + } + + pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { + return p + q - mk_and(p, q); + } + + pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) { + if (m_semantics == mod2_e) + return p + q; + return p + q - 2*mk_and(p, q); + } + + pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { + pdd q(mk_val(x)); + return mk_xor(p, q); + } + + pdd pdd_manager::mk_not(pdd const& p) { + if (m_semantics == mod2N_e) + return -p - 1; + VERIFY(m_semantics == mod2_e || m_semantics == zero_one_vars_e); + return 1 - p; + } pdd pdd_manager::subst_val(pdd const& p, unsigned v, rational const& val) { pdd r = mk_var(v) + val; @@ -173,15 +196,8 @@ namespace dd { if (m_semantics != mod2N_e) return 0; - if (is_val(p)) { - rational v = val(p); - if (v.is_zero()) - return m_power_of_2 + 1; - unsigned r = 0; - while (v.is_even() && v > 0) - r++, v /= 2; - return r; - } + if (is_val(p)) + return val(p).parity(m_power_of_2); init_mark(); PDD q = p; m_todo.push_back(hi(q)); @@ -189,9 +205,9 @@ namespace dd { q = lo(q); m_todo.push_back(hi(q)); } - unsigned p2 = val(q).trailing_zeros(); + unsigned parity = val(q).parity(m_power_of_2); init_mark(); - while (p2 != 0 && !m_todo.empty()) { + while (parity != 0 && !m_todo.empty()) { PDD r = m_todo.back(); m_todo.pop_back(); if (is_marked(r)) @@ -203,11 +219,11 @@ namespace dd { } else if (val(r).is_zero()) continue; - else if (val(r).trailing_zeros() < p2) - p2 = val(r).trailing_zeros(); + else + parity = std::min(parity, val(r).trailing_zeros()); } m_todo.reset(); - return p2; + return parity; } pdd pdd_manager::subst_val(pdd const& p, pdd const& s) { @@ -246,7 +262,7 @@ namespace dd { } pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) { - bool first = true; + unsigned count = 0; SASSERT(well_formed()); scoped_push _sp(*this); while (true) { @@ -255,8 +271,9 @@ namespace dd { } catch (const mem_out &) { try_gc(); - if (!first) throw; - first = false; + if (count > 0) + m_max_num_nodes *= 2; + count++; } } SASSERT(well_formed()); @@ -507,7 +524,7 @@ namespace dd { if (m_semantics == mod2_e) { return a; } - bool first = true; + unsigned count = 0; SASSERT(well_formed()); scoped_push _sp(*this); while (true) { @@ -516,8 +533,9 @@ namespace dd { } catch (const mem_out &) { try_gc(); - if (!first) throw; - first = false; + if (count > 0) + m_max_num_nodes *= 2; + ++count; } } SASSERT(well_formed()); @@ -565,7 +583,7 @@ namespace dd { return true; } SASSERT(c.is_int()); - bool first = true; + unsigned count = 0; SASSERT(well_formed()); scoped_push _sp(*this); while (true) { @@ -578,8 +596,9 @@ namespace dd { } catch (const mem_out &) { try_gc(); - if (!first) throw; - first = false; + if (count > 0) + m_max_num_nodes *= 2; + ++count; } } } @@ -1138,6 +1157,7 @@ namespace dd { unsigned pdd_manager::max_pow2_divisor(PDD p) { init_mark(); unsigned min_j = UINT_MAX; + SASSERT(m_todo.empty()); m_todo.push_back(p); while (!m_todo.empty()) { PDD r = m_todo.back(); @@ -1785,27 +1805,42 @@ namespace dd { } pdd& pdd::operator=(pdd const& other) { + if (m != other.m) { + verbose_stream() << "pdd manager confusion: " << *this << " (mod 2^" << power_of_2() << ") := " << other << " (mod 2^" << other.power_of_2() << ")\n"; + // TODO: in the end, this operator should probably be changed to also update the manager. But for now I want to detect such confusions. + } + SASSERT_EQ(power_of_2(), other.power_of_2()); + VERIFY_EQ(power_of_2(), other.power_of_2()); + VERIFY_EQ(m, other.m); unsigned r1 = root; root = other.root; - m.inc_ref(root); - m.dec_ref(r1); + m->inc_ref(root); + m->dec_ref(r1); return *this; } pdd& pdd::operator=(unsigned k) { - m.dec_ref(root); - root = m.mk_val(k).root; - m.inc_ref(root); + m->dec_ref(root); + root = m->mk_val(k).root; + m->inc_ref(root); return *this; } pdd& pdd::operator=(rational const& k) { - m.dec_ref(root); - root = m.mk_val(k).root; - m.inc_ref(root); + m->dec_ref(root); + root = m->mk_val(k).root; + m->inc_ref(root); return *this; } + /* Reset pdd to 0. Allows re-assigning the pdd manager. */ + void pdd::reset(pdd_manager& new_m) { + m->dec_ref(root); + root = 0; + m = &new_m; + SASSERT(is_zero()); + } + rational const& pdd::leading_coefficient() const { pdd p = *this; while (!p.is_val()) @@ -1813,11 +1848,10 @@ namespace dd { return p.val(); } - rational const& pdd::offset() const { - pdd p = *this; - while (!p.is_val()) - p = p.lo(); - return p.val(); + rational const& pdd_manager::offset(PDD p) const { + while (!is_val(p)) + p = lo(p); + return val(p); } pdd pdd::shl(unsigned n) const { @@ -1831,7 +1865,7 @@ namespace dd { pdd pdd::subst_pdd(unsigned v, pdd const& r) const { if (is_val()) return *this; - if (m.m_var2level[var()] < m.m_var2level[v]) + if (m->m_var2level[var()] < m->m_var2level[v]) return *this; pdd l = lo().subst_pdd(v, r); pdd h = hi().subst_pdd(v, r); @@ -1840,7 +1874,7 @@ namespace dd { else if (l == lo() && h == hi()) return *this; else - return m.mk_var(var())*h + l; + return m->mk_var(var())*h + l; } std::pair pdd::var_factors() const { @@ -1871,7 +1905,7 @@ namespace dd { ++i; ++j; } - else if (m.m_var2level[lo_vars[i]] > m.m_var2level[hi_vars[j]]) + else if (m->m_var2level[lo_vars[i]] > m->m_var2level[hi_vars[j]]) hi_vars[jr++] = hi_vars[j++]; else lo_vars[ir++] = lo_vars[i++]; @@ -1882,7 +1916,7 @@ namespace dd { auto mul = [&](unsigned_vector const& vars, pdd p) { for (auto v : vars) - p *= m.mk_var(v); + p *= m->mk_var(v); return p; }; @@ -1908,7 +1942,7 @@ namespace dd { std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); } void pdd_iterator::next() { - auto& m = m_pdd.m; + auto& m = m_pdd.manager(); while (!m_nodes.empty()) { auto& p = m_nodes.back(); if (p.first && !m.is_val(p.second)) { @@ -1935,13 +1969,16 @@ namespace dd { void pdd_iterator::first() { unsigned n = m_pdd.root; - auto& m = m_pdd.m; + auto& m = m_pdd.manager(); while (!m.is_val(n)) { m_nodes.push_back(std::make_pair(true, n)); m_mono.vars.push_back(m.var(n)); n = m.hi(n); } m_mono.coeff = m.val(n); + // if m_pdd is constant and non-zero, the iterator should return a single monomial + if (m_nodes.empty() && !m_mono.coeff.is_zero()) + m_nodes.push_back(std::make_pair(false, n)); } pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); } @@ -1960,5 +1997,32 @@ namespace dd { return out; } + void pdd_linear_iterator::first() { + m_next = m_pdd.root; + next(); + } -} + void pdd_linear_iterator::next() { + SASSERT(m_next != pdd_manager::null_pdd); + auto& m = m_pdd.manager(); + while (!m.is_val(m_next)) { + unsigned const var = m.var(m_next); + rational const val = m.offset(m.hi(m_next)); + m_next = m.lo(m_next); + if (!val.is_zero()) { + m_mono = {val, var}; + return; + } + } + m_next = pdd_manager::null_pdd; + } + + pdd_linear_iterator pdd::pdd_linear_monomials::begin() const { + return pdd_linear_iterator(m_pdd, true); + } + + pdd_linear_iterator pdd::pdd_linear_monomials::end() const { + return pdd_linear_iterator(m_pdd, false); + } + +} // namespace dd diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index f2547e962..2dc9a9480 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -45,6 +45,7 @@ namespace dd { class pdd; class pdd_manager; class pdd_iterator; + class pdd_linear_iterator; class pdd_manager { public: @@ -53,13 +54,14 @@ namespace dd { friend test; friend pdd; friend pdd_iterator; + friend pdd_linear_iterator; typedef unsigned PDD; typedef vector> monomials_t; - const PDD null_pdd = UINT_MAX; - const PDD zero_pdd = 0; - const PDD one_pdd = 1; + static constexpr PDD null_pdd = UINT_MAX; + static constexpr PDD zero_pdd = 0; + static constexpr PDD one_pdd = 1; enum pdd_op { pdd_add_op = 2, @@ -261,6 +263,7 @@ namespace dd { inline PDD lo(PDD p) const { return m_nodes[p].m_lo; } inline PDD hi(PDD p) const { return m_nodes[p].m_hi; } inline rational const& val(PDD p) const { SASSERT(is_val(p)); return m_values[lo(p)]; } + inline rational get_signed_val(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); rational const& a = val(p); return a.get_bit(power_of_2() - 1) ? a - two_to_N() : a; } inline void inc_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount++; SASSERT(!m_free_nodes.contains(p)); } inline void dec_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount--; SASSERT(!m_free_nodes.contains(p)); } inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; } @@ -341,9 +344,10 @@ namespace dd { pdd mul(rational const& c, pdd const& b); pdd div(pdd const& a, rational const& c); bool try_div(pdd const& a, rational const& c, pdd& out_result); + pdd mk_and(pdd const& p, pdd const& q); pdd mk_or(pdd const& p, pdd const& q); pdd mk_xor(pdd const& p, pdd const& q); - pdd mk_xor(pdd const& p, unsigned q); + pdd mk_xor(pdd const& p, unsigned x); pdd mk_not(pdd const& p); pdd reduce(pdd const& a, pdd const& b); pdd subst_val0(pdd const& a, vector> const& s); @@ -368,6 +372,8 @@ namespace dd { bool is_univariate_in(PDD p, unsigned v); void get_univariate_coefficients(PDD p, vector& coeff); + rational const& offset(PDD p) const; + // create an spoly r if leading monomials of a and b overlap bool try_spoly(pdd const& a, pdd const& b, pdd& r); @@ -399,106 +405,120 @@ namespace dd { friend test; friend class pdd_manager; friend class pdd_iterator; + friend class pdd_linear_iterator; unsigned root; - pdd_manager& m; - pdd(unsigned root, pdd_manager& m): root(root), m(m) { m.inc_ref(root); } - pdd(unsigned root, pdd_manager* _m): root(root), m(*_m) { m.inc_ref(root); } + pdd_manager* m; + pdd(unsigned root, pdd_manager& pm): root(root), m(&pm) { m->inc_ref(root); } + pdd(unsigned root, pdd_manager* pm): root(root), m(pm) { m->inc_ref(root); } public: - pdd(pdd_manager& pm): root(0), m(pm) { SASSERT(is_zero()); } - pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); } - pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); } + pdd(pdd_manager& m): pdd(0, m) { SASSERT(is_zero()); } + pdd(pdd const& other): pdd(other.root, other.m) { m->inc_ref(root); } + pdd(pdd && other) noexcept : pdd(0, other.m) { std::swap(root, other.root); } pdd& operator=(pdd const& other); pdd& operator=(unsigned k); pdd& operator=(rational const& k); - ~pdd() { m.dec_ref(root); } - pdd lo() const { return pdd(m.lo(root), m); } - pdd hi() const { return pdd(m.hi(root), m); } + // TODO: pdd& operator=(pdd&& other); (just swap like move constructor?) + ~pdd() { m->dec_ref(root); } + void reset(pdd_manager& new_m); + pdd lo() const { return pdd(m->lo(root), m); } + pdd hi() const { return pdd(m->hi(root), m); } unsigned index() const { return root; } - unsigned var() const { return m.var(root); } - rational const& val() const { SASSERT(is_val()); return m.val(root); } + unsigned var() const { return m->var(root); } + rational const& val() const { return m->val(root); } + rational get_signed_val() const { return m->get_signed_val(root); } rational const& leading_coefficient() const; - rational const& offset() const; - bool is_val() const { return m.is_val(root); } - bool is_one() const { return m.is_one(root); } - bool is_zero() const { return m.is_zero(root); } - bool is_linear() const { return m.is_linear(root); } - bool is_var() const { return m.is_var(root); } - bool is_max() const { return m.is_max(root); } + rational const& offset() const { return m->offset(root); } + bool is_val() const { return m->is_val(root); } + bool is_one() const { return m->is_one(root); } + bool is_zero() const { return m->is_zero(root); } + bool is_linear() const { return m->is_linear(root); } + bool is_var() const { return m->is_var(root); } + bool is_max() const { return m->is_max(root); } /** Polynomial is of the form a * x + b for some numerals a, b. */ bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); } /** Polynomial is of the form a * x for some numeral a. */ bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); } - bool is_binary() const { return m.is_binary(root); } - bool is_monomial() const { return m.is_monomial(root); } - bool is_univariate() const { return m.is_univariate(root); } - bool is_univariate_in(unsigned v) const { return m.is_univariate_in(root, v); } - void get_univariate_coefficients(vector& coeff) const { m.get_univariate_coefficients(root, coeff); } - vector get_univariate_coefficients() const { vector coeff; m.get_univariate_coefficients(root, coeff); return coeff; } - bool is_never_zero() const { return m.is_never_zero(root); } - unsigned min_parity() const { return m.min_parity(root); } - bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); } + bool is_binary() const { return m->is_binary(root); } + bool is_monomial() const { return m->is_monomial(root); } + bool is_univariate() const { return m->is_univariate(root); } + bool is_univariate_in(unsigned v) const { return m->is_univariate_in(root, v); } + void get_univariate_coefficients(vector& coeff) const { m->get_univariate_coefficients(root, coeff); } + vector get_univariate_coefficients() const { vector coeff; m->get_univariate_coefficients(root, coeff); return coeff; } + bool is_never_zero() const { return m->is_never_zero(root); } + unsigned min_parity() const { return m->min_parity(root); } + bool var_is_leaf(unsigned v) const { return m->var_is_leaf(root, v); } - pdd operator-() const { return m.minus(*this); } - pdd operator+(pdd const& other) const { return m.add(*this, other); } - pdd operator-(pdd const& other) const { return m.sub(*this, other); } - pdd operator*(pdd const& other) const { return m.mul(*this, other); } - pdd operator&(pdd const& other) const { return m.mul(*this, other); } - pdd operator|(pdd const& other) const { return m.mk_or(*this, other); } - pdd operator^(pdd const& other) const { return m.mk_xor(*this, other); } - pdd operator^(unsigned other) const { return m.mk_xor(*this, other); } + pdd operator-() const { return m->minus(*this); } + pdd operator+(pdd const& other) const { VERIFY_EQ(m, other.m); return m->add(*this, other); } + pdd operator-(pdd const& other) const { VERIFY_EQ(m, other.m); return m->sub(*this, other); } + pdd operator*(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mul(*this, other); } + pdd operator&(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mk_and(*this, other); } + pdd operator|(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mk_or(*this, other); } + pdd operator^(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mk_xor(*this, other); } + pdd operator^(unsigned other) const { return m->mk_xor(*this, m->mk_val(other)); } - pdd operator*(rational const& other) const { return m.mul(other, *this); } - pdd operator+(rational const& other) const { return m.add(other, *this); } - pdd operator~() const { return m.mk_not(*this); } + pdd operator*(rational const& other) const { return m->mul(other, *this); } + pdd operator+(rational const& other) const { return m->add(other, *this); } + pdd operator~() const { return m->mk_not(*this); } pdd shl(unsigned n) const; - pdd rev_sub(rational const& r) const { return m.sub(m.mk_val(r), *this); } - pdd div(rational const& other) const { return m.div(*this, other); } - bool try_div(rational const& other, pdd& out_result) const { return m.try_div(*this, other, out_result); } - pdd pow(unsigned j) const { return m.pow(*this, j); } - pdd reduce(pdd const& other) const { return m.reduce(*this, other); } - bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); } - void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { m.factor(*this, v, degree, lc, rest); } - bool factor(unsigned v, unsigned degree, pdd& lc) const { return m.factor(*this, v, degree, lc); } - bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); } - pdd reduce(unsigned v, pdd const& other) const { return m.reduce(v, *this, other); } + pdd rev_sub(rational const& r) const { return m->sub(m->mk_val(r), *this); } + pdd div(rational const& other) const { return m->div(*this, other); } + bool try_div(rational const& other, pdd& out_result) const { VERIFY_EQ(m, out_result.m); return m->try_div(*this, other, out_result); } + pdd pow(unsigned j) const { return m->pow(*this, j); } + pdd reduce(pdd const& other) const { VERIFY_EQ(m, other.m); return m->reduce(*this, other); } + bool different_leading_term(pdd const& other) const { VERIFY_EQ(m, other.m); return m->different_leading_term(*this, other); } + void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { VERIFY_EQ(m, lc.m); VERIFY_EQ(m, rest.m); m->factor(*this, v, degree, lc, rest); } + bool factor(unsigned v, unsigned degree, pdd& lc) const { VERIFY_EQ(m, lc.m); return m->factor(*this, v, degree, lc); } + bool resolve(unsigned v, pdd const& other, pdd& result) { VERIFY_EQ(m, other.m); VERIFY_EQ(m, result.m); return m->resolve(v, *this, other, result); } + pdd reduce(unsigned v, pdd const& other) const { VERIFY_EQ(m, other.m); return m->reduce(v, *this, other); } /** * \brief factor out variables */ std::pair var_factors() const; - pdd subst_val0(vector> const& s) const { return m.subst_val0(*this, s); } - pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); } - pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); } - pdd subst_add(unsigned var, rational const& val) const { return m.subst_add(*this, var, val); } - bool subst_get(unsigned var, rational& out_val) const { return m.subst_get(*this, var, out_val); } + pdd subst_val0(vector> const& s) const { return m->subst_val0(*this, s); } + pdd subst_val(pdd const& s) const { VERIFY_EQ(m, s.m); return m->subst_val(*this, s); } + pdd subst_val(unsigned v, rational const& val) const { return m->subst_val(*this, v, val); } + pdd subst_add(unsigned var, rational const& val) const { return m->subst_add(*this, var, val); } + bool subst_get(unsigned var, rational& out_val) const { return m->subst_get(*this, var, out_val); } /** * \brief substitute variable v by r. */ pdd subst_pdd(unsigned v, pdd const& r) const; - std::ostream& display(std::ostream& out) const { return m.display(out, *this); } - bool operator==(pdd const& other) const { return root == other.root; } - bool operator!=(pdd const& other) const { return root != other.root; } + std::ostream& display(std::ostream& out) const { return m->display(out, *this); } + bool operator==(pdd const& other) const { return root == other.root && m == other.m; } + bool operator!=(pdd const& other) const { return !operator==(other); } unsigned hash() const { return root; } - unsigned power_of_2() const { return m.power_of_2(); } + unsigned power_of_2() const { return m->power_of_2(); } - unsigned dag_size() const { return m.dag_size(*this); } - double tree_size() const { return m.tree_size(*this); } - unsigned degree() const { return m.degree(*this); } - unsigned degree(unsigned v) const { return m.degree(root, v); } - unsigned max_pow2_divisor() const { return m.max_pow2_divisor(root); } - unsigned_vector const& free_vars() const { return m.free_vars(*this); } + unsigned dag_size() const { return m->dag_size(*this); } + double tree_size() const { return m->tree_size(*this); } + unsigned degree() const { return m->degree(*this); } + unsigned degree(unsigned v) const { return m->degree(root, v); } + unsigned max_pow2_divisor() const { return m->max_pow2_divisor(root); } + unsigned_vector const& free_vars() const { return m->free_vars(*this); } - void swap(pdd& other) { std::swap(root, other.root); } + void swap(pdd& other) { VERIFY_EQ(m, other.m); std::swap(root, other.root); } pdd_iterator begin() const; pdd_iterator end() const; - pdd_manager& manager() const { return m; } + class pdd_linear_monomials { + friend class pdd; + pdd const& m_pdd; + pdd_linear_monomials(pdd const& p): m_pdd(p) {} + public: + pdd_linear_iterator begin() const; + pdd_linear_iterator end() const; + }; + pdd_linear_monomials linear_monomials() const { return pdd_linear_monomials(*this); } + + pdd_manager& manager() const { return *m; } }; inline pdd operator*(rational const& r, pdd const& b) { return b * r; } @@ -552,7 +572,27 @@ namespace dd { pdd_iterator& operator++() { next(); return *this; } pdd_iterator operator++(int) { auto tmp = *this; next(); return tmp; } bool operator==(pdd_iterator const& other) const { return m_nodes == other.m_nodes; } - bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; } + bool operator!=(pdd_iterator const& other) const { return !operator==(other); } + }; + + class pdd_linear_iterator { + friend class pdd::pdd_linear_monomials; + pdd m_pdd; + std::pair m_mono; + pdd_manager::PDD m_next = pdd_manager::null_pdd; + pdd_linear_iterator(pdd const& p, bool at_start): m_pdd(p) { if (at_start) first(); } + void first(); + void next(); + public: + using value_type = std::pair; // coefficient and variable + using reference = value_type const&; + using pointer = value_type const*; + reference operator*() const { return m_mono; } + pointer operator->() const { return &m_mono; } + pdd_linear_iterator& operator++() { next(); return *this; } + pdd_linear_iterator operator++(int) { auto tmp = *this; next(); return tmp; } + bool operator==(pdd_linear_iterator const& other) const { return m_next == other.m_next; } + bool operator!=(pdd_linear_iterator const& other) const { return m_next != other.m_next; } }; class val_pp { From 9293923b8adb69f9775e7cce53ed17b032730fb6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 13:50:38 -0800 Subject: [PATCH 26/33] Add intblast solver --- RELEASE_NOTES.md | 6 + src/ast/arith_decl_plugin.cpp | 31 +- src/ast/arith_decl_plugin.h | 65 +- src/ast/bv_decl_plugin.cpp | 5 + src/ast/bv_decl_plugin.h | 29 + src/ast/euf/euf_bv_plugin.cpp | 7 +- src/math/dd/dd_pdd.cpp | 2 + src/math/lp/lp_api.h | 2 + src/sat/sat_solver.cpp | 21 +- src/sat/smt/CMakeLists.txt | 2 + src/sat/smt/arith_axioms.cpp | 74 ++ src/sat/smt/arith_internalize.cpp | 6 + src/sat/smt/arith_solver.cpp | 33 +- src/sat/smt/arith_solver.h | 6 + src/sat/smt/arith_value.cpp | 145 ++++ src/sat/smt/arith_value.h | 52 ++ src/sat/smt/dt_solver.cpp | 2 +- src/sat/smt/euf_internalize.cpp | 1 - src/sat/smt/euf_model.cpp | 5 +- src/sat/smt/euf_solver.cpp | 42 +- src/sat/smt/euf_solver.h | 3 + src/sat/smt/intblast_solver.cpp | 985 +++++++++++++++++++++++++++ src/sat/smt/intblast_solver.h | 143 ++++ src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_bv_params.cpp | 2 + src/smt/params/theory_bv_params.h | 1 + src/smt/theory_datatype.cpp | 2 +- src/util/trail.h | 6 +- 28 files changed, 1621 insertions(+), 58 deletions(-) create mode 100644 src/sat/smt/arith_value.cpp create mode 100644 src/sat/smt/arith_value.h create mode 100644 src/sat/smt/intblast_solver.cpp create mode 100644 src/sat/smt/intblast_solver.h diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 9a7bc1856..a10af72a6 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -12,6 +12,12 @@ Version 4.next Version 4.12.5 ============== +- Fixes to pypi setup and build for MacOS distributions +- A new theory solver "int-blast" enabled by using: + - sat.smt=true smt.bv.solver=2 + - It solves a few bit-vector problems not handled by bit-blasting, especially if the bit-widths are large. + - It is based on encoding bit-vector constraints to non-linear integer arithemtic. + Version 4.12.4 ============== diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index ba2b4b4a7..8317b37c3 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -523,6 +523,12 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); } + if (k == OP_ARITH_BAND) { + if (arity != 2 || domain[0] != m_int_decl || domain[1] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) + m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer"); + return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl, + func_decl_info(m_family_id, k, num_parameters, parameters)); + } if (m_manager->int_real_coercions() && use_coercion(k)) { return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl)); @@ -548,6 +554,14 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); } + if (k == OP_ARITH_BAND) { + if (num_args != 2 || args[0]->get_sort() != m_int_decl || args[1]->get_sort() != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) + m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer"); + sort* domain[2] = { m_int_decl, m_int_decl }; + return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl, + func_decl_info(m_family_id, k, num_parameters, parameters)); + } + if (m_manager->int_real_coercions() && use_coercion(k)) { return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl)); } @@ -693,7 +707,16 @@ expr * arith_decl_plugin::get_some_value(sort * s) { return mk_numeral(rational(0), s == m_int_decl); } -bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const { +bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const { + if (is_irrational_algebraic_numeral(n)) { + scoped_anum an(am()); + is_irrational_algebraic_numeral2(n, an); + if (am().is_rational(an)) { + am().to_rational(an, val); + is_int = val.is_int(); + return true; + } + } if (!is_app_of(n, arith_family_id, OP_NUM)) return false; func_decl * decl = to_app(n)->get_decl(); @@ -724,7 +747,7 @@ bool arith_recognizers::is_int_expr(expr const *e) const { if (is_to_real(e)) { // pass } - else if (is_numeral(e, r) && r.is_int()) { + else if (is_numeral(e) && is_int(e)) { // pass } else if (is_add(e) || is_mul(e)) { @@ -747,14 +770,14 @@ void arith_util::init_plugin() { m_plugin = static_cast(m_manager.get_plugin(arith_family_id)); } -bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) { +bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) const { if (!is_app_of(n, arith_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) return false; am().set(val, to_irrational_algebraic_numeral(n)); return true; } -algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr const * n) { +algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr const * n) const { SASSERT(is_irrational_algebraic_numeral(n)); return plugin().aw().to_anum(to_app(n)->get_decl()); } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index fa359a9a7..25c4977e9 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -70,6 +70,8 @@ enum arith_op_kind { OP_ASINH, OP_ACOSH, OP_ATANH, + // Bit-vector functions + OP_ARITH_BAND, // constants OP_PI, OP_E, @@ -235,26 +237,10 @@ public: family_id get_family_id() const { return arith_family_id; } bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == arith_family_id; } - bool is_irrational_algebraic_numeral(expr const * n) const; - bool is_unsigned(expr const * n, unsigned& u) const { - rational val; - bool is_int = true; - return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true); - } - bool is_numeral(expr const * n, rational & val, bool & is_int) const; - bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); } - bool is_numeral(expr const * n) const { return is_app_of(n, arith_family_id, OP_NUM); } - bool is_zero(expr const * n) const { rational val; return is_numeral(n, val) && val.is_zero(); } - bool is_minus_one(expr * n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); } - // return true if \c n is a term of the form (* -1 r) - bool is_times_minus_one(expr * n, expr * & r) const { - if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) { - r = to_app(n)->get_arg(1); - return true; - } - return false; - } + bool is_irrational_algebraic_numeral(expr const* n) const; + + bool is_numeral(expr const* n) const { return is_app_of(n, arith_family_id, OP_NUM); } bool is_int_expr(expr const * e) const; bool is_le(expr const * n) const { return is_app_of(n, arith_family_id, OP_LE); } @@ -309,6 +295,16 @@ public: bool is_int_real(sort const * s) const { return s->get_family_id() == arith_family_id; } bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); } + bool is_band(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); } + bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { + if (!is_band(n)) + return false; + x = to_app(n)->get_arg(0); + y = to_app(n)->get_arg(1); + sz = to_app(n)->get_parameter(0).get_int(); + return true; + } + bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); } bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); } bool is_tan(expr const* n) const { return is_app_of(n, arith_family_id, OP_TAN); } @@ -387,13 +383,32 @@ public: return *m_plugin; } - algebraic_numbers::manager & am() { + algebraic_numbers::manager & am() const { return plugin().am(); } + // return true if \c n is a term of the form (* -1 r) + bool is_zero(expr const* n) const { rational val; return is_numeral(n, val) && val.is_zero(); } + bool is_minus_one(expr* n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); } + bool is_times_minus_one(expr* n, expr*& r) const { + if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) { + r = to_app(n)->get_arg(1); + return true; + } + return false; + } + bool is_unsigned(expr const* n, unsigned& u) const { + rational val; + bool is_int = true; + return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true); + } + bool is_numeral(expr const* n) const { return arith_recognizers::is_numeral(n); } + bool is_numeral(expr const* n, rational& val, bool& is_int) const; + bool is_numeral(expr const* n, rational& val) const { bool is_int; return is_numeral(n, val, is_int); } + bool convert_int_numerals_to_real() const { return plugin().convert_int_numerals_to_real(); } - bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val); - algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n); + bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) const; + algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n) const; sort * mk_int() { return m_manager.mk_sort(arith_family_id, INT_SORT); } sort * mk_real() { return m_manager.mk_sort(arith_family_id, REAL_SORT); } @@ -471,6 +486,8 @@ public: app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER, arg1, arg2); } app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); } + app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); } + app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); } app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); } app * mk_tan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TAN, arg); } @@ -498,11 +515,11 @@ public: if none of them are numerals, then the left-hand-side has a smaller id than the right hand side. */ app * mk_eq(expr * lhs, expr * rhs) { - if (is_numeral(lhs) || (!is_numeral(rhs) && lhs->get_id() > rhs->get_id())) + if (arith_recognizers::is_numeral(lhs) || (!arith_recognizers::is_numeral(rhs) && lhs->get_id() > rhs->get_id())) std::swap(lhs, rhs); if (lhs == rhs) return m_manager.mk_true(); - if (is_numeral(lhs) && is_numeral(rhs)) { + if (arith_recognizers::is_numeral(lhs) && arith_recognizers::is_numeral(rhs)) { SASSERT(lhs != rhs); return m_manager.mk_false(); } diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index f725fefc5..30cfe4cdb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -942,3 +942,8 @@ app * bv_util::mk_bv2int(expr* e) { parameter p(s); return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e); } + +app* bv_util::mk_int2bv(unsigned sz, expr* e) { + parameter p(sz); + return m_manager.mk_app(get_fid(), OP_INT2BV, 1, &p, 1, &e); +} diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 9126b97b7..89588ee0e 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -386,9 +386,31 @@ public: bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); } bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); } bool is_bv_umul_no_ovfl(expr const* e) const { return is_app_of(e, get_fid(), OP_BUMUL_NO_OVFL); } + bool is_redand(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDAND); } + bool is_redor(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDOR); } + bool is_comp(expr const* e) const { return is_app_of(e, get_fid(), OP_BCOMP); } + bool is_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_LEFT); } + bool is_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_RIGHT); } + bool is_ext_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_LEFT); } + bool is_ext_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_RIGHT); } + + bool is_rotate_left(expr const* e, unsigned& n, expr*& x) const { + return is_rotate_left(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true); + } + bool is_rotate_right(expr const* e, unsigned& n, expr*& x) const { + return is_rotate_right(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true); + } + bool is_int2bv(expr const* e, unsigned& n, expr*& x) const { + return is_int2bv(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true); + } MATCH_UNARY(is_bv_not); + MATCH_UNARY(is_redand); + MATCH_UNARY(is_redor); + MATCH_BINARY(is_ext_rotate_left); + MATCH_BINARY(is_ext_rotate_right); + MATCH_BINARY(is_comp); MATCH_BINARY(is_bv_add); MATCH_BINARY(is_bv_sub); MATCH_BINARY(is_bv_mul); @@ -411,6 +433,12 @@ public: MATCH_BINARY(is_bv_sdiv); MATCH_BINARY(is_bv_udiv); MATCH_BINARY(is_bv_smod); + MATCH_BINARY(is_bv_and); + MATCH_BINARY(is_bv_or); + MATCH_BINARY(is_bv_xor); + MATCH_BINARY(is_bv_nand); + MATCH_BINARY(is_bv_nor); + MATCH_BINARY(is_bv_uremi); MATCH_BINARY(is_bv_sremi); @@ -516,6 +544,7 @@ public: app * mk_bv_lshr(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_BLSHR, arg1, arg2); } app * mk_bv2int(expr* e); + app * mk_int2bv(unsigned sz, expr* e); // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return` app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); } diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 99bf8941b..f640b3ed0 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -104,8 +104,8 @@ namespace euf { } void bv_plugin::merge_eh(enode* x, enode* y) { - SASSERT(x == x->get_root()); - SASSERT(x == y->get_root()); + if (!bv.is_bv(x->get_expr())) + return; TRACE("bv", tout << "merge_eh " << g.bpp(x) << " == " << g.bpp(y) << "\n"); SASSERT(!m_internal); @@ -343,7 +343,8 @@ namespace euf { enode* hi = mk_extract(n, cut, w - 1); enode* lo = mk_extract(n, 0, cut - 1); auto& i = info(n); - SASSERT(i.value); + if (!i.value) + i.value = n; i.hi = hi; i.lo = lo; i.cut = cut; diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 55156c53a..3ad64acfd 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -1807,7 +1807,9 @@ namespace dd { pdd& pdd::operator=(pdd const& other) { if (m != other.m) { verbose_stream() << "pdd manager confusion: " << *this << " (mod 2^" << power_of_2() << ") := " << other << " (mod 2^" << other.power_of_2() << ")\n"; + UNREACHABLE(); // TODO: in the end, this operator should probably be changed to also update the manager. But for now I want to detect such confusions. + reset(*other.m); } SASSERT_EQ(power_of_2(), other.power_of_2()); VERIFY_EQ(power_of_2(), other.power_of_2()); diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 2a4e5058d..0eb8b6b37 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -108,6 +108,7 @@ namespace lp_api { unsigned m_gomory_cuts; unsigned m_assume_eqs; unsigned m_branch; + unsigned m_band_axioms; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); @@ -128,6 +129,7 @@ namespace lp_api { st.update("arith-gomory-cuts", m_gomory_cuts); st.update("arith-assume-eqs", m_assume_eqs); st.update("arith-branch", m_branch); + st.update("arith-band-axioms", m_band_axioms); } }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 96b3c13c4..a1b88bed1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -879,7 +879,6 @@ namespace sat { m_conflict = c; m_not_l = not_l; TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n")); - TRACE("sat", display_watches(tout)); } void solver::assign_core(literal l, justification j) { @@ -1720,6 +1719,9 @@ namespace sat { if (next == null_bool_var) return false; } + else { + SASSERT(value(next) == l_undef); + } push(); m_stats.m_decision++; @@ -1729,11 +1731,14 @@ namespace sat { phase = guess(next) ? l_true: l_false; literal next_lit(next, false); + SASSERT(value(next_lit) == l_undef); if (m_ext && m_ext->decide(next, phase)) { + if (used_queue) m_case_split_queue.unassign_var_eh(next); next_lit = literal(next, false); + SASSERT(value(next_lit) == l_undef); } if (phase == l_undef) @@ -2429,9 +2434,8 @@ namespace sat { m_conflicts_since_restart++; m_conflicts_since_gc++; m_stats.m_conflict++; - if (m_step_size > m_config.m_step_size_min) { - m_step_size -= m_config.m_step_size_dec; - } + if (m_step_size > m_config.m_step_size_min) + m_step_size -= m_config.m_step_size_dec; bool unique_max; m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max); @@ -2554,7 +2558,8 @@ namespace sat { } SASSERT(lvl(c_var) < m_conflict_lvl); } - CTRACE("sat", idx == 0, + CTRACE("sat", idx == 0, + tout << "conflict level " << m_conflict_lvl << "\n"; for (literal lit : m_trail) if (is_marked(lit.var())) tout << "missed " << lit << "@" << lvl(lit) << "\n";); @@ -2809,8 +2814,9 @@ namespace sat { unsigned level = 0; if (not_l != null_literal) { - level = lvl(not_l); + level = lvl(not_l); } + TRACE("sat", tout << "level " << not_l << " is " << level << " " << js << "\n"); switch (js.get_kind()) { case justification::NONE: @@ -3485,11 +3491,10 @@ namespace sat { // // ----------------------- void solver::push() { + SASSERT(!m_ext || !m_ext->can_propagate()); SASSERT(!inconsistent()); TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";); SASSERT(m_qhead == m_trail.size()); - if (m_ext) - m_ext->unit_propagate(); m_scopes.push_back(scope()); scope & s = m_scopes.back(); m_scope_lvl++; diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 7caccded6..e5d35a4f9 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -5,6 +5,7 @@ z3_add_component(sat_smt arith_internalize.cpp arith_sls.cpp arith_solver.cpp + arith_value.cpp array_axioms.cpp array_diagnostics.cpp array_internalize.cpp @@ -27,6 +28,7 @@ z3_add_component(sat_smt euf_proof_checker.cpp euf_relevancy.cpp euf_solver.cpp + intblast_solver.cpp fpa_solver.cpp pb_card.cpp pb_constraint.cpp diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 173ae28c8..f004422a6 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -205,6 +205,80 @@ namespace arith { add_clause(dgez, neg); } + bool solver::check_band_term(app* n) { + unsigned sz; + expr* x, * y; + if (!ctx.is_relevant(expr2enode(n))) + return true; + VERIFY(a.is_band(n, sz, x, y)); + expr_ref vx(m), vy(m),vn(m); + if (!get_value(expr2enode(x), vx) || !get_value(expr2enode(y), vy) || !get_value(expr2enode(n), vn)) { + IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n"); + found_unsupported(n); + return true; + } + rational valn, valx, valy; + bool is_int; + if (!a.is_numeral(vn, valn, is_int) || !is_int || !a.is_numeral(vx, valx, is_int) || !is_int || !a.is_numeral(vy, valy, is_int) || !is_int) { + IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n"); + found_unsupported(n); + return true; + } + // verbose_stream() << "band: " << mk_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n"; + rational N = rational::power_of_two(sz); + valx = mod(valx, N); + valy = mod(valy, N); + SASSERT(0 <= valn && valn < N); + + // x mod 2^{i + 1} >= 2^i means the i'th bit is 1. + auto bitof = [&](expr* x, unsigned i) { + expr_ref r(m); + r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i))); + return mk_literal(r); + }; + for (unsigned i = 0; i < sz; ++i) { + bool xb = valx.get_bit(i); + bool yb = valy.get_bit(i); + bool nb = valn.get_bit(i); + if (xb && yb && !nb) + add_clause(~bitof(x, i), ~bitof(y, i), bitof(n, i)); + else if (nb && !xb) + add_clause(~bitof(n, i), bitof(x, i)); + else if (nb && !yb) + add_clause(~bitof(n, i), bitof(y, i)); + else + continue; + return false; + } + return true; + } + + bool solver::check_band_terms() { + for (app* n : m_band_terms) { + if (!check_band_term(n)) { + ++m_stats.m_band_axioms; + return false; + } + } + return true; + } + + /* + * 0 <= x&y < 2^sz + * x&y <= x + * x&y <= y + */ + void solver::mk_band_axiom(app* n) { + unsigned sz; + expr* x, * y; + VERIFY(a.is_band(n, sz, x, y)); + rational N = rational::power_of_two(sz); + add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); + add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); + add_clause(mk_literal(a.mk_le(n, a.mk_mod(x, a.mk_int(N))))); + add_clause(mk_literal(a.mk_le(n, a.mk_mod(y, a.mk_int(N))))); + } + void solver::mk_bound_axioms(api_bound& b) { theory_var v = b.get_var(); lp_api::bound_kind kind1 = b.get_bound_kind(); diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 3c6286317..decd49019 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -252,6 +252,12 @@ namespace arith { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } + else if (a.is_band(n)) { + m_band_terms.push_back(to_app(n)); + mk_band_axiom(to_app(n)); + ctx.push(push_back_vector(m_band_terms)); + ensure_arg_vars(to_app(n)); + } else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) { found_unsupported(n); ensure_arg_vars(to_app(n)); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 2be9b6b60..eff25bc4a 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -619,17 +619,17 @@ namespace arith { } } - void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + bool solver::get_value(euf::enode* n, expr_ref& value) { theory_var v = n->get_th_var(get_id()); expr* o = n->get_expr(); - expr_ref value(m); + if (m.is_value(n->get_root()->get_expr())) { value = n->get_root()->get_expr(); } else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) { anum const& an = nl_value(v, m_nla->tmp1()); if (a.is_int(o) && !m_nla->am().is_int(an)) - value = a.mk_numeral(rational::zero(), a.is_int(o)); + value = a.mk_numeral(rational::zero(), a.is_int(o)); else value = a.mk_numeral(m_nla->am(), nl_value(v, m_nla->tmp1()), a.is_int(o)); } @@ -637,24 +637,35 @@ namespace arith { rational r = get_value(v); TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";); SASSERT("integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m_not_handled != nullptr || m.limit().is_canceled())); - if (a.is_int(o) && !r.is_int()) + if (a.is_int(o) && !r.is_int()) r = floor(r); value = a.mk_numeral(r, o->get_sort()); } + else + return false; + + return true; + } + + + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr_ref value(m); + expr* o = n->get_expr(); + if (get_value(n, value)) + ; else if (a.is_arith_expr(o) && reflect(o)) { expr_ref_vector args(m); for (auto* arg : *to_app(o)) { if (m.is_value(arg)) args.push_back(arg); - else + else args.push_back(values.get(ctx.get_enode(arg)->get_root_id())); } value = m.mk_app(to_app(o)->get_decl(), args.size(), args.data()); ctx.get_rewriter()(value); } - else { - value = mdl.get_fresh_value(o->get_sort()); - } + else + value = mdl.get_fresh_value(n->get_sort()); mdl.register_value(value); values.set(n->get_root_id(), value); } @@ -1042,6 +1053,9 @@ namespace arith { if (!check_delayed_eqs()) return sat::check_result::CR_CONTINUE; + if (!int_undef && !check_band_terms()) + return sat::check_result::CR_CONTINUE; + if (ctx.get_config().m_arith_ignore_int && int_undef) return sat::check_result::CR_GIVEUP; if (m_not_handled != nullptr) { @@ -1192,7 +1206,8 @@ namespace arith { lia_check = l_undef; break; case lp::lia_move::continue_with_check: - lia_check = l_undef; + TRACE("arith", tout << "continue-with-check\n"); + lia_check = l_false; break; default: UNREACHABLE(); diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 20ae599c2..022dbeaea 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -214,6 +214,7 @@ namespace arith { expr* m_not_handled = nullptr; ptr_vector m_underspecified; ptr_vector m_idiv_terms; + ptr_vector m_band_terms; vector > m_use_list; // bounds where variables are used. // attributes for incremental version: @@ -317,6 +318,7 @@ namespace arith { void mk_bound_axioms(api_bound& b); void mk_bound_axiom(api_bound& b1, api_bound& b2); void mk_power0_axioms(app* t, app* n); + void mk_band_axiom(app* n); void flush_bound_axioms(); void add_farkas_clause(sat::literal l1, sat::literal l2); @@ -408,6 +410,8 @@ namespace arith { bool check_delayed_eqs(); lbool check_lia(); lbool check_nla(); + bool check_band_terms(); + bool check_band_term(app* n); void add_lemmas(); void propagate_nla(); void add_equality(lpvar v, rational const& k, lp::explanation const& exp); @@ -522,6 +526,8 @@ namespace arith { bool add_eq(lpvar u, lpvar v, lp::explanation const& e, bool is_fixed); void consume(rational const& v, lp::constraint_index j); bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational& bval) const; + + bool get_value(euf::enode* n, expr_ref& val); }; diff --git a/src/sat/smt/arith_value.cpp b/src/sat/smt/arith_value.cpp new file mode 100644 index 000000000..bb301808e --- /dev/null +++ b/src/sat/smt/arith_value.cpp @@ -0,0 +1,145 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + smt_arith_value.cpp + +Abstract: + + Utility to extract arithmetic values from context. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-12-08. + +Revision History: + +--*/ + +#include "ast/ast_pp.h" +#include "sat/smt/arith_value.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/arith_solver.h" + +namespace arith { + + arith_value::arith_value(euf::solver& s) : + s(s), m(s.get_manager()), a(m) {} + + void arith_value::init() { + if (!as) + as = dynamic_cast(s.fid2solver(a.get_family_id())); + } + + bool arith_value::get_value(expr* e, rational& val) { + auto n = s.get_enode(e); + expr_ref _val(m); + init(); + return n && as->get_value(n, _val) && a.is_numeral(_val, val); + } + +#if 0 + bool arith_value::get_lo_equiv(expr* e, rational& lo, bool& is_strict) { + if (!s.get_enode(e)) + return false; + init(); + is_strict = false; + bool found = false; + bool is_strict1; + rational lo1; + for (auto sib : euf::enode_class(s.get_enode(e))) { + if (!as->get_lower(sib, lo1, is_strict1)) + continue; + if (!found || lo1 > lo || lo == lo1 && is_strict1) + lo = lo1, is_strict = is_strict1; + found = true; + } + CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";); + return found; + } + + bool arith_value::get_up_equiv(expr* e, rational& hi, bool& is_strict) { + if (!s.get_enode(e)) + return false; + init(); + is_strict = false; + bool found = false; + bool is_strict1; + rational hi1; + for (auto sib : euf::enode_class(s.get_enode(e))) { + if (!as->get_upper(sib, hi1, is_strict1)) + continue; + if (!found || hi1 < hi || hi == hi1 && is_strict1) + hi = hi1, is_strict = is_strict1; + found = true; + } + CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";); + return found; + } + + bool arith_value::get_up(expr* e, rational& up, bool& is_strict) const { + init(); + enode* n = s.get_enode(e); + is_strict = false; + return n && as->get_upper(n, up, is_strict); + } + + bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) const { + init(); + enode* n = s.get_enode(e); + is_strict = false; + return n && as->get_lower(n, lo, is_strict); + } + +#endif + + +#if 0 + + + bool arith_value::get_value_equiv(expr* e, rational& val) const { + if (!m_ctx->e_internalized(e)) return false; + expr_ref _val(m); + enode* next = m_ctx->get_enode(e), * n = next; + do { + e = next->get_expr(); + if (m_tha && m_tha->get_value(next, _val) && a.is_numeral(_val, val)) return true; + if (m_thi && m_thi->get_value(next, _val) && a.is_numeral(_val, val)) return true; + if (m_thr && m_thr->get_value(next, val)) return true; + next = next->get_next(); + } while (next != n); + TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";); + return false; + } + + expr_ref arith_value::get_lo(expr* e) const { + rational lo; + bool s = false; + if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) { + return expr_ref(a.mk_numeral(lo, e->get_sort()), m); + } + return expr_ref(e, m); + } + + expr_ref arith_value::get_up(expr* e) const { + rational up; + bool s = false; + if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) { + return expr_ref(a.mk_numeral(up, e->get_sort()), m); + } + return expr_ref(e, m); + } + + expr_ref arith_value::get_fixed(expr* e) const { + rational lo, up; + bool s = false; + if (a.is_int_real(e) && get_lo(e, lo, s) && !s && get_up(e, up, s) && !s && lo == up) { + return expr_ref(a.mk_numeral(lo, e->get_sort()), m); + } + return expr_ref(e, m); + } + +#endif + +}; diff --git a/src/sat/smt/arith_value.h b/src/sat/smt/arith_value.h new file mode 100644 index 000000000..b858ff896 --- /dev/null +++ b/src/sat/smt/arith_value.h @@ -0,0 +1,52 @@ + +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + arith_value.h + +Abstract: + + Utility to extract arithmetic values from context. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-12-08. + +Revision History: + +--*/ +#pragma once + +#include "ast/arith_decl_plugin.h" + +namespace euf { + class solver; +} +namespace arith { + + class solver; + + class arith_value { + euf::solver& s; + ast_manager& m; + arith_util a; + solver* as = nullptr; + void init(); + public: + arith_value(euf::solver& s); + bool get_value(expr* e, rational& value); + +#if 0 + bool get_lo_equiv(expr* e, rational& lo, bool& strict); + bool get_up_equiv(expr* e, rational& up, bool& strict); + bool get_lo(expr* e, rational& lo, bool& strict); + bool get_up(expr* e, rational& up, bool& strict); + bool get_value_equiv(expr* e, rational& value); + expr_ref get_lo(expr* e); + expr_ref get_up(expr* e); + expr_ref get_fixed(expr* e); +#endif + }; +}; diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index daecb7325..52c4ed953 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -400,7 +400,7 @@ namespace dt { return; } SASSERT(val == l_undef || (val == l_false && !d->m_constructor)); - ctx.push(set_vector_idx_trail(d->m_recognizers, c_idx)); + ctx.push(set_vector_idx_trail(d->m_recognizers, c_idx)); d->m_recognizers[c_idx] = recognizer; if (val == l_false) propagate_recognizer(v, recognizer); diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 943d0b324..f750f186d 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -106,7 +106,6 @@ namespace euf { attach_node(mk_enode(e, 0, nullptr)); return true; } - bool solver::post_visit(expr* e, bool sign, bool root) { unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0; m_args.reset(); diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index b117ac1e3..073d164be 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -302,7 +302,7 @@ namespace euf { if (mval != sval) { if (r->bool_var() != sat::null_bool_var) out << "b" << r->bool_var() << " "; - out << bpp(r) << " :=\neval: " << sval << "\nmval: " << mval << "\n"; + out << bpp(r) << " :=\nvalue obtained from model: " << sval << "\nvalue of the root expression: " << mval << "\n"; continue; } if (!m.is_bool(val)) @@ -310,7 +310,7 @@ namespace euf { auto bval = s().value(r->bool_var()); bool tt = l_true == bval; if (tt != m.is_true(sval)) - out << bpp(r) << " :=\neval: " << sval << "\nmval: " << bval << "\n"; + out << bpp(r) << " :=\nvalue according to model: " << sval << "\nvalue of Boolean literal: " << bval << "\n"; } for (euf::enode* r : nodes) if (r) @@ -357,6 +357,7 @@ namespace euf { if (!tt && !mdl.is_true(e)) continue; CTRACE("euf", first, display_validation_failure(tout, mdl, n);); + CTRACE("euf", first, display(tout)); IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n);); (void)first; first = false; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 3ae4425fc..ff11b0749 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -21,6 +21,7 @@ Author: #include "sat/smt/sat_smt.h" #include "sat/smt/pb_solver.h" #include "sat/smt/bv_solver.h" +#include "sat/smt/intblast_solver.h" #include "sat/smt/euf_solver.h" #include "sat/smt/array_solver.h" #include "sat/smt/arith_solver.h" @@ -134,8 +135,16 @@ namespace euf { special_relations_util sp(m); if (pb.get_family_id() == fid) ext = alloc(pb::solver, *this, fid); - else if (bvu.get_family_id() == fid) - ext = alloc(bv::solver, *this, fid); + else if (bvu.get_family_id() == fid) { + if (get_config().m_bv_solver == 0) + ext = alloc(bv::solver, *this, fid); + else if (get_config().m_bv_solver == 1) + throw default_exception("polysat solver is not integrated"); + else if (get_config().m_bv_solver == 2) + ext = alloc(intblast::solver, *this); + else + throw default_exception("unknown bit-vector solver. Accepted values 0 (bit blast), 1 (polysat), 2 (int blast)"); + } else if (au.get_family_id() == fid) ext = alloc(array::solver, *this, fid); else if (fpa.get_family_id() == fid) @@ -209,6 +218,15 @@ namespace euf { s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx)); } + lbool solver::resolve_conflict() { + for (auto* s : m_solvers) { + lbool r = s->resolve_conflict(); + if (r != l_undef) + return r; + } + return l_undef; + } + /** Retrieve set of literals r that imply r. Since the set of literals are retrieved modulo multiple theories in a single implication @@ -281,6 +299,26 @@ namespace euf { } } + void solver::get_eq_antecedents(enode* a, enode* b, literal_vector& r) { + m_egraph.begin_explain(); + m_explain.reset(); + m_egraph.explain_eq(m_explain, nullptr, a, b); + for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) { + size_t* e = m_explain[qhead]; + if (is_literal(e)) + r.push_back(get_literal(e)); + else { + size_t idx = get_justification(e); + auto* ext = sat::constraint_base::to_extension(idx); + SASSERT(ext != this); + sat::literal lit = sat::null_literal; + ext->get_antecedents(lit, idx, r, true); + } + } + m_egraph.end_explain(); + } + + void solver::get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) { for (auto lit : euf::th_explain::lits(jst)) r.push_back(lit); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index db99ec512..7d2d01473 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -363,11 +363,13 @@ namespace euf { bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); } size_t* to_justification(sat::literal l) { return to_ptr(l); } void set_conflict(th_explain* p) { set_conflict(p->to_index()); } + bool inconsistent() const { return s().inconsistent() || m_egraph.inconsistent(); } bool set_root(literal l, literal r) override; void flush_roots() override; void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override; + void get_eq_antecedents(enode* a, enode* b, literal_vector& r); void get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing); void add_eq_antecedent(bool probing, enode* a, enode* b); void explain_diseq(ptr_vector& ex, cc_justification* cc, enode* a, enode* b); @@ -378,6 +380,7 @@ namespace euf { bool get_case_split(bool_var& var, lbool& phase) override; void asserted(literal l) override; sat::check_result check() override; + lbool resolve_conflict() override; void push() override; void pop(unsigned n) override; void user_push() override; diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp new file mode 100644 index 000000000..9d03d0ad0 --- /dev/null +++ b/src/sat/smt/intblast_solver.cpp @@ -0,0 +1,985 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + intblast_solver.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2023-12-10 + +--*/ + +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "ast/rewriter/bv_rewriter.h" +#include "params/bv_rewriter_params.hpp" +#include "sat/smt/intblast_solver.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/arith_value.h" + + +namespace intblast { + + solver::solver(euf::solver& ctx) : + th_euf_solver(ctx, symbol("intblast"), ctx.get_manager().get_family_id("bv")), + ctx(ctx), + s(ctx.s()), + m(ctx.get_manager()), + bv(m), + a(m), + m_translate(m), + m_args(m), + m_pinned(m) + {} + + euf::theory_var solver::mk_var(euf::enode* n) { + auto r = euf::th_euf_solver::mk_var(n); + ctx.attach_th_var(n, this, r); + TRACE("bv", tout << "mk-var: v" << r << " " << ctx.bpp(n) << "\n";); + return r; + } + + sat::literal solver::internalize(expr* e, bool sign, bool root) { + force_push(); + SASSERT(m.is_bool(e)); + if (!visit_rec(m, e, sign, root)) + return sat::null_literal; + sat::literal lit = expr2literal(e); + if (sign) + lit.neg(); + return lit; + } + + void solver::internalize(expr* e) { + force_push(); + visit_rec(m, e, false, false); + } + + bool solver::visit(expr* e) { + if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { + ctx.internalize(e); + return true; + } + m_stack.push_back(sat::eframe(e)); + return false; + } + + bool solver::visited(expr* e) { + euf::enode* n = expr2enode(e); + return n && n->is_attached_to(get_id()); + } + + + + bool solver::post_visit(expr* e, bool sign, bool root) { + euf::enode* n = expr2enode(e); + app* a = to_app(e); + if (visited(e)) + return true; + SASSERT(!n || !n->is_attached_to(get_id())); + if (!n) + n = mk_enode(e, false); + SASSERT(!n->is_attached_to(get_id())); + mk_var(n); + SASSERT(n->is_attached_to(get_id())); + internalize_bv(a); + return true; + } + + void solver::eq_internalized(euf::enode* n) { + expr* e = n->get_expr(); + expr* x, * y; + VERIFY(m.is_eq(n->get_expr(), x, y)); + SASSERT(bv.is_bv(x)); + if (!is_translated(e)) { + ensure_translated(x); + ensure_translated(y); + m_args.reset(); + m_args.push_back(a.mk_sub(translated(x), translated(y))); + set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); + } + m_preds.push_back(e); + ctx.push(push_back_vector(m_preds)); + } + + void solver::set_translated(expr* e, expr* r) { + SASSERT(r); + SASSERT(!is_translated(e)); + m_translate.setx(e->get_id(), r); + ctx.push(set_vector_idx_trail(m_translate, e->get_id())); + } + + void solver::internalize_bv(app* e) { + ensure_translated(e); + if (m.is_bool(e)) { + m_preds.push_back(e); + ctx.push(push_back_vector(m_preds)); + } + } + + bool solver::add_bound_axioms() { + if (m_vars_qhead == m_vars.size()) + return false; + ctx.push(value_trail(m_vars_qhead)); + for (; m_vars_qhead < m_vars.size(); ++m_vars_qhead) { + auto v = m_vars[m_vars_qhead]; + auto w = translated(v); + auto sz = rational::power_of_two(bv.get_bv_size(v->get_sort())); + auto lo = ctx.mk_literal(a.mk_ge(w, a.mk_int(0))); + auto hi = ctx.mk_literal(a.mk_le(w, a.mk_int(sz - 1))); + ctx.mark_relevant(lo); + ctx.mark_relevant(hi); + add_unit(lo); + add_unit(hi); + } + return true; + } + + bool solver::add_predicate_axioms() { + if (m_preds_qhead == m_preds.size()) + return false; + ctx.push(value_trail(m_preds_qhead)); + for (; m_preds_qhead < m_preds.size(); ++m_preds_qhead) { + expr* e = m_preds[m_preds_qhead]; + expr_ref r(translated(e), m); + ctx.get_rewriter()(r); + auto a = expr2literal(e); + auto b = mk_literal(r); + ctx.mark_relevant(b); +// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; + add_equiv(a, b); + } + return true; + } + + bool solver::unit_propagate() { + return add_bound_axioms() || add_predicate_axioms(); + } + + void solver::ensure_translated(expr* e) { + if (m_translate.get(e->get_id(), nullptr)) + return; + ptr_vector todo; + ast_fast_mark1 visited; + todo.push_back(e); + visited.mark(e); + for (unsigned i = 0; i < todo.size(); ++i) { + expr* e = todo[i]; + if (!is_app(e)) + continue; + app* a = to_app(e); + if (m.is_bool(e) && a->get_family_id() != bv.get_family_id()) + continue; + for (auto arg : *a) + if (!visited.is_marked(arg) && !m_translate.get(arg->get_id(), nullptr)) { + visited.mark(arg); + todo.push_back(arg); + } + } + std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); + for (expr* e : todo) + translate_expr(e); + } + + lbool solver::check_solver_state() { + sat::literal_vector literals; + uint_set selected; + for (auto const& clause : s.clauses()) { + if (any_of(*clause, [&](auto lit) { return selected.contains(lit.index()); })) + continue; + if (any_of(*clause, [&](auto lit) { return s.value(lit) == l_true && !is_bv(lit); })) + continue; + // TBD: if we associate "status" with clauses, we can also remove theory axioms from polysat + sat::literal selected_lit = sat::null_literal; + for (auto lit : *clause) { + if (s.value(lit) != l_true) + continue; + SASSERT(is_bv(lit)); + if (selected_lit == sat::null_literal || s.lvl(selected_lit) > s.lvl(lit)) + selected_lit = lit; + } + if (selected_lit == sat::null_literal) { + UNREACHABLE(); + return l_undef; + } + selected.insert(selected_lit.index()); + literals.push_back(selected_lit); + } + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + auto lit = s.trail_literal(i); + if (selected.contains(lit.index()) || !is_bv(lit)) + continue; + selected.insert(lit.index()); + literals.push_back(lit); + } + svector> bin; + s.collect_bin_clauses(bin, false, false); + for (auto [a, b] : bin) { + if (selected.contains(a.index())) + continue; + if (selected.contains(b.index())) + continue; + if (s.value(a) == l_true && !is_bv(a)) + continue; + if (s.value(b) == l_true && !is_bv(b)) + continue; + if (s.value(a) == l_false) + std::swap(a, b); + if (s.value(b) == l_true && s.value(a) == l_true && s.lvl(b) < s.lvl(a)) + std::swap(a, b); + selected.insert(a.index()); + literals.push_back(a); + } + + m_core.reset(); + m_is_plugin = false; + m_solver = mk_smt2_solver(m, s.params(), symbol::null); + + expr_ref_vector es(m); + for (auto lit : literals) + es.push_back(ctx.literal2expr(lit)); + + translate(es); + + for (auto e : m_vars) { + auto v = translated(e); + auto b = rational::power_of_two(bv.get_bv_size(e)); + m_solver->assert_expr(a.mk_le(a.mk_int(0), v)); + m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); + } + + IF_VERBOSE(10, verbose_stream() << "check\n"; + m_solver->display(verbose_stream()); + verbose_stream() << es << "\n"); + + lbool r = m_solver->check_sat(es); + + m_solver->collect_statistics(m_stats); + + IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); + + if (r == l_false) { + expr_ref_vector core(m); + m_solver->get_unsat_core(core); + obj_map e2index; + for (unsigned i = 0; i < es.size(); ++i) + e2index.insert(es.get(i), i); + for (auto e : core) { + unsigned idx = e2index[e]; + if (idx < literals.size()) + m_core.push_back(literals[idx]); + else + m_core.push_back(ctx.mk_literal(e)); + } + } + return r; + }; + + bool solver::is_bv(sat::literal lit) { + expr* e = ctx.bool_var2expr(lit.var()); + if (!e) + return false; + if (m.is_and(e) || m.is_or(e) || m.is_not(e) || m.is_implies(e) || m.is_iff(e)) + return false; + return any_of(subterms::all(expr_ref(e, m)), [&](auto* p) { return bv.is_bv_sort(p->get_sort()); }); + } + + void solver::sorted_subterms(expr_ref_vector& es, ptr_vector& sorted) { + expr_fast_mark1 visited; + for (expr* e : es) { + if (is_translated(e)) + continue; + sorted.push_back(e); + visited.mark(e); + } + for (unsigned i = 0; i < sorted.size(); ++i) { + expr* e = sorted[i]; + if (is_app(e)) { + app* a = to_app(e); + for (expr* arg : *a) { + if (!visited.is_marked(arg) && !is_translated(arg)) { + visited.mark(arg); + sorted.push_back(arg); + } + } + + // + // Add ground equalities to ensure the model is valid with respect to the current case splits. + // This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal + // assignment from complete level. + // E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment. + // If intblast is SAT, then force the model and literal assignment on the rest of the literals. + // + if (!is_ground(e)) + continue; + euf::enode* n = ctx.get_enode(e); + if (!n) + continue; + if (n == n->get_root()) + continue; + expr* r = n->get_root()->get_expr(); + es.push_back(m.mk_eq(e, r)); + r = es.back(); + if (!visited.is_marked(r) && !is_translated(r)) { + visited.mark(r); + sorted.push_back(r); + } + } + else if (is_quantifier(e)) { + quantifier* q = to_quantifier(e); + expr* b = q->get_expr(); + if (!visited.is_marked(b) && !is_translated(b)) { + visited.mark(b); + sorted.push_back(b); + } + } + } + std::stable_sort(sorted.begin(), sorted.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); + } + + void solver::translate(expr_ref_vector& es) { + ptr_vector todo; + + sorted_subterms(es, todo); + + for (expr* e : todo) + translate_expr(e); + + TRACE("bv", + for (expr* e : es) + tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated(e), m) << "\n"; + ); + + for (unsigned i = 0; i < es.size(); ++i) + es[i] = translated(es.get(i)); + } + + sat::check_result solver::check() { + // ensure that bv2int is injective + for (auto e : m_bv2int) { + euf::enode* n = expr2enode(e); + euf::enode* r1 = n->get_arg(0)->get_root(); + for (auto sib : euf::enode_class(n)) { + if (sib == n) + continue; + if (!bv.is_bv2int(sib->get_expr())) + continue; + if (sib->get_arg(0)->get_root() == r1) + continue; + auto a = eq_internalize(n, sib); + auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); + ctx.mark_relevant(a); + ctx.mark_relevant(b); + add_clause(~a, b, nullptr); + return sat::check_result::CR_CONTINUE; + } + } + // ensure that int2bv respects values + // bv2int(int2bv(x)) = x mod N + for (auto e : m_int2bv) { + auto n = expr2enode(e); + auto x = n->get_arg(0)->get_expr(); + auto bv2int = bv.mk_bv2int(e); + ctx.internalize(bv2int); + auto N = rational::power_of_two(bv.get_bv_size(e)); + auto xModN = a.mk_mod(x, a.mk_int(N)); + ctx.internalize(xModN); + auto nBv2int = ctx.get_enode(bv2int); + auto nxModN = ctx.get_enode(xModN); + if (nBv2int->get_root() != nxModN->get_root()) { + auto a = eq_internalize(nBv2int, nxModN); + ctx.mark_relevant(a); + add_unit(a); + return sat::check_result::CR_CONTINUE; + } + } + return sat::check_result::CR_DONE; + } + + expr* solver::umod(expr* bv_expr, unsigned i) { + expr* x = arg(i); + rational r; + rational N = bv_size(bv_expr); + if (a.is_numeral(x, r)) { + if (0 <= r && r < N) + return x; + return a.mk_int(mod(r, N)); + } + if (any_of(m_vars, [&](expr* v) { return translated(v) == x && bv.get_bv_size(v) == bv.get_bv_size(bv_expr); })) + return x; + return a.mk_mod(x, a.mk_int(N)); + } + + expr* solver::smod(expr* bv_expr, unsigned i) { + expr* x = arg(i); + auto N = bv_size(bv_expr); + auto shift = N / 2; + rational r; + if (a.is_numeral(x, r)) + return a.mk_int(mod(r + shift, N)); + return a.mk_mod(a.mk_add(x, a.mk_int(shift)), a.mk_int(N)); + } + + rational solver::bv_size(expr* bv_expr) { + return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort())); + } + + void solver::translate_expr(expr* e) { + if (is_quantifier(e)) + translate_quantifier(to_quantifier(e)); + else if (is_var(e)) + translate_var(to_var(e)); + else { + app* ap = to_app(e); + if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) { + set_translated(e, e); + return; + } + m_args.reset(); + for (auto arg : *ap) + m_args.push_back(translated(arg)); + + if (ap->get_family_id() == basic_family_id) + translate_basic(ap); + else if (ap->get_family_id() == bv.get_family_id()) + translate_bv(ap); + else + translate_app(ap); + } + } + + void solver::translate_quantifier(quantifier* q) { + if (is_lambda(q)) + throw default_exception("lambdas are not supported in intblaster"); + if (m_is_plugin) { + set_translated(q, q); + return; + } + expr* b = q->get_expr(); + unsigned nd = q->get_num_decls(); + ptr_vector sorts; + for (unsigned i = 0; i < nd; ++i) { + auto s = q->get_decl_sort(i); + if (bv.is_bv_sort(s)) { + NOT_IMPLEMENTED_YET(); + sorts.push_back(a.mk_int()); + } + else + + sorts.push_back(s); + } + b = translated(b); + // TODO if sorts contain integer, then created bounds variables. + set_translated(q, m.update_quantifier(q, b)); + } + + void solver::translate_var(var* v) { + if (bv.is_bv_sort(v->get_sort())) + set_translated(v, m.mk_var(v->get_idx(), a.mk_int())); + else + set_translated(v, v); + } + + // Translate functions that are not built-in or bit-vectors. + // Base method uses fresh functions. + // Other method could use bv2int, int2bv axioms and coercions. + // f(args) = bv2int(f(int2bv(args')) + // + + void solver::translate_app(app* e) { + + if (m_is_plugin && m.is_bool(e)) { + set_translated(e, e); + return; + } + + bool has_bv_sort = bv.is_bv(e); + func_decl* f = e->get_decl(); + + for (unsigned i = 0; i < m_args.size(); ++i) + if (bv.is_bv(e->get_arg(i))) + m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i)); + + if (has_bv_sort) + m_vars.push_back(e); + + if (m_is_plugin) { + expr* r = m.mk_app(f, m_args); + if (has_bv_sort) { + ctx.push(push_back_vector(m_vars)); + r = bv.mk_bv2int(r); + } + set_translated(e, r); + return; + } + else if (has_bv_sort) { + if (f->get_family_id() != null_family_id) + throw default_exception("conversion for interpreted functions is not supported by intblast solver"); + func_decl* g = nullptr; + if (!m_new_funs.find(f, g)) { + g = m.mk_fresh_func_decl(e->get_decl()->get_name(), symbol("bv"), f->get_arity(), f->get_domain(), a.mk_int()); + m_new_funs.insert(f, g); + } + f = g; + m_pinned.push_back(f); + } + set_translated(e, m.mk_app(f, m_args)); + } + + void solver::translate_bv(app* e) { + + auto bnot = [&](expr* e) { + return a.mk_sub(a.mk_int(-1), e); + }; + + auto band = [&](expr_ref_vector const& args) { + expr* r = arg(0); + for (unsigned i = 1; i < args.size(); ++i) + r = a.mk_band(bv.get_bv_size(e), r, arg(i)); + return r; + }; + + auto rotate_left = [&](unsigned n) { + auto sz = bv.get_bv_size(e); + n = n % sz; + expr* r = arg(0); + if (n != 0 && sz != 1) { + // r[sz - n - 1 : 0] ++ r[sz - 1 : sz - n] + // r * 2^(sz - n) + (r div 2^n) mod 2^(sz - n)??? + // r * A + (r div B) mod A + auto N = bv_size(e); + auto A = rational::power_of_two(sz - n); + auto B = rational::power_of_two(n); + auto hi = a.mk_mul(r, a.mk_int(A)); + auto lo = a.mk_mod(a.mk_idiv(umod(e, 0), a.mk_int(B)), a.mk_int(A)); + r = a.mk_add(hi, lo); + } + return r; + }; + + expr* bv_expr = e; + expr* r = nullptr; + auto const& args = m_args; + switch (e->get_decl_kind()) { + case OP_BADD: + r = a.mk_add(args); + break; + case OP_BSUB: + r = a.mk_sub(args.size(), args.data()); + break; + case OP_BMUL: + r = a.mk_mul(args); + break; + case OP_ULEQ: + bv_expr = e->get_arg(0); + r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_UGEQ: + bv_expr = e->get_arg(0); + r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_ULT: + bv_expr = e->get_arg(0); + r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_UGT: + bv_expr = e->get_arg(0); + r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_SLEQ: + bv_expr = e->get_arg(0); + r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_SGEQ: + r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_SLT: + bv_expr = e->get_arg(0); + r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_SGT: + bv_expr = e->get_arg(0); + r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_BNEG: + r = a.mk_uminus(arg(0)); + break; + case OP_CONCAT: { + unsigned sz = 0; + for (unsigned i = args.size(); i-- > 0;) { + expr* old_arg = e->get_arg(i); + expr* new_arg = umod(old_arg, i); + if (sz > 0) { + new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz))); + r = a.mk_add(r, new_arg); + } + else + r = new_arg; + sz += bv.get_bv_size(old_arg->get_sort()); + } + break; + } + case OP_EXTRACT: { + unsigned lo, hi; + expr* old_arg; + VERIFY(bv.is_extract(e, lo, hi, old_arg)); + r = arg(0); + if (lo > 0) + r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo))); + break; + } + case OP_BV_NUM: { + rational val; + unsigned sz; + VERIFY(bv.is_numeral(e, val, sz)); + r = a.mk_int(val); + break; + } + case OP_BUREM: + case OP_BUREM_I: { + expr* x = umod(e, 0), * y = umod(e, 1); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, a.mk_mod(x, y)); + break; + } + case OP_BUDIV: + case OP_BUDIV_I: { + expr* x = arg(0), * y = umod(e, 1); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y)); + break; + } + case OP_BUMUL_NO_OVFL: { + bv_expr = e->get_arg(0); + r = a.mk_lt(a.mk_mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr))); + break; + } + case OP_BSHL: { + expr* x = arg(0), * y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); + break; + } + case OP_BNOT: + r = bnot(arg(0)); + break; + case OP_BLSHR: { + expr* x = arg(0), * y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); + break; + } + case OP_BOR: { + // p | q := (p + q) - band(p, q) + r = arg(0); + for (unsigned i = 1; i < args.size(); ++i) + r = a.mk_sub(a.mk_add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i))); + break; + } + case OP_BNAND: + r = bnot(band(args)); + break; + case OP_BAND: + r = band(args); + break; + case OP_BXNOR: + case OP_BXOR: { + // p ^ q := (p + q) - 2*band(p, q); + unsigned sz = bv.get_bv_size(e); + r = arg(0); + for (unsigned i = 1; i < args.size(); ++i) { + expr* q = arg(i); + r = a.mk_sub(a.mk_add(r, q), a.mk_mul(a.mk_int(2), a.mk_band(sz, r, q))); + } + if (e->get_decl_kind() == OP_BXNOR) + r = bnot(r); + break; + } + case OP_BASHR: { + // + // ashr(x, y) + // if y = k & x >= 0 -> x / 2^k + // if y = k & x < 0 -> (x / 2^k) - 1 + 2^{N-k} + // + unsigned sz = bv.get_bv_size(e); + rational N = bv_size(e); + expr* x = umod(e, 0), *y = umod(e, 1); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0)); + for (unsigned i = 0; i < sz; ++i) { + expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), + m.mk_ite(signx, a.mk_add(d, a.mk_int(- rational::power_of_two(sz-i))), d), + r); + } + break; + } + case OP_ZERO_EXT: + bv_expr = e->get_arg(0); + r = umod(bv_expr, 0); + SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr)); + break; + case OP_SIGN_EXT: { + bv_expr = e->get_arg(0); + r = umod(bv_expr, 0); + SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr)); + unsigned arg_sz = bv.get_bv_size(bv_expr); + unsigned sz = bv.get_bv_size(e); + rational N = rational::power_of_two(sz); + rational M = rational::power_of_two(arg_sz); + expr* signbit = a.mk_ge(r, a.mk_int(M / 2)); + r = m.mk_ite(signbit, a.mk_uminus(r), r); + break; + } + case OP_INT2BV: + m_int2bv.push_back(e); + ctx.push(push_back_vector(m_int2bv)); + r = arg(0); + break; + case OP_BV2INT: + m_bv2int.push_back(e); + ctx.push(push_back_vector(m_bv2int)); + r = umod(e->get_arg(0), 0); + break; + case OP_BCOMP: + bv_expr = e->get_arg(0); + r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0)); + break; + case OP_BSMOD_I: + case OP_BSMOD: { + expr* x = umod(e, 0), *y = umod(e, 1); + rational N = bv_size(e); + expr* signx = a.mk_ge(x, a.mk_int(N/2)); + expr* signy = a.mk_ge(y, a.mk_int(N/2)); + expr* u = a.mk_mod(x, y); + // u = 0 -> 0 + // y = 0 -> x + // x < 0, y < 0 -> -u + // x < 0, y >= 0 -> y - u + // x >= 0, y < 0 -> y + u + // x >= 0, y >= 0 -> u + r = a.mk_uminus(u); + r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), a.mk_add(u, y), r); + r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r); + r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r); + r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); + break; + } + case OP_BSDIV_I: + case OP_BSDIV: { + // d = udiv(abs(x), abs(y)) + // y = 0, x > 0 -> 1 + // y = 0, x <= 0 -> -1 + // x = 0, y != 0 -> 0 + // x > 0, y < 0 -> -d + // x < 0, y > 0 -> -d + // x > 0, y > 0 -> d + // x < 0, y < 0 -> d + expr* x = umod(e, 0), * y = umod(e, 1); + rational N = bv_size(e); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + expr* signy = a.mk_ge(y, a.mk_int(N / 2)); + x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x); + y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); + expr* d = a.mk_idiv(x, y); + r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r); + break; + } + case OP_BSREM_I: + case OP_BSREM: { + // y = 0 -> x + // else x - sdiv(x, y) * y + expr* x = umod(e, 0), * y = umod(e, 1); + rational N = bv_size(e); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + expr* signy = a.mk_ge(y, a.mk_int(N / 2)); + expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x); + expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); + expr* d = a.mk_idiv(absx, absy); + d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); + r = a.mk_sub(x, a.mk_mul(d, y)); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); + break; + } + case OP_ROTATE_LEFT: { + auto n = e->get_parameter(0).get_int(); + r = rotate_left(n); + break; + } + case OP_ROTATE_RIGHT: { + unsigned sz = bv.get_bv_size(e); + auto n = e->get_parameter(0).get_int(); + r = rotate_left(sz - n); + break; + } + case OP_EXT_ROTATE_LEFT: { + unsigned sz = bv.get_bv_size(e); + expr* y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < sz; ++i) + r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r); + break; + } + case OP_EXT_ROTATE_RIGHT: { + unsigned sz = bv.get_bv_size(e); + expr* y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < sz; ++i) + r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r); + break; + } + case OP_REPEAT: { + unsigned n = e->get_parameter(0).get_int(); + expr* x = umod(e->get_arg(0), 0); + r = x; + rational N = bv_size(e->get_arg(0)); + rational N0 = N; + for (unsigned i = 1; i < n; ++i) + r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0; + break; + } + case OP_BREDOR: { + r = umod(e->get_arg(0), 0); + r = m.mk_not(m.mk_eq(r, a.mk_int(0))); + break; + } + case OP_BREDAND: { + rational N = bv_size(e->get_arg(0)); + r = umod(e->get_arg(0), 0); + r = m.mk_not(m.mk_eq(r, a.mk_int(N - 1))); + break; + } + default: + verbose_stream() << mk_pp(e, m) << "\n"; + NOT_IMPLEMENTED_YET(); + } + set_translated(e, r); + } + + void solver::translate_basic(app* e) { + if (m.is_eq(e)) { + bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); }); + if (has_bv_arg) { + expr* bv_expr = e->get_arg(0); + m_args[0] = a.mk_sub(arg(0), arg(1)); + set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0))); + } + else + set_translated(e, m.mk_eq(arg(0), arg(1))); + } + else if (m.is_ite(e)) + set_translated(e, m.mk_ite(arg(0), arg(1), arg(2))); + else if (m_is_plugin) + set_translated(e, e); + else + set_translated(e, m.mk_app(e->get_decl(), m_args)); + } + + rational solver::get_value(expr* e) const { + SASSERT(bv.is_bv(e)); + model_ref mdl; + m_solver->get_model(mdl); + expr_ref r(m); + r = translated(e); + rational val; + if (!mdl->eval_expr(r, r, true)) + return rational::zero(); + if (!a.is_numeral(r, val)) + return rational::zero(); + return val; + } + + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + if (m_is_plugin) + add_value_plugin(n, mdl, values); + else + add_value_solver(n, mdl, values); + } + + bool solver::add_dep(euf::enode* n, top_sort& dep) { + if (!is_app(n->get_expr())) + return false; + app* e = to_app(n->get_expr()); + if (n->num_args() == 0) { + dep.insert(n, nullptr); + return true; + } + if (e->get_family_id() != bv.get_family_id()) + return false; + for (euf::enode* arg : euf::enode_args(n)) + dep.add(n, arg->get_root()); + return true; + } + + // TODO: handle dependencies properly by using arithmetical model to retrieve values of translated + // bit-vectors directly. + void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr* e = n->get_expr(); + SASSERT(bv.is_bv(e)); + + if (bv.is_numeral(e)) { + values.setx(n->get_root_id(), e); + return; + } + + rational r, N = rational::power_of_two(bv.get_bv_size(e)); + expr* te = translated(e); + model_ref mdlr; + m_solver->get_model(mdlr); + expr_ref value(m); + if (mdlr->eval_expr(te, value, true) && a.is_numeral(value, r)) { + values.setx(n->get_root_id(), bv.mk_numeral(mod(r, N), bv.get_bv_size(e))); + return; + } + ctx.s().display(verbose_stream()); + verbose_stream() << "failed to evaluate " << mk_pp(te, m) << " " << value << "\n"; + UNREACHABLE(); + } + + void solver::add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr_ref value(m); + if (n->interpreted()) + value = n->get_expr(); + else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) { + bv_rewriter rw(m); + expr_ref_vector args(m); + for (auto arg : euf::enode_args(n)) + args.push_back(values.get(arg->get_root_id())); + rw.mk_app(n->get_decl(), args.size(), args.data(), value); + } + else { + expr_ref bv2int(bv.mk_bv2int(n->get_expr()), m); + euf::enode* b2i = ctx.get_enode(bv2int); + if (!b2i) verbose_stream() << bv2int << "\n"; + SASSERT(b2i); + VERIFY(b2i); + arith::arith_value av(ctx); + rational r; + VERIFY(av.get_value(b2i->get_expr(), r)); + verbose_stream() << ctx.bpp(n) << " := " << r << "\n"; + value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr())); + } + values.set(n->get_root_id(), value); + TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); + } + + sat::literal_vector const& solver::unsat_core() { + return m_core; + } + + std::ostream& solver::display(std::ostream& out) const { + if (m_solver) + m_solver->display(out); + return out; + } + + void solver::collect_statistics(statistics& st) const { + st.copy(m_stats); + } + +} diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h new file mode 100644 index 000000000..d59dac935 --- /dev/null +++ b/src/sat/smt/intblast_solver.h @@ -0,0 +1,143 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + intblast_solver.h + +Abstract: + + Int-blast solver. + + check_solver_state assumes a full assignment to literals in + irredundant clauses. + It picks a satisfying Boolean assignment and + checks if it is feasible for bit-vectors using + an arithmetic solver. + + The solver plugin is self-contained. + + Internalize: + - internalize bit-vector terms bottom-up by updating m_translate. + - add axioms of the form: + - ule(b,a) <=> translate(ule(b, a)) + - let arithmetic solver handle bit-vector constraints. + - For shared b + - Ensure: int2bv(translate(b)) = b + - but avoid bit-blasting by ensuring int2bv is injective (mod N) during final check + +Author: + + Nikolaj Bjorner (nbjorner) 2023-12-10 + +--*/ +#pragma once + +#include "ast/arith_decl_plugin.h" +#include "ast/bv_decl_plugin.h" +#include "solver/solver.h" +#include "sat/smt/sat_th.h" +#include "util/statistics.h" + +namespace euf { + class solver; +} + +namespace intblast { + + class solver : public euf::th_euf_solver { + euf::solver& ctx; + sat::solver& s; + ast_manager& m; + bv_util bv; + arith_util a; + scoped_ptr<::solver> m_solver; + obj_map m_new_funs; + expr_ref_vector m_translate, m_args; + ast_ref_vector m_pinned; + sat::literal_vector m_core; + ptr_vector m_bv2int, m_int2bv; + statistics m_stats; + bool m_is_plugin = true; // when the solver is used as a plugin, then do not translate below quantifiers. + + bool is_bv(sat::literal lit); + void translate(expr_ref_vector& es); + void sorted_subterms(expr_ref_vector& es, ptr_vector& sorted); + + + + bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); } + expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; } + void set_translated(expr* e, expr* r); + expr* arg(unsigned i) { return m_args.get(i); } + + expr* umod(expr* bv_expr, unsigned i); + expr* smod(expr* bv_expr, unsigned i); + rational bv_size(expr* bv_expr); + + void translate_expr(expr* e); + void translate_bv(app* e); + void translate_basic(app* e); + void translate_app(app* e); + void translate_quantifier(quantifier* q); + void translate_var(var* v); + + void ensure_translated(expr* e); + void internalize_bv(app* e); + + unsigned m_vars_qhead = 0, m_preds_qhead = 0; + ptr_vector m_vars, m_preds; + bool add_bound_axioms(); + bool add_predicate_axioms(); + + euf::theory_var mk_var(euf::enode* n) override; + + void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values); + void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values); + + public: + solver(euf::solver& ctx); + + ~solver() override {} + + lbool check_solver_state(); + + sat::literal_vector const& unsat_core(); + + void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; + + bool add_dep(euf::enode* n, top_sort& dep) override; + + std::ostream& display(std::ostream& out) const override; + + void collect_statistics(statistics& st) const override; + + bool unit_propagate() override; + + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {} + + sat::check_result check() override; + + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return out; } + + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out; } + + euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } + + void internalize(expr* e) override; + + bool visited(expr* e) override; + + bool post_visit(expr* e, bool sign, bool root) override; + + bool visit(expr* e) override; + + sat::literal internalize(expr* e, bool, bool) override; + + void eq_internalized(euf::enode* n) override; + + rational get_value(expr* e) const; + + }; + +} diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 300bef1fb..b882c1abf 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -54,6 +54,7 @@ def_module_params(module_name='smt', ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'), ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'), ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'), + ('bv.solver', UINT, 1, '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.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index 734a983fb..8a3ddcf37 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -28,6 +28,7 @@ void theory_bv_params::updt_params(params_ref const & _p) { m_bv_enable_int2bv2int = p.bv_enable_int2bv(); m_bv_delay = p.bv_delay(); m_bv_size_reduce = p.bv_size_reduce(); + m_bv_solver = p.bv_solver(); } #define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; @@ -42,4 +43,5 @@ void theory_bv_params::display(std::ostream & out) const { DISPLAY_PARAM(m_bv_enable_int2bv2int); DISPLAY_PARAM(m_bv_delay); DISPLAY_PARAM(m_bv_size_reduce); + DISPLAY_PARAM(m_bv_solver); } diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 523459f09..97428c8ba 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -36,6 +36,7 @@ struct theory_bv_params { bool m_bv_watch_diseq = false; bool m_bv_delay = true; bool m_bv_size_reduce = false; + unsigned m_bv_solver = 0; theory_bv_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index cfc1f06f2..b794a44b5 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -915,7 +915,7 @@ namespace smt { } SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr)); d->m_recognizers[c_idx] = recognizer; - m_trail_stack.push(set_vector_idx_trail(d->m_recognizers, c_idx)); + m_trail_stack.push(set_vector_idx_trail(d->m_recognizers, c_idx)); if (val == l_false) { propagate_recognizer(v, recognizer); } diff --git a/src/util/trail.h b/src/util/trail.h index 1aa7e4441..43e698234 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -219,12 +219,12 @@ public: } }; -template +template class set_vector_idx_trail : public trail { - ptr_vector & m_vector; + V & m_vector; unsigned m_idx; public: - set_vector_idx_trail(ptr_vector & v, unsigned idx): + set_vector_idx_trail(V & v, unsigned idx): m_vector(v), m_idx(idx) { } From 4778f27b46aba4171a05c385ed2bb1cf0694cc95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 14:33:23 -0800 Subject: [PATCH 27/33] revert to standard solver Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index b882c1abf..455dd9240 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -54,7 +54,7 @@ def_module_params(module_name='smt', ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'), ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'), ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'), - ('bv.solver', UINT, 1, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'), + ('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.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), From b44ab2f6204b12d338cccdfa28449cc5c0993553 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 14:55:02 -0800 Subject: [PATCH 28/33] add rewriters for and Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 29 +++++++++++++++++++++++++++++ src/ast/rewriter/arith_rewriter.h | 1 + 2 files changed, 30 insertions(+) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 44b91826f..ddfabed83 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -91,6 +91,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_SINH: SASSERT(num_args == 1); st = mk_sinh_core(args[0], result); break; case OP_COSH: SASSERT(num_args == 1); st = mk_cosh_core(args[0], result); break; case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break; + case OP_ARITH_BAND: SASSERT(num_args == 2); st = mk_band_core(f->get_parameter(0).get_int(), args[0], args[1], result); break; default: st = BR_FAILED; break; } CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m); @@ -1349,6 +1350,34 @@ app* arith_rewriter_core::mk_power(expr* x, rational const& r, sort* s) { return y; } +br_status arith_rewriter::mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) { + numeral x, y, N; + bool is_num_x = m_util.is_numeral(arg1, x); + bool is_num_y = m_util.is_numeral(arg2, y); + N = rational::power_of_two(sz); + if (is_num_x) + x = mod(x, N); + if (is_num_y) + y = mod(y, N); + if (is_num_x && x.is_zero()) { + result = m_util.mk_int(0); + return BR_DONE; + } + if (is_num_y && y.is_zero()) { + result = m_util.mk_int(0); + return BR_DONE; + } + if (is_num_x && is_num_y) { + rational r(0); + for (unsigned i = 0; i < sz; ++i) + if (x.get_bit(i) && y.get_bit(i)) + r += rational::power_of_two(i); + result = m_util.mk_int(r); + return BR_DONE; + } + return BR_FAILED; +} + br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & result) { numeral x, y; bool is_num_x = m_util.is_numeral(arg1, x); diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index edc84b25a..548ab80db 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -159,6 +159,7 @@ public: br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result); + br_status mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result); void mk_div(expr * arg1, expr * arg2, expr_ref & result) { if (mk_div_core(arg1, arg2, result) == BR_FAILED) result = m.mk_app(get_fid(), OP_DIV, arg1, arg2); From 50e0fd3ba66e4e2910a081e21671be2429a48ac5 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 16 Dec 2023 19:14:53 +0700 Subject: [PATCH 29/33] Use `noexcept` more. (#7058) --- src/ast/recfun_decl_plugin.cpp | 9 --------- src/ast/recfun_decl_plugin.h | 6 ------ src/math/dd/dd_pdd.h | 4 ++-- src/math/lp/lp_core_solver_base.h | 2 +- src/math/polynomial/algebraic_numbers.cpp | 4 ++-- src/math/polynomial/algebraic_numbers.h | 2 +- src/math/polynomial/polynomial.cpp | 2 +- src/math/polynomial/upolynomial.cpp | 2 +- src/math/polynomial/upolynomial.h | 2 +- src/math/polynomial/upolynomial_factorization_int.h | 2 +- src/math/realclosure/mpz_matrix.h | 4 ++-- src/math/realclosure/realclosure.cpp | 6 +++--- src/math/realclosure/realclosure.h | 2 +- src/muz/rel/dl_base.h | 4 ++-- src/muz/rel/dl_finite_product_relation.cpp | 2 +- src/muz/rel/dl_finite_product_relation.h | 2 +- src/muz/rel/dl_vector_relation.h | 2 +- src/nlsat/nlsat_assignment.h | 4 ++-- src/nlsat/nlsat_scoped_literal_vector.h | 2 +- src/nlsat/nlsat_solver.cpp | 2 +- src/sat/sat_cutset.h | 2 +- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_model_converter.h | 2 +- src/sat/smt/pb_card.h | 2 +- src/sat/smt/pb_constraint.h | 2 +- src/sat/smt/pb_pb.h | 2 +- src/smt/old_interval.cpp | 2 +- src/smt/old_interval.h | 2 +- src/util/array.h | 2 +- src/util/basic_interval.h | 6 +++--- src/util/bit_vector.h | 2 +- src/util/chashtable.h | 2 +- src/util/double_manager.h | 2 +- src/util/f2n.h | 4 ++-- src/util/hashtable.h | 2 +- src/util/heap.h | 2 +- src/util/hwf.h | 2 +- src/util/inf_eps_rational.h | 2 +- src/util/inf_int_rational.h | 2 +- src/util/inf_rational.h | 2 +- src/util/inf_s_integer.h | 2 +- src/util/map.h | 2 +- src/util/mpbq.h | 6 +++--- src/util/mpf.cpp | 2 +- src/util/mpf.h | 4 ++-- src/util/mpff.h | 6 +++--- src/util/mpfx.h | 6 +++--- src/util/mpq.h | 4 ++-- src/util/mpq_inf.h | 2 +- src/util/mpz.h | 6 +++--- src/util/mpzzp.h | 2 +- src/util/numeral_buffer.h | 2 +- src/util/obj_hashtable.h | 2 +- src/util/obj_ref.h | 4 ++-- src/util/obj_ref_hashtable.h | 2 +- src/util/optional.h | 2 +- src/util/permutation.cpp | 2 +- src/util/permutation.h | 2 +- src/util/rational.h | 4 ++-- src/util/ref.h | 4 ++-- src/util/ref_pair_vector.h | 6 +++--- src/util/ref_vector.h | 6 +++--- src/util/s_integer.h | 2 +- src/util/scoped_numeral.h | 4 ++-- src/util/scoped_ptr_vector.h | 4 ++-- src/util/tbv.h | 2 +- src/util/uint_set.h | 2 +- src/util/util.h | 4 ++-- src/util/vector.h | 2 +- 69 files changed, 97 insertions(+), 112 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 7a3e9521d..495f3cb20 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -602,15 +602,6 @@ namespace recfun { m_args.append(n->get_num_args(), n->get_args()); } - case_expansion::case_expansion(case_expansion const & from) - : m_lhs(from.m_lhs), - m_def(from.m_def), - m_args(from.m_args) {} - case_expansion::case_expansion(case_expansion && from) - : m_lhs(from.m_lhs), - m_def(from.m_def), - m_args(std::move(from.m_args)) {} - std::ostream& case_expansion::display(std::ostream & out) const { return out << "case_exp(" << m_lhs << ")"; } diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 442bdadbd..3a1dc8e84 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -301,8 +301,6 @@ namespace recfun { recfun::def * m_def; expr_ref_vector m_args; case_expansion(recfun::util& u, app * n); - case_expansion(case_expansion const & from); - case_expansion(case_expansion && from); std::ostream& display(std::ostream& out) const; }; @@ -323,10 +321,6 @@ namespace recfun { } body_expansion(app_ref & pred, recfun::case_def const & d, expr_ref_vector & args) : m_pred(pred), m_cdef(&d), m_args(args) {} - body_expansion(body_expansion const & from): - m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {} - body_expansion(body_expansion && from) noexcept : - m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {} std::ostream& display(std::ostream& out) const; }; diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 2dc9a9480..fa545c06e 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -503,7 +503,7 @@ namespace dd { unsigned max_pow2_divisor() const { return m->max_pow2_divisor(root); } unsigned_vector const& free_vars() const { return m->free_vars(*this); } - void swap(pdd& other) { VERIFY_EQ(m, other.m); std::swap(root, other.root); } + void swap(pdd& other) noexcept { VERIFY_EQ(m, other.m); std::swap(root, other.root); } pdd_iterator begin() const; pdd_iterator end() const; @@ -547,7 +547,7 @@ namespace dd { inline pdd& operator-=(pdd & p, rational const& q) { p = p - q; return p; } inline pdd& operator+=(pdd & p, rational const& q) { p = p + q; return p; } - inline void swap(pdd& p, pdd& q) { p.swap(q); } + inline void swap(pdd& p, pdd& q) noexcept { p.swap(q); } std::ostream& operator<<(std::ostream& out, pdd const& b); diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 099c692c6..a5b79e9c8 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -517,7 +517,7 @@ public: template - static void swap(vector &v, unsigned i, unsigned j) { + static void swap(vector &v, unsigned i, unsigned j) noexcept { auto t = v[i]; v[i] = v[j]; v[j] = t; diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 1a4769ac3..736d08708 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -358,7 +358,7 @@ namespace algebraic_numbers { return a.to_algebraic()->m_p_sz - 1; } - void swap(numeral & a, numeral & b) { + void swap(numeral & a, numeral & b) noexcept { std::swap(a.m_cell, b.m_cell); } @@ -2935,7 +2935,7 @@ namespace algebraic_numbers { return m_imp->to_rational(const_cast(a), r); } - void manager::swap(numeral & a, numeral & b) { + void manager::swap(numeral & a, numeral & b) noexcept { return m_imp->swap(a, b); } diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index 00af9a7a8..63b833b80 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -129,7 +129,7 @@ namespace algebraic_numbers { void set(numeral & a, mpq const & n); void set(numeral & a, numeral const & n); - void swap(numeral & a, numeral & b); + void swap(numeral & a, numeral & b) noexcept; /** \brief Store in b an integer value smaller than 'a'. diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index a352d1d37..dde4a5f80 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -447,7 +447,7 @@ namespace polynomial { } }; - inline void swap(monomial * & m1, monomial * & m2) { std::swap(m1, m2); } + inline void swap(monomial * & m1, monomial * & m2) noexcept { std::swap(m1, m2); } typedef chashtable monomial_table; diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index ac0aec8ef..a354ed295 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -126,7 +126,7 @@ namespace upolynomial { m_factors[i].swap(p); } - void core_manager::factors::swap(factors & other) { + void core_manager::factors::swap(factors & other) noexcept { m_factors.swap(other.m_factors); m_degrees.swap(other.m_degrees); nm().swap(m_constant, other.m_constant); diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index faa0e5e09..2afdbb7b3 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -89,7 +89,7 @@ namespace upolynomial { void push_back_swap(numeral_vector & p, unsigned degree); void swap_factor(unsigned i, numeral_vector & p); - void swap(factors & other); + void swap(factors & other) noexcept; void multiply(numeral_vector & out) const; void display(std::ostream & out) const; diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h index e66fd2f1b..a65e5ee62 100644 --- a/src/math/polynomial/upolynomial_factorization_int.h +++ b/src/math/polynomial/upolynomial_factorization_int.h @@ -85,7 +85,7 @@ namespace upolynomial { unsigned max_degree() const { return m_set.size() - 1; } - void swap(factorization_degree_set & other) { + void swap(factorization_degree_set & other) noexcept { m_set.swap(other.m_set); } diff --git a/src/math/realclosure/mpz_matrix.h b/src/math/realclosure/mpz_matrix.h index 878fb72f9..91fe22681 100644 --- a/src/math/realclosure/mpz_matrix.h +++ b/src/math/realclosure/mpz_matrix.h @@ -50,7 +50,7 @@ public: SASSERT(j < n); return a_ij[i*n + j]; } mpz & operator()(unsigned i, unsigned j) { SASSERT(i < m); SASSERT(j < n); return a_ij[i*n + j]; } - void swap(mpz_matrix & B) { std::swap(m, B.m); std::swap(n, B.n); std::swap(a_ij, B.a_ij); } + void swap(mpz_matrix & B) noexcept { std::swap(m, B.m); std::swap(n, B.n); std::swap(a_ij, B.a_ij); } mpz * row(unsigned i) const { SASSERT(i < m); return a_ij + i*n; } }; @@ -136,7 +136,7 @@ public: mpz_matrix const & get() const { return A; } mpz_matrix & get() { return A; } - void swap(mpz_matrix & B) { A.swap(B); } + void swap(mpz_matrix & B) noexcept { A.swap(B); } void set(unsigned i, unsigned j, mpz const & v) { nm().set(A(i, j), v); } void set(unsigned i, unsigned j, int v) { nm().set(A(i, j), v); } diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index d179ec575..ecea560a5 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -135,7 +135,7 @@ namespace realclosure { typedef interval_manager mpbqi_manager; typedef mpbqi_manager::interval mpbqi; - void swap(mpbqi & a, mpbqi & b) { + void swap(mpbqi & a, mpbqi & b) noexcept { swap(a.m_lower, b.m_lower); swap(a.m_upper, b.m_upper); std::swap(a.m_lower_inf, b.m_lower_inf); @@ -2534,7 +2534,7 @@ namespace realclosure { return depends_on_infinitesimals(a.m_value); } - static void swap(mpbqi & a, mpbqi & b) { + static void swap(mpbqi & a, mpbqi & b) noexcept { realclosure::swap(a, b); } @@ -6313,7 +6313,7 @@ namespace realclosure { m_imp->set(a, n); } - void manager::swap(numeral & a, numeral & b) { + void manager::swap(numeral & a, numeral & b) noexcept { std::swap(a.m_value, b.m_value); } diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index f63b43a5d..12247627b 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -164,7 +164,7 @@ namespace realclosure { void set(numeral & a, mpq const & n); void set(numeral & a, numeral const & n); - void swap(numeral & a, numeral & b); + void swap(numeral & a, numeral & b) noexcept; /** \brief Return a^{1/k} diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index f6d031624..158df4906 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -484,7 +484,7 @@ namespace datalog { virtual bool can_swap(const base_object & o) const { return false; } - virtual void swap(base_object & o) { + virtual void swap(base_object & o) noexcept { std::swap(m_kind, o.m_kind); #if DL_LEAK_HUNTING m_leak_guard = get_plugin().get_ast_manager().mk_fresh_sort(get_plugin().get_name().bare_str()); @@ -910,7 +910,7 @@ namespace datalog { public: table_signature() : m_functional_columns(0) {} - void swap(table_signature & s) { + void swap(table_signature & s) noexcept { signature_base::swap(s); std::swap(m_functional_columns, s.m_functional_columns); } diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index b1cdf0553..293cc72e2 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -1835,7 +1835,7 @@ namespace datalog { } } - void finite_product_relation::swap(relation_base & r0) { + void finite_product_relation::swap(relation_base & r0) noexcept { SASSERT(can_swap(r0)); finite_product_relation & r = finite_product_relation_plugin::get(r0); SASSERT(get_signature()==r.get_signature()); diff --git a/src/muz/rel/dl_finite_product_relation.h b/src/muz/rel/dl_finite_product_relation.h index f1387437b..324564469 100644 --- a/src/muz/rel/dl_finite_product_relation.h +++ b/src/muz/rel/dl_finite_product_relation.h @@ -316,7 +316,7 @@ namespace datalog { Both relations must come from the same plugin and be of the same signature. */ - void swap(relation_base & r) override; + void swap(relation_base & r) noexcept override; /** \brief Create a \c finite_product_relation object. diff --git a/src/muz/rel/dl_vector_relation.h b/src/muz/rel/dl_vector_relation.h index ad9204b41..e61fc5a2a 100644 --- a/src/muz/rel/dl_vector_relation.h +++ b/src/muz/rel/dl_vector_relation.h @@ -59,7 +59,7 @@ namespace datalog { dealloc(m_elems); } - void swap(relation_base& other) override { + void swap(relation_base& other) noexcept override { vector_relation& o = dynamic_cast(other); if (&o == this) return; std::swap(o.m_eqs, m_eqs); diff --git a/src/nlsat/nlsat_assignment.h b/src/nlsat/nlsat_assignment.h index 6729b73cd..d96c8099e 100644 --- a/src/nlsat/nlsat_assignment.h +++ b/src/nlsat/nlsat_assignment.h @@ -33,7 +33,7 @@ namespace nlsat { public: assignment(anum_manager & _m):m_values(_m) {} anum_manager & am() const { return m_values.m(); } - void swap(assignment & other) { + void swap(assignment & other) noexcept { m_values.swap(other.m_values); m_assigned.swap(other.m_assigned); } @@ -67,7 +67,7 @@ namespace nlsat { anum_manager & m() const override { return am(); } bool contains(var x) const override { return is_assigned(x); } anum const & operator()(var x) const override { SASSERT(is_assigned(x)); return value(x); } - void swap(var x, var y) { + void swap(var x, var y) noexcept { SASSERT(x < m_values.size() && y < m_values.size()); std::swap(m_assigned[x], m_assigned[y]); std::swap(m_values[x], m_values[y]); diff --git a/src/nlsat/nlsat_scoped_literal_vector.h b/src/nlsat/nlsat_scoped_literal_vector.h index a2b617e55..9b4b62fe8 100644 --- a/src/nlsat/nlsat_scoped_literal_vector.h +++ b/src/nlsat/nlsat_scoped_literal_vector.h @@ -67,7 +67,7 @@ namespace nlsat { void append(scoped_literal_vector const& ls) { append(ls.size(), ls.data()); } - void swap(scoped_literal_vector& other) { + void swap(scoped_literal_vector& other) noexcept { SASSERT(&m_solver == &other.m_solver); m_lits.swap(other.m_lits); } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 8993182a2..40bdd10d6 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -48,7 +48,7 @@ namespace nlsat { typedef chashtable root_atom_table; // for apply_permutation procedure - void swap(clause * & c1, clause * & c2) { + void swap(clause * & c1, clause * & c2) noexcept { std::swap(c1, c2); } diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h index cb97c41d4..f8451d412 100644 --- a/src/sat/sat_cutset.h +++ b/src/sat/sat_cutset.h @@ -183,7 +183,7 @@ namespace sat { void reset(on_update_t& on_del) { shrink(on_del, 0); } cut const & operator[](unsigned idx) const { return m_cuts[idx]; } void shrink(on_update_t& on_del, unsigned j); - void swap(cut_set& other) { + void swap(cut_set& other) noexcept { std::swap(m_var, other.m_var); std::swap(m_size, other.m_size); std::swap(m_max_size, other.m_max_size); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 27cc6823a..ddb277e9b 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -369,7 +369,7 @@ namespace sat { return result; } - void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) { + void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) noexcept { for (unsigned j = 0; j < sz; ++j) { if (v == clause[j].var()) { std::swap(clause[0], clause[j]); diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 8a3891797..a331bef8e 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -91,7 +91,7 @@ namespace sat { bool legal_to_flip(bool_var v) const; - void swap(bool_var v, unsigned sz, literal_vector& clause); + void swap(bool_var v, unsigned sz, literal_vector& clause) noexcept; void add_elim_stack(entry & e); diff --git a/src/sat/smt/pb_card.h b/src/sat/smt/pb_card.h index 6df50d81c..26c6d3bb1 100644 --- a/src/sat/smt/pb_card.h +++ b/src/sat/smt/pb_card.h @@ -33,7 +33,7 @@ namespace pb { literal const* begin() const { return m_lits; } literal const* end() const { return static_cast(m_lits) + m_size; } void negate() override; - void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); } + void swap(unsigned i, unsigned j) noexcept override { std::swap(m_lits[i], m_lits[j]); } literal_vector literals() const override { return literal_vector(m_size, m_lits); } bool is_watching(literal l) const override; literal get_lit(unsigned i) const override { return m_lits[i]; } diff --git a/src/sat/smt/pb_constraint.h b/src/sat/smt/pb_constraint.h index d8cec6de9..26c5f8b08 100644 --- a/src/sat/smt/pb_constraint.h +++ b/src/sat/smt/pb_constraint.h @@ -102,7 +102,7 @@ namespace pb { virtual bool is_watching(literal l) const { UNREACHABLE(); return false; }; virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); } - virtual void swap(unsigned i, unsigned j) { UNREACHABLE(); } + virtual void swap(unsigned i, unsigned j) noexcept { UNREACHABLE(); } virtual literal get_lit(unsigned i) const { UNREACHABLE(); return sat::null_literal; } virtual void set_lit(unsigned i, literal l) { UNREACHABLE(); } virtual void negate() { UNREACHABLE(); } diff --git a/src/sat/smt/pb_pb.h b/src/sat/smt/pb_pb.h index 5db177d07..169fe2479 100644 --- a/src/sat/smt/pb_pb.h +++ b/src/sat/smt/pb_pb.h @@ -46,7 +46,7 @@ namespace pb { bool is_cardinality() const; void negate() override; void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); } - void swap(unsigned i, unsigned j) override { std::swap(m_wlits[i], m_wlits[j]); } + void swap(unsigned i, unsigned j) noexcept override { std::swap(m_wlits[i], m_wlits[j]); } literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } bool is_watching(literal l) const override; literal get_lit(unsigned i) const override { return m_wlits[i].second; } diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index e719f7e2b..c4d49d00a 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -238,7 +238,7 @@ interval & interval::operator=(interval const & other) { return *this; } -interval & interval::operator=(interval && other) { +interval & interval::operator=(interval && other) noexcept { SASSERT(&m_manager == &other.m_manager); m_lower = std::move(other.m_lower); m_upper = std::move(other.m_upper); diff --git a/src/smt/old_interval.h b/src/smt/old_interval.h index 7a6f41e26..bf68a0d26 100644 --- a/src/smt/old_interval.h +++ b/src/smt/old_interval.h @@ -92,7 +92,7 @@ public: rational const & get_lower_value() const { SASSERT(!minus_infinity()); return m_lower.to_rational(); } rational const & get_upper_value() const { SASSERT(!plus_infinity()); return m_upper.to_rational(); } old_interval & operator=(old_interval const & other); - old_interval & operator=(old_interval && other); + old_interval & operator=(old_interval && other) noexcept; old_interval & operator+=(old_interval const & other); old_interval & operator-=(old_interval const & other); old_interval & operator*=(old_interval const & other); diff --git a/src/util/array.h b/src/util/array.h index a4c2aa2c7..2954035f6 100644 --- a/src/util/array.h +++ b/src/util/array.h @@ -184,7 +184,7 @@ public: T const * data() const { return m_data; } T * data() { return m_data; } - void swap(array & other) { + void swap(array & other) noexcept { std::swap(m_data, other.m_data); } diff --git a/src/util/basic_interval.h b/src/util/basic_interval.h index ca5868b88..ea35259a0 100644 --- a/src/util/basic_interval.h +++ b/src/util/basic_interval.h @@ -52,8 +52,8 @@ public: interval const & get() const { return m_interval; } interval & get() { return m_interval; } void reset() { m().reset(m_interval); } - void swap(scoped_interval & a) { m().swap(m_interval, a.m_interval); } - void swap(interval & a) { m().swap(m_interval, a); } + void swap(scoped_interval & a) noexcept { m().swap(m_interval, a.m_interval); } + void swap(interval & a) noexcept { m().swap(m_interval, a); } bound const & lower() const { return m_interval.lower(); } bound const & upper() const { return m_interval.upper(); } bound & lower() { return m_interval.lower(); } @@ -146,7 +146,7 @@ public: m().set(a.m_upper, n); } - void swap(interval & a, interval & b) { + void swap(interval & a, interval & b) noexcept { m().swap(a.m_lower, b.m_lower); m().swap(a.m_upper, b.m_upper); } diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index cb29bdd9c..12f86dd00 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -98,7 +98,7 @@ public: m_num_bits = 0; } - void swap(bit_vector & other) { + void swap(bit_vector & other) noexcept { std::swap(m_data, other.m_data); std::swap(m_num_bits, other.m_num_bits); std::swap(m_capacity, other.m_capacity); diff --git a/src/util/chashtable.h b/src/util/chashtable.h index 3a2d2685b..450d2bfa4 100644 --- a/src/util/chashtable.h +++ b/src/util/chashtable.h @@ -553,7 +553,7 @@ public: iterator begin() const { return iterator(m_table, m_table + m_slots); } iterator end() const { return iterator(); } - void swap(chashtable & other) { + void swap(chashtable & other) noexcept { std::swap(m_table, other.m_table); std::swap(m_capacity, other.m_capacity); std::swap(m_init_slots, other.m_init_slots); diff --git a/src/util/double_manager.h b/src/util/double_manager.h index 6bd691d24..c21894582 100644 --- a/src/util/double_manager.h +++ b/src/util/double_manager.h @@ -76,7 +76,7 @@ public: static void set(double & a, unsigned val) { a = static_cast(val); } static void set(double & a, int64_t val) { a = static_cast(val); } static void set(double & a, uint64_t val) { a = static_cast(val); } - static void swap(double & a, double & b) { std::swap(a, b); } + static void swap(double & a, double & b) noexcept { std::swap(a, b); } bool is_pos(double a) const { return a > m_zero_tolerance; } bool is_neg(double a) const { return a < m_zero_tolerance; } bool is_zero(double a) const { return -m_zero_tolerance <= a && a <= m_zero_tolerance; } diff --git a/src/util/f2n.h b/src/util/f2n.h index 2b6c9799a..e94c21ce2 100644 --- a/src/util/f2n.h +++ b/src/util/f2n.h @@ -45,7 +45,7 @@ public: m_manager.set(m_one, ebits, sbits, 1); } - f2n(f2n && other) : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits), + f2n(f2n && other) noexcept : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits), m_tmp1(std::move(other.m_tmp1)), m_one(std::move(other.m_one)) {} ~f2n() { @@ -86,7 +86,7 @@ public: void set(numeral & o, numeral const & x) { m().set(o, x); check(o); } void set(numeral & o, mpq const & x) { m().set(o, m_ebits, m_sbits, m_mode, x); check(o); } void reset(numeral & o) { m().reset(o, m_ebits, m_sbits); } - static void swap(numeral & x, numeral & y) { x.swap(y); } + static void swap(numeral & x, numeral & y) noexcept { x.swap(y); } void add(numeral const & x, numeral const & y, numeral & o) { m().add(m_mode, x, y, o); check(o); } void sub(numeral const & x, numeral const & y, numeral & o) { m().sub(m_mode, x, y, o); check(o); } diff --git a/src/util/hashtable.h b/src/util/hashtable.h index cfe4d20ca..b2830326b 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -283,7 +283,7 @@ public: delete_table(); } - void swap(core_hashtable & source) { + void swap(core_hashtable & source) noexcept { std::swap(m_table, source.m_table); std::swap(m_capacity, source.m_capacity); std::swap(m_size, source.m_size); diff --git a/src/util/heap.h b/src/util/heap.h index 332f4e53e..c080c6ebd 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -259,7 +259,7 @@ public: return m_values.end(); } - void swap(heap & other) { + void swap(heap & other) noexcept { if (this != &other) { CASSERT("heap", other.check_invariant()); CASSERT("heap", check_invariant()); diff --git a/src/util/hwf.h b/src/util/hwf.h index 4e1081ebf..209a8fe77 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -35,7 +35,7 @@ class hwf { } public: - void swap(hwf & other) { std::swap(value, other.value); } + void swap(hwf & other) noexcept { std::swap(value, other.value); } }; diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h index b28a6d794..ea7ec52fc 100644 --- a/src/util/inf_eps_rational.h +++ b/src/util/inf_eps_rational.h @@ -38,7 +38,7 @@ class inf_eps_rational { struct eq_proc { bool operator()(inf_eps_rational const& r1, inf_eps_rational const& r2) const { return r1 == r2; } }; - void swap(inf_eps_rational & n) { + void swap(inf_eps_rational & n) noexcept { m_infty.swap(n.m_infty); m_r.swap(n.m_r); } diff --git a/src/util/inf_int_rational.h b/src/util/inf_int_rational.h index 458843cb0..2025af319 100644 --- a/src/util/inf_int_rational.h +++ b/src/util/inf_int_rational.h @@ -43,7 +43,7 @@ class inf_int_rational { struct eq_proc { bool operator()(inf_int_rational const& r1, inf_int_rational const& r2) const { return r1 == r2; } }; - void swap(inf_int_rational & n) { + void swap(inf_int_rational & n) noexcept { m_first.swap(n.m_first); std::swap(m_second, n.m_second); } diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index fb8a71e5f..2d7963ff0 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -44,7 +44,7 @@ class inf_rational { struct eq_proc { bool operator()(inf_rational const& r1, inf_rational const& r2) const { return r1 == r2; } }; - void swap(inf_rational & n) { + void swap(inf_rational & n) noexcept { m_first.swap(n.m_first); m_second.swap(n.m_second); } diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h index b99167b32..a02ba70fd 100644 --- a/src/util/inf_s_integer.h +++ b/src/util/inf_s_integer.h @@ -37,7 +37,7 @@ class inf_s_integer { struct eq_proc { bool operator()(inf_s_integer const& r1, inf_s_integer const& r2) const { return r1 == r2; } }; - void swap(inf_s_integer & n) { + void swap(inf_s_integer & n) noexcept { std::swap(m_first, n.m_first); std::swap(m_second, n.m_second); } diff --git a/src/util/map.h b/src/util/map.h index e9880e0a0..0068be31b 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -184,7 +184,7 @@ public: unsigned long long get_num_collision() const { return m_table.get_num_collision(); } - void swap(table2map & other) { + void swap(table2map & other) noexcept { m_table.swap(other.m_table); } diff --git a/src/util/mpbq.h b/src/util/mpbq.h index 13cd6ae0c..edd864dc3 100644 --- a/src/util/mpbq.h +++ b/src/util/mpbq.h @@ -40,10 +40,10 @@ public: mpbq(int v, unsigned k):m_num(v), m_k(k) {} mpz const & numerator() const { return m_num; } unsigned k() const { return m_k; } - void swap(mpbq & other) { m_num.swap(other.m_num); std::swap(m_k, other.m_k); } + void swap(mpbq & other) noexcept { m_num.swap(other.m_num); std::swap(m_k, other.m_k); } }; -inline void swap(mpbq & m1, mpbq & m2) { m1.swap(m2); } +inline void swap(mpbq & m1, mpbq & m2) noexcept { m1.swap(m2); } typedef svector mpbq_vector; @@ -72,7 +72,7 @@ public: mpbq_manager(unsynch_mpz_manager & m); ~mpbq_manager(); - static void swap(mpbq & a, mpbq & b) { a.swap(b); } + static void swap(mpbq & a, mpbq & b) noexcept { a.swap(b); } void del(mpbq & a) { m_manager.del(a.m_num); } void reset(mpbq & a) { m_manager.reset(a.m_num); a.m_k = 0; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 605b12aab..da0e10571 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -41,7 +41,7 @@ mpf::mpf(unsigned _ebits, unsigned _sbits): set(ebits, sbits); } -void mpf::swap(mpf & other) { +void mpf::swap(mpf & other) noexcept { unsigned tmp = ebits; ebits = other.ebits; other.ebits = tmp; diff --git a/src/util/mpf.h b/src/util/mpf.h index 2c3e528d3..b979e78c1 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -52,7 +52,7 @@ public: mpf & operator=(mpf const & other) = delete; unsigned get_ebits() const { return ebits; } unsigned get_sbits() const { return sbits; } - void swap(mpf & other); + void swap(mpf & other) noexcept; }; class mpf_manager { @@ -87,7 +87,7 @@ public: void neg(mpf & o); void neg(mpf const & x, mpf & o); - void swap(mpf& a, mpf& b) { a.swap(b); } + void swap(mpf& a, mpf& b) noexcept { a.swap(b); } bool is_zero(mpf const & x); bool is_neg(mpf const & x); diff --git a/src/util/mpff.h b/src/util/mpff.h index c9012a2d0..254c52572 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -44,14 +44,14 @@ public: m_exponent(0) { } - void swap(mpff & other) { + void swap(mpff & other) noexcept { unsigned sign = m_sign; m_sign = other.m_sign; other.m_sign = sign; unsigned sig_idx = m_sig_idx; m_sig_idx = other.m_sig_idx; other.m_sig_idx = sig_idx; std::swap(m_exponent, other.m_exponent); } }; -inline void swap(mpff & m1, mpff & m2) { m1.swap(m2); } +inline void swap(mpff & m1, mpff & m2) noexcept { m1.swap(m2); } class mpz; class mpq; @@ -316,7 +316,7 @@ public: */ static void abs(mpff & a) { a.m_sign = 0; } - static void swap(mpff & a, mpff & b) { a.swap(b); } + static void swap(mpff & a, mpff & b) noexcept { a.swap(b); } /** \brief c <- a + b diff --git a/src/util/mpfx.h b/src/util/mpfx.h index 7f34e7dc1..c563c2872 100644 --- a/src/util/mpfx.h +++ b/src/util/mpfx.h @@ -38,13 +38,13 @@ public: m_sig_idx(0) { } - void swap(mpfx & other) { + void swap(mpfx & other) noexcept { unsigned sign = m_sign; m_sign = other.m_sign; other.m_sign = sign; unsigned sig_idx = m_sig_idx; m_sig_idx = other.m_sig_idx; other.m_sig_idx = sig_idx; } }; -inline void swap(mpfx & m1, mpfx & m2) { m1.swap(m2); } +inline void swap(mpfx & m1, mpfx & m2) noexcept { m1.swap(m2); } class mpz; class mpq; @@ -228,7 +228,7 @@ public: */ static void abs(mpfx & a) { a.m_sign = 0; } - static void swap(mpfx & a, mpfx & b) { a.swap(b); } + static void swap(mpfx & a, mpfx & b) noexcept { a.swap(b); } /** \brief c <- a + b diff --git a/src/util/mpq.h b/src/util/mpq.h index 1bdf8f31b..fa6e8ec75 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -761,9 +761,9 @@ public: return temp; } - void swap(mpz & a, mpz & b) { mpz_manager::swap(a, b); } + void swap(mpz & a, mpz & b) noexcept { mpz_manager::swap(a, b); } - void swap(mpq & a, mpq & b) { + void swap(mpq & a, mpq & b) noexcept { swap(a.m_num, b.m_num); swap(a.m_den, b.m_den); } diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h index e2bcbcba6..d8e9148e1 100644 --- a/src/util/mpq_inf.h +++ b/src/util/mpq_inf.h @@ -52,7 +52,7 @@ public: m.del(a.second); } - void swap(mpq_inf & a, mpq_inf & b) { + void swap(mpq_inf & a, mpq_inf & b) noexcept { m.swap(a.first, b.first); m.swap(a.second, b.second); } diff --git a/src/util/mpz.h b/src/util/mpz.h index bb1141ea7..44e3e9c0b 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -110,7 +110,7 @@ public: return *this; } - void swap(mpz & other) { + void swap(mpz & other) noexcept { std::swap(m_val, other.m_val); std::swap(m_ptr, other.m_ptr); unsigned o = m_owner; m_owner = other.m_owner; other.m_owner = o; @@ -131,7 +131,7 @@ public: class mpz_stack : public mpz {}; #endif -inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); } +inline void swap(mpz & m1, mpz & m2) noexcept { m1.swap(m2); } template class mpz_manager { @@ -573,7 +573,7 @@ public: // deallocates any memory. void reset(mpz & a); - void swap(mpz & a, mpz & b) { + void swap(mpz & a, mpz & b) noexcept { std::swap(a.m_val, b.m_val); std::swap(a.m_ptr, b.m_ptr); auto o = a.m_owner; a.m_owner = b.m_owner; b.m_owner = o; diff --git a/src/util/mpzzp.h b/src/util/mpzzp.h index 731b116ce..24fb64ea3 100644 --- a/src/util/mpzzp.h +++ b/src/util/mpzzp.h @@ -183,7 +183,7 @@ public: } } - void swap(mpz & a, mpz & b) { + void swap(mpz & a, mpz & b) noexcept { SASSERT(is_p_normalized(a) && is_p_normalized(b)); m().swap(a, b); } diff --git a/src/util/numeral_buffer.h b/src/util/numeral_buffer.h index 5bd678d78..1951b5449 100644 --- a/src/util/numeral_buffer.h +++ b/src/util/numeral_buffer.h @@ -81,7 +81,7 @@ public: m_buffer.reserve(sz); } - void swap(svector & other) { + void swap(svector & other) noexcept { m_buffer.swap(other); } diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 254f5f70d..49b37ca61 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -209,7 +209,7 @@ public: } } - void swap(obj_map & other) { + void swap(obj_map & other) noexcept { m_table.swap(other.m_table); } }; diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 04ae9e412..9ab68676d 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -93,7 +93,7 @@ public: return *this; } - obj_ref & operator=(obj_ref && n) { + obj_ref & operator=(obj_ref && n) noexcept { SASSERT(&m_manager == &n.m_manager); std::swap(m_obj, n.m_obj); n.reset(); @@ -105,7 +105,7 @@ public: m_obj = nullptr; } - void swap(obj_ref & n) { + void swap(obj_ref & n) noexcept { std::swap(m_obj, n.m_obj); } diff --git a/src/util/obj_ref_hashtable.h b/src/util/obj_ref_hashtable.h index d3e17a4a3..dba6550d4 100644 --- a/src/util/obj_ref_hashtable.h +++ b/src/util/obj_ref_hashtable.h @@ -104,7 +104,7 @@ public: unsigned long long get_num_collision() const { return m_table.get_num_collision(); } - void swap(obj_ref_map & other) { + void swap(obj_ref_map & other) noexcept { m_table.swap(other.m_table); } diff --git a/src/util/optional.h b/src/util/optional.h index 50a2148d1..8e515f4be 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -94,7 +94,7 @@ public: return * this; } - optional & operator=(optional && val) { + optional & operator=(optional && val) noexcept { std::swap(m_obj, val.m_obj); return *this; } diff --git a/src/util/permutation.cpp b/src/util/permutation.cpp index 5b20580eb..8b7adedf3 100644 --- a/src/util/permutation.cpp +++ b/src/util/permutation.cpp @@ -31,7 +31,7 @@ void permutation::reset(unsigned size) { } } -void permutation::swap(unsigned i, unsigned j) { +void permutation::swap(unsigned i, unsigned j) noexcept { unsigned i_prime = m_p[i]; unsigned j_prime = m_p[j]; std::swap(m_p[i], m_p[j]); diff --git a/src/util/permutation.h b/src/util/permutation.h index 1fb7dc9e7..dfc52b370 100644 --- a/src/util/permutation.h +++ b/src/util/permutation.h @@ -31,7 +31,7 @@ public: unsigned operator()(unsigned i) const { return m_p[i]; } unsigned inv(unsigned i_prime) const { return m_inv_p[i_prime]; } - void swap(unsigned i, unsigned j); + void swap(unsigned i, unsigned j) noexcept; void move_after(unsigned i, unsigned j); void display(std::ostream & out) const; diff --git a/src/util/rational.h b/src/util/rational.h index 88a0552ba..db60077ac 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -86,7 +86,7 @@ public: struct eq_proc { bool operator()(rational const& r1, rational const& r2) const { return r1 == r2; } }; - void swap(rational & n) { m().swap(m_val, n.m_val); } + void swap(rational & n) noexcept { m().swap(m_val, n.m_val); } std::string to_string() const { return m().to_string(m_val); } @@ -671,6 +671,6 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati return result; } -inline void swap(rational& r1, rational& r2) { +inline void swap(rational& r1, rational& r2) noexcept { r1.swap(r2); } diff --git a/src/util/ref.h b/src/util/ref.h index 1f30aae82..849e23b38 100644 --- a/src/util/ref.h +++ b/src/util/ref.h @@ -97,7 +97,7 @@ public: return *this; } - ref & operator=(ref &&r) { + ref & operator=(ref &&r) noexcept { if (this != &r) { dec_ref (); m_ptr = r.detach (); @@ -123,7 +123,7 @@ public: friend bool operator!=(const ref & r1, const ref & r2) { return r1.m_ptr != r2.m_ptr; } - friend void swap (ref &r1, ref &r2) { + friend void swap (ref &r1, ref &r2) noexcept { T* tmp = r1.m_ptr; r1.m_ptr = r2.m_ptr; r2.m_ptr = tmp; diff --git a/src/util/ref_pair_vector.h b/src/util/ref_pair_vector.h index 489767912..40f845af6 100644 --- a/src/util/ref_pair_vector.h +++ b/src/util/ref_pair_vector.h @@ -143,7 +143,7 @@ public: push_back(other[i]); } - void swap(unsigned idx1, unsigned idx2) { + void swap(unsigned idx1, unsigned idx2) noexcept { std::swap(m_nodes[idx1], m_nodes[idx2]); } @@ -179,7 +179,7 @@ public: this->append(other); } - ref_pair_vector(ref_pair_vector && other) : super(std::move(other)) {} + ref_pair_vector(ref_pair_vector && other) noexcept : super(std::move(other)) {} ref_pair_vector(TManager & m, unsigned sz, elem_t const * data): super(ref_manager_wrapper(m)) { @@ -194,7 +194,7 @@ public: return get_manager(); } - void swap(ref_pair_vector & other) { + void swap(ref_pair_vector & other) noexcept { SASSERT(&(this->m_manager) == &(other.m_manager)); this->m_nodes.swap(other.m_nodes); } diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index 406f7be61..3a8492c29 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -197,14 +197,14 @@ public: push_back(data[i]); } - void operator=(ref_vector_core && other) { + void operator=(ref_vector_core && other) noexcept { if (this != &other) { reset(); m_nodes = std::move(other.m_nodes); } } - void swap(unsigned idx1, unsigned idx2) { + void swap(unsigned idx1, unsigned idx2) noexcept { std::swap(m_nodes[idx1], m_nodes[idx2]); } @@ -262,7 +262,7 @@ public: return get_manager(); } - void swap(ref_vector & other) { + void swap(ref_vector & other) noexcept { SASSERT(&(this->m_manager) == &(other.m_manager)); this->m_nodes.swap(other.m_nodes); } diff --git a/src/util/s_integer.h b/src/util/s_integer.h index 506b4f0a3..6ddd2bf67 100644 --- a/src/util/s_integer.h +++ b/src/util/s_integer.h @@ -34,7 +34,7 @@ public: struct hash_proc { unsigned operator()(s_integer const& r) const { return r.hash(); } }; struct eq_proc { bool operator()(s_integer const& r1, s_integer const& r2) const { return r1 == r2; } }; - void swap(s_integer & n) { + void swap(s_integer & n) noexcept { std::swap(m_val, n.m_val); } diff --git a/src/util/scoped_numeral.h b/src/util/scoped_numeral.h index 65b75053d..b90ba640a 100644 --- a/src/util/scoped_numeral.h +++ b/src/util/scoped_numeral.h @@ -60,11 +60,11 @@ public: m().reset(m_num); } - void swap(_scoped_numeral & n) { + void swap(_scoped_numeral & n) noexcept { m().swap(m_num, n.m_num); } - void swap(numeral & n) { + void swap(numeral & n) noexcept { m().swap(m_num, n); } diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h index 3c33cc708..90afbb6ef 100644 --- a/src/util/scoped_ptr_vector.h +++ b/src/util/scoped_ptr_vector.h @@ -34,7 +34,7 @@ public: scoped_ptr_vector(scoped_ptr_vector&& other) noexcept { m_vector.swap(other.m_vector); } - scoped_ptr_vector& operator=(scoped_ptr_vector&& other) { + scoped_ptr_vector& operator=(scoped_ptr_vector&& other) noexcept { if (this == &other) return *this; reset(); @@ -55,7 +55,7 @@ public: dealloc(m_vector[idx]); m_vector[idx] = ptr; } - void swap(unsigned i, unsigned j) { std::swap(m_vector[i], m_vector[j]); } + void swap(unsigned i, unsigned j) noexcept { std::swap(m_vector[i], m_vector[j]); } unsigned size() const { return m_vector.size(); } bool empty() const { return m_vector.empty(); } void resize(unsigned sz) { diff --git a/src/util/tbv.h b/src/util/tbv.h index cffdc2460..3bda89b3f 100644 --- a/src/util/tbv.h +++ b/src/util/tbv.h @@ -135,7 +135,7 @@ class tbv_ref { public: tbv_ref(tbv_manager& mgr) : mgr(mgr), d(nullptr) {} tbv_ref(tbv_manager& mgr, tbv* d) : mgr(mgr), d(d) {} - tbv_ref(tbv_ref&& d) : mgr(d.mgr), d(d.detach()) {} + tbv_ref(tbv_ref&& d) noexcept : mgr(d.mgr), d(d.detach()) {} ~tbv_ref() { if (d) mgr.deallocate(d); } diff --git a/src/util/uint_set.h b/src/util/uint_set.h index 2106d7af8..73c3bce1f 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -28,7 +28,7 @@ public: typedef unsigned data; - void swap(uint_set & other) { + void swap(uint_set & other) noexcept { unsigned_vector::swap(other); } diff --git a/src/util/util.h b/src/util/util.h index 275374512..a4bf78073 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -265,7 +265,7 @@ public: return *this; } - scoped_ptr& operator=(scoped_ptr&& other) { + scoped_ptr& operator=(scoped_ptr&& other) noexcept { *this = other.detach(); return *this; }; @@ -276,7 +276,7 @@ public: return tmp; } - void swap(scoped_ptr & p) { + void swap(scoped_ptr & p) noexcept { std::swap(m_ptr, p.m_ptr); } }; diff --git a/src/util/vector.h b/src/util/vector.h index 55b52d745..ea621b5fb 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -330,7 +330,7 @@ public: return *this; } - vector & operator=(vector && source) { + vector & operator=(vector && source) noexcept { if (this == &source) { return *this; } From d0a59f37404c7ccf0d2e13eda40dd8da3f6884d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Dec 2023 15:12:57 -0800 Subject: [PATCH 30/33] intblast with lazy expansion of shl, ashr, lshr Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 21 +++- src/ast/arith_decl_plugin.h | 31 ++++-- src/ast/rewriter/arith_rewriter.cpp | 103 +++++++++++++++++++ src/ast/rewriter/arith_rewriter.h | 3 + src/math/lp/lp_api.h | 4 +- src/sat/smt/arith_axioms.cpp | 149 ++++++++++++++++++++++------ src/sat/smt/arith_internalize.cpp | 8 +- src/sat/smt/arith_solver.cpp | 2 +- src/sat/smt/arith_solver.h | 8 +- src/sat/smt/intblast_solver.cpp | 75 ++++++++------ 10 files changed, 321 insertions(+), 83 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 8317b37c3..f09daaf75 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -508,6 +508,19 @@ static bool is_const_op(decl_kind k) { //k == OP_0_PW_0_REAL; } +symbol arith_decl_plugin::bv_symbol(decl_kind k) const { + switch (k) { + case OP_ARITH_BAND: return symbol("band"); + case OP_ARITH_SHL: return symbol("shl"); + case OP_ARITH_ASHR: return symbol("ashr"); + case OP_ARITH_LSHR: return symbol("lshr"); + default: + UNREACHABLE(); + } + return symbol(); +} + + func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (k == OP_NUM) @@ -523,10 +536,10 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); } - if (k == OP_ARITH_BAND) { + if (k == OP_ARITH_BAND || k == OP_ARITH_SHL || k == OP_ARITH_ASHR || k == OP_ARITH_LSHR) { if (arity != 2 || domain[0] != m_int_decl || domain[1] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer"); - return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl, + return m_manager->mk_func_decl(bv_symbol(k), 2, domain, m_int_decl, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -554,11 +567,11 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); } - if (k == OP_ARITH_BAND) { + if (k == OP_ARITH_BAND || k == OP_ARITH_SHL || k == OP_ARITH_ASHR || k == OP_ARITH_LSHR) { if (num_args != 2 || args[0]->get_sort() != m_int_decl || args[1]->get_sort() != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer"); sort* domain[2] = { m_int_decl, m_int_decl }; - return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl, + return m_manager->mk_func_decl(bv_symbol(k), 2, domain, m_int_decl, func_decl_info(m_family_id, k, num_parameters, parameters)); } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 25c4977e9..308bc1326 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -72,6 +72,9 @@ enum arith_op_kind { OP_ATANH, // Bit-vector functions OP_ARITH_BAND, + OP_ARITH_SHL, + OP_ARITH_ASHR, + OP_ARITH_LSHR, // constants OP_PI, OP_E, @@ -150,6 +153,8 @@ protected: bool m_convert_int_numerals_to_real; + symbol bv_symbol(decl_kind k) const; + func_decl * mk_func_decl(decl_kind k, bool is_real); void set_manager(ast_manager * m, family_id id) override; decl_kind fix_kind(decl_kind k, unsigned arity); @@ -233,6 +238,14 @@ public: executed in different threads. */ class arith_recognizers { + bool is_arith_op(expr const* n, decl_kind k, unsigned& sz, expr*& x, expr*& y) { + if (!is_app_of(n, arith_family_id, k)) + return false; + x = to_app(n)->get_arg(0); + y = to_app(n)->get_arg(1); + sz = to_app(n)->get_parameter(0).get_int(); + return true; + } public: family_id get_family_id() const { return arith_family_id; } @@ -296,14 +309,13 @@ public: bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); } bool is_band(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); } - bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { - if (!is_band(n)) - return false; - x = to_app(n)->get_arg(0); - y = to_app(n)->get_arg(1); - sz = to_app(n)->get_parameter(0).get_int(); - return true; - } + bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_BAND, sz, x, y); } + bool is_shl(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_SHL); } + bool is_shl(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_SHL, sz, x, y); } + bool is_lshr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_LSHR); } + bool is_lshr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_LSHR, sz, x, y); } + bool is_ashr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_ASHR); } + bool is_ashr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_ASHR, sz, x, y); } bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); } bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); } @@ -487,6 +499,9 @@ public: app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); } app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); } + app* mk_shl(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, 2, args); } + app* mk_ashr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, 2, args); } + app* mk_lshr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, 2, args); } app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); } app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index ddfabed83..d8a06ada6 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -92,6 +92,9 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_COSH: SASSERT(num_args == 1); st = mk_cosh_core(args[0], result); break; case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break; case OP_ARITH_BAND: SASSERT(num_args == 2); st = mk_band_core(f->get_parameter(0).get_int(), args[0], args[1], result); break; + case OP_ARITH_SHL: SASSERT(num_args == 2); st = mk_shl_core(f->get_parameter(0).get_int(), args[0], args[1], result); break; + case OP_ARITH_ASHR: SASSERT(num_args == 2); st = mk_ashr_core(f->get_parameter(0).get_int(), args[0], args[1], result); break; + case OP_ARITH_LSHR: SASSERT(num_args == 2); st = mk_lshr_core(f->get_parameter(0).get_int(), args[0], args[1], result); break; default: st = BR_FAILED; break; } CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m); @@ -1350,6 +1353,98 @@ app* arith_rewriter_core::mk_power(expr* x, rational const& r, sort* s) { return y; } +br_status arith_rewriter::mk_shl_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) { + numeral x, y, N; + bool is_num_x = m_util.is_numeral(arg1, x); + bool is_num_y = m_util.is_numeral(arg2, y); + N = rational::power_of_two(sz); + if (is_num_x) + x = mod(x, N); + if (is_num_y) + y = mod(y, N); + if (is_num_x && is_num_y) { + if (y >= sz) + result = m_util.mk_int(0); + else + result = m_util.mk_int(mod(x * rational::power_of_two(y.get_unsigned()), N)); + return BR_DONE; + } + if (is_num_y) { + if (y >= sz) + result = m_util.mk_int(0); + else + result = m_util.mk_mod(m_util.mk_mul(arg1, m_util.mk_int(rational::power_of_two(y.get_unsigned()))), m_util.mk_int(N)); + return BR_REWRITE1; + } + if (is_num_x && x == 0) { + result = m_util.mk_int(0); + return BR_DONE; + } + return BR_FAILED; +} +br_status arith_rewriter::mk_ashr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) { + numeral x, y, N; + bool is_num_x = m_util.is_numeral(arg1, x); + bool is_num_y = m_util.is_numeral(arg2, y); + N = rational::power_of_two(sz); + if (is_num_x) + x = mod(x, N); + if (is_num_y) + y = mod(y, N); + if (is_num_x && x == 0) { + result = m_util.mk_int(0); + return BR_DONE; + } + if (is_num_x && is_num_y) { + bool signx = x >= N/2; + rational d = div(x, rational::power_of_two(y.get_unsigned())); + SASSERT(y >= 0); + if (signx) { + if (y >= sz) + result = m_util.mk_int(N-1); + else + result = m_util.mk_int(d); + } + else { + if (y >= sz) + result = m_util.mk_int(0); + else + result = m_util.mk_int(mod(d - rational::power_of_two(sz - y.get_unsigned()), N)); + } + return BR_DONE; + } + return BR_FAILED; +} + +br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) { + numeral x, y, N; + bool is_num_x = m_util.is_numeral(arg1, x); + bool is_num_y = m_util.is_numeral(arg2, y); + N = rational::power_of_two(sz); + if (is_num_x) + x = mod(x, N); + if (is_num_y) + y = mod(y, N); + if (is_num_x && x == 0) { + result = m_util.mk_int(0); + return BR_DONE; + } + if (is_num_y && y == 0) { + result = arg1; + return BR_DONE; + } + if (is_num_x && is_num_y) { + if (y >= sz) + result = m_util.mk_int(N-1); + else { + rational d = div(x, rational::power_of_two(y.get_unsigned())); + result = m_util.mk_int(d); + } + return BR_DONE; + } + return BR_FAILED; +} + br_status arith_rewriter::mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) { numeral x, y, N; bool is_num_x = m_util.is_numeral(arg1, x); @@ -1375,6 +1470,14 @@ br_status arith_rewriter::mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr result = m_util.mk_int(r); return BR_DONE; } + if (is_num_x && (x + 1).is_power_of_two()) { + result = m_util.mk_mod(arg2, m_util.mk_int(x + 1)); + return BR_REWRITE1; + } + if (is_num_y && (y + 1).is_power_of_two()) { + result = m_util.mk_mod(arg1, m_util.mk_int(y + 1)); + return BR_REWRITE1; + } return BR_FAILED; } diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 548ab80db..6066c9eb4 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -160,6 +160,9 @@ public: br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result); br_status mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result); + br_status mk_shl_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result); + br_status mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result); + br_status mk_ashr_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result); void mk_div(expr * arg1, expr * arg2, expr_ref & result) { if (mk_div_core(arg1, arg2, result) == BR_FAILED) result = m.mk_app(get_fid(), OP_DIV, arg1, arg2); diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 0eb8b6b37..021501ecd 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -108,7 +108,7 @@ namespace lp_api { unsigned m_gomory_cuts; unsigned m_assume_eqs; unsigned m_branch; - unsigned m_band_axioms; + unsigned m_bv_axioms; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); @@ -129,7 +129,7 @@ namespace lp_api { st.update("arith-gomory-cuts", m_gomory_cuts); st.update("arith-assume-eqs", m_assume_eqs); st.update("arith-branch", m_branch); - st.update("arith-band-axioms", m_band_axioms); + st.update("arith-bv-axioms", m_bv_axioms); } }; diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index f004422a6..ae67783eb 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -205,58 +205,117 @@ namespace arith { add_clause(dgez, neg); } - bool solver::check_band_term(app* n) { + bool solver::check_bv_term(app* n) { unsigned sz; - expr* x, * y; + expr* _x, * _y; if (!ctx.is_relevant(expr2enode(n))) return true; - VERIFY(a.is_band(n, sz, x, y)); expr_ref vx(m), vy(m),vn(m); - if (!get_value(expr2enode(x), vx) || !get_value(expr2enode(y), vy) || !get_value(expr2enode(n), vn)) { + rational valn, valx, valy; + bool is_int; + VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y)); + if (!get_value(expr2enode(_x), vx) || !get_value(expr2enode(_y), vy) || !get_value(expr2enode(n), vn)) { IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n"); found_unsupported(n); return true; } - rational valn, valx, valy; - bool is_int; if (!a.is_numeral(vn, valn, is_int) || !is_int || !a.is_numeral(vx, valx, is_int) || !is_int || !a.is_numeral(vy, valy, is_int) || !is_int) { IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n"); found_unsupported(n); return true; } - // verbose_stream() << "band: " << mk_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n"; rational N = rational::power_of_two(sz); valx = mod(valx, N); valy = mod(valy, N); + expr_ref x(a.mk_mod(_x, a.mk_int(N)), m); + expr_ref y(a.mk_mod(_y, a.mk_int(N)), m); SASSERT(0 <= valn && valn < N); - + // x mod 2^{i + 1} >= 2^i means the i'th bit is 1. auto bitof = [&](expr* x, unsigned i) { expr_ref r(m); r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i))); return mk_literal(r); }; - for (unsigned i = 0; i < sz; ++i) { - bool xb = valx.get_bit(i); - bool yb = valy.get_bit(i); - bool nb = valn.get_bit(i); - if (xb && yb && !nb) - add_clause(~bitof(x, i), ~bitof(y, i), bitof(n, i)); - else if (nb && !xb) - add_clause(~bitof(n, i), bitof(x, i)); - else if (nb && !yb) - add_clause(~bitof(n, i), bitof(y, i)); - else - continue; + + if (a.is_band(n)) { + IF_VERBOSE(2, verbose_stream() << "band: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n"); + for (unsigned i = 0; i < sz; ++i) { + bool xb = valx.get_bit(i); + bool yb = valy.get_bit(i); + bool nb = valn.get_bit(i); + if (xb && yb && !nb) + add_clause(~bitof(x, i), ~bitof(y, i), bitof(n, i)); + else if (nb && !xb) + add_clause(~bitof(n, i), bitof(x, i)); + else if (nb && !yb) + add_clause(~bitof(n, i), bitof(y, i)); + else + continue; + return false; + } + } + if (a.is_shl(n)) { + SASSERT(valy >= 0); + if (valy >= sz || valy == 0) + return true; + unsigned k = valy.get_unsigned(); + sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N))); + if (s().value(eq) == l_true) + return true; + add_clause(~eq_internalize(y, a.mk_int(k)), eq); + IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n"); + return false; + } + if (a.is_lshr(n)) { + SASSERT(valy >= 0); + if (valy >= sz || valy == 0) + return true; + unsigned k = valy.get_unsigned(); + sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k)))); + if (s().value(eq) == l_true) + return true; + add_clause(~eq_internalize(y, a.mk_int(k)), eq); + IF_VERBOSE(2, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n"); + return false; + } + if (a.is_ashr(n)) { + SASSERT(valy >= 0); + if (valy >= sz || valy == 0) + return true; + unsigned k = valy.get_unsigned(); + sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); + sat::literal eq; + expr* xdiv2k; + switch (s().value(signx)) { + case l_true: + // x < 0 & y = k -> n = (x div 2^k - 2^{N-k}) mod 2^N + xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k))); + eq = eq_internalize(n, a.mk_mod(a.mk_add(xdiv2k, a.mk_int(-rational::power_of_two(sz - k))), a.mk_int(N))); + if (s().value(eq) == l_true) + return true; + break; + case l_false: + // x >= 0 & y = k -> n = x div 2^k + xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k))); + eq = eq_internalize(n, xdiv2k); + if (s().value(eq) == l_true) + return true; + break; + case l_undef: + ctx.mark_relevant(signx); + return false; + } + add_clause(~eq_internalize(y, a.mk_int(k)), ~signx, eq); return false; } return true; } - bool solver::check_band_terms() { - for (app* n : m_band_terms) { - if (!check_band_term(n)) { - ++m_stats.m_band_axioms; + bool solver::check_bv_terms() { + for (app* n : m_bv_terms) { + if (!check_bv_term(n)) { + ++m_stats.m_bv_axioms; return false; } } @@ -268,15 +327,43 @@ namespace arith { * x&y <= x * x&y <= y */ - void solver::mk_band_axiom(app* n) { + void solver::mk_bv_axiom(app* n) { unsigned sz; - expr* x, * y; - VERIFY(a.is_band(n, sz, x, y)); + expr* _x, * _y; + VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y)); rational N = rational::power_of_two(sz); - add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); - add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); - add_clause(mk_literal(a.mk_le(n, a.mk_mod(x, a.mk_int(N))))); - add_clause(mk_literal(a.mk_le(n, a.mk_mod(y, a.mk_int(N))))); + expr_ref x(a.mk_mod(_x, a.mk_int(N)), m); + expr_ref y(a.mk_mod(_y, a.mk_int(N)), m); + + if (a.is_band(n)) { + add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); + add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); + add_clause(mk_literal(a.mk_le(n, x))); + add_clause(mk_literal(a.mk_le(n, y))); + } + else if (a.is_shl(n)) { + // y >= sz => n = 0 + // y = 0 => n = x + add_clause(~mk_literal(a.mk_ge(y, a.mk_int(sz))), mk_literal(m.mk_eq(n, a.mk_int(0)))); + add_clause(~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x))); + } + else if (a.is_lshr(n)) { + // y >= sz => n = 0 + // y = 0 => n = x + add_clause(~mk_literal(a.mk_ge(y, a.mk_int(sz))), mk_literal(m.mk_eq(n, a.mk_int(0)))); + add_clause(~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x))); + } + else if (a.is_ashr(n)) { + // y >= sz & x < 2^{sz-1} => n = 0 + // y >= sz & x >= 2^{sz-1} => n = -1 + // y = 0 => n = x + auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); + add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0)))); + add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1)))); + add_clause(~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x))); + } + else + UNREACHABLE(); } void solver::mk_bound_axioms(api_bound& b) { diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index decd49019..ed49092fd 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -252,10 +252,10 @@ namespace arith { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } - else if (a.is_band(n)) { - m_band_terms.push_back(to_app(n)); - mk_band_axiom(to_app(n)); - ctx.push(push_back_vector(m_band_terms)); + else if (a.is_band(n) || a.is_shl(n) || a.is_ashr(n) || a.is_lshr(n)) { + m_bv_terms.push_back(to_app(n)); + ctx.push(push_back_vector(m_bv_terms)); + mk_bv_axiom(to_app(n)); ensure_arg_vars(to_app(n)); } else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) { diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index eff25bc4a..078515184 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1053,7 +1053,7 @@ namespace arith { if (!check_delayed_eqs()) return sat::check_result::CR_CONTINUE; - if (!int_undef && !check_band_terms()) + if (!int_undef && !check_bv_terms()) return sat::check_result::CR_CONTINUE; if (ctx.get_config().m_arith_ignore_int && int_undef) diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 022dbeaea..cbf4206a9 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -214,7 +214,7 @@ namespace arith { expr* m_not_handled = nullptr; ptr_vector m_underspecified; ptr_vector m_idiv_terms; - ptr_vector m_band_terms; + ptr_vector m_bv_terms; vector > m_use_list; // bounds where variables are used. // attributes for incremental version: @@ -318,7 +318,7 @@ namespace arith { void mk_bound_axioms(api_bound& b); void mk_bound_axiom(api_bound& b1, api_bound& b2); void mk_power0_axioms(app* t, app* n); - void mk_band_axiom(app* n); + void mk_bv_axiom(app* n); void flush_bound_axioms(); void add_farkas_clause(sat::literal l1, sat::literal l2); @@ -410,8 +410,8 @@ namespace arith { bool check_delayed_eqs(); lbool check_lia(); lbool check_nla(); - bool check_band_terms(); - bool check_band_term(app* n); + bool check_bv_terms(); + bool check_bv_term(app* n); void add_lemmas(); void propagate_nla(); void add_equality(lpvar v, rational const& k, lp::explanation const& exp); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 9d03d0ad0..fed43e217 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -656,24 +656,58 @@ namespace intblast { break; } case OP_BSHL: { - expr* x = arg(0), * y = umod(e, 1); - r = a.mk_int(0); - for (unsigned i = 0; i < bv.get_bv_size(e); ++i) - r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); + if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) + r = a.mk_shl(bv.get_bv_size(e), arg(0),arg(1)); + else { + expr* x = arg(0), * y = umod(e, 1); + r = a.mk_int(0); + IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); + } break; } case OP_BNOT: r = bnot(arg(0)); break; - case OP_BLSHR: { - expr* x = arg(0), * y = umod(e, 1); - r = a.mk_int(0); - for (unsigned i = 0; i < bv.get_bv_size(e); ++i) - r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); + case OP_BLSHR: + if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) + r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1)); + else { + expr* x = arg(0), * y = umod(e, 1); + r = a.mk_int(0); + IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); + } + break; + case OP_BASHR: + if (!a.is_numeral(arg(1))) + r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1)); + else { + + // + // ashr(x, y) + // if y = k & x >= 0 -> x / 2^k + // if y = k & x < 0 -> (x / 2^k) - 2^{N-k} + // + unsigned sz = bv.get_bv_size(e); + rational N = bv_size(e); + expr* x = umod(e, 0), *y = umod(e, 1); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0)); + IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); + for (unsigned i = 0; i < sz; ++i) { + expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), + m.mk_ite(signx, a.mk_add(d, a.mk_int(- rational::power_of_two(sz-i))), d), + r); + } + } break; - } case OP_BOR: { // p | q := (p + q) - band(p, q) + IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); r = arg(0); for (unsigned i = 1; i < args.size(); ++i) r = a.mk_sub(a.mk_add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i))); @@ -683,12 +717,14 @@ namespace intblast { r = bnot(band(args)); break; case OP_BAND: + IF_VERBOSE(2, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); r = band(args); break; case OP_BXNOR: case OP_BXOR: { // p ^ q := (p + q) - 2*band(p, q); unsigned sz = bv.get_bv_size(e); + IF_VERBOSE(2, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n"); r = arg(0); for (unsigned i = 1; i < args.size(); ++i) { expr* q = arg(i); @@ -698,25 +734,6 @@ namespace intblast { r = bnot(r); break; } - case OP_BASHR: { - // - // ashr(x, y) - // if y = k & x >= 0 -> x / 2^k - // if y = k & x < 0 -> (x / 2^k) - 1 + 2^{N-k} - // - unsigned sz = bv.get_bv_size(e); - rational N = bv_size(e); - expr* x = umod(e, 0), *y = umod(e, 1); - expr* signx = a.mk_ge(x, a.mk_int(N / 2)); - r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0)); - for (unsigned i = 0; i < sz; ++i) { - expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); - r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), - m.mk_ite(signx, a.mk_add(d, a.mk_int(- rational::power_of_two(sz-i))), d), - r); - } - break; - } case OP_ZERO_EXT: bv_expr = e->get_arg(0); r = umod(bv_expr, 0); From 4867073290378ec4a31eb06b4df507c815a12473 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Dec 2023 10:04:49 -0800 Subject: [PATCH 31/33] remove windowsArm64 from nightly Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 45 ------------------------ src/ast/rewriter/arith_rewriter.cpp | 2 +- src/sat/smt/arith_axioms.cpp | 17 +++++++-- src/sat/smt/euf_model.cpp | 2 +- src/sat/smt/intblast_solver.cpp | 53 +++++++++++++++-------------- src/sat/smt/intblast_solver.h | 2 ++ 6 files changed, 47 insertions(+), 74 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 0f5337654..5c1bdff6a 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -233,46 +233,6 @@ stages: symbolServerType: TeamServices detailedLog: true - - job: "WindowsArm64" - displayName: "WindowsArm64" - pool: - vmImage: "windows-latest" - variables: - arch: "amd64_arm64" - bindings: "-DCMAKE_BUILD_TYPE=RelWithDebInfo" - steps: - - script: md build - - script: | - cd build - call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch) - cmake $(bindings) -G "NMake Makefiles" ../ - nmake - cd .. - - task: CopyFiles@2 - inputs: - sourceFolder: build - contents: '*z3*.*' - targetFolder: $(Build.ArtifactStagingDirectory) - - task: PublishPipelineArtifact@1 - inputs: - targetPath: $(Build.ArtifactStagingDirectory) - artifactName: 'WindowsArm64' - - task: CopyFiles@2 - displayName: 'Collect Symbols' - inputs: - sourceFolder: build - contents: '**/*.pdb' - targetFolder: '$(Build.ArtifactStagingDirectory)/symbols' - # Publish symbol archive to match nuget package - # Index your source code and publish symbols to a file share or Azure Artifacts symbol server - - task: PublishSymbols@2 - inputs: - symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols' - searchPattern: '**/*.pdb' - indexSources: false # Github not supported - publishSymbols: true - symbolServerType: TeamServices - detailedLog: true - stage: Package @@ -576,11 +536,6 @@ stages: inputs: artifactName: 'Windows32' targetPath: tmp - - task: DownloadPipelineArtifact@2 - displayName: "Download windowsArm64" - inputs: - artifactName: 'WindowsArm64' - targetPath: tmp - task: DownloadPipelineArtifact@2 displayName: "Download windows64" inputs: diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d8a06ada6..13e50da4a 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1435,7 +1435,7 @@ br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr } if (is_num_x && is_num_y) { if (y >= sz) - result = m_util.mk_int(N-1); + result = m_util.mk_int(0); else { rational d = div(x, rational::power_of_two(y.get_unsigned())); result = m_util.mk_int(d); diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index ae67783eb..20bc78260 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -260,6 +260,9 @@ namespace arith { if (valy >= sz || valy == 0) return true; unsigned k = valy.get_unsigned(); + rational r = mod(valx * rational::power_of_two(k), N); + if (r == valn) + return true; sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N))); if (s().value(eq) == l_true) return true; @@ -272,6 +275,9 @@ namespace arith { if (valy >= sz || valy == 0) return true; unsigned k = valy.get_unsigned(); + rational r = mod(div(valx, rational::power_of_two(k)), N); + if (r == valn) + return true; sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k)))); if (s().value(eq) == l_true) return true; @@ -284,6 +290,12 @@ namespace arith { if (valy >= sz || valy == 0) return true; unsigned k = valy.get_unsigned(); + bool signvalx = x >= N/2; + rational valxdiv2k = div(valx, rational::power_of_two(k)); + if (signvalx) + valxdiv2k = mod(valxdiv2k - rational::power_of_two(sz - k), N); + if (valn == valxdiv2k) + return true; sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); sat::literal eq; expr* xdiv2k; @@ -335,9 +347,10 @@ namespace arith { expr_ref x(a.mk_mod(_x, a.mk_int(N)), m); expr_ref y(a.mk_mod(_y, a.mk_int(N)), m); + add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); + add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); + if (a.is_band(n)) { - add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); - add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); add_clause(mk_literal(a.mk_le(n, x))); add_clause(mk_literal(a.mk_le(n, y))); } diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 073d164be..2035e16b6 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -282,7 +282,7 @@ namespace euf { } void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) { - out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n"; + out << "Failed to validate b" << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n"; s().display(out); euf::enode_vector nodes; nodes.push_back(n); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index fed43e217..55ab4846c 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -148,7 +148,7 @@ namespace intblast { auto a = expr2literal(e); auto b = mk_literal(r); ctx.mark_relevant(b); -// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; + // verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; add_equiv(a, b); } return true; @@ -305,28 +305,6 @@ namespace intblast { sorted.push_back(arg); } } - - // - // Add ground equalities to ensure the model is valid with respect to the current case splits. - // This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal - // assignment from complete level. - // E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment. - // If intblast is SAT, then force the model and literal assignment on the rest of the literals. - // - if (!is_ground(e)) - continue; - euf::enode* n = ctx.get_enode(e); - if (!n) - continue; - if (n == n->get_root()) - continue; - expr* r = n->get_root()->get_expr(); - es.push_back(m.mk_eq(e, r)); - r = es.back(); - if (!visited.is_marked(r) && !is_translated(r)) { - visited.mark(r); - sorted.push_back(r); - } } else if (is_quantifier(e)) { quantifier* q = to_quantifier(e); @@ -646,7 +624,7 @@ namespace intblast { } case OP_BUDIV: case OP_BUDIV_I: { - expr* x = arg(0), * y = umod(e, 1); + expr* x = umod(e, 0), * y = umod(e, 1); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y)); break; } @@ -978,13 +956,38 @@ namespace intblast { arith::arith_value av(ctx); rational r; VERIFY(av.get_value(b2i->get_expr(), r)); - verbose_stream() << ctx.bpp(n) << " := " << r << "\n"; value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr())); + verbose_stream() << ctx.bpp(n) << " := " << value << "\n"; } values.set(n->get_root_id(), value); TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); } + void solver::finalize_model(model& mdl) { + for (auto n : ctx.get_egraph().nodes()) { + expr* e = n->get_expr(); + if (!bv.is_bv(e)) + continue; + if (!is_translated(e)) + continue; + expr* f = translated(e); + rational r1, r2; + expr_ref val1 = mdl(e); + expr_ref val2 = mdl(f); + if (bv.is_numeral(val1, r1) && a.is_numeral(val2, r2) && r1 != r2) { + rational N = rational::power_of_two(bv.get_bv_size(e)); + r2 = mod(r2, N); + if (r1 == r2) + continue; + verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n"; + verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n"; + for (expr* arg : *to_app(e)) { + verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n"; + } + } + } + } + sat::literal_vector const& solver::unsat_core() { return m_core; } diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h index d59dac935..1739fc09b 100644 --- a/src/sat/smt/intblast_solver.h +++ b/src/sat/smt/intblast_solver.h @@ -108,6 +108,8 @@ namespace intblast { bool add_dep(euf::enode* n, top_sort& dep) override; + void finalize_model(model& mdl) override; + std::ostream& display(std::ostream& out) const override; void collect_statistics(statistics& st) const override; From bb99f442147bf87cc2cd437e6edfdf2ae7e9a068 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Dec 2023 17:42:55 -0800 Subject: [PATCH 32/33] fix bugs in elim-unconstr2 and fix bugs in intblast_solver Signed-off-by: Nikolaj Bjorner --- src/ast/converters/expr_inverter.cpp | 1 + src/ast/simplifiers/elim_unconstrained.cpp | 26 +++++- .../model_reconstruction_trail.cpp | 4 +- src/sat/smt/intblast_solver.cpp | 92 +++++++++---------- 4 files changed, 70 insertions(+), 53 deletions(-) diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp index bdc32e97c..a06d125a5 100644 --- a/src/ast/converters/expr_inverter.cpp +++ b/src/ast/converters/expr_inverter.cpp @@ -400,6 +400,7 @@ class bv_expr_inverter : public iexpr_inverter { } bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) { +// return false; if (num == 0) return false; if (!uncnstr(num, args)) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 231858897..c7cf2d11c 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -66,7 +66,6 @@ bool elim_unconstrained::is_var_lt(int v1, int v2) const { } void elim_unconstrained::eliminate() { - while (!m_heap.empty()) { expr_ref r(m); int v = m_heap.erase_min(); @@ -86,7 +85,12 @@ void elim_unconstrained::eliminate() { n.m_refcount = 0; continue; } + if (m_heap.contains(root(e))) { + IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n"); + continue; + } app* t = to_app(e); + TRACE("elim_unconstrained", tout << "eliminating " << mk_pp(t, m) << "\n";); unsigned sz = m_args.size(); for (expr* arg : *to_app(t)) m_args.push_back(reconstruct_term(get_node(arg))); @@ -99,12 +103,15 @@ void elim_unconstrained::eliminate() { proof * pr = m.mk_apply_def(s, r, pr1); m_trail.push_back(pr); } + expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m); n.m_refcount = 0; m_args.shrink(sz); if (!inverted) { IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n"); continue; } + + IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n"); TRACE("elim_unconstrained", tout << mk_pp(t, m) << " -> " << r << "\n"); SASSERT(r->get_sort() == t->get_sort()); @@ -119,7 +126,8 @@ void elim_unconstrained::eliminate() { get_node(e).m_term = r; get_node(e).m_proof = pr; get_node(e).m_refcount++; - IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n"); + get_node(e).m_dirty = false; + IF_VERBOSE(11, verbose_stream() << "set " << &get_node(e) << " " << root(e) << " " << mk_bounded_pp(e, m) << " := " << mk_bounded_pp(r, m) << "\n"); SASSERT(!m_heap.contains(root(e))); if (is_uninterp_const(r)) m_heap.insert(root(e)); @@ -283,13 +291,22 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) { expr* t = n0.m_term; if (!n0.m_dirty) return expr_ref(t, m); + if (!is_node(t)) + return expr_ref(t, m); ptr_vector todo; todo.push_back(t); while (!todo.empty()) { t = todo.back(); + if (!is_node(t)) { + UNREACHABLE(); + } node& n = get_node(t); unsigned sz0 = todo.size(); - if (is_app(t)) { + if (is_app(t)) { + if (n.m_term != t) { + todo.pop_back(); + continue; + } for (expr* arg : *to_app(t)) if (get_node(arg).m_dirty || !get_node(arg).m_term) todo.push_back(arg); @@ -300,7 +317,6 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) { for (expr* arg : *to_app(t)) m_args.push_back(get_node(arg).m_term); n.m_term = m.mk_app(to_app(t)->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz); - m_args.shrink(sz); } else if (is_quantifier(t)) { @@ -410,7 +426,7 @@ void elim_unconstrained::reduce() { generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained"); m_inverter.set_model_converter(mc.get()); m_created_compound = true; - for (unsigned rounds = 0; m_created_compound && rounds < 3; ++rounds) { + for (unsigned rounds = 0; m_created_compound && rounds < 1; ++rounds) { m_created_compound = false; init_nodes(); eliminate(); diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 95f73fd7a..47ebea525 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -182,11 +182,11 @@ std::ostream& model_reconstruction_trail::display(std::ostream& out) const { out << "hide " << t->m_decl->get_name() << "\n"; else if (t->is_def()) { for (auto const& [f, def, dep] : t->m_defs) - out << f->get_name() << " <- " << mk_pp(def, m) << "\n"; + out << "def: " << f->get_name() << " <- " << mk_pp(def, m) << "\n"; } else { for (auto const& [v, def] : t->m_subst->sub()) - out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n"; + out << "sub: " << mk_pp(v, m) << " -> " << mk_pp(def, m) << "\n"; } for (auto const& d : t->m_removed) out << "rm: " << d << "\n"; diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 55ab4846c..d0ecff794 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -104,10 +104,10 @@ namespace intblast { ctx.push(push_back_vector(m_preds)); } - void solver::set_translated(expr* e, expr* r) { + void solver::set_translated(expr* e, expr* r) { SASSERT(r); - SASSERT(!is_translated(e)); - m_translate.setx(e->get_id(), r); + SASSERT(!is_translated(e)); + m_translate.setx(e->get_id(), r); ctx.push(set_vector_idx_trail(m_translate, e->get_id())); } @@ -157,7 +157,7 @@ namespace intblast { bool solver::unit_propagate() { return add_bound_axioms() || add_predicate_axioms(); } - + void solver::ensure_translated(expr* e) { if (m_translate.get(e->get_id(), nullptr)) return; @@ -179,7 +179,7 @@ namespace intblast { } } std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); - for (expr* e : todo) + for (expr* e : todo) translate_expr(e); } @@ -335,7 +335,7 @@ namespace intblast { es[i] = translated(es.get(i)); } - sat::check_result solver::check() { + sat::check_result solver::check() { // ensure that bv2int is injective for (auto e : m_bv2int) { euf::enode* n = expr2enode(e); @@ -347,10 +347,12 @@ namespace intblast { continue; if (sib->get_arg(0)->get_root() == r1) continue; - auto a = eq_internalize(n, sib); - auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); - ctx.mark_relevant(a); - ctx.mark_relevant(b); + if (sib->get_arg(0)->get_sort() != n->get_arg(0)->get_sort()) + continue; + auto a = eq_internalize(n, sib); + auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); + ctx.mark_relevant(a); + ctx.mark_relevant(b); add_clause(~a, b, nullptr); return sat::check_result::CR_CONTINUE; } @@ -368,13 +370,13 @@ namespace intblast { auto nBv2int = ctx.get_enode(bv2int); auto nxModN = ctx.get_enode(xModN); if (nBv2int->get_root() != nxModN->get_root()) { - auto a = eq_internalize(nBv2int, nxModN); - ctx.mark_relevant(a); + auto a = eq_internalize(nBv2int, nxModN); + ctx.mark_relevant(a); add_unit(a); return sat::check_result::CR_CONTINUE; } } - return sat::check_result::CR_DONE; + return sat::check_result::CR_DONE; } expr* solver::umod(expr* bv_expr, unsigned i) { @@ -482,8 +484,8 @@ namespace intblast { m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i)); if (has_bv_sort) - m_vars.push_back(e); - + m_vars.push_back(e); + if (m_is_plugin) { expr* r = m.mk_app(f, m_args); if (has_bv_sort) { @@ -504,7 +506,7 @@ namespace intblast { f = g; m_pinned.push_back(f); } - set_translated(e, m.mk_app(f, m_args)); + set_translated(e, m.mk_app(f, m_args)); } void solver::translate_bv(app* e) { @@ -536,7 +538,7 @@ namespace intblast { r = a.mk_add(hi, lo); } return r; - }; + }; expr* bv_expr = e; expr* r = nullptr; @@ -634,22 +636,22 @@ namespace intblast { break; } case OP_BSHL: { - if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) - r = a.mk_shl(bv.get_bv_size(e), arg(0),arg(1)); + if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) + r = a.mk_shl(bv.get_bv_size(e), arg(0), arg(1)); else { expr* x = arg(0), * y = umod(e, 1); r = a.mk_int(0); IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < bv.get_bv_size(e); ++i) - r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); } break; } case OP_BNOT: r = bnot(arg(0)); break; - case OP_BLSHR: - if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) + case OP_BLSHR: + if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1)); else { expr* x = arg(0), * y = umod(e, 1); @@ -659,11 +661,11 @@ namespace intblast { r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); } break; - case OP_BASHR: + case OP_BASHR: if (!a.is_numeral(arg(1))) r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1)); else { - + // // ashr(x, y) // if y = k & x >= 0 -> x / 2^k @@ -671,15 +673,15 @@ namespace intblast { // unsigned sz = bv.get_bv_size(e); rational N = bv_size(e); - expr* x = umod(e, 0), *y = umod(e, 1); + expr* x = umod(e, 0), * y = umod(e, 1); expr* signx = a.mk_ge(x, a.mk_int(N / 2)); - r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0)); + r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0)); IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < sz; ++i) { - expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); + expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), - m.mk_ite(signx, a.mk_add(d, a.mk_int(- rational::power_of_two(sz-i))), d), - r); + m.mk_ite(signx, a.mk_add(d, a.mk_int(-rational::power_of_two(sz - i))), d), + r); } } break; @@ -744,11 +746,11 @@ namespace intblast { r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0)); break; case OP_BSMOD_I: - case OP_BSMOD: { - expr* x = umod(e, 0), *y = umod(e, 1); - rational N = bv_size(e); - expr* signx = a.mk_ge(x, a.mk_int(N/2)); - expr* signy = a.mk_ge(y, a.mk_int(N/2)); + case OP_BSMOD: { + expr* x = umod(e, 0), * y = umod(e, 1); + rational N = bv_size(e); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + expr* signy = a.mk_ge(y, a.mk_int(N / 2)); expr* u = a.mk_mod(x, y); // u = 0 -> 0 // y = 0 -> x @@ -756,14 +758,14 @@ namespace intblast { // x < 0, y >= 0 -> y - u // x >= 0, y < 0 -> y + u // x >= 0, y >= 0 -> u - r = a.mk_uminus(u); + r = a.mk_uminus(u); r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), a.mk_add(u, y), r); r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r); r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r); r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); break; - } + } case OP_BSDIV_I: case OP_BSDIV: { // d = udiv(abs(x), abs(y)) @@ -799,7 +801,7 @@ namespace intblast { d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); r = a.mk_sub(x, a.mk_mul(d, y)); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); - break; + break; } case OP_ROTATE_LEFT: { auto n = e->get_parameter(0).get_int(); @@ -812,11 +814,11 @@ namespace intblast { r = rotate_left(sz - n); break; } - case OP_EXT_ROTATE_LEFT: { + case OP_EXT_ROTATE_LEFT: { unsigned sz = bv.get_bv_size(e); expr* y = umod(e, 1); r = a.mk_int(0); - for (unsigned i = 0; i < sz; ++i) + for (unsigned i = 0; i < sz; ++i) r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r); break; } @@ -824,7 +826,7 @@ namespace intblast { unsigned sz = bv.get_bv_size(e); expr* y = umod(e, 1); r = a.mk_int(0); - for (unsigned i = 0; i < sz; ++i) + for (unsigned i = 0; i < sz; ++i) r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r); break; } @@ -837,7 +839,7 @@ namespace intblast { for (unsigned i = 1; i < n; ++i) r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0; break; - } + } case OP_BREDOR: { r = umod(e->get_arg(0), 0); r = m.mk_not(m.mk_eq(r, a.mk_int(0))); @@ -897,7 +899,7 @@ namespace intblast { } bool solver::add_dep(euf::enode* n, top_sort& dep) { - if (!is_app(n->get_expr())) + if (!is_app(n->get_expr())) return false; app* e = to_app(n->get_expr()); if (n->num_args() == 0) { @@ -916,7 +918,7 @@ namespace intblast { void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) { expr* e = n->get_expr(); SASSERT(bv.is_bv(e)); - + if (bv.is_numeral(e)) { values.setx(n->get_root_id(), e); return; @@ -957,7 +959,6 @@ namespace intblast { rational r; VERIFY(av.get_value(b2i->get_expr(), r)); value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr())); - verbose_stream() << ctx.bpp(n) << " := " << value << "\n"; } values.set(n->get_root_id(), value); TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); @@ -981,9 +982,8 @@ namespace intblast { continue; verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n"; verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n"; - for (expr* arg : *to_app(e)) { + for (expr* arg : *to_app(e)) verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n"; - } } } } From 2f2bf749b9d3fb71f2ae49ffaafde5b6e370f96c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Dec 2023 18:15:51 -0800 Subject: [PATCH 33/33] fixes to intblast encoding and more arithmetic rewriters Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 52 ++++++++++++++++++++++------- src/ast/rewriter/arith_rewriter.h | 1 + src/sat/smt/intblast_solver.cpp | 10 +++--- 3 files changed, 46 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 13e50da4a..635d5a3f2 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1232,19 +1232,20 @@ static rational symmod(rational const& a, rational const& b) { br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(arg1->get_sort()); - numeral v1, v2; - bool is_int; - if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { - result = m_util.mk_numeral(mod(v1, v2), is_int); + numeral x, y; + bool is_num_x = m_util.is_numeral(arg1, x); + bool is_num_y = m_util.is_numeral(arg2, y); + if (is_num_x && is_num_y && !y.is_zero()) { + result = m_util.mk_int(mod(x, y)); return BR_DONE; } - if (m_util.is_numeral(arg2, v2, is_int) && is_int && (v2.is_one() || v2.is_minus_one())) { + if (is_num_y && y.is_int() && (y.is_one() || y.is_minus_one())) { result = m_util.mk_numeral(numeral(0), true); return BR_DONE; } - if (arg1 == arg2 && !m_util.is_numeral(arg2)) { + if (arg1 == arg2 && !is_num_y) { expr_ref zero(m_util.mk_int(0), m); result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero); return BR_DONE; @@ -1252,29 +1253,35 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul // mod is idempotent on non-zero modulus. expr* t1, *t2; - if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) { + if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && is_num_y && y.is_int() && !y.is_zero()) { + result = arg1; + return BR_DONE; + } + + rational lo, hi; + if (is_num_y && get_range(arg1, lo, hi) && 0 <= lo && hi < y) { result = arg1; return BR_DONE; } // propagate mod inside only if there is something to reduce. - if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { + if (is_num_y && y.is_int() && y.is_pos() && (is_add(arg1) || is_mul(arg1))) { TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n";); expr_ref_buffer args(m); bool change = false; for (expr* arg : *to_app(arg1)) { rational arg_v; - if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) != arg_v) { + if (m_util.is_numeral(arg, arg_v) && mod(arg_v, y) != arg_v) { change = true; - args.push_back(m_util.mk_numeral(mod(arg_v, v2), true)); + args.push_back(m_util.mk_numeral(mod(arg_v, y), true)); } else if (m_util.is_mod(arg, t1, t2) && t2 == arg2) { change = true; args.push_back(t1); } - else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, v2) != arg_v) { + else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, y) != arg_v) { change = true; - args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, v2), true), t2)); + args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, y), true), t2)); } else { args.push_back(arg); @@ -1291,6 +1298,27 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul return BR_FAILED; } +bool arith_rewriter::get_range(expr* e, rational& lo, rational& hi) { + expr* x, *y; + rational r; + if (m_util.is_idiv(e, x, y) && m_util.is_numeral(y, r) && get_range(x, lo, hi) && 0 <= lo && r > 0) { + lo = div(lo, r); + hi = div(hi, r); + return true; + } + if (m_util.is_mod(e, x, y) && m_util.is_numeral(y, r) && r > 0) { + lo = 0; + hi = r - 1; + return true; + } + if (m_util.is_numeral(e, r)) { + lo = hi = r; + return true; + } + return false; +} + + br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(arg1->get_sort()); numeral v1, v2; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 6066c9eb4..a9a30fe00 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -63,6 +63,7 @@ class arith_rewriter : public poly_rewriter { bool m_eq2ineq; unsigned m_max_degree; + bool get_range(expr* e, rational& lo, rational& hi); void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts); enum const_treatment { CT_FLOOR, CT_CEIL, CT_FALSE }; bool div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index d0ecff794..d1b3a7205 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -37,7 +37,6 @@ namespace intblast { euf::theory_var solver::mk_var(euf::enode* n) { auto r = euf::th_euf_solver::mk_var(n); ctx.attach_th_var(n, this, r); - TRACE("bv", tout << "mk-var: v" << r << " " << ctx.bpp(n) << "\n";); return r; } @@ -98,7 +97,7 @@ namespace intblast { ensure_translated(y); m_args.reset(); m_args.push_back(a.mk_sub(translated(x), translated(y))); - set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); + set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); } m_preds.push_back(e); ctx.push(push_back_vector(m_preds)); @@ -148,7 +147,7 @@ namespace intblast { auto a = expr2literal(e); auto b = mk_literal(r); ctx.mark_relevant(b); - // verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; + TRACE("intblast", tout << "add-predicate-axiom: " << mk_bounded_pp(e, m) << " \n" << r << "\n"); add_equiv(a, b); } return true; @@ -606,9 +605,10 @@ namespace intblast { unsigned lo, hi; expr* old_arg; VERIFY(bv.is_extract(e, lo, hi, old_arg)); - r = arg(0); if (lo > 0) - r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo))); + r = a.mk_idiv(umod(old_arg, 0), a.mk_int(rational::power_of_two(lo))); + else + r = arg(0); break; } case OP_BV_NUM: {