mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Code Activity

#5518

Browse source 
patch a gaping hole in recfun
This commit is contained in:
Nikolaj Bjorner 2021-08-31 19:49:18 -07:00
parent 1426390aec
commit 7c782a7ef8
1 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/smt/recfun_solver.cpp
View file

@ -40,7 +40,6 @@ namespace recfun {
} }
void solver::reset() { void solver::reset() {
m_propagation_queue.reset();
m_stats.reset(); m_stats.reset();
m_disabled_guards.reset(); m_disabled_guards.reset();
m_enabled_guards.reset(); m_enabled_guards.reset();
@ -229,7 +228,7 @@ namespace recfun {
} }
void solver::push_prop(propagation_item* p) { void solver::push_prop(propagation_item* p) {
m_propagation_queue.push_back(p); m_propagation_queue.push_back(p);
ctx.push(push_back_vector<scoped_ptr_vector<propagation_item>>(m_propagation_queue)); ctx.push(push_back_vector<scoped_ptr_vector<propagation_item>>(m_propagation_queue));
} }
@ -273,7 +272,8 @@ namespace recfun {
if (!n) if (!n)
n = mk_enode(e, false); n = mk_enode(e, false);
SASSERT(!n->is_attached_to(get_id())); SASSERT(!n->is_attached_to(get_id()));
mk_var(n); euf::theory_var w = mk_var(n);
ctx.attach_th_var(n, this, w);
if (u().is_defined(e) && u().has_defs()) if (u().is_defined(e) && u().has_defs())
push_case_expand(e); push_case_expand(e);
return true; return true;
@ -292,6 +292,8 @@ namespace recfun {
s().assign_scoped(assumption); s().assign_scoped(assumption);
} }
} }
for (expr* g : m_enabled_guards)
push_guard(g);
} }
bool solver::should_research(sat::literal_vector const& core) { bool solver::should_research(sat::literal_vector const& core) {
@ -322,14 +324,11 @@ namespace recfun {
if (to_delete) { if (to_delete) {
m_disabled_guards.erase(to_delete); m_disabled_guards.erase(to_delete);
m_enabled_guards.push_back(to_delete); m_enabled_guards.push_back(to_delete);
push_guard(to_delete);
IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n"); IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n");
} }
else { else {
IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n"); IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n");
} }
for (expr* g : m_enabled_guards)
push_guard(g);
} }
return found; return found;
} }