mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

disable some debug output

Browse source
This commit is contained in:
Jakob Rath 2023-03-29 15:40:17 +02:00
parent 64e452e086
commit 810a68ace9
1 changed files with 12 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/math/polysat/viable.cpp
View file

@ -608,12 +608,12 @@ namespace {
do {
rational coeff_val = mod(e->coeff * val, mod_value);
if (e->interval.currently_contains(coeff_val)) {
IF_LOGGING(
verbose_stream() << "refine-equal-lin for v" << v << " in src: ";
for (const auto& src : e->src)
verbose_stream() << lit_pp(s, src) << "\n";
);
LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << " " << num_pp(s, v, e->coeff, true) << " * " << e->interval);
// IF_LOGGING(
// verbose_stream() << "refine-equal-lin for v" << v << " in src: ";
// for (const auto& src : e->src)
// verbose_stream() << lit_pp(s, src) << "\n";
// );
// LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << " " << num_pp(s, v, e->coeff, true) << " * " << e->interval);
if (mod(e->interval.hi_val() + 1, mod_value) == e->interval.lo_val()) {
// We have an equation: a * v == b
@ -735,11 +735,12 @@ namespace {
m_diseq_lin[v] = m_diseq_lin[v]->next();
do {
IF_LOGGING(
verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
for (const auto& src : e->src)
verbose_stream() << lit_pp(s, src) << "\n";
);
// IF_LOGGING(
// verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
// for (const auto& src : e->src)
// verbose_stream() << lit_pp(s, src) << "\n";
// );
// We compute an interval if the concrete value 'val' violates the constraint:
// p*val + q > r*val + s if e->src.is_positive()
// p*val + q >= r*val + s if e->src.is_negative()