mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-03-26 13:06:05 +00:00
commit 52390989dd
19 changed files with 2773 additions and 548 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/tactic/sat_tactic.cpp
View file

@ -66,7 +66,9 @@ class sat_tactic : public tactic {
CASSERT("sat_solver", m_solver.check_invariant());
IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
TRACE("sat_dimacs", m_solver.display_dimacs(tout););
//m_solver.display_dimacs(std::cerr);
//exit(0);
lbool r = m_solver.check();
if (r == l_false) {
g->assert_expr(m.mk_false(), 0, 0);

4
src/tactic/portfolio/default_tactic.cpp
View file

@ -28,10 +28,12 @@ Notes:
#include"probe_arith.h"
#include"quant_tactics.h"
#include"qffpa_tactic.h"
#include"sls_tactic.h"
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
tactic * st = using_params(and_then(mk_simplify_tactic(m),
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m),
cond(mk_is_qfbv_probe(), mk_qfbv_sls_tactic(m),
// cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m),
cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),

5
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -37,11 +37,14 @@ Notes:
#include"horn_tactic.h"
#include"smt_solver.h"
#include"sls_tactic.h"
tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
if (logic=="QF_UF")
return mk_qfuf_tactic(m, p);
else if (logic=="QF_BV")
return mk_qfbv_tactic(m, p);
// return mk_qfbv_tactic(m, p);
return mk_qfbv_sls_tactic(m, p);
else if (logic=="QF_IDL")
return mk_qfidl_tactic(m, p);
else if (logic=="QF_LIA")

168
src/tactic/sls/sls_compilation_settings.h Normal file
View file

@ -0,0 +1,168 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sls_compilation_constants.h
Abstract:
Stochastic Local Search (SLS) compilation constants
Author:
Christoph (cwinter) 2014-03-19
Notes:
This file should go away completely once we have evaluated all options.
--*/
#ifndef _SLS_COMPILATION_SETTINGS_H_
#define _SLS_COMPILATION_SETTINGS_H_
// which unsatisfied assertion is selected? only works with _FOCUS_ > 0
// 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score
#define _BFS_ 0
// how many terms are considered for variable selection?
// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT), 2 = only one bottom level atom
#define _FOCUS_ 1
// probability of choosing the same assertion again in the next step
#define _PERC_STICKY_ 0
// do we use dirty unit propagation to get rid of nested top level assertions?
#define _DIRTY_UP_ 0
// do we use restarts?
// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time
#define _RESTARTS_ 3
// limit of moves/plateaus/seconds until first restart occurs
#define _RESTART_LIMIT_ 10
// 0 = initialize with all zero, 1 initialize with random value
#define _RESTART_INIT_ 0
// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat
#define _RESTART_SCHEME_ 1
// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3
#define _RESTART_CONST_ARMIN_ 3.0
// timelimit
#define _TIMELIMIT_ 3600
// should score of conjunctions be calculated by average rather than max?
#define _SCORE_AND_AVG_ 0
// should score of discunctions be calculated by multiplication of the inverse score rather than min?
#define _SCORE_OR_MUL_ 0
// do we use some kind of variable neighbourhood-search?
// 0 = no, 1 = only consider flipping bits if no better score can be obtained otherwise, 2 = only consider flipping bits until a better score can be obtained
#define _VNS_ 0
// do we reduce the score of unsatisfied literals?
// 0 = no
// 1 = yes, by multiplying it with some factor
// 2 = yes, by squaring it
// 3 = yes, by setting it to zero
// 4 = by progessively increasing weight (_TIMELIMIT_ needs to be set appropriately!)
#define _WEIGHT_DIST_ 1
// the factor used for _WEIGHT_DIST_ = 1
#define _WEIGHT_DIST_FACTOR_ 0.25
// shall we toggle the weight after each restart?
#define _WEIGHT_TOGGLE_ 0
// do we use intensification steps in local minima? if so, how many?
#define _INTENSIFICATION_ 0
#define _INTENSIFICATION_TRIES_ 0
// what is the percentage of random moves in plateaus (instead of full randomization)?
#define _PERC_PLATEAU_MOVES_ 0
// shall we repick clause when randomizing in a plateau or use the current one?
#define _REPICK_ 1
// do we use some UCT-like scheme for assertion-selection? overrides _BFS_
#define _UCT_ 1
// how much diversification is used in the UCT-scheme?
#define _UCT_CONSTANT_ 10.0
// is uct clause selection probabilistic similar to variable selection in sparrow?
// 0 = no, 1 = yes, use uct-value, 2 = yes, use score-value (_UCT_CONSTANT_ = 0.0) with squared score
#define _PROBABILISTIC_UCT_ 0
// additive constants for probabilistic uct > 0
#define _UCT_EPS_ 0.0001
// shall we reset _UCT_ touched values after restart?
#define _UCT_RESET_ 0
// how shall we initialize the _UCT_ total touched counter?
// 0 = initialize with one, 1 = initialize with number of assertions
#define _UCT_INIT_ 1
// do we gradually reduce the touched values of _UCT_?
#define _UCT_FORGET_ 0
#define _UCT_FORGET_FACTOR_ 0.5
// shall we use addition/subtraction?
#define _USE_ADDSUB_ 1
// shall we try multilication and division by 2?
#define _USE_MUL2DIV2_ 0
// shall we try multiplication by 3?
#define _USE_MUL3_ 0
// shall we try unary minus (= inverting and incrementing)
#define _USE_UNARY_MINUS_ 0
// is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0
#define _UNIFORM_RANDOM_ 0
// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
#define _REAL_RS_ 0
#define _REAL_PBFS_ 0
// how many bits do we neglect in each iteration?
#define _SKIP_BITS_ 0
// when randomizing local, what is the probability for changing a single bit?
// 0 = use standard scheme and pick a new value at random (= 50), otherwise the value (as int) gives the percentage
#define _PERC_CHANGE_ 0
// do we use random steps for noise?
// 0 = no, 1 = randomize local, 2 = make random move
#define _TYPE_RSTEP_ 0
// with what probability _PERM_STEP_/1000 will the random step happen?
#define _PERM_RSTEP_ 0
// shall we use early pruning for incremental update?
#define _EARLY_PRUNE_ 1
// shall we use caching for top_score?
#define _CACHE_TOP_SCORE_ 1
#if ((_BFS_ > 0) + (_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1)
InvalidConfiguration;
#endif
#if (_PROBABILISTIC_UCT_ && !_UCT_)
InvalidConfiguration;
#endif
#if (_PERM_RSTEP_ && !_TYPE_RSTEP_)
InvalidConfiguration;
#endif
#if (_PERC_CHANGE_ == 50)
InvalidConfiguration;
#endif
#if (_PERC_STICKY_ && !_FOCUS_)
InvalidConfiguration;
#endif
#endif

1160
src/tactic/sls/sls_engine.cpp Normal file
View file

File diff suppressed because it is too large Load diff

159
src/tactic/sls/sls_engine.h Normal file
View file

@ -0,0 +1,159 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sls_engine.h
Abstract:
A Stochastic Local Search (SLS) engine
Author:
Christoph (cwinter) 2014-03-19
Notes:
--*/
#ifndef _SLS_ENGINE_H_
#define _SLS_ENGINE_H_
#include"stopwatch.h"
#include"lbool.h"
#include"model_converter.h"
#include"sls_compilation_settings.h"
#include"sls_tracker.h"
#include"sls_evaluator.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, m_umins, m_mul2s, m_mul3s, m_div2s;
stats() :
m_restarts(0),
m_full_evals(0),
m_incr_evals(0),
m_moves(0),
m_umins(0),
m_mul2s(0),
m_mul3s(0),
m_div2s(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;
bool m_produce_models;
volatile bool m_cancel;
bv_util m_bv_util;
sls_tracker m_tracker;
sls_evaluator m_evaluator;
unsigned m_restart_limit;
unsigned m_max_restarts;
unsigned m_plateau_limit;
ptr_vector<mpz> m_old_values;
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV, MV_UMIN, MV_MUL2, MV_MUL3, MV_DIV2 } move_type;
public:
sls_engine(ast_manager & m, params_ref const & p);
~sls_engine();
ast_manager & m() const { return m_manager; }
void set_cancel(bool f) { m_cancel = f; }
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
void updt_params(params_ref const & _p);
stats const & get_stats(void) { return m_stats; }
void reset_statistics(void) { m_stats.reset(); }
bool full_eval(goal_ref const & g, model & mdl);
void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result);
void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result);
void mk_div2(unsigned bv_sz, const mpz & old_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);
double find_best_move(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_local(expr * e, ptr_vector<func_decl> & to_evaluate,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp,
double & best_score, mpz & best_value, unsigned i);
double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i);
lbool search(goal_ref const & g);
void operator()(goal_ref const & g, model_converter_ref & mc);
protected:
void checkpoint();
lbool search_old(goal_ref const & g);
double get_restart_armin(unsigned cnt_restarts);
bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
bool what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
double top_score(goal_ref const & g);
double rescore(goal_ref const & g);
double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
#if _EARLY_PRUNE_
double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value);
#endif
double find_best_move_vns(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
void mk_random_move(ptr_vector<func_decl> & unsat_constants);
void mk_random_move(goal_ref const & g);
bool handle_plateau(goal_ref const & g);
bool handle_plateau(goal_ref const & g, double old_score);
inline unsigned check_restart(unsigned curr_value);
};
#endif

322
src/tactic/sls/sls_evaluator.h
View file

@ -20,6 +20,9 @@ Notes:
#ifndef _SLS_EVALUATOR_H_
#define _SLS_EVALUATOR_H_
#include"model_evaluator.h"
#include"sls_compilation_settings.h"
#include"sls_powers.h"
#include"sls_tracker.h"
@ -34,6 +37,9 @@ class sls_evaluator {
powers & m_powers;
expr_ref_buffer m_temp_exprs;
vector<ptr_vector<expr> > m_traversal_stack;
#if _EARLY_PRUNE_
vector<ptr_vector<expr> > m_traversal_stack_bool;
#endif
public:
sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) :
@ -75,7 +81,11 @@ public:
case OP_AND: {
m_mpz_manager.set(result, m_one);
for (unsigned i = 0; i < n_args; i++)
#if _DIRTY_UP_
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) && !m_tracker.is_top_expr(args[i])) {
#else
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
#endif
m_mpz_manager.set(result, m_zero);
break;
}
@ -83,7 +93,11 @@ public:
}
case OP_OR: {
for (unsigned i = 0; i < n_args; i++)
#if _DIRTY_UP_
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result) || m_tracker.is_top_expr(args[i])) {
#else
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
#endif
m_mpz_manager.set(result, m_one);
break;
}
@ -91,9 +105,16 @@ public:
}
case OP_NOT: {
SASSERT(n_args == 1);
#if _DIRTY_UP_
if (m_tracker.is_top_expr(args[0]))
m_mpz_manager.set(result, m_zero);
else
m_mpz_manager.set(result, (m_mpz_manager.is_zero(m_tracker.get_value(args[0]))) ? m_one : m_zero);
#else
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);
m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero);
#endif
break;
}
case OP_EQ: {
@ -519,11 +540,15 @@ public:
}
}
void run_update(unsigned cur_depth) {
void run_serious_update(unsigned cur_depth) {
// precondition: m_traversal_stack contains the entry point(s)
expr_fast_mark1 visited;
mpz new_value;
#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
double new_score;
#endif
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];
@ -533,8 +558,97 @@ public:
(*this)(to_app(cur), new_value);
m_tracker.set_value(cur, new_value);
m_tracker.set_score(cur, m_tracker.score(cur));
#if _REAL_RS_ || _REAL_PBFS_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
{
if (m_mpz_manager.eq(new_value,m_one))
m_tracker.make_assertion(cur);
else
m_tracker.break_assertion(cur);
}
#endif
#if _EARLY_PRUNE_
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
#endif
m_tracker.set_score(cur, new_score);
m_tracker.set_score_prune(cur, new_score);
#else
#if _CACHE_TOP_SCORE_
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
#endif
#endif
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;
#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
double new_score;
#endif
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);
#if _EARLY_PRUNE_
new_score = m_tracker.score(cur);
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
#endif
m_tracker.set_score(cur, new_score);
m_tracker.set_score_prune(cur, new_score);
#else
#if _CACHE_TOP_SCORE_
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
#endif
#endif
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
@ -569,8 +683,11 @@ public:
m_traversal_stack[cur_depth].push_back(ep);
if (cur_depth > max_depth) max_depth = cur_depth;
}
#if _REAL_RS_ || _REAL_PBFS_
run_serious_update(max_depth);
#else
run_update(max_depth);
#endif
}
void update(func_decl * fd, const mpz & new_value) {
@ -584,9 +701,164 @@ public:
run_update(cur_depth);
}
void randomize_local(goal_ref const & g) {
ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g);
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);
}
#if _EARLY_PRUNE_
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 _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
#endif
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);
}
}
}
else
{
}
}
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];
#if _CACHE_TOP_SCORE_
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
#endif
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);
// should 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);
}
#endif
void randomize_local(ptr_vector<func_decl> & unsat_constants) {
// Randomize _all_ candidates:
//// bool did_something = false;
@ -603,8 +875,37 @@ public:
// Randomize _one_ candidate:
unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size();
func_decl * fd = unsat_constants[r];
#if _PERC_CHANGE_
sort * srt = fd->get_range();
mpz temp;
if (m_manager.is_bool(srt))
m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
else
{
mpz temp2, mask;
unsigned bv_sz = m_bv_util.get_bv_size(srt);
m_mpz_manager.set(temp, m_tracker.get_value(fd));
for (unsigned bit = 0; bit < bv_sz; bit++)
if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_)
{
m_mpz_manager.set(mask, m_powers(bit));
m_mpz_manager.bitwise_xor(temp, mask, temp2);
m_mpz_manager.set(temp, temp2);
}
m_mpz_manager.del(mask);
m_mpz_manager.del(temp2);
}
#else
mpz temp = m_tracker.get_random(fd->get_range());
#endif
#if _REAL_RS_ || _REAL_PBFS_
serious_update(fd, temp);
#else
update(fd, temp);
#endif
m_mpz_manager.del(temp);
TRACE("sls", /*tout << "Randomization candidates: ";
@ -614,6 +915,15 @@ public:
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(goal_ref const & g, unsigned int flip) {
randomize_local(m_tracker.get_unsat_constants(g, flip));
}
};

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

@ -16,507 +16,30 @@ Author:
Notes:
--*/
#include<iomanip>
#include"map.h"
#include"nnf.h"
#include"cooperate.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
#include"var_subst.h"
#include"model_pp.h"
#include"model_evaluator.h"
#include"solve_eqs_tactic.h"
#include"elim_uncnstr_tactic.h"
#include"bv_size_reduction_tactic.h"
#include"max_bv_sharing_tactic.h"
#include"simplify_tactic.h"
#include"stopwatch.h"
#include"propagate_values_tactic.h"
#include"sls_tactic.h"
#include"ctx_simplify_tactic.h"
#include"elim_uncnstr_tactic.h"
#include"nnf_tactic.h"
#include"stopwatch.h"
#include"sls_tactic.h"
#include"sls_params.hpp"
#include"sls_evaluator.h"
#include"sls_tracker.h"
#include"sls_engine.h"
class sls_tactic : public tactic {
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();
}
};
struct imp {
ast_manager & m_manager;
stats & m_stats;
unsynch_mpz_manager m_mpz_manager;
powers m_powers;
mpz m_zero, m_one, m_two;
bool m_produce_models;
volatile bool m_cancel;
bv_util m_bv_util;
sls_tracker m_tracker;
sls_evaluator m_evaluator;
unsigned m_max_restarts;
unsigned m_plateau_limit;
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type;
imp(ast_manager & m, params_ref const & p, stats & s) :
m_manager(m),
m_stats(s),
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_cancel(false),
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);
}
~imp() {
m_mpz_manager.del(m_zero);
m_mpz_manager.del(m_one);
m_mpz_manager.del(m_two);
}
ast_manager & m() const { return m_manager; }
void set_cancel(bool f) { m_cancel = f; }
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
static void collect_param_descrs(param_descrs & r) {
sls_params::collect_param_descrs(r);
}
void updt_params(params_ref const & _p) {
sls_params p(_p);
m_produce_models = _p.get_bool("model", false);
m_max_restarts = p.restarts();
m_tracker.set_random_seed(p.random_seed());
m_plateau_limit = p.plateau_limit();
}
void checkpoint() {
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
cooperate("sls");
}
bool full_eval(goal_ref const & g, model & mdl) {
bool res = true;
unsigned sz = g->size();
for (unsigned i = 0; i < sz && res; i++) {
checkpoint();
expr_ref o(m_manager);
if (!mdl.eval(g->form(i), o, true))
exit(ERR_INTERNAL_FATAL);
res = m_manager.is_true(o.get());
}
TRACE("sls", tout << "Evaluation: " << res << std::endl;);
return res;
}
double top_score(goal_ref const & g) {
#if 0
double min = m_tracker.get_score(g->form(0));
unsigned sz = g->size();
for (unsigned i = 1; i < sz; i++) {
double q = m_tracker.get_score(g->form(i));
if (q < min) min = q;
}
TRACE("sls_top", tout << "Score distribution:";
for (unsigned i = 0; i < sz; i++)
tout << " " << m_tracker.get_score(g->form(i));
tout << " MIN: " << min << std::endl; );
return min;
#else
double top_sum = 0.0;
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
top_sum += m_tracker.get_score(g->form(i));
}
TRACE("sls_top", tout << "Score distribution:";
for (unsigned i = 0; i < sz; i++)
tout << " " << m_tracker.get_score(g->form(i));
tout << " AVG: " << top_sum / (double) sz << std::endl; );
return top_sum / (double) sz;
#endif
}
double rescore(goal_ref const & g) {
m_evaluator.update_all();
m_stats.m_full_evals++;
return top_score(g);
}
double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
m_evaluator.update(fd, new_value);
m_stats.m_incr_evals++;
return top_score(g);
}
bool what_if(goal_ref const & g, 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 = incremental_score(g, 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
if (r >= best_score) {
best_score = r;
best_const = fd_inx;
m_mpz_manager.set(best_value, temp);
return true;
}
return false;
}
void 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 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 mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted) {
m_mpz_manager.bitwise_not(bv_sz, old_value, inverted);
}
void 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 mk_random_move(goal_ref const & g) {
unsigned rnd_mv = 0;
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++;
move_type mt = (move_type) rnd_mv;
// inversion doesn't make sense, let's do a flip instead.
if (mt == MV_INV) mt = MV_FLIP;
ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g);
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;
unsigned bit = 0;
switch (mt)
{
case MV_FLIP: {
unsigned bv_sz = m_bv_util.get_bv_size(fd->get_range());
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();
}
m_evaluator.update(fd, new_value);
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_mpz_manager.del(new_value);
}
double find_best_move(goal_ref const & g, 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;
for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0 ; 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 && new_score < 1.0; j++) {
// What would happen if we flipped bit #i ?
mk_flip(srt, old_value, j, temp);
if (what_if(g, 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(g, 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(g, fd, i, temp, new_score, best_const, best_value))
move = MV_DEC;
}
// try inverting
mk_inv(bv_sz, old_value, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
}
// reset to what it was before
double check = incremental_score(g, fd, old_value);
SASSERT(check == score);
}
m_mpz_manager.del(old_value);
m_mpz_manager.del(temp);
return new_score;
}
lbool search(goal_ref const & g) {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit = 0;
mpz new_value;
move_type move;
score = rescore(g);
TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl;
tout << "Score distribution:";
for (unsigned i = 0; i < g->size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i));
tout << " TOP: " << score << std::endl; );
unsigned plateau_cnt = 0;
while (plateau_cnt < m_plateau_limit) {
do {
checkpoint();
old_score = score;
new_const = (unsigned)-1;
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g);
TRACE("sls_constants", tout << "Evaluating these constants: " << std::endl;
for (unsigned i = 0 ; i < to_evaluate.size(); i++)
tout << to_evaluate[i]->get_name() << std::endl; );
score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move);
if (new_const == static_cast<unsigned>(-1)) {
TRACE("sls", tout << "Local maximum reached; unsatisfied constraints: " << std::endl;
for (unsigned i = 0; i < g->size(); i++) {
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
tout << mk_ismt2_pp(g->form(i), m_manager) << std::endl;
});
TRACE("sls_max", m_tracker.show_model(tout);
tout << "Scores: " << std::endl;
for (unsigned i = 0; i < g->size(); i++)
tout << mk_ismt2_pp(g->form(i), m_manager) << " ---> " <<
m_tracker.get_score(g->form(i)) << std::endl; );
score = old_score;
}
else {
m_stats.m_moves++;
func_decl * fd = to_evaluate[new_const];
TRACE("sls", tout << "Setting " << fd->get_name() << " to " << m_mpz_manager.to_string(new_value) << " (Move: ";
switch (move) {
case MV_FLIP:
tout << "Flip";
if (!m_manager.is_bool(fd->get_range())) tout << " #" << new_bit;
break;
case MV_INC:
tout << "+1";
break;
case MV_DEC:
tout << "-1";
break;
case MV_INV:
tout << "NEG";
break;
};
tout << ") ; new score = " << std::setprecision(32) << score << std::endl; );
switch (move) {
case MV_FLIP: m_stats.m_flips++; break;
case MV_INC: m_stats.m_incs++; break;
case MV_DEC: m_stats.m_decs++; break;
case MV_INV: m_stats.m_invs++; break;
}
score = incremental_score(g, fd, new_value);
TRACE("sls", tout << "Score distribution:";
for (unsigned i = 0; i < g->size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i));
tout << " TOP: " << score << std::endl; );
}
if (score >= 1.0) {
// score could theoretically be imprecise.
bool all_true = true;
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
all_true=false;
if (all_true) {
res = l_true; // sat
goto bailout;
} else
TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;);
}
}
while (score > old_score && res == l_undef);
if (score != old_score)
plateau_cnt = 0;
else {
plateau_cnt++;
if (plateau_cnt < m_plateau_limit) {
TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl; );
m_evaluator.randomize_local(g);
//mk_random_move(g);
score = top_score(g);
}
}
}
bailout:
m_mpz_manager.del(new_value);
return res;
}
void operator()(goal_ref const & g, model_converter_ref & mc) {
if (g->inconsistent()) {
mc = 0;
return;
}
m_tracker.initialize(g);
lbool res = l_undef;
do {
checkpoint();
if ((m_stats.m_restarts % 100) == 0)
report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
res = search(g);
if (res == l_undef)
m_tracker.randomize();
}
while (res != l_true && m_stats.m_restarts++ < m_max_restarts);
if (res == l_true) {
if (m_produce_models) {
model_ref mdl = m_tracker.get_model();
mc = model2model_converter(mdl.get());
TRACE("sls_model", mc->display(tout); );
}
g->reset();
}
else
mc = 0;
}
};
class sls_tactic : public tactic {
ast_manager & m;
params_ref m_params;
imp * m_imp;
stats m_stats;
sls_engine * m_engine;
public:
sls_tactic(ast_manager & _m, params_ref const & p):
m(_m),
m_params(p) {
m_imp = alloc(imp, m, p, m_stats);
m_engine = alloc(sls_engine, m, p);
}
virtual tactic * translate(ast_manager & m) {
@ -524,16 +47,16 @@ public:
}
virtual ~sls_tactic() {
dealloc(m_imp);
dealloc(m_engine);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
m_imp->updt_params(p);
m_engine->updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
imp::collect_param_descrs(r);
sls_params::collect_param_descrs(r);
}
virtual void operator()(goal_ref const & g,
@ -541,14 +64,13 @@ public:
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
m_imp->m_produce_models = g->models_enabled();
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0; result.reset();
TRACE("sls", g->display(tout););
tactic_report report("sls", *g);
m_imp->operator()(g, mc);
m_engine->operator()(g, mc);
g->inc_depth();
result.push_back(g.get());
@ -557,40 +79,41 @@ public:
}
virtual void cleanup() {
imp * d = m_imp;
sls_engine * d = m_engine;
#pragma omp critical (tactic_cancel)
{
d = m_imp;
d = m_engine;
}
dealloc(d);
d = alloc(imp, m, m_params, m_stats);
d = alloc(sls_engine, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
m_engine = d;
}
}
virtual void 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);
sls_engine::stats const & stats = m_engine->get_stats();
double seconds = stats.m_stopwatch.get_current_seconds();
st.update("sls restarts", stats.m_restarts);
st.update("sls full evals", stats.m_full_evals);
st.update("sls incr evals", stats.m_incr_evals);
st.update("sls incr evals/sec", stats.m_incr_evals / seconds);
st.update("sls FLIP moves", stats.m_flips);
st.update("sls INC moves", stats.m_incs);
st.update("sls DEC moves", stats.m_decs);
st.update("sls INV moves", stats.m_invs);
st.update("sls moves", stats.m_moves);
st.update("sls moves/sec", stats.m_moves / seconds);
}
virtual void reset_statistics() {
m_stats.reset();
m_engine->reset_statistics();
}
virtual void set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
if (m_engine)
m_engine->set_cancel(f);
}
};
@ -625,6 +148,9 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
// conservative gaussian elimination.
gaussian_p.set_uint("gaussian_max_occs", 2);
params_ref ctx_p;
ctx_p.set_uint("max_depth", 32);
ctx_p.set_uint("max_steps", 5000000);
return and_then(and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
using_params(mk_solve_eqs_tactic(m), gaussian_p),
@ -633,6 +159,11 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
using_params(mk_simplify_tactic(m), simp2_p)),
using_params(mk_simplify_tactic(m), hoist_p),
mk_max_bv_sharing_tactic(m),
// Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this?
//mk_ctx_simplify_tactic(m, ctx_p),
// Andreas: This one at least eliminates top level duplicates ...
//mk_simplify_tactic(m),
// Andreas: How does a NNF actually look like? Can it contain ITE operators?
mk_nnf_tactic(m, p));
}

830
src/tactic/sls/sls_tracker.h
View file

@ -20,6 +20,12 @@ Notes:
#ifndef _SLS_TRACKER_H_
#define _SLS_TRACKER_H_
#include"goal.h"
#include"model.h"
#include"sls_compilation_settings.h"
#include"sls_powers.h"
class sls_tracker {
ast_manager & m_manager;
unsynch_mpz_manager & m_mpz_manager;
@ -28,21 +34,32 @@ class sls_tracker {
random_gen m_rng;
unsigned m_random_bits;
unsigned m_random_bits_cnt;
mpz m_zero, m_one, m_two;
mpz m_zero, m_one, m_two;
struct value_score {
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { };
#if _EARLY_PRUNE_
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1), score_prune(0.0), has_pos_occ(0), has_neg_occ(0) { };
#else
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1) { };
#endif
~value_score() { if (m) m->del(value); }
unsynch_mpz_manager * m;
mpz value;
double score;
#if _EARLY_PRUNE_
double score_prune;
unsigned has_pos_occ;
unsigned has_neg_occ;
#endif
unsigned distance; // max distance from any root
unsigned touched;
value_score & operator=(const value_score & other) {
SASSERT(m == 0 || m == other.m);
if (m) m->set(value, 0); else m = other.m;
m->set(value, other.value);
score = other.score;
distance = other.distance;
touched = other.touched;
return *this;
}
};
@ -54,12 +71,27 @@ private:
typedef obj_map<expr, value_score> scores_type;
typedef obj_map<expr, ptr_vector<expr> > uplinks_type;
typedef obj_map<expr, ptr_vector<func_decl> > occ_type;
obj_hashtable<expr> m_top_expr;
scores_type m_scores;
uplinks_type m_uplinks;
entry_point_type m_entry_points;
ptr_vector<func_decl> m_constants;
ptr_vector<func_decl> m_temp_constants;
occ_type m_constants_occ;
#if _UCT_
unsigned m_touched;
#endif
#if _REAL_RS_ || _REAL_PBFS_
ptr_vector<expr> m_unsat_expr;
obj_map<expr, unsigned> m_where_false;
expr** m_list_false;
#endif
#if _CACHE_TOP_SCORE_
double m_top_sum;
#endif
#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_
double m_weight_dist_factor;
#endif
public:
sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) :
@ -79,6 +111,26 @@ public:
m_mpz_manager.del(m_two);
}
#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_
inline void set_weight_dist_factor(double val) {
m_weight_dist_factor = val;
}
#endif
#if _CACHE_TOP_SCORE_
inline void adapt_top_sum(double add, double sub) {
m_top_sum += add - sub;
}
inline void set_top_sum(double new_score) {
m_top_sum = new_score;
}
inline double get_top_sum() {
return m_top_sum;
}
#endif
inline void set_value(expr * n, const mpz & r) {
SASSERT(m_scores.contains(n));
m_mpz_manager.set(m_scores.find(n).value, r);
@ -123,6 +175,28 @@ public:
return get_score(ep);
}
#if _EARLY_PRUNE_
inline void set_score_prune(expr * n, double score) {
SASSERT(m_scores.contains(n));
m_scores.find(n).score_prune = score;
}
inline double & get_score_prune(expr * n) {
SASSERT(m_scores.contains(n));
return m_scores.find(n).score_prune;
}
inline unsigned has_pos_occ(expr * n) {
SASSERT(m_scores.contains(n));
return m_scores.find(n).has_pos_occ;
}
inline unsigned has_neg_occ(expr * n) {
SASSERT(m_scores.contains(n));
return m_scores.find(n).has_neg_occ;
}
#endif
inline unsigned get_distance(expr * n) {
SASSERT(m_scores.contains(n));
return m_scores.find(n).distance;
@ -146,11 +220,76 @@ public:
return m_uplinks.contains(n);
}
inline bool is_top_expr(expr * n) {
return m_top_expr.contains(n);
}
inline ptr_vector<expr> & get_uplinks(expr * n) {
SASSERT(m_uplinks.contains(n));
return m_uplinks.find(n);
}
#if _REAL_RS_ || _REAL_PBFS_
void debug_real(goal_ref const & g, unsigned flip)
{
unsigned count = 0;
for (unsigned i = 0; i < g->size(); i++)
{
expr * e = g->form(i);
if (m_mpz_manager.eq(get_value(e),m_one) && m_where_false.contains(e))
{
printf("iteration %d: ", flip);
printf("form %d is sat but in unsat list at position %d of %d\n", i, m_where_false.find(e), m_where_false.size());
exit(4);
}
if (m_mpz_manager.eq(get_value(e),m_zero) && !m_where_false.contains(e))
{
printf("iteration %d: ", flip);
printf("form %d is unsat but not in unsat list\n", i);
exit(4);
}
if (m_mpz_manager.eq(get_value(e),m_zero) && m_where_false.contains(e))
{
unsigned pos = m_where_false.find(e);
expr * q = m_list_false[pos];
if (q != e)
{
printf("iteration %d: ", flip);
printf("form %d is supposed to be at pos %d in unsat list but something else was there\n", i, pos);
exit(4);
}
}
if (m_mpz_manager.eq(get_value(e),m_zero))
count++;
}
// should be true now that duplicate assertions are removed
if (count != m_where_false.size())
{
printf("iteration %d: ", flip);
printf("%d are unsat but list is of size %d\n", count, m_where_false.size());
exit(4);
}
}
#endif
void uct_forget(goal_ref const & g) {
expr * e;
unsigned touched_old, touched_new;
for (unsigned i = 0; i < g->size(); i++)
{
e = g->form(i);
touched_old = m_scores.find(e).touched;
touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
m_scores.find(e).touched = touched_new;
m_touched += touched_new - touched_old;
}
}
void initialize(app * n) {
// Build score table
if (!m_scores.contains(n)) {
@ -249,12 +388,50 @@ public:
}
}
void initialize_recursive(init_proc proc, expr_mark visited, expr * e) {
if (m_manager.is_and(e) || m_manager.is_or(e)) {
app * a = to_app(e);
expr * const * args = a->get_args();
unsigned int sz = a->get_num_args();
for (unsigned int i = 0; i < sz; i++) {
expr * q = args[i];
initialize_recursive(proc, visited, q);
}
}
for_each_expr(proc, visited, e);
}
void initialize_recursive(expr * e) {
if (m_manager.is_and(e) || m_manager.is_or(e)) {
app * a = to_app(e);
expr * const * args = a->get_args();
unsigned int sz = a->get_num_args();
for (unsigned int i = 0; i < sz; i++) {
expr * q = args[i];
initialize_recursive(q);
}
}
ptr_vector<func_decl> t;
m_constants_occ.insert_if_not_there(e, t);
find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e));
expr_fast_mark1 visited;
quick_for_each_expr(ffd_proc, visited, e);
}
void initialize(goal_ref const & g) {
init_proc proc(m_manager, *this);
expr_mark visited;
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
expr * e = g->form(i);
if (!m_top_expr.contains(e))
m_top_expr.insert(e);
else
printf("this is already in ...\n");
// Andreas: Maybe not fully correct.
#if _FOCUS_ == 2
initialize_recursive(proc, visited, e);
#endif
for_each_expr(proc, visited, e);
}
@ -262,6 +439,10 @@ public:
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
// Andreas: Maybe not fully correct.
#if _FOCUS_ == 2 || _INTENSIFICATION_
initialize_recursive(e);
#endif
ptr_vector<func_decl> t;
m_constants_occ.insert_if_not_there(e, t);
find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e));
@ -272,8 +453,65 @@ public:
calculate_expr_distances(g);
TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); );
#if _REAL_RS_ || _REAL_PBFS_
m_list_false = new expr*[sz];
//for (unsigned i = 0; i < sz; i++)
//{
// if (m_mpz_manager.eq(get_value(g->form(i)),m_zero))
// break_assertion(g->form(i));
//}
#endif
#if _EARLY_PRUNE_
for (unsigned i = 0; i < sz; i++)
setup_occs(g->form(i));
#endif
#if _UCT_
m_touched = _UCT_INIT_ ? g->size() : 1;
#endif
}
#if _REAL_RS_ || _REAL_PBFS_
void make_assertion(expr * e)
{
if (m_where_false.contains(e))
{
unsigned pos = m_where_false.find(e);
m_where_false.erase(e);
if (pos != m_where_false.size())
{
expr * q = m_list_false[m_where_false.size()];
m_list_false[pos] = q;
m_where_false.find(q) = pos;
//printf("Moving %d from %d to %d\n", q, m_where_false.size(), pos);
}
//else
//printf("Erasing %d from %d to %d\n", e, pos);
// m_list_false[m_where_false.size()] = 0;
// printf("Going in %d\n", m_where_false.size());
}
//if (m_unsat_expr.contains(e))
//m_unsat_expr.erase(e);
}
void break_assertion(expr * e)
{
//printf("I'm broken... that's still fine.\n");
if (!m_where_false.contains(e))
{
//printf("This however is not so cool...\n");
unsigned pos = m_where_false.size();
m_list_false[pos] = e;
m_where_false.insert(e, pos);
// printf("Going in %d\n", m_where_false.size());
}
//if (!m_unsat_expr.contains(e))
//m_unsat_expr.push_back(e);
}
#endif
void show_model(std::ostream & out) {
unsigned sz = get_num_constants();
for (unsigned i = 0; i < sz; i++) {
@ -368,7 +606,7 @@ public:
NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
}
void randomize() {
void randomize(goal_ref const & g) {
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
@ -380,9 +618,64 @@ public:
}
TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); );
#if _UCT_RESET_
m_touched = _UCT_INIT_ ? g->size() : 1;
for (unsigned i = 0; i < g->size(); i++)
m_scores.find(g->form(i)).touched = 1;
#endif
}
#define _SCORE_AND_MIN
void reset(goal_ref const & g) {
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
mpz temp = m_zero;
set_value(it->m_value, temp);
m_mpz_manager.del(temp);
}
#if _UCT_RESET_
m_touched = _UCT_INIT_ ? g->size() : 1;
for (unsigned i = 0; i < g->size(); i++)
m_scores.find(g->form(i)).touched = 1;
#endif
}
#if _EARLY_PRUNE_
void setup_occs(expr * n, bool negated = false) {
if (m_manager.is_bool(n))
{
if (m_manager.is_and(n) || m_manager.is_or(n))
{
SASSERT(!negated);
app * a = to_app(n);
expr * const * args = a->get_args();
for (unsigned i = 0; i < a->get_num_args(); i++)
setup_occs(args[i]);
}
else if (m_manager.is_not(n))
{
SASSERT(!negated);
app * a = to_app(n);
SASSERT(a->get_num_args() == 1);
expr * child = a->get_arg(0);
if (m_manager.is_and(child) || m_manager.is_or(child))
NOT_IMPLEMENTED_YET();
setup_occs(child, true);
}
else
{
if (negated)
m_scores.find(n).has_neg_occ = 1;
else
m_scores.find(n).has_pos_occ = 1;
}
}
else
NOT_IMPLEMENTED_YET();
}
#endif
double score_bool(expr * n, bool negated = false) {
TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; );
@ -400,30 +693,57 @@ public:
SASSERT(!negated);
app * a = to_app(n);
expr * const * args = a->get_args();
#ifdef _SCORE_AND_MIN
// Andreas: Seems to have no effect. Probably it does not even occur.
#if _SCORE_AND_AVG_
double sum = 0.0;
for (unsigned i = 0; i < a->get_num_args(); i++)
#if _DIRTY_UP_
sum += is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
#else
sum += get_score(args[i]);
#endif
res = sum / (double) a->get_num_args();
#else
double min = 1.0;
for (unsigned i = 0; i < a->get_num_args(); i++) {
#if _DIRTY_UP_
double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
#else
double cur = get_score(args[i]);
#endif
if (cur < min) min = cur;
}
res = min;
#else
double sum = 0.0;
for (unsigned i = 0; i < a->get_num_args(); i++)
sum += get_score(args[i]);
res = sum / (double) a->get_num_args();
#endif
#endif
}
else if (m_manager.is_or(n)) {
SASSERT(!negated);
app * a = to_app(n);
expr * const * args = a->get_args();
// Andreas: Seems to have no effect. Probably it is still too similar to the original version.
#if _SCORE_OR_MUL_
double inv = 1.0;
for (unsigned i = 0; i < a->get_num_args(); i++) {
#if _DIRTY_UP_
double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
#else
double cur = get_score(args[i]);
#endif
inv *= (1.0 - get_score(args[i]));
}
res = 1.0 - inv;
#else
double max = 0.0;
for (unsigned i = 0; i < a->get_num_args(); i++) {
#if _DIRTY_UP_
double cur = is_top_expr(args[i]) ? 1.0 : get_score(args[i]);
#else
double cur = get_score(args[i]);
#endif
if (cur > max) max = cur;
}
res = max;
#endif
}
else if (m_manager.is_ite(n)) {
SASSERT(!negated);
@ -441,7 +761,7 @@ public:
expr * arg1 = a->get_arg(1);
const mpz & v0 = get_value(arg0);
const mpz & v1 = get_value(arg1);
if (negated) {
res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0;
TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " <<
@ -468,7 +788,7 @@ public:
}
m_mpz_manager.machine_div(diff, m_two, diff);
}
res = 1.0 - (hamming_distance / (double) bv_sz);
res = 1.0 - (hamming_distance / (double) bv_sz);
#else
rational r(diff);
r /= m_powers(bv_sz);
@ -574,7 +894,11 @@ public:
expr * child = a->get_arg(0);
if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF.
NOT_IMPLEMENTED_YET();
#if _DIRTY_UP_
res = is_top_expr(child) ? 0.0 : score_bool(child, true);
#else
res = score_bool(child, true);
#endif
}
else if (m_manager.is_distinct(n)) {
app * a = to_app(n);
@ -598,10 +922,30 @@ public:
SASSERT(res >= 0.0 && res <= 1.0);
#if _WEIGHT_DIST_
app * a = to_app(n);
family_id afid = a->get_family_id();
if (afid == m_bv_util.get_family_id())
#endif
#if _WEIGHT_DIST_ == 1
#if _WEIGHT_TOGGLE_
if (res < 1.0) res *= m_weight_dist_factor;
#else
if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_;
#endif
#elif _WEIGHT_DIST_ == 2
res *= res;
#elif _WEIGHT_DIST_ == 3
if (res < 1.0) res = 0.0;
#elif _WEIGHT_DIST_ == 4
if (res < 1.0) res *= m_weight_dist_factor;
#endif
TRACE("sls_score", tout << "SCORE = " << res << std::endl; );
return res;
}
double score_bv(expr * n) {
return 0.0; // a bv-expr is always scored as 0.0; we won't use those scores.
}
@ -647,29 +991,455 @@ public:
NOT_IMPLEMENTED_YET();
}
ptr_vector<func_decl> & get_unsat_constants(goal_ref const & g) {
expr * get_unsat_expression(expr * e) {
if (m_manager.is_bool(e)) {
if (m_manager.is_and(e) || m_manager.is_or(e)) {
app * a = to_app(e);
expr * const * args = a->get_args();
// Andreas: might be used for guided branching
//for (unsigned i = 0; i < a->get_num_args(); i++) {
//double cur = get_score(args[i]);
//}
// Andreas: A random number is better here since reusing flip will cause patterns.
unsigned int sz = a->get_num_args();
unsigned int pos = get_random_uint(16) % sz;
for (unsigned int i = pos; i < sz; i++) {
expr * q = args[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return get_unsat_expression(q);
}
for (unsigned int i = 0; i < pos; i++) {
expr * q = args[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return get_unsat_expression(q);
}
}
}
return e;
}
ptr_vector<func_decl> & get_constants(expr * e) {
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
unsigned sz = this_decls.size();
for (unsigned i = 0; i < sz; i++) {
func_decl * fd = this_decls[i];
if (!m_temp_constants.contains(fd))
m_temp_constants.push_back(fd);
}
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) {
if (sz == 1)
return get_constants();
m_temp_constants.reset();
for (unsigned i = 0; i < sz; i++) {
expr * q = g->form(i);
if (m_mpz_manager.eq(get_value(q), m_one))
continue;
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
unsigned sz2 = this_decls.size();
for (unsigned j = 0; j < sz2; j++) {
func_decl * fd = this_decls[j];
if (!m_temp_constants.contains(fd))
m_temp_constants.push_back(fd);
}
}
return m_temp_constants;
}
expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) {
for (unsigned i = pos; i < sz; i++) {
expr * q = g->form(i);
if (m_mpz_manager.neq(get_value(q), m_one))
return q;
}
for (unsigned i = 0; i < pos; i++) {
expr * q = g->form(i);
if (m_mpz_manager.neq(get_value(q), m_one))
return q;
}
return 0;
}
ptr_vector<func_decl> & get_unsat_constants_walksat(goal_ref const & g, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(g, sz, pos);
// Andreas: I should probably fix this. If this is the case then the formula is SAT anyway but this is not checked in the first iteration.
if (!q)
return m_temp_constants;
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
unsigned sz2 = this_decls.size();
for (unsigned j = 0; j < sz2; j++) {
func_decl * fd = this_decls[j];
if (!m_temp_constants.contains(fd))
m_temp_constants.push_back(fd);
}
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_walksat(expr * e) {
if (!e || m_temp_constants.size())
return m_temp_constants;
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
unsigned sz = this_decls.size();
for (unsigned j = 0; j < sz; j++) {
func_decl * fd = this_decls[j];
if (!m_temp_constants.contains(fd))
m_temp_constants.push_back(fd);
}
return m_temp_constants;
}
ptr_vector<func_decl> & go_deeper(expr * e) {
if (m_manager.is_bool(e)) {
if (m_manager.is_and(e)) {
app * a = to_app(e);
expr * const * args = a->get_args();
// Andreas: might be used for guided branching
//for (unsigned i = 0; i < a->get_num_args(); i++) {
//double cur = get_score(args[i]);
//}
// Andreas: A random number is better here since reusing flip will cause patterns.
unsigned int sz = a->get_num_args();
unsigned int pos = get_random_uint(16) % sz;
for (unsigned int i = pos; i < sz; i++) {
expr * q = args[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return go_deeper(q);
}
for (unsigned int i = 0; i < pos; i++) {
expr * q = args[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return go_deeper(q);
}
}
else if (m_manager.is_or(e)) {
app * a = to_app(e);
expr * const * args = a->get_args();
unsigned int sz = a->get_num_args();
unsigned int pos = get_random_uint(16) % sz;
for (unsigned int i = pos; i < sz; i++) {
expr * q = args[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return go_deeper(q);
}
for (unsigned int i = 0; i < pos; i++) {
expr * q = args[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return go_deeper(q);
}
}
}
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
unsigned sz2 = this_decls.size();
for (unsigned j = 0; j < sz2; j++) {
func_decl * fd = this_decls[j];
if (!m_temp_constants.contains(fd))
m_temp_constants.push_back(fd);
}
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_crsat(goal_ref const & g, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(g, sz, pos);
if (!q)
return m_temp_constants;
return go_deeper(q);
}
ptr_vector<func_decl> & get_unsat_constants(goal_ref const & g, unsigned int flip) {
unsigned sz = g->size();
if (sz == 1) {
return get_constants();
if (m_mpz_manager.eq(get_value(g->form(0)), m_one))
return m_temp_constants;
else
return get_constants();
}
else {
m_temp_constants.reset();
for (unsigned i = 0; i < sz; i++) {
expr * q = g->form(i);
if (m_mpz_manager.eq(get_value(q), m_one))
continue;
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
unsigned sz2 = this_decls.size();
for (unsigned j = 0; j < sz2; j++) {
func_decl * fd = this_decls[j];
if (!m_temp_constants.contains(fd))
m_temp_constants.push_back(fd);
}
#if _FOCUS_ == 1
#if _UCT_
unsigned pos = -1;
value_score vscore;
#if _PROBABILISTIC_UCT_
double sum_score = 0.0;
unsigned start_index = get_random_uint(16) % sz;
for (unsigned i = start_index; i < sz; i++)
{
expr * e = g->form(i);
vscore = m_scores.find(e);
#if _PROBABILISTIC_UCT_ == 2
double q = vscore.score * vscore.score;
#else
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_;
#endif
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
sum_score += q;
if (rand() <= (q * RAND_MAX / sum_score) + 1)
pos = i;
}
}
return m_temp_constants;
for (unsigned i = 0; i < start_index; i++)
{
expr * e = g->form(i);
vscore = m_scores.find(e);
#if _PROBABILISTIC_UCT_ == 2
double q = vscore.score * vscore.score;
#else
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_;
#endif
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
sum_score += q;
if (rand() <= (q * RAND_MAX / sum_score) + 1)
pos = i;
}
}
#else
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
// for (unsigned i = 0; i < m_where_false.size(); i++) {
// expr * e = m_list_false[i];
vscore = m_scores.find(e);
#if _UCT_ == 1
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched)/vscore.touched);
#elif _UCT_ == 2
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
#elif _UCT_ == 3
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16));
#endif
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
}
#endif
if (pos == static_cast<unsigned>(-1))
return m_temp_constants;
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++;
m_touched++;
#elif _UCT_ == 2
m_scores.find(g->form(pos)).touched = flip;
#endif
expr * e = g->form(pos);
// expr * e = m_list_false[pos];
#elif _BFS_ == 3
unsigned int pos = -1;
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
double q = get_score(e);
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
}
if (pos == static_cast<unsigned>(-1))
return m_temp_constants;
expr * e = g->form(pos);
#elif _BFS_ == 2
unsigned int pos = -1;
double min = 2.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
double q = get_score(e);
if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; }
}
if (pos == static_cast<unsigned>(-1))
return m_temp_constants;
expr * e = g->form(pos);
#elif _BFS_ == 1
// I guess it was buggy ...
// unsigned int pos = flip % m_constants.size();
unsigned int pos = flip % sz;
expr * e = get_unsat_assertion(g, sz, pos);
#elif _UNIFORM_RANDOM_
unsigned cnt_unsat = 0, pos = -1;
for (unsigned i = 0; i < sz; i++)
if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;
if (pos == static_cast<unsigned>(-1))
return m_temp_constants;
expr * e = g->form(pos);
#elif _REAL_RS_
//unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
//expr * e = get_unsat_assertion(g, sz, pos);
//expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()];
sz = m_where_false.size();
if (sz == 0)
return m_temp_constants;
expr * e = m_list_false[get_random_uint(16) % sz];
#elif _REAL_PBFS_
//unsigned pos = m_false_list[flip % m_cnt_false];
//expr * e = get_unsat_assertion(g, sz, pos);
//expr * e = m_unsat_expr[flip % m_unsat_expr.size()];
sz = m_where_false.size();
if (sz == 0)
return m_temp_constants;
else
expr * e = m_list_false[flip % sz];
#else
// I guess it was buggy ...
// unsigned int pos = get_random_uint(16) % m_constants.size();
unsigned int pos = get_random_uint(16) % sz;
expr * e = get_unsat_assertion(g, sz, pos);
#endif
return get_unsat_constants_walksat(e);
#elif _FOCUS_ == 2
#if _BFS_
// I guess it was buggy ...
// unsigned int pos = flip % m_constants.size();
unsigned int pos = flip % sz;
#else
// I guess it was buggy ...
// unsigned int pos = get_random_uint(16) % m_constants.size();
unsigned int pos = get_random_uint(16) % sz;
#endif
return get_unsat_constants_crsat(g, sz, pos);
#else
return get_unsat_constants_gsat(g, sz);
#endif
}
}
expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) {
unsigned sz = g->size();
if (sz == 1)
return g->form(0);
m_temp_constants.reset();
#if _FOCUS_ == 1
#if _UCT_
unsigned pos = -1;
value_score vscore;
#if _PROBABILISTIC_UCT_
double sum_score = 0.0;
unsigned start_index = get_random_uint(16) % sz;
for (unsigned i = start_index; i < sz; i++)
{
expr * e = g->form(i);
vscore = m_scores.find(e);
#if _PROBABILISTIC_UCT_ == 2
double q = vscore.score * vscore.score + _UCT_EPS_;
#else
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_;
#endif
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
sum_score += q;
if (rand() <= (q * RAND_MAX / sum_score) + 1)
pos = i;
}
}
for (unsigned i = 0; i < start_index; i++)
{
expr * e = g->form(i);
vscore = m_scores.find(e);
#if _PROBABILISTIC_UCT_ == 2
double q = vscore.score * vscore.score + _UCT_EPS_;
#else
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + _UCT_EPS_;
#endif
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
sum_score += q;
if (rand() <= (q * RAND_MAX / sum_score) + 1)
pos = i;
}
}
#else
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
// for (unsigned i = 0; i < m_where_false.size(); i++) {
// expr * e = m_list_false[i];
vscore = m_scores.find(e);
#if _UCT_ == 1
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched);
#elif _UCT_ == 2
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
#elif _UCT_ == 3
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16));
#endif
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
}
#endif
if (pos == static_cast<unsigned>(-1))
return 0;
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++;
m_touched++;
#elif _UCT_ == 2
m_scores.find(g->form(pos)).touched = flip;
#endif
// return m_list_false[pos];
return g->form(pos);
#elif _BFS_ == 3
unsigned int pos = -1;
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
double q = get_score(e);
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
if (pos == static_cast<unsigned>(-1))
return 0;
return g->form(pos);
#elif _BFS_ == 2
unsigned int pos = -1;
double min = 2.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
double q = get_score(e);
if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; }
}
if (pos == static_cast<unsigned>(-1))
return 0;
return g->form(pos);
#elif _BFS_ == 1
unsigned int pos = flip % sz;
return get_unsat_assertion(g, sz, pos);
#elif _UNIFORM_RANDOM_
unsigned cnt_unsat = 0, pos = -1;
for (unsigned i = 0; i < sz; i++)
if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;
if (pos == static_cast<unsigned>(-1))
return 0;
return g->form(pos);
#elif _REAL_RS_
//unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
//expr * e = get_unsat_assertion(g, sz, pos);
//expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()];
sz = m_where_false.size();
if (sz == 0)
return 0;
return m_list_false[get_random_uint(16) % sz];
#elif _REAL_PBFS_
//unsigned pos = m_false_list[flip % m_cnt_false];
//expr * e = get_unsat_assertion(g, sz, pos);
//expr * e = m_unsat_expr[flip % m_unsat_expr.size()];
sz = m_where_false.size();
if (sz == 0)
return0;
else
return m_list_false[flip % sz];
#else
unsigned int pos = get_random_uint(16) % sz;
return get_unsat_assertion(g, sz, pos);
#endif
return g->form(pos);
#elif _FOCUS_ == 2
#if _BFS_
unsigned int pos = flip % sz;
#else
unsigned int pos = get_random_uint(16) % sz;
#endif
return get_unsat_constants_crsat(g, sz, pos);
#endif
}
};
#endif