mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Removed remaining debug output

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-01-11 10:32:38 +01:00
parent 2581754c3e
commit 7aeabe39a3
2 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/op_constraint.cpp
View file

@ -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);
}

2
src/math/polysat/variable_elimination.cpp
View file

@ -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;