mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity

Merge remote-tracking branch 'microsoft/master' into eis-sls3

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 18:03:14 +01:00
parent 0227cebee4 bcf66f214f
commit 0cfaf5ad92
8 changed files with 185 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_ast.cpp
View file

@ -425,6 +425,20 @@ extern "C" {
RETURN_Z3(of_app(reinterpret_cast<app*>(a)));
}
bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a) {
LOG_Z3_is_ground(c, a);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, 0);
return is_ground(to_expr(a));
}
unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a) {
LOG_Z3_get_depth(c, a);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, 0);
return get_depth(to_expr(a));
}
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a) {
LOG_Z3_to_func_decl(c, a);
RESET_ERROR_CODE();

4
src/api/js/src/high-level/high-level.ts
View file

@ -1524,11 +1524,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
return new AstVectorImpl(check(Z3.optimize_get_assertions(contextPtr, this.ptr)));
}
maximize(expr: Arith<Name>) {
maximize(expr: Arith<Name> | BitVec<number, Name>) {
check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast));
}
minimize(expr: Arith<Name>) {
minimize(expr: Arith<Name> | BitVec<number, Name>) {
check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast));
}

10
src/api/z3_api.h
View file

@ -4992,6 +4992,16 @@ extern "C" {
*/
bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
/**
def_API('Z3_is_ground', BOOL, (_in(CONTEXT), _in(AST)))
*/
bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a);
/**
def_API('Z3_get_depth', UINT, (_in(CONTEXT), _in(AST)))
*/
unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a);
/**
def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST)))
*/

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

@ -33,11 +33,23 @@ namespace sls {
m(ev.m) {
}
/**
* Main entry point. The lookahead solver is invoked periodically
* before any other propagation with the main BV solver.
*/
void bv_lookahead::start_propagation() {
if (m_stats.m_num_propagations++ % m_config.propagation_base == 0)
search();
}
/**
* Main search loop.
* - Selects candidate variables
* - Applies random moves with a small probability
* - Applies guided moves to reduce cost of false literals
* - Applies random updates if no progress is made
*/
void bv_lookahead::search() {
updt_params(ctx.get_params());
rescore();
@ -53,36 +65,87 @@ namespace sls {
if (vars.empty())
return;
// random walk with probability 1024/wp
// random walk
if (ctx.rand(2047) < m_config.wp && apply_random_move(vars))
continue;
// guided moves, greedily reducing cost of false literals
if (apply_guided_move(vars))
continue;
// bail out if no progress, and try random update
if (apply_random_update(get_candidate_uninterp()))
recalibrate_weights();
}
m_config.max_moves_base += 100;
}
/**
* guided move: apply lookahead search for the selected variables
* and possible moves
*/
bool bv_lookahead::apply_guided_move(ptr_vector<expr> const& vars) {
m_best_expr = nullptr;
m_best_score = m_top_score;
unsigned sz = vars.size();
unsigned start = ctx.rand(sz);
unsigned start = ctx.rand();
for (unsigned i = 0; i < sz; ++i)
add_updates(vars[(start + i) % sz]);
TRACE("bv", tout << "guided update " << m_best_score << " " << (m_best_expr?"no update":"") << "\n";);
CTRACE("bv", !m_best_expr, tout << "no guided move\n";);
if (!m_best_expr)
return false;
apply_update(m_best_expr, m_best_value);
//verbose_stream() << "increasing move " << mk_bounded_pp(m_best_expr, m)
// << " := " << m_best_value << " score: " << m_top_score << "\n";
apply_update(m_best_expr, m_best_value, "increasing move");
return true;
}
/**
* random update: select a variable at random and set bits to random values
*/
bool bv_lookahead::apply_random_update(ptr_vector<expr> const& vars) {
expr* e = vars[ctx.rand(vars.size())];
auto& v = wval(e);
m_v_updated.set_bw(v.bw);
v.get_variant(m_v_updated, m_ev.m_rand);
if (!v.can_set(m_v_updated))
return false;
apply_update(e, m_v_updated, "random update");
return true;
}
/**
* random move: select a variable at random and use one of the moves: flip, add1, sub1
*/
bool bv_lookahead::apply_random_move(ptr_vector<expr> const& vars) {
expr* e = vars[ctx.rand(vars.size())];
auto& v = wval(e);
m_v_updated.set_bw(v.bw);
v.bits().copy_to(v.nw, m_v_updated);
switch (ctx.rand(3)) {
case 0: {
// flip a random bit
auto bit = ctx.rand(v.bw);
m_v_updated.set(bit, !m_v_updated.get(bit));
break;
}
case 1:
v.add1(m_v_updated);
break;
default:
v.sub1(m_v_updated);
break;
}
if (!v.can_set(m_v_updated))
return false;
apply_update(e, m_v_updated, "random move");
return true;
}
/**
* Retrieve a candidate top-level predicate that is false, give preference to
* those with high score, but back off if they are frequently chosen.
*/
ptr_vector<expr> const& bv_lookahead::get_candidate_uninterp() {
auto const& lits = ctx.root_literals();
app* e = nullptr;
@ -93,8 +156,8 @@ namespace sls {
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))
auto q = score
+ m_config.ucb_constant * sqrt(log((double)m_touched) / get_touched(a))
+ m_config.ucb_noise * ctx.rand(512);
if (q > max)
max = q, e = a;
@ -121,47 +184,6 @@ namespace sls {
return vars;
}
bool bv_lookahead::apply_random_update(ptr_vector<expr> const& vars) {
expr* e = vars[ctx.rand(vars.size())];
auto& v = wval(e);
m_v_updated.set_bw(v.bw);
v.get_variant(m_v_updated, m_ev.m_rand);
if (!v.can_set(m_v_updated))
return false;
apply_update(e, m_v_updated);
//verbose_stream() << "random update " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n";
return true;
}
bool bv_lookahead::apply_random_move(ptr_vector<expr> const& vars) {
expr* e = vars[ctx.rand(vars.size())];
auto& v = wval(e);
m_v_updated.set_bw(v.bw);
v.bits().copy_to(v.nw, m_v_updated);
switch (ctx.rand(3)) {
case 0: {
// flip a random bit
auto bit = ctx.rand(v.bw);
m_v_updated.set(bit, !m_v_updated.get(bit));
break;
}
case 1:
v.add1(m_v_updated);
break;
default:
v.sub1(m_v_updated);
break;
}
if (!v.can_set(m_v_updated))
return false;
apply_update(e, m_v_updated);
TRACE("bv", tout << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << "\n";);
// verbose_stream() << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n";
return true;
}
void bv_lookahead::check_restart() {
if (m_stats.m_moves % m_config.restart_base == 0) {
@ -183,6 +205,9 @@ namespace sls {
rescore();
}
/**
* Reset variables that occur in false literals.
*/
void bv_lookahead::reset_uninterp_in_false_literals() {
auto const& lits = ctx.root_literals();
expr_mark marked;
@ -199,7 +224,7 @@ namespace sls {
m_v_updated.set_bw(v.bw);
m_v_updated.set_zero();
if (v.can_set(m_v_updated)) {
apply_update(e, m_v_updated);
apply_update(e, m_v_updated, "reset");
}
}
}
@ -225,7 +250,6 @@ namespace sls {
void bv_lookahead::updt_params(params_ref const& _p) {
sls_params p(_p);
m_config.walksat = p.walksat();
m_config.walksat_repick = p.walksat_repick();
m_config.paws_sp = p.paws_sp();
@ -236,18 +260,21 @@ namespace sls {
m_config.restart_init = p.restart_init();
m_config.early_prune = p.early_prune();
m_config.ucb = p.walksat_ucb();
m_config.ucb_constant = p.walksat_ucb_constant();
m_config.ucb_forget = p.walksat_ucb_forget();
m_config.ucb_init = p.walksat_ucb_init();
m_config.ucb_noise = p.walksat_ucb_noise();
}
/**
* Score of a predicate based on how close the current
* solution is to satisfying it. The proximity measure is
* based on hamming distance for equalities, and differences
* for inequalities.
*/
double bv_lookahead::new_score(app* a) {
bool is_true = ctx.is_true(a);
bool is_true_new = m_ev.bval1(a);
if (!ctx.is_relevant(a))
return 0;
if (is_true == is_true_new)
return 1;
expr* x, * y;
@ -327,6 +354,10 @@ namespace sls {
return 0;
}
/**
* Rehearse an update. The update is revered while a score is computed and returned.
* Walk all parents, until hitting predicates where their scores are computed.
*/
double bv_lookahead::lookahead_update(expr* e, bvect const& new_value) {
SASSERT(bv.is_bv(e));
SASSERT(is_uninterp(e));
@ -441,16 +472,18 @@ namespace sls {
try_set(u, m_v_updated);
}
void bv_lookahead::apply_update(expr* e, bvect const& new_value) {
TRACE("bv", tout << "apply " << mk_bounded_pp(e, m) << " new value " << new_value << "\n");
/**
* Apply an update to a variable.
* The update is committed.
*/
void bv_lookahead::apply_update(expr* e, bvect const& new_value, char const* reason) {
SASSERT(bv.is_bv(e));
SASSERT(is_uninterp(e));
SASSERT(m_restore.empty());
wval(e).eval = new_value;
double old_top_score = m_top_score;
//verbose_stream() << mk_bounded_pp(e, m) << " := " << new_value << "\n";
VERIFY(wval(e).commit_eval());
insert_update_stack(e);
unsigned max_depth = get_depth(e);
@ -461,7 +494,7 @@ namespace sls {
m_ev.eval(e); // updates wval(e).eval
if (!wval(e).commit_eval()) {
TRACE("bv", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
IF_VERBOSE(0, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
IF_VERBOSE(2, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
// bv_plugin::is_sat picks up discrepancies
continue;
}
@ -484,8 +517,9 @@ namespace sls {
m_update_stack[depth].reset();
}
m_in_update_stack.reset();
TRACE("bv", tout << mk_bounded_pp(e, m) << " := "
<< new_value << " " << m_top_score << " (" << old_top_score << ")\n");
TRACE("bv", tout << reason << " " << mk_bounded_pp(m_best_expr, m)
<< " := " << new_value
<< " score " << m_top_score << "\n";);
}
bool bv_lookahead::insert_update(expr* e) {

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

@ -108,7 +108,7 @@ namespace sls {
void try_set(expr* u, bvect const& new_value);
void add_updates(expr* u);
void apply_update(expr* e, bvect const& new_value);
void apply_update(expr* e, bvect const& new_value, char const* reason);
bool apply_random_move(ptr_vector<expr> const& vars);
bool apply_guided_move(ptr_vector<expr> const& vars);
bool apply_random_update(ptr_vector<expr> const& vars);

61
src/ast/sls/sls_seq_plugin.cpp
View file

@ -95,9 +95,17 @@ Equality solving using stochastic Nelson.
#include "ast/sls/sls_seq_plugin.h"
#include "ast/sls/sls_context.h"
#include "ast/ast_pp.h"
#include "params/sls_params.hpp"
namespace sls {
struct zstring_hash_proc {
unsigned operator()(zstring const & s) const {
auto str = s.encode();
return string_hash(str.c_str(), static_cast<unsigned>(s.length()), 17);
}
};
seq_plugin::seq_plugin(context& c):
plugin(c),
@ -107,6 +115,8 @@ namespace sls {
thrw(c.get_manager())
{
m_fid = seq.get_family_id();
sls_params p(c.get_params());
m_str_update_strategy = p.str_update_strategy() == 0 ? EDIT_CHAR : EDIT_SUBSTR;
}
void seq_plugin::propagate_literal(sat::literal lit) {
@ -531,7 +541,7 @@ namespace sls {
len_u = r.get_unsigned();
if (len_u == val_x.length())
return true;
if (len_u < val_x.length()) {
if (len_u < val_x.length()) {
for (unsigned i = 0; i + len_u < val_x.length(); ++i)
m_str_updates.push_back({ x, val_x.extract(i, len_u), 1 });
}
@ -623,7 +633,7 @@ namespace sls {
if (!is_value(x))
m_str_updates.push_back({ x, strval1(y), 1 });
if (!is_value(y))
m_str_updates.push_back({ y, strval1(x), 1 });
m_str_updates.push_back({ y, strval1(x), 1 });
}
else {
// disequality
@ -669,8 +679,39 @@ namespace sls {
return d[n][m];
}
void seq_plugin::add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
if (m_str_update_strategy == EDIT_CHAR)
add_char_edit_updates(w, val, val_other, chars);
else
add_substr_edit_updates(w, val, val_other, chars);
}
void seq_plugin::add_substr_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
// all consecutive subsequences of val_other
hashtable<zstring, zstring_hash_proc, default_eq<zstring>> set;
set.insert(zstring(""));
for (unsigned i = 0; i < val_other.length(); ++i) {
for (unsigned j = val_other.length(); j > 0; ++j) {
zstring sub = val_other.extract(i, j);
if (set.contains(sub))
break;
set.insert(sub);
}
}
for (auto x : w) {
if (is_value(x))
continue;
zstring const& a = strval0(x);
for (auto& seq : set) {
if (seq == a)
continue;
m_str_updates.push_back({ x, seq, 1 });
}
}
}
void seq_plugin::add_char_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
for (auto x : w) {
if (is_value(x))
continue;
@ -1071,7 +1112,7 @@ namespace sls {
}
if (!is_value(xi)) {
m_str_updates.push_back({ xi, vi.extract(0, i), score });
m_str_updates.push_back({ xi, vi.extract(0, i) + zstring(vj[j]), score});
m_str_updates.push_back({ xi, vi.extract(0, i) + zstring(vj[j]), score});
}
if (!is_value(yj)) {
m_str_updates.push_back({ yj, vj.extract(0, j), score });
@ -1249,7 +1290,7 @@ namespace sls {
if (!is_value(x)) {
m_str_updates.push_back({ x, zstring(), 1 });
if (lenx > r && r >= 0)
m_str_updates.push_back({ x, sx.extract(0, r.get_unsigned()), 1 });
m_str_updates.push_back({ x, sx.extract(0, r.get_unsigned()), 1 });
}
if (!m.is_value(y)) {
m_int_updates.push_back({ y, rational(lenx), 1 });
@ -1307,7 +1348,7 @@ namespace sls {
if (value == -1) {
m_str_updates.push_back({ y, zstring(m_chars[ctx.rand(m_chars.size())]), 1 });
if (lenx > 0)
m_str_updates.push_back({ x, zstring(), 1 });
m_str_updates.push_back({ x, zstring(), 1 });
}
// change x:
// insert y into x at offset
@ -1325,7 +1366,7 @@ namespace sls {
if (offset_r.is_unsigned() && 0 <= value && offset_u + value < lenx) {
unsigned offs = offset_u + value.get_unsigned();
for (unsigned i = offs; i < lenx; ++i)
m_str_updates.push_back({ y, sx.extract(offs, i - offs + 1), 1 });
m_str_updates.push_back({ y, sx.extract(offs, i - offs + 1), 1 });
}
// change offset:
@ -1456,13 +1497,13 @@ namespace sls {
if (idx > 0)
su = sa.extract(0, idx);
su = su + sa.extract(idx + sb.length(), sa.length() - idx - sb.length());
m_str_updates.push_back({a, su, 1});
m_str_updates.push_back({ a, su, 1});
}
if (!m_chars.empty() && !is_value(b)) {
zstring sb1 = sb + zstring(m_chars[ctx.rand(m_chars.size())]);
zstring sb2 = zstring(m_chars[ctx.rand(m_chars.size())]) + sb;
m_str_updates.push_back({b, sb1, 1});
m_str_updates.push_back({b, sb2, 1});
m_str_updates.push_back({ b, sb1, 1});
m_str_updates.push_back({ b, sb2, 1});
}
}
return apply_update();

10
src/ast/sls/sls_seq_plugin.h
View file

@ -42,13 +42,19 @@ namespace sls {
ptr_vector<expr> lhs, rhs;
};
enum edit_distance_strategy {
EDIT_CHAR,
EDIT_SUBSTR,
};
seq_util seq;
arith_util a;
seq_rewriter rw;
th_rewriter thrw;
scoped_ptr_vector<eval> m_values;
indexed_uint_set m_chars; // set of characters in the problem
bool m_initialized = false;
bool m_initialized = false;
edit_distance_strategy m_str_update_strategy;
struct str_update {
expr* e;
@ -122,6 +128,8 @@ namespace sls {
unsigned edit_distance_with_updates(string_instance const& a, string_instance const& b);
unsigned edit_distance(zstring const& a, zstring const& b);
void add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);
void add_char_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);
void add_substr_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);
zstring trunc_pad_to_fit(unsigned min_length, unsigned max_length, zstring const& s);

5
src/params/sls_params.pyg
View file

@ -3,7 +3,7 @@ def_module_params('sls',
description='Experimental Stochastic Local Search Solver (for QFBV only).',
params=(max_memory_param(),
('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
('max_repairs', UINT, 1000, 'maximum number of repairs before restart'),
('max_repairs', UINT, 1000, 'maximum number of repairs before restart'),
('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'),
('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'),
('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'),
@ -24,5 +24,6 @@ def_module_params('sls',
('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
('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')
('random_seed', UINT, 0, 'random seed'),
('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update')
))