mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

intblast debugging

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-11 10:00:11 -08:00
parent f89de2b455
commit 9373e1b7f5
8 changed files with 121 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/euf/euf_bv_plugin.cpp
View file

@ -343,7 +343,8 @@ namespace euf {
enode* hi = mk_extract(n, cut, w - 1);
enode* lo = mk_extract(n, 0, cut - 1);
auto& i = info(n);
SASSERT(i.value);
if (!i.value)
i.value = n;
i.hi = hi;
i.lo = lo;
i.cut = cut;

36
src/sat/smt/intblast_solver.cpp
View file

@ -82,6 +82,7 @@ namespace intblast {
m_core.reset();
m_vars.reset();
m_trail.reset();
m_new_funs.reset();
m_solver = mk_smt2_solver(m, s.params(), symbol::null);
expr_ref_vector es(m);
@ -228,12 +229,19 @@ namespace intblast {
}
continue;
}
if (m.is_ite(e)) {
m_trail.push_back(m.mk_ite(args.get(0), args.get(1), args.get(2)));
translated.insert(e, m_trail.back());
continue;
}
if (ap->get_family_id() != bv.get_family_id()) {
bool has_bv_arg = any_of(*ap, [&](expr* arg) { return bv.is_bv(arg); });
bool has_bv_sort = bv.is_bv(e);
func_decl* f = ap->get_decl();
if (has_bv_arg) {
verbose_stream() << mk_pp(ap, m) << "\n";
// need to update args with mod where they are bit-vectors.
NOT_IMPLEMENTED_YET();
}
@ -245,14 +253,17 @@ namespace intblast {
domain.push_back(bv.is_bv_sort(s) ? a.mk_int() : s);
}
sort* range = bv.is_bv(e) ? a.mk_int() : e->get_sort();
f = m.mk_fresh_func_decl(ap->get_decl()->get_name(), symbol("bv"), domain.size(), domain.data(), range);
func_decl* g = nullptr;
if (!m_new_funs.find(f, g)) {
g = m.mk_fresh_func_decl(ap->get_decl()->get_name(), symbol("bv"), domain.size(), domain.data(), range);
m_new_funs.insert(f, g);
}
f = g;
}
m_trail.push_back(m.mk_app(f, args));
translated.insert(e, m_trail.back());
verbose_stream() << "translate " << mk_pp(e, m) << " " << has_bv_sort << "\n";
if (has_bv_sort)
m_vars.insert(e, { m_trail.back(), bv_size() });
@ -329,7 +340,7 @@ namespace intblast {
unsigned sz = hi - lo + 1;
expr* new_arg = args.get(0);
if (lo > 0)
new_arg = a.mk_div(new_arg, a.mk_int(rational::power_of_two(lo)));
new_arg = a.mk_idiv(new_arg, a.mk_int(rational::power_of_two(lo)));
m_trail.push_back(new_arg);
break;
}
@ -386,12 +397,19 @@ namespace intblast {
default:
verbose_stream() << mk_pp(e, m) << "\n";
NOT_IMPLEMENTED_YET();
}
verbose_stream() << "insert " << mk_pp(e, m) << " -> " << mk_pp(m_trail.back(), m) << "\n";
}
translated.insert(e, m_trail.back());
}
TRACE("bv",
for (unsigned i = 0; i < es.size(); ++i)
tout << mk_pp(es.get(i), m) << " -> " << mk_pp(translated[es.get(i)], m) << "\n";
);
for (unsigned i = 0; i < es.size(); ++i)
es[i] = translated[es.get(i)];
}
rational solver::get_value(expr* e) const {
@ -414,4 +432,10 @@ namespace intblast {
return m_core;
}
std::ostream& solver::display(std::ostream& out) const {
if (m_solver)
m_solver->display(out);
return out;
}
}

3
src/sat/smt/intblast_solver.h
View file

@ -45,6 +45,7 @@ namespace intblast {
arith_util a;
scoped_ptr<::solver> m_solver;
obj_map<expr, var_info> m_vars;
obj_map<func_decl, func_decl*> m_new_funs;
expr_ref_vector m_trail;
sat::literal_vector m_core;
@ -62,6 +63,8 @@ namespace intblast {
sat::literal_vector const& unsat_core();
rational get_value(expr* e) const;
std::ostream& display(std::ostream& out) const;
};
}

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

@ -115,11 +115,12 @@ namespace polysat {
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
pdd lshr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("lshr nyi"); }
pdd ashr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); }
pdd shl(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); }
pdd band(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); }
pdd bnot(pdd a) { return -a - 1; }
void lshr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("lshr nyi"); }
void ashr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); }
void shl(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); }
void band(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); }
pdd bnot(pdd p) { return -p - 1; }
pvar add_var(unsigned sz);

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

@ -84,9 +84,9 @@ namespace polysat {
case OP_BMUL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
case OP_BADD: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
case OP_BSUB: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
case OP_BLSHR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.lshr(p, q); }); break;
case OP_BSHL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.shl(p, q); }); break;
case OP_BAND: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.band(p, q); }); break;
case OP_BLSHR: internalize_lshr(a); break;
case OP_BSHL: internalize_shl(a); break;
case OP_BAND: internalize_band(a); break;
case OP_BOR: internalize_bor(a); break;
case OP_BXOR: internalize_bxor(a); break;
case OP_BNAND: if_unary(m_core.bnot); internalize_bnand(a); break;
@ -230,6 +230,34 @@ namespace polysat {
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_xor(x, y)); });
}
void solver::internalize_band(app* n) {
if (n->get_num_args() == 2) {
expr* x, * y;
VERIFY(bv.is_bv_and(n, x, y));
m_core.band(expr2pdd(n), expr2pdd(x), expr2pdd(y));
}
else {
expr_ref z(n->get_arg(0), m);
for (unsigned i = 1; i < n->get_num_args(); ++i) {
z = bv.mk_bv_and(z, n->get_arg(i));
ctx.internalize(z);
}
internalize_set(n, expr2pdd(z));
}
}
void solver::internalize_lshr(app* n) {
expr* x, * y;
VERIFY(bv.is_bv_lshr(n, x, y));
m_core.lshr(expr2pdd(n), expr2pdd(x), expr2pdd(y));
}
void solver::internalize_shl(app* n) {
expr* x, * y;
VERIFY(bv.is_bv_shl(n, x, y));
m_core.shl(expr2pdd(n), expr2pdd(x), expr2pdd(y));
}
void solver::internalize_urem_i(app* rem) {
expr* x, *y;
euf::enode* n = expr2enode(rem);
@ -389,14 +417,12 @@ namespace polysat {
}
void solver::internalize_extract(app* e) {
auto p = var2pdd(expr2enode(e)->get_th_var(get_id()));
internalize_set(e, p);
var2pdd(expr2enode(e)->get_th_var(get_id()));
}
void solver::internalize_concat(app* e) {
SASSERT(bv.is_concat(e));
auto p = var2pdd(expr2enode(e)->get_th_var(get_id()));
internalize_set(e, p);
var2pdd(expr2enode(e)->get_th_var(get_id()));
}
void solver::internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn) {

42
src/sat/smt/polysat_model.cpp
View file

@ -18,11 +18,34 @@ Author:
#include "params/bv_rewriter_params.hpp"
#include "sat/smt/polysat_solver.h"
#include "sat/smt/euf_solver.h"
#include "ast/rewriter/bv_rewriter.h"
namespace polysat {
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
if (m_use_intblast_model) {
expr_ref value(m);
if (n->interpreted())
value = n->get_expr();
else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) {
bv_rewriter rw(m);
expr_ref_vector args(m);
for (auto arg : euf::enode_args(n))
args.push_back(values.get(arg->get_root_id()));
rw.mk_app(n->get_decl(), args.size(), args.data(), value);
VERIFY(value);
}
else {
rational r = m_intblast.get_value(n->get_expr());
verbose_stream() << ctx.bpp(n) << " := " << r << "\n";
value = bv.mk_numeral(r, get_bv_size(n));
}
values.set(n->get_root_id(), value);
TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
return;
}
#if 0
auto p = expr2pdd(n->get_expr());
rational val;
@ -31,9 +54,24 @@ namespace polysat {
#endif
}
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
if (!is_app(n->get_expr()))
return false;
app* e = to_app(n->get_expr());
if (n->num_args() == 0) {
dep.insert(n, nullptr);
return true;
}
if (e->get_family_id() != bv.get_family_id())
return false;
for (euf::enode* arg : euf::enode_args(n))
dep.add(n, arg->get_root());
return true;
}
bool solver::check_model(sat::model const& m) const {
return false;
return true;
}
void solver::finalize_model(model& mdl) {
@ -53,6 +91,8 @@ namespace polysat {
for (unsigned v = 0; v < get_num_vars(); ++v)
if (m_var2pdd_valid.get(v, false))
out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
if (m_use_intblast_model)
m_intblast.display(out);
return out;
}
}

2
src/sat/smt/polysat_solver.cpp
View file

@ -40,7 +40,7 @@ namespace polysat {
m_intblast(ctx),
m_lemma(ctx.get_manager())
{
ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
// ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
}
unsigned solver::get_bv_size(euf::enode* n) {

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

@ -119,6 +119,9 @@ namespace polysat {
void internalize_bnor(app* n);
void internalize_bnand(app* n);
void internalize_bxnor(app* n);
void internalize_band(app* n);
void internalize_lshr(app* n);
void internalize_shl(app* n);
template<bool Signed, bool Reverse, bool Negated>
void internalize_le(app* n);
void internalize_zero_extend(app* n);
@ -172,7 +175,7 @@ namespace polysat {
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override {}
euf::th_solver* clone(euf::solver& ctx) override { throw default_exception("nyi"); }
euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx, get_id()); }
extension* copy(sat::solver* s) override { throw default_exception("nyi"); }
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
void gc() override {}
@ -190,6 +193,7 @@ namespace polysat {
bool unit_propagate() override;
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override { return false; }