mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

log_lemma

Browse source
This commit is contained in:
Jakob Rath 2023-02-20 12:32:21 +01:00
parent 1d04d08a0c
commit 61ec3b9e87
1 changed files with 7 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/saturation.cpp
View file

@ -33,15 +33,13 @@ namespace polysat {
saturation::saturation(solver& s) : s(s), m_lemma(s), m_parity_tracker(s) {} saturation::saturation(solver& s) : s(s), m_lemma(s), m_parity_tracker(s) {}
void saturation::log_lemma(pvar v, conflict& core) { void saturation::log_lemma(pvar v, conflict& core) {
verbose_stream() << "Logging lemma:\n"; IF_VERBOSE(1, {
auto const& cl = core.lemmas().back(); auto const& cl = core.lemmas().back();
verbose_stream() << m_rule << " v" << v << " "; verbose_stream() << m_rule << " v" << v << " ";
for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " "; for (auto lit : *cl)
verbose_stream() << " " << *cl << "\n"; verbose_stream() << s.lit2cnstr(lit) << " ";
IF_VERBOSE(1, auto const& cl = core.lemmas().back(); verbose_stream() << " " << *cl << "\n";
verbose_stream() << m_rule << " v" << v << " "; });
for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " ";
verbose_stream() << " " << *cl << "\n");
} }
void saturation::perform(pvar v, conflict& core) { void saturation::perform(pvar v, conflict& core) {