mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

add logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-04-30 16:57:59 -07:00
parent bebcd94703
commit 2ad9f220f2
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/simplifiers/bound_simplifier.cpp
View file

@ -288,7 +288,8 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) { void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) {
scoped_mpq c(nm); scoped_mpq c(nm);
nm.set(c, n.to_mpq()); nm.set(c, n.to_mpq());
TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " < " : " <= ") << n << "\n");
bp.assert_upper(to_var(x), c, strict); bp.assert_upper(to_var(x), c, strict);
} }
@ -296,6 +297,7 @@ void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) {
void bound_simplifier::assert_lower(expr* x, rational const& n, bool strict) { void bound_simplifier::assert_lower(expr* x, rational const& n, bool strict) {
scoped_mpq c(nm); scoped_mpq c(nm);
nm.set(c, n.to_mpq()); nm.set(c, n.to_mpq());
TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " > " : " >= ") << n << "\n");
bp.assert_lower(to_var(x), c, strict); bp.assert_lower(to_var(x), c, strict);
} }
@ -306,6 +308,7 @@ bool bound_simplifier::has_lower(expr* x, rational& n, bool& strict) {
return false; return false;
strict = m_interval.lower_is_open(i); strict = m_interval.lower_is_open(i);
n = m_interval.lower(i); n = m_interval.lower(i);
TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " > " : " >= ") << n << "\n");
return true; return true;
} }
@ -316,6 +319,7 @@ bool bound_simplifier::has_upper(expr* x, rational& n, bool& strict) {
return false; return false;
strict = m_interval.upper_is_open(i); strict = m_interval.upper_is_open(i);
n = m_interval.upper(i); n = m_interval.upper(i);
TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " < " : " <= ") << n << "\n");
return true; return true;
} }