mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
streamline logging in arithmetic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
facc3215da
commit
441dbbb94b
|
@ -417,8 +417,8 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
void theory_arith<Ext>::atom::display(theory_arith<Ext> const& th, std::ostream& out) const {
|
||||
literal l(get_bool_var(), !m_is_true);
|
||||
out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
|
||||
out << l << ":";
|
||||
// out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
|
||||
// out << l << ":";
|
||||
th.get_context().display_detailed_literal(out, l);
|
||||
}
|
||||
|
||||
|
|
|
@ -1069,7 +1069,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
void theory_arith<Ext>::flush_bound_axioms() {
|
||||
CTRACE("arith", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
|
||||
CTRACE("arith_verbose", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
|
||||
|
||||
while (!m_new_atoms.empty()) {
|
||||
ptr_vector<atom> atoms;
|
||||
|
@ -1084,7 +1084,7 @@ namespace smt {
|
|||
--i;
|
||||
}
|
||||
}
|
||||
CTRACE("arith", !atoms.empty(),
|
||||
CTRACE("arith", atoms.size() > 1,
|
||||
for (unsigned i = 0; i < atoms.size(); ++i) {
|
||||
atoms[i]->display(*this, tout); tout << "\n";
|
||||
});
|
||||
|
@ -1292,7 +1292,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
void theory_arith<Ext>::assign_eh(bool_var v, bool is_true) {
|
||||
TRACE("arith", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
|
||||
TRACE("arith_verbose", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
|
||||
atom * a = get_bv2a(v);
|
||||
if (!a) return;
|
||||
SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
|
||||
|
@ -3043,12 +3043,14 @@ namespace smt {
|
|||
m_stats.m_conflicts++;
|
||||
m_num_conflicts++;
|
||||
TRACE("arith_conflict",
|
||||
tout << "scope: " << ctx.get_scope_level() << "\n";
|
||||
for (unsigned i = 0; i < num_literals; i++) {
|
||||
ctx.display_detailed_literal(tout, lits[i]);
|
||||
tout << " ";
|
||||
if (coeffs_enabled()) {
|
||||
tout << "bound: " << bounds.lit_coeffs()[i] << "\n";
|
||||
}
|
||||
tout << "\n";
|
||||
}
|
||||
for (unsigned i = 0; i < num_eqs; i++) {
|
||||
tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " ";
|
||||
|
|
Loading…
Reference in a new issue