From f1b6d1c7f33f344cc0f5f7a6101606250e2cf604 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 18:04:20 -0700 Subject: [PATCH] removing 'fat' from smt 1.0 parser Signed-off-by: Leonardo de Moura --- src/api/smtparser.cpp | 2377 +---------------------------------------- src/api/smtparser.h | 2 - 2 files changed, 3 insertions(+), 2376 deletions(-) diff --git a/src/api/smtparser.cpp b/src/api/smtparser.cpp index 91b636d09..f290c717b 100644 --- a/src/api/smtparser.cpp +++ b/src/api/smtparser.cpp @@ -16,7 +16,6 @@ Author: Revision History: --*/ - #include #include #include @@ -32,17 +31,15 @@ Revision History: #include"ast_pp.h" #include"bv_decl_plugin.h" #include"array_decl_plugin.h" -#include"datatype_decl_plugin.h" #include"warning.h" #include"error_codes.h" #include"pattern_validation.h" -#include"unifier.h" #include"timeit.h" #include"var_subst.h" #include"well_sorted.h" -#include "str_hashtable.h" -#include "front_end_params.h" -#include "stopwatch.h" +#include"str_hashtable.h" +#include"front_end_params.h" +#include"stopwatch.h" front_end_params& Z3_API Z3_get_parameters(Z3_context c); class id_param_info { @@ -464,66 +461,6 @@ private: }; -enum smt_cmd_token { - SMT_CMD_SET_LOGIC, // logic-name - SMT_CMD_DECLARE_SORTS, // sorts-symbols - SMT_CMD_DECLARE_FUNS, // func-decls - SMT_CMD_DECLARE_PREDS, // pred-decls - SMT_CMD_DECLARE_DATATYPES, // datatypes - SMT_CMD_DEFINE, // var expr - SMT_CMD_DEFINE_SORTS, // (var sort)* - SMT_CMD_DECLARE_SORT, // - SMT_CMD_DEFINE_SORT, // (*) - SMT_CMD_DECLARE_FUN, // (*) - SMT_CMD_DECLARE_CONST, // - SMT_CMD_DEFINE_FUN, // (*) - SMT_CMD_GET_VALUE, // (+) - - SMT_CMD_PUSH, // numeral - SMT_CMD_POP, // numeral - SMT_CMD_ASSERT, // expr - SMT_CMD_CHECK_SAT, // - SMT_CMD_GET_CORE, // expr+ - SMT_CMD_NEXT_SAT, - SMT_CMD_SIMPLIFY, // expr - SMT_CMD_GET_IMPLIED_EQUALITIES, // expr* - SMT_CMD_EVAL, // expr - SMT_CMD_GET_ASSERTIONS, // string - SMT_CMD_GET_SAT_ASSERTIONS, // string - SMT_CMD_KEEP_SAT_ASSERTIONS, // - SMT_CMD_GET_UNSAT_CORE, // string - SMT_CMD_GET_PROOF, // string - SMT_CMD_SET_OPTION, // string strings - SMT_CMD_GET_INFO, // string - SMT_CMD_SET_INFO, // string strings - SMT_CMD_ECHO, // string strings - SMT_CMD_EXIT, // - // set-option: - SMT_CMD_PRINT_SUCCESS, - SMT_CMD_RANDOM_SEED, - SMT_CMD_VERBOSITY, - SMT_CMD_EXPAND_DEFINITIONS, - SMT_CMD_OUTPUT_CHANNEL, - SMT_CMD_VERBOSE_OUTPUT_CHANNEL, - SMT_CMD_ENABLE_CORES, - SMT_CMD_SET_PARAM, - SMT_CMD_PRODUCE_MODELS, - // set-info: - SMT_CMD_NAME, - SMT_CMD_VERSION, - SMT_CMD_AUTHORS, - SMT_CMD_LAST_FAILURE, - SMT_CMD_REASON_UNKNOWN, - SMT_CMD_STATS, - SMT_CMD_MODEL, - SMT_CMD_TIME, - SMT_CMD_LABELS, - SMT_CMD_HELP, // help - - SMT_CMD_ERROR // error token -}; - - using namespace smtlib; class idbuilder { @@ -591,1280 +528,6 @@ public: } }; - - - -class scoped_stream { - std::ostream& m_default; - std::ostream* m_stream; - bool m_owned; -public: - - scoped_stream(std::ostream& strm) : m_default(strm) { - m_stream = &strm; - m_owned = false; - } - - scoped_stream(proto_expr* e) : m_default(std::cout), m_stream(0), m_owned(false) { - reset(e, 0); - } - - scoped_stream(proto_expr* e, std::ostream& out) : m_default(out), m_stream(0), m_owned(false) { - reset(e, &out); - } - - ~scoped_stream() { - dealloc_stream(); - } - - void reset(proto_expr* e, std::ostream* out = 0) { - char const* name = (e && e->kind() == proto_expr::ID)?e->string().bare_str():0; - reset(name, out); - } - - void reset(char const* name, std::ostream* out = 0) { - dealloc_stream(); - m_owned = false; - if (!out) { - out = &m_default; - } - if (!name) { - m_stream = out; - } - else if (strcmp(name, "stdout")) { - m_stream = &std::cout; - } - else if (strcmp(name, "stderr")) { - m_stream = &std::cerr; - } - else { - m_stream = alloc(std::ofstream, name, std::ios_base::app); - m_owned = true; - if (m_stream->bad() || m_stream->fail()) { - dealloc(m_stream); - m_stream = out; - m_owned = false; - } - } - SASSERT(m_stream); - } - - std::ostream& operator*() { - return *m_stream; - } - -private: - void dealloc_stream() { - if (m_owned) { - m_stream->flush(); - dealloc(m_stream); - } - m_stream = 0; - m_owned = false; - } -}; - -class cmd_exn { - Z3_error_code m_code; -public: - cmd_exn(Z3_error_code code) : m_code(code) {} - Z3_error_code get() const { return m_code; } -}; - -static void* g_sw = 0; - -#define cmd_context _cmd_context - -class cmd_context { - typedef map str2token; - str2token m_str2token; - ptr_vector m_token2str; - ptr_vector m_token2help; - ptr_vector m_token2args; - svector m_is_command; - - struct cmd_info { - smt_cmd_token m_token; - void (*m_action)(cmd_context&); - cmd_info(smt_cmd_token t, void (*action)(cmd_context&)): - m_token(t), m_action(action) {} - }; - - struct opt { - smt_cmd_token m_token; - bool (*m_action)(cmd_context&, proto_expr* const* exprs); - opt(smt_cmd_token t, bool (*action)(cmd_context&, proto_expr* const* exprs)): - m_token(t), m_action(action) {} - }; - - enum check_sat_state { - state_unsat, - state_sat, - state_unknown, - state_clear, - state_new_assertion - }; - - Z3_context m_context; - Z3_model m_model; - Z3_ast m_proof; - ast_manager& m_manager; - scoped_stream m_out; - scoped_stream m_verbose; - symbol_table m_table; - region m_region; - ast_ref_vector m_trail; - unsigned_vector m_trail_lim; - expr_ref_vector m_asserted; - unsigned_vector m_asserted_lim; - expr_ref_vector m_asserted_proxies; - unsigned_vector m_asserted_proxies_lim; - bool m_print_success; - bool m_enable_cores; - unsigned m_core_size; - svector m_core; - check_sat_state m_check_sat_state; - svector m_check_sat_states; - stopwatch m_watch; - svector m_infos; - svector m_options; - std::ostringstream m_error_stream; - - smtlib::benchmark::status m_status; - -public: - - cmd_context(ast_manager& m, Z3_context ctx, std::istream& is, std::ostream& out): - m_context(ctx), - m_model(0), - m_proof(0), - m_manager(m), - m_out(out), - m_verbose(std::cerr), - m_trail(m), - m_asserted(m), - m_asserted_proxies(m), - m_print_success(Z3_get_parameters(ctx).m_smtlib2_compliant), - m_enable_cores(false), - m_core_size(0), - m_check_sat_state(state_clear), - m_status(smtlib::benchmark::UNKNOWN) - { - add_command("set-logic", - SMT_CMD_SET_LOGIC, - "", "set the background logic"); - add_command("declare-sorts", - SMT_CMD_DECLARE_SORTS, - "", "declare sorts"); - add_command("declare-funs", - SMT_CMD_DECLARE_FUNS, - "", - "declare functions and constants"); - add_command("declare-preds", - SMT_CMD_DECLARE_PREDS, - "", - "declare predicates"); - add_command("declare-datatypes", - SMT_CMD_DECLARE_DATATYPES, - "", - "declare recursive datatypes"); - add_command("define", - SMT_CMD_DEFINE, - " or ( ( )*) ", - "define an expression shorthand"); - add_command("define-sorts", - SMT_CMD_DEFINE_SORTS, - "( )*", - "define shorthand for compound sorts, such as arrays"); - - add_command("declare-sort", - SMT_CMD_DECLARE_SORT, - "", "declare sort"); - add_command("define-sort", - SMT_CMD_DEFINE_SORT, - " (*) ", - "define shorthand for compound sorts, such as arrays"); - add_command("declare-fun", - SMT_CMD_DECLARE_FUN, - " (*) ", - "declare function or constant"); - add_command("declare-const", - SMT_CMD_DECLARE_CONST, - " ", - "declare constant"); - add_command("define-fun", - SMT_CMD_DEFINE_FUN, - " (*) ", - "define an expression shorthand"); - add_command("get-value", - SMT_CMD_GET_VALUE, - "(+)", - "evaluate list of terms"); - - - add_command("push", - SMT_CMD_PUSH, - "[]", - "push 1 (or ) scopes"); - add_command("pop", - SMT_CMD_POP, - "[]", - "pop 1 (or ) scopes"); - add_command("assert", - SMT_CMD_ASSERT, - "", - "assert expression"); - add_command("check-sat", - SMT_CMD_CHECK_SAT, - "*", - "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."); - add_command("get-core", - SMT_CMD_GET_CORE, - "+", - "check if the assumptions are consistent with the current context"); - add_command("next-sat", - SMT_CMD_NEXT_SAT, - "", - "get the next satisfying assignment"); - add_command("simplify", - SMT_CMD_SIMPLIFY, - "", - "simplify expression and print back result"); - add_command("get-implied-equalities", - SMT_CMD_GET_IMPLIED_EQUALITIES, - "*", - "obtain list of identifiers for expressions, such that equal expressions have the same identfiers" - ); - add_command("eval", - SMT_CMD_EVAL, - "", - "evaluate expression using the current model and print back result"); - add_command("get-assertions", - SMT_CMD_GET_ASSERTIONS, - "[]", - "retrieve current assertions"); - add_command("get-sat-assertions", - SMT_CMD_GET_SAT_ASSERTIONS, - "[]", - "retrieve current satisfying assignment"); - add_command("keep-sat-assertions", - SMT_CMD_KEEP_SAT_ASSERTIONS, - "", - "assert current satisfying assignment"); - add_command("get-unsat-core", - SMT_CMD_GET_UNSAT_CORE, - "[]", - "retrieve unsatisfiable core of assertions"); - add_command("get-proof", - SMT_CMD_GET_PROOF, - "[]", - "retrieve proof"); - add_command("set-option", - SMT_CMD_SET_OPTION, - "", - "set auxiliary options"); - add_command("set-info", - SMT_CMD_SET_INFO, - " ", - "set auxiliary information"); - add_command("get-info", - SMT_CMD_GET_INFO, - "", - "retrieve auxiliary information"); - add_command("echo", - SMT_CMD_ECHO, - "", - "display the given strings"); - add_command("exit", - SMT_CMD_EXIT, - "", - "exit Z3 session"); - m_str2token.insert("quit", SMT_CMD_EXIT); - add_option("print-success", - SMT_CMD_PRINT_SUCCESS, - "[]", - "toggle printing success", - &print_success_option); - add_option("verbosity", - SMT_CMD_VERBOSITY, - "", - "set verbosity", - &verbosity_option); - add_option("regular-output-channel", - SMT_CMD_OUTPUT_CHANNEL, - "[]", - "set name of alternate output channel", - &output_channel_option); - add_option("enable-cores", - SMT_CMD_ENABLE_CORES, - "", - "enable core extraction during solving", - &enable_cores_option); - add_option("set-param", - SMT_CMD_SET_PARAM, - " ", - "update a mutable configuration parameter", - &update_param_option); - - add_option("verbose-output-channel", - SMT_CMD_VERBOSE_OUTPUT_CHANNEL, - "", - "set output channel", - &set_verbose_output_channel_option - ); - add_option("produce-models", - SMT_CMD_PRODUCE_MODELS, - "[]", - "toggle model generation", - &produce_models_option); - // - // other options: - // add_option("random-seed", SMT_CMD_RANDOM_SEED, 0, ""); - // add_option("expand-definitions",SMT_CMD_EXPAND_DEFINITIONS, 0, ""); - // "produce-proofs" - // "produce-models" - // "produce-assignments" - // - - add_info("name", - SMT_CMD_NAME, - "", - "solver name", - &name_info - ); - add_info("version", - SMT_CMD_VERSION, - "", - "solver version", - &version_info - ); - add_info("authors", - SMT_CMD_AUTHORS, - "", - "solver authors", - &authors_info); - add_info("statistics", - SMT_CMD_STATS, - "", - "search statistics", - &stats_info); - add_info("all-statistics", - SMT_CMD_STATS, - "", - "search statistics", - &stats_info); - add_info("model", - SMT_CMD_MODEL, - "", - "model from satisfied assertions", - &model_info - ); - add_info("last-failure", - SMT_CMD_LAST_FAILURE, - "", - "reason for previous search failure", - &last_failure_info - ); - add_info("reason-unknown", - SMT_CMD_REASON_UNKNOWN, - "", - "reason for previous unknown answer; 'memout' for out of memory, 'incomplete' for everything else", - &reason_unknown_info - ); - add_info("time", - SMT_CMD_TIME, - "", - "time taken by solver", - &time_info - ); - add_info("labels", - SMT_CMD_LABELS, - "", - "retrieve (Boogie) labels from satisfiable assertion", - &labels_info); - add_info("help", - SMT_CMD_HELP, - "", - "print this help", - &help_info); - - - -#ifdef _EXTERNAL_RELEASE - Z3_set_ast_print_mode(m_context, Z3_PRINT_SMTLIB2_COMPLIANT); -#else - // use internal pretty printer - Z3_set_ast_print_mode(m_context, Z3_PRINT_SMTLIB_FULL); - // Z3_set_ast_print_mode(m_context, Z3_PRINT_SMTLIB2_COMPLIANT); -#endif - Z3_set_error_handler(m_context, error_handler); - set_error_stream(&m_error_stream); - set_warning_stream(&m_error_stream); - } - - ~cmd_context() { - if (m_model) { - Z3_del_model(m_context, m_model); - } - set_error_stream(0); - set_warning_stream(0); - } - - // - // NB. As it is now, the symbol table used in m_benchmark is not - // scoped. Declarations just live on or get over-written. - // - void push(unsigned num_scopes) { - while (num_scopes > 0) { - m_table.begin_scope(); - m_region.push_scope(); - Z3_push(m_context); - m_trail_lim.push_back(m_trail.size()); - m_asserted_lim.push_back(m_asserted.size()); - m_asserted_proxies_lim.push_back(m_asserted_proxies.size()); - --num_scopes; - m_check_sat_states.push_back(m_check_sat_state); - } - } - void pop(unsigned num_scopes) { - if (m_trail_lim.size() < num_scopes) { - num_scopes = m_trail_lim.size(); - } - Z3_pop(m_context, num_scopes); - m_region.pop_scope(num_scopes); - while (num_scopes > 0) { - m_table.end_scope(); - --num_scopes; - m_trail.resize(m_trail_lim.back()); - m_trail_lim.pop_back(); - m_asserted.resize(m_asserted_lim.back()); - m_asserted_lim.pop_back(); - m_asserted_proxies.resize(m_asserted_proxies_lim.back()); - m_asserted_proxies_lim.pop_back(); - m_check_sat_state = m_check_sat_states.back(); - m_check_sat_states.pop_back(); - } - m_proof = 0; - m_core_size = 0; - } - - static void error_handler(Z3_context, Z3_error_code code) { - throw cmd_exn(code); - } - - symbol_table& get_table() { return m_table; } - - Z3_context get_context() { return m_context; } - - std::ostream& get_out() { return *m_out; } - - void print_quoted(const char* str) { get_out() << "\"" << str << "\""; } - - void set_out(proto_expr* e) { m_out.reset(e); } - - void add_trail(ast* a) { m_trail.push_back(a); } - - void add_asserted(expr* e) { - if (get_enable_cores()) { - expr* proxy = m_manager.mk_fresh_const("proxy", m_manager.mk_bool_sort()); - expr_ref imp(m_manager); - // It is not necessary to use iff (it is just overhead). - imp = m_manager.mk_implies(proxy, e); - TRACE("proxy", tout << "new proxy:\n " << mk_pp(imp, m_manager) << "\n";); - Z3_assert_cnstr(m_context, reinterpret_cast(imp.get())); - m_asserted_proxies.push_back(proxy); - } - else { - Z3_assert_cnstr(m_context, reinterpret_cast(e)); - } - m_asserted.push_back(e); - if (m_check_sat_state != state_unsat) { - m_check_sat_state = state_new_assertion; - } - } - - unsigned get_num_assertions() const { return m_asserted.size(); } - - expr* get_assertion(unsigned idx) { return m_asserted[idx].get(); } - - Z3_ast* get_proxies_ptr() { return reinterpret_cast(m_asserted_proxies.c_ptr()); } - - unsigned* get_core_size_ptr() { return &m_core_size; } - - Z3_ast* get_core_ptr() { - m_core.resize(m_asserted_proxies.size()); - if (m_core_size > m_core.size()) { - m_core_size = m_core.size(); - } - return m_core.c_ptr(); - } - - region& get_region() { return m_region; } - - - void set_print_success(bool b) { m_print_success = b; } - - void set_enable_cores() { m_enable_cores = true; } - - void unset_enable_cores() { m_enable_cores = false; } - - void update_param(char const* p, char const* v) { - Z3_update_param_value(m_context, p, v); - } - - bool get_enable_cores() const { return m_enable_cores; } - - void print_success() { - if (m_print_success) { - *m_out << "success\n"; - } - } - - void print_unsupported() { - *m_out << "unsupported\n"; - } - - void print_failure(char const* msg, proto_expr* expr) { - if (Z3_get_parameters(m_context).m_display_error_for_vs) { - if (msg[0] != 'Z' || msg[1] != '3') { - *m_out << "Z3"; - if (expr) { - *m_out << "(" << expr->line() << "," << expr->pos() << ")"; - } - *m_out << ": ERROR: "; - } - *m_out << msg; - if (msg[strlen(msg)-1] != '\n') { - *m_out << "\n"; - } - } - else { - *m_out << "(error \""; - if (expr) { - *m_out << "line " << expr->line() << " column " << expr->pos() << ": "; - } - *m_out << escaped(msg, true) << "\")\n"; -#ifndef _EXTERNAL_RELEASE - exit(ERR_PARSER); -#endif - } - } - - Z3_model* get_model_ptr() { - if (m_model) { - Z3_del_model(m_context, m_model); - m_model = 0; - } - return &m_model; - } - - Z3_model get_model() { return m_model; } - - Z3_ast* get_proof_ptr() { - m_proof = 0; - return &m_proof; - } - - void get_proof(std::ostream& out, proto_expr* p_expr) { - Z3_ast pr = m_proof; - if (pr) { - out << Z3_ast_to_string(m_context, pr) << "\n"; - } - else if (Z3_get_parameters(m_context).m_proof_mode == PGM_DISABLED) { - print_failure("proofs are disabled - enable them using the configuration PROOF_MODE={1,2}", p_expr); - } - else { - print_failure("there is no proof to display", p_expr); - } - } - - smt_cmd_token string2token(char const * str) { - str2token::entry * e = m_str2token.find_core(str); - if (e) - return e->get_data().m_value; - else - return SMT_CMD_ERROR; - } - - class scoped_stopwatch { - cmd_context& m_ctx; - bool m_first; - void (*m_old_handler)(int); - - static scoped_stopwatch* get_sw() { return static_cast(g_sw); } - - static void on_ctrl_c(int) { - if (get_sw()->m_first) { - Z3_soft_check_cancel(get_sw()->m_ctx.get_context()); - get_sw()->m_first = false; - } - else { - signal (SIGINT, get_sw()->m_old_handler); - raise (SIGINT); - } - } - public: - scoped_stopwatch(cmd_context& c) : m_ctx(c), m_first(true) { - g_sw = this; - c.m_watch.reset(); - c.m_watch.start(); - m_old_handler = signal(SIGINT, on_ctrl_c); // TBD: parallel? - } - ~scoped_stopwatch() { - m_ctx.m_watch.stop(); - if (m_old_handler != SIG_ERR) { - signal(SIGINT, m_old_handler); - } - } - }; - - //static scoped_stopwatch* g_sw = 0; - - double get_seconds() { - return m_watch.get_seconds(); - } - - bool get_command_help(std::ostream& out, smt_cmd_token tok) { - if (!m_is_command[tok]) { - return false; - } - out << " (" << m_token2str[tok]; - if (m_token2args[tok] && m_token2args[tok][0]) { - out << " " << m_token2args[tok]; - } - out << ")\n"; - out << " " << m_token2help[tok] << "\n\n"; - return true; - } - - void get_help(std::ostream& out) { - out << "\" available commands:\n\n"; - for (unsigned i = 0; i < m_token2args.size(); ++i) { - get_command_help(out, static_cast(i)); - } - get_info_help(out, " "); - out << "\n"; - set_option_help(out, " "); - out << "\""; - } - - bool get_info(smt_cmd_token tok) { - for (unsigned i = 0; i < m_infos.size(); ++i) { - if (m_infos[i].m_token == tok) { - get_out() << ":" << m_token2str[tok] << " "; - m_infos[i].m_action(*this); - return true; - } - } - return false; - } - - void get_info_help(std::ostream& strm, char const* line_start) { - for (unsigned i = 0; i < m_infos.size(); ++i) { - smt_cmd_token tok = m_infos[i].m_token; - strm << line_start << "(get-info " << m_token2str[tok]; - if (m_token2args[tok] && m_token2args[tok][0]) { - strm << " " << m_token2args[tok]; - } - strm << ")\n"; - strm << line_start << " " << m_token2help[tok] << "\n"; - } - } - - bool set_option(smt_cmd_token tok, proto_expr* const* chs) { - for (unsigned i = 0; i < m_options.size(); ++i) { - if (m_options[i].m_token == tok) { - return m_options[i].m_action(*this, chs); - } - } - return update_param_option(*this, chs-1); - // return false; - } - - bool set_info(proto_expr* e0, proto_expr* const* chs) { - proto_expr* e1 = chs[0]; - symbol s0, s1; - if (e0) - s0 = e0->string(); - if (e1) - s1 = e1->string(); - - if (s0 == symbol("status") && s1 == symbol("sat")) { - m_status = smtlib::benchmark::SAT; - } - else if (s0 == symbol("status") && s1 == symbol("unsat")) { - m_status = smtlib::benchmark::UNSAT; - } - else if (s0 == symbol("status") && s1 == symbol("unknown")) { - m_status = smtlib::benchmark::UNKNOWN; - } - else { -#ifdef Z3DEBUG - std::cout << s0 << " " << s1 << "\n"; -#endif - } - - // :source - // :smt-lib-version - // :category - // :status - // no-op - return true; - } - - void set_option_help(std::ostream& strm, char const* line_start) { - for (unsigned i = 0; i < m_options.size(); ++i) { - smt_cmd_token tok = m_options[i].m_token; - strm << line_start << "(set-option " << m_token2str[tok]; - if (m_token2args[tok] && m_token2args[tok][0]) { - get_out() << " " << m_token2args[tok]; - } - strm << ")\n"; - strm << line_start << " " << m_token2help[tok] << "\n"; - } - } - - unsigned parse_opt_numeral(proto_expr* e, unsigned default_value) { - if (e && e->kind() == proto_expr::INT) { - rational r = e->number(); - if (r.is_unsigned()) { - return r.get_unsigned(); - } - } - return default_value; - } - - bool parse_opt_bool(proto_expr* e, bool default_value) { - if (e && e->kind() == proto_expr::ID) { - if (strcmp(e->string().bare_str(), "true") == 0) { - return true; - } - if (strcmp(e->string().bare_str(), "false") == 0) { - return false; - } - } - return default_value; - } - - - void get_core(proto_expr* p_expr, std::ostream& out, - unsigned sz, expr** exprs, bool just_get_core) { - - - Z3_context ctx = get_context(); - Z3_lbool r; - scoped_stopwatch stopw(*this); - - if (get_enable_cores()) { - print_failure("cores should be disabled", p_expr); - return; - } - - for (unsigned i = 0; i < sz; ++i) { - if (!is_uninterp_const(exprs[i]) || !m_manager.is_bool(exprs[i])) { - print_failure("assumptions must be boolean constants (e.g., p1, p2, q1)", p_expr); - return; - } - } - - // set_enable_cores(); - // push(1); - // for (unsigned i = 0; i < sz; ++i) { - // add_asserted(exprs[i]); - // } - - unsigned max_core_size = sz; - unsigned core_size = sz; - m_core.reserve(max_core_size); - Z3_ast * core = m_core.c_ptr(); - - r = Z3_check_assumptions(ctx, sz, reinterpret_cast(exprs), - get_model_ptr(), get_proof_ptr(), - &core_size, core); - switch(r) { - case Z3_L_FALSE: - if (!just_get_core) - out << "unsat\n"; - print_core_as_is(out, core_size, core); - m_check_sat_state = state_unsat; - break; - case Z3_L_TRUE: - out << "sat\n"; - m_check_sat_state = state_sat; - break; - case Z3_L_UNDEF: - out << "unknown\n"; - m_check_sat_state = state_unknown; - break; - default: - throw default_exception("unexpected output of check-sat\n"); - break; - } - // unset_enable_cores(); - // pop(1); - } - - void check_sat(std::ostream& out) { - Z3_context ctx = get_context(); - Z3_lbool r; - scoped_stopwatch stopw(*this); - - if (get_enable_cores()) { - r = Z3_check_assumptions(ctx, get_num_assertions(), get_proxies_ptr(), - get_model_ptr(), get_proof_ptr(), - get_core_size_ptr(), get_core_ptr()); - - } - else if (Z3_get_parameters(ctx).m_proof_mode != PGM_DISABLED) { - unsigned core_size = 0; - Z3_ast core[1] = { 0 }; - r = Z3_check_assumptions(ctx, 0, 0, get_model_ptr(), get_proof_ptr(), &core_size, core); - } - else if (Z3_get_parameters(ctx).m_model) { - r = Z3_check_and_get_model(ctx, get_model_ptr()); - } - else { - r = Z3_check(ctx); - } - switch(r) { - case Z3_L_FALSE: - out << "unsat\n"; - m_check_sat_state = state_unsat; - break; - case Z3_L_TRUE: - out << "sat\n"; - m_check_sat_state = state_sat; - break; - case Z3_L_UNDEF: - out << "unknown\n"; - m_check_sat_state = state_unknown; - break; - default: - throw default_exception("unexpected output of check-sat\n"); - break; - } - - // check status (duplicate from smtlib_sover) - // smtlib_solver contains support for - // - spc - // - missing. - // - dumping statistics / proofs / model / labels - // - redundant given additional command-line options - // - switch(m_status) { - case smtlib::benchmark::SAT: - if (r == Z3_L_FALSE) { -#ifdef _EXTERNAL_RELEASE - std::cout << "unsat - check annotation which says sat\n"; -#else - std::cout << "BUG: unsoundness.\n"; - exit(ERR_UNSOUNDNESS); -#endif - } - else if (r == Z3_L_UNDEF) { -#ifndef _EXTERNAL_RELEASE - std::cout << "BUG: gaveup.\n"; - exit(ERR_UNKNOWN_RESULT); -#endif - } - break; - case smtlib::benchmark::UNSAT: - if (r == Z3_L_TRUE) { -#ifdef _EXTERNAL_RELEASE - std::cout << "sat - check annotation which says unsat\n"; -#else - std::cout << "BUG: incompleteness.\n"; - exit(ERR_INCOMPLETENESS); -#endif - } - else if (r == Z3_L_UNDEF) { -#ifndef _EXTERNAL_RELEASE - std::cout << "BUG: gaveup.\n"; - exit(ERR_UNKNOWN_RESULT); -#endif - } - break; - default: - break; - } - } - - void next_sat(std::ostream& out) { - Z3_context ctx = get_context(); - if (m_check_sat_state == state_sat || m_check_sat_state == state_unknown) { - Z3_literals lits = Z3_get_relevant_literals(ctx); - if (lits) { - Z3_block_literals(ctx, lits); - Z3_del_literals(ctx, lits); - } - } - check_sat(out); - } - - void get_sat_assertions(std::ostream& out) { - if (m_check_sat_state == state_unsat) { - out << "false\n"; - } - else { - Z3_ast assignment = Z3_get_context_assignment(m_context); - out << Z3_ast_to_string(m_context, reinterpret_cast(assignment)) << "\n"; - } - } - - void get_implied_equalities(std::ostream& out, unsigned num_exprs, expr* const* exprs) { - buffer class_ids(num_exprs, UINT_MAX); - Z3_lbool r = Z3_get_implied_equalities(m_context, - num_exprs, - (Z3_ast*) exprs, - class_ids.c_ptr()); - if (r == Z3_L_FALSE) { - out << "unsat\n"; - return; - } - out << "("; - for (unsigned i = 0; i < num_exprs; ++i) { - out << class_ids[i]; - if (i + 1 < num_exprs) { - out << " "; - } - } - out << ")\n"; - } - - void eval(std::ostream& out, proto_expr* p_expr, expr* e) { - Z3_model m = get_model(); - if (!m) { - print_failure("There is no model in the current context", p_expr); - return; - } - Z3_ast result = 0; - Z3_bool fully_simplified = Z3_eval(m_context, m, reinterpret_cast(e), &result); - if (!result) { - print_failure("Evaluation was not successful", p_expr); - return; - } - (void) fully_simplified; - out << Z3_ast_to_string(m_context, result) << "\n"; - } - - void eval(std::ostream& out, proto_expr* p_expr, unsigned num_args, expr*const* args) { - svector results; - Z3_model m = get_model(); - if (!m) { - print_failure("There is no model in the current context", p_expr); - return; - } - for (unsigned i = 0; i < num_args; ++i) { - Z3_ast result = 0; - Z3_bool fully_simplified = Z3_eval(m_context, m, reinterpret_cast(args[i]), &result); - if (!result) { - print_failure("Evaluation was not successful", p_expr); - return; - } - (void) fully_simplified; - results.push_back(result); - } - out << "("; - for (unsigned i = 0; i < num_args; ++i) { - out << Z3_ast_to_string(m_context, results[i]); - if (i + 1 < num_args) { - out << "\n"; - } - } - out << ")\n"; - } - - - - - void get_unsat_core(std::ostream& out, proto_expr* p_expr) { - if (!get_enable_cores()) { - print_failure("cores have not been enabled, use (set-option enable-cores)", p_expr); - return; - } - print_core(out); - } - - Z3_ast find_proxy(Z3_ast proxy) { - for (unsigned i = 0; i < m_asserted.size(); ++i) { - if (m_asserted_proxies[i] == (expr*)proxy) { - return reinterpret_cast(m_asserted[i].get()); - } - } - UNREACHABLE(); - return proxy; - } - - void print_core(std::ostream& out) { - unsigned csz = *get_core_size_ptr(); - out << "("; - for (unsigned i = 0; i < csz; ++i) { - out << Z3_ast_to_string(m_context, find_proxy(get_core_ptr()[i])); - if (i + 1 < csz) out << "\n"; - } - out << ")\n"; - } - - void print_core_as_is(std::ostream & out, unsigned csz, Z3_ast * core) { - out << "("; - for (unsigned i = 0; i < csz; ++i) { - out << Z3_ast_to_string(m_context, core[i]); - if (i + 1 < csz) out << " "; - } - out << ")\n"; - } - - void get_assertions(std::ostream& out) { - out << "("; - unsigned num_assertions = get_num_assertions(); - for (unsigned i = 0; i < num_assertions; ++i) { - out << Z3_ast_to_string(m_context, reinterpret_cast(get_assertion(i))); - if (i + 1 < num_assertions) out << "\n"; - } - out << ")\n"; - } - - bool has_error() { - return m_error_stream.tellp() > 0; - } - - void flush_errors() { - if (has_error()) { - m_error_stream.put(0); - print_failure(m_error_stream.str().c_str(), 0); - m_error_stream.seekp(0); - m_error_stream.clear(); - } - } - - std::ostream& get_error_stream() { - return m_error_stream; - } - -private: - - void add_command( - char const* name, - smt_cmd_token tok, - char const* args, - char const* help, - bool is_command = true - ) { - m_str2token.insert(name, tok); - if ((unsigned)tok >= m_token2str.size()) { - m_token2str.resize(tok+1); - m_token2help.resize(tok+1); - m_token2args.resize(tok+1); - m_is_command.resize(tok+1); - } - m_token2str[tok] = name; - m_token2help[tok] = help; - m_token2args[tok] = args; - m_is_command[tok] = is_command; - } - - void add_info( - char const* name, - smt_cmd_token t, - char const* args, - char const* help, - void (*action)(cmd_context&) - ) - { - add_command(name, t, args, help, false); - m_infos.push_back(cmd_info(t, action)); - } - - void add_option( - char const* name, - smt_cmd_token t, - char const* args, - char const* help, - bool (*action)(cmd_context&, proto_expr* const* exprs) - ) - { - add_command(name, t, args, help, false); - m_options.push_back(opt(t, action)); - } - - - static void name_info(cmd_context& ctx) { ctx.print_quoted("Z3"); } - - static void version_info(cmd_context& ctx) { - unsigned maj, min, bn, rn; - Z3_get_version(&maj,&min,&bn,&rn); - ctx.get_out() << "\"" << maj << "." << min << "-" << bn << "." << rn << "\""; - } - - static void authors_info(cmd_context& ctx) { ctx.print_quoted("Leonardo de Moura and Nikolaj Bjorner"); } - - static void last_failure_info(cmd_context& cmd_ctx) { - Z3_context ctx = cmd_ctx.get_context(); - Z3_search_failure sf = Z3_get_search_failure(ctx); - static char const * reasons[8] = { "no failure", "unknown", "timeout", "memout", - "user canceled", "exceeded conflict bound", - "incomplete theory support", - "formulas used quantifiers that may not have been instantiated fully" - }; - if (sf < 8) { - cmd_ctx.print_quoted(reasons[sf]); - } - else { - cmd_ctx.print_quoted("not documented"); - UNREACHABLE(); - } - } - - static void reason_unknown_info(cmd_context& cmd_ctx) { - Z3_context ctx = cmd_ctx.get_context(); - Z3_search_failure sf = Z3_get_search_failure(ctx); - - if (sf == 3) - cmd_ctx.print_quoted("memout"); - else - cmd_ctx.print_quoted("incomplete"); - } - - static void stats_info(cmd_context& cmd_ctx) { - cmd_ctx.get_out() << "\"" << escaped(Z3_statistics_to_string(cmd_ctx.get_context()), true) << "\""; - } - - static void model_info(cmd_context& cmd_ctx) { - Z3_context ctx = cmd_ctx.get_context(); - Z3_model m = cmd_ctx.get_model(); - if (m) { - if (Z3_get_parameters(ctx).m_model_v1_pp || Z3_get_parameters(ctx).m_model_v2_pp) { - cmd_ctx.get_out() << "\"" << escaped(Z3_model_to_string(ctx, m), true) << "\""; - } else { - cmd_ctx.get_out() << "(z3_model" << std::endl - << Z3_model_to_string(ctx, m) - << ")"; - } - } - else if (!Z3_get_parameters(ctx).m_model) { - cmd_ctx.print_quoted("models are disabled - enable them using the configuration MODEL=true"); - } - else { - cmd_ctx.print_quoted("there is no model at the current scope"); - } - } - - static void time_info(cmd_context& cmd_ctx) { - cmd_ctx.get_out() << cmd_ctx.get_seconds(); - } - - static void labels_info(cmd_context& cmd_ctx) { - std::ostream& out = cmd_ctx.get_out(); - Z3_context ctx = cmd_ctx.get_context(); - Z3_literals lits = Z3_get_relevant_labels(ctx); - unsigned sz = Z3_get_num_literals(ctx, lits); - if (sz > 0) { - out << "(z3_labels"; - for (unsigned i = 0; i < sz; ++i) { - out << " "; - out << Z3_get_symbol_string(ctx, Z3_get_label_symbol(ctx, lits, i)); - } - out << ")"; - } - Z3_del_literals(ctx, lits); - } - - static void help_info(cmd_context& cmd_ctx) { - cmd_ctx.get_help(cmd_ctx.get_out()); - } - - static bool print_success_option(cmd_context& cmd_ctx, proto_expr*const* chs) { - cmd_ctx.set_print_success(cmd_ctx.parse_opt_bool(chs?*chs:0, true)); - return true; - } - - static bool produce_models_option(cmd_context& cmd_ctx, proto_expr*const* chs) { - cmd_ctx.update_param("MODEL", cmd_ctx.parse_opt_bool(chs?*chs:0, true) ? "true" : "false"); - return true; - } - - static bool verbosity_option(cmd_context& cmd_ctx, proto_expr*const* chs) { - unsigned lvl = cmd_ctx.parse_opt_numeral(chs?*chs:0, 0); - set_verbosity_level(lvl); - return true; - } - - static bool output_channel_option(cmd_context& cmd_ctx, proto_expr*const* chs) { - cmd_ctx.set_out(chs?*chs:0); - return true; - } - - static bool enable_cores_option(cmd_context& cmd_ctx, proto_expr*const* chs) { - cmd_ctx.set_enable_cores(); - return true; - } - - static void print_parameters(cmd_context& cmd_ctx) { - front_end_params& p = Z3_get_parameters(cmd_ctx.m_context); - ini_params ini; - p.register_params(ini); - ini.display_params(cmd_ctx.get_out()); - } - - static void print_parameter_help(char const* param, cmd_context& cmd_ctx) { - front_end_params& p = Z3_get_parameters(cmd_ctx.m_context); - ini_params ini; - p.register_params(ini); - ini.display_parameter_help(param,cmd_ctx.get_out()); - } - - static bool update_param_option(cmd_context& cmd_ctx, proto_expr*const* chs) { - if (!chs) { - print_parameters(cmd_ctx); - return false; - } - if (chs[0] && !chs[1] && chs[0]->kind() == proto_expr::CONS) { - chs = chs[0]->children(); - } - - proto_expr* p = chs[0]; - proto_expr* v = chs[1]; - char const* p_string = 0; - char const*v_string = 0; - std::string v_str; - if (!p || (p->kind() != proto_expr::ID && p->kind() != proto_expr::STRING && p->kind() != proto_expr::ANNOTATION)) { - print_parameters(cmd_ctx); - return false; - } - p_string = p->string().bare_str(); - if (v && (v->kind() == proto_expr::INT || v->kind() == proto_expr::FLOAT)) { - v_str += v->number().to_string(); - v_string = v_str.c_str(); - } - else if (!v || (v->kind() != proto_expr::ID && v->kind() != proto_expr::STRING)) { - print_parameter_help(p->string().bare_str(), cmd_ctx); - return false; - } - else { - v_str = v->string().bare_str(); - if (v_str.length() > 2 && v_str[0] == '|' && v_str[v_str.length() - 1] == '|') { - // strip the quotes - v_str = v_str.substr(1, v_str.length() - 2); - } - v_string = v_str.c_str(); - } - // hack for generating warning message when trying to set PROOF_MODE inside the command context. - if (strcmp(p_string, "PROOF_MODE") == 0) { - warning_msg("PROOF_MODE can only be set as a command line option when invoking z3.exe (e.g., \"z3.exe PROOF_MODE=2 file.smt2\"), or when creating a fresh logical context using the Z3 API."); - return false; - } - cmd_ctx.update_param(p_string, v_string); - return true; - } - - static bool set_verbose_output_channel_option(cmd_context& cmd_ctx, proto_expr*const* chs) { - cmd_ctx.m_verbose.reset(chs?(*chs):0); - set_verbose_stream(*cmd_ctx.m_verbose); - return true; - } -}; - - class smtparser : public parser { struct builtin_op { family_id m_family_id; @@ -1922,7 +585,6 @@ class smtparser : public parser { symbol m_notes; symbol m_theory; symbol m_language; - symbol m_extensions; symbol m_array; symbol m_bang; symbol m_underscore; @@ -1932,8 +594,6 @@ class smtparser : public parser { family_id m_arith_fid; family_id m_array_fid; family_id m_rel_fid; - datatype_decl_plugin * m_dt_plugin; - datatype_util m_dt_util; func_decl * m_sk_hack; std::ostream* m_err; bool m_display_error_for_vs; @@ -1968,12 +628,9 @@ public: m_notes("notes"), m_theory("theory"), m_language("language"), - m_extensions("extensions"), m_array("array"), m_bang("!"), m_underscore("_"), - m_dt_plugin(0), - m_dt_util(m), m_err(0), m_display_error_for_vs(false) { @@ -2024,45 +681,6 @@ public: return parse_stream(is); } - bool parse_commands(Z3_context ctx, std::istream& is, std::ostream& os) { - set_error_stream(os); - cmd_context context(m_manager, ctx, is, os); - set_error_stream(context.get_error_stream()); - proto_region proto_region; - scanner scanner(is, context.get_error_stream(), true); - proto_expr_parser parser(proto_region, scanner, context.get_error_stream()); - - m_display_error_for_vs = Z3_get_parameters(ctx).m_display_error_for_vs; - - ptr_vector exprs; - while (!parser.at_eof()) { - proto_region.reset(); - exprs.reset(); - if (!parser.parse(exprs, true)) { - context.flush_errors(); - context.get_out().flush(); - break; - } - if (exprs.empty()) { - break; - } - SASSERT(exprs.size() == 1); - try { - if (!process_command(context, exprs.back())) { - break; - } - } - catch(cmd_exn(ex)) { - context.flush_errors(); - context.get_out().flush(); - context.print_failure(Z3_get_error_msg(ex.get()), exprs.back()); - } - context.flush_errors(); - context.get_out().flush(); - } - return true; - } - void add_builtin_op(char const * s, family_id fid, decl_kind k) { m_builtin_ops.insert(symbol(s), builtin_op(fid, k)); } @@ -2072,15 +690,6 @@ public: } void initialize_smtlib() { - - if (!m_dt_plugin) { - family_id fid = m_manager.get_family_id("datatype"); - if (!m_manager.has_plugin(fid)) { - m_manager.register_plugin(fid, alloc(datatype_decl_plugin)); - } - m_dt_plugin = static_cast(m_manager.get_plugin(fid)); - } - smtlib::symtable* table = m_benchmark.get_symtable(); symbol arith("arith"); @@ -2253,9 +862,6 @@ private: symbol extrasorts("extrasorts"); symbol extrafuns("extrafuns"); symbol extrapreds("extrapreds"); - symbol datatypes("datatypes"); - symbol unify("unify"); - symbol unify_fail("unify-fail"); symbol assumption("assumption"); symbol assumption_core("assumption-core"); symbol define_sorts_sym("define_sorts"); @@ -2391,20 +997,6 @@ private: ++proto_exprs; continue; } - if (datatypes == e->string() && e1) { - if (!declare_datatypes(e1)) { - return false; - } - ++proto_exprs; - continue; - } - if ((unify == e->string() || unify_fail == e->string()) && e1) { - if (!test_unify(e1, unify == e->string())) { - return false; - } - ++proto_exprs; - continue; - } if (m_notes == e->string() && e1) { ++proto_exprs; continue; @@ -2442,549 +1034,6 @@ private: expr->kind() == proto_expr::ANNOTATION); } - smt_cmd_token get_command_token(cmd_context& ctx, proto_expr* expr) { - if (!expr) { - return SMT_CMD_ERROR; - } - if (!is_id_token(expr)) { - return SMT_CMD_ERROR; - } - return ctx.string2token(expr->string().bare_str()); - } - - bool process_command(cmd_context& cmd_ctx, proto_expr* p_expr) { - proto_expr* const* chs = p_expr->children(); - proto_expr* e0 = chs?chs[0]:0; - proto_expr* e1 = e0?chs[1]:0; - std::ostream& out = cmd_ctx.get_out(); - Z3_context ctx = cmd_ctx.get_context(); - - smt_cmd_token cmd_tok; - if (p_expr->kind() == proto_expr::ID) { - cmd_tok = get_command_token(cmd_ctx, p_expr); - } - else { - cmd_tok = get_command_token(cmd_ctx, e0); - } - - switch(cmd_tok) { - case SMT_CMD_SET_LOGIC: - if (!check_id(e1)) { - cmd_ctx.print_failure("logic identifier expected as argument to logic", p_expr); - break; - } - if (Z3_set_logic(ctx, e1->string().bare_str())) { - // m_smtlib_logic param is only used for pretty printing. - Z3_get_parameters(ctx).m_smtlib_logic = e1->string().bare_str(); - set_default_num_sort(e1->string()); - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("failed to set logic", p_expr); - } - break; - case SMT_CMD_DECLARE_SORTS: - if (!check_valid(cmd_ctx, p_expr, e1, "sort declaration expects an argument")) { - break; - } - if (e0 && e1 && chs[2]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (declare_sorts(e1)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse sort declaration", p_expr); - } - break; - case SMT_CMD_DECLARE_FUNS: // func-decls - if (!check_valid(cmd_ctx, p_expr, e1, "function declaration expects an argument")) { - break; - } - if (e0 && e1 && chs[2]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (declare_funs(e1)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse function declaration", p_expr); - } - break; - case SMT_CMD_DECLARE_PREDS: // pred-decls - if (!check_valid(cmd_ctx, p_expr, e1, "predicate declaration expects an argument")) { - break; - } - if (e0 && e1 && chs[2]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (declare_preds(e1)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse predicate declaration", p_expr); - } - break; - case SMT_CMD_DECLARE_DATATYPES: - if (!check_valid(cmd_ctx, p_expr, e1, "data-type declaration expects an argument")) { - break; - } - if (e0 && e1 && chs[2]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (declare_datatypes(e1)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse data-type declaration", p_expr); - } - break; - case SMT_CMD_DEFINE: { - expr_ref macro_expr(m_manager); - if (define_macro(cmd_ctx.get_table(), cmd_ctx.get_region(), p_expr, macro_expr)) { - cmd_ctx.add_trail(macro_expr); - cmd_ctx.print_success(); - } - break; - } - case SMT_CMD_DEFINE_SORTS: { - if (!check_valid(cmd_ctx, p_expr, e1, "sort definition expects an argument")) { - break; - } - if (e0 && e1 && chs[2]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (define_sorts(e1)) { - cmd_ctx.print_success(); - } - break; - } - case SMT_CMD_DECLARE_SORT: { // - if (!check_id(e1)) { - cmd_ctx.print_failure("identifier argument expected", p_expr); - break; - - } - unsigned num_args = cmd_ctx.parse_opt_numeral(chs[2], 0); - if (e0 && e1 && chs[2] && chs[3]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - m_benchmark.get_symtable()->insert(e1->string(), alloc(user_sort, m_manager, num_args, e1->string())); - cmd_ctx.print_success(); - - break; - } - case SMT_CMD_DEFINE_SORT: { // (*) - if (!check_id(e1)) { - cmd_ctx.print_failure("sort definition expects three arguments", p_expr); - break; - } - proto_expr* e2 = chs[2]; - if (!check_valid(cmd_ctx, p_expr, e2, "sort definition expects three arguments")) { - break; - } - proto_expr* e3 = chs[3]; - if (!check_valid(cmd_ctx, p_expr, e3, "sort definition expects three arguments")) { - break; - } - if (chs[4]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (define_sort(e1, e2, e3)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse sort definition", p_expr); - } - break; - } - case SMT_CMD_DECLARE_FUN: { // (*) - if (!check_id(e1)) { - cmd_ctx.print_failure("function declaration expects three arguments", p_expr); - break; - } - proto_expr* e2 = chs[2]; - if (!check_valid(cmd_ctx, p_expr, e2, "function declaration expects three arguments")) { - break; - } - proto_expr* e3 = chs[3]; - if (!check_valid(cmd_ctx, p_expr, e3, "function declaration expects three arguments")) { - break; - } - if (chs[4]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (declare_fun(e1,e2,e3)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse function declaration", p_expr); - } - break; - } - case SMT_CMD_DECLARE_CONST: { // - if (!check_id(e1)) { - cmd_ctx.print_failure("constant declaration expects two arguments", p_expr); - break; - } - proto_expr* e2 = chs[2]; - if (!check_valid(cmd_ctx, p_expr, e2, "constant declaration expects two arguments")) { - break; - } - if (chs[3]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - if (declare_fun(e1, 0, e2)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse constant declaration", p_expr); - } - break; - } - case SMT_CMD_DEFINE_FUN: { // (*) - if (!check_id(e1)) { - cmd_ctx.print_failure("function definition expects four arguments", p_expr); - break; - } - proto_expr* e2 = chs[2]; - if (!check_valid(cmd_ctx, p_expr, e2, "function definition expects four arguments")) { - break; - } - proto_expr* e3 = chs[3]; - if (!check_valid(cmd_ctx, p_expr, e3, "function definition expects four arguments")) { - break; - } - proto_expr* e4 = chs[4]; - if (!check_valid(cmd_ctx, p_expr, e4, "function definition expects four arguments")) { - break; - } - if (chs[5]) { - cmd_ctx.print_failure("too many arguments passed to declaration", p_expr); - } - expr_ref macro_expr(m_manager); - if (define_fun(cmd_ctx.get_table(), cmd_ctx.get_region(), e1, e2, e3, e4, macro_expr)) { - cmd_ctx.add_trail(macro_expr); - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_failure("could not parse function definition", p_expr); - } - break; - } - case SMT_CMD_GET_VALUE: { // (+) - if (!check_valid(cmd_ctx, p_expr, e1, "get-value expects a list arguments")) { - break; - } - proto_expr* const* children = e1->children(); - expr_ref_vector exprs(m_manager); - - while (children && children[0]) { - expr_ref e(m_manager); - if (!get_expression(cmd_ctx, cmd_ctx.get_table(), p_expr, children[0], e, "one expression expected to eval")) { - break; - } - exprs.push_back(e); - ++children; - } - cmd_ctx.eval(out, p_expr, exprs.size(), exprs.c_ptr()); - break; - } - case SMT_CMD_PUSH: { // numeral - unsigned num_scopes = cmd_ctx.parse_opt_numeral(e1, 1); - cmd_ctx.push(num_scopes); - cmd_ctx.print_success(); - if (e1 && chs[2]) { - cmd_ctx.print_failure("too many arguments passed to command", p_expr); - } - break; - } - case SMT_CMD_POP: { // numeral - unsigned num_scopes = cmd_ctx.parse_opt_numeral(e1, 1); - cmd_ctx.pop(num_scopes); - cmd_ctx.print_success(); - if (e1 && chs[2]) { - cmd_ctx.print_failure("too many arguments passed to command", p_expr); - } - break; - } - case SMT_CMD_ASSERT: { // expr+ - expr_ref_vector exprs(m_manager); - if (!chs) { - cmd_ctx.print_failure("expecting list of arguments", p_expr); - break; - } - if (!(*chs)) { - cmd_ctx.print_success(); - break; - } - ++chs; - if (!make_bool_expressions(cmd_ctx.get_table(), chs, exprs)) { - if (!cmd_ctx.has_error()) { - cmd_ctx.print_failure("could not parse expression", *chs); - } - return true; - } - for (unsigned i = 0; i < exprs.size(); ++i) { - cmd_ctx.add_asserted(exprs[i].get()); - } - cmd_ctx.print_success(); - break; - } - case SMT_CMD_CHECK_SAT: { // boolean-constants* - if (!chs || !(*chs)) { - cmd_ctx.check_sat(out); - } - else { - ++chs; - if (!chs || !(*chs)) { - cmd_ctx.check_sat(out); - } - else { - expr_ref_vector exprs(m_manager); - if (!make_bool_expressions(cmd_ctx.get_table(), chs, exprs)) { - if (!cmd_ctx.has_error()) { - cmd_ctx.print_failure("could not parse expression", *chs); - } - return true; - } - cmd_ctx.get_core(p_expr, out, exprs.size(), exprs.c_ptr(), false); - } - } - break; - } - case SMT_CMD_GET_CORE: { // boolean-constants+ - expr_ref_vector exprs(m_manager); - if (!chs) { - cmd_ctx.print_failure("expecting list of arguments", p_expr); - break; - } - if (!(*chs)) { - cmd_ctx.print_success(); - break; - } - ++chs; - if (!make_bool_expressions(cmd_ctx.get_table(), chs, exprs)) { - if (!cmd_ctx.has_error()) { - cmd_ctx.print_failure("could not parse expression", *chs); - } - return true; - } - cmd_ctx.get_core(p_expr, out, exprs.size(), exprs.c_ptr(), true); // just get the core - break; - } - case SMT_CMD_NEXT_SAT: { // - cmd_ctx.next_sat(out); - break; - } - case SMT_CMD_SIMPLIFY: { - expr_ref e(m_manager); - if (!get_expression(cmd_ctx, cmd_ctx.get_table(), p_expr, e1, e, "one expression expected to simplify")) { - break; - } - cmd_context::scoped_stopwatch stopw(cmd_ctx); - Z3_ast result = Z3_simplify(ctx, reinterpret_cast(e.get())); - out << Z3_ast_to_string(ctx, result) << "\n"; - break; - } - case SMT_CMD_GET_IMPLIED_EQUALITIES: { - expr_ref_vector exprs(m_manager); - expr_ref e(m_manager); - if (!chs || !(*chs)) { - cmd_ctx.print_failure("expecting list of arguments", p_expr); - break; - } - ++chs; - bool ok = true; - while (*chs) { - if (!get_expression(cmd_ctx, cmd_ctx.get_table(), p_expr, *chs, e, "list of expressions expected")) { - ok = false; - break; - } - exprs.push_back(e); - ++chs; - } - if (!ok) { - break; - } - cmd_context::scoped_stopwatch stopw(cmd_ctx); - cmd_ctx.get_implied_equalities(out, exprs.size(), exprs.c_ptr()); - break; - } - case SMT_CMD_EVAL: { - expr_ref e(m_manager); - if (!get_expression(cmd_ctx, cmd_ctx.get_table(), p_expr, e1, e, "one expression expected to eval")) { - break; - } - cmd_ctx.eval(out, p_expr, e); - break; - } - case SMT_CMD_GET_ASSERTIONS: { // string - scoped_stream strm(e1, out); - cmd_ctx.get_assertions(*strm); - break; - } - case SMT_CMD_GET_SAT_ASSERTIONS: { // string - scoped_stream strm(e1, out); - cmd_ctx.get_sat_assertions(out); - break; - } - case SMT_CMD_KEEP_SAT_ASSERTIONS: { // - Z3_ast assignment = Z3_get_context_assignment(ctx); - cmd_ctx.add_asserted(reinterpret_cast(assignment)); - cmd_ctx.print_success(); - break; - } - case SMT_CMD_GET_UNSAT_CORE: { // string - scoped_stream strm(e1, out); - cmd_ctx.get_unsat_core(out, p_expr); - break; - } - case SMT_CMD_GET_PROOF: { // string - scoped_stream strm(e1, out); - cmd_ctx.get_proof(*strm, p_expr); - break; - } - case SMT_CMD_SET_OPTION: { // string strings - if (!e1) { - cmd_ctx.set_option_help(out, ""); - break; - } - if (cmd_ctx.set_option(get_command_token(cmd_ctx,e1), chs+2)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_unsupported(); - } - break; - } - case SMT_CMD_SET_INFO: { - if (!e1) { - cmd_ctx.set_option_help(out, ""); - break; - } - if (cmd_ctx.set_info(e1, chs+2)) { - cmd_ctx.print_success(); - } - else { - cmd_ctx.print_unsupported(); - } - break; - } - case SMT_CMD_GET_INFO: { // string+ - if (!e1) { - cmd_ctx.get_info_help(out, ""); - break; - } - ++chs; - SASSERT(e1 == *chs); - out << "("; - while(*chs) { - if (!get_info(cmd_ctx, get_command_token(cmd_ctx,*chs))) { - out << ":" << chs[0]->string() << " \"unsupported\""; - } - ++chs; - if (*chs) { - out << "\n"; - } - } - out << ")\n"; - break; - } - case SMT_CMD_ECHO: { // string+ - if (!e1) { - cmd_ctx.get_info_help(out, ""); - break; - } - ++chs; - SASSERT(e1 == *chs); - while(*chs) { - out << chs[0]->string() << "\n"; - ++chs; - } - break; - } - case SMT_CMD_EXIT: // - return false; - case SMT_CMD_ERROR: // error token - cmd_ctx.print_failure("unrecognized command", p_expr); - break; - default: - if (get_info(cmd_ctx, cmd_tok)) { - out << "\n"; - break; - } - if (cmd_ctx.get_command_help(out, cmd_tok)) { - out << "\n"; - break; - } - cmd_ctx.print_failure("this is not a top-level command", p_expr); - break; - } - return true; - } - - void flatten_exprs(expr_ref_vector& exprs) { - for (unsigned i = 0; i < exprs.size(); ++i) { - expr* e = exprs[i].get(); - if (m_manager.is_and(e)) { - for (unsigned j = 1; j < to_app(e)->get_num_args(); ++j) { - exprs.push_back(to_app(e)->get_arg(j)); - } - exprs[i] = to_app(e)->get_arg(0); - --i; - continue; - } - if (m_manager.is_not(e) && - m_manager.is_or(to_app(e)->get_arg(0))) { - e = to_app(e)->get_arg(0); - app* a = to_app(e); - for (unsigned j = 1; j < a->get_num_args(); ++j) { - e = a->get_arg(j); - if (m_manager.is_not(e)) { - exprs.push_back(to_app(e)->get_arg(0)); - } - else { - exprs.push_back(m_manager.mk_not(e)); - } - } - e = a->get_arg(0); - if (m_manager.is_not(e)) { - exprs[i] = to_app(e)->get_arg(0); - } - else { - exprs[i] = m_manager.mk_not(e); - } - --i; - continue; - } - } - } - - - bool get_info(cmd_context& cmd_ctx, smt_cmd_token cmd_tok) { - return cmd_ctx.get_info(cmd_tok); - } - - bool get_expression(cmd_context& cmd_ctx, symbol_table& table, proto_expr* p_expr, proto_expr* e1, expr_ref& e, char const* msg) { - if (!check_valid(cmd_ctx, p_expr, e1, msg)) { - return false; - } - m_binding_level = 0; - if (!make_expression(table, e1, e)) { - return false; - } - return true; - } - - - bool check_valid(cmd_context& cmd_ctx, proto_expr* p_expr, proto_expr* e, char const* msg) { - if (e == 0) { - cmd_ctx.print_failure(msg, p_expr); - } - return (e != 0); - } - bool check_id(proto_expr* e) { return is_id_token(e); } @@ -4088,186 +2137,6 @@ private: return true; } - bool declare_datatypes(proto_expr * e) { - TRACE("datatypes", tout << "new datatype declarion section\n";); - proto_expr * const* children = e->children(); - - buffer dt_names; - - while (children && *children) { - proto_expr * type_decl = *children; - proto_expr * const* td_children = type_decl->children(); - if (!td_children || !td_children[0] || !(td_children[0]->kind() == proto_expr::ID)) { - set_error("invalid datatype declaration", type_decl); - return false; - } - symbol name = td_children[0]->string(); - sort * dummy; - if (m_benchmark.get_symtable()->find(name, dummy)) { - set_error("invalid datatype declaration, name was already used", type_decl); - return false; - } - dt_names.push_back(name); - TRACE("datatypes", tout << name << "\n";); - ++children; - } - - children = e->children(); - - ptr_buffer datatypes; - - while (children && *children) { - datatype_decl * d = declare_datatype(*children, dt_names); - if (!d) { - return false; - } - datatypes.push_back(d); - ++children; - } - - sort_ref_vector new_types(m_manager); - - bool result = m_dt_plugin->mk_datatypes(datatypes.size(), datatypes.c_ptr(), new_types); - del_datatype_decls(datatypes.size(), datatypes.c_ptr()); - - if (!result) { - set_error("invalid datatype declaration", e); - } - else { - unsigned num_types = new_types.size(); - for (unsigned i = 0; i < num_types; i++) { - sort * d = new_types.get(i); - TRACE("datatype", tout << "new datatype\n" << mk_pp(d, m_manager) << "\n"; - tout << "num. elements: " << d->get_num_elements() << "\n"; - tout << "recursive: " << m_dt_util.is_recursive(d) << "\n"; - tout << "non_rec constructor: " << m_dt_util.get_non_rec_constructor(d)->get_name() << "\n"; - ); - m_benchmark.insert(d); - ptr_vector const * constructors = m_dt_util.get_datatype_constructors(d); - unsigned num_constructors = constructors->size(); - for (unsigned j = 0; j < num_constructors; j++) { - func_decl * c = constructors->get(j); - m_benchmark.insert(c); - func_decl * r = m_dt_util.get_constructor_recognizer(c); - TRACE("datatype", - tout << "new constructor\n" << mk_pp(c, m_manager) << "\n"; - tout << "new recogniser\n" << mk_pp(r, m_manager) << "\n";); - m_benchmark.insert(r); - ptr_vector const * accessors = m_dt_util.get_constructor_accessors(c); - unsigned num_accessors = accessors->size(); - for (unsigned k = 0; k < num_accessors; k++) { - func_decl * a = accessors->get(k); - TRACE("datatype", tout << "new accessor\n" << mk_pp(a, m_manager) << "\n";); - m_benchmark.insert(a); - } - } - } - } - - return result; - } - - datatype_decl * declare_datatype(proto_expr * e, buffer const & dt_names) { - proto_expr* const * children = e->children(); - symbol const& name = children[0]->string(); - - ptr_buffer constructors; - ++children; // consume id - - while (children && *children) { - constructor_decl * c = declare_constructor(*children, dt_names); - if (!c) { - del_constructor_decls(constructors.size(), constructors.c_ptr()); - return 0; - } - constructors.push_back(c); - ++children; - } - - if (constructors.size() == 0) { - set_error("datatype must have at least one constructor", e); - return 0; - } - - return mk_datatype_decl(name, constructors.size(), constructors.c_ptr()); - } - - constructor_decl * declare_constructor(proto_expr * e, buffer const & dt_names) { - if (e->kind() == proto_expr::ID) { - symbol const & name = e->string(); - string_buffer<> tmp; - tmp << "is_" << name; - symbol r_name(tmp.c_str()); - return mk_constructor_decl(name, r_name, 0, 0); - } - - proto_expr* const * children = e->children(); - if (!children || !children[0] || !(children[0]->kind() == proto_expr::ID)) { - set_error("invalid constructor declaration", e); - return 0; - } - - symbol const & name = children[0]->string(); - string_buffer<> tmp; - tmp << "is_" << name; - symbol r_name(tmp.c_str()); - - ptr_buffer accessors; - ++children; // skip id - - while (children && *children) { - accessor_decl * d = declare_accessor(*children, dt_names); - if (!d) { - del_accessor_decls(accessors.size(), accessors.c_ptr()); - return 0; - } - accessors.push_back(d); - ++children; - } - - return mk_constructor_decl(name, r_name, accessors.size(), accessors.c_ptr()); - } - - accessor_decl * declare_accessor(proto_expr * e, buffer const & dt_names) { - proto_expr* const * children = e->children(); - if (!children || - !children[0] || !(children[0]->kind() == proto_expr::ID) || - !children[1] || !(children[1]->kind() == proto_expr::ID) || - children[2]) { - set_error("invalid accessor declaration", e); - return 0; - } - - symbol const& name = children[0]->string(); - symbol const& tname = children[1]->string(); - unsigned tid = 0; - for (; tid < dt_names.size(); tid++) { - if (tname == dt_names[tid]) { - break; - } - } - - type_ref ty; - if (tid < dt_names.size()) { - ty = type_ref(tid); - } - else { - sort_ref s(m_manager); - if (!make_sort(tname, children[1]->num_params(), children[1]->params(), s)) { - set_error("unknown sort", children[1]); - return 0; - } - m_pinned_sorts.push_back(s); - ty = type_ref(s.get()); - } - - return mk_accessor_decl(name, ty); - } - - // - // (define-macro (name (x A) (y B)) body[x,y]) - // - bool can_be_sorted_var(proto_expr* e) { return e && @@ -4351,133 +2220,6 @@ private: return true; } - - - bool define_fun(symbol_table& table, region& r, proto_expr* name, proto_expr* args, - proto_expr* srt, proto_expr* body, expr_ref & macro_expr) { - - symbol macro_name = name->string(); - - proto_expr* const* chs = args->children(); - // parse marco arguments. - table.begin_scope(); - ptr_vector sorts; - sort_ref sort1(m_manager), sort2(m_manager); - while (chs && *chs) { - proto_expr* e1 = *chs; - if (!can_be_sorted_var(e1)) { - set_error("Macro definition takes a list of pairs", e1); - goto error_cleanup; - } - proto_expr* var = e1->children()[0]; - proto_expr* srt = e1->children()[1]; - sort_ref sort(m_manager); - if (!make_sort(srt, sort)) { - goto error_cleanup; - } - sorts.push_back(sort); - m_pinned_sorts.push_back(sort); - table.insert(var->string(), new (r) bound_var(this, sort)); - ++chs; - ++m_binding_level; - } - - if (!make_expression(table, body, macro_expr)) { - goto error_cleanup; - } - - if (!make_sort(srt, sort1)) { - goto error_cleanup; - } - sort2 = m_manager.get_sort(macro_expr); - if (sort1.get() != sort2.get()) { - std::ostringstream strm; - strm << "The expected sort for macro was " << mk_pp(sort1, m_manager) - << " but the macro body has sort " << mk_pp(sort2, m_manager); - set_error(strm.str().c_str(), body); - goto error_cleanup; - } - table.end_scope(); - m_binding_level = 0; - table.insert(macro_name, new (r) macro_builder(r, body, macro_expr, this, sorts.size(), sorts.c_ptr())); - return true; - - error_cleanup: - table.end_scope(); - m_binding_level = 0; - return false; - } - - bool define_macro(symbol_table& table, region& r, proto_expr* macro_defn, expr_ref & macro_expr) { - SASSERT(macro_defn); - proto_expr* const* exprs = macro_defn->children(); - proto_expr* e0 = exprs?exprs[0]:0; - proto_expr* e1 = e0?exprs[1]:0; - proto_expr* e2 = e1?exprs[2]:0; - - m_binding_level = 0; - - if (!e1) { - set_error("macro definition requires two arguments, none given", macro_defn); - return false; - } - if (!e2) { - set_error("macro definition requires two arguments, only one given", macro_defn); - return false; - } - - // parse macro name - symbol macro_name; - proto_expr* const* chs = e1->children(); - if (e1->kind() == proto_expr::ID) { - macro_name = e1->string(); - chs = 0; - } - else if (chs && chs[0] && chs[0]->kind() == proto_expr::ID) { - macro_name = chs[0]->string(); - chs = chs + 1; - } - else { - set_error("first argument to macro definition should be a name or a name applied to arguments", e1); - return false; - } - - // parse marco arguments. - table.begin_scope(); - ptr_vector sorts; - while (chs && *chs) { - e1 = *chs; - if (!can_be_sorted_var(e1)) { - set_error("Macro definition takes a list of pairs", e1); - goto error_cleanup; - } - proto_expr* var = e1->children()[0]; - proto_expr* srt = e1->children()[1]; - sort_ref sort(m_manager); - if (!make_sort(srt, sort)) { - goto error_cleanup; - } - sorts.push_back(sort); - m_pinned_sorts.push_back(sort); - table.insert(var->string(), new (r) bound_var(this, sort)); - ++chs; - ++m_binding_level; - } - - if (!make_expression(table, e2, macro_expr)) { - goto error_cleanup; - } - table.end_scope(); - m_binding_level = 0; - table.insert(macro_name, new (r) macro_builder(r, e2, macro_expr, this, sorts.size(), sorts.c_ptr())); - return true; - - error_cleanup: - table.end_scope(); - m_binding_level = 0; - return false; - } - void fix_parameters(unsigned num_params, parameter* params) { for (unsigned i = 0; i < num_params; ++i) { func_decl* d = 0; @@ -4495,76 +2237,6 @@ private: } } - bool test_unify(proto_expr * e, bool expected) { - proto_expr* const * children = e->children(); - if (!children || !children[0] || !children[1]) { - set_error("invalid unification problem", e); - } - - expr_ref f1(m_manager), f2(m_manager); - if (!make_expression(children[0], f1) || !make_expression(children[1], f2)) - return false; - unsigned num_vars1 = 0; - unsigned num_vars2 = 0; - if (is_forall(f1)) { - num_vars1 = to_quantifier(f1)->get_num_decls(); - f1 = to_quantifier(f1)->get_expr(); - } - if (is_forall(f2)) { - num_vars2 = to_quantifier(f2)->get_num_decls(); - f2 = to_quantifier(f2)->get_expr(); - } - substitution s(m_manager); - s.reserve(2, std::max(num_vars1, num_vars2)); - unifier u(m_manager); - if (u(f1, f2, s)) { - std::cout << "unification: succeeded\n"; - if (!expected) { - get_err() << "WRONG ANSWER\n"; - UNREACHABLE(); - } - unsigned deltas[2] = { 0, num_vars1 }; - s.display(std::cout, 2, deltas); - } - else { - std::cout << "unification: failed\n"; - if (expected) { - get_err() << "WRONG ANSWER\n"; - UNREACHABLE(); - } - } - return true; - } - - void dump_substitution(expr_ref_buffer & s) { - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = s[i]; - if (t) - std::cout << "VAR " << i << " -->\n" << mk_pp(t, m_manager) << "\n"; - } - } - - bool declare_axioms(proto_expr * e) { - proto_expr* const * children = e->children(); - while (children && *children) { - if (!declare_axiom(*children)) { - return false; - } - ++children; - } - return true; - } - - bool declare_axiom(proto_expr * e) { - expr_ref t(m_manager); - if (!make_expression(e, t) || - !push_assumption(t.get())) { - return false; - } - return true; - } - bool make_app(proto_expr * proto_expr, expr_ref_vector const & args, expr_ref & result) { symbol const& name = proto_expr->string(); ptr_vector sorts; @@ -4641,49 +2313,6 @@ private: } }; - class macro_builder : public idbuilder { - proto_expr* m_p_expr; - expr* m_expr; - smtparser* m_parser; - unsigned m_num_sorts; - sort** m_sorts; - public: - macro_builder(region& r, proto_expr* p_expr, expr* e, smtparser* p, unsigned num_sorts, sort* const* sorts) : - m_p_expr(p_expr), m_expr(e), m_parser(p), m_num_sorts(num_sorts) { - m_sorts = new (r) sort*[num_sorts]; - for (unsigned i = 0; i < num_sorts; ++i) { - m_sorts[i] = sorts[i]; - } - } - - virtual bool apply(expr_ref_vector const& args, expr_ref& result) { - ast_manager& m = m_parser->m_manager; - if (args.size() != m_num_sorts) { - m_parser->set_error("wrong number of arguments passed to macro", m_p_expr); - return false; - } - for (unsigned i = 0; i < m_num_sorts; ++i) { - if (m_sorts[i] != m.get_sort(args[i])) { - std::ostringstream strm; - strm << "sort miss-match for argument of macro. Expecting sort: "; - strm << mk_pp(m_sorts[i], m) << " instead argument "; - strm << mk_pp(args[i], m) << " with sort "; - strm << mk_pp(m.get_sort(args[i]), m); - m_parser->set_error(strm.str().c_str(), m_p_expr); - return false; - } - } - if (m_num_sorts == 0) { - result = m_expr; - } - else { - var_subst subst(m); - subst(m_expr, args.size(), args.c_ptr(), result); - } - return true; - } - }; - class identity : public idbuilder { public: identity() {} diff --git a/src/api/smtparser.h b/src/api/smtparser.h index 6750471a8..d593f3f05 100644 --- a/src/api/smtparser.h +++ b/src/api/smtparser.h @@ -42,8 +42,6 @@ namespace smtlib { virtual bool parse_file(char const * path) = 0; virtual bool parse_string(char const * string) = 0; - virtual bool parse_commands(Z3_context ctx, std::istream& is, std::ostream& os) = 0; - virtual benchmark * get_benchmark() = 0; }; };