mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-03-03 07:59:13 -08:00
parent 7c6540e18f 1aeea763ff
commit 50b2389e7f
2 changed files with 56 additions and 55 deletions
src
ast/rewriter/bit_blaster
bit_blaster_rewriter.cpp
sat/sat_solver
inc_sat_solver.cpp

47
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -30,7 +30,7 @@ struct blaster_cfg {
bool_rewriter & m_rewriter;
bv_util & m_util;
blaster_cfg(bool_rewriter & r, bv_util & u):m_rewriter(r), m_util(u) {}
ast_manager & m() const { return m_util.get_manager(); }
numeral power(unsigned n) const { return rational::power_of_two(n); }
void mk_xor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_xor(a, b, r); }
@ -59,7 +59,7 @@ struct blaster_cfg {
mk_or(a, c, t2);
mk_or(b, c, t3);
mk_and(t1, t2, t3, r);
#endif
#endif
}
void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rewriter.mk_ite(c, t, e, r); }
void mk_nand(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nand(a, b, r); }
@ -112,7 +112,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_out.finalize();
m_bindings.finalize();
}
blaster_rewriter_cfg(ast_manager & m, blaster & b, params_ref const & p):
m_manager(m),
m_blaster(b),
@ -120,7 +120,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_in2(m),
m_out(m),
m_bindings(m),
m_keys(m),
m_keys(m),
m_values(m) {
updt_params(p);
}
@ -140,7 +140,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
bool rewrite_patterns() const { return true; }
bool max_steps_exceeded(unsigned num_steps) const {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("bit blaster");
if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG);
@ -167,6 +167,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
void pop(unsigned num_scopes) {
if (num_scopes > 0) {
SASSERT(num_scopes <= m_keyval_lim.size());
unsigned new_sz = m_keyval_lim.size() - num_scopes;
unsigned lim = m_keyval_lim[new_sz];
for (unsigned i = m_keys.size(); i > lim; ) {
@ -219,7 +220,7 @@ void OP(expr * arg, expr_ref & result) { \
MK_UNARY_REDUCE(reduce_not, mk_not);
MK_UNARY_REDUCE(reduce_redor, mk_redor);
MK_UNARY_REDUCE(reduce_redand, mk_redand);
#define MK_BIN_REDUCE(OP, BB_OP) \
void OP(expr * arg1, expr * arg2, expr_ref & result) { \
m_in1.reset(); m_in2.reset(); \
@ -289,11 +290,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
void reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
m_in1.reset();
m_in2.reset();
get_bits(arg2, m_in1);
get_bits(arg3, m_in2);
get_bits(arg2, m_in1);
get_bits(arg3, m_in2);
m_out.reset();
m_blaster.mk_multiplexer(arg1, m_in1.size(), m_in1.c_ptr(), m_in2.c_ptr(), m_out);
result = mk_mkbv(m_out);
result = mk_mkbv(m_out);
}
void reduce_concat(unsigned num_args, expr * const * args, expr_ref & result) {
@ -342,7 +343,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
result = mk_mkbv(bits);
result_pr = 0;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
TRACE("bit_blaster", tout << f->get_name() << " ";
@ -352,7 +353,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
mk_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
if (butil().is_bv(args[0])) {
@ -361,7 +362,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
}
return BR_FAILED;
}
if (m().is_ite(f)) {
SASSERT(num == 3);
@ -371,7 +372,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
}
return BR_FAILED;
}
if (f->get_family_id() == butil().get_family_id()) {
switch (f->get_decl_kind()) {
case OP_BV_NUM:
@ -453,7 +454,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
case OP_BXOR:
reduce_xor(num, args, result);
return BR_DONE;
case OP_CONCAT:
reduce_concat(num, args, result);
return BR_DONE;
@ -507,7 +508,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
SASSERT(num == 2);
reduce_smul_no_underflow(args[0], args[1], result);
return BR_DONE;
case OP_BIT2BOOL:
case OP_MKBV:
case OP_INT2BV:
@ -524,7 +525,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
blast_bv_term(m().mk_app(f, num, args), result, result_pr);
return BR_DONE;
}
return BR_FAILED;
}
@ -570,18 +571,18 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
result_pr = 0;
return true;
}
if (m_blast_full && butil().is_bv(t)) {
blast_bv_term(t, result, result_pr);
return true;
}
return false;
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
@ -627,8 +628,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
blaster m_blaster;
blaster_rewriter_cfg m_cfg;
imp(ast_manager & m, params_ref const & p):
rewriter_tpl<blaster_rewriter_cfg>(m,
m.proofs_enabled(),
rewriter_tpl<blaster_rewriter_cfg>(m,
m.proofs_enabled(),
m_cfg),
m_blaster(m),
m_cfg(m, m_blaster, p) {

64
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -50,14 +50,14 @@ class inc_sat_solver : public solver {
expr_ref_vector m_core;
atom2bool_var m_map;
model_ref m_model;
model_converter_ref m_mc;
bit_blaster_rewriter m_bb_rewriter;
model_converter_ref m_mc;
bit_blaster_rewriter m_bb_rewriter;
tactic_ref m_preprocess;
unsigned m_num_scopes;
sat::literal_vector m_asms;
goal_ref_buffer m_subgoals;
proof_converter_ref m_pc;
model_converter_ref m_mc2;
proof_converter_ref m_pc;
model_converter_ref m_mc2;
expr_dependency_ref m_dep_core;
svector<double> m_weights;
std::string m_unknown;
@ -66,15 +66,15 @@ class inc_sat_solver : public solver {
typedef obj_map<expr, sat::literal> dep2asm_t;
public:
inc_sat_solver(ast_manager& m, params_ref const& p):
m(m), m_solver(p, m.limit(), 0),
m_params(p), m_optimize_model(false),
m_fmls(m),
m(m), m_solver(p, m.limit(), 0),
m_params(p), m_optimize_model(false),
m_fmls(m),
m_asmsf(m),
m_fmls_head(0),
m_core(m),
m_core(m),
m_map(m),
m_bb_rewriter(m, p),
m_num_scopes(0),
m_num_scopes(0),
m_dep_core(m),
m_unknown("no reason given") {
m_params.set_bool("elim_vars", false);
@ -88,17 +88,17 @@ public:
simp2_p.set_bool("flat", true); // required by som
simp2_p.set_bool("hoist_mul", false); // required by som
simp2_p.set_bool("elim_and", true);
m_preprocess =
m_preprocess =
and_then(mk_card2bv_tactic(m, m_params),
using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, &m_bb_rewriter),
mk_bit_blaster_tactic(m, &m_bb_rewriter),
//mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
using_params(mk_simplify_tactic(m), simp2_p));
}
virtual ~inc_sat_solver() {}
virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
ast_translation tr(m, dst_m);
if (m_num_scopes > 0) {
@ -119,7 +119,7 @@ public:
virtual void set_progress_callback(progress_callback * callback) {}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
return check_sat(num_assumptions, assumptions, 0, 0);
}
@ -138,8 +138,8 @@ public:
}
m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr());
}
lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) {
lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) {
m_weights.reset();
if (weights != 0) {
m_weights.append(sz, weights);
@ -182,13 +182,13 @@ public:
m_map.push();
}
virtual void pop(unsigned n) {
if (n < m_num_scopes) { // allow inc_sat_solver to
if (n > m_num_scopes) { // allow inc_sat_solver to
n = m_num_scopes; // take over for another solver.
}
m_bb_rewriter.pop(n);
m_map.pop(n);
SASSERT(n >= m_num_scopes);
m_solver.user_pop(n);
SASSERT(n <= m_num_scopes);
m_solver.user_pop(n);
m_num_scopes -= n;
while (n > 0) {
m_fmls_head = m_fmls_head_lim.back();
@ -227,7 +227,7 @@ public:
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
m_optimize_model = m_params.get_bool("optimize_model", false);
}
}
virtual void collect_statistics(statistics & st) const {
m_preprocess->collect_statistics(st);
m_solver.collect_statistics(st);
@ -246,7 +246,7 @@ public:
UNREACHABLE();
return 0;
}
virtual std::string reason_unknown() const {
return m_unknown;
}
@ -279,13 +279,13 @@ private:
m_preprocess->reset();
SASSERT(g->models_enabled());
SASSERT(!g->proofs_enabled());
TRACE("sat", g->display(tout););
try {
TRACE("sat", g->display(tout););
try {
(*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core);
}
catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
return l_undef;
return l_undef;
}
if (m_subgoals.size() != 1) {
IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";);
@ -309,7 +309,7 @@ private:
lbool res = internalize_goal(g, dep2asm);
if (res == l_true) {
extract_assumptions(sz, asms, dep2asm);
}
}
return res;
}
@ -360,7 +360,7 @@ private:
tout << core[i] << " ";
}
tout << "\n";
);
);
m_core.reset();
for (unsigned i = 0; i < core.size(); ++i) {
@ -402,8 +402,8 @@ private:
}
sat::bool_var v = it->m_value;
switch (sat::value_at(v, ll_m)) {
case l_true:
md->register_decl(to_app(n)->get_decl(), m.mk_true());
case l_true:
md->register_decl(to_app(n)->get_decl(), m.mk_true());
break;
case l_false:
md->register_decl(to_app(n)->get_decl(), m.mk_false());
@ -416,7 +416,7 @@ private:
if (m_mc || !m_bb_rewriter.const2bits().empty()) {
model_converter_ref mc = m_mc;
if (!m_bb_rewriter.const2bits().empty()) {
mc = concat(mc.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter.const2bits()));
mc = concat(mc.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter.const2bits()));
}
(*mc)(m_model);
}
@ -425,9 +425,9 @@ private:
DEBUG_CODE(
for (unsigned i = 0; i < m_fmls.size(); ++i) {
expr_ref tmp(m);
VERIFY(m_model->eval(m_fmls[i].get(), tmp, true));
VERIFY(m_model->eval(m_fmls[i].get(), tmp, true));
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
SASSERT(m.is_true(tmp));