mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
add nff and auto-relevant
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
bc2020a39b
commit
d5e5dcfe45
|
@ -22,6 +22,31 @@ Author:
|
|||
|
||||
namespace euf {
|
||||
|
||||
void solver::add_auto_relevant(expr* e) {
|
||||
if (!relevancy_enabled())
|
||||
return;
|
||||
for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes)
|
||||
m_auto_relevant_lim.push_back(m_auto_relevant.size());
|
||||
m_auto_relevant.push_back(e);
|
||||
}
|
||||
|
||||
void solver::pop_relevant(unsigned n) {
|
||||
if (m_auto_relevant_scopes >= n) {
|
||||
m_auto_relevant_scopes -= n;
|
||||
return;
|
||||
}
|
||||
n -= m_auto_relevant_scopes;
|
||||
m_auto_relevant_scopes = 0;
|
||||
unsigned top = m_auto_relevant_lim.size() - n;
|
||||
unsigned lim = m_auto_relevant_lim[top];
|
||||
m_auto_relevant_lim.shrink(top);
|
||||
m_auto_relevant.shrink(lim);
|
||||
}
|
||||
|
||||
void solver::push_relevant() {
|
||||
++m_auto_relevant_scopes;
|
||||
}
|
||||
|
||||
bool solver::is_relevant(expr* e) const {
|
||||
return m_relevant_expr_ids.get(e->get_id(), true);
|
||||
}
|
||||
|
@ -31,11 +56,11 @@ namespace euf {
|
|||
}
|
||||
|
||||
void solver::ensure_dual_solver() {
|
||||
if (!m_dual_solver) {
|
||||
m_dual_solver = alloc(sat::dual_solver, s().rlimit());
|
||||
for (unsigned i = s().num_user_scopes(); i-- > 0; )
|
||||
m_dual_solver->push();
|
||||
}
|
||||
if (m_dual_solver)
|
||||
return;
|
||||
m_dual_solver = alloc(sat::dual_solver, s().rlimit());
|
||||
for (unsigned i = s().num_user_scopes(); i-- > 0; )
|
||||
m_dual_solver->push();
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -65,8 +90,6 @@ namespace euf {
|
|||
|
||||
bool solver::init_relevancy() {
|
||||
m_relevant_expr_ids.reset();
|
||||
bool_vector visited;
|
||||
ptr_vector<expr> todo;
|
||||
if (!relevancy_enabled())
|
||||
return true;
|
||||
if (!m_dual_solver)
|
||||
|
@ -77,12 +100,16 @@ namespace euf {
|
|||
for (enode* n : m_egraph.nodes())
|
||||
max_id = std::max(max_id, n->get_expr_id());
|
||||
m_relevant_expr_ids.resize(max_id + 1, false);
|
||||
ptr_vector<expr>& todo = m_relevant_todo;
|
||||
bool_vector& visited = m_relevant_visited;
|
||||
auto const& core = m_dual_solver->core();
|
||||
todo.reset();
|
||||
for (auto lit : core) {
|
||||
expr* e = m_bool_var2expr.get(lit.var(), nullptr);
|
||||
if (e)
|
||||
todo.push_back(e);
|
||||
}
|
||||
todo.append(m_auto_relevant);
|
||||
for (unsigned i = 0; i < todo.size(); ++i) {
|
||||
expr* e = todo[i];
|
||||
if (visited.get(e->get_id(), false))
|
||||
|
@ -114,6 +141,9 @@ namespace euf {
|
|||
todo.push_back(arg);
|
||||
}
|
||||
|
||||
for (auto * e : todo)
|
||||
visited[e->get_id()] = false;
|
||||
|
||||
TRACE("euf",
|
||||
for (enode* n : m_egraph.nodes())
|
||||
if (is_relevant(n))
|
||||
|
|
|
@ -183,6 +183,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
void solver::propagate(literal lit, ext_justification_idx idx) {
|
||||
add_auto_relevant(bool_var2expr(lit.var()));
|
||||
s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
|
||||
}
|
||||
|
||||
|
|
|
@ -99,8 +99,7 @@ namespace euf {
|
|||
sat::lookahead* m_lookahead = nullptr;
|
||||
ast_manager* m_to_m;
|
||||
sat::sat_internalizer* m_to_si;
|
||||
scoped_ptr<euf::ackerman> m_ackerman;
|
||||
scoped_ptr<sat::dual_solver> m_dual_solver;
|
||||
scoped_ptr<euf::ackerman> m_ackerman;
|
||||
user_solver::solver* m_user_propagator = nullptr;
|
||||
th_solver* m_qsolver = nullptr;
|
||||
unsigned m_generation = 0;
|
||||
|
@ -182,6 +181,8 @@ namespace euf {
|
|||
|
||||
// relevancy
|
||||
bool_vector m_relevant_expr_ids;
|
||||
bool_vector m_relevant_visited;
|
||||
ptr_vector<expr> m_relevant_todo;
|
||||
void ensure_dual_solver();
|
||||
bool init_relevancy();
|
||||
|
||||
|
@ -363,6 +364,11 @@ namespace euf {
|
|||
|
||||
// relevancy
|
||||
bool m_relevancy = true;
|
||||
scoped_ptr<sat::dual_solver> m_dual_solver;
|
||||
ptr_vector<expr> m_auto_relevant;
|
||||
unsigned_vector m_auto_relevant_lim;
|
||||
unsigned m_auto_relevant_scopes = 0;
|
||||
|
||||
bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; }
|
||||
void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false; }
|
||||
void add_root(unsigned n, sat::literal const* lits);
|
||||
|
@ -377,6 +383,9 @@ namespace euf {
|
|||
void track_relevancy(sat::bool_var v);
|
||||
bool is_relevant(expr* e) const;
|
||||
bool is_relevant(enode* n) const;
|
||||
void add_auto_relevant(expr* e);
|
||||
void pop_relevant(unsigned n);
|
||||
void push_relevant();
|
||||
|
||||
|
||||
// model construction
|
||||
|
|
|
@ -54,7 +54,11 @@ namespace q {
|
|||
m_eval(ctx),
|
||||
m_qstat_gen(m, ctx.get_region()),
|
||||
m_inst_queue(*this, ctx),
|
||||
m_infer_patterns(m, ctx.get_config())
|
||||
m_infer_patterns(m, ctx.get_config()),
|
||||
m_new_defs(m),
|
||||
m_new_proofs(m),
|
||||
m_dn(m),
|
||||
m_nnf(m, m_dn)
|
||||
{
|
||||
std::function<void(euf::enode*, euf::enode*)> _on_merge =
|
||||
[&](euf::enode* root, euf::enode* other) {
|
||||
|
@ -105,6 +109,20 @@ namespace q {
|
|||
m_eval.explain(l, justification::from_index(idx), r, probing);
|
||||
}
|
||||
|
||||
quantifier_ref ematch::nnf_skolem(quantifier* q) {
|
||||
expr_ref r(m);
|
||||
proof_ref p(m);
|
||||
m_new_defs.reset();
|
||||
m_new_proofs.reset();
|
||||
m_nnf(q, m_new_defs, m_new_proofs, r, p);
|
||||
SASSERT(is_quantifier(r));
|
||||
for (expr* d : m_new_defs)
|
||||
m_qs.add_unit(m_qs.mk_literal(d));
|
||||
CTRACE("q", r != q, tout << mk_pp(q, m) << " -->\n" << r << "\n" << m_new_defs << "\n";);
|
||||
return quantifier_ref(to_quantifier(r), m);
|
||||
}
|
||||
|
||||
|
||||
std::ostream& ematch::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
|
||||
auto& j = justification::from_index(idx);
|
||||
auto& c = j.m_clause;
|
||||
|
@ -218,8 +236,6 @@ namespace q {
|
|||
}
|
||||
};
|
||||
|
||||
|
||||
|
||||
binding* ematch::tmp_binding(clause& c, app* pat, euf::enode* const* b) {
|
||||
if (c.num_decls() > m_tmp_binding_capacity) {
|
||||
void* mem = memory::allocate(sizeof(binding) + c.num_decls() * sizeof(euf::enode*));
|
||||
|
@ -430,7 +446,10 @@ namespace q {
|
|||
cl->m_literal.neg();
|
||||
expr_ref body(mk_not(m, q->get_expr()), m);
|
||||
q = m.update_quantifier(q, forall_k, body);
|
||||
}
|
||||
}
|
||||
q = nnf_skolem(q);
|
||||
|
||||
|
||||
expr_ref_vector ors(m);
|
||||
flatten_or(q->get_expr(), ors);
|
||||
for (expr* arg : ors)
|
||||
|
|
|
@ -19,6 +19,7 @@ Author:
|
|||
#include "util/nat_set.h"
|
||||
#include "ast/quantifier_stat.h"
|
||||
#include "ast/pattern/pattern_inference.h"
|
||||
#include "ast/normal_forms/nnf.h"
|
||||
#include "solver/solver.h"
|
||||
#include "sat/smt/sat_th.h"
|
||||
#include "sat/smt/q_mam.h"
|
||||
|
@ -119,6 +120,13 @@ namespace q {
|
|||
|
||||
bool propagate(bool flush);
|
||||
|
||||
expr_ref_vector m_new_defs;
|
||||
proof_ref_vector m_new_proofs;
|
||||
defined_names m_dn;
|
||||
nnf m_nnf;
|
||||
|
||||
quantifier_ref nnf_skolem(quantifier* q);
|
||||
|
||||
public:
|
||||
|
||||
ematch(euf::solver& ctx, solver& s);
|
||||
|
|
Loading…
Reference in a new issue