From 815518dc026e900392bf0d08ed859e5ec42d1e43 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Jul 2022 20:27:06 -0700 Subject: [PATCH] add facility for incremental parsing #6123 Adding new API object to maintain state between calls to parser. The state is incremental: all declarations of sorts and functions are valid in the next parse. The parser produces an ast-vector of assertions that are parsed in the current calls. The following is a unit test: ``` from z3 import * pc = ParserContext() A = DeclareSort('A') pc.add_sort(A) print(pc.from_string("(declare-const x A) (declare-const y A) (assert (= x y))")) print(pc.from_string("(declare-const z A) (assert (= x z))")) print(parse_smt2_string("(declare-const x Int) (declare-const y Int) (assert (= x y))")) s = Solver() s.from_string("(declare-sort A)") s.from_string("(declare-const x A)") s.from_string("(declare-const y A)") s.from_string("(assert (= x y))") print(s.assertions()) s.from_string("(declare-const z A)") print(s.assertions()) s.from_string("(assert (= x z))") print(s.assertions()) ``` It produces results of the form ``` [x == y] [x == z] [x == y] [x == y] [x == y] [x == y, x == z] ``` Thus, the set of assertions returned by a parse call is just the set of assertions added. The solver maintains state between parser calls so that declarations made in a previous call are still available when declaring the constant 'z'. The same holds for the parser_context_from_string function: function and sort declarations either added externally or declared using SMTLIB2 command line format as strings are valid for later calls. --- src/api/api_parsers.cpp | 198 ++++++++++++++++++++++---------- src/api/api_solver.cpp | 6 +- src/api/api_solver.h | 1 + src/api/python/z3/z3.py | 19 +++ src/api/python/z3/z3types.py | 7 ++ src/api/z3_api.h | 52 +++++++++ src/cmd_context/cmd_context.cpp | 24 ++-- src/cmd_context/cmd_context.h | 1 + 8 files changed, 235 insertions(+), 73 deletions(-) diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 1c5afb34f..f00d0a44a 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -35,6 +35,136 @@ extern "C" { // --------------- // Support for SMTLIB2 + struct Z3_parser_context_ref : public api::object { + scoped_ptr ctx; + + Z3_parser_context_ref(api::context& c): api::object(c) { + ast_manager& m = c.m(); + ctx = alloc(cmd_context, false, &(m)); + install_dl_cmds(*ctx.get()); + install_opt_cmds(*ctx.get()); + install_smt2_extra_cmds(*ctx.get()); + ctx->register_plist(); + ctx->set_ignore_check(true); + } + + ~Z3_parser_context_ref() override {} + }; + + inline Z3_parser_context_ref * to_parser_context(Z3_parser_context pc) { return reinterpret_cast(pc); } + inline Z3_parser_context of_parser_context(Z3_parser_context_ref* pc) { return reinterpret_cast(pc); } + + Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_parser_context(c); + RESET_ERROR_CODE(); + Z3_parser_context_ref * pc = alloc(Z3_parser_context_ref, *mk_c(c)); + mk_c(c)->save_object(pc); + Z3_parser_context r = of_parser_context(pc); + RETURN_Z3(r); + Z3_CATCH_RETURN(nullptr); + } + + void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc) { + Z3_TRY; + LOG_Z3_parser_context_inc_ref(c, pc); + RESET_ERROR_CODE(); + to_parser_context(pc)->inc_ref(); + Z3_CATCH; + } + + void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc) { + Z3_TRY; + LOG_Z3_parser_context_dec_ref(c, pc); + RESET_ERROR_CODE(); + to_parser_context(pc)->dec_ref(); + Z3_CATCH; + } + + static void insert_datatype(ast_manager& m, scoped_ptr& ctx, sort* srt) { + datatype_util dt(m); + if (!dt.is_datatype(srt)) + return; + + for (func_decl * c : *dt.get_datatype_constructors(srt)) { + ctx->insert(c->get_name(), c); + func_decl * r = dt.get_constructor_recognizer(c); + ctx->insert(r->get_name(), r); + for (func_decl * a : *dt.get_constructor_accessors(c)) { + ctx->insert(a->get_name(), a); + } + } + } + + static void insert_sort(ast_manager& m, scoped_ptr& ctx, symbol const& name, sort* srt) { + if (ctx->find_psort_decl(name)) + return; + psort* ps = ctx->pm().mk_psort_cnst(srt); + ctx->insert(ctx->pm().mk_psort_user_decl(0, name, ps)); + insert_datatype(m, ctx, srt); + } + + void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s) { + Z3_TRY; + LOG_Z3_parser_context_add_sort(c, pc, s); + RESET_ERROR_CODE(); + auto& ctx = to_parser_context(pc)->ctx; + sort* srt = to_sort(s); + symbol name = srt->get_name(); + insert_sort(mk_c(c)->m(), ctx, name, srt); + Z3_CATCH; + } + + void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f) { + Z3_TRY; + LOG_Z3_parser_context_add_decl(c, pc, f); + RESET_ERROR_CODE(); + auto& ctx = *to_parser_context(pc)->ctx; + func_decl* fn = to_func_decl(f); + symbol name = fn->get_name(); + ctx.insert(name, fn); + Z3_CATCH; + } + + Z3_ast_vector Z3_parser_context_parse_stream(Z3_context c, scoped_ptr& ctx, bool owned, std::istream& is) { + Z3_TRY; + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + std::stringstream errstrm; + ctx->set_regular_stream(errstrm); + try { + if (!parse_smt2_commands(*ctx, is)) { + if (owned) + ctx = nullptr; + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); + return of_ast_vector(v); + } + } + catch (z3_exception& e) { + if (owned) + ctx = nullptr; + errstrm << e.msg(); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); + return of_ast_vector(v); + } + for (expr* e : ctx->tracked_assertions()) + v->m_ast_vector.push_back(e); + ctx->reset_tracked_assertions(); + return of_ast_vector(v); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string str) { + Z3_TRY; + LOG_Z3_parser_context_from_string(c, pc, str); + std::string s(str); + std::istringstream is(s); + auto& ctx = to_parser_context(pc)->ctx; + Z3_ast_vector r = Z3_parser_context_parse_stream(c, ctx, false, is); + RETURN_Z3(r); + Z3_CATCH_RETURN(nullptr); + } + Z3_ast_vector parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is, unsigned num_sorts, Z3_symbol const _sort_names[], @@ -48,70 +178,16 @@ extern "C" { install_dl_cmds(*ctx.get()); install_opt_cmds(*ctx.get()); install_smt2_extra_cmds(*ctx.get()); - ctx->register_plist(); ctx->set_ignore_check(true); - Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m); - - vector sort_names; - ptr_vector sorts; - for (unsigned i = 0; i < num_sorts; ++i) { - sorts.push_back(to_sort(_sorts[i])); - sort_names.push_back(to_symbol(_sort_names[i])); - } - mk_c(c)->save_object(v); - for (unsigned i = 0; i < num_decls; ++i) { - func_decl* d = to_func_decl(decls[i]); - ctx->insert(to_symbol(decl_names[i]), d); - sort_names.push_back(d->get_range()->get_name()); - sorts.push_back(d->get_range()); - for (sort* s : *d) { - sort_names.push_back(s->get_name()); - sorts.push_back(s); - } - } - datatype_util dt(m); - for (unsigned i = 0; i < num_sorts; ++i) { - sort* srt = sorts[i]; - symbol name = sort_names[i]; - if (ctx->find_psort_decl(name)) { - continue; - } - psort* ps = ctx->pm().mk_psort_cnst(srt); - ctx->insert(ctx->pm().mk_psort_user_decl(0, name, ps)); - if (!dt.is_datatype(srt)) { - continue; - } + for (unsigned i = 0; i < num_decls; ++i) + ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i])); - for (func_decl * c : *dt.get_datatype_constructors(srt)) { - ctx->insert(c->get_name(), c); - func_decl * r = dt.get_constructor_recognizer(c); - ctx->insert(r->get_name(), r); - for (func_decl * a : *dt.get_constructor_accessors(c)) { - ctx->insert(a->get_name(), a); - } - } - } - std::stringstream errstrm; - ctx->set_regular_stream(errstrm); - try { - if (!parse_smt2_commands(*ctx.get(), is)) { - ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); - return of_ast_vector(v); - } - } - catch (z3_exception& e) { - errstrm << e.msg(); - ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); - return of_ast_vector(v); - } - for (expr* e : ctx->tracked_assertions()) { - v->m_ast_vector.push_back(e); - } - return of_ast_vector(v); + for (unsigned i = 0; i < num_sorts; ++i) + insert_sort(m, ctx, to_symbol(_sort_names[i]), to_sort(_sorts[i])); + + return Z3_parser_context_parse_stream(c, ctx, true, is); Z3_CATCH_RETURN(nullptr); } @@ -180,4 +256,6 @@ extern "C" { RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str())); } + + }; diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 8e5ebcf2a..53fe1166d 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -256,7 +256,10 @@ extern "C" { } void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) { - scoped_ptr ctx = alloc(cmd_context, false, &(mk_c(c)->m())); + auto& solver = *to_solver(s); + if (!solver.m_cmd_context) + solver.m_cmd_context = alloc(cmd_context, false, &(mk_c(c)->m())); + auto& ctx = solver.m_cmd_context; ctx->set_ignore_check(true); std::stringstream errstrm; ctx->set_regular_stream(errstrm); @@ -272,6 +275,7 @@ extern "C" { init_solver(c, s); for (expr* e : ctx->tracked_assertions()) to_solver(s)->assert_expr(e); + ctx->reset_tracked_assertions(); to_solver_ref(s)->set_model_converter(ctx->get_model_converter()); } diff --git a/src/api/api_solver.h b/src/api/api_solver.h index 5e01d5349..62be1ee60 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -44,6 +44,7 @@ struct Z3_solver_ref : public api::object { params_ref m_params; symbol m_logic; scoped_ptr m_pp; + scoped_ptr m_cmd_context; mutex m_mux; event_handler* m_eh; diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 7dbef9f6e..5d728e594 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9192,6 +9192,25 @@ def _dict2darray(decls, ctx): i = i + 1 return sz, _names, _decls +class ParserContext: + def __init__(self, ctx= None): + self.ctx = _get_ctx(ctx) + self.pctx = Z3_mk_parser_context(self.ctx.ref()) + Z3_parser_context_inc_ref(self.ctx.ref(), self.pctx) + + def __del__(self): + if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None: + Z3_parser_context_dec_ref(self.ctx.ref(), self.pctx) + self.pctx = None + + def add_sort(self, sort): + Z3_parser_context_add_sort(self.ctx.ref(), self.pctx, sort.as_ast()) + + def add_decl(self, decl): + Z3_parser_context_add_decl(self.ctx.ref(), self.pctx, decl.as_ast()) + + def from_string(self, s): + return AstVector(Z3_parser_context_from_string(self.ctx.ref(), self.pctx, s), self.ctx) def parse_smt2_string(s, sorts={}, decls={}, ctx=None): """Parse a string in SMT 2.0 format using the given sorts and decls. diff --git a/src/api/python/z3/z3types.py b/src/api/python/z3/z3types.py index 6c93c0bee..500e3606e 100644 --- a/src/api/python/z3/z3types.py +++ b/src/api/python/z3/z3types.py @@ -216,6 +216,13 @@ class ParamDescrs(ctypes.c_void_p): def from_param(obj): return obj +class ParserContextObj(ctypes.c_void_p): + def __init__(self, pc): + self._as_parameter_ = pc + + def from_param(obj): + return obj + class FuncInterpObj(ctypes.c_void_p): def __init__(self, f): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index dbf8d9252..831e03b0e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -20,6 +20,7 @@ DEFINE_TYPE(Z3_constructor); DEFINE_TYPE(Z3_constructor_list); DEFINE_TYPE(Z3_params); DEFINE_TYPE(Z3_param_descrs); +DEFINE_TYPE(Z3_parser_context); DEFINE_TYPE(Z3_goal); DEFINE_TYPE(Z3_tactic); DEFINE_TYPE(Z3_probe); @@ -58,6 +59,7 @@ DEFINE_TYPE(Z3_rcf_num); - \c Z3_constructor_list: list of constructors for a (recursive) datatype. - \c Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc. - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. + - \c Z3_parser_context: context for incrementally parsing strings. Declarations can be added incrementally to the parser state. - \c Z3_model: model for the constraints asserted into the logical context. - \c Z3_func_interp: interpretation of a function in a model. - \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point. @@ -1413,6 +1415,7 @@ typedef enum def_Type('CONSTRUCTOR_LIST', 'Z3_constructor_list', 'ConstructorList') def_Type('SOLVER', 'Z3_solver', 'SolverObj') def_Type('SOLVER_CALLBACK', 'Z3_solver_callback', 'SolverCallbackObj') + def_Type('PARSER_CONTEXT', 'Z3_parser_context', 'ParserContextObj') def_Type('GOAL', 'Z3_goal', 'GoalObj') def_Type('TACTIC', 'Z3_tactic', 'TacticObj') def_Type('PARAMS', 'Z3_params', 'Params') @@ -5827,6 +5830,55 @@ extern "C" { Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str); + + /** + \brief Create a parser context. + + A parser context maintains state between calls to \c Z3_parser_context_parse_string + where the caller can pass in a set of SMTLIB2 commands. + It maintains all the declarations from previous calls together with + of sorts and function declarations (including 0-ary) that are added directly to the context. + + def_API('Z3_mk_parser_context', PARSER_CONTEXT, (_in(CONTEXT),)) + */ + Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c); + + /** + \brief Increment the reference counter of the given \c Z3_parser_context object. + + def_API('Z3_parser_context_inc_ref', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT))) + */ + void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc); + + /** + \brief Decrement the reference counter of the given \c Z3_parser_context object. + + def_API('Z3_parser_context_dec_ref', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT))) + */ + void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc); + + /** + \brief Add a sort declaration. + + def_API('Z3_parser_context_add_sort', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT), _in(SORT))) + */ + void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s); + + /** + \brief Add a function declaration. + + def_API('Z3_parser_context_add_decl', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT), _in(FUNC_DECL))) + */ + void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f); + + /** + \brief Parse a string of SMTLIB2 commands. Return assertions. + + def_API('Z3_parser_context_from_string', AST_VECTOR, (_in(CONTEXT), _in(PARSER_CONTEXT), _in(STRING))) + */ + Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s); + + /**@}*/ /** @name Error Handling */ diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 2174c9e0b..705396f53 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2203,22 +2203,25 @@ expr_ref_vector cmd_context::tracked_assertions() { for (unsigned i = 0; i < assertions().size(); ++i) { expr* an = assertion_names()[i]; expr* asr = assertions()[i]; - if (an) { + if (an) result.push_back(m().mk_implies(an, asr)); - } - else { + else result.push_back(asr); - } } } else { - for (expr * e : assertions()) { + for (expr * e : assertions()) result.push_back(e); - } } return result; } +void cmd_context::reset_tracked_assertions() { + m_assertion_names.reset(); + for (expr* a : m_assertions) + m().dec_ref(a); + m_assertions.reset(); +} void cmd_context::display_assertions() { if (!m_interactive_mode) @@ -2254,9 +2257,8 @@ format_ns::format * cmd_context::pp(sort * s) const { } cmd_context::pp_env & cmd_context::get_pp_env() const { - if (m_pp_env.get() == nullptr) { + if (m_pp_env.get() == nullptr) const_cast(this)->m_pp_env = alloc(pp_env, *const_cast(this)); - } return *(m_pp_env.get()); } @@ -2314,9 +2316,8 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr out << "(set-logic " << logic << ")" << std::endl; // collect uninterpreted function declarations decl_collector decls(m()); - for (unsigned i = 0; i < num; i++) { + for (unsigned i = 0; i < num; i++) decls.visit(assertions[i]); - } // TODO: display uninterpreted sort decls, and datatype decls. @@ -2342,9 +2343,8 @@ void cmd_context::slow_progress_sample() { svector labels; m_solver->get_labels(labels); regular_stream() << "(labels"; - for (symbol const& s : labels) { + for (symbol const& s : labels) regular_stream() << " " << s; - } regular_stream() << "))" << std::endl; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 60a6e930b..c51809190 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -485,6 +485,7 @@ public: ptr_vector const& assertions() const { return m_assertions; } ptr_vector const& assertion_names() const { return m_assertion_names; } expr_ref_vector tracked_assertions(); + void reset_tracked_assertions(); /** \brief Hack: consume assertions if there are no scopes.