Skip to content

Commit

Permalink
rely on is_sat fallback for failed repair-up, add separate file for W…
Browse files Browse the repository at this point in the history 
…IP on lookahead.
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Dec 26, 2024
1 parent 13dcfd2 commit d3a6521
Show file tree
Hide file tree
Showing 7 changed files with 243 additions and 152 deletions.
1 change: 1 addition & 0 deletions src/ast/sls/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ z3_add_component(ast_sls
sls_bv_engine.cpp
sls_bv_eval.cpp
sls_bv_fixed.cpp
sls_bv_lookahead.cpp
sls_bv_plugin.cpp
sls_bv_terms.cpp
sls_bv_valuation.cpp
Expand Down
173 changes: 39 additions & 134 deletions src/ast/sls/sls_bv_eval.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ namespace sls {
m(ctx.get_manager()),
ctx(ctx),
terms(terms),
m_lookahead(*this),
bv(m),
m_fix(*this, terms, ctx)
{}
Expand Down Expand Up @@ -121,8 +122,8 @@ namespace sls {
SASSERT(m.is_bool(e));
SASSERT(e->get_family_id() == bv.get_fid());

bool use_current1 = use_current || (e->get_num_args() > 0 && !m_on_restore.is_marked(e->get_arg(0)));
bool use_current2 = use_current || (e->get_num_args() > 1 && !m_on_restore.is_marked(e->get_arg(1)));
bool use_current1 = use_current || (e->get_num_args() > 0 && !m_lookahead.on_restore(e->get_arg(0)));
bool use_current2 = use_current || (e->get_num_args() > 1 && !m_lookahead.on_restore(e->get_arg(1)));
auto ucompare = [&](std::function<bool(int)> const& f) {
auto& a = wval(e->get_arg(0));
auto& b = wval(e->get_arg(1));
Expand Down Expand Up @@ -211,8 +212,8 @@ namespace sls {
return bval1_bv(e, false);
expr* x, * y;
if (m.is_eq(e, x, y) && bv.is_bv(x)) {
bool use_current1 = !m_on_restore.is_marked(x);
bool use_current2 = !m_on_restore.is_marked(y);
bool use_current1 = !m_lookahead.on_restore(x);
bool use_current2 = !m_lookahead.on_restore(y);
return wval(x).tmp_bits(use_current1) == wval(y).tmp_bits(use_current2);
}
verbose_stream() << mk_bounded_pp(e, m) << "\n";
Expand Down Expand Up @@ -882,35 +883,8 @@ namespace sls {
}

bool bv_eval::try_repair_eq_lookahead(app* e) {
return false;
auto is_true = bval0(e);
if (!is_true)
return false;
auto const& uninterp = terms.uninterp_occurs(e);
if (uninterp.empty())
return false;
// for (auto e : uninterp)
// verbose_stream() << mk_bounded_pp(e, m) << " ";
// verbose_stream() << "\n";
return m_lookahead.try_repair_down(e);

expr* t = uninterp[m_rand() % uninterp.size()];

auto& v = wval(t);
if (v.set_random(m_rand)) {
//verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n";
ctx.new_value_eh(t);
return true;
}
return false;


for (auto e : uninterp) {
auto& v = wval(e);
v.get_variant(m_tmp, m_rand);
auto d = lookahead(e, m_tmp);
//verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n";
}
return false;
}

bool bv_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
Expand All @@ -936,13 +910,9 @@ namespace sls {
}
}
#endif
if (m_rand(20) != 0)
if (a.try_set(b.bits()))
return true;

if (m_rand(20) == 0)
return a.set_random(m_rand);
return false;
if (m_rand(20) != 0 && a.try_set(b.bits()))
return true;
return a.set_random(m_rand);
}
else {
bool try_above = m_rand(2) == 0;
Expand Down Expand Up @@ -1925,7 +1895,20 @@ namespace sls {
for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, ve.get(i + bw));
a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp);
bool r = a.try_set(m_tmp);
if (!r) {
a.add1(m_tmp);
r = a.try_set(m_tmp);
}
if (!r) {
r = a.set_repair(random_bool(), m_tmp);
}
if (!r) {
verbose_stream() << "repair concat " << mk_bounded_pp(e, m) << "\n";
verbose_stream() << idx << " " << a << "\n" << m_tmp << "\n";

}
return r;
}

//
Expand All @@ -1934,7 +1917,7 @@ namespace sls {
// set a outside of [hi:lo] to random values with preference to 0 or 1 bits
//
bool bv_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
// verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n";
// IF_VERBOSE(4, verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n");
if (false && m_rand(m_config.m_prob_randomize_extract) <= 100) {
a.get_variant(m_tmp, m_rand);
if (0 == (m_rand(2))) {
Expand All @@ -1953,13 +1936,11 @@ namespace sls {
for (unsigned i = 0; i < e.bw; ++i)
m_tmp.set(i + lo, e.get(i));
m_tmp.set_bw(a.bw);
// verbose_stream() << a << " := " << m_tmp << "\n";
if (m_rand(20) != 0 && a.try_set(m_tmp))
//verbose_stream() << a << " := " << m_tmp << "\n";
if (a.try_set(m_tmp))
return true;
if (m_rand(20) != 0)
return false;
bool ok = a.set_random(m_rand);
// verbose_stream() << "set random " << ok << " " << a << "\n";
//verbose_stream() << "set random " << ok << " " << a << "\n";
return ok;
}

Expand Down Expand Up @@ -1994,6 +1975,7 @@ namespace sls {
bool bv_eval::repair_up(expr* 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);
Expand All @@ -2006,29 +1988,20 @@ namespace sls {

if (!bv.is_bv(e))
return false;
auto& v = eval(to_app(e));

for (unsigned i = 0; i < v.nw; ++i) {
if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
//verbose_stream() << "Fail to set " << mk_bounded_pp(e, m) << " " << i << " " << v.fixed[i] << " " << v.bits()[i] << " " << v.eval[i] << "\n";
v.bits().copy_to(v.nw, v.eval);
auto& v = eval(to_app(e));
if (v.eval == v.bits())
return true;

for (unsigned i = 0; i < v.nw; ++i)
if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i])))
return false;
}
}

if (v.eval == v.bits())
return true;
//verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
if (v.commit_eval()) {
ctx.new_value_eh(e);
return true;
}
//verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
//for (expr* arg : *to_app(e))
// verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n";
v.bits().copy_to(v.nw, v.eval);
return false;
if (!v.commit_eval())
return false;

ctx.new_value_eh(e);
return true;
}

sls::bv_valuation& bv_eval::wval(expr* e) const {
Expand Down Expand Up @@ -2097,73 +2070,5 @@ namespace sls {
return out << "?";
}

double bv_eval::lookahead(expr* e, bvect const& new_value) {
SASSERT(bv.is_bv(e));
SASSERT(is_uninterp(e));
SASSERT(m_restore.empty());

bool has_tabu = false;
double break_count = 0, make_count = 0;

wval(e).eval = new_value;
if (!insert_update(e)) {
restore_lookahead();
return -1000000;
}
insert_update_stack(e);
unsigned max_depth = get_depth(e);
for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
for (unsigned i = 0; !has_tabu && i < m_update_stack[depth].size(); ++i) {
e = m_update_stack[depth][i];
if (bv.is_bv(e)) {
auto& v = eval(to_app(e));
if (insert_update(e)) {
for (auto p : ctx.parents(e)) {
insert_update_stack(p);
max_depth = std::max(max_depth, get_depth(p));
}
}
else
has_tabu = true;
}
else if (m.is_bool(e) && can_eval1(to_app(e))) {
bool is_true = ctx.is_true(e);
bool is_true_new = bval1(to_app(e));
bool is_true_old = bval1_tmp(to_app(e));
// verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n";
if (is_true == is_true_new && is_true_new != is_true_old)
++make_count;
if (is_true == is_true_old && is_true_new != is_true_old)
++break_count;
}
}
m_update_stack[depth].reset();
}
restore_lookahead();
if (has_tabu)
return -10000;
return make_count - break_count;
}

bool bv_eval::insert_update(expr* e) {
m_restore.push_back(e);
m_on_restore.mark(e);
auto& v = wval(e);
v.save_value();
return v.commit_eval();
}

void bv_eval::insert_update_stack(expr* e) {
unsigned depth = get_depth(e);
m_update_stack.reserve(depth + 1);
if (!m_update_stack[depth].contains(e))
m_update_stack[depth].push_back(e);
}

void bv_eval::restore_lookahead() {
for (auto e : m_restore)
wval(e).restore_value();
m_restore.reset();
m_on_restore.reset();
}

}
12 changes: 5 additions & 7 deletions src/ast/sls/sls_bv_eval.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,10 @@ Module Name:
#include "ast/sls/sls_bv_valuation.h"
#include "ast/sls/sls_bv_fixed.h"
#include "ast/sls/sls_context.h"
#include "ast/sls/sls_bv_lookahead.h"
#include "ast/bv_decl_plugin.h"



namespace sls {

Expand All @@ -31,6 +33,8 @@ namespace sls {
using bvect = sls::bvect;

class bv_eval {
friend class bv_lookahead;

struct config {
unsigned m_prob_randomize_extract = 50;
};
Expand All @@ -40,6 +44,7 @@ namespace sls {
ast_manager& m;
sls::context& ctx;
sls::bv_terms& terms;
sls::bv_lookahead m_lookahead;
bv_util bv;
sls::bv_fixed m_fix;
mutable mpn_manager mpn;
Expand All @@ -58,13 +63,6 @@ namespace sls {

void init_eval_bv(app* e);

ptr_vector<expr> m_restore;
vector<ptr_vector<expr>> m_update_stack;
expr_mark m_on_restore;
void insert_update_stack(expr* e);
bool insert_update(expr* e);
double lookahead(expr* e, bvect const& new_value);
void restore_lookahead();

/**
* Register e as a bit-vector.
Expand Down
Loading

0 comments on commit d3a6521

Please sign in to comment.