From 91cdc082c47008c916f35d7d1b7f662a2e21e0cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 28 Oct 2022 17:57:22 -0300 Subject: [PATCH] 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 --- src/api/api_context.cpp | 2 + src/api/api_context.h | 18 ++++++ src/api/api_parsers.cpp | 3 +- src/parsers/smt2/smt2parser.cpp | 14 +++++ src/parsers/smt2/smt2parser.h | 9 ++- src/parsers/smt2/smt2scanner.cpp | 18 ++++-- src/parsers/smt2/smt2scanner.h | 3 +- src/test/smt2print_parse.cpp | 96 +++++++++++++++++++++++++++++++- 8 files changed, 154 insertions(+), 9 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 6d9af74a0..cef63621d 100644 --- a/src/api/api_context.cpp +++ b/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) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 3bc0d4403..a3f027dd5 100644 --- a/src/api/api_context.h +++ b/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 diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 2510d5e17..899750ef7 100644 --- a/src/api/api_parsers.cpp +++ b/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())); } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 45a9a9cc9..9f61d48ca 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/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); diff --git a/src/parsers/smt2/smt2parser.h b/src/parsers/smt2/smt2parser.h index ad8f040b4..30089b7a2 100644 --- a/src/parsers/smt2/smt2parser.h +++ b/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); diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 2027698eb..2fb45db3b 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/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(m_stream.gcount()); + m_stream->read(m_buffer, SCANNER_BUFFER_SIZE); + m_bend = static_cast(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(); + } }; diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h index 5fb59c7cd..dd1aa04c0 100644 --- a/src/parsers/smt2/smt2scanner.h +++ b/src/parsers/smt2/smt2scanner.h @@ -49,7 +49,7 @@ namespace smt2 { unsigned m_bpos; unsigned m_bend; svector m_string; - std::istream& m_stream; + std::istream* m_stream; bool m_cache_input; svector 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); }; diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 81b7ba1e9..ed674de8b 100644 --- a/src/test/smt2print_parse.cpp +++ b/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(); }