mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

#5223

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-05 13:10:48 -07:00
parent 179988e161
commit 85bd4b5242
5 changed files with 26 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/sat/smt/bv_internalize.cpp
View file

@ -162,7 +162,7 @@ namespace bv {
#define internalize_bin(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin);
#define internalize_un(F) un = [&](unsigned sz, expr* const* xs, expr_ref_vector& bits) { m_bb.F(sz, xs, bits);}; internalize_unary(a, un);
#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin);
#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin);
#define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
#define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
#define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);
@ -559,27 +559,19 @@ namespace bv {
init_bits(n, bits);
}
void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
SASSERT(e->get_num_args() == 2);
expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
get_arg_bits(e, 0, arg1_bits);
get_arg_bits(e, 1, arg2_bits);
SASSERT(arg1_bits.size() == arg2_bits.size());
fn(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), bits);
init_bits(e, bits);
}
void solver::internalize_ac_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
SASSERT(e->get_num_args() >= 1);
expr_ref_vector bits(m), new_bits(m), arg_bits(m);
unsigned i = e->get_num_args() - 1;
get_arg_bits(e, i, bits);
for (; i-- > 0; ) {
get_arg_bits(e, 0, bits);
for (unsigned i = 1; i < e->get_num_args(); ++i) {
arg_bits.reset();
get_arg_bits(e, i, arg_bits);
SASSERT(arg_bits.size() == bits.size());
new_bits.reset();
fn(arg_bits.size(), arg_bits.data(), bits.data(), new_bits);
fn(bits.size(), bits.data(), arg_bits.data(), new_bits);
bits.swap(new_bits);
}
init_bits(e, bits);

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

@ -239,7 +239,6 @@ namespace bv {
bool internalize_circuit(app* a);
void internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn);
void internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
void internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn);
void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);

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

@ -469,12 +469,12 @@ namespace dt {
void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
// v1 is the new root
TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n";);
SASSERT(v1 == static_cast<int>(m_find.find(v1)));
var_data* d1 = m_var_data[v1];
var_data* d2 = m_var_data[v2];
auto* con1 = d1->m_constructor;
auto* con2 = d2->m_constructor;
TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";);
if (con1 && con2 && con1->get_decl() != con2->get_decl())
ctx.set_conflict(euf::th_explain::conflict(*this, con1, con2));
else if (con2 && !con1) {
@ -721,6 +721,19 @@ namespace dt {
return true;
}
bool solver::include_func_interp(func_decl* f) const {
if (!dt.is_accessor(f))
return false;
func_decl* con = dt.get_accessor_constructor(f);
for (enode* app : ctx.get_egraph().enodes_of(f)) {
enode* arg = app->get_arg(0)->get_root();
if (is_constructor(arg) && arg->get_decl() != con)
return true;
}
return false;
}
sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
if (!visit_rec(m, e, sign, root, redundant))
return sat::null_literal;

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

@ -60,7 +60,7 @@ namespace dt {
stats() { reset(); }
};
datatype_util dt;
mutable datatype_util dt;
array_util m_autil;
stats m_stats;
ptr_vector<var_data> m_var_data;
@ -150,6 +150,7 @@ namespace dt {
bool unit_propagate() override { return false; }
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 include_func_interp(func_decl* f) const override;
sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override;
void internalize(expr* e, bool redundant) override;
euf::theory_var mk_var(euf::enode* n) override;

5
src/sat/smt/euf_model.cpp
View file

@ -208,7 +208,6 @@ namespace euf {
fi = alloc(func_interp, m, arity);
mdl->register_decl(f, fi);
}
TRACE("euf", tout << f->get_name() << "\n";);
args.reset();
for (enode* arg : enode_args(n))
args.push_back(m_values.get(arg->get_root_id()));
@ -216,6 +215,10 @@ namespace euf {
SASSERT(args.size() == arity);
if (!fi->get_entry(args.data()))
fi->insert_new_entry(args.data(), v);
TRACE("euf", tout << f->get_name() << "\n";
for (expr* arg : args) tout << mk_pp(arg, m) << " ";
tout << "\n -> " << mk_pp(v, m) << "\n";);
}
}
}