From 7e415c1b6972c32b5385de6a38b08d46c7ea9bb0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Dec 2019 23:08:41 +0300 Subject: [PATCH] update to logging --- src/ast/rewriter/seq_rewriter.cpp | 19 +++++++++---------- src/smt/smt_clause.cpp | 2 +- src/smt/smt_conflict_resolution.cpp | 26 ++++++++++++++++++-------- src/smt/smt_conflict_resolution.h | 2 +- src/smt/smt_context.cpp | 2 +- src/smt/smt_context.h | 4 ++++ src/smt/smt_context_pp.cpp | 10 +++++----- src/smt/smt_literal.cpp | 13 +++++++++++++ src/smt/smt_literal.h | 2 ++ 9 files changed, 54 insertions(+), 26 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 90e3c85f0..0a28f192a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -549,7 +549,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case _OP_STRING_STRIDOF: UNREACHABLE(); } - CTRACE("seq_verbose", st != BR_FAILED, tout << f->get_name() << " " << result << "\n";); + CTRACE("seq_verbose", st != BR_FAILED, tout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";); return st; } @@ -616,32 +616,31 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { m_util.str.get_concat(a, m_es); unsigned len = 0; unsigned j = 0; - for (unsigned i = 0; i < m_es.size(); ++i) { - if (m_util.str.is_string(m_es[i].get(), b)) { + for (expr* e : m_es) { + if (m_util.str.is_string(e, b)) { len += b.length(); } - else if (m_util.str.is_unit(m_es[i].get())) { + else if (m_util.str.is_unit(e)) { len += 1; } - else if (m_util.str.is_empty(m_es[i].get())) { + else if (m_util.str.is_empty(e)) { // skip } else { - m_es[j] = m_es[i].get(); - ++j; + m_es[j++] = e; } } if (j == 0) { - result = m_autil.mk_numeral(rational(len, rational::ui64()), true); + result = m_autil.mk_int(len); return BR_DONE; } if (j != m_es.size() || j != 1) { expr_ref_vector es(m()); for (unsigned i = 0; i < j; ++i) { - es.push_back(m_util.str.mk_length(m_es[i].get())); + es.push_back(m_util.str.mk_length(m_es.get(i))); } if (len != 0) { - es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true)); + es.push_back(m_autil.mk_int(len)); } result = m_autil.mk_add(es.size(), es.c_ptr()); return BR_REWRITE2; diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index 4aee1f98c..f1c62a3cf 100644 --- a/src/smt/smt_clause.cpp +++ b/src/smt/smt_clause.cpp @@ -123,7 +123,7 @@ namespace smt { if (lit.sign()) args[args.size()-1] = m.mk_not(args.back()); } expr_ref disj(m.mk_or(args.size(), args.c_ptr()), m); - return out << mk_bounded_pp(disj, m, 3); + return out << mk_pp(disj, m, 3); } }; diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 2d7826386..b6c14c5d7 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -101,7 +101,7 @@ namespace smt { */ void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) { SASSERT(m_antecedents); - TRACE("conflict_detail", + TRACE("conflict_", ast_manager& m = get_manager(); tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m); switch (js.get_kind()) { @@ -333,7 +333,6 @@ namespace smt { } if (lvl == m_conflict_lvl) { - TRACE("conflict", m_ctx.display_literal(tout << "marking:", antecedent) << "\n";); num_marks++; } else { @@ -343,12 +342,21 @@ namespace smt { } } - void conflict_resolution::process_justification(justification * js, unsigned & num_marks) { + void conflict_resolution::process_justification(literal consequent, justification * js, unsigned & num_marks) { literal_vector & antecedents = m_tmp_literal_vector; antecedents.reset(); justification2literals_core(js, antecedents); for (literal l : antecedents) process_antecedent(l, num_marks); + (void)consequent; + TRACE("conflict_smt2", + for (literal& l : antecedents) { + l.neg(); + SASSERT(m_ctx.get_assignment(l) == l_false); + } + antecedents.push_back(consequent); + m_ctx.display_literals_smt2(tout, antecedents);); + } /** @@ -505,8 +513,7 @@ namespace smt { switch (js.get_kind()) { case b_justification::CLAUSE: { clause * cls = js.get_clause(); - TRACE("conflict", m_ctx.display_clause_detail(tout, cls);); - TRACE("conflict", tout << literal_vector(cls->get_num_literals(), cls->begin()) << "\n";); + TRACE("conflict_smt2", m_ctx.display_clause_smt2(tout, *cls);); if (cls->is_lemma()) cls->inc_clause_activity(); unsigned num_lits = cls->get_num_literals(); @@ -530,17 +537,18 @@ namespace smt { } justification * js = cls->get_justification(); if (js) - process_justification(js, num_marks); + process_justification(consequent, js, num_marks); break; } case b_justification::BIN_CLAUSE: + TRACE("conflict_smt2", m_ctx.display_literals_smt2(tout, consequent, ~js.get_literal()) << "\n";); SASSERT(consequent.var() != js.get_literal().var()); process_antecedent(js.get_literal(), num_marks); break; case b_justification::AXIOM: break; case b_justification::JUSTIFICATION: - process_justification(js.get_justification(), num_marks); + process_justification(consequent, js.get_justification(), num_marks); break; default: UNREACHABLE(); @@ -572,11 +580,13 @@ namespace smt { } while (num_marks > 0); - TRACE("conflict", tout << "FUIP: "; m_ctx.display_literal(tout, consequent); tout << "\n";); + TRACE("conflict", tout << "FUIP: "; m_ctx.display_literal(tout, consequent)<< "\n";); m_lemma[0] = ~consequent; m_lemma_atoms.set(0, m_ctx.bool_var2expr(consequent.var())); + TRACE("conflict_smt2", m_ctx.display_literals_smt2(tout << "lemma:", m_lemma) << "\n";); + // TODO: // // equality optimization should go here. diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h index 90390ae7e..e88a8c6ae 100644 --- a/src/smt/smt_conflict_resolution.h +++ b/src/smt/smt_conflict_resolution.h @@ -177,7 +177,7 @@ namespace smt { unsigned get_max_lvl(literal consequent, b_justification js); unsigned skip_literals_above_conflict_level(); void process_antecedent(literal antecedent, unsigned & num_marks); - void process_justification(justification * js, unsigned & num_marks); + void process_justification(literal consequent, justification * js, unsigned & num_marks); bool_var_vector m_unmark; bool_var_vector m_lemma_min_stack; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 27465aaf5..27a6011b5 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3935,7 +3935,7 @@ namespace smt { for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; tout << l << " "; - display_literal(tout, l); + display_literal_smt2(tout, l); tout << ", ilvl: " << get_intern_level(l.var()) << "\n" << mk_pp(bool_var2expr(l.var()), m) << "\n"; }); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 451c367f5..d3735f199 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1318,8 +1318,12 @@ namespace smt { std::ostream& display_literal_smt2(std::ostream& out, literal lit) const; + std::ostream& display_literals_smt2(std::ostream& out, literal l1, literal l2) const { literal ls[2] = { l1, l2 }; return display_literals_smt2(out, 2, ls); } + std::ostream& display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const; + std::ostream& display_literals_smt2(std::ostream& out, literal_vector const& ls) const { return display_literals_smt2(out, ls.size(), ls.c_ptr()); } + std::ostream& display_literal_verbose(std::ostream & out, literal lit) const; std::ostream& display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index a698d94a0..02ad786dd 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -103,9 +103,9 @@ namespace smt { std::ostream& context::display_literal_smt2(std::ostream& out, literal l) const { if (l.sign()) - out << " (not " << mk_pp(bool_var2expr(l.var()), m) << ") "; + out << "(not " << mk_pp(bool_var2expr(l.var()), m) << ") "; else - out << " " << mk_pp(bool_var2expr(l.var()), m) << " "; + out << mk_pp(bool_var2expr(l.var()), m) << " "; return out; } @@ -173,8 +173,7 @@ namespace smt { } std::ostream& context::display_clause_smt2(std::ostream & out, clause const& cls) const { - cls.display_smt2(out, m, m_bool_var2expr.c_ptr()); - return out; + return display_literals_smt2(out, cls.get_num_literals(), cls.begin()); } std::ostream& context::display_clauses(std::ostream & out, ptr_vector const & v) const { @@ -604,7 +603,8 @@ namespace smt { case b_justification::JUSTIFICATION: { literal_vector lits; const_cast(*m_conflict_resolution).justification2literals(j.get_justification(), lits); - out << "justification " << j.get_justification()->get_from_theory() << ": " << lits; + out << "justification " << j.get_justification()->get_from_theory() << ": "; + display_literals_smt2(out, lits); break; } default: diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp index 67afbe962..aade0f51b 100644 --- a/src/smt/smt_literal.cpp +++ b/src/smt/smt_literal.cpp @@ -35,6 +35,19 @@ namespace smt { out << mk_bounded_pp(bool_var2expr_map[var()], m, 3); } + void literal::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { + if (*this == true_literal) + out << "true"; + else if (*this == false_literal) + out << "false"; + else if (*this == null_literal) + out << "null"; + else if (sign()) + out << "(not " << mk_pp(bool_var2expr_map[var()], m, 3) << ")"; + else + out << mk_pp(bool_var2expr_map[var()], m, 3); + } + void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const { if (*this == true_literal) out << "true"; diff --git a/src/smt/smt_literal.h b/src/smt/smt_literal.h index 598335cff..e18b5dc0a 100644 --- a/src/smt/smt_literal.h +++ b/src/smt/smt_literal.h @@ -63,6 +63,8 @@ namespace smt { void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; + void display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; + void display_compact(std::ostream & out, expr * const * bool_var2expr_map) const; unsigned hash() const { return m_val; }