mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

bv updates

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-07-14 19:34:24 -07:00
parent 1cd95e9db4
commit 402fdf667d
7 changed files with 49 additions and 60 deletions
Download patch file Download diff file Expand all files Collapse all files

56
src/ast/sls/bv_sls_eval.cpp
View file

@ -38,7 +38,11 @@ namespace bv {
auto& v = wval(e);
for (unsigned i = 0; i < v.bw; ++i)
m_tmp.set(i, false);
v.set_repair(random_bool(), m_tmp);
v.set_repair(random_bool(), m_tmp);
}
if (bv.is_bv(e)) {
auto& v = wval(e);
v.bits().copy_to(v.nw, v.eval);
}
}
@ -89,11 +93,13 @@ namespace bv {
}
bool sls_eval::can_eval1(app* e) const {
expr* x, * y, * z;
expr* x, * y;
if (m.is_eq(e, x, y))
return m.is_bool(x) || bv.is_bv(x);
if (m.is_ite(e, x, y, z))
return m.is_bool(y) || bv.is_bv(y);
return bv.is_bv(x);
if (m.is_ite(e))
return bv.is_bv(e);
if (m.is_distinct(e))
return bv.is_bv(e->get_arg(0));
if (e->get_family_id() == bv.get_fid()) {
switch (e->get_decl_kind()) {
case OP_BNEG_OVFL:
@ -107,10 +113,8 @@ namespace bv {
return true;
}
}
if (e->get_family_id() == basic_family_id)
return true;
if (is_uninterp_const(e))
return m.is_bool(e) || bv.is_bv(e);
return bv.is_bv(e);
return false;
}
@ -1843,7 +1847,19 @@ namespace bv {
}
bool sls_eval::repair_up(expr* e) {
if (!bv.is_bv(e) || !is_app(e))
if (!is_app(e) || !can_eval1(to_app(e)))
return false;
if (m.is_bool(e)) {
bool b = bval1(to_app(e));
auto v = ctx.atom2bool_var(e);
if (v == sat::null_bool_var)
ctx.set_value(e, b ? m.mk_true() : m.mk_false());
else if (ctx.is_true(v) != b)
ctx.flip(v);
return true;
}
if (!bv.is_bv(e))
return false;
auto& v = eval(to_app(e));
for (unsigned i = 0; i < v.nw; ++i) {
@ -1863,18 +1879,11 @@ namespace bv {
return *m_values[e->get_id()];
}
void sls_eval::init_eval(app* t) {
if (bv.is_bv(t)) {
auto& v = wval(t);
v.bits().copy_to(v.nw, v.eval);
}
}
void sls_eval::commit_eval(app* e) {
if (!bv.is_bv(e))
return;
VERIFY(wval(e).commit_eval());
// todo: if e is shared, then ctx.set_value().
VERIFY(wval(e).commit_eval());
}
void sls_eval::set_random(app* e) {
@ -1895,19 +1904,6 @@ namespace bv {
return false;
}
bool sls_eval::re_eval_is_correct(app* e) {
if (!can_eval1(e))
return false;
if (m.is_bool(e))
return bval0(e) ==bval1(e);
if (bv.is_bv(e)) {
auto const& v = eval(e);
return v.eval == v.bits();
}
UNREACHABLE();
return false;
}
expr_ref sls_eval::get_value(app* e) {
if (m.is_bool(e))
return expr_ref(m.mk_bool_val(bval0(e)), m);

7
src/ast/sls/bv_sls_eval.h
View file

@ -61,7 +61,6 @@ namespace bv {
void add_bit_vector(app* e);
sls_valuation* alloc_valuation(app* e);
//bool bval1_basic(app* e) const;
bool bval1_bv(app* e) const;
void fold_oper(bvect& out, app* e, unsigned i, std::function<void(bvect&, bvval const&)> const& f);
@ -137,8 +136,6 @@ namespace bv {
public:
sls_eval(sls_terms& terms, sls::context& ctx);
// void init_eval(std::function<bool(expr*, unsigned)> const& eval);
void tighten_range() { m_fix.init(); }
void register_term(expr* e);
@ -157,14 +154,10 @@ namespace bv {
void commit_eval(app* e);
void init_eval(app* e);
void set_random(app* e);
bool eval_is_correct(app* e);
bool re_eval_is_correct(app* e);
expr_ref get_value(app* e);
bool bval1(app* e) const;

18
src/ast/sls/bv_sls_fixed.cpp
View file

@ -31,17 +31,15 @@ namespace bv {
for (auto e : ctx.subterms())
set_fixed(e);
for (auto const& c : ctx.clauses()) {
if (c.m_clause.size() == 1) {
auto lit = c.m_clause[0];
auto a = ctx.atom(lit.var());
if (!a)
continue;
if (is_app(a))
init_range(to_app(a), lit.sign());
ev.m_fixed.setx(a->get_id(), true, false);
}
for (auto lit : ctx.unit_literals()) {
auto a = ctx.atom(lit.var());
if (!a)
continue;
if (is_app(a))
init_range(to_app(a), lit.sign());
ev.m_fixed.setx(a->get_id(), true, false);
}
for (auto e : ctx.subterms())
propagate_range_up(e);
}

2
src/ast/sls/sls_arith_base.cpp
View file

@ -554,7 +554,7 @@ namespace sls {
add_args(ineq, y, num_t(-1));
init_ineq(bv, ineq);
}
else if (m.is_distinct(e) && a.is_int_real(e->get_arg(0))) {
else if (m.is_distinct(e) && a.is_int_real(to_app(e)->get_arg(0))) {
NOT_IMPLEMENTED_YET();
}
else if (a.is_is_int(e, x))

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

@ -29,6 +29,7 @@ namespace sls {
void bv_plugin::register_term(expr* e) {
m_terms.register_term(e);
m_eval.register_term(e);
}
expr_ref bv_plugin::get_value(expr* e) {
@ -59,7 +60,7 @@ namespace sls {
void bv_plugin::initialize() {
if (!m_initialized) {
// compute fixed ranges
m_eval.tighten_range();
m_initialized = true;
}
}
@ -92,8 +93,9 @@ namespace sls {
return;
rational val;
VERIFY(bv.is_numeral(v, val));
NOT_IMPLEMENTED_YET();
// set value of e to val,
auto& w = m_eval.eval(to_app(e));
w.set_value(w.eval, val);
w.commit_eval();
}
void bv_plugin::repair_down(app* e) {
@ -135,17 +137,14 @@ namespace sls {
}
void bv_plugin::repair_up(app* e) {
if (!bv.is_bv(e))
;
else if (m_eval.repair_up(e)) {
if (m_eval.repair_up(e)) {
if (!m_eval.eval_is_correct(e)) {
verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
}
SASSERT(m_eval.eval_is_correct(e));
for (auto p : ctx.parents(e))
ctx.new_value_eh(p);
ctx.new_value_eh(e);
}
else if (ctx.rand(10) != 0) {
else if (bv.is_bv(e)) {
IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e));
m_eval.set_random(e);
ctx.new_value_eh(e);
@ -163,5 +162,4 @@ namespace sls {
IF_VERBOSE(2, verbose_stream()
<< "(bvsls :restarts " << m_stats.m_restarts << ")\n");
}
}
}

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

@ -299,6 +299,7 @@ namespace sls {
m_relevant.reset();
m_visited.reset();
m_root_literals.reset();
m_unit_literals.reset();
for (auto const& clause : s.clauses()) {
bool has_relevant = false;
unsigned n = 0;
@ -317,6 +318,8 @@ namespace sls {
if (m_rand() % ++n == 0)
selected_lit = lit;
}
if (clause.m_clause.size() == 1)
m_unit_literals.push_back(clause.m_clause[0]);
if (!has_relevant && selected_lit != sat::null_literal) {
m_relevant.insert(m_atoms[selected_lit.var()]->get_id());
m_root_literals.push_back(selected_lit);

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

@ -94,7 +94,7 @@ namespace sls {
expr_ref_vector m_atoms;
unsigned_vector m_atom2bool_var;
vector<ptr_vector<expr>> m_parents;
sat::literal_vector m_root_literals;
sat::literal_vector m_root_literals, m_unit_literals;
random_gen m_rand;
bool m_initialized = false;
bool m_new_constraint = false;
@ -140,6 +140,7 @@ namespace sls {
unsigned rand() { return m_rand(); }
unsigned rand(unsigned n) { return m_rand(n); }
sat::literal_vector const& root_literals() const { return m_root_literals; }
sat::literal_vector const& unit_literals() const { return m_unit_literals; }
void reinit_relevant();