mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

working on new solver core

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-30 14:38:35 -08:00
parent f519c58ace
commit 523578e3f6
13 changed files with 224 additions and 81 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/euf/euf_egraph.cpp
View file

@ -23,8 +23,8 @@ Notes:
namespace euf {
enode* egraph::mk_enode(expr* f, unsigned num_args, enode * const* args) {
enode* n = enode::mk(m_region, f, num_args, args);
enode* egraph::mk_enode(expr* f, unsigned generation, unsigned num_args, enode * const* args) {
enode* n = enode::mk(m_region, f, generation, num_args, args);
m_nodes.push_back(n);
m_exprs.push_back(f);
if (is_app(f) && num_args > 0) {
@ -83,10 +83,10 @@ namespace euf {
n->set_update_children();
}
enode* egraph::mk(expr* f, unsigned num_args, enode *const* args) {
enode* egraph::mk(expr* f, unsigned generation, unsigned num_args, enode *const* args) {
SASSERT(!find(f));
force_push();
enode *n = mk_enode(f, num_args, args);
enode *n = mk_enode(f, generation, num_args, args);
SASSERT(n->class_size() == 1);
if (num_args == 0 && m.is_unique_value(f))
n->mark_interpreted();
@ -552,6 +552,7 @@ namespace euf {
void egraph::push_congruence(enode* n1, enode* n2, bool comm) {
SASSERT(is_app(n1->get_expr()));
SASSERT(n1->get_decl() == n2->get_decl());
m_uses_congruence = true;
if (m_used_cc && !comm) {
m_used_cc(to_app(n1->get_expr()), to_app(n2->get_expr()));
}
@ -598,6 +599,7 @@ namespace euf {
void egraph::begin_explain() {
SASSERT(m_todo.empty());
m_uses_congruence = false;
}
void egraph::end_explain() {
@ -672,15 +674,16 @@ namespace euf {
out << " " << p->get_expr_id();
out << "] ";
}
if (n->value() != l_undef) {
if (n->value() != l_undef)
out << "[v" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
}
if (n->has_th_vars()) {
out << "[t";
for (auto v : enode_th_vars(n))
out << " " << v.get_id() << ":" << v.get_var();
out << "] ";
}
if (n->generation() > 0)
out << "[g " << n->generation() << "] ";
if (n->m_target && m_display_justification)
n->m_justification.display(out << "[j " << n->m_target->get_expr_id() << " ", m_display_justification) << "] ";
out << "\n";
@ -722,7 +725,7 @@ namespace euf {
for (unsigned j = 0; j < n1->num_args(); ++j)
args.push_back(old_expr2new_enode[n1->get_arg(j)->get_expr_id()]);
expr* e2 = tr(e1);
enode* n2 = mk(e2, args.size(), args.c_ptr());
enode* n2 = mk(e2, n1->generation(), args.size(), args.c_ptr());
old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
n2->set_value(n2->value());
n2->m_bool_var = n1->m_bool_var;

6
src/ast/euf/euf_egraph.h
View file

@ -164,6 +164,7 @@ namespace euf {
bool_vector m_th_propagates_diseqs;
enode_vector m_todo;
stats m_stats;
bool m_uses_congruence { false };
std::function<void(expr*,expr*,expr*)> m_used_eq;
std::function<void(app*,app*)> m_used_cc;
std::function<void(std::ostream&, void*)> m_display_justification;
@ -180,7 +181,7 @@ namespace euf {
void add_literal(enode* n, bool is_eq);
void undo_eq(enode* r1, enode* n1, unsigned r2_num_parents);
void undo_add_th_var(enode* n, theory_id id);
enode* mk_enode(expr* f, unsigned num_args, enode * const* args);
enode* mk_enode(expr* f, unsigned generation, unsigned num_args, enode * const* args);
void force_push();
void set_conflict(enode* n1, enode* n2, justification j);
void merge(enode* n1, enode* n2, justification j);
@ -217,7 +218,7 @@ namespace euf {
egraph(ast_manager& m);
~egraph();
enode* find(expr* f) const { return m_expr2enode.get(f->get_id(), nullptr); }
enode* mk(expr* f, unsigned n, enode *const* args);
enode* mk(expr* f, unsigned generation, unsigned n, enode *const* args);
enode_vector const& enodes_of(func_decl* f);
void push() { ++m_num_scopes; }
void pop(unsigned num_scopes);
@ -272,6 +273,7 @@ namespace euf {
void begin_explain();
void end_explain();
bool uses_congruence() const { return m_uses_congruence; }
template <typename T>
void explain(ptr_vector<T>& justifications);
template <typename T>

27
src/ast/euf/euf_enode.h
View file

@ -45,17 +45,18 @@ namespace euf {
bool m_commutative{ false };
bool m_update_children{ false };
bool m_interpreted{ false };
bool m_merge_enabled{ true };
bool m_is_equality{ false };
lbool m_value;
unsigned m_bool_var { UINT_MAX };
unsigned m_class_size{ 1 };
unsigned m_table_id{ UINT_MAX };
bool m_merge_enabled{ true };
bool m_is_equality{ false }; // Does the expression represent an equality
lbool m_value; // Assignment by SAT solver for Boolean node
unsigned m_bool_var { UINT_MAX }; // SAT solver variable associated with Boolean node
unsigned m_class_size{ 1 }; // Size of the equivalence class if the enode is the root.
unsigned m_table_id{ UINT_MAX };
unsigned m_generation { 0 }; // Tracks how many quantifier instantiation rounds were needed to generate this enode.
enode_vector m_parents;
enode* m_next{ nullptr };
enode* m_root{ nullptr };
enode* m_target{ nullptr };
enode* m_cg { nullptr };
enode* m_next { nullptr };
enode* m_root { nullptr };
enode* m_target { nullptr };
enode* m_cg { nullptr };
th_var_list m_th_vars;
justification m_justification;
unsigned m_num_args{ 0 };
@ -72,13 +73,14 @@ namespace euf {
return sizeof(enode) + num_args * sizeof(enode*);
}
static enode* mk(region& r, expr* f, unsigned num_args, enode* const* args) {
static enode* mk(region& r, expr* f, unsigned generation, unsigned num_args, enode* const* args) {
SASSERT(num_args <= (is_app(f) ? to_app(f)->get_num_args() : 0));
void* mem = r.allocate(get_enode_size(num_args));
enode* n = new (mem) enode();
n->m_expr = f;
n->m_next = n;
n->m_root = n;
n->m_generation = generation,
n->m_commutative = num_args == 2 && is_app(f) && to_app(f)->get_decl()->is_commutative();
n->m_num_args = num_args;
n->m_merge_enabled = true;
@ -142,9 +144,12 @@ namespace euf {
enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; }
unsigned hash() const { return m_expr->hash(); }
unsigned get_table_id() const { return m_table_id; }
void set_table_id(unsigned t) { m_table_id = t; }
unsigned generation() const { return m_generation; }
void mark1() { m_mark1 = true; }
void unmark1() { m_mark1 = false; }
bool is_marked1() { return m_mark1; }

1
src/sat/smt/arith_axioms.cpp
View file

@ -312,6 +312,7 @@ namespace arith {
force_push();
expr* e1 = var2expr(v1);
expr* e2 = var2expr(v2);
TRACE("arith", tout << "new eq: v" << v1 << " v" << v2 << "\n";);
if (e1->get_id() > e2->get_id())
std::swap(e1, e2);

32
src/sat/smt/arith_solver.cpp
View file

@ -590,14 +590,17 @@ namespace arith {
theory_var v = n->get_th_var(get_id());
expr* o = n->get_expr();
expr_ref value(m);
if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
if (m.is_value(n->get_root()->get_expr())) {
value = n->get_root()->get_expr();
}
else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
anum const& an = nl_value(v, *m_a1);
if (a.is_int(o) && !m_nla->am().is_int(an))
value = a.mk_numeral(rational::zero(), a.is_int(o));
else
value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o));
}
else {
else if (v != euf::null_theory_var) {
rational r = get_value(v);
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
@ -605,9 +608,34 @@ namespace arith {
r = floor(r);
value = a.mk_numeral(r, m.get_sort(o));
}
else if (a.is_arith_expr(o)) {
expr_ref_vector args(m);
for (auto* arg : euf::enode_args(n)) {
if (m.is_value(arg->get_expr()))
args.push_back(arg->get_expr());
else
args.push_back(values.get(arg->get_root_id()));
}
value = m.mk_app(to_app(o)->get_decl(), args.size(), args.c_ptr());
ctx.get_rewriter()(value);
}
else {
UNREACHABLE();
}
values.set(n->get_root_id(), value);
}
void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
expr* e = n->get_expr();
if (a.is_arith_expr(e) && to_app(e)->get_num_args() > 0) {
for (auto* arg : euf::enode_args(n))
dep.add(n, arg);
}
else {
dep.insert(n, nullptr);
}
}
void solver::push_core() {
TRACE("arith_verbose", tout << "push\n";);
m_scopes.push_back(scope());

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

@ -429,6 +429,7 @@ namespace arith {
void init_model() override;
void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); }
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
void internalize(expr* e, bool redundant) override;
void eq_internalized(euf::enode* n) override;

8
src/sat/smt/euf_internalize.cpp
View file

@ -81,7 +81,7 @@ namespace euf {
if (auto* s = expr2solver(e))
s->internalize(e, m_is_redundant);
else
attach_node(m_egraph.mk(e, 0, nullptr));
attach_node(m_egraph.mk(e, m_generation, 0, nullptr));
return true;
}
@ -95,7 +95,7 @@ namespace euf {
if (auto* s = expr2solver(e))
s->internalize(e, m_is_redundant);
else
attach_node(m_egraph.mk(e, num, m_args.c_ptr()));
attach_node(m_egraph.mk(e, m_generation, num, m_args.c_ptr()));
return true;
}
@ -149,7 +149,7 @@ namespace euf {
m_var_trail.push_back(v);
enode* n = m_egraph.find(e);
if (!n)
n = m_egraph.mk(e, 0, nullptr);
n = m_egraph.mk(e, m_generation, 0, nullptr);
SASSERT(n->bool_var() == UINT_MAX || n->bool_var() == v);
m_egraph.set_bool_var(n, v);
if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
@ -249,7 +249,7 @@ namespace euf {
for (unsigned i = 0; i < sz; ++i) {
expr_ref fapp(m.mk_app(f, e->get_arg(i)), m);
expr_ref fresh(m.mk_fresh_const("dist-value", u), m);
enode* n = m_egraph.mk(fresh, 0, nullptr);
enode* n = m_egraph.mk(fresh, m_generation, 0, nullptr);
n->mark_interpreted();
expr_ref eq = mk_eq(fapp, fresh);
sat::literal lit = mk_literal(eq);

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

@ -112,6 +112,7 @@ namespace euf {
void solver::dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl) {
for (enode* n : deps.top_sorted()) {
unsigned id = n->get_root_id();
if (m_values.get(id, nullptr))
continue;
@ -181,15 +182,14 @@ namespace euf {
mdl->register_decl(f, v);
else {
auto* fi = mdl->get_func_interp(f);
if (!fi) {
if (!fi) {
fi = alloc(func_interp, m, arity);
mdl->register_decl(f, fi);
}
args.reset();
for (enode* arg : enode_args(n)) {
args.push_back(m_values.get(arg->get_root_id()));
SASSERT(args.back());
}
args.reset();
for (enode* arg : enode_args(n))
args.push_back(m_values.get(arg->get_root_id()));
DEBUG_CODE(for (expr* arg : args) VERIFY(arg););
SASSERT(args.size() == arity);
if (!fi->get_entry(args.c_ptr()))
fi->insert_new_entry(args.c_ptr(), v);
@ -207,6 +207,11 @@ namespace euf {
for (enode* n : m_egraph.nodes())
if (n->is_root() && m_values.get(n->get_expr_id()))
m_values2root.insert(m_values.get(n->get_expr_id()), n);
#if 0
for (auto kv : m_values2root) {
std::cout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";
}
#endif
return m_values2root;
}

38
src/sat/smt/euf_solver.cpp
View file

@ -41,7 +41,6 @@ namespace euf {
m_lookahead(nullptr),
m_to_m(&m),
m_to_si(&si),
m_reinit_exprs(m),
m_values(m)
{
updt_params(p);
@ -96,6 +95,8 @@ namespace euf {
return ext;
if (fid == m.get_basic_family_id())
return nullptr;
if (fid == m.get_user_sort_family_id())
return nullptr;
pb_util pb(m);
bv_util bvu(m);
array_util au(m);
@ -369,6 +370,8 @@ namespace euf {
m_explain.reset();
m_egraph.explain_eq<size_t>(m_explain, e.child(), e.root());
m_egraph.end_explain();
if (m_egraph.uses_congruence())
return false;
for (auto p : m_explain) {
if (is_literal(p))
return false;
@ -483,10 +486,11 @@ namespace euf {
}
void solver::start_reinit(unsigned n) {
m_reinit_exprs.reset();
m_reinit.reset();
for (sat::bool_var v : s().get_vars_to_reinit()) {
expr* e = bool_var2expr(v);
m_reinit_exprs.push_back(e);
if (e)
m_reinit.push_back(reinit_t(expr_ref(e, m), get_enode(e)?get_enode(e)->generation():0, v));
}
}
@ -496,8 +500,7 @@ namespace euf {
* and replaying internalization.
*/
void solver::finish_reinit() {
SASSERT(s().get_vars_to_reinit().size() == m_reinit_exprs.size());
if (s().get_vars_to_reinit().empty())
if (m_reinit.empty())
return;
struct scoped_set_replay {
@ -513,26 +516,23 @@ namespace euf {
scoped_set_replay replay(*this);
scoped_suspend_rlimit suspend_rlimit(m.limit());
unsigned i = 0;
for (sat::bool_var v : s().get_vars_to_reinit()) {
expr* e = m_reinit_exprs.get(i++);
if (e)
replay.m.insert(e, v);
}
if (replay.m.empty())
return;
for (auto const& t : m_reinit)
replay.m.insert(std::get<0>(t), std::get<2>(t));
TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";);
for (auto const& kv : replay.m) {
TRACE("euf", tout << "replay: " << kv.m_value << " " << mk_bounded_pp(kv.m_key, m) << "\n";);
for (auto const& t : m_reinit) {
expr_ref e = std::get<0>(t);
unsigned generation = std::get<1>(t);
sat::bool_var v = std::get<2>(t);
scoped_generation _sg(*this, generation);
TRACE("euf", tout << "replay: " << v << " " << mk_bounded_pp(e, m) << "\n";);
sat::literal lit;
expr* e = kv.m_key;
if (si.is_bool_op(e))
lit = literal(replay.m[e], false);
else
lit = si.internalize(kv.m_key, true);
VERIFY(lit.var() == kv.m_value);
attach_lit(lit, kv.m_key);
lit = si.internalize(e, true);
VERIFY(lit.var() == v);
attach_lit(lit, e);
}
TRACE("euf", display(tout << "replay done\n"););
}

19
src/sat/smt/euf_solver.h
View file

@ -95,6 +95,7 @@ namespace euf {
scoped_ptr<sat::dual_solver> m_dual_solver;
user::solver* m_user_propagator{ nullptr };
th_solver* m_qsolver { nullptr };
unsigned m_generation { 0 };
ptr_vector<expr> m_bool_var2expr;
ptr_vector<size_t> m_explain;
@ -121,7 +122,8 @@ namespace euf {
euf::enode* mk_false();
// replay
expr_ref_vector m_reinit_exprs;
typedef std::tuple<expr_ref, unsigned, sat::bool_var> reinit_t;
vector<reinit_t> m_reinit;
void start_reinit(unsigned num_scopes);
void finish_reinit();
@ -214,6 +216,19 @@ namespace euf {
}
};
struct scoped_generation {
solver& s;
unsigned m_g;
scoped_generation(solver& s, unsigned g):
s(s),
m_g(s.m_generation) {
s.m_generation = g;
}
~scoped_generation() {
s.m_generation = m_g;
}
};
// accessors
sat::sat_internalizer& get_si() { return si; }
@ -310,7 +325,7 @@ namespace euf {
void attach_node(euf::enode* n);
expr_ref mk_eq(expr* e1, expr* e2);
expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); }
euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); }
euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, m_generation, n, args); }
expr* bool_var2expr(sat::bool_var v) const { return m_bool_var2expr.get(v, nullptr); }
expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }

124
src/sat/smt/q_mbi.cpp
View file

@ -50,7 +50,7 @@ namespace q {
for (expr* e : universe)
eqs.push_back(m.mk_eq(sk, e));
expr_ref fml = mk_or(eqs);
std::cout << "restrict to universe " << fml << "\n";
// std::cout << "restrict to universe " << fml << "\n";
m_solver->assert_expr(fml);
}
@ -82,14 +82,15 @@ namespace q {
quantifier* q_flat = m_qs.flatten(q);
init_solver();
::solver::scoped_push _sp(*m_solver);
std::cout << "quantifier\n" << mk_pp(q, m, 4) << "\n";
std::cout << mk_pp(q, m, 4) << "\n";
// std::cout << *m_model << "\n";
auto* qb = specialize(q_flat);
if (!qb)
return l_undef;
// return l_undef;
if (m.is_false(qb->mbody))
return l_true;
std::cout << "body\n" << qb->mbody << "\n";
// std::cout << "body\n" << qb->mbody << "\n";
m_solver->assert_expr(qb->mbody);
lbool r = m_solver->check_sat(0, nullptr);
if (r == l_undef)
@ -103,37 +104,29 @@ namespace q {
if (is_exists(q))
qlit.neg();
unsigned i = 0;
expr_ref_vector eqs(m);
if (!qb->var_args.empty()) {
::solver::scoped_push _sp(*m_solver);
add_domain_eqs(*mdl0, *qb);
std::cout << "check\n";
for (; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) {
m_solver->get_model(mdl1);
proj = solver_project(*mdl1, *qb);
proj = solver_project(*mdl1, *qb, eqs, true);
if (!proj)
break;
TRACE("q", tout << "project: " << proj << "\n";);
std::cout << "project\n" << proj << "\n";
std::cout << *m_model << "\n";
std::cout << "eqs: " << eqs << "\n";
static unsigned s_count = 0;
++s_count;
if (s_count == 3)
exit(0);
++m_stats.m_num_instantiations;
m_qs.add_clause(~qlit, ~ctx.mk_literal(proj));
m_solver->assert_expr(m.mk_not(proj));
add_instantiation(qlit, proj);
m_solver->assert_expr(m.mk_not(mk_and(eqs)));
}
}
if (i == 0) {
add_domain_bounds(*mdl0, *qb);
proj = solver_project(*mdl0, *qb);
proj = solver_project(*mdl0, *qb, eqs, false);
if (!proj)
return l_undef;
std::cout << "project-base\n" << proj << "\n";
TRACE("q", tout << "project-base: " << proj << "\n";);
++m_stats.m_num_instantiations;
m_qs.add_clause(~qlit, ~ctx.mk_literal(proj));
add_instantiation(qlit, proj);
}
// TODO: add as top-level clause for relevancy
return l_false;
@ -142,30 +135,45 @@ namespace q {
mbqi::q_body* mbqi::specialize(quantifier* q) {
mbqi::q_body* result = nullptr;
var_subst subst(m);
unsigned sz = q->get_num_decls();
if (!m_q2body.find(q, result)) {
unsigned sz = q->get_num_decls();
result = alloc(q_body, m);
m_q2body.insert(q, result);
ctx.push(new_obj_trail<euf::solver, q_body>(result));
ctx.push(insert_obj_map<euf::solver, quantifier, q_body*>(m_q2body, q));
obj_hashtable<expr> _vars;
app_ref_vector& vars = result->vars;
vars.resize(sz, nullptr);
for (unsigned i = 0; i < sz; ++i) {
sort* s = q->get_decl_sort(i);
vars[i] = m.mk_fresh_const(q->get_decl_name(i), s, false);
if (m_model->has_uninterpreted_sort(s))
restrict_to_universe(vars.get(i), m_model->get_universe(s));
_vars.insert(vars.get(i));
}
expr_ref fml = subst(q->get_expr(), vars);
extract_var_args(q->get_expr(), *result);
if (is_forall(q))
fml = m.mk_not(fml);
flatten_and(fml, result->vbody);
for (expr* e : result->vbody) {
expr* e1 = nullptr, *e2 = nullptr;
if (m.is_not(e, e) && m.is_eq(e, e1, e2)) {
if (_vars.contains(e1) && !_vars.contains(e2) && is_app(e2))
result->var_diff.push_back(std::make_pair(to_app(e1), to_app(e2)->get_decl()));
else if (_vars.contains(e2) && !_vars.contains(e1) && is_app(e1))
result->var_diff.push_back(std::make_pair(to_app(e2), to_app(e1)->get_decl()));
}
}
}
expr_ref& mbody = result->mbody;
if (!m_model->eval_expr(q->get_expr(), mbody, true))
return nullptr;
for (unsigned i = 0; i < sz; ++i) {
sort* s = q->get_decl_sort(i);
if (m_model->has_uninterpreted_sort(s))
restrict_to_universe(result->vars.get(i), m_model->get_universe(s));
}
mbody = subst(mbody, result->vars);
if (is_forall(q))
mbody = mk_not(m, mbody);
@ -173,7 +181,8 @@ namespace q {
return result;
}
expr_ref mbqi::solver_project(model& mdl, q_body& qb) {
expr_ref mbqi::solver_project(model& mdl, q_body& qb, expr_ref_vector& eqs, bool use_inst) {
eqs.reset();
model::scoped_model_completion _sc(mdl, true);
for (app* v : qb.vars)
m_model->register_decl(v->get_decl(), mdl(v));
@ -186,13 +195,14 @@ namespace q {
tout << fmls << "\n";
tout << "model of projection\n" << mdl << "\n";
tout << "var args: " << qb.var_args.size() << "\n";
tout << "domain eqs: " << qb.domain_eqs << "\n";
for (expr* f : fmls)
if (m_model->is_false(f))
tout << mk_pp(f, m) << " := false\n";
tout << "vars: " << vars << "\n";);
expr_safe_replace rep(m);
for (unsigned i = 0; i < vars.size(); ++i) {
for (unsigned i = 0; !use_inst && i < vars.size(); ++i) {
app* v = vars.get(i);
auto* p = get_plugin(v);
if (p && !fmls_extracted) {
@ -213,6 +223,7 @@ namespace q {
rep.insert(v, term);
if (val != term)
rep.insert(val, term);
eqs.push_back(m.mk_eq(v, val));
}
rep(fmls);
return mk_and(fmls);
@ -228,7 +239,59 @@ namespace q {
void mbqi::add_domain_eqs(model& mdl, q_body& qb) {
qb.domain_eqs.reset();
var_subst subst(m);
expr_mark diff_vars;
for (auto vd : qb.var_diff) {
app* v = vd.first;
func_decl* f = vd.second;
expr_ref_vector diff_set(m), vdiff_set(m);
typedef std::tuple<euf::enode*, unsigned, unsigned> tup;
svector<tup> todo;
expr_mark visited;
expr_ref val(m);
for (euf::enode* n : ctx.get_egraph().enodes_of(f)) {
euf::enode* r1 = n->get_root();
expr* e1 = n->get_expr();
todo.push_back(tup(r1, 2, 2));
for (unsigned i = 0; i < todo.size(); ++i) {
auto t = todo[i];
euf::enode* r2 = std::get<0>(t)->get_root();
expr* e2 = r2->get_expr();
if (visited.is_marked(e2))
continue;
visited.mark(e2);
std::cout << "try: " << mk_bounded_pp(e2, m) << " " << std::get<1>(t) << " " << std::get<2>(t) << "\n";
if (r1 != r2 && m.get_sort(e1) == m.get_sort(e2) && m_model->eval_expr(e2, val, true) && !visited.is_marked(val)) {
visited.mark(val);
diff_set.push_back(m.mk_eq(v, val));
vdiff_set.push_back(m.mk_eq(v, e2));
}
if (std::get<1>(t) > 0)
for (euf::enode* p : euf::enode_parents(r2))
todo.push_back(tup(p, std::get<1>(t)-1, std::get<2>(t)+1));
if (std::get<2>(t) > 0)
for (euf::enode* n : euf::enode_class(r2))
for (euf::enode* arg : euf::enode_args(n))
todo.push_back(tup(arg, 0, std::get<2>(t)-1));
}
todo.reset();
}
if (!diff_set.empty()) {
diff_vars.mark(v);
expr_ref diff = mk_or(diff_set);
expr_ref vdiff = mk_or(vdiff_set);
std::cout << "diff: " << vdiff_set << "\n";
m_solver->assert_expr(diff);
qb.domain_eqs.push_back(vdiff);
}
std::cout << "var-diff: " << mk_pp(vd.first, m) << " " << mk_pp(vd.second, m) << "\n";
}
for (auto p : qb.var_args) {
expr_ref arg(p.first->get_arg(p.second), m);
arg = subst(arg, qb.vars);
if (diff_vars.is_marked(arg))
continue;
expr_ref bounds = m_model_fixer.restrict_arg(p.first, p.second);
if (m.is_true(bounds))
continue;
@ -237,13 +300,15 @@ namespace q {
if (!m_model->eval_expr(bounds, mbounds, true))
return;
mbounds = subst(mbounds, qb.vars);
std::cout << "bounds: " << mk_pp(p.first, m) << " @ " << p.second << " - " << bounds << "\n";
std::cout << "domain eqs " << mbounds << "\n";
std::cout << "vbounds " << vbounds << "\n";
std::cout << *m_model << "\n";
m_solver->assert_expr(mbounds);
qb.domain_eqs.push_back(vbounds);
}
}
/*
* Add bounds to sub-terms under uninterpreted functions for projection.
*/
@ -279,8 +344,13 @@ namespace q {
expr_safe_replace rep(m);
var_subst subst(m);
expr_ref_vector eqs(m);
expr_mark visited;
for (auto p : qb.var_args) {
expr_ref _term = subst(p.first, qb.vars);
expr* e = p.first;
if (visited.is_marked(e))
continue;
visited.mark(e);
expr_ref _term = subst(e, qb.vars);
app_ref term(to_app(_term), m);
expr_ref value = (*m_model)(term);
expr* s = m_model_fixer.invert_app(term, value);
@ -313,6 +383,7 @@ namespace q {
lbool mbqi::operator()() {
lbool result = l_true;
m_model = nullptr;
m_instantiations.reset();
for (sat::literal lit : m_qs.m_universal) {
quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
if (!ctx.is_relevant(q))
@ -331,6 +402,9 @@ namespace q {
}
}
m_max_cex += ctx.get_config().m_mbqi_max_cexs;
for (auto p : m_instantiations)
m_qs.add_clause(~p.first, ~ctx.mk_literal(p.second));
m_instantiations.reset();
return result;
}

9
src/sat/smt/q_mbi.h
View file

@ -44,6 +44,7 @@ namespace q {
expr_ref mbody; // body specialized with respect to model
expr_ref_vector vbody; // (negation of) body specialized with respect to vars
expr_ref_vector domain_eqs; // additional domain restrictions
svector<std::pair<app*,func_decl*>> var_diff; // variable differences
svector<std::pair<app*, unsigned>> var_args; // (uninterpreted) functions in vbody that contain arguments with variables
q_body(ast_manager& m) : vars(m), mbody(m), vbody(m), domain_eqs(m) {}
};
@ -59,6 +60,7 @@ namespace q {
scoped_ptr_vector<mbp::project_plugin> m_plugins;
obj_map<quantifier, q_body*> m_q2body;
unsigned m_max_cex{ 1 };
vector<std::pair<sat::literal, expr_ref>> m_instantiations;
void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe);
// void register_value(expr* e);
@ -66,7 +68,7 @@ namespace q {
expr_ref choose_term(euf::enode* r);
lbool check_forall(quantifier* q);
q_body* specialize(quantifier* q);
expr_ref solver_project(model& mdl, q_body& qb);
expr_ref solver_project(model& mdl, q_body& qb, expr_ref_vector& eqs, bool use_inst);
void add_domain_eqs(model& mdl, q_body& qb);
void add_domain_bounds(model& mdl, q_body& qb);
void eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb);
@ -75,6 +77,11 @@ namespace q {
void init_solver();
mbp::project_plugin* get_plugin(app* var);
void add_plugin(mbp::project_plugin* p);
void add_instantiation(sat::literal qlit, expr_ref& proj) {
TRACE("q", tout << "project: " << proj << "\n";);
++m_stats.m_num_instantiations;
m_instantiations.push_back(std::make_pair(qlit, proj));
}
public:

6
src/sat/smt/q_model_fixer.cpp
View file

@ -220,8 +220,10 @@ namespace q {
euf::enode* r = nullptr;
TRACE("q",
tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
if (ctx.values2root().find(value, r))
tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";);
if (ctx.values2root().find(value, r))
tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";
ctx.display(tout);
);
if (ctx.values2root().find(value, r))
return r->get_expr();
return value;