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

Tidy

Browse source
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-10-24 14:08:44 -07:00
parent 80041d7131
commit 8915d0a21f
1 changed files with 43 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

83
src/sat/sat_simplifier.cpp
View file

@ -1044,16 +1044,17 @@ namespace sat {
clause_use_list::iterator it = occs.mk_iterator();
while (!it.at_end()) {
clause & c = it.curr();
it.next();
if (c.is_blocked()) continue;
m_counter -= c.size();
SASSERT(c.contains(l));
s.mark_all_but(c, l);
if (all_tautology(l)) {
block_clause(c, l, new_entry);
s.m_num_blocked_clauses++;
if (!c.is_blocked()) {
m_counter -= c.size();
SASSERT(c.contains(l));
s.mark_all_but(c, l);
if (all_tautology(l)) {
block_clause(c, l, new_entry);
s.m_num_blocked_clauses++;
}
s.unmark_all(c);
}
s.unmark_all(c);
it.next();
}
for (clause* c : m_to_remove)
s.block_clause(*c);
@ -1086,31 +1087,32 @@ namespace sat {
while (!it.at_end()) {
bool tautology = false;
clause & c = it.curr();
it.next();
if (c.is_blocked()) continue;
for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) {
tautology = true;
break;
}
}
if (!tautology) {
if (first) {
for (literal lit : c) {
if (lit != ~l && !s.is_marked(lit)) inter.push_back(lit);
if (!c.is_blocked()) {
for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) {
tautology = true;
break;
}
first = false;
if (inter.empty()) return false;
}
else {
unsigned j = 0;
for (literal lit : inter)
if (c.contains(lit))
inter[j++] = lit;
inter.shrink(j);
if (j == 0) return false;
if (!tautology) {
if (first) {
for (literal lit : c) {
if (lit != ~l && !s.is_marked(lit)) inter.push_back(lit);
}
first = false;
if (inter.empty()) return false;
}
else {
unsigned j = 0;
for (literal lit : inter)
if (c.contains(lit))
inter[j++] = lit;
inter.shrink(j);
if (j == 0) return false;
}
}
}
it.next();
}
return first;
}
@ -1360,17 +1362,18 @@ namespace sat {
clause_use_list::iterator it = neg_occs.mk_iterator();
while (!it.at_end()) {
clause & c = it.curr();
it.next();
if (c.is_blocked()) continue;
m_counter -= c.size();
unsigned sz = c.size();
unsigned i;
for (i = 0; i < sz; i++) {
if (s.is_marked(~c[i]))
break;
if (!c.is_blocked()) {
m_counter -= c.size();
unsigned sz = c.size();
unsigned i;
for (i = 0; i < sz; i++) {
if (s.is_marked(~c[i]))
break;
}
if (i == sz)
return false;
}
if (i == sz)
return false;
it.next();
}
if (s.s.m_ext) {