mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt
Conflicts: src/tactic/sls/sls_compilation_settings.h Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
commit
ac206bacbf
|
@ -1,168 +0,0 @@
|
|||
/*++
|
||||
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_ 1
|
||||
// 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
|
File diff suppressed because it is too large
Load diff
|
@ -37,17 +37,13 @@ public:
|
|||
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;
|
||||
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_umins(0),
|
||||
m_mul2s(0),
|
||||
m_mul3s(0),
|
||||
m_div2s(0),
|
||||
m_flips(0),
|
||||
m_incs(0),
|
||||
m_decs(0),
|
||||
|
@ -75,13 +71,22 @@ protected:
|
|||
sls_evaluator m_evaluator;
|
||||
ptr_vector<expr> m_assertions;
|
||||
|
||||
unsigned m_restart_limit;
|
||||
unsigned m_max_restarts;
|
||||
unsigned m_plateau_limit;
|
||||
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;
|
||||
|
||||
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;
|
||||
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type;
|
||||
|
||||
public:
|
||||
sls_engine(ast_manager & m, params_ref const & p);
|
||||
|
@ -104,15 +109,11 @@ public:
|
|||
bool full_eval(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);
|
||||
|
||||
void init_tracker(void);
|
||||
|
||||
lbool search(void);
|
||||
|
||||
lbool operator()();
|
||||
|
@ -120,36 +121,25 @@ public:
|
|||
|
||||
protected:
|
||||
void checkpoint();
|
||||
double get_restart_armin(unsigned cnt_restarts);
|
||||
|
||||
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
|
||||
double & best_score, unsigned & best_const, mpz & best_value);
|
||||
bool what_if(expr * e, func_decl * fd, const mpz & temp,
|
||||
double & best_score, mpz & best_value, unsigned i);
|
||||
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();
|
||||
double rescore();
|
||||
double serious_score(func_decl * fd, const mpz & new_value);
|
||||
double incremental_score(func_decl * fd, const mpz & new_value);
|
||||
|
||||
#if _EARLY_PRUNE_
|
||||
double incremental_score_prune(func_decl * fd, const mpz & new_value);
|
||||
#endif
|
||||
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_local(expr * e, func_decl * fd, mpz & best_value, unsigned i);
|
||||
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);
|
||||
double find_best_move_vns(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);
|
||||
void mk_random_move();
|
||||
|
||||
bool handle_plateau(void);
|
||||
bool handle_plateau(double old_score);
|
||||
|
||||
//inline double get_restart_armin(unsigned cnt_restarts);
|
||||
inline unsigned check_restart(unsigned curr_value);
|
||||
};
|
||||
|
||||
|
|
|
@ -22,7 +22,6 @@ Notes:
|
|||
|
||||
#include"model_evaluator.h"
|
||||
|
||||
#include"sls_compilation_settings.h"
|
||||
#include"sls_powers.h"
|
||||
#include"sls_tracker.h"
|
||||
|
||||
|
@ -37,9 +36,7 @@ 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) :
|
||||
|
@ -81,11 +78,7 @@ 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;
|
||||
}
|
||||
|
@ -93,11 +86,7 @@ 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;
|
||||
}
|
||||
|
@ -105,16 +94,9 @@ 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);
|
||||
#endif
|
||||
break;
|
||||
}
|
||||
case OP_EQ: {
|
||||
|
@ -553,9 +535,7 @@ public:
|
|||
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)) {
|
||||
|
@ -567,37 +547,19 @@ public:
|
|||
(*this)(to_app(cur), new_value);
|
||||
m_tracker.set_value(cur, new_value);
|
||||
|
||||
#if _REAL_RS_ || _REAL_PBFS_
|
||||
//if (!m_tracker.has_uplinks(cur))
|
||||
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);
|
||||
}
|
||||
#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++) {
|
||||
|
@ -624,9 +586,7 @@ public:
|
|||
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)) {
|
||||
|
@ -637,26 +597,10 @@ public:
|
|||
|
||||
(*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.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
|
||||
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++) {
|
||||
|
@ -691,11 +635,7 @@ 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) {
|
||||
|
@ -720,7 +660,6 @@ public:
|
|||
run_serious_update(cur_depth);
|
||||
}
|
||||
|
||||
#if _EARLY_PRUNE_
|
||||
unsigned run_update_bool_prune(unsigned cur_depth) {
|
||||
expr_fast_mark1 visited;
|
||||
|
||||
|
@ -734,11 +673,9 @@ public:
|
|||
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
|
||||
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);
|
||||
|
||||
|
@ -759,9 +696,6 @@ public:
|
|||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
}
|
||||
}
|
||||
|
||||
cur_depth_exprs.reset();
|
||||
|
@ -775,15 +709,11 @@ public:
|
|||
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.adapt_top_sum(cur, 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++) {
|
||||
|
@ -820,7 +750,7 @@ public:
|
|||
|
||||
(*this)(to_app(cur), new_value);
|
||||
m_tracker.set_value(cur, new_value);
|
||||
// should always have uplinks ...
|
||||
// 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++) {
|
||||
|
@ -864,63 +794,18 @@ public:
|
|||
}
|
||||
return run_update_bool_prune(cur_depth);
|
||||
}
|
||||
#endif
|
||||
|
||||
void randomize_local(ptr_vector<func_decl> & unsat_constants) {
|
||||
// Randomize _all_ candidates:
|
||||
|
||||
//// bool did_something = false;
|
||||
//for (unsigned i = 0; i < unsat_constants.size(); i++) {
|
||||
// func_decl * fd = unsat_constants[i];
|
||||
// mpz temp = m_tracker.get_random(fd->get_range());
|
||||
// // if (m_mpz_manager.neq(temp, m_tracker.get_value(fd))) {
|
||||
// // did_something = true;
|
||||
// // }
|
||||
// update(fd, temp);
|
||||
// m_mpz_manager.del(temp);
|
||||
//}
|
||||
|
||||
// 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: ";
|
||||
for (unsigned i = 0; i < unsat_constants.size(); i++)
|
||||
tout << unsat_constants[i]->get_name() << ", ";
|
||||
tout << std::endl;*/
|
||||
tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;
|
||||
TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;
|
||||
tout << "Locally randomized model: " << std::endl;
|
||||
m_tracker.show_model(tout); );
|
||||
|
||||
|
@ -930,8 +815,8 @@ public:
|
|||
randomize_local(m_tracker.get_constants(e));
|
||||
}
|
||||
|
||||
void randomize_local(ptr_vector<expr> const & as, unsigned int flip) {
|
||||
randomize_local(m_tracker.get_unsat_constants(as, flip));
|
||||
void randomize_local(ptr_vector<expr> const & as) {
|
||||
randomize_local(m_tracker.get_unsat_constants(as));
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -2,7 +2,25 @@ def_module_params('sls',
|
|||
export=True,
|
||||
description='Experimental Stochastic Local Search Solver (for QFBV only).',
|
||||
params=(max_memory_param(),
|
||||
('restarts', UINT, UINT_MAX, '(max) number of restarts'),
|
||||
('plateau_limit', UINT, 10, 'pleateau limit'),
|
||||
('random_seed', UINT, 0, 'random seed')
|
||||
('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
|
||||
('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'),
|
||||
('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'),
|
||||
('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'),
|
||||
('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'),
|
||||
('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'),
|
||||
('walksat_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'),
|
||||
('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'),
|
||||
('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'),
|
||||
('paws_init', UINT, 40, 'initial/minimum assertion weights'),
|
||||
('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'),
|
||||
('wp', UINT, 100, 'random walk with probability wp / 1024'),
|
||||
('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'),
|
||||
('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'),
|
||||
('restart_base', UINT, 100, 'base restart interval given by moves per run'),
|
||||
('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
|
||||
('early_prune', BOOL, 1, 'use early pruning for score prediction'),
|
||||
('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
|
||||
('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
|
||||
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
|
||||
('random_seed', UINT, 0, 'random seed')
|
||||
))
|
||||
|
|
|
@ -148,16 +148,12 @@ 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));
|
||||
}
|
||||
|
||||
tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
|
||||
tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m));
|
||||
//tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m));
|
||||
t->updt_params(p);
|
||||
return t;
|
||||
}
|
||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -94,6 +94,32 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
mk_sat_tactic(m));
|
||||
#endif
|
||||
|
||||
/* use full sls
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
cond(mk_is_qfbv_probe(),
|
||||
cond(mk_is_qfbv_eq_probe(),
|
||||
and_then(mk_bv1_blaster_tactic(m),
|
||||
using_params(mk_smt_tactic(), solver_p)),
|
||||
and_then(mk_nnf_tactic(m, p), mk_sls_tactic(m))),
|
||||
mk_smt_tactic())),
|
||||
main_p);*/
|
||||
|
||||
/* use pure dpll
|
||||
tactic * st = using_params(and_then(mk_simplify_tactic(m),
|
||||
cond(mk_is_qfbv_probe(),
|
||||
and_then(mk_bit_blaster_tactic(m),
|
||||
when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)),
|
||||
and_then(using_params(and_then(mk_simplify_tactic(m),
|
||||
mk_solve_eqs_tactic(m)),
|
||||
local_ctx_p),
|
||||
if_no_proofs(cond(mk_produce_unsat_cores_probe(),
|
||||
mk_aig_tactic(),
|
||||
using_params(mk_aig_tactic(),
|
||||
big_aig_p))))),
|
||||
new_sat),
|
||||
mk_smt_tactic())),
|
||||
main_p);*/
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
// If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
|
||||
// symbols. In this case, we should not use
|
||||
|
|
Loading…
Reference in a new issue