From f128c76f239001cd6ddb438388cce777fcb8aefe Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Mar 2016 18:05:14 +0000 Subject: [PATCH 1/4] whitespace --- .../bit_blaster/bit_blaster_rewriter.cpp | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 49c68fedf..022a2273a 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -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); @@ -219,7 +219,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 +289,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 +342,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 +352,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 +361,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); } return BR_FAILED; } - + if (m().is_ite(f)) { SASSERT(num == 3); @@ -371,7 +371,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 +453,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 +507,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 +524,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 +570,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 +627,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl { blaster m_blaster; blaster_rewriter_cfg m_cfg; imp(ast_manager & m, params_ref const & p): - rewriter_tpl(m, - m.proofs_enabled(), + rewriter_tpl(m, + m.proofs_enabled(), m_cfg), m_blaster(m), m_cfg(m, m_blaster, p) { From dbf9609b4c6712e9130888dd65405c2b03ea6c5f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Mar 2016 18:06:14 +0000 Subject: [PATCH 2/4] added assertion --- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 022a2273a..c260178ad 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -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; ) { From 68416bf6bcc39be3f98bc1b6638ef9385fcf2dd3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Mar 2016 18:25:56 +0000 Subject: [PATCH 3/4] whitespace --- src/sat/sat_solver/inc_sat_solver.cpp | 62 +++++++++++++-------------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index bc57a4099..d06770ac0 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -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 m_weights; std::string m_unknown; @@ -66,15 +66,15 @@ class inc_sat_solver : public solver { typedef obj_map 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); + 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)); From bf40bb8005a02c992775c5a775e784985ba84bb3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Mar 2016 18:27:01 +0000 Subject: [PATCH 4/4] Bugfix for inc_sat_solver --- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index d06770ac0..3d1950179 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -182,7 +182,7 @@ 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);