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.
Z3Prover · Jul 2, 2022 · 815518d · 815518d
1 parent 8c2ba3d
commit 815518d
Show file tree

Hide file tree

Showing 8 changed files with 233 additions and 71 deletions.
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
@@ -35,83 +35,159 @@ extern "C" {
     // ---------------
     // Support for SMTLIB2
 
-    Z3_ast_vector parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is,
-                                       unsigned num_sorts,
-                                       Z3_symbol const _sort_names[],
-                                       Z3_sort const _sorts[],
-                                       unsigned num_decls,
-                                       Z3_symbol const decl_names[],
-                                       Z3_func_decl const decls[]) {
-        Z3_TRY;
-        ast_manager& m = mk_c(c)->m();
-        scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(m));
-        install_dl_cmds(*ctx.get());
-        install_opt_cmds(*ctx.get());
-        install_smt2_extra_cmds(*ctx.get());
+    struct Z3_parser_context_ref : public api::object {
+        scoped_ptr<cmd_context> ctx;
 
-        ctx->register_plist();
-        ctx->set_ignore_check(true);
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
-
-        vector<symbol> sort_names;
-        ptr_vector<sort> 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);
-            }
+        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<Z3_parser_context_ref*>(pc); }
+    inline Z3_parser_context of_parser_context(Z3_parser_context_ref* pc) { return reinterpret_cast<Z3_parser_context>(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<cmd_context>& ctx, sort* srt) {
         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;
+        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);
             }
+        }            
+    }
 
-            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<cmd_context>& 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<cmd_context>& 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.get(), is)) {
-                ctx = nullptr;
+            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();
-            ctx = nullptr;
             SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
             return of_ast_vector(v);
         }
-        for (expr* e : ctx->tracked_assertions()) {
+        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[],
+                                       Z3_sort const _sorts[],
+                                       unsigned num_decls,
+                                       Z3_symbol const decl_names[],
+                                       Z3_func_decl const decls[]) {
+        Z3_TRY;
+        ast_manager& m = mk_c(c)->m();
+        scoped_ptr<cmd_context> 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);
+
+        for (unsigned i = 0; i < num_decls; ++i) 
+            ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
+
+        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
@@ -256,7 +256,10 @@ extern "C" {
     }
 
     void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) {
-        scoped_ptr<cmd_context> 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
@@ -44,6 +44,7 @@ struct Z3_solver_ref : public api::object {
     params_ref                 m_params;
     symbol                     m_logic;
     scoped_ptr<solver2smt2_pp> m_pp;
+    scoped_ptr<cmd_context>    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
@@ -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
@@ -216,6 +216,13 @@ def __init__(self, paramdescrs):
     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
@@ -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 */