mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

add bit blast optio

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-01 11:08:30 -08:00
parent 09b3d99db1
commit fb5f81cf75
5 changed files with 32 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/core.h
View file

@ -183,6 +183,8 @@ namespace polysat {
assignment& get_assignment() { return m_assignment; }
random_gen& rand() { return m_rand; }
pdd mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) { return s.mk_ite(sc, p, q); }
};
}

14
src/sat/smt/polysat/monomials.cpp
View file

@ -118,6 +118,8 @@ namespace polysat {
// bit blast a monomial definition
lbool monomials::bit_blast() {
// disable for now
return l_undef;
init_to_refine();
if (m_to_refine.empty())
return l_true;
@ -330,7 +332,17 @@ namespace polysat {
}
bool monomials::bit_blast(monomial const& mon) {
return false;
if (mon.size() != 2)
return false;
unsigned sz = mon.num_bits();
pdd n = mon.var.manager().mk_val(0);
pdd zero = n.manager().mk_val(0);
pdd p = mon.args[0];
pdd q = mon.args[1];
for (unsigned i = 0; i < sz; ++i)
n += c.mk_ite(C.bit(p, i), c.value(rational::power_of_two(i), sz) * q, zero);
c.add_axiom("bit-blast", { C.eq(mon.var, n) }, true);
return true;
}
std::ostream& monomials::display(std::ostream& out) const {

1
src/sat/smt/polysat/types.h
View file

@ -147,6 +147,7 @@ namespace polysat {
virtual void get_bitvector_sub_slices(pvar v, offset_slices& out) = 0;
virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0;
virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice) = 0;
virtual pdd mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) = 0;
virtual unsigned level(dependency const& d) = 0;
};

15
src/sat/smt/polysat_internalize.cpp
View file

@ -720,6 +720,21 @@ namespace polysat {
mk_atom(lit.var(), sc);
}
pdd solver::mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) {
expr_ref cond = constraint2expr(sc);
expr_ref th = pdd2expr(p);
expr_ref el = pdd2expr(q);
expr* ite = m.mk_ite(cond, th, el);
ctx.internalize(ite);
euf::enode* n = expr2enode(ite);
if (!n->is_attached_to(get_id())) {
auto v = mk_var(n);
pvar r = m_core.add_var(bv.get_bv_size(th));
internalize_set(v, m_core.var(r));
}
return expr2pdd(ite);
}
dd::pdd solver::expr2pdd(expr* e) {
return var2pdd(get_th_var(e));
}

1
src/sat/smt/polysat_solver.h
View file

@ -215,6 +215,7 @@ namespace polysat {
void get_bitvector_super_slices(pvar v, offset_slices& out) override;
void get_bitvector_suffixes(pvar v, offset_slices& out) override;
void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) override;
pdd mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) override;
unsigned level(dependency const& d) override;
dependency explain_slice(pvar v, pvar w, unsigned offset);