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

fix bug in sat-solver where frozen clauses get re-attached

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-05 12:19:03 -07:00
parent eceb92f5ef
commit 1918395f0e
2 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/sat_solver.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/ --*/
#include <cmath> #include <cmath>
#include "sat/sat_solver.h" #include "sat/sat_solver.h"
#include "sat/sat_integrity_checker.h" #include "sat/sat_integrity_checker.h"
@ -298,6 +299,9 @@ namespace sat {
if (!c.is_learned()) { if (!c.is_learned()) {
m_stats.m_non_learned_generation++; m_stats.m_non_learned_generation++;
} }
if (c.frozen()) {
--m_num_frozen;
}
if (m_config.m_drat && !m_drat.is_cleaned(c)) { if (m_config.m_drat && !m_drat.is_cleaned(c)) {
m_drat.del(c); m_drat.del(c);
} }
@ -481,9 +485,10 @@ namespace sat {
} }
unsigned some_idx = c.size() >> 1; unsigned some_idx = c.size() >> 1;
literal block_lit = c[some_idx]; literal block_lit = c[some_idx];
DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off);); VERIFY(!c.frozen());
DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off);); DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
VERIFY(c[0] != c[1]); DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
SASSERT(c[0] != c[1]);
m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off)); m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off)); m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
return reinit; return reinit;
@ -2139,7 +2144,6 @@ namespace sat {
else { else {
c.inc_inact_rounds(); c.inc_inact_rounds();
if (c.inact_rounds() > m_config.m_gc_k) { if (c.inact_rounds() > m_config.m_gc_k) {
m_num_frozen--;
del_clause(c); del_clause(c);
m_stats.m_gc_clause++; m_stats.m_gc_clause++;
deleted++; deleted++;

4
src/sat/sat_solver.h
View file

@ -682,10 +682,10 @@ namespace sat {
bool m_deleted; bool m_deleted;
public: public:
scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) { scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
s.detach_clause(c); if (!c.frozen()) s.detach_clause(c);
} }
~scoped_detach() { ~scoped_detach() {
if (!m_deleted) s.attach_clause(c); if (!m_deleted && !c.frozen()) s.attach_clause(c);
} }
void del_clause() { void del_clause() {