From 2ad9f220f281b82b601b3e2371fd02bfc9b2dc73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 16:57:59 -0700 Subject: [PATCH] add logging --- src/ast/simplifiers/bound_simplifier.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp index 1a5d4c10107..2d5094c4ff6 100644 --- a/src/ast/simplifiers/bound_simplifier.cpp +++ b/src/ast/simplifiers/bound_simplifier.cpp @@ -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) { 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); } @@ -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) { scoped_mpq c(nm); 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); } @@ -306,6 +308,7 @@ bool bound_simplifier::has_lower(expr* x, rational& n, bool& strict) { return false; strict = m_interval.lower_is_open(i); n = m_interval.lower(i); + TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " > " : " >= ") << n << "\n"); return true; } @@ -316,6 +319,7 @@ bool bound_simplifier::has_upper(expr* x, rational& n, bool& strict) { return false; strict = m_interval.upper_is_open(i); n = m_interval.upper(i); + TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " < " : " <= ") << n << "\n"); return true; }