mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

restoring clause sizes after deletion

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-12 01:01:49 -08:00
parent 3c96b51e97
commit e623f1e9c9
2 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/ba_solver.cpp
View file

@ -1065,7 +1065,7 @@ namespace sat {
uint64_t ba_solver::get_coeff(literal lit) const { uint64_t ba_solver::get_coeff(literal lit) const {
int64_t c1 = get_coeff(lit.var()); int64_t c1 = get_coeff(lit.var());
SASSERT(c1 < 0 == lit.sign()); SASSERT((c1 < 0) == lit.sign());
int64_t c = std::abs(c1); int64_t c = std::abs(c1);
m_overflow |= (c != c1); m_overflow |= (c != c1);
return static_cast<uint64_t>(c); return static_cast<uint64_t>(c);

10
src/sat/sat_simplifier.cpp
View file

@ -351,7 +351,8 @@ namespace sat {
break; break;
case 2: case 2:
s.mk_bin_clause(c[0], c[1], c.is_learned()); s.mk_bin_clause(c[0], c[1], c.is_learned());
s.del_clause(c, false); c.restore(sz0);
s.del_clause(c, true);
break; break;
default: default:
*it2 = *it; *it2 = *it;
@ -613,13 +614,9 @@ namespace sat {
} }
} }
if (j < sz && !r) { if (j < sz && !r) {
if (s.m_config.m_drat) {
m_dummy.set(c.size(), c.begin(), c.is_learned());
}
c.shrink(j); c.shrink(j);
if (s.m_config.m_drat) { if (s.m_config.m_drat) {
s.m_drat.add(c, true); s.m_drat.add(c, true);
s.m_drat.del(*m_dummy.get());
} }
} }
return r; return r;
@ -692,6 +689,7 @@ namespace sat {
clause_use_list & occurs = m_use_list.get(l); clause_use_list & occurs = m_use_list.get(l);
occurs.erase_not_removed(c); occurs.erase_not_removed(c);
m_sub_counter -= occurs.size()/2; m_sub_counter -= occurs.size()/2;
unsigned sz0 = c.size();
if (cleanup_clause(c, true /* clause is in the use lists */)) { if (cleanup_clause(c, true /* clause is in the use lists */)) {
// clause was satisfied // clause was satisfied
TRACE("elim_lit", tout << "clause was satisfied\n";); TRACE("elim_lit", tout << "clause was satisfied\n";);
@ -707,12 +705,12 @@ namespace sat {
TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";); TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
propagate_unit(c[0]); propagate_unit(c[0]);
// propagate_unit will delete c. // propagate_unit will delete c.
// remove_clause(c);
break; break;
case 2: case 2:
TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";); TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
s.mk_bin_clause(c[0], c[1], c.is_learned()); s.mk_bin_clause(c[0], c[1], c.is_learned());
m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned())); m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
c.restore(sz0);
remove_clause(c); remove_clause(c);
break; break;
default: default: