mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

better tracing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-27 16:05:57 -07:00
parent 7086a7c26a
commit 3237bd9243
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lar_solver.cpp
View file

@ -1799,7 +1799,7 @@ mpq lar_solver::adjust_bound_for_int(lpvar j, lconstraint_kind& k, const mpq& bo
} }
constraint_index lar_solver::mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { constraint_index lar_solver::mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) {
TRACE("lar_solver", tout << "j = " << j << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;); TRACE("lar_solver", tout << "j = " << get_variable_name(j) << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;);
constraint_index ci; constraint_index ci;
if (!tv::is_term(j)) { // j is a var if (!tv::is_term(j)) { // j is a var
mpq rs = adjust_bound_for_int(j, kind, right_side); mpq rs = adjust_bound_for_int(j, kind, right_side);

4
src/smt/theory_lra.cpp
View file

@ -3050,7 +3050,7 @@ public:
} }
constraint_bound& b = vec[ti]; constraint_bound& b = vec[ti];
if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) { if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
TRACE("arith", tout << "tighter bound " << vi << "\n";); TRACE("arith", tout << "tighter bound " << lp().get_variable_name(vi) << "\n";);
m_history.push_back(vec[ti]); m_history.push_back(vec[ti]);
ctx().push_trail(history_trail<context, constraint_bound>(vec, ti, m_history)); ctx().push_trail(history_trail<context, constraint_bound>(vec, ti, m_history));
b.first = ci; b.first = ci;
@ -3093,7 +3093,7 @@ public:
if (lp::tv::is_term(vi)) { if (lp::tv::is_term(vi)) {
theory_var v = lp().local_to_external(vi); theory_var v = lp().local_to_external(vi);
rational val; rational val;
TRACE("arith", tout << vi << " " << v << "\n";); TRACE("arith", tout << lp().get_variable_name(vi) << " " << v << "\n";);
if (v != null_theory_var && a.is_numeral(get_owner(v), val) && bound == val) { if (v != null_theory_var && a.is_numeral(get_owner(v), val) && bound == val) {
ci = UINT_MAX; ci = UINT_MAX;
return bound == val; return bound == val;