From ac4bcb9034839d6f95b6f091f74ab10cc2b510c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Oct 2020 15:09:23 -0700 Subject: [PATCH] update logging for lemmas --- src/smt/smt_context.h | 2 ++ src/smt/smt_context_pp.cpp | 26 +++++++++++++++----------- 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6b1d2e3a7..8f08d1607 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1420,6 +1420,8 @@ namespace smt { unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs, literal consequent = false_literal, symbol const& logic = symbol::null) const; + std::string mk_lemma_name() const; + void display_assignment_as_smtlib2(std::ostream& out, symbol const& logic = symbol::null) const; void display_normalized_enodes(std::ostream & out) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 3196fa417..c82a995a6 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -430,14 +430,12 @@ namespace smt { out << "(check-sat)\n"; } + unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const { - std::stringstream strm; - std::thread::id this_id = std::this_thread::get_id(); - strm << "lemma_" << this_id << "." << (++m_lemma_id) << ".smt2"; - std::ofstream out(strm.str()); - TRACE("lemma", tout << strm.str() << "\n";); + std::string name = mk_lemma_name(); + std::ofstream out(name); + TRACE("lemma", tout << name << "\n";); display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic); - TRACE("non_linear", display_lemma_as_smt_problem(tout, num_antecedents, antecedents, consequent, logic);); out.close(); return m_lemma_id; } @@ -471,14 +469,20 @@ namespace smt { out << "(check-sat)\n"; } - unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, - unsigned num_eq_antecedents, enode_pair const * eq_antecedents, - literal consequent, symbol const& logic) const { + std::string context::mk_lemma_name() const { std::stringstream strm; std::thread::id this_id = std::this_thread::get_id(); strm << "lemma_" << this_id << "." << (++m_lemma_id) << ".smt2"; - std::ofstream out(strm.str()); - TRACE("lemma", tout << strm.str() << "\n"; + return strm.str(); + } + + + unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, + unsigned num_eq_antecedents, enode_pair const * eq_antecedents, + literal consequent, symbol const& logic) const { + std::string name = mk_lemma_name(); + std::ofstream out(name); + TRACE("lemma", tout << name << "\n"; display_lemma_as_smt_problem(tout, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); ); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);