From f6f3ca150726cfc26a50752de5f0963ccf7d2ab5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Oct 2019 11:44:47 -0700 Subject: [PATCH] adding SMT2 log file for solver interaction #867 Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 67 +++++++++++++++++++++++++++++++++++--- src/api/api_solver.h | 15 +++++++++ src/api/python/z3/z3.py | 16 +++++---- src/api/z3_api.h | 15 +++++++++ src/ast/ast_pp_util.cpp | 51 +++++++++++++++++++++++------ src/ast/ast_pp_util.h | 10 +++++- src/ast/ast_smt_pp.cpp | 2 +- src/ast/decl_collector.cpp | 9 +++-- src/ast/decl_collector.h | 2 +- 9 files changed, 159 insertions(+), 28 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 2e0441653..761ab308b 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -44,6 +44,52 @@ Revision History: extern "C" { + void solver2smt2_pp::assert_expr(expr* e) { + m_pp_util.collect(e); + m_pp_util.display_decls(m_out); + m_pp_util.display_assert(m_out, e, true); + } + + void solver2smt2_pp::assert_expr(expr* e, expr* t) { + m_pp_util.collect(e); + m_pp_util.collect(t); + m_pp_util.display_decls(m_out); + m_pp_util.display_assert_and_track(m_out, e, t, true); + } + + void solver2smt2_pp::push() { + m_out << "(push)\n"; + } + + void solver2smt2_pp::pop(unsigned n) { + m_out << "(pop " << n << ")\n"; + } + + void solver2smt2_pp::check(unsigned n, expr* const* asms) { + m_out << "(check-sat"; + for (unsigned i = 0; i < n; ++i) { + m_out << "\n"; + m_pp_util.display_expr(m_out, asms[i]); + } + m_out << ")\n"; + } + + solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file) { + if (!m_out) { + throw default_exception("could not open file for output"); + } + } + + void Z3_solver_ref::assert_expr(expr * e) { + if (m_pp) m_pp->assert_expr(e); + m_solver->assert_expr(e); + } + + void Z3_solver_ref::assert_expr(expr * e, expr* t) { + if (m_pp) m_pp->assert_expr(e, t); + m_solver->assert_expr(e, t); + } + static void init_solver_core(Z3_context c, Z3_solver _s) { Z3_solver_ref * s = to_solver(_s); bool proofs_enabled, models_enabled, unsat_core_enabled; @@ -85,6 +131,13 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + void Z3_API Z3_solver_open_smt2log(Z3_context c, Z3_solver s, Z3_string file) { + Z3_TRY; + LOG_Z3_solver_open_smt2log(c, s, file); + to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), file); + Z3_CATCH; + } + Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic) { Z3_TRY; LOG_Z3_mk_solver_for_logic(c, logic); @@ -154,7 +207,7 @@ extern "C" { if (!initialized) init_solver(c, s); for (expr * e : ctx->assertions()) { - to_solver_ref(s)->assert_expr(e); + to_solver(s)->assert_expr(e); } to_solver_ref(s)->set_model_converter(ctx->get_model_converter()); } @@ -177,7 +230,7 @@ extern "C" { goal g(m); s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc); for (unsigned i = 0; i < g.size(); ++i) { - to_solver_ref(s)->assert_expr(g.form(i)); + to_solver(s)->assert_expr(g.form(i)); } } @@ -302,6 +355,7 @@ extern "C" { RESET_ERROR_CODE(); init_solver(c, s); to_solver_ref(s)->push(); + if (to_solver(s)->m_pp) to_solver(s)->m_pp->push(); Z3_CATCH; } @@ -314,8 +368,10 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return; } - if (n > 0) + if (n > 0) { to_solver_ref(s)->pop(n); + if (to_solver(s)->m_pp) to_solver(s)->m_pp->pop(n); + } Z3_CATCH; } @@ -342,7 +398,7 @@ extern "C" { RESET_ERROR_CODE(); init_solver(c, s); CHECK_FORMULA(a,); - to_solver_ref(s)->assert_expr(to_expr(a)); + to_solver(s)->assert_expr(to_expr(a)); Z3_CATCH; } @@ -353,7 +409,7 @@ extern "C" { init_solver(c, s); CHECK_FORMULA(a,); CHECK_FORMULA(p,); - to_solver_ref(s)->assert_expr(to_expr(a), to_expr(p)); + to_solver(s)->assert_expr(to_expr(a), to_expr(p)); Z3_CATCH; } @@ -461,6 +517,7 @@ extern "C" { scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { + if (to_solver(s)->m_pp) to_solver(s)->m_pp->check(num_assumptions, _assumptions); result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions); } catch (z3_exception & ex) { diff --git a/src/api/api_solver.h b/src/api/api_solver.h index 90d1c2c65..ed3733a9a 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -21,13 +21,28 @@ Revision History: #include "api/api_util.h" #include "solver/solver.h" +struct solver2smt2_pp { + ast_pp_util m_pp_util; + std::ofstream m_out; + solver2smt2_pp(ast_manager& m, char const* file); + void assert_expr(expr* e); + void assert_expr(expr* e, expr* t); + void push(); + void pop(unsigned n); + void check(unsigned n, expr* const* asms); +}; + struct Z3_solver_ref : public api::object { scoped_ptr m_solver_factory; ref m_solver; params_ref m_params; symbol m_logic; + scoped_ptr m_pp; Z3_solver_ref(api::context& c, solver_factory * f): api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null) {} ~Z3_solver_ref() override {} + + void assert_expr(expr* e); + void assert_expr(expr* e, expr* t); }; inline Z3_solver_ref * to_solver(Z3_solver s) { return reinterpret_cast(s); } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5d24c0292..07198bc91 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6436,7 +6436,7 @@ unknown = CheckSatResult(Z3_L_UNDEF) class Solver(Z3PPObject): """Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.""" - def __init__(self, solver=None, ctx=None): + def __init__(self, solver=None, ctx=None, logFile=None): assert solver is None or ctx is not None self.ctx = _get_ctx(ctx) self.backtrack_level = 4000000000 @@ -6446,6 +6446,8 @@ class Solver(Z3PPObject): else: self.solver = solver Z3_solver_inc_ref(self.ctx.ref(), self.solver) + if logFile is not None: + Z3_solver_open_smt2log(self.ctx.ref(), self.solver, logFile) def __del__(self): if self.solver is not None and self.ctx.ref() is not None: @@ -6906,7 +6908,7 @@ class Solver(Z3PPObject): e = BoolVal(True, self.ctx).as_ast() return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e) -def SolverFor(logic, ctx=None): +def SolverFor(logic, ctx=None, logFile=None): """Create a solver customized for the given logic. The parameter `logic` is a string. It should be contains @@ -6924,9 +6926,9 @@ def SolverFor(logic, ctx=None): """ ctx = _get_ctx(ctx) logic = to_symbol(logic) - return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx) + return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx, logFile) -def SimpleSolver(ctx=None): +def SimpleSolver(ctx=None, logFile=None): """Return a simple general purpose solver with limited amount of preprocessing. >>> s = SimpleSolver() @@ -6936,7 +6938,7 @@ def SimpleSolver(ctx=None): sat """ ctx = _get_ctx(ctx) - return Solver(Z3_mk_simple_solver(ctx.ref()), ctx) + return Solver(Z3_mk_simple_solver(ctx.ref()), ctx, logFile) ######################################### # @@ -7662,7 +7664,7 @@ class Tactic: if self.tactic is not None and self.ctx.ref() is not None: Z3_tactic_dec_ref(self.ctx.ref(), self.tactic) - def solver(self): + def solver(self, logFile=None): """Create a solver using the tactic `self`. The solver supports the methods `push()` and `pop()`, but it @@ -7677,7 +7679,7 @@ class Tactic: >>> s.model() [x = 1.4142135623?] """ - return Solver(Z3_mk_solver_from_tactic(self.ctx.ref(), self.tactic), self.ctx) + return Solver(Z3_mk_solver_from_tactic(self.ctx.ref(), self.tactic), self.ctx, logFile) def apply(self, goal, *arguments, **keywords): """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 673d22a9a..35709ceb5 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6332,6 +6332,21 @@ extern "C" { */ void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s); + /** + \brief Log solver interactions into an SMT2 file. + The tracked interactions are: + - Z3_solver_assert + - Z3_solver_assert_and_track + - Z3_solver_push + - Z3_solver_pop + - Z3_solver_check + - Z3_solver_check_assumptions + Assertions that are loaded from a file are also going to be tracked. + + def_API('Z3_solver_open_smt2log', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING))) + */ + void Z3_API Z3_solver_open_smt2log(Z3_context c, Z3_solver s, Z3_string file); + /** \brief Create a backtracking point. diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index a57ea6040..0a1a5b135 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -38,32 +38,63 @@ void ast_pp_util::collect(expr_ref_vector const& es) { void ast_pp_util::display_decls(std::ostream& out) { ast_smt_pp pp(m); - coll.order_deps(); + bool first = m_num_decls == 0; + coll.order_deps(m_num_sorts); unsigned n = coll.get_num_sorts(); - for (unsigned i = 0; i < n; ++i) { + for (unsigned i = m_num_sorts; i < n; ++i) { pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, nullptr); } + m_num_sorts = n; n = coll.get_num_decls(); - for (unsigned i = 0; i < n; ++i) { + for (unsigned i = m_num_decls; i < n; ++i) { func_decl* f = coll.get_func_decls()[i]; if (f->get_family_id() == null_family_id && !m_removed.contains(f)) { ast_smt2_pp(out, f, m_env) << "\n"; } } - vector> recfuns; - recfun::util u(m); - func_decl_ref_vector funs = u.get_rec_funs(); - if (funs.empty()) return; - for (func_decl * f : funs) { - recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs())); + m_num_decls = n; + if (first) { + vector> recfuns; + recfun::util u(m); + func_decl_ref_vector funs = u.get_rec_funs(); + if (funs.empty()) return; + for (func_decl * f : funs) { + recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs())); + } + ast_smt2_pp_recdefs(out, recfuns, m_env); } - ast_smt2_pp_recdefs(out, recfuns, m_env); } void ast_pp_util::remove_decl(func_decl* f) { m_removed.insert(f); } +std::ostream& ast_pp_util::display_expr(std::ostream& out, expr* f, bool neat) { + if (neat) { + ast_smt2_pp(out, f, m_env); + } + else { + ast_smt_pp ll_smt2_pp(m); + ll_smt2_pp.display_expr_smt2(out, f); + } + return out; +} + +void ast_pp_util::display_assert(std::ostream& out, expr* f, bool neat) { + display_expr(out << "(assert ", f, neat) << ")\n"; +} + +void ast_pp_util::display_assert_and_track(std::ostream& out, expr* f, expr* t, bool neat) { + if (neat) { + ast_smt2_pp(out << "(assert (=> ", t, m_env) << " "; + ast_smt2_pp(out, f, m_env) << "))\n"; + } + else { + ast_smt_pp ll_smt2_pp(m); + ll_smt2_pp.display_expr_smt2(out << "(assert (=> ", t); out << " "; + ll_smt2_pp.display_expr_smt2(out, f); out << "))\n"; + } +} void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) { if (neat) { diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h index e70880672..fb0609968 100644 --- a/src/ast/ast_pp_util.h +++ b/src/ast/ast_pp_util.h @@ -27,11 +27,13 @@ class ast_pp_util { ast_manager& m; obj_hashtable m_removed; smt2_pp_environment_dbg m_env; + unsigned m_num_sorts, m_num_decls; + public: decl_collector coll; - ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m) {} + ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m), m_num_sorts(0), m_num_decls(0) {} void collect(expr* e); @@ -45,6 +47,12 @@ class ast_pp_util { void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true); + void display_assert(std::ostream& out, expr* f, bool neat = true); + + void display_assert_and_track(std::ostream& out, expr* f, expr* t, bool neat = true); + + std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true); + smt2_pp_environment& env() { return m_env; } }; diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index dec1076a6..2785eb1fa 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -957,7 +957,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { #if 0 decls.display_decls(strm); #else - decls.order_deps(); + decls.order_deps(0); ast_mark sort_mark; for (sort* s : decls.get_sorts()) { if (!(*m_is_declared)(s)) { diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index bc415c461..7ddc8bd3d 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -113,11 +113,14 @@ void decl_collector::visit(ast* n) { } } -void decl_collector::order_deps() { +void decl_collector::order_deps(unsigned n) { top_sort st; - for (sort * s : m_sorts) st.insert(s, collect_deps(s)); + for (unsigned i = n; i < m_sorts.size(); ++i) { + sort* s = m_sorts.get(i); + st.insert(s, collect_deps(s)); + } st.topological_sort(); - m_sorts.reset(); + m_sorts.shrink(n); for (sort* s : st.top_sorted()) m_sorts.push_back(s); } diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index a567f759c..b103b58d0 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -52,7 +52,7 @@ public: void visit(unsigned n, expr* const* es); void visit(expr_ref_vector const& es); - void order_deps(); + void order_deps(unsigned n); unsigned get_num_sorts() const { return m_sorts.size(); } unsigned get_num_decls() const { return m_decls.size(); }