add logging

Z3Prover · Apr 30, 2024 · 2ad9f22 · 2ad9f22
1 parent bebcd94
commit 2ad9f22
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp
@@ -288,14 +288,16 @@ 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);
 }
 
 
 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;  
 }