diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h new file mode 100644 index 000000000..77ff50454 --- /dev/null +++ b/src/tactic/sls/sls_evaluator.h @@ -0,0 +1,620 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_evaluator.h + +Abstract: + + SLS Evaluator + +Author: + + Christoph (cwinter) 2012-02-29 + +Notes: + +--*/ + +#ifndef _SLS_EVALUATOR_H_ +#define _SLS_EVALUATOR_H_ + +#include"sls_powers.h" +#include"sls_tracker.h" + +class sls_evaluator { + ast_manager & m_manager; + bv_util & m_bv_util; + family_id m_basic_fid; + family_id m_bv_fid; + sls_tracker & m_tracker; + unsynch_mpz_manager & m_mpz_manager; + mpz m_zero, m_one, m_two; + powers & m_powers; + expr_ref_buffer m_temp_exprs; + vector > m_traversal_stack; + +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; + } + default: + NOT_IMPLEMENTED_YET(); + } + } + else if (nfid == m_bv_fid) { + bv_op_kind k = static_cast(fd->get_decl_kind()); + switch(k) { + case OP_CONCAT: { + SASSERT(n_args >= 2); + for (unsigned i = 0; i < n_args; i++) { + if (i != 0) { + const mpz & p = m_powers(m_bv_util.get_bv_size(args[i])); + m_mpz_manager.mul(result, p, result); + } + m_mpz_manager.add(result, m_tracker.get_value(args[i]), result); + } + break; + } + case OP_EXTRACT: { + SASSERT(n_args == 1); + const mpz & child = m_tracker.get_value(args[0]); + unsigned h = m_bv_util.get_extract_high(n); + unsigned l = m_bv_util.get_extract_low(n); + + m_mpz_manager.rem(child, m_powers(h+1), result); // result = [h:0] of child + m_mpz_manager.machine_div2k(result, l, result); + break; + } + case OP_BADD: { + SASSERT(n_args >= 2); + for (unsigned i = 0; i < n_args; i++) { + const mpz & next = m_tracker.get_value(args[i]); + m_mpz_manager.add(result, next, result); + } + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + m_mpz_manager.rem(result, p, result); + break; + } + case OP_BSUB: { + SASSERT(n_args == 2); + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + mpz temp; + m_mpz_manager.sub(m_tracker.get_value(args[0]), m_tracker.get_value(args[1]), temp); + m_mpz_manager.mod(temp, p, result); + m_mpz_manager.del(temp); + break; + } + case OP_BMUL: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + const mpz & next = m_tracker.get_value(args[i]); + m_mpz_manager.mul(result, next, result); + } + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + m_mpz_manager.rem(result, p, result); + break; + } + case OP_BNEG: { // 2's complement unary minus + SASSERT(n_args == 1); + const mpz & child = m_tracker.get_value(args[0]); + if (m_mpz_manager.is_zero(child)) { + m_mpz_manager.set(result, m_zero); + } + else { + unsigned bv_sz = m_bv_util.get_bv_size(n); + m_mpz_manager.bitwise_not(bv_sz, child, result); + m_mpz_manager.inc(result); // can't overflow + } + break; + } + case OP_BSDIV: + case OP_BSDIV0: + case OP_BSDIV_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + SASSERT(m_mpz_manager.is_nonneg(x) && m_mpz_manager.is_nonneg(y)); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + + if (m_mpz_manager.is_zero(y)) { + if (m_mpz_manager.is_neg(x)) + m_mpz_manager.set(result, m_one); + else { + m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); + m_mpz_manager.dec(result); + } + } + else { + m_mpz_manager.machine_div(x, y, result); + } + if (m_mpz_manager.is_neg(result)) + m_mpz_manager.add(result, p, result); + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BUDIV: + case OP_BUDIV0: + case OP_BUDIV_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + + if (m_mpz_manager.is_zero(y)) { + m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); + m_mpz_manager.dec(result); + } + else { + m_mpz_manager.machine_div(x, y, result); + } + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BSREM: + case OP_BSREM0: + case OP_BSREM_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + + if (m_mpz_manager.is_zero(y)) { + m_mpz_manager.set(result, x); + } + else { + m_mpz_manager.rem(x, y, result); + } + if (m_mpz_manager.is_neg(result)) + m_mpz_manager.add(result, p, result); + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BUREM: + case OP_BUREM0: + case OP_BUREM_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + + if (m_mpz_manager.is_zero(y)) { + m_mpz_manager.set(result, x); + } + else { + m_mpz_manager.mod(x, y, result); + } + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BSMOD: + case OP_BSMOD0: + case OP_BSMOD_I:{ + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + + if (m_mpz_manager.is_zero(y)) + m_mpz_manager.set(result, x); + else { + bool neg_x = m_mpz_manager.is_neg(x); + bool neg_y = m_mpz_manager.is_neg(y); + mpz abs_x, abs_y; + m_mpz_manager.set(abs_x, x); + m_mpz_manager.set(abs_y, y); + if (neg_x) m_mpz_manager.neg(abs_x); + if (neg_y) m_mpz_manager.neg(abs_y); + SASSERT(m_mpz_manager.is_nonneg(abs_x) && m_mpz_manager.is_nonneg(abs_y)); + + m_mpz_manager.mod(abs_x, abs_y, result); + + if (m_mpz_manager.is_zero(result) || (!neg_x && !neg_y)) { + /* Nothing */ + } + else if (neg_x && !neg_y) { + m_mpz_manager.neg(result); + m_mpz_manager.add(result, y, result); + } + else if (!neg_x && neg_y) { + m_mpz_manager.add(result, y, result); + } + else { + m_mpz_manager.neg(result); + } + + m_mpz_manager.del(abs_x); + m_mpz_manager.del(abs_y); + } + + if (m_mpz_manager.is_neg(result)) + m_mpz_manager.add(result, p, result); + + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BAND: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) + m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), result); + break; + } + case OP_BOR: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), result); + } + break; + } + case OP_BXOR: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) + m_mpz_manager.bitwise_xor(result, m_tracker.get_value(args[i]), result); + break; + } + case OP_BNAND: { + SASSERT(n_args >= 2); + mpz temp; + unsigned bv_sz = m_bv_util.get_bv_size(n); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), temp); + m_mpz_manager.bitwise_not(bv_sz, temp, result); + } + m_mpz_manager.del(temp); + break; + } + case OP_BNOR: { + SASSERT(n_args >= 2); + mpz temp; + unsigned bv_sz = m_bv_util.get_bv_size(n); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), temp); + m_mpz_manager.bitwise_not(bv_sz, temp, result); + } + m_mpz_manager.del(temp); + break; + } + case OP_BNOT: { + SASSERT(n_args == 1); + m_mpz_manager.bitwise_not(m_bv_util.get_bv_size(args[0]), m_tracker.get_value(args[0]), result); + break; + } + case OP_ULT: + case OP_ULEQ: + case OP_UGT: + case OP_UGEQ: { + SASSERT(n_args == 2); + const mpz & x = m_tracker.get_value(args[0]); + const mpz & y = m_tracker.get_value(args[1]); + if ((k == OP_ULT && m_mpz_manager.lt(x, y)) || + (k == OP_ULEQ && m_mpz_manager.le(x, y)) || + (k == OP_UGT && m_mpz_manager.gt(x, y)) || + (k == OP_UGEQ && m_mpz_manager.ge(x, y))) + m_mpz_manager.set(result, m_one); + break; + } + case OP_SLT: + case OP_SLEQ: + case OP_SGT: + case OP_SGEQ: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + if ((k == OP_SLT && m_mpz_manager.lt(x, y)) || + (k == OP_SLEQ && m_mpz_manager.le(x, y)) || + (k == OP_SGT && m_mpz_manager.gt(x, y)) || + (k == OP_SGEQ && m_mpz_manager.ge(x, y))) + m_mpz_manager.set(result, m_one); + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BIT2BOOL: { + SASSERT(n_args == 1); + const mpz & child = m_tracker.get_value(args[0]); + m_mpz_manager.set(result, child); + break; + } + case OP_BASHR: { + SASSERT(n_args == 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + mpz first; + const mpz & p = m_powers(m_bv_util.get_bv_size(args[0])-1); + m_mpz_manager.bitwise_and(result, p, first); + mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); + mpz temp; + while (!m_mpz_manager.is_zero(shift)) { + m_mpz_manager.machine_div(result, m_two, temp); + m_mpz_manager.add(temp, first, result); + m_mpz_manager.dec(shift); + } + m_mpz_manager.del(first); + m_mpz_manager.del(shift); + m_mpz_manager.del(temp); + break; + } + case OP_BLSHR: { + SASSERT(n_args == 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); + while (!m_mpz_manager.is_zero(shift)) { + m_mpz_manager.machine_div(result, m_two, result); + m_mpz_manager.dec(shift); + } + m_mpz_manager.del(shift); + break; + } + case OP_BSHL: { + SASSERT(n_args == 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); + while (!m_mpz_manager.is_zero(shift)) { + m_mpz_manager.mul(result, m_two, result); + m_mpz_manager.dec(shift); + } + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + m_mpz_manager.rem(result, p, result); + m_mpz_manager.del(shift); + break; + } + case OP_SIGN_EXT: { + SASSERT(n_args == 1); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + break; + } + default: + NOT_IMPLEMENTED_YET(); + } + } + else { + NOT_IMPLEMENTED_YET(); + } + + TRACE("sls_eval", tout << "(" << fd->get_name(); + for (unsigned i = 0; i < n_args; i++) + tout << " " << m_mpz_manager.to_string(m_tracker.get_value(args[i])); + tout << ") ---> " << m_mpz_manager.to_string(result); + if (m_manager.is_bool(fd->get_range())) tout << " [Boolean]"; + else tout << " [vector size: " << m_bv_util.get_bv_size(fd->get_range()) << "]"; + tout << std::endl; ); + + SASSERT(m_mpz_manager.is_nonneg(result)); + } + + void eval_checked(expr * n, mpz & result) { + switch(n->get_kind()) { + case AST_APP: { + app * a = to_app(n); + (*this)(a, result); + + unsigned n_args = a->get_num_args(); + m_temp_exprs.reset(); + for (unsigned i = 0; i < n_args; i++) { + expr * arg = a->get_arg(i); + const mpz & v = m_tracker.get_value(arg); + m_temp_exprs.push_back(m_tracker.mpz2value(m_manager.get_sort(arg), v)); + } + expr_ref q(m_manager), temp(m_manager); + q = m_manager.mk_app(a->get_decl(), m_temp_exprs.size(), m_temp_exprs.c_ptr()); + 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_update(unsigned cur_depth) { + // precondition: m_traversal_stack contains the entry point(s) + expr_fast_mark1 visited; + mpz new_value; + + SASSERT(cur_depth < m_traversal_stack.size()); + while (cur_depth != static_cast(-1)) { + ptr_vector & 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); + m_tracker.set_score(cur, m_tracker.score(cur)); + + if (m_tracker.has_uplinks(cur)) { + ptr_vector & ups = m_tracker.get_uplinks(cur); + for (unsigned j = 0; j < ups.size(); j++) { + expr * next = ups[j]; + unsigned next_d = m_tracker.get_distance(next); + SASSERT(next_d < cur_depth); + if (!visited.is_marked(next)) { + m_traversal_stack[next_d].push_back(next); + visited.mark(next); + } + } + } + } + + cur_depth_exprs.reset(); + cur_depth--; + } + + m_mpz_manager.del(new_value); + } + + void update_all() { + unsigned max_depth = 0; + + sls_tracker::entry_point_type::iterator start = m_tracker.get_entry_points().begin(); + sls_tracker::entry_point_type::iterator end = m_tracker.get_entry_points().end(); + for (sls_tracker::entry_point_type::iterator it = start; it != end; it++) { + expr * ep = m_tracker.get_entry_point(it->m_key); + unsigned cur_depth = m_tracker.get_distance(ep); + if (m_traversal_stack.size() <= cur_depth) + m_traversal_stack.resize(cur_depth+1); + m_traversal_stack[cur_depth].push_back(ep); + if (cur_depth > max_depth) max_depth = cur_depth; + } + + run_update(max_depth); + } + + void update(func_decl * fd, const mpz & new_value) { + m_tracker.set_value(fd, new_value); + expr * ep = m_tracker.get_entry_point(fd); + unsigned cur_depth = m_tracker.get_distance(ep); + if (m_traversal_stack.size() <= cur_depth) + m_traversal_stack.resize(cur_depth+1); + m_traversal_stack[cur_depth].push_back(ep); + + run_update(cur_depth); + } + + void randomize_local(goal_ref const & g) { + ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g); + + // 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]; + mpz temp = m_tracker.get_random(fd->get_range()); + update(fd, temp); + 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; + tout << "Locally randomized model: " << std::endl; + m_tracker.show_model(tout); ); + } +}; + +#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg new file mode 100644 index 000000000..cc3e05966 --- /dev/null +++ b/src/tactic/sls/sls_params.pyg @@ -0,0 +1,8 @@ +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') + )) diff --git a/src/tactic/sls/sls_powers.h b/src/tactic/sls/sls_powers.h new file mode 100644 index 000000000..d0cc0815e --- /dev/null +++ b/src/tactic/sls/sls_powers.h @@ -0,0 +1,49 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_powers.h + +Abstract: + + Power-of-2 module for SLS + +Author: + + Christoph (cwinter) 2012-02-29 + +Notes: + +--*/ + +#ifndef _SLS_POWERS_H_ +#define _SLS_POWERS_H_ + +#include"mpz.h" + +class powers : public u_map { + unsynch_mpz_manager & m; +public: + powers(unsynch_mpz_manager & m) : m(m) {} + ~powers() { + for (iterator it = begin(); it != end(); it++) { + m.del(*it->m_value); + dealloc(it->m_value); + } + } + + const mpz & operator()(unsigned n) { + u_map::iterator it = find_iterator(n); + if (it != end()) + return *it->m_value; + else { + mpz * new_obj = alloc(mpz); + m.mul2k(m.mk_z(1), n, *new_obj); + insert(n, new_obj); + return *new_obj; + } + } +}; + +#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index eb806e23c..fff082bd8 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -35,6 +35,10 @@ Notes: #include"sls_tactic.h" #include"nnf_tactic.h" +#include"sls_params.hpp" +#include"sls_evaluator.h" +#include"sls_tracker.h" + class sls_tactic : public tactic { class stats { public: @@ -62,1265 +66,7 @@ class sls_tactic : public tactic { } }; - struct imp { - class score_tracker; - - class powers : public u_map { - unsynch_mpz_manager & m; - public: - powers(unsynch_mpz_manager & m) : m(m) {} - ~powers() { - for (iterator it = begin(); it != end(); it++) { - m.del(*it->m_value); - dealloc(it->m_value); - } - } - - const mpz & operator()(unsigned n) { - u_map::iterator it = find_iterator(n); - if (it != end()) - return *it->m_value; - else { - mpz * new_obj = alloc(mpz); - insert(n, new_obj); - m.power(unsynch_mpz_manager::mk_z(2), n, *new_obj); - return *new_obj; - } - } - }; - - class evaluator { - ast_manager & m_manager; - bv_util & m_bv_util; - family_id m_bv_fid; - score_tracker & m_tracker; - unsynch_mpz_manager & m_mpz_manager; - mpz m_zero, m_one, m_two; - powers & m_powers; - - - public: - evaluator(ast_manager & m, bv_util & bvu, score_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_bv_fid = m_bv_util.get_family_id(); - } - - ~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) { - func_decl * fd = n->get_decl(); - unsigned n_args = n->get_num_args(); - expr * const * args = n->get_args(); - - m_mpz_manager.set(result, m_zero); - - if (m_manager.is_and(n)) { - 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; - } - } - } - else if (m_manager.is_or(n)) { - 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; - } - } - } - else if (m_manager.is_not(n)) { - 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); - } - else if (m_manager.is_eq(n)) { - 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; - } - } - } - else if (m_manager.is_distinct(n)) { - 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); - } - } - } - else if (fd->get_family_id() == m_bv_fid) { - bv_op_kind k = static_cast(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); - - mpz mask; - m_mpz_manager.set(mask, m_powers(h+1)); - m_mpz_manager.dec(mask); - m_mpz_manager.bitwise_and(child, mask, result); // result = [h:0] of child - - // shift result by l - for (; l != 0 ; l--) - m_mpz_manager.machine_div(result, m_two, result); - - m_mpz_manager.del(mask); - break; - } - case OP_BADD: { - SASSERT(n_args >= 2); - for (unsigned i = 0; i < n_args; i++) { - const mpz & next = m_tracker.get_value(args[i]); - m_mpz_manager.add(result, next, result); - } - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - m_mpz_manager.rem(result, p, result); - break; - } - case OP_BSUB: { - SASSERT(n_args == 2); - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - mpz temp; - m_mpz_manager.sub(m_tracker.get_value(args[0]), m_tracker.get_value(args[1]), temp); - m_mpz_manager.mod(temp, p, result); - m_mpz_manager.del(temp); - break; - } - case OP_BMUL: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - const mpz & next = m_tracker.get_value(args[i]); - m_mpz_manager.mul(result, next, result); - } - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - m_mpz_manager.rem(result, p, result); - break; - } - case OP_BNEG: { // 2's complement unary minus - SASSERT(n_args == 1); - const mpz & child = m_tracker.get_value(args[0]); - if (m_mpz_manager.is_zero(child)) { - m_mpz_manager.set(result, m_zero); - } - else { - unsigned bv_sz = m_bv_util.get_bv_size(n); - m_mpz_manager.bitwise_not(bv_sz, child, result); - m_mpz_manager.inc(result); // can't overflow - } - break; - } - case OP_BSDIV: - case OP_BSDIV0: - case OP_BSDIV_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - SASSERT(m_mpz_manager.is_nonneg(x) && m_mpz_manager.is_nonneg(y)); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - - if (m_mpz_manager.is_zero(y)) { - if (m_mpz_manager.is_neg(x)) - m_mpz_manager.set(result, m_one); - else { - m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); - m_mpz_manager.dec(result); - } - } - else { - m_mpz_manager.machine_div(x, y, result); - } - if (m_mpz_manager.is_neg(result)) - m_mpz_manager.add(result, p, result); - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BUDIV: - case OP_BUDIV0: - case OP_BUDIV_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - - if (m_mpz_manager.is_zero(y)) { - m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); - m_mpz_manager.dec(result); - } - else { - m_mpz_manager.machine_div(x, y, result); - } - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BSREM: - case OP_BSREM0: - case OP_BSREM_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - - if (m_mpz_manager.is_zero(y)) { - m_mpz_manager.set(result, x); - } - else { - m_mpz_manager.rem(x, y, result); - } - if (m_mpz_manager.is_neg(result)) - m_mpz_manager.add(result, p, result); - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BUREM: - case OP_BUREM0: - case OP_BUREM_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - - if (m_mpz_manager.is_zero(y)) { - m_mpz_manager.set(result, x); - } - else { - m_mpz_manager.mod(x, y, result); - } - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BSMOD: - case OP_BSMOD0: - case OP_BSMOD_I:{ - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - - if (m_mpz_manager.is_zero(y)) - m_mpz_manager.set(result, x); - else { - bool neg_x = m_mpz_manager.is_neg(x); - bool neg_y = m_mpz_manager.is_neg(y); - mpz abs_x, abs_y; - m_mpz_manager.set(abs_x, x); - m_mpz_manager.set(abs_y, y); - if (neg_x) m_mpz_manager.neg(abs_x); - if (neg_y) m_mpz_manager.neg(abs_y); - SASSERT(m_mpz_manager.is_nonneg(abs_x) && m_mpz_manager.is_nonneg(abs_y)); - - m_mpz_manager.mod(abs_x, abs_y, result); - - if (m_mpz_manager.is_zero(result) || (!neg_x && !neg_y)) { - /* Nothing */ - } - else if (neg_x && !neg_y) { - m_mpz_manager.neg(result); - m_mpz_manager.add(result, y, result); - } - else if (!neg_x && neg_y) { - m_mpz_manager.add(result, y, result); - } - else { - m_mpz_manager.neg(result); - } - - m_mpz_manager.del(abs_x); - m_mpz_manager.del(abs_y); - } - - if (m_mpz_manager.is_neg(result)) - m_mpz_manager.add(result, p, result); - - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BAND: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) - m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), result); - break; - } - case OP_BOR: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), result); - } - break; - } - case OP_BXOR: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) - m_mpz_manager.bitwise_xor(result, m_tracker.get_value(args[i]), result); - break; - } - case OP_BNAND: { - SASSERT(n_args >= 2); - mpz temp; - unsigned bv_sz = m_bv_util.get_bv_size(n); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), temp); - m_mpz_manager.bitwise_not(bv_sz, temp, result); - } - m_mpz_manager.del(temp); - break; - } - case OP_BNOR: { - SASSERT(n_args >= 2); - mpz temp; - unsigned bv_sz = m_bv_util.get_bv_size(n); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), temp); - m_mpz_manager.bitwise_not(bv_sz, temp, result); - } - m_mpz_manager.del(temp); - break; - } - case OP_BNOT: { - SASSERT(n_args == 1); - m_mpz_manager.bitwise_not(m_bv_util.get_bv_size(args[0]), m_tracker.get_value(args[0]), result); - break; - } - case OP_ULT: - case OP_ULEQ: - case OP_UGT: - case OP_UGEQ: { - SASSERT(n_args == 2); - const mpz & x = m_tracker.get_value(args[0]); - const mpz & y = m_tracker.get_value(args[1]); - if ((k == OP_ULT && m_mpz_manager.lt(x, y)) || - (k == OP_ULEQ && m_mpz_manager.le(x, y)) || - (k == OP_UGT && m_mpz_manager.gt(x, y)) || - (k == OP_UGEQ && m_mpz_manager.ge(x, y))) - m_mpz_manager.set(result, m_one); - break; - } - case OP_SLT: - case OP_SLEQ: - case OP_SGT: - case OP_SGEQ: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - if ((k == OP_SLT && m_mpz_manager.lt(x, y)) || - (k == OP_SLEQ && m_mpz_manager.le(x, y)) || - (k == OP_SGT && m_mpz_manager.gt(x, y)) || - (k == OP_SGEQ && m_mpz_manager.ge(x, y))) - m_mpz_manager.set(result, m_one); - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BIT2BOOL: { - SASSERT(n_args == 1); - const mpz & child = m_tracker.get_value(args[0]); - m_mpz_manager.set(result, child); - break; - } - case OP_BASHR: { - SASSERT(n_args == 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - mpz first; - const mpz & p = m_powers(m_bv_util.get_bv_size(args[0])-1); - m_mpz_manager.bitwise_and(result, p, first); - mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); - mpz temp; - while (!m_mpz_manager.is_zero(shift)) { - m_mpz_manager.machine_div(result, m_two, temp); - m_mpz_manager.add(temp, first, result); - m_mpz_manager.dec(shift); - } - m_mpz_manager.del(first); - m_mpz_manager.del(shift); - m_mpz_manager.del(temp); - break; - } - case OP_BLSHR: { - SASSERT(n_args == 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); - while (!m_mpz_manager.is_zero(shift)) { - m_mpz_manager.machine_div(result, m_two, result); - m_mpz_manager.dec(shift); - } - m_mpz_manager.del(shift); - break; - } - case OP_BSHL: { - SASSERT(n_args == 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); - while (!m_mpz_manager.is_zero(shift)) { - m_mpz_manager.mul(result, m_two, result); - m_mpz_manager.dec(shift); - } - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - m_mpz_manager.rem(result, p, result); - m_mpz_manager.del(shift); - break; - } - case OP_SIGN_EXT: { - SASSERT(n_args == 1); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - break; - } - default: - NOT_IMPLEMENTED_YET(); - } - } - else { - NOT_IMPLEMENTED_YET(); - } - - TRACE("sls_eval", tout << "(" << fd->get_name(); - for (unsigned i = 0; i < n_args; i++) - tout << " " << m_mpz_manager.to_string(m_tracker.get_value(args[i])); - tout << ") ---> " << m_mpz_manager.to_string(result); - if (m_manager.is_bool(fd->get_range())) tout << " [Boolean]"; - else tout << " [vector size: " << m_bv_util.get_bv_size(fd->get_range()) << "]"; - tout << std::endl; ); - - SASSERT(m_mpz_manager.is_nonneg(result)); - } - }; - - class score_tracker { - ast_manager & m_manager; - unsynch_mpz_manager & m_mpz_manager; - bv_util & m_bv_util; - powers & m_powers; - random_gen m_rng; - unsigned m_random_bits; - unsigned m_random_bits_cnt; - vector > m_traversal_stack; - evaluator m_sls_evaluator; - mpz m_zero, m_one, m_two; - - model m_dummy_model; - model_evaluator m_evaluator; - expr_ref_buffer m_temp_exprs; - - struct value_score { - value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { }; - ~value_score() { if (m) m->del(value); } - unsynch_mpz_manager * m; - mpz value; - double score; - unsigned distance; // max distance from any root - 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; - return *this; - } - }; - - typedef obj_map scores_type; - typedef obj_map > uplinks_type; - typedef obj_map entry_point_type; - typedef obj_map > occ_type; - scores_type m_scores; - uplinks_type m_uplinks; - entry_point_type m_entry_points; - ptr_vector m_constants; - ptr_vector m_temp_constants; - occ_type m_constants_occ; - - public: - score_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : - m_manager(m), - m_mpz_manager(mm), - m_bv_util(bvu), - m_powers(p), - m_random_bits_cnt(0), - m_sls_evaluator(m, m_bv_util, *this, m_mpz_manager, p), - 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_dummy_model(m), - m_evaluator(m_dummy_model), - m_temp_exprs(m) { - } - - ~score_tracker() { - m_mpz_manager.del(m_zero); - m_mpz_manager.del(m_one); - m_mpz_manager.del(m_two); - } - - void set_value(expr * n, const mpz & r) { - SASSERT(m_scores.contains(n)); - m_mpz_manager.set(m_scores.find(n).value, r); - } - - void set_value(func_decl * fd, const mpz & r) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - set_value(ep, r); - } - - mpz & get_value(expr * n) { - SASSERT(m_scores.contains(n)); - return m_scores.find(n).value; - } - - mpz & get_value(func_decl * fd) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - return get_value(ep); - } - - void set_score(expr * n, double score) { - SASSERT(m_scores.contains(n)); - m_scores.find(n).score = score; - } - - void set_score(func_decl * fd, double score) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - set_score(ep, score); - } - - double & get_score(expr * n) { - SASSERT(m_scores.contains(n)); - return m_scores.find(n).score; - } - - double & get_score(func_decl * fd) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - return get_score(ep); - } - - unsigned get_distance(expr * n) { - SASSERT(m_scores.contains(n)); - return m_scores.find(n).distance; - } - - void set_distance(expr * n, unsigned d) { - SASSERT(m_scores.contains(n)); - m_scores.find(n).distance = d; - } - - expr * get_entry_point(func_decl * fd) { - SASSERT(m_entry_points.contains(fd)); - return m_entry_points.find(fd); - } - - bool has_uplinks(expr * n) { - return m_uplinks.contains(n); - } - - ptr_vector & get_uplinks(expr * n) { - SASSERT(m_uplinks.contains(n)); - return m_uplinks.find(n); - } - - void initialize(app * n) { - // Build score table - if (!m_scores.contains(n)) { - value_score vs; - vs.m = & m_mpz_manager; - m_scores.insert(n, vs); - } - - // Update uplinks - unsigned na = n->get_num_args(); - for (unsigned i = 0; i < na; i++) { - expr * c = n->get_arg(i); - uplinks_type::obj_map_entry * entry = m_uplinks.insert_if_not_there2(c, ptr_vector()); - entry->get_data().m_value.push_back(n); - } - - func_decl * d = n->get_decl(); - - if (n->get_num_args() == 0) { - if (d->get_family_id() != null_family_id) { - // Interpreted constant - mpz t; - value2mpz(n, t); - set_value(n, t); - m_mpz_manager.del(t); - } - else { - // Uninterpreted constant - m_entry_points.insert_if_not_there(d, n); - m_constants.push_back(d); - } - } - } - - struct init_proc { - ast_manager & m_manager; - score_tracker & m_tracker; - - init_proc(ast_manager & m, score_tracker & tracker): - m_manager(m), - m_tracker(tracker) { - } - - void operator()(var * n) {} - - void operator()(quantifier * n) {} - - void operator()(app * n) { - m_tracker.initialize(n); - } - }; - - struct find_func_decls_proc { - ast_manager & m_manager; - ptr_vector & m_occs; - - find_func_decls_proc (ast_manager & m, ptr_vector & occs): - m_manager(m), - m_occs(occs) { - } - - void operator()(var * n) {} - - void operator()(quantifier * n) {} - - void operator()(app * n) { - if (n->get_num_args() != 0) - return; - func_decl * d = n->get_decl(); - if (d->get_family_id() != null_family_id) - return; - m_occs.push_back(d); - } - }; - - void calculate_expr_distances(goal_ref const & g) { - // precondition: m_scores is set up. - unsigned sz = g->size(); - ptr_vector stack; - for (unsigned i = 0; i < sz; i++) - stack.push_back(to_app(g->form(i))); - while (!stack.empty()) { - app * cur = stack.back(); - stack.pop_back(); - - unsigned d = get_distance(cur); - - for (unsigned i = 0; i < cur->get_num_args(); i++) { - app * child = to_app(cur->get_arg(i)); - unsigned d_child = get_distance(child); - if (d >= d_child) { - set_distance(child, d+1); - stack.push_back(child); - } - } - } - } - - 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); - for_each_expr(proc, visited, e); - } - - visited.reset(); - - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); - ptr_vector 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); - } - - calculate_expr_distances(g); - - TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); - } - - void show_model(std::ostream & out) { - unsigned sz = get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * fd = get_constant(i); - out << fd->get_name() << " = " << m_mpz_manager.to_string(get_value(fd)) << std::endl; - } - } - - model_ref get_model() { - model_ref res = alloc(model, m_manager); - unsigned sz = get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * fd = get_constant(i); - res->register_decl(fd, mpz2value(fd->get_range(), get_value(fd))); - } - return res; - } - - unsigned get_num_constants() { - return m_constants.size(); - } - - ptr_vector & get_constants() { - return m_constants; - } - - func_decl * get_constant(unsigned i) { - return m_constants[i]; - } - - void set_random_seed(unsigned s) { - m_rng.set_seed(s); - } - - mpz get_random_bv(sort * s) { - SASSERT(m_bv_util.is_bv_sort(s)); - unsigned bv_size = m_bv_util.get_bv_size(s); - mpz r; m_mpz_manager.set(r, 0); - - mpz temp; - do - { - m_mpz_manager.mul(r, m_two, temp); - m_mpz_manager.add(temp, get_random_bool(), r); - } while (--bv_size > 0); - m_mpz_manager.del(temp); - - return r; - } - - mpz & get_random_bool() { - if (m_random_bits_cnt == 0) { - m_random_bits = m_rng(); - m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. - } - - bool val = (m_random_bits & 0x01) != 0; - m_random_bits = m_random_bits >> 1; - m_random_bits_cnt--; - - return (val) ? m_one : m_zero; - } - - unsigned get_random_uint(unsigned bits) { - if (m_random_bits_cnt == 0) { - m_random_bits = m_rng(); - m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. - } - - unsigned val = 0; - while (bits-- > 0) { - if ((m_random_bits & 0x01) != 0) val++; - val <<= 1; - m_random_bits >>= 1; - m_random_bits_cnt--; - - if (m_random_bits_cnt == 0) { - m_random_bits = m_rng(); - m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. - } - } - - return val; - } - - mpz get_random(sort * s) { - if (m_bv_util.is_bv_sort(s)) - return get_random_bv(s); - else if (m_manager.is_bool(s)) - return get_random_bool(); - else - NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. - } - - void randomize() { - 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++) { - func_decl * fd = it->m_key; - sort * s = fd->get_range(); - mpz temp = get_random(s); - set_value(it->m_value, temp); - m_mpz_manager.del(temp); - } - - TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); - } - - void randomize_local(goal_ref const & g) { - ptr_vector & unsat_constants = get_unsat_constants(g); - // bool did_something = false; - for (unsigned i = 0; i < unsat_constants.size(); i++) { - func_decl * fd = unsat_constants[i]; - mpz temp = get_random(fd->get_range()); - if (m_mpz_manager.neq(temp, get_value(fd))) { - // did_something = true; - } - update(fd, temp); - 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 << "Locally randomized model: " << std::endl; show_model(tout); ); - } - - #define _SCORE_AND_MIN - - double score_bool(expr * n, bool negated = false) { - TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); - - double res = 0.0; - - if (is_uninterp_const(n)) { - const mpz & r = get_value(n); - if (negated) - res = (m_mpz_manager.is_one(r)) ? 0.0 : 1.0; - else - res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0; - } - else if (m_manager.is_and(n)) { - SASSERT(!negated); - app * a = to_app(n); - expr * const * args = a->get_args(); - #ifdef _SCORE_AND_MIN - double min = 1.0; - for (unsigned i = 0; i < a->get_num_args(); i++) { - double cur = get_score(args[i]); - 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 - } - else if (m_manager.is_or(n)) { - SASSERT(!negated); - app * a = to_app(n); - expr * const * args = a->get_args(); - double max = 0.0; - for (unsigned i = 0; i < a->get_num_args(); i++) { - double cur = get_score(args[i]); - if (cur > max) max = cur; - } - res = max; - } - else if (m_manager.is_ite(n)) { - SASSERT(!negated); - app * a = to_app(n); - SASSERT(a->get_num_args() == 3); - const mpz & cond = get_value(a->get_arg(0)); - double s_t = get_score(a->get_arg(1)); - double s_f = get_score(a->get_arg(2)); - res = (m_mpz_manager.is_one(cond)) ? s_t : s_f; - } - else if (m_manager.is_eq(n) || m_manager.is_iff(n)) { - app * a = to_app(n); - SASSERT(a->get_num_args() == 2); - expr * arg0 = a->get_arg(0); - 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 = " << - m_mpz_manager.to_string(v1) << std::endl; ); - } - else if (m_manager.is_bool(arg0)) { - res = m_mpz_manager.eq(v0, v1) ? 1.0 : 0.0; - TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << - m_mpz_manager.to_string(v1) << std::endl; ); - } - else if (m_bv_util.is_bv(arg0)) { - mpz diff, diff_m1; - m_mpz_manager.bitwise_xor(v0, v1, diff); - unsigned hamming_distance = 0; - unsigned bv_sz = m_bv_util.get_bv_size(arg0); - #if 1 // unweighted hamming distance - while (!m_mpz_manager.is_zero(diff)) { - //m_mpz_manager.set(diff_m1, diff); - //m_mpz_manager.dec(diff_m1); - //m_mpz_manager.bitwise_and(diff, diff_m1, diff); - //hamming_distance++; - if (!m_mpz_manager.is_even(diff)) { - hamming_distance++; - } - m_mpz_manager.machine_div(diff, m_two, diff); - } - res = 1.0 - (hamming_distance / (double) bv_sz); - #else - rational r(diff); - r /= m_powers(bv_sz); - double dbl = r.get_double(); - res = (dbl < 0.0) ? 1.0 : (dbl > 1.0) ? 0.0 : 1.0 - dbl; - #endif - TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << - m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance << - " ; SZ = " << bv_sz << std::endl; ); - m_mpz_manager.del(diff); - m_mpz_manager.del(diff_m1); - } - else - NOT_IMPLEMENTED_YET(); - } - else if (m_bv_util.is_bv_ule(n)) { // x <= y - app * a = to_app(n); - SASSERT(a->get_num_args() == 2); - const mpz & x = get_value(a->get_arg(0)); - const mpz & y = get_value(a->get_arg(1)); - unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); - - if (negated) { - if (m_mpz_manager.gt(x, y)) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(y, x, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - // In extreme cases, n is 0.9999 but to_double returns something > 1.0 - res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; - m_mpz_manager.del(diff); - } - } - else { - if (m_mpz_manager.le(x, y)) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(x, y, diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; - m_mpz_manager.del(diff); - } - } - TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << - m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); - } - else if (m_bv_util.is_bv_sle(n)) { // x <= y - app * a = to_app(n); - SASSERT(a->get_num_args() == 2); - mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); - mpz y; m_mpz_manager.set(y, get_value(a->get_arg(1))); - unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[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 (negated) { - if (x > y) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(y, x, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= p; - double dbl = n.get_double(); - res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; - m_mpz_manager.del(diff); - } - TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << - m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); - } - else { - if (x <= y) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(x, y, diff); - rational n(diff); - n /= p; - double dbl = n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; - m_mpz_manager.del(diff); - } - TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << - m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); - } - m_mpz_manager.del(x); - m_mpz_manager.del(y); - } - 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)) // Precondition: Assertion set is in NNF. - NOT_IMPLEMENTED_YET(); - res = score_bool(child, true); - } - else if (m_manager.is_distinct(n)) { - app * a = to_app(n); - unsigned pairs = 0, distinct_pairs = 0; - unsigned sz = a->get_num_args(); - for (unsigned i = 0; i < sz; i++) { - for (unsigned j = i+1; j < sz; j++) { - // pair i/j - const mpz & v0 = get_value(a->get_arg(0)); - const mpz & v1 = get_value(a->get_arg(1)); - pairs++; - if (v0 != v1) - distinct_pairs++; - } - } - res = (distinct_pairs/(double)pairs); - if (negated) res = 1.0 - res; - } - else - NOT_IMPLEMENTED_YET(); - - SASSERT(res >= 0.0 && res <= 1.0); - - 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. - } - - void value2mpz(expr * n, mpz & result) { - m_mpz_manager.set(result, m_zero); - - if (m_manager.is_bool(n)) { - m_mpz_manager.set(result, m_manager.is_true(n) ? m_one : m_zero); - } - else if (m_bv_util.is_bv(n)) { - unsigned bv_sz = m_bv_util.get_bv_size(n); - rational q; - if (!m_bv_util.is_numeral(n, q, bv_sz)) - NOT_IMPLEMENTED_YET(); - mpq temp = q.to_mpq(); - SASSERT(m_mpz_manager.is_one(temp.denominator())); - m_mpz_manager.set(result, temp.numerator()); - } - else - NOT_IMPLEMENTED_YET(); - } - - expr_ref mpz2value(sort * s, const mpz & r) { - expr_ref res(m_manager); - if (m_manager.is_bool(s)) - res = (m_mpz_manager.is_zero(r)) ? m_manager.mk_false() : m_manager.mk_true(); - else if (m_bv_util.is_bv_sort(s)) { - rational rat(r); - res = m_bv_util.mk_numeral(rat, s); - } - else - NOT_IMPLEMENTED_YET(); - return res; - } - - void eval(expr * n, mpz & result) { - switch(n->get_kind()) { - case AST_APP: { - app * a = to_app(n); - unsigned n_args = a->get_num_args(); - - if (n_args == 0) { - m_mpz_manager.set(result, get_value(n)); - } - else { - m_sls_evaluator(a, result); - - //#define _EVAL_CHECKED - #ifdef _EVAL_CHECKED - m_temp_exprs.reset(); - for (unsigned i = 0; i < n_args; i++) { - expr * arg = a->get_arg(i); - const mpz & v = get_value(arg); - m_temp_exprs.push_back(mpz2value(m_manager.get_sort(arg), v)); - } - expr_ref q(m_manager), temp(m_manager); - q = m_manager.mk_app(fd, m_temp_exprs.size(), m_temp_exprs.c_ptr()); - m_evaluator(q, temp); - mpz check_res; - value2mpz(temp, check_res); - if (!m_mpz_manager.eq(check_res, result)) - TRACE("sls", 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); - #endif - } - break; - } - default: - NOT_IMPLEMENTED_YET(); - } - // TRACE("sls", tout << "EVAL: " << mk_ismt2_pp(n, m_manager) << " IS " << res << std::endl;); - } - - double score(expr * n) { - if (m_manager.is_bool(n)) - return score_bool(n); - else if (m_bv_util.is_bv(n)) - return score_bv(n); - else - NOT_IMPLEMENTED_YET(); - } - - void run_update(unsigned cur_depth) { - // precondition: m_traversal_stack contains the entry point(s) - expr_fast_mark1 visited; - mpz new_value; - - SASSERT(cur_depth < m_traversal_stack.size()); - while (cur_depth != static_cast(-1)) { - ptr_vector & cur_depth_exprs = m_traversal_stack[cur_depth]; - - for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { - expr * cur = cur_depth_exprs[i]; - - eval(cur, new_value); - set_value(cur, new_value); - set_score(cur, score(cur)); - - if (has_uplinks(cur)) { - ptr_vector & ups = get_uplinks(cur); - for (unsigned j = 0; j < ups.size(); j++) { - expr * next = ups[j]; - unsigned next_d = 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 (entry_point_type::iterator it = m_entry_points.begin(); - it != m_entry_points.end(); - it++) { - expr * ep = get_entry_point(it->m_key); - unsigned cur_depth = get_distance(ep); - if (m_traversal_stack.size() <= cur_depth) - m_traversal_stack.resize(cur_depth+1); - m_traversal_stack[cur_depth].push_back(ep); - if (cur_depth > max_depth) max_depth = cur_depth; - } - - run_update(max_depth); - } - - void update(func_decl * fd, const mpz & new_value) { - set_value(fd, new_value); - expr * ep = get_entry_point(fd); - unsigned cur_depth = get_distance(ep); - if (m_traversal_stack.size() <= cur_depth) - m_traversal_stack.resize(cur_depth+1); - m_traversal_stack[cur_depth].push_back(ep); - - run_update(cur_depth); - } - - ptr_vector & get_unsat_constants(goal_ref const & g) { - unsigned sz = g->size(); - - if (sz == 1) { - 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 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; - } - } - }; - + struct imp { ast_manager & m_manager; stats & m_stats; unsynch_mpz_manager m_mpz_manager; @@ -1329,7 +75,8 @@ class sls_tactic : public tactic { bool m_produce_models; volatile bool m_cancel; bv_util m_bv_util; - score_tracker m_tracker; + sls_tracker m_tracker; + sls_evaluator m_evaluator; unsigned m_max_restarts; unsigned m_plateau_limit; @@ -1345,7 +92,8 @@ class sls_tactic : public tactic { 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_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); } @@ -1363,17 +111,15 @@ class sls_tactic : public tactic { void reset_cancel() { set_cancel(false); } static void collect_param_descrs(param_descrs & r) { - insert_produce_models(r); - r.insert("sls_restarts", CPK_UINT, "(default: infty) # of SLS restarts."); - r.insert("random_seed", CPK_UINT, "(default: 0) random seed."); - r.insert("plateau_limit", CPK_UINT, "(default: 100) SLS plateau limit."); + sls_params::collect_param_descrs(r); } - void updt_params(params_ref const & p) { - m_produce_models = p.get_bool("produce_models", false); - m_max_restarts = p.get_uint("sls_restarts", (unsigned)-1); - m_tracker.set_random_seed(p.get_uint("random_seed", 0)); - m_plateau_limit = p.get_uint("plateau_limit", 100); + 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() { @@ -1429,13 +175,13 @@ class sls_tactic : public tactic { } double rescore(goal_ref const & g) { - m_tracker.update_all(); + 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_tracker.update(fd, new_value); + m_evaluator.update(fd, new_value); m_stats.m_incr_evals++; return top_score(g); } @@ -1539,7 +285,7 @@ class sls_tactic : public tactic { NOT_IMPLEMENTED_YET(); } - m_tracker.update(fd, new_value); + m_evaluator.update(fd, new_value); TRACE("sls", tout << "Randomization candidates: "; for (unsigned i = 0; i < unsat_constants.size(); i++) @@ -1713,7 +459,8 @@ class sls_tactic : public tactic { else { plateau_cnt++; if (plateau_cnt < m_plateau_limit) { - m_tracker.randomize_local(g); + 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); } @@ -1890,13 +637,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { - params_ref sls_p(p); - sls_p.set_uint("sls_restarts", 10000); - sls_p.set_uint("plateau_limit", 100); - - tactic * t = and_then(mk_preamble(m, p), - using_params(mk_sls_tactic(m, p), sls_p)); - + tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m)); t->updt_params(p); return t; } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h new file mode 100644 index 000000000..7fbafec60 --- /dev/null +++ b/src/tactic/sls/sls_tracker.h @@ -0,0 +1,675 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_score_tracker.h + +Abstract: + + Score and value tracking module for SLS + +Author: + + Christoph (cwinter) 2012-02-29 + +Notes: + +--*/ + +#ifndef _SLS_TRACKER_H_ +#define _SLS_TRACKER_H_ + +class sls_tracker { + ast_manager & m_manager; + unsynch_mpz_manager & m_mpz_manager; + bv_util & m_bv_util; + powers & m_powers; + random_gen m_rng; + unsigned m_random_bits; + unsigned m_random_bits_cnt; + 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) { }; + ~value_score() { if (m) m->del(value); } + unsynch_mpz_manager * m; + mpz value; + double score; + unsigned distance; // max distance from any root + 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; + return *this; + } + }; + +public: + typedef obj_map entry_point_type; + +private: + typedef obj_map scores_type; + typedef obj_map > uplinks_type; + typedef obj_map > occ_type; + scores_type m_scores; + uplinks_type m_uplinks; + entry_point_type m_entry_points; + ptr_vector m_constants; + ptr_vector m_temp_constants; + occ_type m_constants_occ; + +public: + sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : + m_manager(m), + m_mpz_manager(mm), + m_bv_util(bvu), + m_powers(p), + m_random_bits_cnt(0), + m_zero(m_mpz_manager.mk_z(0)), + m_one(m_mpz_manager.mk_z(1)), + m_two(m_mpz_manager.mk_z(2)) { + } + + ~sls_tracker() { + m_mpz_manager.del(m_zero); + m_mpz_manager.del(m_one); + m_mpz_manager.del(m_two); + } + + inline void set_value(expr * n, const mpz & r) { + SASSERT(m_scores.contains(n)); + m_mpz_manager.set(m_scores.find(n).value, r); + } + + inline void set_value(func_decl * fd, const mpz & r) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + set_value(ep, r); + } + + inline mpz & get_value(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).value; + } + + inline mpz & get_value(func_decl * fd) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + return get_value(ep); + } + + inline void set_score(expr * n, double score) { + SASSERT(m_scores.contains(n)); + m_scores.find(n).score = score; + } + + inline void set_score(func_decl * fd, double score) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + set_score(ep, score); + } + + inline double & get_score(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).score; + } + + inline double & get_score(func_decl * fd) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + return get_score(ep); + } + + inline unsigned get_distance(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).distance; + } + + inline void set_distance(expr * n, unsigned d) { + SASSERT(m_scores.contains(n)); + m_scores.find(n).distance = d; + } + + inline expr * get_entry_point(func_decl * fd) { + SASSERT(m_entry_points.contains(fd)); + return m_entry_points.find(fd); + } + + inline entry_point_type const & get_entry_points() { + return m_entry_points; + } + + inline bool has_uplinks(expr * n) { + return m_uplinks.contains(n); + } + + inline ptr_vector & get_uplinks(expr * n) { + SASSERT(m_uplinks.contains(n)); + return m_uplinks.find(n); + } + + void initialize(app * n) { + // Build score table + if (!m_scores.contains(n)) { + value_score vs; + vs.m = & m_mpz_manager; + m_scores.insert(n, vs); + } + + // Update uplinks + unsigned na = n->get_num_args(); + for (unsigned i = 0; i < na; i++) { + expr * c = n->get_arg(i); + uplinks_type::obj_map_entry * entry = m_uplinks.insert_if_not_there2(c, ptr_vector()); + entry->get_data().m_value.push_back(n); + } + + func_decl * d = n->get_decl(); + + if (n->get_num_args() == 0) { + if (d->get_family_id() != null_family_id) { + // Interpreted constant + mpz t; + value2mpz(n, t); + set_value(n, t); + m_mpz_manager.del(t); + } + else { + // Uninterpreted constant + m_entry_points.insert_if_not_there(d, n); + m_constants.push_back(d); + } + } + } + + struct init_proc { + ast_manager & m_manager; + sls_tracker & m_tracker; + + init_proc(ast_manager & m, sls_tracker & tracker): + m_manager(m), + m_tracker(tracker) { + } + + void operator()(var * n) {} + + void operator()(quantifier * n) {} + + void operator()(app * n) { + m_tracker.initialize(n); + } + }; + + struct find_func_decls_proc { + ast_manager & m_manager; + ptr_vector & m_occs; + + find_func_decls_proc (ast_manager & m, ptr_vector & occs): + m_manager(m), + m_occs(occs) { + } + + void operator()(var * n) {} + + void operator()(quantifier * n) {} + + void operator()(app * n) { + if (n->get_num_args() != 0) + return; + func_decl * d = n->get_decl(); + if (d->get_family_id() != null_family_id) + return; + m_occs.push_back(d); + } + }; + + void calculate_expr_distances(goal_ref const & g) { + // precondition: m_scores is set up. + unsigned sz = g->size(); + ptr_vector stack; + for (unsigned i = 0; i < sz; i++) + stack.push_back(to_app(g->form(i))); + while (!stack.empty()) { + app * cur = stack.back(); + stack.pop_back(); + + unsigned d = get_distance(cur); + + for (unsigned i = 0; i < cur->get_num_args(); i++) { + app * child = to_app(cur->get_arg(i)); + unsigned d_child = get_distance(child); + if (d >= d_child) { + set_distance(child, d+1); + stack.push_back(child); + } + } + } + } + + 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); + for_each_expr(proc, visited, e); + } + + visited.reset(); + + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); + ptr_vector 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); + } + + calculate_expr_distances(g); + + TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); + } + + void show_model(std::ostream & out) { + unsigned sz = get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * fd = get_constant(i); + out << fd->get_name() << " = " << m_mpz_manager.to_string(get_value(fd)) << std::endl; + } + } + + model_ref get_model() { + model_ref res = alloc(model, m_manager); + unsigned sz = get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * fd = get_constant(i); + res->register_decl(fd, mpz2value(fd->get_range(), get_value(fd))); + } + return res; + } + + unsigned get_num_constants() { + return m_constants.size(); + } + + ptr_vector & get_constants() { + return m_constants; + } + + func_decl * get_constant(unsigned i) { + return m_constants[i]; + } + + void set_random_seed(unsigned s) { + m_rng.set_seed(s); + } + + mpz get_random_bv(sort * s) { + SASSERT(m_bv_util.is_bv_sort(s)); + unsigned bv_size = m_bv_util.get_bv_size(s); + mpz r; m_mpz_manager.set(r, 0); + + mpz temp; + do + { + m_mpz_manager.mul(r, m_two, temp); + m_mpz_manager.add(temp, get_random_bool(), r); + } while (--bv_size > 0); + m_mpz_manager.del(temp); + + return r; + } + + mpz & get_random_bool() { + if (m_random_bits_cnt == 0) { + m_random_bits = m_rng(); + m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. + } + + bool val = (m_random_bits & 0x01) != 0; + m_random_bits = m_random_bits >> 1; + m_random_bits_cnt--; + + return (val) ? m_one : m_zero; + } + + unsigned get_random_uint(unsigned bits) { + if (m_random_bits_cnt == 0) { + m_random_bits = m_rng(); + m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. + } + + unsigned val = 0; + while (bits-- > 0) { + if ((m_random_bits & 0x01) != 0) val++; + val <<= 1; + m_random_bits >>= 1; + m_random_bits_cnt--; + + if (m_random_bits_cnt == 0) { + m_random_bits = m_rng(); + m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. + } + } + + return val; + } + + mpz get_random(sort * s) { + if (m_bv_util.is_bv_sort(s)) + return get_random_bv(s); + else if (m_manager.is_bool(s)) + return get_random_bool(); + else + NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. + } + + void randomize() { + 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++) { + func_decl * fd = it->m_key; + sort * s = fd->get_range(); + mpz temp = get_random(s); + set_value(it->m_value, temp); + m_mpz_manager.del(temp); + } + + TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); + } + +#define _SCORE_AND_MIN + + double score_bool(expr * n, bool negated = false) { + TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); + + double res = 0.0; + + if (is_uninterp_const(n)) { + const mpz & r = get_value(n); + if (negated) + res = (m_mpz_manager.is_one(r)) ? 0.0 : 1.0; + else + res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0; + } + else if (m_manager.is_and(n)) { + SASSERT(!negated); + app * a = to_app(n); + expr * const * args = a->get_args(); + #ifdef _SCORE_AND_MIN + double min = 1.0; + for (unsigned i = 0; i < a->get_num_args(); i++) { + double cur = get_score(args[i]); + 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 + } + else if (m_manager.is_or(n)) { + SASSERT(!negated); + app * a = to_app(n); + expr * const * args = a->get_args(); + double max = 0.0; + for (unsigned i = 0; i < a->get_num_args(); i++) { + double cur = get_score(args[i]); + if (cur > max) max = cur; + } + res = max; + } + else if (m_manager.is_ite(n)) { + SASSERT(!negated); + app * a = to_app(n); + SASSERT(a->get_num_args() == 3); + const mpz & cond = get_value(a->get_arg(0)); + double s_t = get_score(a->get_arg(1)); + double s_f = get_score(a->get_arg(2)); + res = (m_mpz_manager.is_one(cond)) ? s_t : s_f; + } + else if (m_manager.is_eq(n) || m_manager.is_iff(n)) { + app * a = to_app(n); + SASSERT(a->get_num_args() == 2); + expr * arg0 = a->get_arg(0); + 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 = " << + m_mpz_manager.to_string(v1) << std::endl; ); + } + else if (m_manager.is_bool(arg0)) { + res = m_mpz_manager.eq(v0, v1) ? 1.0 : 0.0; + TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << + m_mpz_manager.to_string(v1) << std::endl; ); + } + else if (m_bv_util.is_bv(arg0)) { + mpz diff, diff_m1; + m_mpz_manager.bitwise_xor(v0, v1, diff); + unsigned hamming_distance = 0; + unsigned bv_sz = m_bv_util.get_bv_size(arg0); + #if 1 // unweighted hamming distance + while (!m_mpz_manager.is_zero(diff)) { + //m_mpz_manager.set(diff_m1, diff); + //m_mpz_manager.dec(diff_m1); + //m_mpz_manager.bitwise_and(diff, diff_m1, diff); + //hamming_distance++; + if (!m_mpz_manager.is_even(diff)) { + hamming_distance++; + } + m_mpz_manager.machine_div(diff, m_two, diff); + } + res = 1.0 - (hamming_distance / (double) bv_sz); + #else + rational r(diff); + r /= m_powers(bv_sz); + double dbl = r.get_double(); + res = (dbl < 0.0) ? 1.0 : (dbl > 1.0) ? 0.0 : 1.0 - dbl; + #endif + TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << + m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance << + " ; SZ = " << bv_sz << std::endl; ); + m_mpz_manager.del(diff); + m_mpz_manager.del(diff_m1); + } + else + NOT_IMPLEMENTED_YET(); + } + else if (m_bv_util.is_bv_ule(n)) { // x <= y + app * a = to_app(n); + SASSERT(a->get_num_args() == 2); + const mpz & x = get_value(a->get_arg(0)); + const mpz & y = get_value(a->get_arg(1)); + unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); + + if (negated) { + if (m_mpz_manager.gt(x, y)) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(y, x, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); + double dbl = n.get_double(); + // In extreme cases, n is 0.9999 but to_double returns something > 1.0 + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + m_mpz_manager.del(diff); + } + } + else { + if (m_mpz_manager.le(x, y)) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(x, y, diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); + double dbl = n.get_double(); + res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + m_mpz_manager.del(diff); + } + } + TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << + m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); + } + else if (m_bv_util.is_bv_sle(n)) { // x <= y + app * a = to_app(n); + SASSERT(a->get_num_args() == 2); + mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); + mpz y; m_mpz_manager.set(y, get_value(a->get_arg(1))); + unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[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 (negated) { + if (x > y) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(y, x, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= p; + double dbl = n.get_double(); + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + m_mpz_manager.del(diff); + } + TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << + m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); + } + else { + if (x <= y) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(x, y, diff); + rational n(diff); + n /= p; + double dbl = n.get_double(); + res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + m_mpz_manager.del(diff); + } + TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << + m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); + } + m_mpz_manager.del(x); + m_mpz_manager.del(y); + } + 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)) // Precondition: Assertion set is in NNF. + NOT_IMPLEMENTED_YET(); + res = score_bool(child, true); + } + else if (m_manager.is_distinct(n)) { + app * a = to_app(n); + unsigned pairs = 0, distinct_pairs = 0; + unsigned sz = a->get_num_args(); + for (unsigned i = 0; i < sz; i++) { + for (unsigned j = i+1; j < sz; j++) { + // pair i/j + const mpz & v0 = get_value(a->get_arg(0)); + const mpz & v1 = get_value(a->get_arg(1)); + pairs++; + if (v0 != v1) + distinct_pairs++; + } + } + res = (distinct_pairs/(double)pairs); + if (negated) res = 1.0 - res; + } + else + NOT_IMPLEMENTED_YET(); + + SASSERT(res >= 0.0 && res <= 1.0); + + 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. + } + + void value2mpz(expr * n, mpz & result) { + m_mpz_manager.set(result, m_zero); + + if (m_manager.is_bool(n)) { + m_mpz_manager.set(result, m_manager.is_true(n) ? m_one : m_zero); + } + else if (m_bv_util.is_bv(n)) { + unsigned bv_sz = m_bv_util.get_bv_size(n); + rational q; + if (!m_bv_util.is_numeral(n, q, bv_sz)) + NOT_IMPLEMENTED_YET(); + mpq temp = q.to_mpq(); + SASSERT(m_mpz_manager.is_one(temp.denominator())); + m_mpz_manager.set(result, temp.numerator()); + } + else + NOT_IMPLEMENTED_YET(); + } + + expr_ref mpz2value(sort * s, const mpz & r) { + expr_ref res(m_manager); + if (m_manager.is_bool(s)) + res = (m_mpz_manager.is_zero(r)) ? m_manager.mk_false() : m_manager.mk_true(); + else if (m_bv_util.is_bv_sort(s)) { + rational rat(r); + res = m_bv_util.mk_numeral(rat, s); + } + else + NOT_IMPLEMENTED_YET(); + return res; + } + + double score(expr * n) { + if (m_manager.is_bool(n)) + return score_bool(n); + else if (m_bv_util.is_bv(n)) + return score_bv(n); + else + NOT_IMPLEMENTED_YET(); + } + + ptr_vector & get_unsat_constants(goal_ref const & g) { + unsigned sz = g->size(); + + if (sz == 1) { + 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 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; + } + } +}; + +#endif \ No newline at end of file