mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

#5641

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-03 11:12:09 -08:00
parent cf08cdff9c
commit 2944449884
3 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/sat/sat_solver.cpp
View file

@ -288,6 +288,7 @@ namespace sat {
m_free_vars.pop_back();
m_active_vars.push_back(v);
reset_var(v, ext, dvar);
SASSERT(v < m_justification.size());
return v;
}
m_active_vars.push_back(v);
@ -3508,7 +3509,6 @@ namespace sat {
unsigned old_num_vars = m_vars_lim.pop(num_scopes);
if (old_num_vars == m_active_vars.size())
return;
unsigned free_vars_head = m_free_vars.size();
unsigned sz = m_active_vars.size(), j = old_num_vars;
unsigned new_lvl = m_scopes.size() - num_scopes;
@ -3538,9 +3538,7 @@ namespace sat {
}
else {
set_eliminated(v, true);
if (!is_external(v) || true) {
m_free_vars.push_back(v);
}
m_vars_to_free.push_back(v);
}
}
m_active_vars.shrink(j);
@ -3550,8 +3548,7 @@ namespace sat {
IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
}
};
for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) {
bool_var v = m_free_vars[i];
for (bool_var v : m_vars_to_free) {
cleanup_watch(literal(v, false));
cleanup_watch(literal(v, true));
@ -3560,7 +3557,7 @@ namespace sat {
tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n";
tout << "new level: " << new_lvl << "\n";
tout << "vars to reinit: " << m_vars_to_reinit << "\n";
tout << "free vars: " << bool_var_vector(m_free_vars.size() - free_vars_head, m_free_vars.data() + free_vars_head) << "\n";
tout << "free vars: " << bool_var_vector(m_vars_to_free) << "\n";
for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; )
tout << "reinit: " << m_clauses_to_reinit[i] << "\n";
display(tout););
@ -3599,7 +3596,6 @@ namespace sat {
void solver::pop(unsigned num_scopes) {
if (num_scopes == 0)
return;
unsigned free_vars_head = m_free_vars.size();
if (m_ext) {
pop_vars(num_scopes);
m_ext->pop(num_scopes);
@ -3609,13 +3605,16 @@ namespace sat {
scope & s = m_scopes[new_lvl];
m_inconsistent = false; // TBD: use model seems to make this redundant: s.m_inconsistent;
unassign_vars(s.m_trail_lim, new_lvl);
for (unsigned i = m_free_vars.size(); i-- > free_vars_head; )
m_case_split_queue.del_var_eh(m_free_vars[i]);
for (bool_var v : m_vars_to_free)
m_case_split_queue.del_var_eh(v);
m_scope_lvl -= num_scopes;
reinit_clauses(s.m_clauses_to_reinit_lim);
m_scopes.shrink(new_lvl);
if (m_ext)
if (m_ext) {
m_ext->pop_reinit();
m_free_vars.append(m_vars_to_free);
m_vars_to_free.reset();
}
}
void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) {
@ -3692,6 +3691,7 @@ namespace sat {
//
void solver::user_push() {
pop_to_base_level();
m_free_var_freeze.push_back(m_free_vars);
m_free_vars.reset(); // resetting free_vars forces new variables to be assigned above new_v

2
src/sat/sat_solver.h
View file

@ -124,7 +124,7 @@ namespace sat {
clause_vector m_clauses;
clause_vector m_learned;
unsigned m_num_frozen;
unsigned_vector m_active_vars, m_free_vars, m_vars_to_reinit;
unsigned_vector m_active_vars, m_free_vars, m_vars_to_free, m_vars_to_reinit;
vector<watch_list> m_watches;
svector<lbool> m_assignment;
svector<justification> m_justification;

6
src/sat/tactic/goal2sat.cpp
View file

@ -224,6 +224,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
sat::bool_var add_bool_var(expr* t) override {
force_push();
sat::bool_var v = m_map.to_bool_var(t);
if (v == sat::null_bool_var)
v = mk_bool_var(t);
@ -239,10 +240,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_map.push();
m_cache_lim.push_back(m_cache_trail.size());
}
}
}
void push() override {
++m_num_scopes;
++m_num_scopes;
}
void pop(unsigned n) override {
@ -263,7 +265,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
m_cache_trail.shrink(k);
m_cache_lim.shrink(m_cache_lim.size() - n);
m_cache_lim.shrink(m_cache_lim.size() - n);
}
// remove non-external literals from cache.