mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

add py_value to selected classes in python bindings, add mode for input-assertion based lookahead solving

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-04 13:40:49 -08:00
parent 7e4681d836
commit 05f166f736
18 changed files with 374 additions and 184 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_parsers.cpp
View file

@ -263,7 +263,7 @@ extern "C" {
if (ous.str().empty()) ous << e.what();
SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
}
Z3_CATCH_CORE();
Z3_CATCH_CORE({});
RETURN_Z3(mk_c(c)->mk_external_string(std::move(ous).str()));
}
}

20
src/api/python/z3/z3.py
View file

@ -447,6 +447,10 @@ class AstRef(Z3PPObject):
"""
return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
def py_value(self):
"""Return a Python value that is equivalent to `self`."""
return None
def is_ast(a):
"""Return `True` if `a` is an AST node.
@ -1611,6 +1615,13 @@ class BoolRef(ExprRef):
def __invert__(self):
return Not(self)
def py_value(self):
if is_true(self):
return True
if is_false(self):
return False
return None
@ -3045,6 +3056,9 @@ class IntNumRef(ArithRef):
"""
return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
def py_value(self):
return Z3_get_numeral_double(self.ctx_ref(), self.as_ast())
class RatNumRef(ArithRef):
"""Rational values."""
@ -3142,6 +3156,9 @@ class RatNumRef(ArithRef):
"""
return Fraction(self.numerator_as_long(), self.denominator_as_long())
def py_value(self):
return Z3_get_numeral_double(self.ctx_ref(), self.as_ast())
class AlgebraicNumRef(ArithRef):
"""Algebraic irrational values."""
@ -11005,6 +11022,9 @@ class SeqRef(ExprRef):
return string_at(chars, size=string_length.value).decode("latin-1")
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
def py_value(self):
return self.as_string()
def __le__(self, other):
return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)

10
src/ast/ast.h
View file

@ -150,7 +150,7 @@ public:
~parameter();
parameter& operator=(parameter && other) {
parameter& operator=(parameter && other) noexcept {
std::swap(other.m_val, m_val);
return *this;
}
@ -460,7 +460,7 @@ class ast {
protected:
friend class ast_manager;
unsigned m_id;
unsigned m_id = UINT_MAX;
unsigned m_kind:16;
// Warning: the marks should be used carefully, since they are shared.
unsigned m_mark1:1;
@ -479,8 +479,8 @@ protected:
void mark_so(bool flag) { m_mark_shared_occs = flag; }
void reset_mark_so() { m_mark_shared_occs = false; }
bool is_marked_so() const { return m_mark_shared_occs; }
unsigned m_ref_count;
unsigned m_hash;
unsigned m_ref_count = 0;
unsigned m_hash = 0;
#ifdef Z3DEBUG
// In debug mode, we store who is the owner of the mark.
void * m_mark1_owner;
@ -497,7 +497,7 @@ protected:
--m_ref_count;
}
ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) {
ast(ast_kind k): m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false) {
DEBUG_CODE({
m_mark1_owner = 0;
m_mark2_owner = 0;

2
src/ast/datatype_decl_plugin.h
View file

@ -81,7 +81,7 @@ namespace datatype {
symbol m_name;
symbol m_recognizer;
ptr_vector<accessor> m_accessors;
def* m_def;
def* m_def = nullptr;
public:
constructor(symbol n, symbol const& r): m_name(n), m_recognizer(r) {}
~constructor();

8
src/ast/sls/sls_array_plugin.cpp
View file

@ -111,7 +111,7 @@ namespace sls {
return;
if (are_distinct(nsel, nmap)) {
expr_ref eq(m.mk_eq(nmap->get_expr(), nsel->get_expr()), m);
ctx.add_clause(eq);
ctx.add_theory_axiom(eq);
}
else {
g.merge(nmap, nsel, nullptr);
@ -192,7 +192,7 @@ namespace sls {
auto nsel = mk_select(g, cn, sel);
if (are_distinct(nsel, sel)) {
expr_ref eq(m.mk_eq(val->get_expr(), nsel->get_expr()), m);
ctx.add_clause(eq);
ctx.add_theory_axiom(eq);
}
else {
g.merge(nsel, sel, nullptr);
@ -227,7 +227,7 @@ namespace sls {
expr_ref sel(a.mk_select(args), m);
expr_ref eq(m.mk_eq(sel, to_app(sto)->get_arg(sto->get_num_args() - 1)), m);
IF_VERBOSE(3, verbose_stream() << "add store axiom 1 " << mk_bounded_pp(sto, m) << "\n");
ctx.add_clause(eq);
ctx.add_theory_axiom(eq);
}
void array_plugin::add_store_axiom2(app* sto, app* sel) {
@ -248,7 +248,7 @@ namespace sls {
for (unsigned i = 1; i < sel->get_num_args() - 1; ++i)
ors.push_back(m.mk_eq(sel->get_arg(i), sto->get_arg(i)));
IF_VERBOSE(3, verbose_stream() << "add store axiom 2 " << mk_bounded_pp(sto, m) << " " << mk_bounded_pp(sel, m) << "\n");
ctx.add_clause(m.mk_or(ors));
ctx.add_theory_axiom(m.mk_or(ors));
}
void array_plugin::init_egraph(euf::egraph& g) {

8
src/ast/sls/sls_basic_plugin.cpp
View file

@ -47,13 +47,13 @@ namespace sls {
auto eq_th = expr_ref(m.mk_eq(e, th), m);
auto eq_el = expr_ref(m.mk_eq(e, el), m);
ctx.add_clause(m.mk_or(mk_not(m, c), eq_th));
ctx.add_clause(m.mk_or(c, eq_el));
ctx.add_theory_axiom(m.mk_or(mk_not(m, c), eq_th));
ctx.add_theory_axiom(m.mk_or(c, eq_el));
#if 0
auto eq_th_el = expr_ref(m.mk_eq(th, el), m);
verbose_stream() << mk_bounded_pp(eq_th_el, m) << "\n";
ctx.add_clause(m.mk_or(eq_th_el, c, m.mk_not(eq_th)));
ctx.add_clause(m.mk_or(eq_th_el, m.mk_not(c), m.mk_not(eq_el)));
ctx.add_theory_axiom(m.mk_or(eq_th_el, c, m.mk_not(eq_th)));
ctx.add_theory_axiom(m.mk_or(eq_th_el, m.mk_not(c), m.mk_not(eq_el)));
#endif
}
}

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

@ -97,8 +97,11 @@ namespace sls {
eval(e).commit_eval_check_tabu();
}
bool bv_eval::can_eval1(app* e) const {
bool bv_eval::can_eval1(expr* t) const {
expr* x, * y;
if (!is_app(t))
return false;
app* e = to_app(t);
if (m.is_eq(e, x, y))
return bv.is_bv(x);
if (m.is_ite(e))
@ -197,27 +200,35 @@ namespace sls {
}
void bv_eval::set_bool_value(expr* e, bool val) {
m_tmp_bool_values.setx(e->get_id(), to_lbool(val), l_undef);
m_tmp_bool_value_indices.push_back(e->get_id());
auto id = e->get_id();
auto old_val = m_tmp_bool_values.get(id, l_undef);
m_tmp_bool_values.setx(id, to_lbool(val), l_undef);
m_tmp_bool_value_updates.push_back({ id, old_val });
}
bool bv_eval::get_bool_value(expr* e) const {
auto val = m_tmp_bool_values.get(e->get_id(), l_undef);
SASSERT(m.is_bool(e));
auto id = e->get_id();
auto val = m_tmp_bool_values.get(id, l_undef);
if (val != l_undef)
return val == l_true;
return val == l_true;
bool b;
auto v = ctx.atom2bool_var(e);
if (v != sat::null_bool_var)
return ctx.is_true(v);
auto b = bval1_bool(to_app(e));
m_tmp_bool_values.setx(e->get_id(), to_lbool(val), l_undef);
m_tmp_bool_value_indices.push_back(e->get_id());
b = ctx.is_true(v);
else
b = bval1(e);
m_tmp_bool_values.setx(id, to_lbool(b), l_undef);
m_tmp_bool_value_updates.push_back({ id, l_undef });
return b;
}
void bv_eval::clear_bool_values() {
for (auto i : m_tmp_bool_value_indices)
m_tmp_bool_values[i] = l_undef;
m_tmp_bool_value_indices.reset();
void bv_eval::restore_bool_values(unsigned r) {
for (auto i = m_tmp_bool_value_updates.size(); i-- > r; ) {
auto& [id, val] = m_tmp_bool_value_updates[i];
m_tmp_bool_values.set(id, val);
}
m_tmp_bool_value_updates.shrink(r);
}
bool bv_eval::bval1_bool(app* e) const {
@ -261,23 +272,18 @@ namespace sls {
return false;
}
bool bv_eval::bval1(app* e) const {
bool bv_eval::bval1(expr* t) const {
app* e = to_app(t);
if (e->get_family_id() == bv.get_fid())
return bval1_bv(e);
expr* x, * y;
if (m.is_eq(e, x, y) && bv.is_bv(x)) {
return wval(x).bits() == wval(y).bits();
}
if (m.is_eq(e, x, y) && bv.is_bv(x))
return wval(x).bits() == wval(y).bits();
if (e->get_family_id() == basic_family_id)
return bval1_bool(e);
verbose_stream() << mk_bounded_pp(e, m) << "\n";
UNREACHABLE();
return false;
return ctx.is_true(e);
}
// unsigned ddt_orig(expr* e);
sls::bv_valuation& bv_eval::eval(app* e) const {
SASSERT(m_values.size() > e->get_id());
SASSERT(m_values[e->get_id()]);
@ -290,7 +296,8 @@ namespace sls {
m_values[e->get_id()]->set(val.bits());
}
void bv_eval::eval(app* e, sls::bv_valuation& val) const {
void bv_eval::eval(expr* t, sls::bv_valuation& val) const {
app* e = to_app(t);
SASSERT(bv.is_bv(e));
if (m.is_ite(e)) {
SASSERT(bv.is_bv(e->get_arg(1)));
@ -2056,11 +2063,11 @@ namespace sls {
}
bool bv_eval::repair_up(expr* e) {
if (!is_app(e) || !can_eval1(to_app(e)))
if (!can_eval1(e))
return false;
if (m.is_bool(e)) {
bool b = bval1(to_app(e));
bool b = bval1(e);
auto v = ctx.atom2bool_var(e);
if (v == sat::null_bool_var)
ctx.set_value(e, b ? m.mk_true() : m.mk_false());

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

@ -55,7 +55,7 @@ namespace sls {
unsigned m_lookahead_steps = 0;
unsigned m_lookahead_phase_size = 10;
mutable svector<lbool> m_tmp_bool_values;
mutable unsigned_vector m_tmp_bool_value_indices;
mutable svector<std::pair<unsigned, lbool>> m_tmp_bool_value_updates;
scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation
@ -141,7 +141,7 @@ namespace sls {
sls::bv_valuation& wval(app* e, unsigned i) { return wval(e->get_arg(i)); }
void eval(app* e, sls::bv_valuation& val) const;
void eval(expr* e, sls::bv_valuation& val) const;
bvect const& assign_value(app* e) const { return wval(e).bits(); }
@ -150,7 +150,7 @@ namespace sls {
* Retrieve evaluation based on immediate children.
*/
bool can_eval1(app* e) const;
bool can_eval1(expr* e) const;
void commit_eval(expr* p, app* e);
@ -188,11 +188,13 @@ namespace sls {
expr_ref get_value(app* e);
bool bval0(expr* e) const { return ctx.is_true(e); }
bool bval1(app* e) const;
bool bval1(expr* e) const;
unsigned bool_value_restore_point() const { return m_tmp_bool_value_updates.size(); }
void set_bool_value(expr* e, bool val);
void clear_bool_values();
bool get_bool_value(expr* e)const;
void restore_bool_values(unsigned restore_point);
void commit_bool_values() { m_tmp_bool_value_updates.reset(); }
bool get_bool_value(expr* e) const;
/*
* Try to invert value of child to repair value assignment of parent.

313
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -38,7 +38,6 @@ namespace sls {
* before any other propagation with the main BV solver.
*/
void bv_lookahead::start_propagation() {
//verbose_stream() << "start_propagation " << m_stats.m_num_propagations << "\n";
if (m_stats.m_propagations++ % m_config.propagation_base == 0)
search();
}
@ -53,6 +52,7 @@ namespace sls {
void bv_lookahead::search() {
updt_params(ctx.get_params());
initialize_bool_values();
rescore();
m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
TRACE("bv", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";);
@ -65,8 +65,10 @@ namespace sls {
// get candidate variables
auto& vars = get_candidate_uninterp();
if (vars.empty())
return;
if (vars.empty()) {
finalize_bool_values();
return;
}
// random walk
if (ctx.rand(2047) < m_config.wp && apply_random_move(vars))
@ -83,6 +85,36 @@ namespace sls {
m_config.max_moves_base += 100;
}
void bv_lookahead::initialize_bool_values() {
for (auto t : ctx.subterms()) {
if (bv.is_bv(t)) {
auto& v = m_ev.eval(to_app(t));
v.commit_eval_ignore_tabu();
}
else if (m.is_bool(t)) {
auto b = m_ev.bval1(t);
m_ev.set_bool_value(t, b);
}
}
m_ev.commit_bool_values();
}
/**
* Flip truth values of root literals if they are updated.
*/
void bv_lookahead::finalize_bool_values() {
if (false && !m_config.use_top_level_assertions)
return;
for (auto lit : ctx.root_literals()) {
auto a = ctx.atom(lit.var());
auto v0 = ctx.is_true(lit.var());
auto v1 = m_ev.get_bool_value(a);
if (v0 != v1)
ctx.flip(lit.var());
}
}
/**
* guided move: apply lookahead search for the selected variables
* and possible moves
@ -106,11 +138,14 @@ namespace sls {
return false;
expr* e = vars[ctx.rand(vars.size())];
if (m.is_bool(e)) {
auto v = ctx.atom2bool_var(e);
if (ctx.is_unit(v))
return false ;
TRACE("bv", tout << "random flip " << mk_bounded_pp(e, m) << "\n";);
ctx.flip(v);
if (is_root(e))
return false;
m_ev.set_bool_value(e, !m_ev.get_bool_value(e));
if (!m_config.use_top_level_assertions) {
auto v = ctx.atom2bool_var(e);
TRACE("bv", tout << "random flip " << mk_bounded_pp(e, m) << "\n";);
ctx.flip(v);
}
return true;
}
SASSERT(bv.is_bv(e));
@ -121,6 +156,7 @@ namespace sls {
return apply_update(m_last_atom, e, m_v_updated, move_type::random_t);
}
/**
* random move: select a variable at random and use one of the moves: flip, add1, sub1
*/
@ -129,11 +165,16 @@ namespace sls {
return false;
expr* e = vars[ctx.rand(vars.size())];
if (m.is_bool(e)) {
TRACE("bv", tout << "random move flip " << mk_bounded_pp(e, m) << "\n";);
auto v = ctx.atom2bool_var(e);
if (ctx.is_unit(v))
if (is_root(e))
return false;
ctx.flip(v);
m_ev.set_bool_value(e, !m_ev.get_bool_value(e));
if (!m_config.use_top_level_assertions) {
TRACE("bv", tout << "random move flip " << mk_bounded_pp(e, m) << "\n";);
auto v = ctx.atom2bool_var(e);
if (ctx.is_unit(v))
return false;
ctx.flip(v);
}
return true;
}
SASSERT(bv.is_bv(e));
@ -162,13 +203,17 @@ namespace sls {
* those with high score, but back off if they are frequently chosen.
*/
ptr_vector<expr> const& bv_lookahead::get_candidate_uninterp() {
app* e = nullptr;
expr* e = nullptr;
if (m_config.ucb) {
double max = -1.0;
for (auto lit : ctx.root_literals()) {
if (!is_false_bv_literal(lit))
for (auto a : get_root_assertions()) {
auto const& vars = m_ev.terms.uninterp_occurs(a);
//verbose_stream() << mk_bounded_pp(a, m) << " " << assertion_is_true(a) << " num vars " << vars.size() << "\n";
if (assertion_is_true(a))
continue;
if (vars.empty())
continue;
auto a = to_app(ctx.atom(lit.var()));
auto score = old_score(a);
auto q = score
+ m_config.ucb_constant * sqrt(log((double)m_touched) / get_touched(a))
@ -183,9 +228,9 @@ namespace sls {
}
else {
unsigned n = 0;
for (auto lit : ctx.root_literals())
if (is_false_bv_literal(lit) && ctx.rand() % ++n == 0)
e = to_app(ctx.atom(lit.var()));
for (auto a : get_root_assertions())
if (!assertion_is_true(a) && !m_ev.terms.uninterp_occurs(e).empty() && ctx.rand() % ++n == 0)
e = a;
}
CTRACE("bv", !e, ; display_weights(ctx.display(tout << "no candidate\n")););
@ -228,12 +273,10 @@ namespace sls {
* Reset variables that occur in false literals.
*/
void bv_lookahead::reset_uninterp_in_false_literals() {
auto const& lits = ctx.root_literals();
expr_mark marked;
for (auto lit : ctx.root_literals()) {
if (!is_false_bv_literal(lit))
for (auto a : get_root_assertions()) {
if (assertion_is_true(a))
continue;
app* a = to_app(ctx.atom(lit.var()));
auto const& occs = m_ev.terms.uninterp_occurs(a);
for (auto e : occs) {
if (!bv.is_bv(e))
@ -259,13 +302,11 @@ namespace sls {
return m_ev.can_eval1(a);
}
bool bv_lookahead::is_false_bv_literal(sat::literal lit) {
if (!is_bv_literal(lit))
return false;
app* a = to_app(ctx.atom(lit.var()));
return m_ev.bval0(a) != m_ev.bval1(a);
bool bv_lookahead::assertion_is_true(expr* a) {
if (m_config.use_top_level_assertions)
return m_ev.get_bool_value(a);
return !m_ev.can_eval1(a) || m_ev.bval0(a) == m_ev.bval1(a);
}
void bv_lookahead::updt_params(params_ref const& _p) {
sls_params p(_p);
@ -286,6 +327,7 @@ namespace sls {
m_config.ucb_forget = p.walksat_ucb_forget();
m_config.ucb_init = p.walksat_ucb_init();
m_config.ucb_noise = p.walksat_ucb_noise();
m_config.use_top_level_assertions = p.use_top_level_assertions_bv();
}
/**
@ -294,12 +336,40 @@ namespace sls {
* based on hamming distance for equalities, and differences
* for inequalities.
*/
double bv_lookahead::new_score(app* a) {
bool is_true = m_ev.get_bool_value(a);
bool is_true_new = m_ev.bval1(a);
double bv_lookahead::new_score(expr* a) {
if (m_config.use_top_level_assertions)
return new_score(a, true);
else
return new_score(a, m_ev.bval0(a));
}
double bv_lookahead::new_score(expr* a, bool is_true) {
bool is_true_new = m_ev.get_bool_value(a);
//verbose_stream() << "compute score " << mk_bounded_pp(a, m) << " is-true " << is_true << " is-true-new " << is_true_new << "\n";
if (is_true == is_true_new)
return 1;
expr* x, * y;
if (m.is_not(a, x))
return new_score(x, !is_true);
if ((m.is_and(a) && is_true) || (m.is_or(a) && !is_true)) {
double score = 1;
for (auto arg : *to_app(a))
score = std::min(score, new_score(arg, is_true));
return score;
}
if ((m.is_and(a) && !is_true) || (m.is_or(a) && is_true)) {
double score = 0;
for (auto arg : *to_app(a))
score = std::max(score, new_score(arg, is_true));
return score;
}
if (m.is_iff(a, x, y)) {
auto v0 = m_ev.get_bool_value(x);
auto v1 = m_ev.get_bool_value(y);
return (is_true == (v0 == v1)) ? 1 : 0;
}
if (is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
auto const& vx = wval(x);
auto const& vy = wval(y);
@ -359,13 +429,13 @@ namespace sls {
double dbl = n.get_double();
return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
}
else if (is_true && m.is_distinct(a) && bv.is_bv(a->get_arg(0))) {
else if (is_true && m.is_distinct(a) && bv.is_bv(to_app(a)->get_arg(0))) {
double np = 0, nd = 0;
for (unsigned i = 0; i < a->get_num_args(); ++i) {
auto const& vi = wval(a->get_arg(i));
for (unsigned j = i + 1; j < a->get_num_args(); ++j) {
for (unsigned i = 0; i < to_app(a)->get_num_args(); ++i) {
auto const& vi = wval(to_app(a)->get_arg(i));
for (unsigned j = i + 1; j < to_app(a)->get_num_args(); ++j) {
++np;
auto const& vj = wval(a->get_arg(j));
auto const& vj = wval(to_app(a)->get_arg(j));
if (vi.bits() != vj.bits())
nd++;
}
@ -403,31 +473,35 @@ namespace sls {
m_ev.set_bool_value(t, !m_ev.bval0(t));
}
TRACE("bv_verbose", tout << "lookahead update " << mk_bounded_pp(t, m) << " := " << new_value << "\n";);
insert_update_stack(t);
unsigned restore_point = m_ev.bool_value_restore_point();
unsigned max_depth = get_depth(t);
for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto a = m_update_stack[depth][i];
TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " " << depth << " " << i << "\n";);
TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " depth: " << depth << "\n";);
for (auto p : ctx.parents(a)) {
insert_update_stack(p);
max_depth = std::max(max_depth, get_depth(p));
}
if (is_root(a))
score += get_weight(a) * (new_score(a) - old_score(a));
if (a == t)
continue;
else if (bv.is_bv(a))
m_ev.eval(a);
insert_update(a);
if (t != a) {
if (bv.is_bv(a))
m_ev.eval(a);
insert_update(a);
}
if (is_root(a)) {
TRACE("bv_verbose", tout << "scores " << mk_bounded_pp(a, m) << " old: " << old_score(a) << " new: " << new_score(a) << "\n";);
score += get_weight(a) * (new_score(a) - old_score(a));
}
}
m_update_stack[depth].reset();
}
m_in_update_stack.reset();
restore_lookahead();
m_ev.clear_bool_values();
m_ev.restore_bool_values(restore_point);
TRACE("sls_verbose", tout << mk_bounded_pp(t, m) << " := " << new_value << " score: " << m_top_score << "\n");
@ -481,7 +555,7 @@ namespace sls {
m_v_saved.copy_to(v.nw, m_v_updated);
// flip a single bit
for (unsigned i = 0; i < v.bw && i <= 32; ++i) {
for (unsigned i = 0; i < v.bw && i < 32 ; ++i) {
m_v_updated.set(i, !m_v_updated.get(i));
try_set(u, m_v_updated);
m_v_updated.set(i, !m_v_updated.get(i));
@ -543,6 +617,7 @@ namespace sls {
insert_update_stack(t);
unsigned max_depth = get_depth(t);
unsigned restore_point = m_ev.bool_value_restore_point();
for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto e = m_update_stack[depth][i];
@ -558,49 +633,43 @@ namespace sls {
wval(e).commit_eval_ignore_tabu();
}
else if (m.is_bool(e)) {
auto v = ctx.atom2bool_var(e);
auto v1 = m_ev.bval1(to_app(e));
if (v != sat::null_bool_var) {
if (ctx.is_unit(v))
continue;
if (ctx.is_true(v) == v1)
continue;
auto v1 = m_ev.bval1(e);
if (m_config.use_top_level_assertions) {
if (m_ev.get_bool_value(e) == v1)
continue;
}
else {
if (e == p)
continue;
TRACE("bv", tout << "updated truth value " << v << ": " << mk_bounded_pp(e, m) << "\n";);
unsigned num_unsat = ctx.unsat().size();
#if 0
TRACE("bv", tout << "update flip " << mk_bounded_pp(e, m) << "\n";);
auto r = ctx.reward(v);
auto lit = sat::literal(v, !ctx.is_true(v));
bool is_bv_lit = is_bv_literal(lit);
sat::bool_var_set rotated;
unsigned budget = 100;
bool rot = ctx.try_rotate(v, rotated, budget);
verbose_stream() << "try-rotate " << rot << " " << rotated.size() << "\n";
verbose_stream() << "flip " << ((!p || e == p) ? "top " : "not top ") << is_bv_literal(lit) << " " << mk_bounded_pp(e, m) << " " << lit << " " << r << " num unsat " << num_unsat << " -> " << ctx.unsat().size() << "\n";
verbose_stream() << "new unsat " << ctx.unsat().size() << "\n";
#endif
auto v = ctx.atom2bool_var(e);
if (v != sat::null_bool_var) {
if (ctx.is_unit(v))
continue;
if (ctx.is_true(e) == v1)
continue;
TRACE("bv", tout << "updated truth value " << v << ": " << mk_bounded_pp(e, m) << "\n";);
unsigned num_unsat = ctx.unsat().size();
#if 1
if (allow_costly_flips(mt))
ctx.flip(v);
else if (true) {
sat::bool_var_set rotated;
unsigned budget = 100;
bool rot = ctx.try_rotate(v, rotated, budget);
if (rot)
++m_stats.m_rotations;
(void)rot;
TRACE("bv", tout << "rotate " << v << " " << rot << " " << rotated << "\n";);
//verbose_stream() << "rotate " << v << " " << rot << " " << rotated << "\n";
}
if (allow_costly_flips(mt))
ctx.flip(v);
else if (true) {
sat::bool_var_set rotated;
unsigned budget = 100;
bool rot = ctx.try_rotate(v, rotated, budget);
if (rot)
++m_stats.m_rotations;
TRACE("bv", tout << "rotate " << v << " " << rot << " " << rotated << "\n";);
}
#endif
}
}
m_ev.set_bool_value(to_app(e), v1);
}
@ -615,7 +684,10 @@ namespace sls {
m_update_stack[depth].reset();
}
m_in_update_stack.reset();
m_ev.clear_bool_values();
if (m_config.use_top_level_assertions)
m_ev.commit_bool_values();
else
m_ev.restore_bool_values(restore_point);
TRACE("bv", tout << mt << " " << mk_bounded_pp(t, m)
<< " := " << new_value
<< " score " << m_top_score << "\n";);
@ -631,7 +703,6 @@ namespace sls {
}
void bv_lookahead::insert_update(expr* e) {
TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << "\n");
if (bv.is_bv(e)) {
auto& v = wval(e);
@ -669,7 +740,8 @@ namespace sls {
}
bv_lookahead::bool_info& bv_lookahead::get_bool_info(expr* e) {
return m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0, 1});
m_bool_info.reserve(e->get_id() + 1, { m_config.paws_init, 0, 1 });
return m_bool_info[e->get_id()];
}
void bv_lookahead::dec_weight(expr* e) {
@ -680,29 +752,24 @@ namespace sls {
void bv_lookahead::rescore() {
m_top_score = 0;
m_is_root.reset();
for (auto lit : ctx.root_literals()) {
if (!is_bv_literal(lit))
continue;
auto a = to_app(ctx.atom(lit.var()));
for (auto a : get_root_assertions()) {
m_is_root.mark(a);
double score = new_score(a);
set_score(a, score);
m_top_score += score;
m_is_root.mark(a);
//verbose_stream() << mk_bounded_pp(a, m) << " score: " << score << " assignment: " << m_ev.get_bool_value(a) << "\n";
}
//exit(0);
}
void bv_lookahead::recalibrate_weights() {
for (auto lit : ctx.root_literals()) {
if (!is_bv_literal(lit))
continue;
auto a = to_app(ctx.atom(lit.var()));
bool is_true0 = m_ev.bval0(a);
bool is_true1 = m_ev.bval1(a);
for (auto a : get_root_assertions()) {
if (ctx.rand(2047) < m_config.paws_sp) {
if (is_true0 == is_true1)
if (assertion_is_true(a))
dec_weight(a);
}
else if (is_true0 != is_true1)
else if (!assertion_is_true(a))
inc_weight(a);
}
@ -711,12 +778,9 @@ namespace sls {
std::ostream& bv_lookahead::display_weights(std::ostream& out) {
for (auto lit : ctx.root_literals()) {
if (!is_bv_literal(lit))
continue;
auto a = to_app(ctx.atom(lit.var()));
out << lit << ": "
<< get_weight(a) << " "
for (auto a : get_root_assertions()) {
out << get_weight(a) << " "
<< (assertion_is_true(a)?"T":"F") << " "
<< mk_bounded_pp(a, m) << " "
<< old_score(a) << " "
<< new_score(a) << "\n";
@ -727,10 +791,7 @@ namespace sls {
void bv_lookahead::ucb_forget() {
if (m_config.ucb_forget >= 1.0)
return;
for (auto lit : ctx.root_literals()) {
if (!is_bv_literal(lit))
continue;
auto a = to_app(ctx.atom(lit.var()));
for (auto a : get_root_assertions()) {
auto touched_old = get_touched(a);
auto touched_new = static_cast<unsigned>((touched_old - 1) * m_config.ucb_forget + 1);
set_touched(a, touched_new);
@ -744,4 +805,32 @@ namespace sls {
st.update("sls-bv-restarts", m_stats.m_restarts);
st.update("sls-bv-rotations", m_stats.m_rotations);
}
bv_lookahead::root_assertions::root_assertions(bv_lookahead& la, bool start) : m_la(la) {
if (start) {
idx = 0;
next();
}
else if (m_la.m_config.use_top_level_assertions)
idx = m_la.ctx.input_assertions().size();
else
idx = la.ctx.root_literals().size();
}
void bv_lookahead::root_assertions::next() {
if (m_la.m_config.use_top_level_assertions)
return;
while (idx < m_la.ctx.root_literals().size() && !m_la.is_bv_literal(m_la.ctx.root_literals()[idx]))
++idx;
}
expr* bv_lookahead::root_assertions::operator*() const {
if (m_la.m_config.use_top_level_assertions)
return m_la.ctx.input_assertions().get(idx);
return m_la.ctx.atom(m_la.ctx.root_literals()[idx].var());
};
}

59
src/ast/sls/sls_bv_lookahead.h
View file

@ -46,6 +46,7 @@ namespace sls {
double ucb_forget = 0.1;
bool ucb_init = false;
double ucb_noise = 0.1;
bool use_top_level_assertions = true;
};
struct stats {
@ -78,7 +79,7 @@ namespace sls {
expr* m_best_expr = nullptr;
expr* m_last_atom = nullptr;
ptr_vector<expr> m_empty_vars;
obj_map<expr, bool_info> m_bool_info;
vector<bool_info> m_bool_info;
expr_mark m_is_root;
unsigned m_touched = 1;
@ -92,9 +93,10 @@ namespace sls {
bool_info& get_bool_info(expr* e);
double lookahead_update(expr* u, bvect const& new_value);
double old_score(app* c) { return get_bool_info(c).score; }
void set_score(app* c, double d) { get_bool_info(c).score = d; }
double new_score(app* c);
double old_score(expr* c) { return get_bool_info(c).score; }
void set_score(expr* c, double d) { get_bool_info(c).score = d; }
double new_score(expr* c, bool is_true);
double new_score(expr* c);
double lookahead_flip(sat::bool_var v);
@ -107,9 +109,9 @@ namespace sls {
bool is_root(expr* e) { return m_is_root.is_marked(e); }
void ucb_forget();
unsigned get_touched(app* e) { return get_bool_info(e).touched; }
void set_touched(app* e, unsigned t) { get_bool_info(e).touched = t; }
void inc_touched(app* e) { ++get_bool_info(e).touched; }
unsigned get_touched(expr* e) { return get_bool_info(e).touched; }
void set_touched(expr* e, unsigned t) { get_bool_info(e).touched = t; }
void inc_touched(expr* e) { ++get_bool_info(e).touched; }
enum class move_type { random_t, guided_t, move_t, reset_t };
friend std::ostream& operator<<(std::ostream& out, move_type mt);
@ -128,10 +130,51 @@ namespace sls {
void check_restart();
void reset_uninterp_in_false_literals();
bool is_bv_literal(sat::literal lit);
bool is_false_bv_literal(sat::literal lit);
void search();
class root_assertions {
bv_lookahead& m_la;
unsigned idx = 0;
void next();
public:
root_assertions(bv_lookahead& la, bool start);
expr* operator*() const;
root_assertions& operator++() {
++idx;
next();
return *this;
}
bool operator!=(root_assertions const& other) const {
return idx != other.idx;
}
bool operator==(root_assertions const& other) const {
return idx == other.idx;
}
};
class root_assertion_iterator {
bv_lookahead& m_la;
public:
root_assertion_iterator(bv_lookahead& la) : m_la(la) {}
root_assertions begin() { return root_assertions(m_la, true); }
root_assertions end() { return root_assertions(m_la, false); }
};
root_assertion_iterator get_root_assertions() {
return root_assertion_iterator(*this);
}
bool assertion_is_true(expr* a);
void initialize_bool_values();
void finalize_bool_values();
public:
bv_lookahead(bv_eval& ev);

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

@ -135,8 +135,6 @@ namespace sls {
}
void bv_terms::register_uninterp(expr* e) {
if (!is_bv_predicate(e))
return;
m_uninterp_occurs.reserve(e->get_id() + 1);
auto& occs = m_uninterp_occurs[e->get_id()];
ptr_vector<expr> todo;

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

@ -32,6 +32,8 @@ namespace sls {
}
bool operator==(bvect const& a, bvect const& b) {
if (a.nw == 1)
return a[0] == b[0];
SASSERT(a.nw > 0);
return 0 == memcmp(a.data(), b.data(), a.nw * sizeof(digit_t));
}

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

@ -35,7 +35,7 @@ namespace sls {
}
context::context(ast_manager& m, sat_solver_context& s) :
m(m), s(s), m_atoms(m), m_allterms(m),
m(m), s(s), m_atoms(m), m_input_assertions(m), m_allterms(m),
m_gd(*this),
m_ld(*this),
m_repair_down(m.get_num_asts(), m_gd),
@ -330,20 +330,20 @@ namespace sls {
return;
m_constraint_ids.insert(e->get_id());
m_constraint_trail.push_back(e);
add_clause(e);
add_assertion(e, false);
m_new_constraint = true;
IF_VERBOSE(3, verbose_stream() << "add constraint " << mk_bounded_pp(e, m) << "\n");
++m_stats.m_num_constraints;
}
void context::add_clause(expr* f) {
void context::add_assertion(expr* f, bool is_input) {
expr_ref _e(f, m);
expr* g, * h, * k;
sat::literal_vector clause;
if (m.is_true(f))
return;
if (m.is_not(f, g) && m.is_not(g, g)) {
add_clause(g);
add_assertion(g, is_input);
return;
}
bool sign = m.is_not(f, f);
@ -352,15 +352,17 @@ namespace sls {
for (auto arg : *to_app(f))
clause.push_back(mk_literal(arg));
s.add_clause(clause.size(), clause.data());
if (is_input)
save_input_assertion(f, sign);
}
else if (!sign && m.is_and(f)) {
for (auto arg : *to_app(f))
add_clause(arg);
add_assertion(arg, is_input);
}
else if (sign && m.is_or(f)) {
for (auto arg : *to_app(f)) {
expr_ref fml(m.mk_not(arg), m);
add_clause(fml);
add_assertion(fml, is_input);
}
}
else if (!sign && m.is_implies(f, g, h)) {
@ -368,17 +370,21 @@ namespace sls {
clause.push_back(~mk_literal(g));
clause.push_back(mk_literal(h));
s.add_clause(clause.size(), clause.data());
if (is_input)
save_input_assertion(f, sign);
}
else if (sign && m.is_implies(f, g, h)) {
expr_ref fml(m.mk_not(h), m);
add_clause(fml);
add_clause(g);
add_assertion(fml, is_input);
add_assertion(g, is_input);
}
else if (sign && m.is_and(f)) {
clause.reset();
for (auto arg : *to_app(f))
clause.push_back(~mk_literal(arg));
s.add_clause(clause.size(), clause.data());
if (is_input)
save_input_assertion(f, sign);
}
else if (m.is_iff(f, g, h)) {
auto lit1 = mk_literal(g);
@ -387,6 +393,8 @@ namespace sls {
sat::literal cls2[2] = { sign ? ~lit1 : lit1, ~lit2 };
s.add_clause(2, cls1);
s.add_clause(2, cls2);
if (is_input)
save_input_assertion(f, sign);
}
else if (m.is_ite(f, g, h, k)) {
auto lit1 = mk_literal(g);
@ -399,15 +407,23 @@ namespace sls {
sat::literal cls2[2] = { lit1, sign ? ~lit3 : lit3 };
s.add_clause(2, cls1);
s.add_clause(2, cls2);
if (is_input)
save_input_assertion(f, sign);
}
else {
sat::literal lit = mk_literal(f);
if (sign)
lit.neg();
s.add_clause(1, &lit);
if (is_input)
save_input_assertion(f, sign);
}
}
void context::save_input_assertion(expr* f, bool sign) {
m_input_assertions.push_back(sign ? m.mk_not(f) : f);
}
void context::add_clause(sat::literal_vector const& lits) {
s.add_clause(lits.size(), lits.data());
m_new_constraint = true;
@ -511,6 +527,8 @@ namespace sls {
for (unsigned i = 0; i < m_atoms.size(); ++i)
if (m_atoms.get(i))
register_terms(m_atoms.get(i));
for (auto e : m_input_assertions)
register_terms(e);
for (auto p : m_plugins)
if (p)
p->initialize();

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

@ -120,6 +120,7 @@ namespace sls {
bool m_initialized = false;
bool m_new_constraint = false;
bool m_dirty = false;
expr_ref_vector m_input_assertions;
expr_ref_vector m_allterms;
ptr_vector<expr> m_subterms;
greater_depth m_gd;
@ -137,6 +138,9 @@ namespace sls {
void register_terms(expr* e);
void register_term(expr* e);
void add_assertion(expr* f, bool is_input);
void save_input_assertion(expr* f, bool sign);
void propagate_boolean_assignment();
void propagate_literal(sat::literal lit);
void repair_literals();
@ -173,7 +177,8 @@ namespace sls {
expr* term(unsigned id) const { return m_allterms.get(id); }
sat::bool_var atom2bool_var(expr* e) const { return m_atom2bool_var.get(e->get_id(), sat::null_bool_var); }
sat::literal mk_literal(expr* e);
void add_clause(expr* f);
void add_input_assertion(expr* f) { add_assertion(f, true); }
void add_theory_axiom(expr* f) { add_assertion(f, false); }
void add_clause(sat::literal_vector const& lits);
void flip(sat::bool_var v) { s.flip(v); }
bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
@ -183,6 +188,7 @@ namespace sls {
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; }
expr_ref_vector const& input_assertions() const { return m_input_assertions; }
bool is_unit(sat::literal lit) const { return is_unit(lit.var()); }
bool is_unit(sat::bool_var v) const { return m_unit_indices.contains(v); }
void reinit_relevant();

4
src/ast/sls/sls_smt_solver.cpp
View file

@ -92,7 +92,7 @@ namespace sls {
unsigned num_vars() const override { return m_ddfw.num_vars(); }
indexed_uint_set const& unsat() const override { return m_ddfw.unsat_set(); }
sat::bool_var add_var() override { m_dirty = true; return m_ddfw.add_var(); }
void add_clause(expr* f) { m_context.add_clause(f); }
void add_input_assertion(expr* f) { m_context.add_input_assertion(f); }
void force_restart() override { m_ddfw.force_restart(); }
@ -146,7 +146,7 @@ namespace sls {
lbool smt_solver::check() {
for (auto f : m_assertions)
m_solver_ctx->add_clause(f);
m_solver_ctx->add_input_assertion(f);
IF_VERBOSE(10, m_solver_ctx->display(verbose_stream()));
return m_ddfw.check(0, nullptr);
}

2
src/params/sls_params.pyg
View file

@ -25,5 +25,7 @@ def_module_params('sls',
('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'),
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
('random_seed', UINT, 0, 'random seed'),
('use_top_level_assertions_bv', BOOL, False, 'use top-level assertions for BV lookahead solver'),
('use_lookahead_bv', BOOL, True, 'use lookahead solver for BV'),
('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update')
))

9
src/tactic/sls/sls_tactic.cpp
View file

@ -131,9 +131,6 @@ public:
}
};
tactic* mk_sls_smt_tactic(ast_manager& m, params_ref const& p) {
return alloc(sls_smt_tactic, m, p);
}
class sls_tactic : public tactic {
ast_manager & m;
@ -264,3 +261,9 @@ tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
return t;
}
tactic* mk_sls_smt_tactic(ast_manager& m, params_ref const& p) {
tactic* t = and_then(mk_preamble(m, p), alloc(sls_smt_tactic, m, p));
t->updt_params(p);
return t;
}

2
src/util/obj_hashtable.h
View file

@ -57,7 +57,7 @@ class obj_map {
public:
struct key_data {
Key * m_key = nullptr;
Value m_value;
Value m_value{};
key_data() = default;
key_data(Key * k):
m_key(k) {