mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

clause_iterator

Browse source
This commit is contained in:
Jakob Rath 2022-12-16 15:21:32 +01:00
parent 342774eff8
commit bf92fa4882
3 changed files with 93 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

62
src/math/polysat/constraint_manager.h
View file

@ -126,9 +126,65 @@ namespace polysat {
constraint* const* begin() const { return m_constraints.data(); }
constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }
using clause_iterator = decltype(m_clauses)::const_iterator;
clause_iterator clauses_begin() const { return m_clauses.begin(); }
clause_iterator clauses_end() const { return m_clauses.end(); }
class clause_iterator {
friend class constraint_manager;
using storage_t = decltype(constraint_manager::m_clauses);
using outer_iterator = storage_t::const_iterator;
outer_iterator outer_it;
outer_iterator outer_end;
using inner_iterator = storage_t::data_t::const_iterator;
inner_iterator inner_it;
inner_iterator inner_end;
clause_iterator(storage_t const& cls, bool begin) {
if (begin) {
outer_it = cls.begin();
outer_end = cls.end();
}
else {
outer_it = cls.end();
outer_end = cls.end();
}
begin_inner();
}
void begin_inner() {
if (outer_it == outer_end) {
inner_it = nullptr;
inner_end = nullptr;
}
else {
inner_it = outer_it->begin();
inner_end = outer_it->end();
}
}
public:
clause const& operator*() const {
return *inner_it->get();
}
clause_iterator& operator++() {
++inner_it;
while (inner_it == inner_end && outer_it != outer_end) {
++outer_it;
begin_inner();
}
return *this;
}
bool operator==(clause_iterator const& other) const {
return outer_it == other.outer_it && inner_it == other.inner_it;
}
bool operator!=(clause_iterator const& other) const {
return !operator==(other);
}
};
clause_iterator clauses_begin() const { return clause_iterator(m_clauses, true); }
clause_iterator clauses_end() const { return clause_iterator(m_clauses, false); }
class clauses_t {
constraint_manager const* m_cm;

75
src/math/polysat/solver.cpp
View file

@ -587,15 +587,13 @@ namespace polysat {
// Simple hack to try deciding the boolean skeleton first
if (!can_bdecide()) {
// enqueue all not-yet-true clauses
for (auto const& cls : m_constraints.clauses()) {
for (auto const& cl : cls) {
bool is_true = any_of(*cl, [&](sat::literal lit) { return m_bvars.is_true(lit); });
if (is_true)
continue;
size_t undefs = count_if(*cl, [&](sat::literal lit) { return !m_bvars.is_assigned(lit); });
if (undefs >= 2)
m_lemmas.push_back(cl.get());
}
for (clause const& cl : m_constraints.clauses()) {
bool is_true = any_of(cl, [&](sat::literal lit) { return m_bvars.is_true(lit); });
if (is_true)
continue;
size_t undefs = count_if(cl, [&](sat::literal lit) { return !m_bvars.is_assigned(lit); });
if (undefs >= 2)
m_lemmas.push_back(&cl);
}
}
#endif
@ -606,7 +604,7 @@ namespace polysat {
}
void solver::bdecide() {
clause& lemma = *m_lemmas[m_lemmas_qhead++];
clause const& lemma = *m_lemmas[m_lemmas_qhead++];
on_scope_exit update_trail = [this]() {
// must be done after push_level, but also if we return early.
m_trail.push_back(trail_instr_t::lemma_qhead_i);
@ -1305,12 +1303,10 @@ namespace polysat {
for (auto c : m_constraints)
out << "\t" << c->bvar2string() << ": " << *c << "\n";
out << "Clauses:\n";
for (auto const& cls : m_constraints.clauses()) {
for (auto const& cl : cls) {
out << "\t" << *cl << "\n";
for (auto lit : *cl)
out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n";
}
for (clause const& cl : m_constraints.clauses()) {
out << "\t" << cl << "\n";
for (sat::literal lit : cl)
out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n";
}
return out;
}
@ -1426,23 +1422,20 @@ namespace polysat {
// Check for missed boolean propagations:
// - no clause should have exactly one unassigned literal, unless it is already true.
// - no clause should be false
for (auto const& cls : m_constraints.clauses()) {
for (auto const& clref : cls) {
clause const& cl = *clref;
bool const is_true = any_of(cl, [&](auto lit) { return m_bvars.is_true(lit); });
if (is_true)
continue;
size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); });
if (undefs == 1) {
LOG("Missed boolean propagation of clause: " << cl);
for (sat::literal lit : cl) {
LOG(" " << lit_pp(*this, lit));
}
for (clause const& cl : m_constraints.clauses()) {
bool const is_true = any_of(cl, [&](auto lit) { return m_bvars.is_true(lit); });
if (is_true)
continue;
size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); });
if (undefs == 1) {
LOG("Missed boolean propagation of clause: " << cl);
for (sat::literal lit : cl) {
LOG(" " << lit_pp(*this, lit));
}
SASSERT(undefs != 1);
bool const is_false = all_of(cl, [&](auto lit) { return m_bvars.is_false(lit); });
SASSERT(!is_false);
}
SASSERT(undefs != 1);
bool const is_false = all_of(cl, [&](auto lit) { return m_bvars.is_false(lit); });
SASSERT(!is_false);
}
return true;
}
@ -1483,19 +1476,17 @@ namespace polysat {
all_ok = all_ok && ok;
}
}
for (auto clauses : m_constraints.clauses()) {
for (auto cl : clauses) {
bool clause_ok = false;
for (sat::literal lit : *cl) {
bool ok = lit2cnstr(lit).is_currently_true(*this);
if (ok) {
clause_ok = true;
break;
}
for (clause const& cl : m_constraints.clauses()) {
bool clause_ok = false;
for (sat::literal lit : cl) {
bool ok = lit2cnstr(lit).is_currently_true(*this);
if (ok) {
clause_ok = true;
break;
}
LOG((clause_ok ? "PASS" : "FAIL") << ": " << show_deref(cl) << (cl->is_redundant() ? " (redundant)" : ""));
all_ok = all_ok && clause_ok;
}
LOG((clause_ok ? "PASS" : "FAIL") << ": " << cl << (cl.is_redundant() ? " (redundant)" : ""));
all_ok = all_ok && clause_ok;
}
if (all_ok) LOG("All good!");
return all_ok;

2
src/math/polysat/solver.h
View file

@ -184,7 +184,7 @@ namespace polysat {
constraints m_pwatch_trail;
#endif
ptr_vector<clause> m_lemmas; ///< the non-asserting lemmas
ptr_vector<clause const> m_lemmas; ///< the non-asserting lemmas
unsigned m_lemmas_qhead = 0;
unsigned_vector m_base_levels; // External clients can push/pop scope.