From cfa6bd45347ca9b9047dae718e0ca4c91525e9af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Feb 2024 20:33:06 -0800 Subject: [PATCH] update python build dependencies Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/ast/sls/bv_sls_eval.cpp | 6 +++--- src/ast/sls/sls_valuation.cpp | 8 ++++---- src/ast/sls/sls_valuation.h | 4 ++-- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index d91feea9f..2805cbaf1 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -59,7 +59,7 @@ def init_project_def(): add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'solver_assertions', 'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp']) - add_lib('sat_smt', ['sat', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt') + add_lib('sat_smt', ['sat', 'ast_sls', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt') add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv') diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 0e2ecc768..2331572e4 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -983,6 +983,7 @@ namespace bv { bool sls_eval::try_repair_bxor(bvval const& e, bvval& a, bvval const& b) { for (unsigned i = 0; i < e.nw; ++i) m_tmp[i] = e.bits[i] ^ b.bits[i]; + a.clear_overflow_bits(m_tmp); a.set_repair(random_bool(), m_tmp); return true; } @@ -1517,15 +1518,14 @@ namespace bv { for (unsigned i = 0; i < a.bw; ++i) a.set(m_tmp, i, e.get(e.bits, i + b.bw)); a.clear_overflow_bits(m_tmp); - a.set_repair(random_bool(), m_tmp); + return a.set_repair(random_bool(), m_tmp); } else { for (unsigned i = 0; i < b.bw; ++i) b.set(m_tmp, i, e.get(e.bits, i)); b.clear_overflow_bits(m_tmp); - b.set_repair(random_bool(), m_tmp); + return b.set_repair(random_bool(), m_tmp); } - return true; } bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) { diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 21e44b3fe..15e0aa79a 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -24,7 +24,6 @@ namespace bv { sls_valuation::sls_valuation(unsigned bw): bw(bw) { nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t)); - unsigned num_bytes = nw * sizeof(digit_t); lo.reserve(nw + 1); hi.reserve(nw + 1); bits.reserve(nw + 1); @@ -192,14 +191,17 @@ namespace bv { return true; } - void sls_valuation::set_repair(bool try_down, svector& dst) { + bool sls_valuation::set_repair(bool try_down, svector& dst) { for (unsigned i = 0; i < nw; ++i) dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & bits[i]); bool ok = try_down ? round_down(dst) : round_up(dst); if (!ok) VERIFY(try_down ? round_up(dst) : round_down(dst)); + if (eq(bits, dst)) + return false; set(bits, dst); SASSERT(!has_overflow(dst)); + return true; } void sls_valuation::min_feasible(svector& out) const { @@ -294,8 +296,6 @@ namespace bv { void sls_valuation::shift_right(svector& out, unsigned shift) const { SASSERT(shift < bw); - unsigned n = shift / (8 * sizeof(digit_t)); - unsigned s = shift % (8 * sizeof(digit_t)); for (unsigned i = 0; i < bw; ++i) set(out, i, i + shift < bw ? get(bits, i + shift) : false); SASSERT(!has_overflow(out)); diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 0a020c290..95cb2e894 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -66,7 +66,7 @@ namespace bv { bool is_ones(svector const& a) const { auto bound = bw % (sizeof(digit_t) * 8) == 0 ? nw : nw - 1; for (unsigned i = 0; i < bound; ++i) - if (a[i] != ~0) + if (a[i] != (a[i] ^ 0)) return false; if (bound < nw) { for (unsigned i = bound * sizeof(digit_t) * 8; i < bw; ++i) @@ -116,7 +116,7 @@ namespace bv { bool get_at_least(svector const& src, svector& dst) const; bool round_up(svector& dst) const; bool round_down(svector& dst) const; - void set_repair(bool try_down, svector& dst); + bool set_repair(bool try_down, svector& dst); bool try_set(svector const& src) { if (!can_set(src))