mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
fix sorting network bug, add network compilation,...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
72f09e4729
commit
019ff77613
15 changed files with 350 additions and 100 deletions
|
|
@ -39,8 +39,55 @@ namespace pb {
|
|||
m(m),
|
||||
au(m),
|
||||
pb(m),
|
||||
bv(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(m.mk_or_reduced(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) {
|
||||
|
|
@ -69,7 +116,8 @@ namespace pb {
|
|||
}
|
||||
br_status st = mk_shannon(f, sz, args, result);
|
||||
if (st == BR_FAILED) {
|
||||
return mk_bv(f, sz, args, result);
|
||||
mk_bv(f, sz, args, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
return st;
|
||||
|
|
@ -135,7 +183,7 @@ namespace pb {
|
|||
return false;
|
||||
}
|
||||
|
||||
br_status card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
|
||||
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);
|
||||
|
|
@ -172,7 +220,6 @@ namespace pb {
|
|||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
struct argc_t {
|
||||
|
|
@ -352,10 +399,30 @@ namespace pb {
|
|||
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<pb::card2bv_rewriter_cfg>;
|
||||
|
||||
|
||||
class card2bv_tactic : public tactic {
|
||||
ast_manager & m;
|
||||
params_ref m_params;
|
||||
|
|
@ -402,6 +469,7 @@ public:
|
|||
tactic_report report("card2bv", *g);
|
||||
m_rw1.reset();
|
||||
m_rw2.reset();
|
||||
m_rw2.lemmas().reset();
|
||||
|
||||
if (g->inconsistent()) {
|
||||
result.push_back(g.get());
|
||||
|
|
@ -413,9 +481,12 @@ public:
|
|||
for (unsigned idx = 0; idx < size; idx++) {
|
||||
m_rw1(g->form(idx), new_f1);
|
||||
TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
|
||||
m_rw2(new_f1, new_f2);
|
||||
m_rw2.rewrite(new_f1, new_f2);
|
||||
g->update(idx, new_f2, g->pr(idx), g->dep(idx));
|
||||
}
|
||||
for (unsigned i = 0; i < m_rw2.lemmas().size(); ++i) {
|
||||
g->assert_expr(m_rw2.lemmas()[i].get());
|
||||
}
|
||||
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
|
|
|
|||
|
|
@ -23,6 +23,9 @@ Notes:
|
|||
#include"pb_decl_plugin.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"rewriter.h"
|
||||
#include<typeinfo>
|
||||
#include"sorting_network.h"
|
||||
|
||||
|
||||
class ast_manager;
|
||||
class tactic;
|
||||
|
|
@ -30,12 +33,20 @@ class tactic;
|
|||
namespace pb {
|
||||
|
||||
class card2bv_rewriter {
|
||||
public:
|
||||
typedef expr* literal;
|
||||
typedef ptr_vector<expr> literal_vector;
|
||||
private:
|
||||
ast_manager& m;
|
||||
arith_util au;
|
||||
pb_util pb;
|
||||
bv_util bv;
|
||||
psort_nw<card2bv_rewriter> m_sort;
|
||||
expr_ref_vector m_lemmas;
|
||||
expr_ref_vector m_trail;
|
||||
|
||||
unsigned get_num_bits(func_decl* f);
|
||||
br_status mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
|
||||
void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
|
||||
br_status mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
|
||||
expr* negate(expr* e);
|
||||
expr* mk_ite(expr* c, expr* hi, expr* lo);
|
||||
|
|
@ -45,6 +56,19 @@ namespace pb {
|
|||
public:
|
||||
card2bv_rewriter(ast_manager& m);
|
||||
br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
|
||||
void mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas);
|
||||
|
||||
// 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);
|
||||
literal fresh();
|
||||
literal trail(literal l);
|
||||
void mk_clause(unsigned n, literal const* lits);
|
||||
|
||||
};
|
||||
|
||||
struct card2bv_rewriter_cfg : public default_rewriter_cfg {
|
||||
|
|
@ -55,15 +79,23 @@ namespace pb {
|
|||
result_pr = 0;
|
||||
return m_r.mk_app_core(f, num, args, result);
|
||||
}
|
||||
card2bv_rewriter_cfg(ast_manager & m):m_r(m) {}
|
||||
card2bv_rewriter_cfg(ast_manager & m):m_r(m) {}
|
||||
};
|
||||
|
||||
class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
|
||||
card2bv_rewriter_cfg m_cfg;
|
||||
pb_util pb;
|
||||
expr_ref_vector m_lemmas;
|
||||
public:
|
||||
card_pb_rewriter(ast_manager & m):
|
||||
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
|
||||
m_cfg(m) {}
|
||||
card_pb_rewriter(ast_manager & m):
|
||||
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
|
||||
m_cfg(m),
|
||||
pb(m),
|
||||
m_lemmas(m) {}
|
||||
|
||||
void rewrite(expr* e, expr_ref& result);
|
||||
|
||||
expr_ref_vector& lemmas() { return m_lemmas; }
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue