diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index b01a0e016..74fddd2bb 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -9,14 +9,15 @@ z3_add_component(rewriter datatype_rewriter.cpp der.cpp dl_rewriter.cpp + enum2bv_rewriter.cpp expr_replacer.cpp expr_safe_replace.cpp factor_rewriter.cpp - fd_rewriter.cpp fpa_rewriter.cpp label_rewriter.cpp mk_simplified_app.cpp pb_rewriter.cpp + pb2bv_rewriter.cpp quant_hoist.cpp rewriter.cpp seq_rewriter.cpp diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt index 201cdcf0f..c6f621f25 100644 --- a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt +++ b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt @@ -1,6 +1,9 @@ z3_add_component(portfolio SOURCES default_tactic.cpp + enum2bv_solver.cpp + pb2bv_solver.cpp + bounded_int2bv_solver.cpp fd_solver.cpp smt_strategic_solver.cpp COMPONENT_DEPENDENCIES diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt index acaf186ba..6f6615e0c 100644 --- a/contrib/cmake/src/test/CMakeLists.txt +++ b/contrib/cmake/src/test/CMakeLists.txt @@ -78,6 +78,7 @@ add_executable(test-z3 old_interval.cpp optional.cpp parray.cpp + pb2bv.cpp pdr.cpp permutation.cpp polynomial.cpp diff --git a/src/ast/rewriter/fd_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp similarity index 86% rename from src/ast/rewriter/fd_rewriter.cpp rename to src/ast/rewriter/enum2bv_rewriter.cpp index 026387e22..bbe07f625 100644 --- a/src/ast/rewriter/fd_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation Module Name: - fd_rewriter.cpp + enum2bv_rewriter.cpp Abstract: @@ -19,11 +19,11 @@ Notes: #include"rewriter.h" #include"rewriter_def.h" -#include"fd_rewriter.h" +#include"enum2bv_rewriter.h" #include"ast_util.h" #include"ast_pp.h" -struct fd_rewriter::imp { +struct enum2bv_rewriter::imp { ast_manager& m; params_ref m_params; obj_map m_enum2bv; @@ -258,6 +258,7 @@ struct fd_rewriter::imp { m_enum_defs.resize(lim); m_enum_bvs.resize(lim); } + m_rw.reset(); } void flush_side_constraints(expr_ref_vector& side_constraints) { @@ -275,18 +276,18 @@ struct fd_rewriter::imp { }; -fd_rewriter::fd_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } -fd_rewriter::~fd_rewriter() { dealloc(m_imp); } -void fd_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } -ast_manager & fd_rewriter::m() const { return m_imp->m; } -unsigned fd_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } -void fd_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } -obj_map const& fd_rewriter::enum2bv() const { return m_imp->m_enum2bv; } -obj_map const& fd_rewriter::bv2enum() const { return m_imp->m_bv2enum; } -obj_map const& fd_rewriter::enum2def() const { return m_imp->m_enum2def; } -void fd_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } -void fd_rewriter::push() { m_imp->push(); } -void fd_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } -void fd_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } -unsigned fd_rewriter::num_translated() const { return m_imp->m_num_translated; } -void fd_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); } +enum2bv_rewriter::enum2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } +enum2bv_rewriter::~enum2bv_rewriter() { dealloc(m_imp); } +void enum2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } +ast_manager & enum2bv_rewriter::m() const { return m_imp->m; } +unsigned enum2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } +void enum2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } +obj_map const& enum2bv_rewriter::enum2bv() const { return m_imp->m_enum2bv; } +obj_map const& enum2bv_rewriter::bv2enum() const { return m_imp->m_bv2enum; } +obj_map const& enum2bv_rewriter::enum2def() const { return m_imp->m_enum2def; } +void enum2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } +void enum2bv_rewriter::push() { m_imp->push(); } +void enum2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } +void enum2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } +unsigned enum2bv_rewriter::num_translated() const { return m_imp->m_num_translated; } +void enum2bv_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); } diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp new file mode 100644 index 000000000..0aeeea81a --- /dev/null +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -0,0 +1,453 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + pb2bv_rewriter.cpp + +Abstract: + + Conversion from pseudo-booleans to bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ + +#include"rewriter.h" +#include"rewriter_def.h" +#include"statistics.h" +#include"pb2bv_rewriter.h" +#include"sorting_network.h" +#include"ast_util.h" +#include"ast_pp.h" + + +struct pb2bv_rewriter::imp { + + struct argc_t { + expr* m_arg; + rational m_coeff; + argc_t():m_arg(0), m_coeff(0) {} + argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {} + }; + + struct argc_gt { + bool operator()(argc_t const& a, argc_t const& b) const { + return a.m_coeff > b.m_coeff; + } + }; + + struct argc_entry { + unsigned m_index; + rational m_k; + expr* m_value; + argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {} + argc_entry():m_index(0), m_k(0), m_value(0) {} + + struct eq { + bool operator()(argc_entry const& a, argc_entry const& b) const { + return a.m_index == b.m_index && a.m_k == b.m_k; + } + }; + struct hash { + unsigned operator()(argc_entry const& a) const { + return a.m_index ^ a.m_k.hash(); + } + }; + }; + typedef hashtable argc_cache; + + ast_manager& m; + params_ref m_params; + expr_ref_vector m_lemmas; + func_decl_ref_vector m_fresh; // all fresh variables + unsigned_vector m_fresh_lim; + unsigned m_num_translated; + + struct card2bv_rewriter { + typedef expr* literal; + typedef ptr_vector literal_vector; + psort_nw m_sort; + ast_manager& m; + imp& m_imp; + arith_util au; + pb_util pb; + bv_util bv; + expr_ref_vector m_trail; + + unsigned get_num_bits(func_decl* f) { + rational r(0); + unsigned sz = f->get_arity(); + for (unsigned i = 0; i < sz; ++i) { + r += pb.get_coeff(f, i); + } + r = r > pb.get_k(f)? r : pb.get_k(f); + return r.get_num_bits(); + } + + void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + + expr_ref zero(m), a(m), b(m); + expr_ref_vector es(m); + unsigned bw = get_num_bits(f); + zero = bv.mk_numeral(rational(0), bw); + for (unsigned i = 0; i < sz; ++i) { + es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); + } + switch (es.size()) { + case 0: a = zero; break; + case 1: a = es[0].get(); break; + default: + a = es[0].get(); + for (unsigned i = 1; i < es.size(); ++i) { + a = bv.mk_bv_add(a, es[i].get()); + } + break; + } + b = bv.mk_numeral(pb.get_k(f), bw); + + switch (f->get_decl_kind()) { + case OP_AT_MOST_K: + case OP_PB_LE: + result = bv.mk_ule(a, b); + break; + case OP_AT_LEAST_K: + case OP_PB_GE: + result = bv.mk_ule(b, a); + break; + case OP_PB_EQ: + result = m.mk_eq(a, b); + break; + default: + UNREACHABLE(); + } + TRACE("pb", tout << result << "\n";); + } + + bool mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + decl_kind kind = f->get_decl_kind(); + if (kind != OP_PB_GE && kind != OP_AT_LEAST_K) { + return false; + } + unsigned max_clauses = sz*10; + vector argcs; + for (unsigned i = 0; i < sz; ++i) { + argcs.push_back(argc_t(args[i], pb.get_coeff(f, i))); + } + std::sort(argcs.begin(), argcs.end(), argc_gt()); + DEBUG_CODE( + for (unsigned i = 0; i + 1 < sz; ++i) { + SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff); + }); + result = m.mk_app(f, sz, args); + TRACE("pb", tout << result << "\n";); + argc_cache cache; + expr_ref_vector trail(m); + vector todo_k; + unsigned_vector todo_i; + todo_k.push_back(pb.get_k(f)); + todo_i.push_back(0); + argc_entry entry1; + while (!todo_i.empty()) { + SASSERT(todo_i.size() == todo_k.size()); + if (cache.size() > max_clauses) { + return false; + } + unsigned i = todo_i.back(); + rational k = todo_k.back(); + argc_entry entry(i, k); + if (cache.contains(entry)) { + todo_i.pop_back(); + todo_k.pop_back(); + continue; + } + SASSERT(i < sz); + SASSERT(!k.is_neg()); + rational const& coeff = argcs[i].m_coeff; + expr* arg = argcs[i].m_arg; + if (i + 1 == sz) { + if (k.is_zero()) { + entry.m_value = m.mk_true(); + } + else if (coeff < k) { + entry.m_value = m.mk_false(); + } + else if (coeff.is_zero()) { + entry.m_value = m.mk_true(); + } + else { + SASSERT(coeff >= k && k.is_pos()); + entry.m_value = arg; + } + todo_i.pop_back(); + todo_k.pop_back(); + cache.insert(entry); + continue; + } + entry.m_index++; + expr* lo = 0, *hi = 0; + if (cache.find(entry, entry1)) { + lo = entry1.m_value; + } + else { + todo_i.push_back(i+1); + todo_k.push_back(k); + } + entry.m_k -= coeff; + if (!entry.m_k.is_pos()) { + hi = m.mk_true(); + } + else if (cache.find(entry, entry1)) { + hi = entry1.m_value; + } + else { + todo_i.push_back(i+1); + todo_k.push_back(entry.m_k); + } + if (hi && lo) { + todo_i.pop_back(); + todo_k.pop_back(); + entry.m_index = i; + entry.m_k = k; + entry.m_value = mk_ite(arg, hi, lo); + trail.push_back(entry.m_value); + cache.insert(entry); + } + } + argc_entry entry(0, pb.get_k(f)); + VERIFY(cache.find(entry, entry)); + result = entry.m_value; + TRACE("pb", tout << result << "\n";); + return true; + } + + expr* negate(expr* e) { + if (m.is_not(e, e)) return e; + return m.mk_not(e); + } + expr* mk_ite(expr* c, expr* hi, expr* lo) { + while (m.is_not(c, c)) { + std::swap(hi, lo); + } + if (hi == lo) return hi; + if (m.is_true(hi) && m.is_false(lo)) return c; + if (m.is_false(hi) && m.is_true(lo)) return negate(c); + if (m.is_true(hi)) return m.mk_or(c, lo); + if (m.is_false(lo)) return m.mk_and(c, hi); + if (m.is_false(hi)) return m.mk_and(negate(c), lo); + if (m.is_true(lo)) return m.mk_implies(c, hi); + return m.mk_ite(c, hi, lo); + } + + bool is_or(func_decl* f) { + switch (f->get_decl_kind()) { + case OP_AT_MOST_K: + case OP_PB_LE: + return false; + case OP_AT_LEAST_K: + case OP_PB_GE: + return pb.get_k(f).is_one(); + case OP_PB_EQ: + return false; + default: + UNREACHABLE(); + return false; + } + } + + + public: + + card2bv_rewriter(imp& i, ast_manager& m): + m(m), + m_imp(i), + au(m), + pb(m), + bv(m), + m_sort(*this), + m_trail(m) + {} + + br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + if (f->get_family_id() == pb.get_family_id()) { + mk_pb(f, sz, args, result); + ++m_imp.m_num_translated; + return BR_DONE; + } + else if (f->get_family_id() == au.get_family_id() && mk_arith(f, sz, args, result)) { + ++m_imp.m_num_translated; + return BR_DONE; + } + else { + return BR_FAILED; + } + } + + // + // NSB: review + // we should remove this code and rely on a layer above to deal with + // whatever it accomplishes. It seems to break types. + // + bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + if (f->get_decl_kind() == OP_ADD) { + unsigned bits = 0; + for (unsigned i = 0; i < sz; i++) { + rational val1, val2; + if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) { + bits += val1.get_num_bits(); + } + else if (m.is_ite(args[i]) && + au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() && + au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) { + bits++; + } + else + return false; + } + + result = 0; + for (unsigned i = 0; i < sz; i++) { + rational val1, val2; + expr * q; + if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) + q = bv.mk_numeral(val1, bits); + else + q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits)); + result = (i == 0) ? q : bv.mk_bv_add(result.get(), q); + } + return true; + } + else { + return false; + } + } + + void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + SASSERT(f->get_family_id() == pb.get_family_id()); + if (is_or(f)) { + result = m.mk_or(sz, args); + } + else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) { + result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) { + result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { + result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { + result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { + result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (!mk_shannon(f, sz, args, result)) { + mk_bv(f, sz, args, result); + } + } + + // definitions used for sorting network + literal mk_false() { return m.mk_false(); } + literal mk_true() { return m.mk_true(); } + literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); } + literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); } + literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } + + std::ostream& pp(std::ostream& out, literal lit) { return out << mk_ismt2_pp(lit, m); } + + literal trail(literal l) { + m_trail.push_back(l); + return l; + } + literal fresh() { + expr_ref fr(m.mk_fresh_const("sn", m.mk_bool_sort()), m); + m_imp.m_fresh.push_back(to_app(fr)->get_decl()); + return trail(fr); + } + + void mk_clause(unsigned n, literal const* lits) { + m_imp.m_lemmas.push_back(mk_or(m, n, lits)); + } + }; + + struct card2bv_rewriter_cfg : public default_rewriter_cfg { + card2bv_rewriter m_r; + bool rewrite_patterns() const { return false; } + bool flat_assoc(func_decl * f) const { return false; } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + result_pr = 0; + return m_r.mk_app_core(f, num, args, result); + } + card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {} + }; + + class card_pb_rewriter : public rewriter_tpl { + public: + card2bv_rewriter_cfg m_cfg; + card_pb_rewriter(imp& i, ast_manager & m): + rewriter_tpl(m, false, m_cfg), + m_cfg(i, m) {} + }; + + card_pb_rewriter m_rw; + + imp(ast_manager& m, params_ref const& p): + m(m), m_params(p), m_lemmas(m), + m_fresh(m), + m_num_translated(0), + m_rw(*this, m) { + } + + void updt_params(params_ref const & p) {} + unsigned get_num_steps() const { return m_rw.get_num_steps(); } + void cleanup() { m_rw.cleanup(); } + void operator()(expr * e, expr_ref & result, proof_ref & result_proof) { + m_rw(e, result, result_proof); + } + void push() { + m_fresh_lim.push_back(m_fresh.size()); + } + void pop(unsigned num_scopes) { + SASSERT(m_lemmas.empty()); // lemmas must be flushed before pop. + if (num_scopes > 0) { + SASSERT(num_scopes <= m_fresh_lim.size()); + unsigned new_sz = m_fresh_lim.size() - num_scopes; + unsigned lim = m_fresh_lim[new_sz]; + m_fresh.resize(lim); + m_fresh_lim.resize(new_sz); + } + m_rw.reset(); + } + + void flush_side_constraints(expr_ref_vector& side_constraints) { + side_constraints.append(m_lemmas); + m_lemmas.reset(); + } + + void collect_statistics(statistics & st) const { + st.update("pb-aux-variables", m_fresh.size()); + st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses); + } + +}; + + +pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } +pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); } +void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } +ast_manager & pb2bv_rewriter::m() const { return m_imp->m; } +unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } +void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } +func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; } +void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } +void pb2bv_rewriter::push() { m_imp->push(); } +void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } +void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } +unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; } + +void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); } diff --git a/src/ast/rewriter/fd_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h similarity index 52% rename from src/ast/rewriter/fd_rewriter.h rename to src/ast/rewriter/pb2bv_rewriter.h index 3d4ecae9c..47d8361cb 100644 --- a/src/ast/rewriter/fd_rewriter.h +++ b/src/ast/rewriter/pb2bv_rewriter.h @@ -3,46 +3,44 @@ Copyright (c) 2016 Microsoft Corporation Module Name: - fd_rewriter.h + pb2bv_rewriter.h Abstract: - Conversion from enumeration types to bit-vectors. + Conversion from pseudo-booleans to bit-vectors. Author: - Nikolaj Bjorner (nbjorner) 2016-10-18 + Nikolaj Bjorner (nbjorner) 2016-10-23 Notes: --*/ -#ifndef ENUM_REWRITER_H_ -#define ENUM_REWRITER_H_ +#ifndef PB2BV_REWRITER_H_ +#define PB2BV_REWRITER_H_ -#include"datatype_decl_plugin.h" +#include"pb_decl_plugin.h" #include"rewriter_types.h" #include"expr_functors.h" -class fd_rewriter { +class pb2bv_rewriter { struct imp; imp* m_imp; public: - fd_rewriter(ast_manager & m, params_ref const& p); - ~fd_rewriter(); + pb2bv_rewriter(ast_manager & m, params_ref const& p); + ~pb2bv_rewriter(); void updt_params(params_ref const & p); ast_manager & m() const; unsigned get_num_steps() const; void cleanup(); - obj_map const& enum2bv() const; - obj_map const& bv2enum() const; - obj_map const& enum2def() const; + func_decl_ref_vector const& fresh_constants() const; void operator()(expr * e, expr_ref & result, proof_ref & result_proof); void push(); void pop(unsigned num_scopes); void flush_side_constraints(expr_ref_vector& side_constraints); unsigned num_translated() const; - void set_is_fd(i_sort_pred* sp) const; + void collect_statistics(statistics & st) const; }; #endif diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index d233604f9..0fdbc858d 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -257,7 +257,12 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons all_unit &= m_coeffs.back().is_one(); } if (is_eq) { - result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k); + if (sz == 0) { + result = k.is_zero()?m.mk_true():m.mk_false(); + } + else { + result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k); + } } else if (all_unit && k.is_one()) { result = mk_or(m, sz, m_args.c_ptr()); diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 7a49f8fd0..d9fe9ab72 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -182,8 +182,8 @@ struct check_logic::imp { m_quantifiers = false; } else if (logic == "QF_FD") { - m_bvs = true; - m_uf = true; + m_bvs = true; + m_uf = true; m_ints = true; } else { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 1df28b8e5..b7c80f65a 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -547,6 +547,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "QF_BVFP" || s == "QF_S" || s == "ALL" || + s == "QF_FD" || s == "HORN"; } diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h index 17c5a51bf..5b7f630b4 100644 --- a/src/opt/opt_sls_solver.h +++ b/src/opt/opt_sls_solver.h @@ -90,19 +90,6 @@ namespace opt { virtual void get_labels(svector & r) { m_solver->get_labels(r); } - virtual void set_cancel(bool f) { - m_solver->set_cancel(f); - m_pb2bv.set_cancel(f); - #pragma omp critical (sls_solver) - { - if (m_bvsls) { - m_bvsls->set_cancel(f); - } - if (m_pbsls) { - m_pbsls->set_cancel(f); - } - } - } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } @@ -203,14 +190,11 @@ namespace opt { } void pbsls_opt(model_ref& mdl) { - #pragma omp critical (sls_solver) - { - if (m_pbsls) { - m_pbsls->reset(); - } - else { - m_pbsls = alloc(smt::pb_sls, m); - } + if (m_pbsls) { + m_pbsls->reset(); + } + else { + m_pbsls = alloc(smt::pb_sls, m); } m_pbsls->set_model(mdl); m_pbsls->updt_params(m_params); @@ -226,10 +210,7 @@ namespace opt { } void bvsls_opt(model_ref& mdl) { - #pragma omp critical (sls_solver) - { - m_bvsls = alloc(bvsls_opt_engine, m, m_params); - } + m_bvsls = alloc(bvsls_opt_engine, m, m_params); assertions2sls(); expr_ref objective = soft2bv(m_soft, m_weights); TRACE("opt", tout << objective << "\n";); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 3819f05cb..df39b4186 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -222,6 +222,12 @@ namespace smt { m_imp->assert_expr(e); } + void kernel::assert_expr(expr_ref_vector const& es) { + for (unsigned i = 0; i < es.size(); ++i) { + m_imp->assert_expr(es[i]); + } + } + void kernel::assert_expr(expr * e, proof * pr) { m_imp->assert_expr(e, pr); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 0fec4a21b..ea09081ec 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -70,7 +70,8 @@ namespace smt { This method uses the "asserted" proof as a justification for e. */ void assert_expr(expr * e); - + + void assert_expr(expr_ref_vector const& es); /** \brief Assert the given assertion with the given proof as a justification. */ diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 7b032dce9..d53371c3c 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1270,28 +1270,25 @@ namespace smt { TRACE("pb", tout << in << " >= " << k << "\n";); + psort_expr ps(ctx, *this); + psort_nw sortnw(ps); + sortnw.m_stats.reset(); + if (ctx.get_assignment(thl) == l_true && ctx.get_assign_level(thl) == ctx.get_base_level()) { - psort_expr ps(ctx, *this); - psort_nw sortnw(ps); - sortnw.m_stats.reset(); at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr()); TRACE("pb", tout << ~thl << " " << at_least_k << "\n";); ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k)); - m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars; - m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses; } else { - psort_expr ps(ctx, *this); - psort_nw sortnw(ps); - sortnw.m_stats.reset(); literal at_least_k = sortnw.ge(true, k, in.size(), in.c_ptr()); TRACE("pb", tout << ~thl << " " << at_least_k << "\n";); ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k)); ctx.mk_clause(~at_least_k, thl, justify(thl, ~at_least_k)); - m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars; - m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses; } + m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars; + m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses; + IF_VERBOSE(1, verbose_stream() << "(smt.pb compile sorting network bound: " << k << " literals: " << in.size() << ")\n";); diff --git a/src/tactic/arith/bv2int_rewriter.h b/src/tactic/arith/bv2int_rewriter.h index 0f68257f1..15a425857 100644 --- a/src/tactic/arith/bv2int_rewriter.h +++ b/src/tactic/arith/bv2int_rewriter.h @@ -34,7 +34,7 @@ class bv2int_rewriter_ctx { public: bv2int_rewriter_ctx(ast_manager& m, params_ref const& p) : - m_side_conditions(m), m_trail(m) { update_params(p); } + m_max_size(UINT_MAX), m_side_conditions(m), m_trail(m) { update_params(p); } void reset() { m_side_conditions.reset(); m_trail.reset(); m_power2.reset(); } void add_side_condition(expr* e) { m_side_conditions.push_back(e); } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 5019b6550..096e52981 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -18,500 +18,22 @@ Notes: --*/ #include"tactical.h" #include"cooperate.h" -#include"rewriter_def.h" #include"ast_smt2_pp.h" -#include"expr_substitution.h" #include"card2bv_tactic.h" -#include"pb_rewriter.h" +#include"pb2bv_rewriter.h" #include"ast_util.h" #include"ast_pp.h" - -namespace pb { - unsigned card2bv_rewriter::get_num_bits(func_decl* f) { - rational r(0); - unsigned sz = f->get_arity(); - for (unsigned i = 0; i < sz; ++i) { - r += pb.get_coeff(f, i); - } - r = r > pb.get_k(f)? r : pb.get_k(f); - return r.get_num_bits(); - } - - card2bv_rewriter::card2bv_rewriter(ast_manager& m): - m(m), - au(m), - pb(m), - bv(m), - m_sort(*this), - m_lemmas(m), - m_trail(m) - {} - - void card2bv_rewriter::mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas) { - m_lemmas.reset(); - SASSERT(f->get_family_id() == pb.get_family_id()); - if (is_or(f)) { - result = m.mk_or(sz, args); - } - else if (is_and(f)) { - result = m.mk_and(sz, args); - } - else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args); - } - else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - result = m_sort.le(false, pb.get_k(f).get_unsigned(), sz, args); - } - else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - result = m_sort.ge(false, pb.get_k(f).get_unsigned(), sz, args); - } - else { - br_status st = mk_shannon(f, sz, args, result); - if (st == BR_FAILED) { - mk_bv(f, sz, args, result); - } - } - lemmas.append(m_lemmas); - } - - std::ostream& card2bv_rewriter::pp(std::ostream& out, literal lit) { - return out << mk_ismt2_pp(lit, m); - } - - card2bv_rewriter::literal card2bv_rewriter::trail(literal l) { - m_trail.push_back(l); - return l; - } - card2bv_rewriter::literal card2bv_rewriter::fresh() { - return trail(m.mk_fresh_const("sn", m.mk_bool_sort())); - } - - void card2bv_rewriter::mk_clause(unsigned n, literal const* lits) { - m_lemmas.push_back(mk_or(m, n, lits)); - } - - - br_status card2bv_rewriter::mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - if (f->get_family_id() == null_family_id) { - if (sz == 1) { - // Expecting minimize/maximize. - func_decl_ref fd(m); - fd = m.mk_func_decl(f->get_name(), m.get_sort(args[0]), f->get_range()); - result = m.mk_app(fd.get(), args[0]); - return BR_DONE; - } - else - return BR_FAILED; - } - else if (f->get_family_id() == m.get_basic_family_id()) { - result = m.mk_app(f, sz, args); - return BR_DONE; - } - else if (f->get_family_id() == pb.get_family_id()) { - if (is_or(f)) { - result = m.mk_or(sz, args); - return BR_DONE; - } - if (is_and(f)) { - result = m.mk_and(sz, args); - return BR_DONE; - } - if (is_atmost1(f, sz, args, result)) { - return BR_DONE; - } - br_status st = mk_shannon(f, sz, args, result); - if (st == BR_FAILED) { - mk_bv(f, sz, args, result); - return BR_DONE; - } - else { - return st; - } - } - // NSB: review - // we should remove this code and rely on a layer above to deal with - // whatever it accomplishes. It seems to break types. - // - else if (f->get_family_id() == au.get_family_id()) { - if (f->get_decl_kind() == OP_ADD) { - unsigned bits = 0; - for (unsigned i = 0; i < sz; i++) { - rational val1, val2; - if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) { - bits += val1.get_num_bits(); - } - else if (m.is_ite(args[i]) && - au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() && - au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) { - bits++; - } - else - return BR_FAILED; - } - - result = 0; - for (unsigned i = 0; i < sz; i++) { - rational val1, val2; - expr * q; - if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) - q = bv.mk_numeral(val1, bits); - else - q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits)); - result = (i == 0) ? q : bv.mk_bv_add(result.get(), q); - } - return BR_DONE; - } - else - return BR_FAILED; - } - else - return BR_FAILED; - } - - expr_ref card2bv_rewriter::mk_atmost1(unsigned n, expr * const* xs) { - expr_ref_vector result(m), in(m); - in.append(n, xs); - unsigned inc_size = 4; - while (!in.empty()) { - expr_ref_vector ors(m); - unsigned i = 0; - unsigned n = in.size(); - bool last = n <= inc_size; - for (; i + inc_size < n; i += inc_size) { - mk_at_most_1_small(last, inc_size, in.c_ptr() + i, result, ors); - } - if (i < n) { - mk_at_most_1_small(last, n - i, in.c_ptr() + i, result, ors); - } - if (last) { - break; - } - in.reset(); - in.append(ors); - } - return mk_and(result); - } - - void card2bv_rewriter::mk_at_most_1_small(bool last, unsigned n, literal const* xs, expr_ref_vector& result, expr_ref_vector& ors) { - if (!last) { - ors.push_back(m.mk_or(n, xs)); - } - for (unsigned i = 0; i < n; ++i) { - for (unsigned j = i + 1; j < n; ++j) { - result.push_back(m.mk_not(m.mk_and(xs[i], xs[j]))); - } - } - } - - bool card2bv_rewriter::is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result) { - switch (f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - if (pb.get_k(f).is_one() && pb.has_unit_coefficients(f)) { - result = mk_atmost1(sz, args); - return true; - } - return false; - case OP_AT_LEAST_K: - case OP_PB_GE: - if (pb.get_k(f) == rational(sz-1) && pb.has_unit_coefficients(f)) { - expr_ref_vector nargs(m); - for (unsigned i = 0; i < sz; ++i) { - nargs.push_back(mk_not(args[i])); - } - result = mk_atmost1(nargs.size(), nargs.c_ptr()); - return true; - } - return false; - case OP_PB_EQ: - return false; - default: - UNREACHABLE(); - return false; - } - } - - bool card2bv_rewriter::is_or(func_decl* f) { - switch (f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - return false; - case OP_AT_LEAST_K: - case OP_PB_GE: - return pb.get_k(f).is_one(); - case OP_PB_EQ: - return false; - default: - UNREACHABLE(); - return false; - } - } - - bool card2bv_rewriter::is_and(func_decl* f) { - return false; - } - - void card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - expr_ref zero(m), a(m), b(m); - expr_ref_vector es(m); - unsigned bw = get_num_bits(f); - zero = bv.mk_numeral(rational(0), bw); - for (unsigned i = 0; i < sz; ++i) { - es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); - } - switch (es.size()) { - case 0: a = zero; break; - case 1: a = es[0].get(); break; - default: - a = es[0].get(); - for (unsigned i = 1; i < es.size(); ++i) { - a = bv.mk_bv_add(a, es[i].get()); - } - break; - } - b = bv.mk_numeral(pb.get_k(f), bw); - - switch (f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - UNREACHABLE(); - result = bv.mk_ule(a, b); - break; - case OP_AT_LEAST_K: - UNREACHABLE(); - case OP_PB_GE: - result = bv.mk_ule(b, a); - break; - case OP_PB_EQ: - result = m.mk_eq(a, b); - break; - default: - UNREACHABLE(); - } - TRACE("card2bv", tout << result << "\n";); - } - - struct argc_t { - expr* m_arg; - rational m_coeff; - argc_t():m_arg(0), m_coeff(0) {} - argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {} - }; - struct argc_gt { - bool operator()(argc_t const& a, argc_t const& b) const { - return a.m_coeff > b.m_coeff; - } - }; - struct argc_entry { - unsigned m_index; - rational m_k; - expr* m_value; - argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {} - argc_entry():m_index(0), m_k(0), m_value(0) {} - - struct eq { - bool operator()(argc_entry const& a, argc_entry const& b) const { - return a.m_index == b.m_index && a.m_k == b.m_k; - } - }; - struct hash { - unsigned operator()(argc_entry const& a) const { - return a.m_index ^ a.m_k.hash(); - } - }; - }; - typedef hashtable argc_cache; - - br_status card2bv_rewriter::mk_shannon( - func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - - unsigned max_clauses = sz*10; - vector argcs; - for (unsigned i = 0; i < sz; ++i) { - argcs.push_back(argc_t(args[i], pb.get_coeff(f, i))); - } - std::sort(argcs.begin(), argcs.end(), argc_gt()); - DEBUG_CODE( - for (unsigned i = 0; i + 1 < sz; ++i) { - SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff); - } - ); - result = m.mk_app(f, sz, args); - TRACE("card2bv", tout << result << "\n";); - argc_cache cache; - expr_ref_vector trail(m); - vector todo_k; - unsigned_vector todo_i; - todo_k.push_back(pb.get_k(f)); - todo_i.push_back(0); - decl_kind kind = f->get_decl_kind(); - argc_entry entry1; - while (!todo_i.empty()) { - SASSERT(todo_i.size() == todo_k.size()); - if (cache.size() > max_clauses) { - return BR_FAILED; - } - unsigned i = todo_i.back(); - rational k = todo_k.back(); - argc_entry entry(i, k); - if (cache.contains(entry)) { - todo_i.pop_back(); - todo_k.pop_back(); - continue; - } - SASSERT(i < sz); - SASSERT(!k.is_neg()); - rational const& coeff = argcs[i].m_coeff; - expr* arg = argcs[i].m_arg; - if (i + 1 == sz) { - switch(kind) { - case OP_AT_MOST_K: - case OP_PB_LE: - if (coeff <= k) { - entry.m_value = m.mk_true(); - } - else { - entry.m_value = negate(arg); - trail.push_back(entry.m_value); - } - break; - case OP_AT_LEAST_K: - case OP_PB_GE: - if (k.is_zero()) { - entry.m_value = m.mk_true(); - } - else if (coeff < k) { - entry.m_value = m.mk_false(); - } - else if (coeff.is_zero()) { - entry.m_value = m.mk_true(); - } - else { - SASSERT(coeff >= k && k.is_pos()); - entry.m_value = arg; - } - break; - case OP_PB_EQ: - if (coeff == k) { - entry.m_value = arg; - } - else if (k.is_zero()) { - entry.m_value = negate(arg); - trail.push_back(entry.m_value); - } - else { - entry.m_value = m.mk_false(); - } - break; - } - todo_i.pop_back(); - todo_k.pop_back(); - cache.insert(entry); - continue; - } - entry.m_index++; - expr* lo = 0, *hi = 0; - if (cache.find(entry, entry1)) { - lo = entry1.m_value; - } - else { - todo_i.push_back(i+1); - todo_k.push_back(k); - } - entry.m_k -= coeff; - if (kind != OP_PB_EQ && !entry.m_k.is_pos()) { - switch (kind) { - case OP_AT_MOST_K: - case OP_PB_LE: - hi = m.mk_false(); - break; - case OP_AT_LEAST_K: - case OP_PB_GE: - hi = m.mk_true(); - break; - default: - UNREACHABLE(); - } - } - else if (cache.find(entry, entry1)) { - hi = entry1.m_value; - } - else { - todo_i.push_back(i+1); - todo_k.push_back(entry.m_k); - } - if (hi && lo) { - todo_i.pop_back(); - todo_k.pop_back(); - entry.m_index = i; - entry.m_k = k; - entry.m_value = mk_ite(arg, hi, lo); - trail.push_back(entry.m_value); - cache.insert(entry); - } - } - argc_entry entry(0, pb.get_k(f)); - VERIFY(cache.find(entry, entry)); - result = entry.m_value; - TRACE("card2bv", tout << result << "\n";); - return BR_DONE; - } - - expr* card2bv_rewriter::negate(expr* e) { - if (m.is_not(e, e)) return e; - return m.mk_not(e); - } - - expr* card2bv_rewriter::mk_ite(expr* c, expr* hi, expr* lo) { - while (m.is_not(c, c)) { - std::swap(hi, lo); - } - if (hi == lo) return hi; - if (m.is_true(hi) && m.is_false(lo)) return c; - if (m.is_false(hi) && m.is_true(lo)) return negate(c); - if (m.is_true(hi)) return m.mk_or(c, lo); - if (m.is_false(lo)) return m.mk_and(c, hi); - if (m.is_false(hi)) return m.mk_and(negate(c), lo); - if (m.is_true(lo)) return m.mk_implies(c, hi); - return m.mk_ite(c, hi, lo); - } - - void card_pb_rewriter::rewrite(expr* e, expr_ref& result) { - if (pb.is_eq(e)) { - app* a = to_app(e); - ast_manager& m = m_lemmas.get_manager(); - unsigned sz = a->get_num_args(); - expr_ref_vector args(m); - expr_ref tmp(m); - for (unsigned i = 0; i < sz; ++i) { - (*this)(a->get_arg(i), tmp); - args.push_back(tmp); - } - m_cfg.m_r.mk_assert(a->get_decl(), sz, args.c_ptr(), result, m_lemmas); - } - else { - (*this)(e, result); - } - } - -}; - -template class rewriter_tpl; - +#include"filter_model_converter.h" class card2bv_tactic : public tactic { ast_manager & m; params_ref m_params; - th_rewriter m_rw1; - pb::card_pb_rewriter m_rw2; public: card2bv_tactic(ast_manager & m, params_ref const & p): m(m), - m_params(p), - m_rw1(m), - m_rw2(m) { + m_params(p) { } virtual tactic * translate(ast_manager & m) { @@ -538,9 +60,8 @@ public: SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; result.reset(); tactic_report report("card2bv", *g); - m_rw1.reset(); - m_rw2.reset(); - m_rw2.lemmas().reset(); + th_rewriter rw1(m, m_params); + pb2bv_rewriter rw2(m, m_params); if (g->inconsistent()) { result.push_back(g.get()); @@ -550,18 +71,28 @@ public: expr_ref new_f1(m), new_f2(m); proof_ref new_pr1(m), new_pr2(m); for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) { - m_rw1(g->form(idx), new_f1, new_pr1); + rw1(g->form(idx), new_f1, new_pr1); TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); - m_rw2.rewrite(new_f1, new_f2); + rw2(new_f1, new_f2, new_pr2); if (m.proofs_enabled()) { new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1); - new_pr2 = m.mk_rewrite(new_f1, new_f2); new_pr1 = m.mk_modus_ponens(new_pr1, new_pr2); } g->update(idx, new_f2, new_pr1, g->dep(idx)); } - for (unsigned i = 0; i < m_rw2.lemmas().size(); ++i) { - g->assert_expr(m_rw2.lemmas()[i].get()); + expr_ref_vector fmls(m); + rw2.flush_side_constraints(fmls); + for (unsigned i = 0; !g->inconsistent() && i < fmls.size(); ++i) { + g->assert_expr(fmls[i].get()); + } + + func_decl_ref_vector const& fns = rw2.fresh_constants(); + if (!fns.empty()) { + filter_model_converter* filter = alloc(filter_model_converter, m); + for (unsigned i = 0; i < fns.size(); ++i) { + filter->insert(fns[i]); + } + mc = filter; } g->inc_depth(); diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 2ecc80980..2ccbe9712 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -29,7 +29,7 @@ Revision History: #include "extension_model_converter.h" #include "var_subst.h" #include "ast_util.h" -#include "fd_rewriter.h" +#include "enum2bv_rewriter.h" class dt2bv_tactic : public tactic { @@ -132,7 +132,7 @@ public: if (!m_fd_sorts.empty()) { ref ext = alloc(extension_model_converter, m); ref filter = alloc(filter_model_converter, m); - fd_rewriter rw(m, m_params); + enum2bv_rewriter rw(m, m_params); rw.set_is_fd(&m_is_fd); expr_ref new_curr(m); proof_ref new_pr(m); diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp new file mode 100644 index 000000000..f7236351c --- /dev/null +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -0,0 +1,296 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + bounded_int2bv_solver.cpp + +Abstract: + + This solver identifies bounded integers and rewrites them to bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ + +#include "bounded_int2bv_solver.h" +#include "solver_na2as.h" +#include "tactic.h" +#include "pb2bv_rewriter.h" +#include "filter_model_converter.h" +#include "extension_model_converter.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" +#include "bound_manager.h" +#include "bv2int_rewriter.h" +#include "expr_safe_replace.h" +#include "bv_decl_plugin.h" +#include "arith_decl_plugin.h" + +class bounded_int2bv_solver : public solver_na2as { + ast_manager& m; + params_ref m_params; + bv_util m_bv; + arith_util m_arith; + expr_ref_vector m_assertions; + ref m_solver; + ptr_vector m_bounds; + func_decl_ref_vector m_bv_fns; + func_decl_ref_vector m_int_fns; + unsigned_vector m_bv_fns_lim; + obj_map m_int2bv; + obj_map m_bv2int; + obj_map m_bv2offset; + bv2int_rewriter_ctx m_rewriter_ctx; + bv2int_rewriter_star m_rewriter; + +public: + + bounded_int2bv_solver(ast_manager& m, params_ref const& p, solver* s): + solver_na2as(m), + m(m), + m_params(p), + m_bv(m), + m_arith(m), + m_assertions(m), + m_solver(s), + m_bv_fns(m), + m_int_fns(m), + m_rewriter_ctx(m, p), + m_rewriter(m, m_rewriter_ctx) + { + m_bounds.push_back(alloc(bound_manager, m)); + } + + virtual ~bounded_int2bv_solver() { + while (!m_bounds.empty()) { + dealloc(m_bounds.back()); + m_bounds.pop_back(); + } + } + + virtual solver* translate(ast_manager& m, params_ref const& p) { + return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p)); + } + + virtual void assert_expr(expr * t) { + m_assertions.push_back(t); + } + + virtual void push_core() { + flush_assertions(); + m_solver->push(); + m_bv_fns_lim.push_back(m_bv_fns.size()); + m_bounds.push_back(alloc(bound_manager, m)); + } + + virtual void pop_core(unsigned n) { + m_assertions.reset(); + m_solver->pop(n); + + if (n > 0) { + SASSERT(n <= m_bv_fns_lim.size()); + unsigned new_sz = m_bv_fns_lim.size() - n; + unsigned lim = m_bv_fns_lim[new_sz]; + for (unsigned i = m_int_fns.size(); i > lim; ) { + --i; + m_int2bv.erase(m_int_fns[i].get()); + m_bv2int.erase(m_bv_fns[i].get()); + m_bv2offset.erase(m_bv_fns[i].get()); + } + m_bv_fns_lim.resize(new_sz); + m_bv_fns.resize(lim); + m_int_fns.resize(lim); + } + + while (n > 0) { + dealloc(m_bounds.back()); + m_bounds.pop_back(); + --n; + } + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + flush_assertions(); + return m_solver->check_sat(num_assumptions, assumptions); + } + + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } + virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } + virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } + virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } + virtual void get_model(model_ref & mdl) { + m_solver->get_model(mdl); + if (mdl) { + extend_model(mdl); + filter_model(mdl); + } + } + virtual proof * get_proof() { return m_solver->get_proof(); } + virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { m_solver->get_labels(r); } + virtual ast_manager& get_manager() const { return m; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + flush_assertions(); + expr_ref_vector bvars(m); + for (unsigned i = 0; i < vars.size(); ++i) { + expr* v = vars[i]; + func_decl* f; + rational offset; + if (is_app(v) && is_uninterp_const(v) && m_int2bv.find(to_app(v)->get_decl(), f)) { + bvars.push_back(m.mk_const(f)); + } + else { + bvars.push_back(v); + } + } + lbool r = m_solver->get_consequences(asms, bvars, consequences); + + // translate bit-vector consequences back to integer values + for (unsigned i = 0; i < consequences.size(); ++i) { + expr* a, *b, *u, *v; + func_decl* f; + rational num; + unsigned bvsize; + rational offset; + VERIFY(m.is_implies(consequences[i].get(), a, b)); + if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_bv2int.find(to_app(u)->get_decl(), f) && m_bv.is_numeral(v, num, bvsize)) { + SASSERT(num.is_unsigned()); + expr_ref head(m); + VERIFY (m_bv2offset.find(to_app(u)->get_decl(), offset)); + // f + offset == num + // f == num - offset + head = m.mk_eq(m.mk_const(f), m_arith.mk_numeral(num + offset, true)); + consequences[i] = m.mk_implies(a, head); + } + } + return r; + + } + +private: + + void filter_model(model_ref& mdl) const { + if (m_bv_fns.empty()) { + return; + } + filter_model_converter filter(m); + func_decl_ref_vector const& fns = m_bv_fns; + for (unsigned i = 0; i < m_bv_fns.size(); ++i) { + filter.insert(m_bv_fns[i]); + } + filter(mdl, 0); + } + + void extend_model(model_ref& mdl) { + extension_model_converter ext(m); + obj_map::iterator it = m_int2bv.begin(), end = m_int2bv.end(); + for (; it != end; ++it) { + rational offset; + VERIFY (m_bv2offset.find(it->m_value, offset)); + expr_ref value(m_bv.mk_bv2int(m.mk_const(it->m_value)), m); + if (!offset.is_zero()) { + value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true)); + } + TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";); + ext.insert(it->m_key, value); + } + ext(mdl, 0); + } + + void accumulate_sub(expr_safe_replace& sub) { + for (unsigned i = 0; i < m_bounds.size(); ++i) { + accumulate_sub(sub, *m_bounds[i]); + } + } + + void accumulate_sub(expr_safe_replace& sub, bound_manager& bm) { + bound_manager::iterator it = bm.begin(), end = bm.end(); + for (; it != end; ++it) { + expr* e = *it; + rational lo, hi; + bool s1, s2; + SASSERT(is_uninterp_const(e)); + func_decl* f = to_app(e)->get_decl(); + + if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) { + func_decl* fbv; + rational offset; + if (!m_int2bv.find(f, fbv)) { + rational n = hi - lo + rational::one(); + unsigned num_bits = get_num_bits(n); + expr_ref b(m); + b = m.mk_fresh_const("b", m_bv.mk_sort(num_bits)); + fbv = to_app(b)->get_decl(); + offset = lo; + m_int2bv.insert(f, fbv); + m_bv2int.insert(fbv, f); + m_bv2offset.insert(fbv, offset); + m_bv_fns.push_back(fbv); + m_int_fns.push_back(f); + unsigned shift; + if (!offset.is_zero() && !n.is_power_of_two(shift)) { + m_assertions.push_back(m_bv.mk_ule(b, m_bv.mk_numeral(n-rational::one(), num_bits))); + } + } + else { + VERIFY(m_bv2offset.find(fbv, offset)); + } + expr_ref t(m.mk_const(fbv), m); + t = m_bv.mk_bv2int(t); + if (!offset.is_zero()) { + t = m_arith.mk_add(t, m_arith.mk_numeral(lo, true)); + } + sub.insert(e, t); + } + } + } + + unsigned get_num_bits(rational const& k) { + SASSERT(!k.is_neg()); + SASSERT(k.is_int()); + rational two(2); + rational bound(1); + unsigned num_bits = 1; + while (bound <= k) { + ++num_bits; + bound *= two; + } + return num_bits; + } + + void flush_assertions() { + bound_manager& bm = *m_bounds.back(); + for (unsigned i = 0; i < m_assertions.size(); ++i) { + bm(m_assertions[i].get()); + } + expr_safe_replace sub(m); + accumulate_sub(sub); + proof_ref proof(m); + expr_ref fml1(m), fml2(m); + if (sub.empty()) { + m_solver->assert_expr(m_assertions); + } + else { + for (unsigned i = 0; i < m_assertions.size(); ++i) { + sub(m_assertions[i].get(), fml1); + m_rewriter(fml1, fml2, proof); + m_solver->assert_expr(fml2); + TRACE("int2bv", tout << fml2 << "\n";); + } + } + m_assertions.reset(); + } +}; + +solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) { + return alloc(bounded_int2bv_solver, m, p, s); +} diff --git a/src/tactic/portfolio/bounded_int2bv_solver.h b/src/tactic/portfolio/bounded_int2bv_solver.h new file mode 100644 index 000000000..5fcf2cd65 --- /dev/null +++ b/src/tactic/portfolio/bounded_int2bv_solver.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + bounded_int2bv_solver.h + +Abstract: + + Finite domain solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ +#ifndef BOUNDED_INT2BV_SOLVER_H_ +#define BOUNDED_INT2BV_SOLVER_H_ + +#include"ast.h" +#include"params.h" + +class solver; + +solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s); + +#endif diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp new file mode 100644 index 000000000..369402114 --- /dev/null +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -0,0 +1,162 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + enum2bv_solver.cpp + +Abstract: + + Finite domain solver. + + Enumeration data-types are translated into bit-vectors, and then + the incremental sat-solver is applied to the resulting assertions. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-17 + +Notes: + +--*/ + +#include "solver_na2as.h" +#include "tactic.h" +#include "bv_decl_plugin.h" +#include "datatype_decl_plugin.h" +#include "enum2bv_rewriter.h" +#include "extension_model_converter.h" +#include "filter_model_converter.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" +#include "enum2bv_solver.h" + +class enum2bv_solver : public solver_na2as { + ast_manager& m; + params_ref m_params; + ref m_solver; + enum2bv_rewriter m_rewriter; + +public: + + enum2bv_solver(ast_manager& m, params_ref const& p, solver* s): + solver_na2as(m), + m(m), + m_params(p), + m_solver(s), + m_rewriter(m, p) + { + } + + virtual ~enum2bv_solver() {} + + virtual solver* translate(ast_manager& m, params_ref const& p) { + return alloc(enum2bv_solver, m, p, m_solver->translate(m, p)); + } + + virtual void assert_expr(expr * t) { + expr_ref tmp(t, m); + expr_ref_vector bounds(m); + proof_ref tmp_proof(m); + m_rewriter(t, tmp, tmp_proof); + m_solver->assert_expr(tmp); + m_rewriter.flush_side_constraints(bounds); + m_solver->assert_expr(bounds); + } + + virtual void push_core() { + m_rewriter.push(); + m_solver->push(); + } + + virtual void pop_core(unsigned n) { + m_solver->pop(n); + m_rewriter.pop(n); + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + return m_solver->check_sat(num_assumptions, assumptions); + } + + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } + virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } + virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } + virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } + virtual void get_model(model_ref & mdl) { + m_solver->get_model(mdl); + if (mdl) { + extend_model(mdl); + filter_model(mdl); + } + } + virtual proof * get_proof() { return m_solver->get_proof(); } + virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { m_solver->get_labels(r); } + virtual ast_manager& get_manager() const { return m; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + + datatype_util dt(m); + bv_util bv(m); + + // translate enumeration constants to bit-vectors. + expr_ref_vector bvars(m), conseq(m); + for (unsigned i = 0; i < vars.size(); ++i) { + func_decl* f; + if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { + bvars.push_back(m.mk_const(f)); + } + else { + bvars.push_back(vars[i]); + } + } + lbool r = m_solver->get_consequences(asms, bvars, consequences); + std::cout << consequences.size() << "\n"; + + + // translate bit-vector consequences back to enumeration types + for (unsigned i = 0; i < consequences.size(); ++i) { + expr* a, *b, *u, *v; + func_decl* f; + rational num; + unsigned bvsize; + VERIFY(m.is_implies(consequences[i].get(), a, b)); + if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { + SASSERT(num.is_unsigned()); + expr_ref head(m); + ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); + head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); + consequences[i] = m.mk_implies(a, head); + } + } + return r; + } + + void filter_model(model_ref& mdl) { + filter_model_converter filter(m); + obj_map::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end(); + for (; it != end; ++it) { + filter.insert(it->m_value); + } + filter(mdl, 0); + } + + void extend_model(model_ref& mdl) { + extension_model_converter ext(m); + obj_map::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end(); + for (; it != end; ++it) { + ext.insert(it->m_key, it->m_value); + + } + ext(mdl, 0); + } + +}; + +solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s) { + return alloc(enum2bv_solver, m, p, s); +} diff --git a/src/tactic/portfolio/enum2bv_solver.h b/src/tactic/portfolio/enum2bv_solver.h new file mode 100644 index 000000000..b113c6747 --- /dev/null +++ b/src/tactic/portfolio/enum2bv_solver.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + enum2bv_solver.h + +Abstract: + + Finite domain solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-17 + +Notes: + +--*/ +#ifndef ENUM2BV_SOLVER_H_ +#define ENUM2BV_SOLVER_H_ + +#include"ast.h" +#include"params.h" + +class solver; + +solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s); + +#endif diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp index 9447c158c..a534337bc 100644 --- a/src/tactic/portfolio/fd_solver.cpp +++ b/src/tactic/portfolio/fd_solver.cpp @@ -9,9 +9,6 @@ Abstract: Finite domain solver. - Enumeration data-types are translated into bit-vectors, and then - the incremental sat-solver is applied to the resulting assertions. - Author: Nikolaj Bjorner (nbjorner) 2016-10-17 @@ -21,141 +18,16 @@ Notes: --*/ #include "fd_solver.h" -#include "solver_na2as.h" #include "tactic.h" #include "inc_sat_solver.h" -#include "bv_decl_plugin.h" -#include "datatype_decl_plugin.h" -#include "fd_rewriter.h" -#include "extension_model_converter.h" -#include "filter_model_converter.h" -#include "ast_pp.h" -#include "model_smt2_pp.h" - -class fd_solver : public solver_na2as { - ast_manager& m; - params_ref m_params; - ref m_solver; - fd_rewriter m_rewriter; - -public: - - fd_solver(ast_manager& m, params_ref const& p): - solver_na2as(m), - m(m), - m_params(p), - m_solver(mk_inc_sat_solver(m, p)), - m_rewriter(m, p) - { - } - - virtual ~fd_solver() {} - - virtual solver* translate(ast_manager& m, params_ref const& p) { - return alloc(fd_solver, m, p); - } - - virtual void assert_expr(expr * t) { - expr_ref tmp(t, m); - expr_ref_vector bounds(m); - proof_ref tmp_proof(m); - m_rewriter(t, tmp, tmp_proof); - m_solver->assert_expr(tmp); - m_rewriter.flush_side_constraints(bounds); - m_solver->assert_expr(bounds); - } - - virtual void push_core() { - m_rewriter.push(); - m_solver->push(); - } - - virtual void pop_core(unsigned n) { - m_solver->pop(n); - m_rewriter.pop(n); - } - - virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { - return m_solver->check_sat(num_assumptions, assumptions); - } - - virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } - virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } - virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } - virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } - virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } - virtual void get_model(model_ref & mdl) { - m_solver->get_model(mdl); - if (mdl) { - extend_model(mdl); - filter_model(mdl); - } - } - virtual proof * get_proof() { return m_solver->get_proof(); } - virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } - virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } - virtual void get_labels(svector & r) { m_solver->get_labels(r); } - virtual ast_manager& get_manager() const { return m; } - virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } - - virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { - - datatype_util dt(m); - bv_util bv(m); - - // translate enumeration constants to bit-vectors. - expr_ref_vector bvars(m), conseq(m); - for (unsigned i = 0; i < vars.size(); ++i) { - func_decl* f; - if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { - bvars.push_back(m.mk_const(f)); - } - else { - bvars.push_back(vars[i]); - } - } - lbool r = m_solver->get_consequences(asms, bvars, consequences); - - // translate bit-vector consequences back to enumeration types - for (unsigned i = 0; i < consequences.size(); ++i) { - expr* a, *b, *u, *v; - func_decl* f; - rational num; - unsigned bvsize; - VERIFY(m.is_implies(consequences[i].get(), a, b)); - if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { - SASSERT(num.is_unsigned()); - expr_ref head(m); - ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); - head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); - consequences[i] = m.mk_implies(a, head); - } - } - return r; - } - - void filter_model(model_ref& mdl) { - filter_model_converter filter(m); - obj_map::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end(); - for (; it != end; ++it) { - filter.insert(it->m_value); - } - filter(mdl, 0); - } - - void extend_model(model_ref& mdl) { - extension_model_converter ext(m); - obj_map::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end(); - for (; it != end; ++it) { - ext.insert(it->m_key, it->m_value); - - } - ext(mdl, 0); - } - -}; +#include "enum2bv_solver.h" +#include "pb2bv_solver.h" +#include "bounded_int2bv_solver.h" solver * mk_fd_solver(ast_manager & m, params_ref const & p) { - return alloc(fd_solver, m, p); + solver* s = mk_inc_sat_solver(m, p); + s = mk_enum2bv_solver(m, p, s); + s = mk_pb2bv_solver(m, p, s); + s = mk_bounded_int2bv_solver(m, p, s); + return s; } diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp new file mode 100644 index 000000000..bfd533e8a --- /dev/null +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -0,0 +1,127 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + pb2bv_solver.cpp + +Abstract: + + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ + +#include "pb2bv_solver.h" +#include "solver_na2as.h" +#include "tactic.h" +#include "pb2bv_rewriter.h" +#include "filter_model_converter.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" + +class pb2bv_solver : public solver_na2as { + ast_manager& m; + params_ref m_params; + expr_ref_vector m_assertions; + ref m_solver; + pb2bv_rewriter m_rewriter; + +public: + + pb2bv_solver(ast_manager& m, params_ref const& p, solver* s): + solver_na2as(m), + m(m), + m_params(p), + m_assertions(m), + m_solver(s), + m_rewriter(m, p) + { + } + + virtual ~pb2bv_solver() {} + + virtual solver* translate(ast_manager& m, params_ref const& p) { + return alloc(pb2bv_solver, m, p, m_solver->translate(m, p)); + } + + virtual void assert_expr(expr * t) { + m_assertions.push_back(t); + } + + virtual void push_core() { + flush_assertions(); + m_rewriter.push(); + m_solver->push(); + } + + virtual void pop_core(unsigned n) { + m_assertions.reset(); + m_solver->pop(n); + m_rewriter.pop(n); + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + flush_assertions(); + return m_solver->check_sat(num_assumptions, assumptions); + } + + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } + virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } + virtual void collect_statistics(statistics & st) const { + m_rewriter.collect_statistics(st); + m_solver->collect_statistics(st); + } + virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } + virtual void get_model(model_ref & mdl) { + m_solver->get_model(mdl); + if (mdl) { + filter_model(mdl); + } + } + virtual proof * get_proof() { return m_solver->get_proof(); } + virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { m_solver->get_labels(r); } + virtual ast_manager& get_manager() const { return m; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + flush_assertions(); + return m_solver->get_consequences(asms, vars, consequences); } + + void filter_model(model_ref& mdl) { + if (m_rewriter.fresh_constants().empty()) { + return; + } + filter_model_converter filter(m); + func_decl_ref_vector const& fns = m_rewriter.fresh_constants(); + for (unsigned i = 0; i < fns.size(); ++i) { + filter.insert(fns[i]); + } + filter(mdl, 0); + } + +private: + void flush_assertions() { + proof_ref proof(m); + expr_ref fml(m); + expr_ref_vector fmls(m); + for (unsigned i = 0; i < m_assertions.size(); ++i) { + m_rewriter(m_assertions[i].get(), fml, proof); + m_solver->assert_expr(fml); + } + m_rewriter.flush_side_constraints(fmls); + m_solver->assert_expr(fmls); + m_assertions.reset(); + } +}; + +solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s) { + return alloc(pb2bv_solver, m, p, s); +} diff --git a/src/tactic/portfolio/pb2bv_solver.h b/src/tactic/portfolio/pb2bv_solver.h new file mode 100644 index 000000000..e861e769b --- /dev/null +++ b/src/tactic/portfolio/pb2bv_solver.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + pb2bv_solver.h + +Abstract: + + Pseudo-Boolean to bit-vector solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ +#ifndef PB2BV_SOLVER_H_ +#define PB2BV_SOLVER_H_ + +#include"ast.h" +#include"params.h" + +class solver; + +solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s); + +#endif diff --git a/src/test/main.cpp b/src/test/main.cpp index 9c6cdd668..320eddd7b 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -229,6 +229,7 @@ int main(int argc, char ** argv) { TST_ARGV(ddnf); TST(model_evaluator); TST(get_consequences); + TST(pb2bv); //TST_ARGV(hs); } diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp new file mode 100644 index 000000000..c114997c5 --- /dev/null +++ b/src/test/pb2bv.cpp @@ -0,0 +1,195 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + +#include "trace.h" +#include "vector.h" +#include "ast.h" +#include "ast_pp.h" +#include "statistics.h" +#include "reg_decl_plugins.h" +#include "pb2bv_rewriter.h" +#include "smt_kernel.h" +#include "model_smt2_pp.h" +#include "smt_params.h" +#include "ast_util.h" +#include "pb_decl_plugin.h" +#include "th_rewriter.h" +#include "fd_solver.h" +#include "solver.h" + +static void test1() { + ast_manager m; + reg_decl_plugins(m); + pb_util pb(m); + params_ref p; + pb2bv_rewriter rw(m, p); + expr_ref_vector vars(m); + unsigned N = 5; + for (unsigned i = 0; i < N; ++i) { + std::stringstream strm; + strm << "b" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + } + + for (unsigned k = 1; k <= N; ++k) { + expr_ref fml(m), result(m); + proof_ref proof(m); + fml = pb.mk_at_least_k(vars.size(), vars.c_ptr(), k); + rw(fml, result, proof); + std::cout << fml << " |-> " << result << "\n"; + } + expr_ref_vector lemmas(m); + rw.flush_side_constraints(lemmas); + std::cout << lemmas << "\n"; +} + +static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k, unsigned kind) { + pb_util pb(m); + params_ref p; + pb2bv_rewriter rw(m, p); + unsigned N = vars.size(); + expr_ref fml1(m), fml2(m), result1(m), result2(m); + proof_ref proof(m); + expr_ref_vector lemmas(m); + th_rewriter th_rw(m); + + switch (kind) { + case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + } + rw(fml1, result1, proof); + rw.flush_side_constraints(lemmas); + std::cout << lemmas << "\n"; + for (unsigned values = 0; values < static_cast(1 << N); ++values) { + smt_params fp; + smt::kernel solver(m, fp); + expr_ref_vector tf(m); + for (unsigned i = 0; i < N; ++i) { + bool is_true = 0 != (values & (1 << i)); + tf.push_back(is_true ? m.mk_true() : m.mk_false()); + solver.assert_expr(is_true ? vars[i] : m.mk_not(vars[i])); + } + + solver.assert_expr(lemmas); + switch (kind) { + case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + } + std::cout << fml1 << " " << fml2 << "\n"; + th_rw(fml2, result2, proof); + SASSERT(m.is_true(result2) || m.is_false(result2)); + lbool res = solver.check(); + SASSERT(res == l_true); + solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); + res = solver.check(); + SASSERT(res == l_false); + } +} + +static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k) { + test_semantics(m, vars, coeffs, k, 0); + test_semantics(m, vars, coeffs, k, 1); + test_semantics(m, vars, coeffs, k, 2); +} + +static void test2() { + ast_manager m; + reg_decl_plugins(m); + expr_ref_vector vars(m); + unsigned N = 4; + for (unsigned i = 0; i < N; ++i) { + std::stringstream strm; + strm << "b" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + } + for (unsigned coeff = 0; coeff < static_cast(1 << N); ++coeff) { + vector coeffs; + for (unsigned i = 0; i < N; ++i) { + bool is_one = 0 != (coeff & (1 << i)); + coeffs.push_back(is_one ? rational(1) : rational(2)); + } + for (unsigned i = 0; i <= N; ++i) { + test_semantics(m, vars, coeffs, i); + } + } +} + + +static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k, unsigned kind) { + pb_util pb(m); + params_ref p; + unsigned N = vars.size(); + expr_ref fml1(m), fml2(m), result1(m), result2(m); + proof_ref proof(m); + th_rewriter th_rw(m); + + switch (kind) { + case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + } + result1 = m.mk_fresh_const("xx", m.mk_bool_sort()); + for (unsigned values = 0; values < static_cast(1 << N); ++values) { + ref slv = mk_fd_solver(m, p); + expr_ref_vector tf(m); + for (unsigned i = 0; i < N; ++i) { + bool is_true = 0 != (values & (1 << i)); + tf.push_back(is_true ? m.mk_true() : m.mk_false()); + slv->assert_expr(is_true ? vars[i] : m.mk_not(vars[i])); + } + slv->assert_expr(m.mk_eq(result1, fml1)); + + switch (kind) { + case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + } + std::cout << fml1 << " " << fml2 << "\n"; + th_rw(fml2, result2, proof); + SASSERT(m.is_true(result2) || m.is_false(result2)); + lbool res = slv->check_sat(0,0); + SASSERT(res == l_true); + slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); + res = slv->check_sat(0,0); + SASSERT(res == l_false); + } +} + +static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k) { + test_solver_semantics(m, vars, coeffs, k, 0); + test_solver_semantics(m, vars, coeffs, k, 1); + test_solver_semantics(m, vars, coeffs, k, 2); +} + +static void test3() { + ast_manager m; + reg_decl_plugins(m); + expr_ref_vector vars(m); + unsigned N = 4; + for (unsigned i = 0; i < N; ++i) { + std::stringstream strm; + strm << "b" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + } + for (unsigned coeff = 0; coeff < static_cast(1 << N); ++coeff) { + vector coeffs; + for (unsigned i = 0; i < N; ++i) { + bool is_one = 0 != (coeff & (1 << i)); + coeffs.push_back(is_one ? rational(1) : rational(2)); + } + for (unsigned i = 0; i <= N; ++i) { + test_solver_semantics(m, vars, coeffs, i); + } + } +} + +void tst_pb2bv() { + test1(); + test2(); + test3(); +} + diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index 31ad8a452..0f5d2838e 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -226,7 +226,12 @@ Notes: m_t = EQ; card(k+1, n, xs, out); SASSERT(out.size() >= k+1); - return ctx.mk_min(out[k-1], ctx.mk_not(out[k])); + if (k == 0) { + return ctx.mk_not(out[k]); + } + else { + return ctx.mk_min(out[k-1], ctx.mk_not(out[k])); + } } }