diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 88f0f79c1..d6c3d4e64 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -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& 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& fn) { + void solver::internalize_binary(app* e, std::function& 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); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 4bb65c995..daf21a132 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -239,7 +239,6 @@ namespace bv { bool internalize_circuit(app* a); void internalize_unary(app* n, std::function& fn); void internalize_binary(app* n, std::function& fn); - void internalize_ac_binary(app* n, std::function& fn); void internalize_par_unary(app* n, std::function& fn); void internalize_novfl(app* n, std::function& fn); void internalize_interp(app* n, std::function& ibin, std::function& un); diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index adc99ce9e..133510a84 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -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(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; diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index 7e78acb27..cd5529075 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -60,7 +60,7 @@ namespace dt { stats() { reset(); } }; - datatype_util dt; + mutable datatype_util dt; array_util m_autil; stats m_stats; ptr_vector 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& 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; diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index c8780252a..7020ed08c 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -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";); + } } }