mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

disable all propagation until ematch incompleteness is fixed

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-05 11:25:35 -07:00
parent 94cc4ead72
commit c0c3e685e7
3 changed files with 14 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -236,9 +236,10 @@ namespace q {
}
binding* ematch::alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) {
binding* b = tmp_binding(c, pat, _binding);
if (m_bindings.contains(b))
if (m_bindings.contains(b))
return nullptr;
for (unsigned i = c.num_decls(); i-- > 0; )
@ -260,12 +261,12 @@ namespace q {
return b;
}
euf::enode* const* ematch::alloc_nodes(clause& c, euf::enode* const* _binding) {
euf::enode* const* ematch::copy_nodes(clause& c, euf::enode* const* nodes) {
unsigned sz = sizeof(euf::enode* const*) * c.num_decls();
euf::enode** binding = (euf::enode**)ctx.get_region().allocate(sz);
euf::enode** new_nodes = (euf::enode**)ctx.get_region().allocate(sz);
for (unsigned i = 0; i < c.num_decls(); ++i)
binding[i] = _binding[i];
return binding;
new_nodes[i] = nodes[i];
return new_nodes;
}
void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) {
@ -277,7 +278,7 @@ namespace q {
if (!b)
return;
if (propagate(false, _binding, max_generation, c, new_propagation))
if (false && propagate(false, _binding, max_generation, c, new_propagation))
return;
binding::push_to_front(c.m_bindings, b);
@ -305,7 +306,7 @@ namespace q {
if (ev == l_undef && max_generation > m_generation_propagation_threshold)
return false;
if (!is_owned)
binding = alloc_nodes(c, binding);
binding = copy_nodes(c, binding);
auto j_idx = mk_justification(idx, c, binding);
@ -568,7 +569,7 @@ namespace q {
continue;
do {
if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated))
if (false && propagate(true, b->m_nodes, b->m_max_generation, c, propagated))
to_remove.push_back(b);
else if (flush) {
instantiate(*b);
@ -613,6 +614,7 @@ namespace q {
for (unsigned i = 0; i < m_clauses.size(); ++i)
if (m_clauses[i]->m_bindings)
std::cout << "missed propagation " << i << "\n";
TRACE("q", tout << "no more propagation\n";);
return false;
}

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

@ -89,7 +89,7 @@ namespace q {
unsigned_vector m_clause_queue;
euf::enode_pair_vector m_evidence;
euf::enode* const* alloc_nodes(clause& c, euf::enode* const* _binding);
euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding);
binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding);
binding* alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top);
@ -127,7 +127,6 @@ namespace q {
bool unit_propagate();
// void init_search();
void add(quantifier* q);

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

@ -146,7 +146,7 @@ namespace q {
unsigned gen = get_new_gen(f, ent.m_cost);
bool new_propagation = false;
if (em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
if (false && em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
return;
auto* ebindings = m_subst(q, num_bindings);
@ -223,15 +223,14 @@ namespace q {
}
}
bool instantiated = false;
unsigned idx = 0;
for (entry & e : m_delayed_entries) {
for (unsigned idx = 0; idx < m_delayed_entries.size(); ++idx) {
entry & e = m_delayed_entries[idx];
if (!e.m_instantiated && e.m_cost <= cost_limit) {
instantiated = true;
ctx.push(reset_instantiated(*this, idx));
m_stats.m_num_lazy_instances++;
instantiate(e);
}
++idx;
}
return instantiated;
}