From 7aeabe39a359e8d402dfc45f635e9403102e49e2 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Wed, 11 Jan 2023 10:32:38 +0100 Subject: [PATCH] Removed remaining debug output --- src/math/polysat/op_constraint.cpp | 2 -- src/math/polysat/variable_elimination.cpp | 2 -- 2 files changed, 4 deletions(-) diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index abeb2f87a..a438b2be7 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -641,8 +641,6 @@ namespace polysat { // p assigned => r = pseudo_inverse(eval(p)) if (pv.is_val() && !rv.is_val()) { - verbose_stream() << "Inverse ---+++ \n"; - verbose_stream() << "Inverse of " << s.eq(p(), pv) << " = " << s.eq(r(), pv.val().pseudo_inverse(m.power_of_2())) << "\n"; return s.mk_clause(~invc, ~s.eq(p(), pv), s.eq(r(), pv.val().pseudo_inverse(m.power_of_2())), true); } diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp index ec200b8ea..4554b7a8b 100644 --- a/src/math/polysat/variable_elimination.cpp +++ b/src/math/polysat/variable_elimination.cpp @@ -576,7 +576,6 @@ namespace polysat { return s.var(m_inverse[v]); pvar inv = s.add_var(p.power_of_2()); - verbose_stream() << "Inverse v" << inv << " of " << p << " introduced\n"; pdd inv_pdd = s.var(inv); m_inverse.setx(v, inv, -1); s.add_clause(s.eq(inv_pdd * p, p.manager().one()), false); @@ -698,7 +697,6 @@ namespace polysat { pdd a_pi = s.pseudo_inv(a); //precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?) precondition.insert_eval(~s.parity_at_most(a, a_parity)); - verbose_stream() << "parity at most: " << ~s.parity_at_most(a, a_parity) << "\n"; #endif pdd shift = a;