mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity
z3/src/sat/sat_model_converter.cpp
LeeYoungJoon 0a93ff515d
Centralize and document TRACE tags using X-macros (#7657) 
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros

* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md

* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

* trace: improve trace tag handling system with hierarchical tagging

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
  (class names and descriptions to be refined in a future update)

* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

* trace : add cstring header

* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.

* trace : Add TODO comment for future implementation of tag_class activation

* trace : Disable code related to tag_class until implementation is ready (#7663).
2025-05-28 14:31:25 +01:00

460 lines
16 KiB
C++
Raw Blame History

/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_model_converter.cpp
Abstract:
Low level model converter for SAT solver.
Author:
Leonardo de Moura (leonardo) 2011-05-26.
Revision History:
--*/
#include "sat/sat_model_converter.h"
#include "sat/sat_clause.h"
#include "sat/sat_solver.h"
#include "util/trace.h"
namespace sat {
model_converter& model_converter::operator=(model_converter const& other) {
copy(other);
return *this;
}
bool model_converter::legal_to_flip(bool_var v) const {
if (m_solver && m_solver->is_assumption(v)) {
IF_VERBOSE(0, verbose_stream() << "flipping assumption v" << v << "\n";);
UNREACHABLE();
throw solver_exception("flipping assumption");
}
if (m_solver && m_solver->is_external(v) && m_solver->is_incremental()) {
IF_VERBOSE(0, verbose_stream() << "flipping external v" << v << "\n";);
UNREACHABLE();
throw solver_exception("flipping external");
}
return !m_solver || !m_solver->is_assumption(v);
}
void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const {
SASSERT(!stack.empty());
unsigned sz = stack.size();
for (unsigned i = sz; i-- > 0; ) {
unsigned csz = stack[i].first;
literal lit = stack[i].second;
bool sat = false;
for (unsigned j = 0; !sat && j < csz; ++j) {
sat = value_at(c[j], m) == l_true;
}
if (!sat) {
VERIFY(legal_to_flip(lit.var()));
m[lit.var()] = lit.sign() ? l_false : l_true;
}
}
}
void model_converter::operator()(model & m) const {
bool first = false;
literal_vector clause;
for (unsigned i = m_entries.size(); i-- > m_exposed_lim; ) {
entry const& e = m_entries[i];
bool_var v0 = e.var();
SASSERT(e.get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef);
// if e.get_kind() == BCE, then it might be the case that m[v] != l_undef,
// and the following procedure flips its value.
bool sat = false;
bool var_sign = false;
unsigned index = 0;
clause.reset();
VERIFY(v0 == null_bool_var || legal_to_flip(v0));
for (literal l : e.m_clauses) {
if (l == null_literal) {
// end of clause
VERIFY (sat || e.get_kind() != ATE);
if (!sat && e.get_kind() != ATE && v0 != null_bool_var) {
VERIFY(legal_to_flip(v0));
m[v0] = var_sign ? l_false : l_true;
}
elim_stack* st = e.m_elim_stack[index];
if (st) {
process_stack(m, clause, st->stack());
}
sat = false;
VERIFY(!first || !m_solver || m_solver->check_clauses(m));
++index;
clause.reset();
continue;
}
clause.push_back(l);
if (sat)
continue;
bool sign = l.sign();
bool_var v = l.var();
VERIFY(v < m.size());
if (v == v0)
var_sign = sign;
if (value_at(l, m) == l_true)
sat = true;
else if (!sat && v != v0 && m[v] == l_undef) {
VERIFY(legal_to_flip(v));
// clause can be satisfied by assigning v.
m[v] = sign ? l_false : l_true;
sat = true;
VERIFY(!first || !m_solver || m_solver->check_clauses(m));
}
}
DEBUG_CODE({
// all clauses must be satisfied
bool sat = false;
bool undef = false;
for (literal const& l : e.m_clauses) {
if (l == null_literal) {
CTRACE(sat, !sat,
tout << "exposed: " << m_exposed_lim << "\n";
if (m_solver) m_solver->display(tout);
display(tout);
for (unsigned v = 0; v < m.size(); ++v) tout << v << ": " << m[v] << "\n";
for (literal const& l2 : e.m_clauses) {
if (l2 == null_literal) tout << "\n"; else tout << l2 << " ";
if (&l == &l2) break;
}
);
SASSERT(sat || undef);
sat = false;
undef = false;
continue;
}
if (sat)
continue;
switch (value_at(l, m)) {
case l_undef: undef = true; break;
case l_true: sat = true; break;
default: break;
}
}
});
}
}
/**
\brief Test if after applying the model converter, all eliminated clauses are
satisfied by m.
*/
bool model_converter::check_model(model const & m) const {
bool ok = true;
for (entry const & e : m_entries) {
bool sat = false;
literal_vector::const_iterator it = e.m_clauses.begin();
literal_vector::const_iterator itbegin = it;
literal_vector::const_iterator end = e.m_clauses.end();
for (; it != end; ++it) {
literal l = *it;
if (l == null_literal) {
// end of clause
if (!sat) {
TRACE(sat_model_bug, tout << "failed eliminated: " << mk_lits_pp(static_cast<unsigned>(it - itbegin), itbegin) << "\n";);
(void)itbegin;
ok = false;
}
sat = false;
itbegin = it;
itbegin++;
continue;
}
if (sat)
continue;
if (value_at(l, m) == l_true)
sat = true;
}
}
return ok;
}
model_converter::entry & model_converter::mk(kind k, bool_var v) {
m_entries.push_back(entry(k, v));
entry & e = m_entries.back();
SASSERT(e.var() == v);
SASSERT(e.get_kind() == k);
VERIFY(v == null_bool_var || legal_to_flip(v));
return e;
}
void model_converter::add_ate(clause const& c) {
if (stackv().empty()) return;
insert(mk(ATE, null_bool_var), c);
}
void model_converter::add_ate(literal_vector const& lits) {
if (stackv().empty()) return;
insert(mk(ATE, null_bool_var), lits);
}
void model_converter::add_ate(literal l1, literal l2) {
if (stackv().empty()) return;
insert(mk(ATE, null_bool_var), l1, l2);
}
void model_converter::add_elim_stack(entry & e) {
e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, std::move(m_elim_stack)));
// VERIFY(for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var())););
stackv().reset();
}
void model_converter::set_clause(entry & e, literal l1, literal l2) {
e.m_clause.push_back(l1);
e.m_clause.push_back(l2);
}
void model_converter::set_clause(entry & e, clause const & c) {
e.m_clause.append(c.size(), c.begin());
}
void model_converter::insert(entry & e, clause const & c) {
SASSERT(c.contains(e.var()));
SASSERT(m_entries.begin() <= &e);
SASSERT(&e < m_entries.end());
for (literal l : c) e.m_clauses.push_back(l);
e.m_clauses.push_back(null_literal);
add_elim_stack(e);
TRACE(sat_mc_bug, tout << "adding: " << c << "\n";);
}
void model_converter::insert(entry & e, literal l1, literal l2) {
SASSERT(l1.var() == e.var() || l2.var() == e.var());
SASSERT(m_entries.begin() <= &e);
SASSERT(&e < m_entries.end());
e.m_clauses.push_back(l1);
e.m_clauses.push_back(l2);
e.m_clauses.push_back(null_literal);
add_elim_stack(e);
TRACE(sat_mc_bug, tout << "adding (binary): " << l1 << " " << l2 << "\n";);
}
void model_converter::insert(entry & e, clause_wrapper const & c) {
SASSERT(c.contains(e.var()));
SASSERT(m_entries.begin() <= &e);
SASSERT(&e < m_entries.end());
unsigned sz = c.size();
for (unsigned i = 0; i < sz; ++i)
e.m_clauses.push_back(c[i]);
e.m_clauses.push_back(null_literal);
add_elim_stack(e);
// TRACE(sat_mc_bug, tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
}
void model_converter::insert(entry & e, literal_vector const& c) {
SASSERT(e.var() == null_bool_var || c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true)));
SASSERT(m_entries.begin() <= &e);
SASSERT(&e < m_entries.end());
for (literal l : c) e.m_clauses.push_back(l);
e.m_clauses.push_back(null_literal);
add_elim_stack(e);
TRACE(sat_mc_bug, tout << "adding: " << c << "\n";);
}
bool model_converter::check_invariant(unsigned num_vars) const {
// After a variable v occurs in an entry n and the entry has kind ELIM_VAR,
// then the variable must not occur in any other entry occurring after it.
vector<entry>::const_iterator it = m_entries.begin();
vector<entry>::const_iterator end = m_entries.end();
for (; it != end; ++it) {
SASSERT(it->var() == null_bool_var || it->var() < num_vars);
if (it->get_kind() == ELIM_VAR) {
svector<entry>::const_iterator it2 = it;
it2++;
for (; it2 != end; ++it2) {
SASSERT(it2->var() != it->var());
if (it2->var() == it->var()) return false;
for (literal l : it2->m_clauses) {
CTRACE(sat_model_converter, l.var() == it->var(), tout << "var: " << it->var() << "\n"; display(tout););
SASSERT(l.var() != it->var());
VERIFY(l == null_literal || l.var() < num_vars);
if (it2->var() == it->var()) return false;
}
}
}
}
return true;
}
void model_converter::display(std::ostream & out) const {
out << "(sat::model-converter\n";
bool first = true;
for (auto & entry : m_entries) {
if (first) first = false; else out << "\n";
display(out, entry);
}
out << ")\n";
}
std::ostream& model_converter::display(std::ostream& out, entry const& entry) const {
out << " (" << entry.get_kind() << " ";
if (entry.var() != null_bool_var) out << entry.var();
bool start = true;
unsigned index = 0;
for (literal l : entry.m_clauses) {
if (start) {
out << "\n (";
start = false;
}
else {
if (l != null_literal)
out << " ";
}
if (l == null_literal) {
out << ")";
start = true;
elim_stack* st = entry.m_elim_stack[index];
if (st) {
elim_stackv const& stack = st->stack();
unsigned sz = stack.size();
for (unsigned i = sz; i-- > 0; ) {
out << "\n " << stack[i].first << " " << stack[i].second;
}
}
++index;
continue;
}
out << l;
}
out << ")";
return out;
}
void model_converter::copy(model_converter const & src) {
m_entries.reset();
m_entries.append(src.m_entries);
m_exposed_lim = src.m_exposed_lim;
}
void model_converter::flush(model_converter & src) {
VERIFY(this != &src);
m_entries.append(src.m_entries);
m_exposed_lim += src.m_exposed_lim;
src.m_entries.reset();
src.m_exposed_lim = 0;
}
void model_converter::collect_vars(bool_var_set & s) const {
for (entry const & e : m_entries) {
s.insert(e.m_var);
}
}
unsigned model_converter::max_var(unsigned min) const {
unsigned result = min;
for (entry const& e : m_entries) {
for (literal l : e.m_clauses) {
if (l != null_literal) {
if (l.var() != null_bool_var && l.var() > result)
result = l.var();
}
}
}
return result;
}
void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) noexcept {
for (unsigned j = 0; j < sz; ++j) {
if (v == clause[j].var()) {
std::swap(clause[0], clause[j]);
return;
}
}
IF_VERBOSE(0, verbose_stream() << "not found: v" << v << " " << clause << "\n";);
UNREACHABLE();
}
void model_converter::expand(literal_vector& update_stack) {
sat::literal_vector clause;
for (unsigned i = m_exposed_lim; i < m_entries.size(); ++i) {
entry const& e = m_entries[i];
unsigned index = 0;
clause.reset();
for (literal l : e.m_clauses) {
if (l == null_literal) {
elim_stack* st = e.m_elim_stack[index];
if (st) {
// clause sizes increase, so we can always swap
// the blocked literal to the front from the prefix.
for (auto const& p : st->stack()) {
unsigned csz = p.first;
literal lit = p.second;
swap(lit.var(), csz, clause);
update_stack.append(csz, clause.data());
update_stack.push_back(null_literal);
}
}
if (e.var() != null_bool_var) {
swap(e.var(), clause.size(), clause);
update_stack.append(clause);
update_stack.push_back(null_literal);
}
clause.reset();
}
else {
clause.push_back(l);
}
}
}
m_exposed_lim = m_entries.size();
}
void model_converter::init_search(solver& s) {
#if 0
unsigned j = 0, k = 0;
literal_vector clause;
for (unsigned i = 0; i < m_entries.size(); ++i) {
entry & e = m_entries[i];
if (!m_mark[e.var()]) {
m_entries[j++] = e;
if (i < m_exposed_lim) k++;
continue;
}
clause.reset();
// For covered clauses we record the original clause. The role of m_clauses is to record ALA
// tautologies and are not part of the clause that is removed.
if (!e.m_clause.empty()) {
clause.append(e.m_clause);
s.mk_clause(clause.size(), clause.c_ptr(), false);
continue;
}
for (literal lit : e.m_clauses) {
if (lit == null_literal) {
s.mk_clause(clause.size(), clause.c_ptr(), false);
clause.reset();
}
else {
clause.push_back(lit);
}
}
}
m_entries.shrink(j);
m_exposed_lim = k;
for (bool& m : m_mark) {
m = false;
}
#endif
}
void model_converter::add_clause(unsigned n, literal const* lits) {
if (m_entries.empty()) {
return;
}
// TBD: we just mark variables instead of literals because entries don't have directly literal information.
for (unsigned i = 0; i < n; ++i) {
m_mark.reserve(lits[i].var() + 1);
m_mark[lits[i].var()] = true;
}
}
};
View git blame Copy permalink