mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 06:43:40 +00:00
Code Activity

Refactor bv_sls files to sls_bv with namespace and class name adjustments

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-08-30 17:41:50 -07:00
parent 27702ba09c
commit 6b66e81897
16 changed files with 226 additions and 202 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -1709,7 +1709,7 @@ ast * ast_manager::register_node_core(ast * n) {
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
// track_id(*this, n, 77); // track_id(*this, n, 9213);
// TRACE("ast", tout << (s_count++) << " Object " << n->m_id << " was created.\n";); // TRACE("ast", tout << (s_count++) << " Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);

2
src/ast/rewriter/bv_rewriter.h
View file

@ -222,7 +222,7 @@ public:
#define MK_BV_BINARY(OP) \ #define MK_BV_BINARY(OP) \
expr_ref OP(expr* a, expr* b) { \ expr_ref OP(expr* a, expr* b) { \
expr_ref result(m); \ expr_ref result(m), _a(a, m), _b(b, m); \
if (BR_FAILED == OP(a, b, result)) \ if (BR_FAILED == OP(a, b, result)) \
result = m_util.OP(a, b); \ result = m_util.OP(a, b); \
return result; \ return result; \

8
src/ast/sls/CMakeLists.txt
View file

@ -1,19 +1,19 @@
z3_add_component(ast_sls z3_add_component(ast_sls
SOURCES SOURCES
bvsls_opt_engine.cpp bvsls_opt_engine.cpp
bv_sls_eval.cpp
bv_sls_fixed.cpp
bv_sls_terms.cpp
sat_ddfw.cpp sat_ddfw.cpp
sls_arith_base.cpp sls_arith_base.cpp
sls_arith_plugin.cpp sls_arith_plugin.cpp
sls_basic_plugin.cpp sls_basic_plugin.cpp
sls_bv_eval.cpp
sls_bv_fixed.cpp
sls_bv_plugin.cpp sls_bv_plugin.cpp
sls_bv_terms.cpp
sls_bv_valuation.cpp
sls_context.cpp sls_context.cpp
sls_engine.cpp sls_engine.cpp
sls_euf_plugin.cpp sls_euf_plugin.cpp
sls_smt_solver.cpp sls_smt_solver.cpp
sls_valuation.cpp
COMPONENT_DEPENDENCIES COMPONENT_DEPENDENCIES
ast ast
converters converters

174
src/ast/sls/sls_bv_eval.cpp
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Microsoft Corporation
Module Name: Module Name:
bv_sls_eval.cpp sls_bv_eval.cpp
Author: Author:
@ -13,12 +13,12 @@ Author:
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/sls/bv_sls_eval.h" #include "ast/sls/sls_bv_eval.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
namespace bv { namespace sls {
sls_eval::sls_eval(sls_terms& terms, sls::context& ctx): bv_eval::bv_eval(sls::bv_terms& terms, sls::context& ctx):
m(ctx.get_manager()), m(ctx.get_manager()),
ctx(ctx), ctx(ctx),
terms(terms), terms(terms),
@ -27,7 +27,7 @@ namespace bv {
{} {}
void sls_eval::register_term(expr* e) { void bv_eval::register_term(expr* e) {
if (!is_app(e)) if (!is_app(e))
return; return;
app* a = to_app(e); app* a = to_app(e);
@ -46,7 +46,7 @@ namespace bv {
} }
} }
void sls_eval::add_bit_vector(app* e) { void bv_eval::add_bit_vector(app* e) {
if (!bv.is_bv(e)) if (!bv.is_bv(e))
return; return;
m_values.reserve(e->get_id() + 1); m_values.reserve(e->get_id() + 1);
@ -64,9 +64,9 @@ namespace bv {
return; return;
} }
sls_valuation* sls_eval::alloc_valuation(app* e) { sls::bv_valuation* bv_eval::alloc_valuation(app* e) {
auto bit_width = bv.get_bv_size(e); auto bit_width = bv.get_bv_size(e);
auto* r = alloc(sls_valuation, bit_width); auto* r = alloc(sls::bv_valuation, bit_width);
while (m_tmp.size() < 2 * r->nw) { while (m_tmp.size() < 2 * r->nw) {
m_tmp.push_back(0); m_tmp.push_back(0);
m_tmp2.push_back(0); m_tmp2.push_back(0);
@ -87,12 +87,12 @@ namespace bv {
} }
void sls_eval::init_eval_bv(app* e) { void bv_eval::init_eval_bv(app* e) {
if (bv.is_bv(e)) if (bv.is_bv(e))
eval(e).commit_eval(); eval(e).commit_eval();
} }
bool sls_eval::can_eval1(app* e) const { bool bv_eval::can_eval1(app* e) const {
expr* x, * y; expr* x, * y;
if (m.is_eq(e, x, y)) if (m.is_eq(e, x, y))
return bv.is_bv(x); return bv.is_bv(x);
@ -116,7 +116,7 @@ namespace bv {
return false; return false;
} }
bool sls_eval::bval1_bv(app* e) const { bool bv_eval::bval1_bv(app* e) const {
SASSERT(m.is_bool(e)); SASSERT(m.is_bool(e));
SASSERT(e->get_family_id() == bv.get_fid()); SASSERT(e->get_family_id() == bv.get_fid());
@ -191,7 +191,7 @@ namespace bv {
return false; return false;
} }
bool sls_eval::bval1(app* e) const { bool bv_eval::bval1(app* e) const {
if (e->get_family_id() == bv.get_fid()) if (e->get_family_id() == bv.get_fid())
return bval1_bv(e); return bval1_bv(e);
expr* x, * y; expr* x, * y;
@ -203,17 +203,17 @@ namespace bv {
return false; return false;
} }
sls_valuation& sls_eval::eval(app* e) const { sls::bv_valuation& bv_eval::eval(app* e) const {
auto& val = *m_values[e->get_id()]; auto& val = *m_values[e->get_id()];
eval(e, val); eval(e, val);
return val; return val;
} }
void sls_eval::set(expr* e, sls_valuation const& val) { void bv_eval::set(expr* e, sls::bv_valuation const& val) {
m_values[e->get_id()]->set(val.bits()); m_values[e->get_id()]->set(val.bits());
} }
void sls_eval::eval(app* e, sls_valuation& val) const { void bv_eval::eval(app* e, sls::bv_valuation& val) const {
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
if (m.is_ite(e)) { if (m.is_ite(e)) {
SASSERT(bv.is_bv(e->get_arg(1))); SASSERT(bv.is_bv(e->get_arg(1)));
@ -630,12 +630,12 @@ namespace bv {
val.clear_overflow_bits(val.eval); val.clear_overflow_bits(val.eval);
} }
digit_t sls_eval::random_bits() { digit_t bv_eval::random_bits() {
return sls_valuation::random_bits(m_rand); return sls::bv_valuation::random_bits(m_rand);
} }
bool sls_eval::is_uninterpreted(app* e) const { bool bv_eval::is_uninterpreted(app* e) const {
if (is_uninterp(e)) if (is_uninterp(e))
return true; return true;
if (e->get_family_id() != bv.get_family_id()) if (e->get_family_id() != bv.get_family_id())
@ -656,7 +656,7 @@ namespace bv {
} }
} }
bool sls_eval::repair_down(app* e, unsigned i) { bool bv_eval::repair_down(app* e, unsigned i) {
expr* arg = e->get_arg(i); expr* arg = e->get_arg(i);
if (m.is_value(arg)) if (m.is_value(arg))
return false; return false;
@ -673,7 +673,7 @@ namespace bv {
return false; return false;
} }
bool sls_eval::try_repair_bv(app* e, unsigned i) { bool bv_eval::try_repair_bv(app* e, unsigned i) {
switch (e->get_decl_kind()) { switch (e->get_decl_kind()) {
case OP_BAND: case OP_BAND:
SASSERT(e->get_num_args() >= 2); SASSERT(e->get_num_args() >= 2);
@ -845,7 +845,7 @@ namespace bv {
} }
} }
bool sls_eval::try_repair_eq(app* e, unsigned i) { bool bv_eval::try_repair_eq(app* e, unsigned i) {
auto child = e->get_arg(i); auto child = e->get_arg(i);
auto is_true = bval0(e); auto is_true = bval0(e);
if (bv.is_bv(child)) { if (bv.is_bv(child)) {
@ -856,7 +856,7 @@ namespace bv {
return false; return false;
} }
bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) { bool bv_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
if (is_true) { if (is_true) {
if (m_rand(20) != 0) if (m_rand(20) != 0)
if (a.try_set(b.bits())) if (a.try_set(b.bits()))
@ -884,7 +884,7 @@ namespace bv {
} }
} }
void sls_eval::fold_oper(bvect& out, app* t, unsigned i, std::function<void(bvect&, bvval const&)> const& f) { void bv_eval::fold_oper(bvect& out, app* t, unsigned i, std::function<void(bvect&, bvval const&)> const& f) {
auto i2 = i == 0 ? 1 : 0; auto i2 = i == 0 ? 1 : 0;
auto const& c = wval(t->get_arg(i2)); auto const& c = wval(t->get_arg(i2));
for (unsigned j = 0; j < c.nw; ++j) for (unsigned j = 0; j < c.nw; ++j)
@ -904,13 +904,13 @@ namespace bv {
// e[i] = 0 & b[i] = 0 -> a[i] = random // e[i] = 0 & b[i] = 0 -> a[i] = random
// a := e[i] | (~b[i] & a[i]) // a := e[i] | (~b[i] & a[i])
bool sls_eval::try_repair_band(bvect const& e, bvval& a, bvval const& b) { bool bv_eval::try_repair_band(bvect const& e, bvval& a, bvval const& b) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = ~a.fixed[i] & (e[i] | (~b.bits()[i] & random_bits())); m_tmp[i] = ~a.fixed[i] & (e[i] | (~b.bits()[i] & random_bits()));
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
bool sls_eval::try_repair_band(app* t, unsigned i) { bool bv_eval::try_repair_band(app* t, unsigned i) {
bvect const& e = assign_value(t); bvect const& e = assign_value(t);
auto f = [&](bvect& out, bvval const& c) { auto f = [&](bvect& out, bvval const& c) {
for (unsigned j = 0; j < c.nw; ++j) for (unsigned j = 0; j < c.nw; ++j)
@ -930,13 +930,13 @@ namespace bv {
// set a[i] to 1 where b[i] = 0, e[i] = 1 // set a[i] to 1 where b[i] = 0, e[i] = 1
// set a[i] to 0 where e[i] = 0, a[i] = 1 // set a[i] to 0 where e[i] = 0, a[i] = 1
// //
bool sls_eval::try_repair_bor(bvect const& e, bvval& a, bvval const& b) { bool bv_eval::try_repair_bor(bvect const& e, bvval& a, bvval const& b) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = e[i] & (~b.bits()[i] | random_bits()); m_tmp[i] = e[i] & (~b.bits()[i] | random_bits());
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
bool sls_eval::try_repair_bor(app* t, unsigned i) { bool bv_eval::try_repair_bor(app* t, unsigned i) {
bvect const& e = assign_value(t); bvect const& e = assign_value(t);
auto f = [&](bvect& out, bvval const& c) { auto f = [&](bvect& out, bvval const& c) {
for (unsigned j = 0; j < c.nw; ++j) for (unsigned j = 0; j < c.nw; ++j)
@ -945,12 +945,12 @@ namespace bv {
fold_oper(m_tmp2, t, i, f); fold_oper(m_tmp2, t, i, f);
bvval& a = wval(t, i); bvval& a = wval(t, i);
for (unsigned j = 0; j < a.nw; ++j) for (unsigned j = 0; j < a.nw; ++j)
m_tmp[j] = e[i] & (~m_tmp2[i] | random_bits()); m_tmp[j] = e[j] & (~m_tmp2[j] | random_bits());
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) { bool bv_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = e[i] ^ b.bits()[i]; m_tmp[i] = e[i] ^ b.bits()[i];
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
@ -958,7 +958,7 @@ namespace bv {
bool sls_eval::try_repair_bxor(app* t, unsigned i) { bool bv_eval::try_repair_bxor(app* t, unsigned i) {
bvect const& e = assign_value(t); bvect const& e = assign_value(t);
auto f = [&](bvect& out, bvval const& c) { auto f = [&](bvect& out, bvval const& c) {
for (unsigned j = 0; j < c.nw; ++j) for (unsigned j = 0; j < c.nw; ++j)
@ -968,7 +968,7 @@ namespace bv {
bvval& a = wval(t, i); bvval& a = wval(t, i);
for (unsigned j = 0; j < a.nw; ++j) for (unsigned j = 0; j < a.nw; ++j)
m_tmp[j] = e[i] ^ m_tmp2[i]; m_tmp[j] = e[j] ^ m_tmp2[j];
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
@ -978,7 +978,7 @@ namespace bv {
// first try to set a := e - b // first try to set a := e - b
// If this fails, set a to a random value // If this fails, set a to a random value
// //
bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) { bool bv_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
if (m_rand(20) != 0) { if (m_rand(20) != 0) {
a.set_sub(m_tmp, e, b.bits()); a.set_sub(m_tmp, e, b.bits());
if (a.try_set(m_tmp)) if (a.try_set(m_tmp))
@ -987,7 +987,7 @@ namespace bv {
return a.set_random(m_rand); return a.set_random(m_rand);
} }
bool sls_eval::try_repair_add(app* t, unsigned i) { bool bv_eval::try_repair_add(app* t, unsigned i) {
bvval& a = wval(t, i); bvval& a = wval(t, i);
bvect const& e = assign_value(t); bvect const& e = assign_value(t);
if (m_rand(20) != 0) { if (m_rand(20) != 0) {
@ -1002,7 +1002,7 @@ namespace bv {
return a.set_random(m_rand); return a.set_random(m_rand);
} }
bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) { bool bv_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
if (m_rand(20) != 0) { if (m_rand(20) != 0) {
if (i == 0) if (i == 0)
// e = a - b -> a := e + b // e = a - b -> a := e + b
@ -1021,7 +1021,7 @@ namespace bv {
* e = a*b, then a = e * b^-1 * e = a*b, then a = e * b^-1
* 8*e = a*(2b), then a = 4e*b^-1 * 8*e = a*(2b), then a = 4e*b^-1
*/ */
bool sls_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) { bool bv_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
//verbose_stream() << e << " := " << a << " * " << b << "\n"; //verbose_stream() << e << " := " << a << " * " << b << "\n";
unsigned parity_e = a.parity(e); unsigned parity_e = a.parity(e);
unsigned parity_b = a.parity(b); unsigned parity_b = a.parity(b);
@ -1133,14 +1133,14 @@ namespace bv {
return a.set_random(m_rand); return a.set_random(m_rand);
} }
bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) { bool bv_eval::try_repair_bnot(bvect const& e, bvval& a) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = ~e[i]; m_tmp[i] = ~e[i];
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
bool sls_eval::try_repair_bneg(bvect const& e, bvval& a) { bool bv_eval::try_repair_bneg(bvect const& e, bvval& a) {
a.set_sub(m_tmp, m_zero, e); a.set_sub(m_tmp, m_zero, e);
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
@ -1154,7 +1154,7 @@ namespace bv {
// infeasible if b + 1 = p2 // infeasible if b + 1 = p2
// solve for x >=s b + 1 // solve for x >=s b + 1
// //
bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) { bool bv_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
auto& p2 = m_b; auto& p2 = m_b;
b.set_zero(p2); b.set_zero(p2);
p2.set(b.bw - 1, true); p2.set(b.bw - 1, true);
@ -1180,7 +1180,7 @@ namespace bv {
// infeasible if b = 0 // infeasible if b = 0
// solve for x <=s b - 1 // solve for x <=s b - 1
// //
bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) { bool bv_eval::try_repair_sge(bool e, bvval& a, bvval const& b) {
auto& p2 = m_b; auto& p2 = m_b;
b.set_zero(p2); b.set_zero(p2);
p2.set(b.bw - 1, true); p2.set(b.bw - 1, true);
@ -1211,7 +1211,7 @@ namespace bv {
// or // or
// x := random p2 <= x <= b if c < p2 (b >= p2) // x := random p2 <= x <= b if c < p2 (b >= p2)
// //
bool sls_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) { bool bv_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) {
bool r = false; bool r = false;
if (b < p2) { if (b < p2) {
bool coin = m_rand(2) == 0; bool coin = m_rand(2) == 0;
@ -1236,7 +1236,7 @@ namespace bv {
// x := random b <= x or x < p2 if d < p2 // x := random b <= x or x < p2 if d < p2
// //
bool sls_eval::try_repair_sge(bvval& a, bvect const& b, bvect const& p2) { bool bv_eval::try_repair_sge(bvval& a, bvect const& b, bvect const& p2) {
auto& p2_1 = m_tmp4; auto& p2_1 = m_tmp4;
a.set_sub(p2_1, p2, m_one); a.set_sub(p2_1, p2, m_one);
p2_1.set_bw(a.bw); p2_1.set_bw(a.bw);
@ -1258,14 +1258,14 @@ namespace bv {
return r; return r;
} }
void sls_eval::add_p2_1(bvval const& a, bvect& t) const { void bv_eval::add_p2_1(bvval const& a, bvect& t) const {
m_zero.set(a.bw - 1, true); m_zero.set(a.bw - 1, true);
a.set_add(t, a.bits(), m_zero); a.set_add(t, a.bits(), m_zero);
m_zero.set(a.bw - 1, false); m_zero.set(a.bw - 1, false);
a.clear_overflow_bits(t); a.clear_overflow_bits(t);
} }
bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) { bool bv_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
//verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n"; //verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n";
if (e) { if (e) {
// a <= t // a <= t
@ -1281,7 +1281,7 @@ namespace bv {
} }
} }
bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) { bool bv_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
//verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n"; //verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n";
if (e) { if (e) {
// a >= t // a >= t
@ -1297,11 +1297,11 @@ namespace bv {
} }
} }
bool sls_eval::try_repair_bit2bool(bvval& a, unsigned idx) { bool bv_eval::try_repair_bit2bool(bvval& a, unsigned idx) {
return a.try_set_bit(idx, !a.get_bit(idx)); return a.try_set_bit(idx, !a.get_bit(idx));
} }
bool sls_eval::try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
unsigned sh = b.to_nat(b.bw); unsigned sh = b.to_nat(b.bw);
if (sh == 0) if (sh == 0)
@ -1324,23 +1324,39 @@ namespace bv {
} }
} }
else { else {
// NB. blind sub-range of possible values for b
SASSERT(i == 1); SASSERT(i == 1);
unsigned sh = m_rand(a.bw + 1); if (a.is_zero())
b.set(m_tmp, sh); return b.set_random(m_rand);
return b.try_set(m_tmp);
unsigned start = m_rand();
for (unsigned j = 0; j <= a.bw; ++j) {
unsigned sh = (j + start) % (a.bw + 1);
m_tmp.set_bw(a.bw);
m_tmp2.set_bw(a.bw);
b.set(m_tmp, sh);
if (!b.can_set(m_tmp))
continue;
m_tmp2.set_shift_left(a.bits(), m_tmp);
if (m_tmp2 == e && b.try_set(m_tmp))
return true;
}
if (m_rand(2) == 0)
return false;
return b.set_random(m_rand);
} }
return false; return false;
} }
bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) { bool bv_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
if (i == 0) if (i == 0)
return try_repair_ashr0(e, a, b); return try_repair_ashr0(e, a, b);
else else
return try_repair_ashr1(e, a, b); return try_repair_ashr1(e, a, b);
} }
bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) if (i == 0)
return try_repair_lshr0(e, a, b); return try_repair_lshr0(e, a, b);
else else
@ -1354,7 +1370,7 @@ namespace bv {
* - e = 0 -> a := random * - e = 0 -> a := random
* - e > 0 -> a := random with msb(a) >= msb(e) * - e > 0 -> a := random with msb(a) >= msb(e)
*/ */
bool sls_eval::try_repair_lshr0(bvect const& e, bvval& a, bvval const& b) { bool bv_eval::try_repair_lshr0(bvect const& e, bvval& a, bvval const& b) {
auto& t = m_tmp; auto& t = m_tmp;
// t := e << b // t := e << b
@ -1433,7 +1449,7 @@ namespace bv {
* - e = 0: b := random * - e = 0: b := random
* - e > 0: b := random >= clz(e) * - e > 0: b := random >= clz(e)
*/ */
bool sls_eval::try_repair_lshr1(bvect const& e, bvval const& a, bvval& b) { bool bv_eval::try_repair_lshr1(bvect const& e, bvval const& a, bvval& b) {
auto& t = m_tmp; auto& t = m_tmp;
auto clza = a.clz(a.bits()); auto clza = a.clz(a.bits());
@ -1487,7 +1503,7 @@ namespace bv {
* weak: * weak:
* *
*/ */
bool sls_eval::try_repair_ashr0(bvect const& e, bvval& a, bvval const& b) { bool bv_eval::try_repair_ashr0(bvect const& e, bvval& a, bvval const& b) {
auto& t = m_tmp; auto& t = m_tmp;
t.set_bw(b.bw); t.set_bw(b.bw);
auto n = b.msb(b.bits()); auto n = b.msb(b.bits());
@ -1548,7 +1564,7 @@ namespace bv {
* - e > 0: b := random >= clz(e) * - e > 0: b := random >= clz(e)
*/ */
bool sls_eval::try_repair_ashr1(bvect const& e, bvval const& a, bvval& b) { bool bv_eval::try_repair_ashr1(bvect const& e, bvval const& a, bvval& b) {
auto& t = m_tmp; auto& t = m_tmp;
auto clza = a.clz(a.bits()); auto clza = a.clz(a.bits());
@ -1590,7 +1606,7 @@ namespace bv {
return b.set_repair(random_bool(), t); return b.set_repair(random_bool(), t);
} }
bool sls_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) {
SASSERT(e[0] == 0 || e[0] == 1); SASSERT(e[0] == 0 || e[0] == 1);
SASSERT(e.bw == 1); SASSERT(e.bw == 1);
return try_repair_eq(e[0] == 1, i == 0 ? a : b, i == 0 ? b : a); return try_repair_eq(e[0] == 1, i == 0 ? a : b, i == 0 ? b : a);
@ -1601,7 +1617,7 @@ namespace bv {
// b = 0 => e = -1 // nothing to repair on a // b = 0 => e = -1 // nothing to repair on a
// e != -1 => max(a) >=u e // e != -1 => max(a) >=u e
bool sls_eval::try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
if (a.is_zero(e) && a.is_ones(a.fixed) && a.is_ones()) if (a.is_zero(e) && a.is_ones(a.fixed) && a.is_ones())
return false; return false;
@ -1666,7 +1682,7 @@ namespace bv {
// (s != t => exists y . (mcb(x, y) and y >u t and (s - t) mod y = 0) // (s != t => exists y . (mcb(x, y) and y >u t and (s - t) mod y = 0)
bool sls_eval::try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
if (b.is_zero()) { if (b.is_zero()) {
@ -1711,21 +1727,21 @@ namespace bv {
} }
} }
bool sls_eval::add_overflow_on_fixed(bvval const& a, bvect const& t) { bool bv_eval::add_overflow_on_fixed(bvval const& a, bvect const& t) {
a.set(m_tmp3, m_zero); a.set(m_tmp3, m_zero);
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp3[i] = a.fixed[i] & a.bits()[i]; m_tmp3[i] = a.fixed[i] & a.bits()[i];
return a.set_add(m_tmp4, t, m_tmp3); return a.set_add(m_tmp4, t, m_tmp3);
} }
bool sls_eval::mul_overflow_on_fixed(bvval const& a, bvect const& t) { bool bv_eval::mul_overflow_on_fixed(bvval const& a, bvect const& t) {
a.set(m_tmp3, m_zero); a.set(m_tmp3, m_zero);
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp3[i] = a.fixed[i] & a.bits()[i]; m_tmp3[i] = a.fixed[i] & a.bits()[i];
return a.set_mul(m_tmp4, m_tmp3, t); return a.set_mul(m_tmp4, m_tmp3, t);
} }
bool sls_eval::try_repair_rotate_left(bvect const& e, bvval& a, unsigned n) const { bool bv_eval::try_repair_rotate_left(bvect const& e, bvval& a, unsigned n) const {
// a := rotate_right(e, n) // a := rotate_right(e, n)
n = (a.bw - n) % a.bw; n = (a.bw - n) % a.bw;
for (unsigned i = a.bw - n; i < a.bw; ++i) for (unsigned i = a.bw - n; i < a.bw; ++i)
@ -1735,7 +1751,7 @@ namespace bv {
return a.set_repair(true, m_tmp); return a.set_repair(true, m_tmp);
} }
bool sls_eval::try_repair_rotate_left(bvect const& e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_rotate_left(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
rational n = b.get_value(); rational n = b.get_value();
n = mod(n, rational(b.bw)); n = mod(n, rational(b.bw));
@ -1749,7 +1765,7 @@ namespace bv {
} }
} }
bool sls_eval::try_repair_rotate_right(bvect const& e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_rotate_right(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
rational n = b.get_value(); rational n = b.get_value();
n = mod(b.bw - n, rational(b.bw)); n = mod(b.bw - n, rational(b.bw));
@ -1763,7 +1779,7 @@ namespace bv {
} }
} }
bool sls_eval::try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i) { bool bv_eval::try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i) {
if (e) { if (e) {
// maximize // maximize
if (i == 0) { if (i == 0) {
@ -1792,7 +1808,7 @@ namespace bv {
// prefix of e must be 1s or 0 and match bit position of last bit in a. // prefix of e must be 1s or 0 and match bit position of last bit in a.
// set a to suffix of e, matching signs. // set a to suffix of e, matching signs.
// //
bool sls_eval::try_repair_sign_ext(bvect const& e, bvval& a) { bool bv_eval::try_repair_sign_ext(bvect const& e, bvval& a) {
for (unsigned i = a.bw; i < e.bw; ++i) for (unsigned i = a.bw; i < e.bw; ++i)
if (e.get(i) != e.get(a.bw - 1)) if (e.get(i) != e.get(a.bw - 1))
return false; return false;
@ -1806,7 +1822,7 @@ namespace bv {
// //
// prefix of e must be 0s. // prefix of e must be 0s.
// //
bool sls_eval::try_repair_zero_ext(bvect const& e, bvval& a) { bool bv_eval::try_repair_zero_ext(bvect const& e, bvval& a) {
for (unsigned i = a.bw; i < e.bw; ++i) for (unsigned i = a.bw; i < e.bw; ++i)
if (e.get(i)) if (e.get(i))
return false; return false;
@ -1817,7 +1833,7 @@ namespace bv {
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
bool sls_eval::try_repair_concat(app* e, unsigned idx) { bool bv_eval::try_repair_concat(app* e, unsigned idx) {
unsigned bw = 0; unsigned bw = 0;
auto& ve = assign_value(e); auto& ve = assign_value(e);
for (unsigned j = e->get_num_args() - 1; j > idx; --j) for (unsigned j = e->get_num_args() - 1; j > idx; --j)
@ -1834,7 +1850,7 @@ namespace bv {
// for the randomized assignment, // for the randomized assignment,
// set a outside of [hi:lo] to random values with preference to 0 or 1 bits // set a outside of [hi:lo] to random values with preference to 0 or 1 bits
// //
bool sls_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) { bool bv_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
if (m_rand(m_config.m_prob_randomize_extract) <= 100) { if (m_rand(m_config.m_prob_randomize_extract) <= 100) {
a.get_variant(m_tmp, m_rand); a.get_variant(m_tmp, m_rand);
if (0 == (m_rand(2))) { if (0 == (m_rand(2))) {
@ -1857,7 +1873,7 @@ namespace bv {
return a.set_random(m_rand); return a.set_random(m_rand);
} }
bool sls_eval::try_repair_int2bv(bvect const& e, expr* arg) { bool bv_eval::try_repair_int2bv(bvect const& e, expr* arg) {
rational r = e.get_value(e.nw); rational r = e.get_value(e.nw);
arith_util a(m); arith_util a(m);
expr_ref intval(a.mk_int(r), m); expr_ref intval(a.mk_int(r), m);
@ -1865,7 +1881,7 @@ namespace bv {
return true; return true;
} }
void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw, void bv_eval::set_div(bvect const& a, bvect const& b, unsigned bw,
bvect& quot, bvect& rem) const { bvect& quot, bvect& rem) const {
unsigned nw = (bw + 8 * sizeof(digit_t) - 1) / (8 * sizeof(digit_t)); unsigned nw = (bw + 8 * sizeof(digit_t) - 1) / (8 * sizeof(digit_t));
unsigned bnw = nw; unsigned bnw = nw;
@ -1885,7 +1901,7 @@ namespace bv {
} }
} }
bool sls_eval::repair_up(expr* e) { bool bv_eval::repair_up(expr* e) {
if (!is_app(e) || !can_eval1(to_app(e))) if (!is_app(e) || !can_eval1(to_app(e)))
return false; return false;
if (m.is_bool(e)) { if (m.is_bool(e)) {
@ -1913,13 +1929,13 @@ namespace bv {
return false; return false;
} }
sls_valuation& sls_eval::wval(expr* e) const { sls::bv_valuation& bv_eval::wval(expr* e) const {
// if (!m_values[e->get_id()]) verbose_stream() << mk_bounded_pp(e, m) << "\n"; // if (!m_values[e->get_id()]) verbose_stream() << mk_bounded_pp(e, m) << "\n";
return *m_values[e->get_id()]; return *m_values[e->get_id()];
} }
void sls_eval::commit_eval(app* e) { void bv_eval::commit_eval(app* e) {
if (!bv.is_bv(e)) if (!bv.is_bv(e))
return; return;
// //
@ -1927,12 +1943,12 @@ namespace bv {
VERIFY(wval(e).commit_eval()); VERIFY(wval(e).commit_eval());
} }
void sls_eval::set_random(app* e) { void bv_eval::set_random(app* e) {
if (bv.is_bv(e)) if (bv.is_bv(e))
eval(e).set_random(m_rand); eval(e).set_random(m_rand);
} }
bool sls_eval::eval_is_correct(app* e) { bool bv_eval::eval_is_correct(app* e) {
if (!can_eval1(e)) if (!can_eval1(e))
return false; return false;
if (m.is_bool(e)) if (m.is_bool(e))
@ -1947,7 +1963,7 @@ namespace bv {
return false; return false;
} }
expr_ref sls_eval::get_value(app* e) { expr_ref bv_eval::get_value(app* e) {
if (m.is_bool(e)) if (m.is_bool(e))
return expr_ref(m.mk_bool_val(bval0(e)), m); return expr_ref(m.mk_bool_val(bval0(e)), m);
else if (bv.is_bv(e)) { else if (bv.is_bv(e)) {
@ -1958,7 +1974,7 @@ namespace bv {
return expr_ref(m); return expr_ref(m);
} }
std::ostream& sls_eval::display(std::ostream& out) const { std::ostream& bv_eval::display(std::ostream& out) const {
auto& terms = ctx.subterms(); auto& terms = ctx.subterms();
for (expr* e : terms) { for (expr* e : terms) {
if (!bv.is_bv(e)) if (!bv.is_bv(e))
@ -1971,7 +1987,7 @@ namespace bv {
return out; return out;
} }
std::ostream& sls_eval::display_value(std::ostream& out, expr* e) const { std::ostream& bv_eval::display_value(std::ostream& out, expr* e) const {
if (bv.is_bv(e)) if (bv.is_bv(e))
return out << wval(e); return out << wval(e);
return out << "?"; return out << "?";

40
src/ast/sls/sls_bv_eval.h
View file

@ -17,27 +17,31 @@ Author:
#pragma once #pragma once
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/sls/sls_valuation.h" #include "ast/sls/sls_bv_valuation.h"
#include "ast/sls/bv_sls_fixed.h" #include "ast/sls/sls_bv_fixed.h"
#include "ast/sls/sls_context.h" #include "ast/sls/sls_context.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
namespace bv {
class sls_terms; namespace sls {
class sls_eval { class bv_terms;
using bvect = sls::bvect;
class bv_eval {
struct config { struct config {
unsigned m_prob_randomize_extract = 50; unsigned m_prob_randomize_extract = 50;
}; };
friend class sls_fixed; friend class sls::bv_fixed;
friend class sls_test; friend class sls_test;
ast_manager& m; ast_manager& m;
sls::context& ctx; sls::context& ctx;
sls_terms& terms; sls::bv_terms& terms;
bv_util bv; bv_util bv;
sls_fixed m_fix; sls::bv_fixed m_fix;
mutable mpn_manager mpn; mutable mpn_manager mpn;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
random_gen m_rand; random_gen m_rand;
@ -45,12 +49,12 @@ namespace bv {
bool_vector m_fixed; bool_vector m_fixed;
scoped_ptr_vector<sls_valuation> m_values; // expr-id -> bv valuation scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation
mutable bvect m_tmp, m_tmp2, m_tmp3, m_tmp4, m_mul_tmp, m_zero, m_one, m_minus_one; mutable bvect m_tmp, m_tmp2, m_tmp3, m_tmp4, m_mul_tmp, m_zero, m_one, m_minus_one;
bvect m_a, m_b, m_nextb, m_nexta, m_aux; bvect m_a, m_b, m_nextb, m_nexta, m_aux;
using bvval = sls_valuation; using bvval = sls::bv_valuation;
void init_eval_bv(app* e); void init_eval_bv(app* e);
@ -59,7 +63,7 @@ namespace bv {
* Return true if not already registered, false if already registered. * Return true if not already registered, false if already registered.
*/ */
void add_bit_vector(app* e); void add_bit_vector(app* e);
sls_valuation* alloc_valuation(app* e); sls::bv_valuation* alloc_valuation(app* e);
bool bval1_bv(app* e) const; bool bval1_bv(app* e) const;
@ -120,13 +124,12 @@ namespace bv {
digit_t random_bits(); digit_t random_bits();
bool random_bool() { return m_rand() % 2 == 0; } bool random_bool() { return m_rand() % 2 == 0; }
sls_valuation& wval(app* e, unsigned i) { return wval(e->get_arg(i)); } sls::bv_valuation& wval(app* e, unsigned i) { return wval(e->get_arg(i)); }
void eval(app* e, sls_valuation& val) const; void eval(app* e, sls::bv_valuation& val) const;
bvect const& assign_value(app* e) const { return wval(e).bits(); } bvect const& assign_value(app* e) const { return wval(e).bits(); }
bool bval0(expr* e) const { return ctx.is_true(e); }
/** /**
* Retrieve evaluation based on immediate children. * Retrieve evaluation based on immediate children.
@ -137,7 +140,7 @@ namespace bv {
void commit_eval(app* e); void commit_eval(app* e);
public: public:
sls_eval(sls_terms& terms, sls::context& ctx); bv_eval(sls::bv_terms& terms, sls::context& ctx);
void init() { m_fix.init(); } void init() { m_fix.init(); }
@ -149,13 +152,13 @@ namespace bv {
* wval - Word (bit-vector) values * wval - Word (bit-vector) values
*/ */
sls_valuation& wval(expr* e) const; sls::bv_valuation& wval(expr* e) const;
void set(expr* e, sls_valuation const& val); void set(expr* e, sls::bv_valuation const& val);
bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); } bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); }
sls_valuation& eval(app* e) const; sls::bv_valuation& eval(app* e) const;
void set_random(app* e); void set_random(app* e);
@ -165,6 +168,7 @@ namespace bv {
expr_ref get_value(app* e); expr_ref get_value(app* e);
bool bval0(expr* e) const { return ctx.is_true(e); }
bool bval1(app* e) const; bool bval1(app* e) const;
/* /*

28
src/ast/sls/sls_bv_fixed.cpp
View file

@ -13,13 +13,13 @@ Author:
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/sls/bv_sls_fixed.h" #include "ast/sls/sls_bv_fixed.h"
#include "ast/sls/bv_sls_terms.h" #include "ast/sls/sls_bv_terms.h"
#include "ast/sls/bv_sls_eval.h" #include "ast/sls/sls_bv_eval.h"
namespace bv { namespace sls {
sls_fixed::sls_fixed(sls_eval& ev, sls_terms& terms, sls::context& ctx): bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx):
ev(ev), ev(ev),
terms(terms), terms(terms),
m(ev.m), m(ev.m),
@ -27,7 +27,7 @@ namespace bv {
ctx(ctx) ctx(ctx)
{} {}
void sls_fixed::init() { void bv_fixed::init() {
for (auto e : ctx.subterms()) for (auto e : ctx.subterms())
set_fixed(e); set_fixed(e);
@ -44,7 +44,7 @@ namespace bv {
propagate_range_up(e); propagate_range_up(e);
} }
void sls_fixed::propagate_range_up(expr* e) { void bv_fixed::propagate_range_up(expr* e) {
expr* t, * s; expr* t, * s;
rational v; rational v;
if (bv.is_concat(e, t, s)) { if (bv.is_concat(e, t, s)) {
@ -81,7 +81,7 @@ namespace bv {
// s <=s t <=> s + K <= t + K, K = 2^{bw-1} // s <=s t <=> s + K <= t + K, K = 2^{bw-1}
bool sls_fixed::init_range(app* e, bool sign) { bool bv_fixed::init_range(app* e, bool sign) {
expr* s, * t, * x, * y; expr* s, * t, * x, * y;
rational a, b; rational a, b;
unsigned idx; unsigned idx;
@ -149,7 +149,7 @@ namespace bv {
return false; return false;
} }
bool sls_fixed::init_eq(expr* t, rational const& a, bool sign) { bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) {
unsigned lo, hi; unsigned lo, hi;
rational b(0); rational b(0);
// verbose_stream() << mk_bounded_pp(t, m) << " == " << a << "\n"; // verbose_stream() << mk_bounded_pp(t, m) << " == " << a << "\n";
@ -213,7 +213,7 @@ namespace bv {
// a < x + b <=> ! (x + b <= a) <=> x not in [-a, b - a [ <=> x in [b - a, -a [ a != -1 // a < x + b <=> ! (x + b <= a) <=> x not in [-a, b - a [ <=> x in [b - a, -a [ a != -1
// x + a < x + b <=> ! (x + b <= x + a) <=> x in [-a, -b [ a != b // x + a < x + b <=> ! (x + b <= x + a) <=> x in [-a, -b [ a != b
// //
bool sls_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) { bool bv_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) {
if (!x && !y) if (!x && !y)
return false; return false;
if (!x) if (!x)
@ -225,7 +225,7 @@ namespace bv {
return false; return false;
} }
bool sls_fixed::add_range(expr* e, rational lo, rational hi, bool sign) { bool bv_fixed::add_range(expr* e, rational lo, rational hi, bool sign) {
auto& v = ev.wval(e); auto& v = ev.wval(e);
lo = mod(lo, rational::power_of_two(bv.get_bv_size(e))); lo = mod(lo, rational::power_of_two(bv.get_bv_size(e)));
hi = mod(hi, rational::power_of_two(bv.get_bv_size(e))); hi = mod(hi, rational::power_of_two(bv.get_bv_size(e)));
@ -252,7 +252,7 @@ namespace bv {
return true; return true;
} }
void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) { void bv_fixed::get_offset(expr* e, expr*& x, rational& offset) {
expr* s, * t; expr* s, * t;
x = e; x = e;
offset = 0; offset = 0;
@ -275,13 +275,13 @@ namespace bv {
x = nullptr; x = nullptr;
} }
bool sls_fixed::is_fixed1(app* e) const { bool bv_fixed::is_fixed1(app* e) const {
if (is_uninterp(e)) if (is_uninterp(e))
return false; return false;
return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); }); return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); });
} }
void sls_fixed::set_fixed(expr* _e) { void bv_fixed::set_fixed(expr* _e) {
if (!is_app(_e)) if (!is_app(_e))
return; return;
auto e = to_app(_e); auto e = to_app(_e);

17
src/ast/sls/sls_bv_fixed.h
View file

@ -17,18 +17,19 @@ Author:
#pragma once #pragma once
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/sls/sls_valuation.h" #include "ast/sls/sls_bv_valuation.h"
#include "ast/sls/sls_context.h" #include "ast/sls/sls_context.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
namespace bv {
class sls_eval; namespace sls {
class sls_terms;
class sls_fixed { class bv_terms;
sls_eval& ev; class bv_eval;
sls_terms& terms;
class bv_fixed {
typename bv_eval& ev;
typename bv_terms& terms;
ast_manager& m; ast_manager& m;
bv_util& bv; bv_util& bv;
sls::context& ctx; sls::context& ctx;
@ -44,7 +45,7 @@ namespace bv {
void set_fixed(expr* e); void set_fixed(expr* e);
public: public:
sls_fixed(sls_eval& ev, sls_terms& terms, sls::context& ctx); bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx);
void init(); void init();
}; };
} }

3
src/ast/sls/sls_bv_plugin.cpp
View file

@ -57,7 +57,6 @@ namespace sls {
return; return;
auto a = to_app(e); auto a = to_app(e);
// verbose_stream() << "propagate " << mk_bounded_pp(e, m) << " " << m_eval.eval_is_correct(a) << "\n";
if (!m_eval.eval_is_correct(a)) if (!m_eval.eval_is_correct(a))
ctx.new_value_eh(e); ctx.new_value_eh(e);
} }
@ -201,7 +200,7 @@ namespace sls {
// unsigned value = 0; // unsigned value = 0;
// if (bv.is_bv(e)) // if (bv.is_bv(e))
// value = svector_hash<unsigned_hash>()(m_eval.wval(e).bits()); // value = svector_hash<unsigned_hash>()(m_eval.wval(e).bits());
IF_VERBOSE(2, verbose_stream() << mk_bounded_pp(e, m) << " " << (up_down?"u":"d") << " " << (success ? "S" : "F"); IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << " " << (up_down?"u":"d") << " " << (success ? "S" : "F");
// if (bv.is_bv(e)) verbose_stream() << " " << m_eval.wval(e).bits(); // if (bv.is_bv(e)) verbose_stream() << " " << m_eval.wval(e).bits();
verbose_stream() << "\n"); verbose_stream() << "\n");
} }

8
src/ast/sls/sls_bv_plugin.h
View file

@ -18,15 +18,15 @@ Author:
#include "ast/sls/sls_context.h" #include "ast/sls/sls_context.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/sls/bv_sls_terms.h" #include "ast/sls/sls_bv_terms.h"
#include "ast/sls/bv_sls_eval.h" #include "ast/sls/sls_bv_eval.h"
namespace sls { namespace sls {
class bv_plugin : public plugin { class bv_plugin : public plugin {
bv_util bv; bv_util bv;
bv::sls_terms m_terms; sls::bv_terms m_terms;
bv::sls_eval m_eval; bv_eval m_eval;
bv::sls_stats m_stats; bv::sls_stats m_stats;
bool m_initialized = false; bool m_initialized = false;

16
src/ast/sls/sls_bv_terms.cpp
View file

@ -16,25 +16,25 @@ Author:
--*/ --*/
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/sls/bv_sls_terms.h" #include "ast/sls/sls_bv_terms.h"
#include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/bv_rewriter.h" #include "ast/rewriter/bv_rewriter.h"
namespace bv { namespace sls {
sls_terms::sls_terms(sls::context& ctx): bv_terms::bv_terms(sls::context& ctx):
ctx(ctx), ctx(ctx),
m(ctx.get_manager()), m(ctx.get_manager()),
bv(m), bv(m),
m_axioms(m) {} m_axioms(m) {}
void sls_terms::register_term(expr* e) { void bv_terms::register_term(expr* e) {
auto r = ensure_binary(e); auto r = ensure_binary(e);
if (r != e) if (r != e)
m_axioms.push_back(m.mk_eq(e, r)); m_axioms.push_back(m.mk_eq(e, r));
} }
expr_ref sls_terms::ensure_binary(expr* e) { expr_ref bv_terms::ensure_binary(expr* e) {
app* a = to_app(e); app* a = to_app(e);
auto arg = [&](unsigned i) { auto arg = [&](unsigned i) {
@ -64,7 +64,7 @@ namespace bv {
return r; return r;
} }
expr_ref sls_terms::mk_sdiv(expr* x, expr* y) { expr_ref bv_terms::mk_sdiv(expr* x, expr* y) {
// d = udiv(abs(x), abs(y)) // d = udiv(abs(x), abs(y))
// y = 0, x >= 0 -> -1 // y = 0, x >= 0 -> -1
// y = 0, x < 0 -> 1 // y = 0, x < 0 -> 1
@ -92,7 +92,7 @@ namespace bv {
return r; return r;
} }
expr_ref sls_terms::mk_smod(expr* x, expr* y) { expr_ref bv_terms::mk_smod(expr* x, expr* y) {
// u := umod(abs(x), abs(y)) // u := umod(abs(x), abs(y))
// u = 0 -> 0 // u = 0 -> 0
// y = 0 -> x // y = 0 -> x
@ -116,7 +116,7 @@ namespace bv {
return r; return r;
} }
expr_ref sls_terms::mk_srem(expr* x, expr* y) { expr_ref bv_terms::mk_srem(expr* x, expr* y) {
// y = 0 -> x // y = 0 -> x
// else x - sdiv(x, y) * y // else x - sdiv(x, y) * y
expr_ref r(m); expr_ref r(m);

8
src/ast/sls/sls_bv_terms.h
View file

@ -23,12 +23,12 @@ Author:
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/sls/sls_stats.h" #include "ast/sls/sls_stats.h"
#include "ast/sls/sls_powers.h" #include "ast/sls/sls_powers.h"
#include "ast/sls/sls_valuation.h" #include "ast/sls/sls_bv_valuation.h"
#include "ast/sls/sls_context.h" #include "ast/sls/sls_context.h"
namespace bv { namespace sls {
class sls_terms { class bv_terms {
sls::context& ctx; sls::context& ctx;
ast_manager& m; ast_manager& m;
bv_util bv; bv_util bv;
@ -41,7 +41,7 @@ namespace bv {
expr_ref mk_srem(expr* x, expr* y); expr_ref mk_srem(expr* x, expr* y);
public: public:
sls_terms(sls::context& ctx); bv_terms(sls::context& ctx);
void register_term(expr* e); void register_term(expr* e);

77
src/ast/sls/sls_bv_valuation.cpp
View file

@ -18,9 +18,9 @@ Author:
--*/ --*/
#include "ast/sls/sls_valuation.h" #include "ast/sls/sls_bv_valuation.h"
namespace bv { namespace sls {
void bvect::set_bw(unsigned bw) { void bvect::set_bw(unsigned bw) {
this->bw = bw; this->bw = bw;
@ -138,6 +138,7 @@ namespace bv {
set_bw(a.bw); set_bw(a.bw);
SASSERT(a.bw == b.bw); SASSERT(a.bw == b.bw);
unsigned shift = b.to_nat(b.bw); unsigned shift = b.to_nat(b.bw);
if (shift == 0) if (shift == 0)
a.copy_to(a.nw, *this); a.copy_to(a.nw, *this);
else if (shift >= a.bw) else if (shift >= a.bw)
@ -148,7 +149,7 @@ namespace bv {
return *this; return *this;
} }
sls_valuation::sls_valuation(unsigned bw) { bv_valuation::bv_valuation(unsigned bw) {
set_bw(bw); set_bw(bw);
m_lo.set_bw(bw); m_lo.set_bw(bw);
m_hi.set_bw(bw); m_hi.set_bw(bw);
@ -162,7 +163,7 @@ namespace bv {
fixed[nw - 1] = ~mask; fixed[nw - 1] = ~mask;
} }
void sls_valuation::set_bw(unsigned b) { void bv_valuation::set_bw(unsigned b) {
bw = b; bw = b;
nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t)); nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t));
mask = (1 << (bw % (8 * sizeof(digit_t)))) - 1; mask = (1 << (bw % (8 * sizeof(digit_t)))) - 1;
@ -170,7 +171,7 @@ namespace bv {
mask = ~(digit_t)0; mask = ~(digit_t)0;
} }
bool sls_valuation::commit_eval() { bool bv_valuation::commit_eval() {
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
if (0 != (fixed[i] & (m_bits[i] ^ eval[i]))) if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))
return false; return false;
@ -184,7 +185,7 @@ namespace bv {
return true; return true;
} }
bool sls_valuation::in_range(bvect const& bits) const { bool bv_valuation::in_range(bvect const& bits) const {
mpn_manager m; mpn_manager m;
auto c = m.compare(m_lo.data(), nw, m_hi.data(), nw); auto c = m.compare(m_lo.data(), nw, m_hi.data(), nw);
SASSERT(!has_overflow(bits)); SASSERT(!has_overflow(bits));
@ -207,7 +208,7 @@ namespace bv {
// largest dst <= src and dst is feasible // largest dst <= src and dst is feasible
// //
bool sls_valuation::get_at_most(bvect const& src, bvect& dst) const { bool bv_valuation::get_at_most(bvect const& src, bvect& dst) const {
SASSERT(!has_overflow(src)); SASSERT(!has_overflow(src));
src.copy_to(nw, dst); src.copy_to(nw, dst);
sup_feasible(dst); sup_feasible(dst);
@ -227,7 +228,7 @@ namespace bv {
// //
// smallest dst >= src and dst is feasible with respect to this. // smallest dst >= src and dst is feasible with respect to this.
bool sls_valuation::get_at_least(bvect const& src, bvect& dst) const { bool bv_valuation::get_at_least(bvect const& src, bvect& dst) const {
SASSERT(!has_overflow(src)); SASSERT(!has_overflow(src));
src.copy_to(nw, dst); src.copy_to(nw, dst);
dst.set_bw(bw); dst.set_bw(bw);
@ -244,7 +245,7 @@ namespace bv {
return true; return true;
} }
bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) { bool bv_valuation::set_random_at_most(bvect const& src, random_gen& r) {
m_tmp.set_bw(bw); m_tmp.set_bw(bw);
if (!get_at_most(src, m_tmp)) if (!get_at_most(src, m_tmp))
return false; return false;
@ -258,7 +259,7 @@ namespace bv {
return (can_set(m_tmp) || get_at_most(src, m_tmp)) && m_tmp <= src && try_set(m_tmp); return (can_set(m_tmp) || get_at_most(src, m_tmp)) && m_tmp <= src && try_set(m_tmp);
} }
bool sls_valuation::set_random_at_least(bvect const& src, random_gen& r) { bool bv_valuation::set_random_at_least(bvect const& src, random_gen& r) {
m_tmp.set_bw(bw); m_tmp.set_bw(bw);
if (!get_at_least(src, m_tmp)) if (!get_at_least(src, m_tmp))
return false; return false;
@ -272,7 +273,7 @@ namespace bv {
return (can_set(m_tmp) || get_at_least(src, m_tmp)) && src <= m_tmp && try_set(m_tmp); return (can_set(m_tmp) || get_at_least(src, m_tmp)) && src <= m_tmp && try_set(m_tmp);
} }
bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) { bool bv_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) {
bvect& tmp = m_tmp; bvect& tmp = m_tmp;
if (0 == r(2)) { if (0 == r(2)) {
if (!get_at_least(lo, tmp)) if (!get_at_least(lo, tmp))
@ -299,27 +300,27 @@ namespace bv {
return false; return false;
} }
void sls_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) { void bv_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
for (unsigned i = bw; !is_feasible(dst) && i-- > 0; ) for (unsigned i = bw; !is_feasible(dst) && i-- > 0; )
if (!fixed.get(i) && dst.get(i)) if (!fixed.get(i) && dst.get(i))
dst.set(i, false); dst.set(i, false);
repair_sign_bits(dst); repair_sign_bits(dst);
} }
void sls_valuation::round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) { void bv_valuation::round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
for (unsigned i = 0; !is_feasible(dst) && i < bw; ++i) for (unsigned i = 0; !is_feasible(dst) && i < bw; ++i)
if (!fixed.get(i) && !dst.get(i)) if (!fixed.get(i) && !dst.get(i))
dst.set(i, true); dst.set(i, true);
repair_sign_bits(dst); repair_sign_bits(dst);
} }
void sls_valuation::set_random_above(bvect& dst, random_gen& r) { void bv_valuation::set_random_above(bvect& dst, random_gen& r) {
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
dst[i] = dst[i] | (random_bits(r) & ~fixed[i]); dst[i] = dst[i] | (random_bits(r) & ~fixed[i]);
repair_sign_bits(dst); repair_sign_bits(dst);
} }
void sls_valuation::set_random_below(bvect& dst, random_gen& r) { void bv_valuation::set_random_below(bvect& dst, random_gen& r) {
if (is_zero(dst)) if (is_zero(dst))
return; return;
unsigned n = 0, idx = UINT_MAX; unsigned n = 0, idx = UINT_MAX;
@ -336,7 +337,7 @@ namespace bv {
repair_sign_bits(dst); repair_sign_bits(dst);
} }
bool sls_valuation::set_repair(bool try_down, bvect& dst) { bool bv_valuation::set_repair(bool try_down, bvect& dst) {
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]); dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
clear_overflow_bits(dst); clear_overflow_bits(dst);
@ -372,7 +373,7 @@ namespace bv {
return repaired; return repaired;
} }
void sls_valuation::min_feasible(bvect& out) const { void bv_valuation::min_feasible(bvect& out) const {
if (m_lo < m_hi) if (m_lo < m_hi)
m_lo.copy_to(nw, out); m_lo.copy_to(nw, out);
else { else {
@ -383,7 +384,7 @@ namespace bv {
SASSERT(!has_overflow(out)); SASSERT(!has_overflow(out));
} }
void sls_valuation::max_feasible(bvect& out) const { void bv_valuation::max_feasible(bvect& out) const {
if (m_lo < m_hi) { if (m_lo < m_hi) {
m_hi.copy_to(nw, out); m_hi.copy_to(nw, out);
sub1(out); sub1(out);
@ -396,7 +397,7 @@ namespace bv {
SASSERT(!has_overflow(out)); SASSERT(!has_overflow(out));
} }
unsigned sls_valuation::msb(bvect const& src) const { unsigned bv_valuation::msb(bvect const& src) const {
SASSERT(!has_overflow(src)); SASSERT(!has_overflow(src));
for (unsigned i = nw; i-- > 0; ) for (unsigned i = nw; i-- > 0; )
if (src[i] != 0) if (src[i] != 0)
@ -404,7 +405,7 @@ namespace bv {
return bw; return bw;
} }
unsigned sls_valuation::clz(bvect const& src) const { unsigned bv_valuation::clz(bvect const& src) const {
SASSERT(!has_overflow(src)); SASSERT(!has_overflow(src));
unsigned i = bw; unsigned i = bw;
for (; i-- > 0; ) for (; i-- > 0; )
@ -414,36 +415,36 @@ namespace bv {
} }
void sls_valuation::set_value(bvect& bits, rational const& n) { void bv_valuation::set_value(bvect& bits, rational const& n) {
for (unsigned i = 0; i < bw; ++i) for (unsigned i = 0; i < bw; ++i)
bits.set(i, n.get_bit(i)); bits.set(i, n.get_bit(i));
clear_overflow_bits(bits); clear_overflow_bits(bits);
} }
void sls_valuation::get(bvect& dst) const { void bv_valuation::get(bvect& dst) const {
m_bits.copy_to(nw, dst); m_bits.copy_to(nw, dst);
} }
digit_t sls_valuation::random_bits(random_gen& rand) { digit_t bv_valuation::random_bits(random_gen& rand) {
digit_t r = 0; digit_t r = 0;
for (digit_t i = 0; i < sizeof(digit_t); ++i) for (digit_t i = 0; i < sizeof(digit_t); ++i)
r ^= rand() << (8 * i); r ^= rand() << (8 * i);
return r; return r;
} }
void sls_valuation::get_variant(bvect& dst, random_gen& r) const { void bv_valuation::get_variant(bvect& dst, random_gen& r) const {
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
dst[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & m_bits[i]); dst[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & m_bits[i]);
repair_sign_bits(dst); repair_sign_bits(dst);
clear_overflow_bits(dst); clear_overflow_bits(dst);
} }
bool sls_valuation::set_random(random_gen& r) { bool bv_valuation::set_random(random_gen& r) {
get_variant(m_tmp, r); get_variant(m_tmp, r);
return set_repair(r(2) == 0, m_tmp); return set_repair(r(2) == 0, m_tmp);
} }
void sls_valuation::repair_sign_bits(bvect& dst) const { void bv_valuation::repair_sign_bits(bvect& dst) const {
if (m_signed_prefix == 0) if (m_signed_prefix == 0)
return; return;
bool sign = m_signed_prefix == bw ? dst.get(bw - 1) : dst.get(bw - m_signed_prefix - 1); bool sign = m_signed_prefix == bw ? dst.get(bw - 1) : dst.get(bw - m_signed_prefix - 1);
@ -469,7 +470,7 @@ namespace bv {
// 0 = (new_bits ^ bits) & fixedf // 0 = (new_bits ^ bits) & fixedf
// also check that new_bits are in range // also check that new_bits are in range
// //
bool sls_valuation::can_set(bvect const& new_bits) const { bool bv_valuation::can_set(bvect const& new_bits) const {
SASSERT(!has_overflow(new_bits)); SASSERT(!has_overflow(new_bits));
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
if (0 != ((new_bits[i] ^ m_bits[i]) & fixed[i])) if (0 != ((new_bits[i] ^ m_bits[i]) & fixed[i]))
@ -477,21 +478,21 @@ namespace bv {
return in_range(new_bits); return in_range(new_bits);
} }
unsigned sls_valuation::to_nat(unsigned max_n) const { unsigned bv_valuation::to_nat(unsigned max_n) const {
bvect const& d = m_bits; bvect const& d = m_bits;
SASSERT(!has_overflow(d)); SASSERT(!has_overflow(d));
return d.to_nat(max_n); return d.to_nat(max_n);
} }
void sls_valuation::shift_right(bvect& out, unsigned shift) const { void bv_valuation::shift_right(bvect& out, unsigned shift) const {
SASSERT(shift < bw); SASSERT(shift < bw);
for (unsigned i = 0; i < bw; ++i) for (unsigned i = 0; i < bw; ++i)
out.set(i, i + shift < bw ? out.get(i + shift) : false); out.set(i, i + shift < bw ? out.get(i + shift) : false);
SASSERT(well_formed()); SASSERT(well_formed());
} }
void sls_valuation::add_range(rational l, rational h) { void bv_valuation::add_range(rational l, rational h) {
l = mod(l, rational::power_of_two(bw)); l = mod(l, rational::power_of_two(bw));
h = mod(h, rational::power_of_two(bw)); h = mod(h, rational::power_of_two(bw));
@ -550,7 +551,7 @@ namespace bv {
// update bits based on ranges // update bits based on ranges
// //
unsigned sls_valuation::diff_index(bvect const& a) const { unsigned bv_valuation::diff_index(bvect const& a) const {
unsigned index = 0; unsigned index = 0;
for (unsigned i = nw; i-- > 0; ) { for (unsigned i = nw; i-- > 0; ) {
auto diff = fixed[i] & (m_bits[i] ^ a[i]); auto diff = fixed[i] & (m_bits[i] ^ a[i]);
@ -560,7 +561,7 @@ namespace bv {
return index; return index;
} }
void sls_valuation::inf_feasible(bvect& a) const { void bv_valuation::inf_feasible(bvect& a) const {
unsigned lo_index = diff_index(a); unsigned lo_index = diff_index(a);
if (lo_index != 0) { if (lo_index != 0) {
@ -583,7 +584,7 @@ namespace bv {
} }
} }
void sls_valuation::sup_feasible(bvect& a) const { void bv_valuation::sup_feasible(bvect& a) const {
unsigned hi_index = diff_index(a); unsigned hi_index = diff_index(a);
if (hi_index != 0) { if (hi_index != 0) {
hi_index--; hi_index--;
@ -605,7 +606,7 @@ namespace bv {
} }
} }
void sls_valuation::tighten_range() { void bv_valuation::tighten_range() {
if (m_lo == m_hi) if (m_lo == m_hi)
return; return;
@ -691,13 +692,13 @@ namespace bv {
SASSERT(well_formed()); SASSERT(well_formed());
} }
void sls_valuation::set_sub(bvect& out, bvect const& a, bvect const& b) const { void bv_valuation::set_sub(bvect& out, bvect const& a, bvect const& b) const {
digit_t c; digit_t c;
mpn_manager().sub(a.data(), nw, b.data(), nw, out.data(), &c); mpn_manager().sub(a.data(), nw, b.data(), nw, out.data(), &c);
clear_overflow_bits(out); clear_overflow_bits(out);
} }
bool sls_valuation::set_add(bvect& out, bvect const& a, bvect const& b) const { bool bv_valuation::set_add(bvect& out, bvect const& a, bvect const& b) const {
digit_t c; digit_t c;
mpn_manager().add(a.data(), nw, b.data(), nw, out.data(), nw + 1, &c); mpn_manager().add(a.data(), nw, b.data(), nw, out.data(), nw + 1, &c);
bool ovfl = out[nw] != 0 || has_overflow(out); bool ovfl = out[nw] != 0 || has_overflow(out);
@ -705,7 +706,7 @@ namespace bv {
return ovfl; return ovfl;
} }
bool sls_valuation::set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow) const { bool bv_valuation::set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow) const {
out.reserve(2 * nw); out.reserve(2 * nw);
SASSERT(out.size() >= 2 * nw); SASSERT(out.size() >= 2 * nw);
mpn_manager().mul(a.data(), nw, b.data(), nw, out.data()); mpn_manager().mul(a.data(), nw, b.data(), nw, out.data());
@ -719,7 +720,7 @@ namespace bv {
return ovfl; return ovfl;
} }
bool sls_valuation::is_power_of2(bvect const& src) const { bool bv_valuation::is_power_of2(bvect const& src) const {
unsigned c = 0; unsigned c = 0;
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
c += get_num_1bits(src[i]); c += get_num_1bits(src[i]);

18
src/ast/sls/sls_bv_valuation.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Microsoft Corporation
Module Name: Module Name:
sls_valuation.h sls_bv_valuation.h
Abstract: Abstract:
@ -20,12 +20,10 @@ Author:
#include "util/params.h" #include "util/params.h"
#include "util/scoped_ptr_vector.h" #include "util/scoped_ptr_vector.h"
#include "util/uint_set.h" #include "util/uint_set.h"
#include "ast/ast.h" #include "util/mpz.h"
#include "ast/sls/sls_stats.h" #include "util/rational.h"
#include "ast/sls/sls_powers.h"
#include "ast/bv_decl_plugin.h"
namespace bv { namespace sls {
class bvect : public svector<digit_t> { class bvect : public svector<digit_t> {
public: public:
@ -106,7 +104,7 @@ namespace bv {
inline bool operator!=(bvect const& a, bvect const& b) { return !(a == b); } inline bool operator!=(bvect const& a, bvect const& b) { return !(a == b); }
std::ostream& operator<<(std::ostream& out, bvect const& v); std::ostream& operator<<(std::ostream& out, bvect const& v);
class sls_valuation { class bv_valuation {
protected: protected:
bvect m_bits; bvect m_bits;
bvect m_lo, m_hi; // range assignment to bit-vector, as wrap-around interval bvect m_lo, m_hi; // range assignment to bit-vector, as wrap-around interval
@ -125,7 +123,7 @@ namespace bv {
bvect eval; // current evaluation bvect eval; // current evaluation
sls_valuation(unsigned bw); bv_valuation(unsigned bw);
void set_bw(unsigned bw); void set_bw(unsigned bw);
void set_signed(unsigned prefix) { m_signed_prefix = prefix; } void set_signed(unsigned prefix) { m_signed_prefix = prefix; }
@ -176,7 +174,7 @@ namespace bv {
bool in_range(bvect const& bits) const; bool in_range(bvect const& bits) const;
bool can_set(bvect const& bits) const; bool can_set(bvect const& bits) const;
bool eq(sls_valuation const& other) const { return eq(other.m_bits); } bool eq(bv_valuation const& other) const { return eq(other.m_bits); }
bool eq(bvect const& other) const { return other == m_bits; } bool eq(bvect const& other) const { return other == m_bits; }
bool is_zero() const { return is_zero(m_bits); } bool is_zero() const { return is_zero(m_bits); }
@ -343,6 +341,6 @@ namespace bv {
}; };
inline std::ostream& operator<<(std::ostream& out, sls_valuation const& v) { return v.display(out); } inline std::ostream& operator<<(std::ostream& out, bv_valuation const& v) { return v.display(out); }
} }

11
src/ast/sls/sls_context.cpp
View file

@ -36,7 +36,8 @@ namespace sls {
m_gd(*this), m_gd(*this),
m_ld(*this), m_ld(*this),
m_repair_down(m.get_num_asts(), m_gd), m_repair_down(m.get_num_asts(), m_gd),
m_repair_up(m.get_num_asts(), m_ld) { m_repair_up(m.get_num_asts(), m_ld),
m_todo(m) {
register_plugin(alloc(euf_plugin, *this)); register_plugin(alloc(euf_plugin, *this));
register_plugin(alloc(arith_plugin, *this)); register_plugin(alloc(arith_plugin, *this));
register_plugin(alloc(bv_plugin, *this)); register_plugin(alloc(bv_plugin, *this));
@ -417,6 +418,8 @@ namespace sls {
m_todo.pop_back(); m_todo.pop_back();
else if (is_app(e)) { else if (is_app(e)) {
if (all_of(*to_app(e), [&](expr* arg) { return is_visited(arg); })) { if (all_of(*to_app(e), [&](expr* arg) { return is_visited(arg); })) {
expr_ref _e(e, m);
m_todo.pop_back();
for (expr* arg : *to_app(e)) { for (expr* arg : *to_app(e)) {
m_parents.reserve(arg->get_id() + 1); m_parents.reserve(arg->get_id() + 1);
m_parents[arg->get_id()].push_back(e); m_parents[arg->get_id()].push_back(e);
@ -425,7 +428,6 @@ namespace sls {
mk_literal(e); mk_literal(e);
register_term(e); register_term(e);
visit(e); visit(e);
m_todo.pop_back();
} }
else { else {
for (expr* arg : *to_app(e)) for (expr* arg : *to_app(e))
@ -433,9 +435,10 @@ namespace sls {
} }
} }
else { else {
expr_ref _e(e, m);
m_todo.pop_back();
register_term(e); register_term(e);
visit(e); visit(e);
m_todo.pop_back();
} }
} }
} }
@ -452,6 +455,8 @@ namespace sls {
m_repair_down.reserve(e->get_id() + 1); m_repair_down.reserve(e->get_id() + 1);
m_repair_up.reserve(e->get_id() + 1); m_repair_up.reserve(e->get_id() + 1);
if (!term(e->get_id()))
verbose_stream() << "no term " << mk_bounded_pp(e, m) << "\n";
SASSERT(e == term(e->get_id())); SASSERT(e == term(e->get_id()));
if (!m_repair_down.contains(e->get_id())) if (!m_repair_down.contains(e->get_id()))
m_repair_down.insert(e->get_id()); m_repair_down.insert(e->get_id());

2
src/ast/sls/sls_context.h
View file

@ -124,7 +124,7 @@ namespace sls {
void register_plugin(plugin* p); void register_plugin(plugin* p);
void init(); void init();
ptr_vector<expr> m_todo; expr_ref_vector m_todo;
void register_terms(expr* e); void register_terms(expr* e);
void register_term(expr* e); void register_term(expr* e);

12
src/test/sls_test.cpp
View file

@ -1,6 +1,6 @@
#include "ast/sls/bv_sls_eval.h" #include "ast/sls/sls_bv_eval.h"
#include "ast/sls/bv_sls_terms.h" #include "ast/sls/sls_bv_terms.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "ast/reg_decl_plugins.h" #include "ast/reg_decl_plugins.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
@ -57,8 +57,8 @@ namespace bv {
my_sat_solver_context solver; my_sat_solver_context solver;
sls::context ctx(m, solver); sls::context ctx(m, solver);
sls_terms terms(ctx); sls::bv_terms terms(ctx);
sls_eval ev(terms, ctx); sls::bv_eval ev(terms, ctx);
for (auto e : es) for (auto e : es)
ev.register_term(e); ev.register_term(e);
ev.init(); ev.init();
@ -176,8 +176,8 @@ namespace bv {
my_sat_solver_context solver; my_sat_solver_context solver;
sls::context ctx(m, solver); sls::context ctx(m, solver);
sls_terms terms(ctx); sls::bv_terms terms(ctx);
sls_eval ev(terms, ctx); sls::bv_eval ev(terms, ctx);
for (auto e : es) for (auto e : es)
ev.register_term(e); ev.register_term(e);
ev.init(); ev.init();