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

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-16 21:24:50 -05:00
parent df9084ba23
commit 1dedfe3164
4 changed files with 18 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/q_clause.h
View file

@ -56,8 +56,8 @@ namespace q {
vector<lit> m_lits; vector<lit> m_lits;
quantifier_ref m_q; quantifier_ref m_q;
sat::literal m_literal; sat::literal m_literal;
q::quantifier_stat* m_stat { nullptr }; q::quantifier_stat* m_stat = nullptr;
binding* m_bindings { nullptr }; binding* m_bindings = nullptr;
clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {} clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {}

16
src/sat/smt/q_ematch.cpp
View file

@ -213,6 +213,14 @@ namespace q {
unsigned sz = sizeof(binding) + sizeof(euf::enode* const*)*n; unsigned sz = sizeof(binding) + sizeof(euf::enode* const*)*n;
void* mem = ctx.get_region().allocate(sz); void* mem = ctx.get_region().allocate(sz);
return new (mem) binding(pat, max_generation, min_top, max_top); return new (mem) binding(pat, max_generation, min_top, max_top);
}
euf::enode* const* ematch::alloc_binding(clause& c, euf::enode* const* _binding) {
unsigned sz = sizeof(euf::enode* const*) * c.num_decls();
euf::enode** binding = (euf::enode**)ctx.get_region().allocate(sz);
for (unsigned i = 0; i < c.num_decls(); ++i)
binding[i] = _binding[i];
return binding;
} }
void ematch::add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) { void ematch::add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) {
@ -230,11 +238,11 @@ namespace q {
unsigned idx = m_q2clauses[q]; unsigned idx = m_q2clauses[q];
clause& c = *m_clauses[idx]; clause& c = *m_clauses[idx];
bool new_propagation = false; bool new_propagation = false;
if (!propagate(_binding, max_generation, c, new_propagation)) if (!propagate(false, _binding, max_generation, c, new_propagation))
add_binding(c, pat, _binding, max_generation, min_gen, max_gen); add_binding(c, pat, _binding, max_generation, min_gen, max_gen);
} }
bool ematch::propagate(euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) { bool ematch::propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) {
TRACE("q", c.display(ctx, tout) << "\n";); TRACE("q", c.display(ctx, tout) << "\n";);
unsigned idx = UINT_MAX; unsigned idx = UINT_MAX;
lbool ev = m_eval(binding, c, idx); lbool ev = m_eval(binding, c, idx);
@ -252,6 +260,8 @@ namespace q {
} }
if (ev == l_undef && max_generation > m_generation_propagation_threshold) if (ev == l_undef && max_generation > m_generation_propagation_threshold)
return false; return false;
if (!is_owned)
binding = alloc_binding(c, binding);
auto j_idx = mk_justification(idx, c, binding); auto j_idx = mk_justification(idx, c, binding);
if (ev == l_false) { if (ev == l_false) {
++m_stats.m_num_conflicts; ++m_stats.m_num_conflicts;
@ -482,7 +492,7 @@ namespace q {
continue; continue;
do { do {
if (propagate(b->m_nodes, b->m_max_generation, c, propagated)) if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated))
to_remove.push_back(b); to_remove.push_back(b);
else if (flush) { else if (flush) {
instantiate(*b, c); instantiate(*b, c);

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

@ -81,6 +81,7 @@ namespace q {
unsigned_vector m_clause_queue; unsigned_vector m_clause_queue;
binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top); binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top);
euf::enode* const* alloc_binding(clause& c, euf::enode* const* _binding);
void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top); void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top);
sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b); sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b);
@ -130,7 +131,7 @@ namespace q {
void add_instantiation(clause& c, binding& b, sat::literal lit); void add_instantiation(clause& c, binding& b, sat::literal lit);
bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c, bool& new_propagation); bool propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& new_propagation);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;

2
src/sat/smt/q_queue.cpp
View file

@ -146,7 +146,7 @@ namespace q {
unsigned gen = get_new_gen(f, ent.m_cost); unsigned gen = get_new_gen(f, ent.m_cost);
bool new_propagation = false; bool new_propagation = false;
if (em.propagate(f.nodes(), gen, *f.c, new_propagation)) if (em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
return; return;
auto* ebindings = m_subst(q, num_bindings); auto* ebindings = m_subst(q, num_bindings);