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

@@ -35,6 +35,136 @@ extern "C" {
     // ---------------
     // Support for SMTLIB2
 
+    struct Z3_parser_context_ref : public api::object {
+        scoped_ptr<cmd_context> 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<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);
+        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<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, 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<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);
-            }
-        }
-        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()));
     }
+
+
 };

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());
     }
 

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;
 

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.

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):

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 */

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<cmd_context*>(this)->m_pp_env = alloc(pp_env, *const_cast<cmd_context*>(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<symbol> 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;
 }
 

src/cmd_context/cmd_context.h

@@ -485,6 +485,7 @@ public:
     ptr_vector<expr> const& assertions() const { return m_assertions; }
     ptr_vector<expr> 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.