From fd1974845b01fbc4c66fd584e062d3888b23dec9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Oct 2019 21:16:41 -0700 Subject: [PATCH] fix assert-and-track semantics for smt2 logging Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 28 +++++++++++++++++----------- src/api/api_solver.h | 2 ++ src/ast/normal_forms/nnf.cpp | 15 ++++++++------- src/smt/smt_context.cpp | 2 +- 4 files changed, 28 insertions(+), 19 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 76dadae6964..df77c5ed7d4 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -21,6 +21,7 @@ Revision History: #include "util/cancel_eh.h" #include "util/file_path.h" #include "util/scoped_timer.h" +#include "util/file_path.h" #include "ast/ast_pp.h" #include "api/z3.h" #include "api/api_log_macros.h" @@ -30,11 +31,10 @@ Revision History: #include "api/api_model.h" #include "api/api_stats.h" #include "api/api_ast_vector.h" -#include "solver/tactic2solver.h" -#include "util/file_path.h" #include "smt/smt_solver.h" #include "smt/smt_implied_equalities.h" #include "solver/smt_logics.h" +#include "solver/tactic2solver.h" #include "cmd_context/cmd_context.h" #include "parsers/smt2/smt2parser.h" #include "sat/dimacs.h" @@ -55,28 +55,34 @@ extern "C" { m_pp_util.collect(t); m_pp_util.display_decls(m_out); m_pp_util.display_assert_and_track(m_out, e, t, true); + m_tracked.push_back(t); } void solver2smt2_pp::push() { m_out << "(push)\n"; m_pp_util.push(); - } - - void solver2smt2_pp::reset() { - m_out << "(reset)\n"; - m_pp_util.reset(); + m_tracked_lim.push_back(m_tracked.size()); } void solver2smt2_pp::pop(unsigned n) { m_out << "(pop " << n << ")\n"; m_pp_util.pop(n); + m_tracked.shrink(m_tracked_lim[m_tracked_lim.size() - n]); + m_tracked_lim.shrink(m_tracked_lim.size() - n); + } + + void solver2smt2_pp::reset() { + m_out << "(reset)\n"; + m_pp_util.reset(); } void solver2smt2_pp::check(unsigned n, expr* const* asms) { - m_out << "(check-sat"; + m_out << "(check-sat"; for (unsigned i = 0; i < n; ++i) { - m_out << "\n"; - m_pp_util.display_expr(m_out, asms[i]); + m_pp_util.display_expr(m_out << "\n", asms[i]); + } + for (expr* e : m_tracked) { + m_pp_util.display_expr(m_out << "\n", e); } m_out << ")\n"; m_out.flush(); @@ -98,7 +104,7 @@ extern "C" { } - solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file) { + solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file), m_tracked(m) { if (!m_out) { throw default_exception("could not open " + std::string(file) + " for output"); } diff --git a/src/api/api_solver.h b/src/api/api_solver.h index 787a150f0ba..a49cb67064d 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -24,6 +24,8 @@ Revision History: struct solver2smt2_pp { ast_pp_util m_pp_util; std::ofstream m_out; + expr_ref_vector m_tracked; + unsigned_vector m_tracked_lim; solver2smt2_pp(ast_manager& m, char const* file); void assert_expr(expr* e); void assert_expr(expr* e, expr* t); diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index d8db6df8199..5eaf4e63e18 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -70,6 +70,8 @@ class skolemizer { bool m_sk_hack_enabled; cache m_cache; cache m_cache_pr; + bool m_proofs_enabled; + void process(quantifier * q, expr_ref & r, proof_ref & p) { if (q->get_kind() == lambda_k) { @@ -142,7 +144,7 @@ class skolemizer { } r = s(body, substitution.size(), substitution.c_ptr()); p = nullptr; - if (m.proofs_enabled()) { + if (m_proofs_enabled) { if (q->get_kind() == forall_k) p = m.mk_skolemization(m.mk_not(q), m.mk_not(r)); else @@ -156,7 +158,8 @@ class skolemizer { m_sk_hack("sk_hack"), m_sk_hack_enabled(false), m_cache(m), - m_cache_pr(m) { + m_cache_pr(m), + m_proofs_enabled(m.proofs_enabled()) { } void set_sk_hack(bool f) { @@ -167,13 +170,13 @@ class skolemizer { r = m_cache.find(q); if (r.get() != nullptr) { p = nullptr; - if (m.proofs_enabled()) + if (m_proofs_enabled) p = static_cast(m_cache_pr.find(q)); } else { process(q, r, p); m_cache.insert(q, r); - if (m.proofs_enabled()) + if (m_proofs_enabled) m_cache_pr.insert(q, p); } } @@ -273,15 +276,13 @@ struct nnf::imp { updt_params(p); for (unsigned i = 0; i < 4; i++) { m_cache[i] = alloc(act_cache, m); - if (m.proofs_enabled()) + if (proofs_enabled()) m_cache_pr[i] = alloc(act_cache, m); } m_name_nested_formulas = mk_nested_formula_namer(m, n); m_name_quant = mk_quantifier_label_namer(m, n); } - // ast_manager & m() const { return m; } - bool proofs_enabled() const { return m.proofs_enabled(); } ~imp() { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f04ec64ba8f..da63437f3f6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3240,7 +3240,7 @@ namespace smt { else assign(l, b_justification::mk_axiom()); m_assumptions.push_back(l); - get_bdata(l.var()).m_assumption = true; + get_bdata(l.var()).m_assumption = true; } } m_search_lvl = m_scope_lvl;