3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
relevancy propagation applies to quantifier unfolding.
This commit is contained in:
Nikolaj Bjorner 2021-07-29 15:04:49 -07:00
parent 211a6c8752
commit b8a437bd8a
8 changed files with 60 additions and 36 deletions

View file

@ -248,8 +248,7 @@ public:
}
}
void operator()(quantifier * n) {
display_def_header(n);
void display_quantifier_header(quantifier* n) {
m_out << "(" << (n->get_kind() == forall_k ? "forall" : (n->get_kind() == exists_k ? "exists" : "lambda")) << " ";
unsigned num_decls = n->get_num_decls();
m_out << "(vars ";
@ -272,6 +271,12 @@ public:
display_children(n->get_num_no_patterns(), n->get_no_patterns());
m_out << ") ";
}
}
void operator()(quantifier * n) {
display_def_header(n);
display_quantifier_header(n);
display_child(n->get_expr());
m_out << ")\n";
}
@ -281,6 +286,12 @@ public:
m_out << "(:var " << to_var(n)->get_idx() << ")";
return;
}
if (is_quantifier(n)) {
display_quantifier_header(to_quantifier(n));
display(to_quantifier(n)->get_expr(), depth - 1);
m_out << ")";
return;
}
if (!is_app(n) || depth == 0 || to_app(n)->get_num_args() == 0) {
display_child(n);
@ -304,16 +315,11 @@ public:
void display_bounded(ast * n, unsigned depth) {
if (!n)
m_out << "null";
else if (is_app(n)) {
display(to_expr(n), depth);
}
else if (is_var(n)) {
m_out << "(:var " << to_var(n)->get_idx() << ")";
}
else {
m_out << "#" << n->get_id();
}
m_out << "null";
else if (is_expr(n))
display(to_expr(n), depth);
else
m_out << "#" << n->get_id();
}
};

View file

@ -281,9 +281,9 @@ struct pull_quant::imp {
m.mk_rewrite(old_q, result);
return true;
}
if (is_lambda(old_q)) {
return false;
}
if (is_lambda(old_q))
return false;
if (!is_forall(new_body))
return false;

View file

@ -336,7 +336,6 @@ namespace recfun {
return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
}
void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
expr_ref rhs1(rhs, m());
if (!is_macro)
@ -531,7 +530,6 @@ namespace recfun {
}
return result;
}
}
case_expansion::case_expansion(recfun::util& u, app * n) :

View file

@ -48,8 +48,7 @@ namespace euf {
if (!relevancy_enabled())
return;
ensure_dual_solver();
if (s().at_search_lvl())
m_dual_solver->add_root(n, lits);
m_dual_solver->add_root(n, lits);
}
void solver::add_aux(unsigned n, sat::literal const* lits) {

View file

@ -489,6 +489,8 @@ namespace euf {
for (auto* e : m_solvers)
e->push();
m_egraph.push();
if (m_dual_solver)
m_dual_solver->push();
}
void solver::pop(unsigned n) {
@ -506,20 +508,18 @@ namespace euf {
}
m_var_trail.shrink(sc.m_var_lim);
m_scopes.shrink(m_scopes.size() - n);
if (m_dual_solver)
m_dual_solver->pop(n);
SASSERT(m_egraph.num_scopes() == m_scopes.size());
TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
}
void solver::user_push() {
push();
if (m_dual_solver)
m_dual_solver->push();
push();
}
void solver::user_pop(unsigned n) {
pop(n);
if (m_dual_solver)
m_dual_solver->pop(n);
}
void solver::start_reinit(unsigned n) {

View file

@ -66,10 +66,11 @@ namespace q {
}
}
m_max_cex += ctx.get_config().m_mbqi_max_cexs;
for (auto p : m_instantiations) {
unsigned generation = std::get<2>(p);
for (auto [qlit, fml, generation] : m_instantiations) {
euf::solver::scoped_generation sg(ctx, generation + 1);
m_qs.add_clause(~std::get<0>(p), ~ctx.mk_literal(std::get<1>(p)));
sat::literal lit = ctx.mk_literal(fml);
m_qs.add_clause(~qlit, ~lit);
ctx.add_root(~qlit, ~lit);
}
m_instantiations.reset();
return result;

View file

@ -28,15 +28,28 @@ namespace sat {
SASSERT(!m_solver.get_config().m_drat);
}
void dual_solver::push() {
m_solver.user_push();
m_roots.push_scope();
m_tracked_vars.push_scope();
m_units.push_scope();
m_vars.push_scope();
void dual_solver::flush() {
while (m_num_scopes > 0) {
m_solver.user_push();
m_roots.push_scope();
m_tracked_vars.push_scope();
m_units.push_scope();
m_vars.push_scope();
--m_num_scopes;
}
}
void dual_solver::pop(unsigned num_scopes) {
void dual_solver::push() {
++m_num_scopes;
}
void dual_solver::pop(unsigned num_scopes) {
if (m_num_scopes >= num_scopes) {
m_num_scopes -= num_scopes;
return;
}
num_scopes -= m_num_scopes;
m_num_scopes = 0;
m_solver.user_pop(num_scopes);
unsigned old_sz = m_tracked_vars.old_size(num_scopes);
for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
@ -66,6 +79,7 @@ namespace sat {
}
void dual_solver::track_relevancy(bool_var w) {
flush();
bool_var v = ext2var(w);
if (!m_is_tracked.get(v, false)) {
m_is_tracked.setx(v, true, false);
@ -81,7 +95,8 @@ namespace sat {
return literal(m_var2ext[lit.var()], lit.sign());
}
void dual_solver::add_root(unsigned sz, literal const* clause) {
void dual_solver::add_root(unsigned sz, literal const* clause) {
flush();
if (sz == 1) {
TRACE("dual", tout << "unit: " << clause[0] << "\n";);
m_units.push_back(clause[0]);
@ -95,6 +110,7 @@ namespace sat {
}
void dual_solver::add_aux(unsigned sz, literal const* clause) {
flush();
TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << "\n";);
m_lits.reset();
for (unsigned i = 0; i < sz; ++i)
@ -103,6 +119,7 @@ namespace sat {
}
void dual_solver::add_assumptions(solver const& s) {
flush();
m_lits.reset();
for (bool_var v : m_tracked_vars)
m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
@ -113,7 +130,7 @@ namespace sat {
}
}
bool dual_solver::operator()(solver const& s) {
bool dual_solver::operator()(solver const& s) {
m_core.reset();
m_core.append(m_units);
if (m_roots.empty())

View file

@ -35,6 +35,7 @@ namespace sat {
unsigned_vector m_ext2var;
unsigned_vector m_var2ext;
lim_svector<unsigned> m_vars;
unsigned m_num_scopes = 0;
void add_literal(literal lit);
bool_var ext2var(bool_var v);
@ -46,6 +47,8 @@ namespace sat {
std::ostream& display(solver const& s, std::ostream& out) const;
void flush();
public:
dual_solver(reslimit& l);
void push();