Optimize calls to Z3_eval_smtlib2_string (#6422)

* Allow reseting the stream of smt2::scanner

* Put the parser of parse_smt2_commands in the cmd_context

* Move parser streams to cmd_context

* Move parser fields from cmd_context to api::context

* Move forward declarations from cmd_context.h to api_context.h

* Change parse_smt2_commands_with_parser to use *& instead of **

* Add tests for Z3_eval_smtlib2_string

* Don't reuse the streams in Z3_eval_smtlib2_string

* Fix indentation

* Add back unnecessary deleted line

Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>

src/api/api_context.cpp

@@ -149,6 +149,8 @@ namespace api {
 
 
     context::~context() {
+        if (m_parser)
+            smt2::free_parser(m_parser);
         m_last_obj = nullptr;
         flush_objects();
         for (auto& kv : m_allocated_objects) {

src/api/api_context.h

@@ -50,6 +50,11 @@ namespace realclosure {
     class manager;
 };
 
+namespace smt2 {
+    class parser;
+    void free_parser(parser*);
+};
+
 namespace api {
        
     class seq_expr_solver : public expr_solver {
@@ -233,6 +238,19 @@ namespace api {
 
         void check_sorts(ast * n);
 
+
+        // ------------------------------------------------
+        //
+        // State reused by calls to Z3_eval_smtlib2_string
+        //
+        // ------------------------------------------------
+        //
+        // The m_parser field is reused by all calls of Z3_eval_smtlib2_string using this context.
+        // It is an optimization to save the cost of recreating these objects on each invocation.
+        //
+        // See https://github.com/Z3Prover/z3/pull/6422 for the motivation
+        smt2::parser*                m_parser = nullptr;
+
         // ------------------------
         //
         // Polynomial manager & caches

src/api/api_parsers.cpp

@@ -246,7 +246,8 @@ extern "C" {
         ctx->set_diagnostic_stream(ous);
         cmd_context::scoped_redirect _redirect(*ctx);
         try {
-            if (!parse_smt2_commands(*ctx.get(), is)) {
+            // See api::context::m_parser for a motivation about the reuse of the parser
+            if (!parse_smt2_commands_with_parser(mk_c(c)->m_parser, *ctx.get(), is)) {
                 SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
                 RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
             }

src/parsers/smt2/smt2parser.cpp

@@ -3105,6 +3105,10 @@ namespace smt2 {
 
         }
 
+        void reset_input(std::istream & is, bool interactive) {
+            m_scanner.reset_input(is, interactive);
+        }
+
         sexpr_ref parse_sexpr_ref() {
             m_num_bindings    = 0;
             m_num_open_paren = 0;
@@ -3204,6 +3208,8 @@ namespace smt2 {
             }
         }
     };
+
+    void free_parser(parser * p) { dealloc(p); }
 };
 
 bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) {
@@ -3211,6 +3217,14 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive,
     return p();
 }
 
+bool parse_smt2_commands_with_parser(class smt2::parser *& p, cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) {
+    if (p)
+        p->reset_input(is, interactive);
+    else
+        p = alloc(smt2::parser, ctx, is, interactive, ps, filename);
+    return (*p)();
+}
+
 sort_ref parse_smt2_sort(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) {
     smt2::parser p(ctx, is, interactive, ps, filename);
     return p.parse_sort_ref(filename);

src/parsers/smt2/smt2parser.h

@@ -20,7 +20,14 @@ Revision History:
 
 #include "cmd_context/cmd_context.h"
 
-bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref(), char const * filename = nullptr);
+namespace smt2 {
+    class parser;
+    void free_parser(parser * p);
+}
+
+bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & ps = params_ref(), char const * filename = nullptr);
+
+bool parse_smt2_commands_with_parser(class smt2::parser *& p, cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & ps = params_ref(), char const * filename = nullptr);
 
 sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename);
 

src/parsers/smt2/smt2scanner.cpp

@@ -27,8 +27,8 @@ namespace smt2 {
         if (m_at_eof)
             throw scanner_exception("unexpected end of file");
         if (m_interactive) {
-            m_curr = m_stream.get();
-            if (m_stream.eof())
+            m_curr = m_stream->get();
+            if (m_stream->eof())
                 m_at_eof = true;
         }
         else if (m_bpos < m_bend) {
@@ -36,8 +36,8 @@ namespace smt2 {
             m_bpos++;
         }
         else {
-            m_stream.read(m_buffer, SCANNER_BUFFER_SIZE);
-            m_bend = static_cast<unsigned>(m_stream.gcount());
+            m_stream->read(m_buffer, SCANNER_BUFFER_SIZE);
+            m_bend = static_cast<unsigned>(m_stream->gcount());
             m_bpos = 0;
             if (m_bpos == m_bend) {
                 m_at_eof = true;
@@ -281,7 +281,7 @@ namespace smt2 {
         m_bv_size(UINT_MAX),
         m_bpos(0),
         m_bend(0),
-        m_stream(stream),
+        m_stream(&stream),
         m_cache_input(false) {
 
 
@@ -390,5 +390,13 @@ namespace smt2 {
         return m_cache_result.begin();
     }
 
+    void scanner::reset_input(std::istream & stream, bool interactive) {
+        m_stream = &stream;
+        m_interactive = interactive;
+        m_at_eof = false;
+        m_bpos = 0;
+        m_bend = 0;
+        next();
+    }
 };
 

src/parsers/smt2/smt2scanner.h

@@ -49,7 +49,7 @@ namespace smt2 {
         unsigned           m_bpos;
         unsigned           m_bend;
         svector<char>      m_string;
-        std::istream&      m_stream;
+        std::istream*      m_stream;
         
         bool               m_cache_input;
         svector<char>      m_cache;
@@ -99,6 +99,7 @@ namespace smt2 {
         void stop_caching() { m_cache_input = false; }
         unsigned cache_size() const { return m_cache.size(); }
         void reset_cache() { m_cache.reset(); }
+        void reset_input(std::istream & stream, bool interactive = false);
 
         char const * cached_str(unsigned begin, unsigned end);
     };

src/test/smt2print_parse.cpp

@@ -64,6 +64,98 @@ void test_parseprint(char const* spec) {
     Z3_del_context(ctx);
 }
 
+void test_eval(Z3_context ctx, Z3_string spec, bool shouldFail) {
+    std::cout << "spec:\n" << spec << "\n";
+
+    Z3_string resp;
+    bool failed = false;
+    try {
+        resp = Z3_eval_smtlib2_string(ctx, spec);
+    }
+    catch (std::runtime_error& e) {
+        resp = e.what();
+        failed = true;
+    }
+
+    std::cout << "response:\n" << resp << "\n";
+
+    if (shouldFail != failed) {
+        if (shouldFail)
+            throw std::runtime_error("should have failed");
+        else
+            throw std::runtime_error("should have succeeded");
+    }
+}
+
+void throwError(Z3_context c, Z3_error_code e) {
+    throw std::runtime_error(Z3_get_error_msg(c, e));
+}
+
+void test_repeated_eval() {
+    // Z3_eval_smtlib2_string reuses the parser and the scanner
+    // when called repeteadly on the same context.
+    //
+    // These tests rehearse that earlier calls do not interfere
+    // with the result of later calls if the SMT queries are independent.
+
+    char const* spec1 =
+        "(push)\n"
+        "(declare-datatypes (T) ((list (nil) (cons (car T) (cdr list)))))\n"
+        "(declare-const x Int)\n"
+        "(declare-const l (list Int))\n"
+        "(declare-fun f ((list Int)) Bool)\n"
+        "(assert (f (cons x l)))\n"
+        "(check-sat)\n"
+        "(pop)\n";
+
+    char const* spec2 =
+        "(push)\n"
+        "(declare-const a (Array Int Int))\n"
+        "(declare-const b (Array (Array Int Int) Bool))\n"
+        "(assert (select b a))\n"
+        "(assert (= b ((as const (Array (Array Int Int) Bool)) true)))\n"
+        "(assert (= b (store b a true)))\n"
+        "(declare-const b1 (Array Bool Bool))\n"
+        "(declare-const b2 (Array Bool Bool))\n"
+        "(assert (= ((as const (Array Bool Bool)) false) ((_ map and) b1 b2)))\n"
+        "(check-sat)\n"
+        "(pop)\n";
+
+    char const* spec3 =
+        "(push)\n"
+        "(declare-const a@ (Array Int Int))\n"
+        "(declare-const b (Array (Array Int Int) Bool))\n"
+        "(assert (select b a))\n"
+        "(check-sat)\n"
+        "(pop)\n";
+
+    char const* spec4 =
+        "(push)\n"
+        "(declare-const a (Array Int Int))\n"
+        "(declare-const b# (Array (Array Int Int) Bool))\n"
+        "(assert (select b a))\n"
+        "(check-sat)\n"
+        "(pop)\n";
+
+    Z3_context ctx = Z3_mk_context(nullptr);
+    Z3_set_error_handler(ctx, throwError);
+    std::cout << "testing Z3_eval_smtlib2_string\n";
+
+    test_eval(ctx, spec1, false);
+    std::cout << "successful call after successful call\n";
+    test_eval(ctx, spec2, false);
+    std::cout << "failing call after successful call\n";
+    test_eval(ctx, spec3, true);
+    std::cout << "failing call after failing call\n";
+    test_eval(ctx, spec4, true);
+    std::cout << "successful call after failing call\n";
+    test_eval(ctx, spec1, false);
+
+    std::cout << "done evaluating\n";
+
+    Z3_del_context(ctx);
+}
+
 void tst_smt2print_parse() {
 
     // test basic datatypes  
@@ -126,6 +218,8 @@ void tst_smt2print_parse() {
 
     test_parseprint(spec6);
 
-    // Test ?     
+    // Test ?
+
+    test_repeated_eval();
 
 }