mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

print clauses

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 17:09:44 +02:00
parent c082ea4357
commit 18710a86d7
4 changed files with 23 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/constraint.cpp
View file

@ -116,6 +116,7 @@ namespace polysat {
}
else {
m_constraint_table.insert(c1);
store(c1);
return c1;
}
}

13
src/math/polysat/constraint.h
View file

@ -97,6 +97,19 @@ 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 clauses_t {
constraint_manager const* m_cm;
public:
clauses_t(constraint_manager const& cm): m_cm(&cm) {}
auto begin() const { return m_cm->clauses_begin(); }
auto end() const { return m_cm->clauses_end(); }
};
clauses_t clauses() const { return {*this}; }
};

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

@ -746,7 +746,6 @@ namespace polysat {
}
SASSERT(lemma->size() > 0);
clause* cl = m_constraints.store(std::move(lemma));
m_redundant_clauses.push_back(cl);
if (cl->size() == 1) {
signed_constraint c = m_constraints.lookup((*cl)[0]);
c->set_unit_clause(cl);
@ -801,13 +800,15 @@ namespace polysat {
out << "Boolean assignment:\n\t" << m_bvars << "\n";
out << "Constraints:\n";
for (auto c : m_constraints)
out << "\t" << c << "\n";
out << "Redundant clauses:\n";
for (auto* cl : m_redundant_clauses) {
out << "\t" << *cl << "\n";
for (auto lit : *cl) {
auto c = m_constraints.lookup(lit);
out << "\t\t" << lit << ": " << c << "\n";
out << "\t" << *c << "\n";
out << "Clauses:\n";
for (auto cls : m_constraints.clauses()) {
for (auto cl : cls) {
out << "\t" << *cl << "\n";
for (auto lit : *cl) {
auto c = m_constraints.lookup(lit);
out << "\t\t" << lit << ": " << c << "\n";
}
}
}
return out;

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

@ -86,7 +86,6 @@ namespace polysat {
// Per constraint state
constraint_manager m_constraints;
ptr_vector<clause> m_redundant_clauses;
svector<sat::bool_var> m_disjunctive_lemma;