#pragma once
#include "model/model_evaluator.h"
#include "ast/sls/sls_powers.h"
#include "ast/sls/sls_bv_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); 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: { 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); }
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)) {
}
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]));
auto const& shift = m_tracker.get_value(args[1]);
if (m_mpz_manager.is_small(shift)) {
int s = m_mpz_manager.get_int(shift);
SASSERT(s >= 0);
m_mpz_manager.machine_div2k(result, s);
}
else
m_mpz_manager.set(result, m_zero);
break;
}
case OP_BSHL: {
SASSERT(n_args == 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
auto const& shift = m_tracker.get_value(args[1]);
if (m_mpz_manager.is_small(shift)) {
int s = m_mpz_manager.get_int(shift);
SASSERT(s >= 0);
int sz = m_bv_util.get_bv_size(n);
if (s >= sz)
m_mpz_manager.set(result, m_zero);
else {
m_mpz_manager.mul2k(result, s);
const mpz& p = m_powers(sz);
m_mpz_manager.rem(result, p, result);
}
}
else
m_mpz_manager.set(result, m_zero);
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) {
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) {
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;
for (auto const& [key, value] : m_tracker.get_entry_points()) {
expr* ep = m_tracker.get_entry_point(key);
unsigned cur_depth = m_tracker.get_distance(ep);
m_traversal_stack.reserve(cur_depth + 1);
m_traversal_stack[cur_depth].push_back(ep);
max_depth = std::max(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);
m_traversal_stack.reserve(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) {
TRACE(sls, tout << "set: " << fd->get_name() << " to " << m_mpz_manager.to_string(new_value) << std::endl;);
m_tracker.set_value(fd, new_value);
expr * ep = m_tracker.get_entry_point(fd);
unsigned cur_depth = m_tracker.get_distance(ep);
m_traversal_stack.reserve(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) {
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);
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) {
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));
}
};