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

move sls core functionality to be independent of tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-22 12:00:52 -08:00
parent 606a9a7409
commit e321643bf5
13 changed files with 60 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

367
src/ast/sls/bvsls_opt_engine.cpp Normal file
View file

@ -0,0 +1,367 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
bvsls_opt_engine.cpp
Abstract:
Optimization extensions to bvsls
Author:
Christoph (cwinter) 2014-03-28
Notes:
--*/
#include "ast/normal_forms/nnf.h"
#include "ast/sls/bvsls_opt_engine.h"
bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
sls_engine(m, p),
m_hard_tracker(sls_engine::m_tracker),
m_obj_tracker(m, m_bv_util, m_mpz_manager, m_powers),
m_obj_evaluator(m, m_bv_util, m_obj_tracker, m_mpz_manager, m_powers)
{
m_best_model = alloc(model, m);
}
bvsls_opt_engine::~bvsls_opt_engine()
{
}
bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
expr_ref const & objective,
model_ref initial_model,
bool _maximize)
{
SASSERT(m_bv_util.is_bv(objective));
TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " <<
mk_ismt2_pp(objective, m()) << std::endl;);
m_hard_tracker.initialize(m_assertions);
setup_opt_tracker(objective, _maximize);
if (initial_model.get() != nullptr) {
TRACE("sls_opt", tout << "Initial model provided: " << std::endl;
for (unsigned i = 0; i < initial_model->get_num_constants(); i++) {
func_decl * fd = initial_model->get_constant(i);
expr * val = initial_model->get_const_interp(fd);
tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl;
});
m_hard_tracker.set_model(initial_model);
m_evaluator.update_all();
}
optimization_result res(m_manager);
lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
TRACE("sls_opt", tout << "initial model is sat? " << is_sat << std::endl;);
for (m_stats.m_restarts = 0;
m_stats.m_restarts < m_max_restarts;
m_stats.m_restarts++)
{
mpz old_best;
m_mpz_manager.set(old_best, m_best_model_score);
if (is_sat != l_true) {
do {
checkpoint();
IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
is_sat = search();
if (is_sat == l_undef)
m_hard_tracker.randomize(m_assertions);
}
while (is_sat != l_true &&
m_stats.m_restarts++ < m_max_restarts);
}
if (is_sat == l_true) {
IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
res.is_sat = l_true;
m_obj_tracker.set_model(m_hard_tracker.get_model());
m_obj_evaluator.update_all();
expr_ref local_best = maximize();
if ((_maximize && m_mpz_manager.gt(m_best_model_score, old_best)) ||
(!_maximize && m_mpz_manager.lt(m_best_model_score, old_best)))
{
res.optimum = local_best;
}
}
m_hard_tracker.randomize(m_assertions);
m_evaluator.update_all();
is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
}
TRACE("sls_opt", tout << "sat: " << res.is_sat << "; optimum: " << mk_ismt2_pp(res.optimum, m()) << std::endl;);
return res;
}
void bvsls_opt_engine::setup_opt_tracker(expr_ref const & objective, bool _max)
{
expr_ref obj(m_manager);
obj = objective;
if (!_max)
obj = m_bv_util.mk_bv_neg(objective);
m_obj_e = obj.get();
m_obj_bv_sz = m_bv_util.get_bv_size(m_obj_e);
ptr_vector<expr> objs;
objs.push_back(m_obj_e);
m_obj_tracker.initialize(objs);
}
expr_ref bvsls_opt_engine::maximize()
{
SASSERT(m_hard_tracker.is_sat());
TRACE("sls_opt", tout << "Initial opt model:" << std::endl; m_obj_tracker.show_model(tout););
mpz score, old_score, max_score, new_value;
unsigned new_const = (unsigned)-1, new_bit = 0;
ptr_vector<func_decl> consts = m_obj_tracker.get_constants();
move_type move;
m_mpz_manager.set(score, top_score());
m_mpz_manager.set(max_score, m_powers(m_obj_bv_sz)); m_mpz_manager.dec(max_score);
IF_VERBOSE(10, verbose_stream() << "Initial score: " << m_mpz_manager.to_string(score) << std::endl;);
save_model(score);
while (m_mpz_manager.lt(score, max_score) && check_restart(m_stats.m_moves))
{
checkpoint();
m_stats.m_moves++;
m_mpz_manager.set(old_score, score);
new_const = (unsigned)-1;
mpz score(0);
m_mpz_manager.set(score,
find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, m_obj_e));
if (new_const == static_cast<unsigned>(-1)) {
m_mpz_manager.set(score, old_score);
if (m_mpz_manager.gt(score, m_best_model_score))
save_model(score);
if (!randomize_wrt_hard()) {
// Can't improve and can't randomize; can't do anything other than bail out.
TRACE("sls_opt", tout << "Got stuck; bailing out." << std::endl;);
IF_VERBOSE(10, verbose_stream() << "No local improvements possible." << std::endl;);
goto bailout;
}
m_mpz_manager.set(score, top_score());
}
else {
m_stats.m_moves++;
TRACE("sls_opt", tout << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;);
IF_VERBOSE(10, verbose_stream() << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;);
func_decl * fd = consts[new_const];
incremental_score(fd, new_value);
m_obj_evaluator.update(fd, new_value);
m_mpz_manager.set(score, top_score());
}
}
bailout:
m_mpz_manager.del(new_value);
expr_ref res(m_manager);
res = m_bv_util.mk_numeral(m_best_model_score, m_obj_bv_sz);
return res;
}
void bvsls_opt_engine::save_model(mpz const & score) {
model_ref mdl = m_hard_tracker.get_model();
model_ref obj_mdl = m_obj_tracker.get_model();
for (unsigned i = 0; i < obj_mdl->get_num_constants(); i++) {
func_decl * fd = obj_mdl->get_constant(i);
expr * val = obj_mdl->get_const_interp(fd);
if (mdl->has_interpretation(fd)) {
if (mdl->get_const_interp(fd) != val)
TRACE("sls_opt", tout << "model disagreement on " << fd->get_name() << ": " <<
mk_ismt2_pp(val, m()) << " != " << mk_ismt2_pp(mdl->get_const_interp(fd), m()) << std::endl;);
SASSERT(mdl->get_const_interp(fd) == val);
}
else
mdl->register_decl(fd, val);
}
m_best_model = mdl;
m_mpz_manager.set(m_best_model_score, score);
}
// checks whether the score outcome of a given move is better than the previous score
bool bvsls_opt_engine::what_if(
func_decl * fd,
const unsigned & fd_inx,
const mpz & temp,
mpz & best_score,
unsigned & best_const,
mpz & best_value)
{
#if _EARLY_PRUNE_
double r = incremental_score_prune(fd, temp);
#else
double r = incremental_score(fd, temp);
#endif
if (r >= 1.0 && m_hard_tracker.is_sat()) {
m_obj_evaluator.update(fd, temp);
mpz cur_best(0);
m_mpz_manager.set(cur_best, top_score());
TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
" --> " << r << "; score=" << m_mpz_manager.to_string(cur_best) << std::endl;);
if (m_mpz_manager.gt(cur_best, best_score)) {
m_mpz_manager.set(best_score, cur_best);
best_const = fd_inx;
m_mpz_manager.set(best_value, temp);
return true;
}
}
else
{
TRACE("sls_whatif_failed", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
" --> unsatisfied hard constraints" << std::endl;);
}
return false;
}
mpz bvsls_opt_engine::find_best_move(
ptr_vector<func_decl> & to_evaluate,
mpz & score,
unsigned & best_const,
mpz & best_value,
unsigned & new_bit,
move_type & move,
mpz const & max_score,
expr * objective)
{
mpz old_value, temp;
#if _USE_MUL3_ || _USE_UNARY_MINUS_
mpz temp2;
#endif
unsigned bv_sz;
mpz new_score;
m_mpz_manager.set(new_score, score);
for (unsigned i = 0; i < to_evaluate.size() && m_mpz_manager.lt(new_score, max_score); i++) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
m_mpz_manager.set(old_value, m_obj_tracker.get_value(fd));
// first try to flip every bit
for (unsigned j = 0; j < bv_sz && m_mpz_manager.lt(new_score, max_score); j++) {
// What would happen if we flipped bit #i ?
mk_flip(srt, old_value, j, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value)) {
new_bit = j;
move = MV_FLIP;
}
}
if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
#if _USE_ADDSUB_
if (!m_mpz_manager.is_even(old_value)) {
// for odd values, try +1
mk_inc(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INC;
}
else {
// for even values, try -1
mk_dec(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_DEC;
}
#endif
// try inverting
mk_inv(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
#if _USE_UNARY_MINUS_
mk_inc(bv_sz, temp, temp2);
if (what_if(fd, i, temp2, new_score, best_const, best_value))
move = MV_UMIN;
#endif
#if _USE_MUL2DIV2_
// try multiplication by 2
mk_mul2(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_MUL2;
#if _USE_MUL3_
// try multiplication by 3
mk_add(bv_sz, old_value, temp, temp2);
if (what_if(fd, i, temp2, new_score, best_const, best_value))
move = MV_MUL3;
#endif
// try division by 2
mk_div2(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_DIV2;
#endif
}
// reset to what it was before
//double check =
incremental_score(fd, old_value);
m_obj_evaluator.update(fd, old_value);
}
m_mpz_manager.del(old_value);
m_mpz_manager.del(temp);
#if _USE_MUL3_
m_mpz_manager.del(temp2);
#endif
return new_score;
}
bool bvsls_opt_engine::randomize_wrt_hard() {
ptr_vector<func_decl> consts = m_obj_tracker.get_constants();
unsigned csz = consts.size();
unsigned retry_count = csz;
while (retry_count-- > 0)
{
unsigned ri = (m_obj_tracker.get_random_uint((csz < 16) ? 4 : (csz < 256) ? 8 : (csz < 4096) ? 12 : (csz < 65536) ? 16 : 32)) % csz;
func_decl * random_fd = consts[ri]; // Random constant
mpz random_val; // random value.
m_mpz_manager.set(random_val, m_obj_tracker.get_random(random_fd->get_range()));
mpz old_value;
m_mpz_manager.set(old_value, m_obj_tracker.get_value(random_fd));
if (!m_mpz_manager.eq(random_val, old_value)) {
m_evaluator.update(random_fd, random_val);
if (m_hard_tracker.is_sat()) {
TRACE("sls_opt", tout << "Randomizing " << random_fd->get_name() << " to " <<
m_mpz_manager.to_string(random_val) << std::endl;);
m_obj_evaluator.update(random_fd, random_val);
return true;
}
else
m_evaluator.update(random_fd, old_value);
}
}
return false;
}

71
src/ast/sls/bvsls_opt_engine.h Normal file
View file

@ -0,0 +1,71 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
bvsls_opt_engine.h
Abstract:
Optimization extensions to bvsls
Author:
Christoph (cwinter) 2014-03-28
Notes:
--*/
#pragma once
#include "ast/sls/sls_engine.h"
class bvsls_opt_engine : public sls_engine {
sls_tracker & m_hard_tracker;
sls_tracker m_obj_tracker;
sls_evaluator m_obj_evaluator;
model_ref m_best_model;
mpz m_best_model_score;
unsigned m_obj_bv_sz;
expr * m_obj_e;
public:
bvsls_opt_engine(ast_manager & m, params_ref const & p);
~bvsls_opt_engine();
class optimization_result {
public:
lbool is_sat;
expr_ref optimum;
optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {}
};
optimization_result optimize(expr_ref const & objective, model_ref initial_model = model_ref(), bool maximize=true);
void get_model(model_ref & result) { result = m_best_model; }
protected:
void setup_opt_tracker(expr_ref const & objective, bool _max);
expr_ref maximize();
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
mpz & best_score, unsigned & best_const, mpz & best_value);
mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz & score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
mpz const & max_score, expr * objective);
mpz top_score() {
mpz res(0);
obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
for (obj_hashtable<expr>::iterator it = top_exprs.begin();
it != top_exprs.end();
it++)
m_mpz_manager.add(res, m_obj_tracker.get_value(*it), res);
return res;
}
void save_model(mpz const & score);
bool randomize_wrt_hard();
};

592
src/ast/sls/sls_engine.cpp Normal file
View file

@ -0,0 +1,592 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
sls_engine.cpp
Abstract:
A Stochastic Local Search (SLS) engine
Author:
Christoph (cwinter) 2014-03-19
Notes:
--*/
#include<float.h> // Need DBL_MAX
#include "util/map.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/var_subst.h"
#include "model/model_pp.h"
#include "tactic/tactic.h"
#include "util/luby.h"
#include "params/sls_params.hpp"
#include "ast/sls/sls_engine.h"
sls_engine::sls_engine(ast_manager & m, params_ref const & p) :
m_manager(m),
m_powers(m_mpz_manager),
m_zero(m_mpz_manager.mk_z(0)),
m_one(m_mpz_manager.mk_z(1)),
m_two(m_mpz_manager.mk_z(2)),
m_bv_util(m),
m_tracker(m, m_bv_util, m_mpz_manager, m_powers),
m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers)
{
updt_params(p);
m_tracker.updt_params(p);
}
sls_engine::~sls_engine() {
m_mpz_manager.del(m_zero);
m_mpz_manager.del(m_one);
m_mpz_manager.del(m_two);
}
void sls_engine::updt_params(params_ref const & _p) {
sls_params p(_p);
m_max_restarts = p.max_restarts();
m_tracker.set_random_seed(p.random_seed());
m_walksat = p.walksat();
m_walksat_repick = p.walksat_repick();
m_paws_sp = p.paws_sp();
m_paws = m_paws_sp < 1024;
m_wp = p.wp();
m_vns_mc = p.vns_mc();
m_vns_repick = p.vns_repick();
m_restart_base = p.restart_base();
m_restart_next = m_restart_base;
m_restart_init = p.restart_init();
m_early_prune = p.early_prune();
m_random_offset = p.random_offset();
m_rescore = p.rescore();
// Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT.
if (m_walksat_repick && !m_walksat)
NOT_IMPLEMENTED_YET();
if (m_vns_repick && !m_walksat)
NOT_IMPLEMENTED_YET();
}
void sls_engine::collect_statistics(statistics& st) const {
double seconds = m_stats.m_stopwatch.get_current_seconds();
st.update("sls restarts", m_stats.m_restarts);
st.update("sls full evals", m_stats.m_full_evals);
st.update("sls incr evals", m_stats.m_incr_evals);
st.update("sls incr evals/sec", m_stats.m_incr_evals / seconds);
st.update("sls FLIP moves", m_stats.m_flips);
st.update("sls INC moves", m_stats.m_incs);
st.update("sls DEC moves", m_stats.m_decs);
st.update("sls INV moves", m_stats.m_invs);
st.update("sls moves", m_stats.m_moves);
st.update("sls moves/sec", m_stats.m_moves / seconds);
}
void sls_engine::checkpoint() {
tactic::checkpoint(m_manager);
}
bool sls_engine::full_eval(model & mdl) {
model::scoped_model_completion _scm(mdl, true);
for (expr* a : m_assertions) {
checkpoint();
if (!mdl.is_true(a)) {
TRACE("sls", tout << "Evaluation: false\n";);
return false;
}
}
return true;
}
double sls_engine::top_score() {
double top_sum = 0.0;
for (expr* e : m_assertions) {
top_sum += m_tracker.get_score(e);
}
TRACE("sls_top", tout << "Score distribution:";
for (expr* e : m_assertions)
tout << " " << m_tracker.get_score(e);
tout << " AVG: " << top_sum / (double)m_assertions.size() << std::endl;);
m_tracker.set_top_sum(top_sum);
return top_sum;
}
double sls_engine::rescore() {
m_evaluator.update_all();
m_stats.m_full_evals++;
return top_score();
}
double sls_engine::serious_score(func_decl * fd, const mpz & new_value) {
m_evaluator.serious_update(fd, new_value);
m_stats.m_incr_evals++;
return m_tracker.get_top_sum();
}
double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) {
m_evaluator.update(fd, new_value);
m_stats.m_incr_evals++;
return m_tracker.get_top_sum();
}
double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) {
m_stats.m_incr_evals++;
if (m_evaluator.update_prune(fd, new_value))
return m_tracker.get_top_sum();
else
return -DBL_MAX;
}
// checks whether the score outcome of a given move is better than the previous score
bool sls_engine::what_if(
func_decl * fd,
const unsigned & fd_inx,
const mpz & temp,
double & best_score,
unsigned & best_const,
mpz & best_value) {
#ifdef Z3DEBUG
mpz old_value;
m_mpz_manager.set(old_value, m_tracker.get_value(fd));
#endif
double r;
if (m_early_prune)
r = incremental_score_prune(fd, temp);
else
r = incremental_score(fd, temp);
#ifdef Z3DEBUG
TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
" --> " << r << std::endl;);
m_mpz_manager.del(old_value);
#endif
// Andreas: Had this idea on my last day. Maybe we could add a noise here similar to the one that worked so well for ucb assertion selection.
// r += 0.0001 * m_tracker.get_random_uint(8);
// Andreas: For some reason it is important to use > here instead of >=. Probably related to preferring the LSB.
if (r > best_score) {
best_score = r;
best_const = fd_inx;
m_mpz_manager.set(best_value, temp);
return true;
}
return false;
}
void sls_engine::mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result) {
mpz temp, mask, mask2;
m_mpz_manager.add(old_value, add_value, temp);
m_mpz_manager.set(mask, m_powers(bv_sz));
m_mpz_manager.bitwise_not(bv_sz, mask, mask2);
m_mpz_manager.bitwise_and(temp, mask2, result);
m_mpz_manager.del(temp);
m_mpz_manager.del(mask);
m_mpz_manager.del(mask2);
}
void sls_engine::mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) {
unsigned shift;
m_mpz_manager.add(old_value, m_one, incremented);
if (m_mpz_manager.is_power_of_two(incremented, shift) && shift == bv_sz)
m_mpz_manager.set(incremented, m_zero);
}
void sls_engine::mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented) {
if (m_mpz_manager.is_zero(old_value)) {
m_mpz_manager.set(decremented, m_powers(bv_sz));
m_mpz_manager.dec(decremented);
}
else
m_mpz_manager.sub(old_value, m_one, decremented);
}
void sls_engine::mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted) {
m_mpz_manager.bitwise_not(bv_sz, old_value, inverted);
}
void sls_engine::mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped) {
m_mpz_manager.set(flipped, m_zero);
if (m_bv_util.is_bv_sort(s)) {
mpz mask;
m_mpz_manager.set(mask, m_powers(bit));
m_mpz_manager.bitwise_xor(old_value, mask, flipped);
m_mpz_manager.del(mask);
}
else if (m_manager.is_bool(s))
m_mpz_manager.set(flipped, (m_mpz_manager.is_zero(old_value)) ? m_one : m_zero);
else
NOT_IMPLEMENTED_YET();
}
void sls_engine::mk_random_move(ptr_vector<func_decl> & unsat_constants)
{
unsigned rnd_mv = 0;
unsigned ucc = unsat_constants.size();
unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc;
func_decl * fd = unsat_constants[rc];
mpz new_value;
sort * srt = fd->get_range();
if (m_manager.is_bool(srt))
m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
else
{
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv = 2;
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++;
// Andreas: The other option would be to scale the probability for flips according to the bit-width.
/* unsigned bv_sz2 = m_bv_util.get_bv_size(srt);
rnd_mv = m_tracker.get_random_uint(16) % (bv_sz2 + 3);
if (rnd_mv > 3) rnd_mv = 0; */
move_type mt = (move_type)rnd_mv;
// Andreas: Christoph claimed inversion doesn't make sense, let's do a flip instead. Is this really true?
if (mt == MV_INV) mt = MV_FLIP;
unsigned bit = 0;
switch (mt)
{
case MV_FLIP: {
unsigned bv_sz = m_bv_util.get_bv_size(srt);
bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz;
mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value);
break;
}
case MV_INC:
mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
case MV_DEC:
mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
case MV_INV:
mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
default:
NOT_IMPLEMENTED_YET();
}
TRACE("sls", tout << "Randomization candidates: ";
for (unsigned i = 0; i < unsat_constants.size(); i++)
tout << unsat_constants[i]->get_name() << ", ";
tout << std::endl;
tout << "Random move: ";
switch (mt) {
case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break;
case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break;
case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break;
case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break;
}
tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout););
}
m_evaluator.serious_update(fd, new_value);
m_mpz_manager.del(new_value);
}
// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
double sls_engine::find_best_move(
ptr_vector<func_decl> & to_evaluate,
double score,
unsigned & best_const,
mpz & best_value,
unsigned & new_bit,
move_type & move)
{
mpz old_value, temp;
unsigned bv_sz;
double new_score = score;
// Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list.
unsigned sz = to_evaluate.size();
unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0;
for (unsigned j = 0; j < sz; j++) {
unsigned i = j + offset;
if (i >= sz) i -= sz;
//for (unsigned i = 0; i < to_evaluate.size(); i++) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
m_mpz_manager.set(old_value, m_tracker.get_value(fd));
// first try to flip every bit
for (unsigned j = 0; j < bv_sz; j++) {
// What would happen if we flipped bit #i ?
mk_flip(srt, old_value, j, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value)) {
new_bit = j;
move = MV_FLIP;
}
}
if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
if (!m_mpz_manager.is_even(old_value)) {
// for odd values, try +1
mk_inc(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INC;
}
else {
// for even values, try -1
mk_dec(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_DEC;
}
// try inverting
mk_inv(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
}
// reset to what it was before
incremental_score(fd, old_value);
}
m_mpz_manager.del(old_value);
m_mpz_manager.del(temp);
return new_score;
}
// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
double sls_engine::find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value) {
mpz old_value, temp, temp2;
unsigned bv_sz;
double new_score = score;
// Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list.
unsigned sz = to_evaluate.size();
unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0;
for (unsigned j = 0; j < sz; j++) {
unsigned i = j + offset;
if (i >= sz) i -= sz;
//for (unsigned i = 0; i < to_evaluate.size(); i++) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
m_mpz_manager.set(old_value, m_tracker.get_value(fd));
if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) {
for (unsigned j = 0; j < bv_sz; j++) {
mk_flip(srt, old_value, j, temp);
for (unsigned l = 0; l < m_vns_mc && l < bv_sz / 2; l++)
{
unsigned k = m_tracker.get_random_uint(16) % bv_sz;
while (k == j)
k = m_tracker.get_random_uint(16) % bv_sz;
mk_flip(srt, temp, k, temp2);
what_if(fd, i, temp2, new_score, best_const, best_value);
}
}
}
// reset to what it was before
incremental_score(fd, old_value);
}
m_mpz_manager.del(old_value);
m_mpz_manager.del(temp);
m_mpz_manager.del(temp2);
return new_score;
}
// main search loop
lbool sls_engine::search() {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit;
mpz new_value;
move_type move;
score = rescore();
unsigned sz = m_assertions.size();
while (check_restart(m_stats.m_moves)) {
checkpoint();
m_stats.m_moves++;
// Andreas: Every base restart interval ...
if (m_stats.m_moves % m_restart_base == 0)
{
// ... potentially smooth the touched counters ...
m_tracker.ucb_forget(m_assertions);
// ... or normalize the top-level score.
if (m_rescore) score = rescore();
}
// get candidate variables
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(m_assertions);
if (to_evaluate.empty())
{
res = l_true;
goto bailout;
}
// random walk with probability wp / 1024
if (m_wp && m_tracker.get_random_uint(10) < m_wp)
{
mk_random_move(to_evaluate);
score = m_tracker.get_top_sum();
continue;
}
old_score = score;
new_const = (unsigned)-1;
// find best increasing move
score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move);
// use Monte Carlo 2-bit-flip sampling if no increasing move was found previously
if (m_vns_mc && (new_const == static_cast<unsigned>(-1)))
score = find_best_move_mc(to_evaluate, score, new_const, new_value);
// repick assertion if no increasing move was found previously
if (m_vns_repick && (new_const == static_cast<unsigned>(-1)))
{
expr * q = m_tracker.get_new_unsat_assertion(m_assertions);
// only apply if another unsatisfied assertion actually exists
if (q)
{
ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(q);
score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move);
if (new_const != static_cast<unsigned>(-1)) {
func_decl * fd = to_evaluate2[new_const];
score = serious_score(fd, new_value);
continue;
}
}
}
// randomize if no increasing move was found
if (new_const == static_cast<unsigned>(-1)) {
score = old_score;
if (m_walksat_repick)
m_evaluator.randomize_local(m_assertions);
else
m_evaluator.randomize_local(to_evaluate);
score = m_tracker.get_top_sum();
// update assertion weights if a weighting is enabled (sp < 1024)
if (m_paws)
{
for (unsigned i = 0; i < sz; i++)
{
expr * q = m_assertions[i];
// smooth weights with probability sp / 1024
if (m_tracker.get_random_uint(10) < m_paws_sp)
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_one))
m_tracker.decrease_weight(q);
}
// increase weights otherwise
else
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero))
m_tracker.increase_weight(q);
}
}
}
}
// otherwise, apply most increasing move
else {
func_decl * fd = to_evaluate[new_const];
score = serious_score(fd, new_value);
}
}
bailout:
m_mpz_manager.del(new_value);
return res;
}
lbool sls_engine::operator()() {
m_tracker.initialize(m_assertions);
m_tracker.reset(m_assertions);
if (m_restart_init)
m_tracker.randomize(m_assertions);
lbool res = l_undef;
do {
checkpoint();
// report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
res = search();
if (res == l_undef)
{
if (m_restart_init)
m_tracker.randomize(m_assertions);
else
m_tracker.reset(m_assertions);
}
} while (res != l_true && m_stats.m_restarts++ < m_max_restarts);
verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
return res;
}
/* Andreas: Needed for Armin's restart scheme if we don't want to use loops.
double sls_engine::get_restart_armin(unsigned cnt_restarts)
{
unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts));
unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2;
return pow((double) _RESTART_CONST_ARMIN_, (int) inner_id + 1);
}
*/
unsigned sls_engine::check_restart(unsigned curr_value)
{
if (curr_value > m_restart_next)
{
/* Andreas: My own scheme (= 1) seems to work best. Other schemes are disabled so that we save one parameter.
I leave the other versions as comments in case you want to try it again somewhen.
#if _RESTART_SCHEME_ == 5
m_restart_next += (unsigned)(m_restart_base * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts));
#elif _RESTART_SCHEME_ == 4
m_restart_next += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? m_restart_base : (m_restart_base * m_stats.m_restarts + 1);
#elif _RESTART_SCHEME_ == 3
m_restart_next += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * m_restart_base;
#elif _RESTART_SCHEME_ == 2
m_restart_next += get_luby(m_stats.m_restarts + 1) * m_restart_base;
#elif _RESTART_SCHEME_ == 1
if (m_stats.m_restarts & 1)
m_restart_next += m_restart_base;
else
m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base;
#else
m_restart_limit += m_restart_base;
#endif */
if (m_stats.m_restarts & 1)
m_restart_next += m_restart_base;
else
m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base;
return 0;
}
return 1;
}

144
src/ast/sls/sls_engine.h Normal file
View file

@ -0,0 +1,144 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sls_engine.h
Abstract:
A Stochastic Local Search (SLS) engine
Author:
Christoph (cwinter) 2014-03-19
Notes:
--*/
#pragma once
#include "util/stopwatch.h"
#include "util/lbool.h"
#include "ast/converters/model_converter.h"
#include "ast/sls/sls_tracker.h"
#include "ast/sls/sls_evaluator.h"
#include "util/statistics.h"
class sls_engine {
public:
class stats {
public:
unsigned m_restarts;
stopwatch m_stopwatch;
unsigned m_full_evals;
unsigned m_incr_evals;
unsigned m_moves, m_flips, m_incs, m_decs, m_invs;
stats() :
m_restarts(0),
m_full_evals(0),
m_incr_evals(0),
m_moves(0),
m_flips(0),
m_incs(0),
m_decs(0),
m_invs(0) {
m_stopwatch.reset();
m_stopwatch.start();
}
void reset() {
m_full_evals = m_flips = m_incr_evals = 0;
m_stopwatch.reset();
m_stopwatch.start();
}
};
protected:
ast_manager & m_manager;
stats m_stats;
unsynch_mpz_manager m_mpz_manager;
powers m_powers;
mpz m_zero, m_one, m_two;
bv_util m_bv_util;
sls_tracker m_tracker;
sls_evaluator m_evaluator;
ptr_vector<expr> m_assertions;
unsigned m_max_restarts;
unsigned m_walksat;
unsigned m_walksat_repick;
unsigned m_wp;
unsigned m_vns_mc;
unsigned m_vns_repick;
unsigned m_paws;
unsigned m_paws_sp;
unsigned m_restart_base;
unsigned m_restart_next;
unsigned m_restart_init;
unsigned m_early_prune;
unsigned m_random_offset;
unsigned m_rescore;
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type;
public:
sls_engine(ast_manager & m, params_ref const & p);
~sls_engine();
ast_manager & m() const { return m_manager; }
void updt_params(params_ref const & _p);
void assert_expr(expr * e) { m_assertions.push_back(e); }
stats const & get_stats(void) { return m_stats; }
void collect_statistics(statistics & st) const;
void reset_statistics() { m_stats.reset(); }
bool full_eval(model & mdl);
void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result);
void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented);
void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented);
void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);
lbool search();
lbool operator()();
mpz & get_value(expr * n) { return m_tracker.get_value(n); }
model_ref get_model() { return m_tracker.get_model(); }
unsynch_mpz_manager& get_mpz_manager() { return m_mpz_manager; }
protected:
void checkpoint();
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
double top_score();
double rescore();
double serious_score(func_decl * fd, const mpz & new_value);
double incremental_score(func_decl * fd, const mpz & new_value);
double incremental_score_prune(func_decl * fd, const mpz & new_value);
double find_best_move(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value);
void mk_random_move(ptr_vector<func_decl> & unsat_constants);
//double get_restart_armin(unsigned cnt_restarts);
unsigned check_restart(unsigned curr_value);
};

821
src/ast/sls/sls_evaluator.h Normal file
View file

@ -0,0 +1,821 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
sls_evaluator.h
Abstract:
SLS Evaluator
Author:
Christoph (cwinter) 2012-02-29
Notes:
--*/
#pragma once
#include "model/model_evaluator.h"
#include "ast/sls/sls_powers.h"
#include "ast/sls/sls_tracker.h"
class sls_evaluator {
ast_manager & m_manager;
bv_util & m_bv_util;
family_id m_basic_fid;
family_id m_bv_fid;
sls_tracker & m_tracker;
unsynch_mpz_manager & m_mpz_manager;
mpz m_zero, m_one, m_two;
powers & m_powers;
expr_ref_buffer m_temp_exprs;
vector<ptr_vector<expr> > m_traversal_stack;
vector<ptr_vector<expr> > m_traversal_stack_bool;
public:
sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) :
m_manager(m),
m_bv_util(bvu),
m_tracker(t),
m_mpz_manager(mm),
m_zero(m_mpz_manager.mk_z(0)),
m_one(m_mpz_manager.mk_z(1)),
m_two(m_mpz_manager.mk_z(2)),
m_powers(p),
m_temp_exprs(m) {
m_bv_fid = m_bv_util.get_family_id();
m_basic_fid = m_manager.get_basic_family_id();
}
~sls_evaluator() {
m_mpz_manager.del(m_zero);
m_mpz_manager.del(m_one);
m_mpz_manager.del(m_two);
}
void operator()(app * n, mpz & result) {
family_id nfid = n->get_family_id();
func_decl * fd = n->get_decl();
unsigned n_args = n->get_num_args();
if (n_args == 0) {
m_mpz_manager.set(result, m_tracker.get_value(n));
return;
}
expr * const * args = n->get_args();
m_mpz_manager.set(result, m_zero);
if (nfid == m_basic_fid) {
switch (n->get_decl_kind()) {
case OP_AND: {
m_mpz_manager.set(result, m_one);
for (unsigned i = 0; i < n_args; i++)
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
m_mpz_manager.set(result, m_zero);
break;
}
break;
}
case OP_OR: {
for (unsigned i = 0; i < n_args; i++)
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
m_mpz_manager.set(result, m_one);
break;
}
break;
}
case OP_NOT: {
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child));
m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero);
break;
}
case OP_EQ: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_one);
const mpz & first = m_tracker.get_value(args[0]);
for (unsigned i = 1; i < n_args; i++)
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), first)) {
m_mpz_manager.set(result, m_zero);
break;
}
break;
}
case OP_DISTINCT: {
m_mpz_manager.set(result, m_one);
for (unsigned i = 0; i < n_args && m_mpz_manager.is_one(result); i++) {
for (unsigned j = i+1; j < n_args && m_mpz_manager.is_one(result); j++) {
if (m_mpz_manager.eq(m_tracker.get_value(args[i]), m_tracker.get_value(args[j])))
m_mpz_manager.set(result, m_zero);
}
}
break;
}
case OP_ITE: {
SASSERT(n_args = 3);
if (m_mpz_manager.is_one(m_tracker.get_value(args[0])))
m_mpz_manager.set(result, m_tracker.get_value(args[1]));
else
m_mpz_manager.set(result, m_tracker.get_value(args[2]));
break;
}
default:
NOT_IMPLEMENTED_YET();
}
}
else if (nfid == m_bv_fid) {
bv_op_kind k = static_cast<bv_op_kind>(fd->get_decl_kind());
switch(k) {
case OP_CONCAT: {
SASSERT(n_args >= 2);
for (unsigned i = 0; i < n_args; i++) {
if (i != 0) {
const mpz & p = m_powers(m_bv_util.get_bv_size(args[i]));
m_mpz_manager.mul(result, p, result);
}
m_mpz_manager.add(result, m_tracker.get_value(args[i]), result);
}
break;
}
case OP_EXTRACT: {
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
unsigned h = m_bv_util.get_extract_high(n);
unsigned l = m_bv_util.get_extract_low(n);
m_mpz_manager.rem(child, m_powers(h+1), result); // result = [h:0] of child
m_mpz_manager.machine_div2k(result, l, result);
break;
}
case OP_BADD: {
SASSERT(n_args >= 2);
for (unsigned i = 0; i < n_args; i++) {
const mpz & next = m_tracker.get_value(args[i]);
m_mpz_manager.add(result, next, result);
}
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
m_mpz_manager.rem(result, p, result);
break;
}
case OP_BSUB: {
SASSERT(n_args == 2);
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
mpz temp;
m_mpz_manager.sub(m_tracker.get_value(args[0]), m_tracker.get_value(args[1]), temp);
m_mpz_manager.mod(temp, p, result);
m_mpz_manager.del(temp);
break;
}
case OP_BMUL: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
const mpz & next = m_tracker.get_value(args[i]);
m_mpz_manager.mul(result, next, result);
}
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
m_mpz_manager.rem(result, p, result);
break;
}
case OP_BNEG: { // 2's complement unary minus
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
if (m_mpz_manager.is_zero(child)) {
m_mpz_manager.set(result, m_zero);
}
else {
unsigned bv_sz = m_bv_util.get_bv_size(n);
m_mpz_manager.bitwise_not(bv_sz, child, result);
m_mpz_manager.inc(result); // can't overflow
}
break;
}
case OP_BSDIV:
case OP_BSDIV0:
case OP_BSDIV_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
SASSERT(m_mpz_manager.is_nonneg(x) && m_mpz_manager.is_nonneg(y));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if (m_mpz_manager.is_zero(y)) {
if (m_mpz_manager.is_neg(x))
m_mpz_manager.set(result, m_one);
else {
m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n)));
m_mpz_manager.dec(result);
}
}
else {
m_mpz_manager.machine_div(x, y, result);
}
if (m_mpz_manager.is_neg(result))
m_mpz_manager.add(result, p, result);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BUDIV:
case OP_BUDIV0:
case OP_BUDIV_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
if (m_mpz_manager.is_zero(y)) {
m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n)));
m_mpz_manager.dec(result);
}
else {
m_mpz_manager.machine_div(x, y, result);
}
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BSREM:
case OP_BSREM0:
case OP_BSREM_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if (m_mpz_manager.is_zero(y)) {
m_mpz_manager.set(result, x);
}
else {
m_mpz_manager.rem(x, y, result);
}
if (m_mpz_manager.is_neg(result))
m_mpz_manager.add(result, p, result);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BUREM:
case OP_BUREM0:
case OP_BUREM_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
if (m_mpz_manager.is_zero(y)) {
m_mpz_manager.set(result, x);
}
else {
m_mpz_manager.mod(x, y, result);
}
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BSMOD:
case OP_BSMOD0:
case OP_BSMOD_I:{
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if (m_mpz_manager.is_zero(y))
m_mpz_manager.set(result, x);
else {
bool neg_x = m_mpz_manager.is_neg(x);
bool neg_y = m_mpz_manager.is_neg(y);
mpz abs_x, abs_y;
m_mpz_manager.set(abs_x, x);
m_mpz_manager.set(abs_y, y);
if (neg_x) m_mpz_manager.neg(abs_x);
if (neg_y) m_mpz_manager.neg(abs_y);
SASSERT(m_mpz_manager.is_nonneg(abs_x) && m_mpz_manager.is_nonneg(abs_y));
m_mpz_manager.mod(abs_x, abs_y, result);
if (m_mpz_manager.is_zero(result) || (!neg_x && !neg_y)) {
/* Nothing */
}
else if (neg_x && !neg_y) {
m_mpz_manager.neg(result);
m_mpz_manager.add(result, y, result);
}
else if (!neg_x && neg_y) {
m_mpz_manager.add(result, y, result);
}
else {
m_mpz_manager.neg(result);
}
m_mpz_manager.del(abs_x);
m_mpz_manager.del(abs_y);
}
if (m_mpz_manager.is_neg(result))
m_mpz_manager.add(result, p, result);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BAND: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++)
m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), result);
break;
}
case OP_BOR: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), result);
}
break;
}
case OP_BXOR: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++)
m_mpz_manager.bitwise_xor(result, m_tracker.get_value(args[i]), result);
break;
}
case OP_BNAND: {
SASSERT(n_args >= 2);
mpz temp;
unsigned bv_sz = m_bv_util.get_bv_size(n);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), temp);
m_mpz_manager.bitwise_not(bv_sz, temp, result);
}
m_mpz_manager.del(temp);
break;
}
case OP_BNOR: {
SASSERT(n_args >= 2);
mpz temp;
unsigned bv_sz = m_bv_util.get_bv_size(n);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), temp);
m_mpz_manager.bitwise_not(bv_sz, temp, result);
}
m_mpz_manager.del(temp);
break;
}
case OP_BNOT: {
SASSERT(n_args == 1);
m_mpz_manager.bitwise_not(m_bv_util.get_bv_size(args[0]), m_tracker.get_value(args[0]), result);
break;
}
case OP_ULT:
case OP_ULEQ:
case OP_UGT:
case OP_UGEQ: {
SASSERT(n_args == 2);
const mpz & x = m_tracker.get_value(args[0]);
const mpz & y = m_tracker.get_value(args[1]);
if ((k == OP_ULT && m_mpz_manager.lt(x, y)) ||
(k == OP_ULEQ && m_mpz_manager.le(x, y)) ||
(k == OP_UGT && m_mpz_manager.gt(x, y)) ||
(k == OP_UGEQ && m_mpz_manager.ge(x, y)))
m_mpz_manager.set(result, m_one);
break;
}
case OP_SLT:
case OP_SLEQ:
case OP_SGT:
case OP_SGEQ: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if ((k == OP_SLT && m_mpz_manager.lt(x, y)) ||
(k == OP_SLEQ && m_mpz_manager.le(x, y)) ||
(k == OP_SGT && m_mpz_manager.gt(x, y)) ||
(k == OP_SGEQ && m_mpz_manager.ge(x, y)))
m_mpz_manager.set(result, m_one);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BIT2BOOL: {
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
m_mpz_manager.set(result, child);
break;
}
case OP_BASHR: {
SASSERT(n_args == 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
mpz first;
const mpz & p = m_powers(m_bv_util.get_bv_size(args[0])-1);
m_mpz_manager.bitwise_and(result, p, first);
mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1]));
mpz temp;
while (!m_mpz_manager.is_zero(shift)) {
m_mpz_manager.machine_div(result, m_two, temp);
m_mpz_manager.add(temp, first, result);
m_mpz_manager.dec(shift);
}
m_mpz_manager.del(first);
m_mpz_manager.del(shift);
m_mpz_manager.del(temp);
break;
}
case OP_BLSHR: {
SASSERT(n_args == 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1]));
while (!m_mpz_manager.is_zero(shift)) {
m_mpz_manager.machine_div(result, m_two, result);
m_mpz_manager.dec(shift);
}
m_mpz_manager.del(shift);
break;
}
case OP_BSHL: {
SASSERT(n_args == 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1]));
while (!m_mpz_manager.is_zero(shift)) {
m_mpz_manager.mul(result, m_two, result);
m_mpz_manager.dec(shift);
}
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
m_mpz_manager.rem(result, p, result);
m_mpz_manager.del(shift);
break;
}
case OP_SIGN_EXT: {
SASSERT(n_args == 1);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
break;
}
default:
NOT_IMPLEMENTED_YET();
}
}
else {
NOT_IMPLEMENTED_YET();
}
TRACE("sls_eval", tout << "(" << fd->get_name();
for (unsigned i = 0; i < n_args; i++)
tout << " " << m_mpz_manager.to_string(m_tracker.get_value(args[i]));
tout << ") ---> " << m_mpz_manager.to_string(result);
if (m_manager.is_bool(fd->get_range())) tout << " [Boolean]";
else tout << " [vector size: " << m_bv_util.get_bv_size(fd->get_range()) << "]";
tout << std::endl; );
SASSERT(m_mpz_manager.is_nonneg(result));
}
void eval_checked(expr * n, mpz & result) {
switch(n->get_kind()) {
case AST_APP: {
app * a = to_app(n);
(*this)(a, result);
unsigned n_args = a->get_num_args();
m_temp_exprs.reset();
for (unsigned i = 0; i < n_args; i++) {
expr * arg = a->get_arg(i);
const mpz & v = m_tracker.get_value(arg);
m_temp_exprs.push_back(m_tracker.mpz2value(arg->get_sort(), v));
}
expr_ref q(m_manager), temp(m_manager);
q = m_manager.mk_app(a->get_decl(), m_temp_exprs.size(), m_temp_exprs.data());
model dummy_model(m_manager);
model_evaluator evaluator(dummy_model);
evaluator(q, temp);
mpz check_res;
m_tracker.value2mpz(temp, check_res);
CTRACE("sls", !m_mpz_manager.eq(check_res, result),
tout << "EVAL BUG: IS " << m_mpz_manager.to_string(result) <<
" SHOULD BE " << m_mpz_manager.to_string(check_res) << std::endl; );
SASSERT(m_mpz_manager.eq(check_res, result));
m_mpz_manager.del(check_res);
break;
}
default:
NOT_IMPLEMENTED_YET();
}
}
void run_serious_update(unsigned cur_depth) {
// precondition: m_traversal_stack contains the entry point(s)
expr_fast_mark1 visited;
mpz new_value;
double new_score;
SASSERT(cur_depth < m_traversal_stack.size());
while (cur_depth != static_cast<unsigned>(-1)) {
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
expr * cur = cur_depth_exprs[i];
(*this)(to_app(cur), new_value);
m_tracker.set_value(cur, new_value);
new_score = m_tracker.score(cur);
if (m_tracker.is_top_expr(cur))
{
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
if (m_mpz_manager.eq(new_value,m_one))
m_tracker.make_assertion(cur);
else
m_tracker.break_assertion(cur);
}
m_tracker.set_score(cur, new_score);
m_tracker.set_score_prune(cur, new_score);
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
m_traversal_stack[next_d].push_back(next);
visited.mark(next);
}
}
}
}
cur_depth_exprs.reset();
cur_depth--;
}
m_mpz_manager.del(new_value);
}
void run_update(unsigned cur_depth) {
// precondition: m_traversal_stack contains the entry point(s)
expr_fast_mark1 visited;
mpz new_value;
double new_score;
SASSERT(cur_depth < m_traversal_stack.size());
while (cur_depth != static_cast<unsigned>(-1)) {
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
expr * cur = cur_depth_exprs[i];
(*this)(to_app(cur), new_value);
m_tracker.set_value(cur, new_value);
new_score = m_tracker.score(cur);
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
m_traversal_stack[next_d].push_back(next);
visited.mark(next);
}
}
}
}
cur_depth_exprs.reset();
cur_depth--;
}
m_mpz_manager.del(new_value);
}
void update_all() {
unsigned max_depth = 0;
sls_tracker::entry_point_type::iterator start = m_tracker.get_entry_points().begin();
sls_tracker::entry_point_type::iterator end = m_tracker.get_entry_points().end();
for (sls_tracker::entry_point_type::iterator it = start; it != end; it++) {
expr * ep = m_tracker.get_entry_point(it->m_key);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
m_traversal_stack[cur_depth].push_back(ep);
if (cur_depth > max_depth) max_depth = cur_depth;
}
run_serious_update(max_depth);
}
void update(func_decl * fd, const mpz & new_value) {
m_tracker.set_value(fd, new_value);
expr * ep = m_tracker.get_entry_point(fd);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
m_traversal_stack[cur_depth].push_back(ep);
run_update(cur_depth);
}
void serious_update(func_decl * fd, const mpz & new_value) {
m_tracker.set_value(fd, new_value);
expr * ep = m_tracker.get_entry_point(fd);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
m_traversal_stack[cur_depth].push_back(ep);
run_serious_update(cur_depth);
}
unsigned run_update_bool_prune(unsigned cur_depth) {
expr_fast_mark1 visited;
double prune_score, new_score;
unsigned pot_benefits = 0;
SASSERT(cur_depth < m_traversal_stack_bool.size());
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack_bool[cur_depth];
for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
expr * cur = cur_depth_exprs[i];
new_score = m_tracker.score(cur);
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
prune_score = m_tracker.get_score_prune(cur);
m_tracker.set_score(cur, new_score);
if ((new_score > prune_score) && (m_tracker.has_pos_occ(cur)))
pot_benefits = 1;
if ((new_score <= prune_score) && (m_tracker.has_neg_occ(cur)))
pot_benefits = 1;
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
m_traversal_stack_bool[next_d].push_back(next);
visited.mark(next);
}
}
}
}
cur_depth_exprs.reset();
cur_depth--;
while (cur_depth != static_cast<unsigned>(-1)) {
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack_bool[cur_depth];
if (pot_benefits)
{
unsigned cur_size = cur_depth_exprs.size();
for (unsigned i = 0; i < cur_size; i++) {
expr * cur = cur_depth_exprs[i];
new_score = m_tracker.score(cur);
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
m_traversal_stack_bool[next_d].push_back(next);
visited.mark(next);
}
}
}
}
}
cur_depth_exprs.reset();
cur_depth--;
}
return pot_benefits;
}
void run_update_prune(unsigned max_depth) {
// precondition: m_traversal_stack contains the entry point(s)
expr_fast_mark1 visited;
mpz new_value;
unsigned cur_depth = max_depth;
SASSERT(cur_depth < m_traversal_stack.size());
while (cur_depth != static_cast<unsigned>(-1)) {
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
expr * cur = cur_depth_exprs[i];
(*this)(to_app(cur), new_value);
m_tracker.set_value(cur, new_value);
// Andreas: Should actually always have uplinks ...
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
if (m_manager.is_bool(next))
m_traversal_stack_bool[max_depth].push_back(next);
else
m_traversal_stack[next_d].push_back(next);
visited.mark(next);
}
}
}
}
cur_depth_exprs.reset();
cur_depth--;
}
m_mpz_manager.del(new_value);
}
unsigned update_prune(func_decl * fd, const mpz & new_value) {
m_tracker.set_value(fd, new_value);
expr * ep = m_tracker.get_entry_point(fd);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack_bool.size() <= cur_depth)
m_traversal_stack_bool.resize(cur_depth+1);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
if (m_manager.is_bool(ep))
m_traversal_stack_bool[cur_depth].push_back(ep);
else
{
m_traversal_stack[cur_depth].push_back(ep);
run_update_prune(cur_depth);
}
return run_update_bool_prune(cur_depth);
}
void randomize_local(ptr_vector<func_decl> & unsat_constants) {
// Randomize _one_ candidate:
unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size();
func_decl * fd = unsat_constants[r];
mpz temp = m_tracker.get_random(fd->get_range());
serious_update(fd, temp);
m_mpz_manager.del(temp);
TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;
tout << "Locally randomized model: " << std::endl;
m_tracker.show_model(tout); );
}
void randomize_local(expr * e) {
randomize_local(m_tracker.get_constants(e));
}
void randomize_local(ptr_vector<expr> const & as) {
randomize_local(m_tracker.get_unsat_constants(as));
}
};

47
src/ast/sls/sls_powers.h Normal file
View file

@ -0,0 +1,47 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
sls_powers.h
Abstract:
Power-of-2 module for SLS
Author:
Christoph (cwinter) 2012-02-29
Notes:
--*/
#pragma once
#include "util/mpz.h"
class powers : public u_map<mpz*> {
unsynch_mpz_manager & m;
public:
powers(unsynch_mpz_manager & m) : m(m) {}
~powers() {
for (iterator it = begin(); it != end(); it++) {
m.del(*it->m_value);
dealloc(it->m_value);
}
}
const mpz & operator()(unsigned n) {
u_map<mpz*>::iterator it = find_iterator(n);
if (it != end())
return *it->m_value;
else {
mpz * new_obj = alloc(mpz);
m.mul2k(m.mk_z(1), n, *new_obj);
insert(n, new_obj);
return *new_obj;
}
}
};

1094
src/ast/sls/sls_tracker.h Normal file
View file

File diff suppressed because it is too large Load diff