From 95a25265f26cc23bd952045e4ee947cab8e2eeb0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 17:18:41 -0700 Subject: [PATCH] removed native low level parser Signed-off-by: Leonardo de Moura --- src/api/api_parsers.cpp | 35 - src/api/z3_api.h | 17 - src/api/z3_solver.cpp | 1304 -------------------------------- src/api/z3_solver.h | 1007 ------------------------ src/bindings/dotnet/Context.cs | 24 - 5 files changed, 2387 deletions(-) delete mode 100644 src/api/z3_solver.cpp delete mode 100644 src/api/z3_solver.h diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index d74ade1a7..03e947c8a 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -23,7 +23,6 @@ Revision History: #include"cmd_context.h" #include"smt2parser.h" #include"smtparser.h" -#include"z3_solver.h" extern "C" { @@ -248,40 +247,6 @@ extern "C" { return mk_c(c)->m_smtlib_error_buffer.c_str(); Z3_CATCH_RETURN(""); } - - Z3_ast parse_z3_stream(Z3_context c, std::istream& is) { - z3_solver parser(c, is, verbose_stream(), mk_c(c)->fparams(), false); - if (!parser.parse()) { - SET_ERROR_CODE(Z3_PARSER_ERROR); - return of_ast(mk_c(c)->m().mk_true()); - } - expr_ref_vector assumptions(mk_c(c)->m()); - parser.get_assumptions(assumptions); - return of_ast(mk_c(c)->mk_and(assumptions.size(), assumptions.c_ptr())); - } - - Z3_ast Z3_API Z3_parse_z3_string(Z3_context c, Z3_string str) { - Z3_TRY; - LOG_Z3_parse_z3_string(c, str); - std::string s(str); - std::istringstream is(s); - Z3_ast r = parse_z3_stream(c, is); - RETURN_Z3(r); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_parse_z3_file(Z3_context c, Z3_string file_name) { - Z3_TRY; - LOG_Z3_parse_z3_file(c, file_name); - std::ifstream is(file_name); - if (!is) { - SET_ERROR_CODE(Z3_PARSER_ERROR); - return 0; - } - Z3_ast r = parse_z3_stream(c, is); - RETURN_Z3(r); - Z3_CATCH_RETURN(0); - } // --------------- // Support for SMTLIB2 diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 70518b54c..9e3c73ac3 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4977,23 +4977,6 @@ BEGIN_MLAPI_EXCLUDE Z3_string Z3_API Z3_get_smtlib_error(__in Z3_context c); END_MLAPI_EXCLUDE - /** - \brief \mlh parse_z3_string c str \endmlh - Parse the given string using the Z3 native parser. - - Return the conjunction of asserts made in the input. - - def_API('Z3_parse_z3_string', AST, (_in(CONTEXT), _in(STRING))) - */ - Z3_ast Z3_API Z3_parse_z3_string(__in Z3_context c, __in Z3_string str); - - /** - \brief Similar to #Z3_parse_z3_string, but reads the benchmark from a file. - - def_API('Z3_parse_z3_file', AST, (_in(CONTEXT), _in(STRING))) - */ - Z3_ast Z3_API Z3_parse_z3_file(__in Z3_context c, __in Z3_string file_name); - /*@}*/ #ifdef CorML4 diff --git a/src/api/z3_solver.cpp b/src/api/z3_solver.cpp deleted file mode 100644 index 097f39a86..000000000 --- a/src/api/z3_solver.cpp +++ /dev/null @@ -1,1304 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - z3_solver.cpp - -Abstract: - - Native ast parser. - -Author: - - Nikolaj Bjorner (nbjorner) 2007-07-17 - -Revision History: - ---*/ - -#include "z3_solver.h" -#include "z3_private.h" -#include "warning.h" -#include "ast_pp.h" -#include "ast_ll_pp.h" -#include "ast_smt_pp.h" -#include "version.h" -#include "array_decl_plugin.h" -#include "bv_decl_plugin.h" -#include "arith_decl_plugin.h" -#include "lbool.h" -#include - -#define CHECK(_b_) if (!(_b_)) { return false; } - -#define CHECK_P(_b_,_m_) if (!(_b_)) { warning_msg(_m_); return false; } - -#define CHECK_CB(_b_,_cb_) if (!(_b_)) { _cb_; return false; } - -#define TRY_CHECK(_b_) if (!(_b_)) { return false; } - - -ast_manager& Z3_get_manager(Z3_context c); -Z3_context Z3_mk_context_from_params(front_end_params const& p); -void Z3_display_statistics(Z3_context c, std::ostream& s); -void Z3_display_istatistics(Z3_context c, std::ostream& s); - -z3_solver::z3_solver( - Z3_context context, - std::istream& ins, - std::ostream& ous, - front_end_params & params, - bool is_active - ) - : - m_context(context?context:Z3_mk_context_from_params(params)), - m_owns_context(context?false:true), - m_manager(Z3_get_manager(m_context)), - m_params(params), - m_in(ins), - m_out(ous), - m_is_active(is_active), - m_assumptions(m_manager), - m_num_checks(0), - m_eof(false), - m_line(1), - m_arith(m_manager), - m_bv(m_manager), - m_pinned(m_manager), - m_last_check_result(Z3_L_UNDEF) -{ - add_builtins(m_manager.get_family_id("bv")); - add_builtins(m_manager.get_family_id("arith")); - add_builtins(m_manager.get_basic_family_id()); - add_builtins(m_manager.get_family_id("array")); - add_builtins(m_manager.get_family_id("datatype")); -} - -z3_solver::z3_solver( - ast_manager& m, - std::istream& ins, - std::ostream& ous, - front_end_params & params - ) - : - m_context(0), - m_owns_context(true), - m_manager(m), - m_params(params), - m_in(ins), - m_out(ous), - m_is_active(false), - m_assumptions(m_manager), - m_num_checks(0), - m_eof(false), - m_line(1), - m_arith(m_manager), - m_bv(m_manager), - m_pinned(m_manager) -{ - add_builtins(m_manager.get_family_id("bv")); - add_builtins(m_manager.get_family_id("arith")); - add_builtins(m_manager.get_basic_family_id()); - add_builtins(m_manager.get_family_id("array")); - add_builtins(m_manager.get_family_id("datatype")); - -} - - -z3_solver::~z3_solver() -{ - m_assumptions.reset(); - m_pinned.reset(); - if (m_owns_context && m_context) { - Z3_del_context(m_context); - } -} - -void z3_solver::skip_blank() { - while (*m_in == ' ' || *m_in == '\t' || *m_in == '\r') { - ++m_in; - } -} - -bool z3_solver::next_token() { - if (m_eof) { - warning_msg("line %d. EOF reached, expecting string", m_line); - return false; - } - skip_blank(); - if (*m_in == EOF) { - m_eof = true; - return true; - } - m_string.clear(); - while (*m_in != '\n' && *m_in != ' ' && - *m_in != '\r' && - *m_in != '\t' && *m_in != EOF) { - m_string.push_back(*m_in); - ++m_in; - } - if (*m_in == '\n' && m_string.empty()) { - m_string = "\n"; - ++m_in; - } - return true; -} - - -bool z3_solver::try_parse(char const* token) { - CHECK(!m_eof); - TRY_CHECK(strcmp(token, m_string.c_str()) == 0); - CHECK(next_token()); - return true; -} - -bool z3_solver::parse_int(int& i) { - if (m_eof) { - warning_msg("line %d. EOF reached, expecting numeral", m_line); - return false; - } - const char* s = m_string.c_str(); - i = 0; - bool negate = false; - if (*s == '-') { - negate = true; - ++s; - } - // NB: overflow checks are ignored. - while ('0' <= *s && *s <= '9') { - i = (i*10) + (*s - '0'); - ++s; - } - if (negate) { - i = -i; - } - CHECK(next_token()); - return true; -} - -bool z3_solver::check_int(int& i) { - if (m_eof) { - return false; - } - const char* s = m_string.c_str(); - bool negate = false; - i = 0; - if (!(('0' <= *s && *s <= '9') || *s == '-')) { - return false; - } - if (*s == '-') { - negate = true; - ++s; - } - while ('0' <= *s && *s <= '9') { - i = (i*10) + (*s - '0'); - ++s; - } - if (negate) { - i = -i; - } - return true; -} - -bool z3_solver::parse_unsigned(unsigned& i) { - if (m_eof) { - warning_msg("line %d. EOF reached, expecting numeral", m_line); - return false; - } - const char* s = m_string.c_str(); - i = 0; - // NB: overflow checks are ignored. - while ('0' <= *s && *s <= '9') { - i = (i*10) + (*s - '0'); - ++s; - } - CHECK(next_token()); - return true; -} - -bool z3_solver::check_unsigned(unsigned& i) { - if (m_eof) { - return false; - } - const char* s = m_string.c_str(); - i = 0; - if (!('0' <= *s && *s <= '9')) { - return false; - } - while ('0' <= *s && *s <= '9') { - i = (i*10) + (*s - '0'); - ++s; - } - return true; -} - - -bool z3_solver::parse_id(symbol& id) { - size_t sz = m_string.size(); - char const* str = m_string.c_str(); - if (strcmp(str,"\"null\"") == 0) { - id = symbol(); - } - else if (sz > 0 && str[0] == '"' && str[sz-1] == '"') { - std::string s(str,sz-1); - id = s.c_str(); - } - else { - id = m_string.c_str(); - } - CHECK(next_token()); - return true; -} - - -bool z3_solver::parse_rational(rational& r) { - if (m_eof) { - warning_msg("line %d. EOF reached, expecting rational", m_line); - return false; - } - r = rational(m_string.c_str()); - CHECK(next_token()); - return true; -} - - -bool z3_solver::parse_eol() { - if (m_eof) { - warning_msg("line %d. EOF reached, expecting newline", m_line); - return false; - } - if (m_string[0] != '\n') { - warning_msg("line %d. Expecting newline, got '%s'\n", m_line, m_string.c_str()); - return false; - } - ++m_line; - CHECK(next_token()); - - return true; -} - - -z3_solver::kind z3_solver::parse_kind() { - try_again: - if (m_eof) { - return T_EOF; - } - kind k = T_ERR; - - switch(m_string[0]) { - case 'A': - if (strcmp(m_string.c_str(), "Assert") == 0) { - k = T_ASSERT; - } - else if (strcmp(m_string.c_str(), "App") == 0) { - k = T_BUILTIN_CONST; - } - break; - case 'C': - if (strcmp(m_string.c_str(), "Const") == 0) { - k = T_NULLARY_CONST; - } - else if (strcmp(m_string.c_str(), "Check") == 0) { - k = T_CHECK; - } - else if (strcmp(m_string.c_str(), "CheckAssumptions") == 0) { - k = T_CHECK_ASSUMPTIONS; - } - break; - case 'D': - if (strcmp(m_string.c_str(), "Dec") == 0) { - k = T_DEC; - } - else if (strcmp(m_string.c_str(), "DbgSat") == 0) { - k = T_DBG_SAT; - } - else if (strcmp(m_string.c_str(), "DbgUnsat") == 0) { - k = T_DBG_UNSAT; - } - break; - case 'E': - if (strcmp(m_string.c_str(), "Echo") == 0) { - k = T_ECHO; - } - break; - case 'F': - if (strcmp(m_string.c_str(), "Fun") == 0) { - k = T_FUNCTION_CONST; - } - break; - case 'G': - if (strcmp(m_string.c_str(), "GetImpliedEqualities") == 0) { - k = T_GET_IMPLIED_EQUALITIES; - } - break; - case 'L': - if (strcmp(m_string.c_str(), "Lab") == 0) { - k = T_LAB; - } - break; - case 'N': - if (strcmp(m_string.c_str(), "Num") == 0) { - k = T_NUM; - } - break; - case 'P': - if (strcmp(m_string.c_str(), "Pat") == 0) { - k = T_PAT; - } - else if (strcmp(m_string.c_str(), "Push") == 0) { - k = T_PUSH; - } - else if (strcmp(m_string.c_str(), "Pop") == 0) { - k = T_POP; - } - break; - case ';': - k = T_COMMENT; - break; - case '\n': - if (!next_token()) { - k = T_ERR; - break; - } - goto try_again; - case 'Q': - if (strcmp(m_string.c_str(), "Qua") == 0) { - k = T_QUA; - } - break; - case 'R': - if (strcmp(m_string.c_str(), "Reset") == 0) { - k = T_RESET; - } - break; - case 'S': - if (strcmp(m_string.c_str(), "Solver") == 0) { - k = T_SOLVER; - } - else if (strcmp(m_string.c_str(), "Simplify") == 0) { - k = T_SIMPLIFY; - } - break; - case 'T': - if (strcmp(m_string.c_str(), "Ty") == 0) { - k = T_TY; - } - else if (strcmp(m_string.c_str(), "Type") == 0) { - k = T_TYPE; - } - break; - case 'V': - if (strcmp(m_string.c_str(), "Var") == 0) { - k = T_VAR; - } - else if (strcmp(m_string.c_str(), "Version") == 0) { - k = T_VERSION; - } - break; - default: - break; - } - if (k == T_ERR) { - warning_msg("line %d. could not recognize token '%s'", m_line, m_string.c_str()); - } - else if (!next_token()) { - k = T_ERR; - warning_msg("line %d. could not recognize token '%s'", m_line, m_string.c_str()); - } - return k; - -} - -bool z3_solver::parse_comment() { - while (m_string[0] != '\n') { - CHECK(next_token()); - } - CHECK(parse_eol()); - return true; -} - -bool z3_solver::parse_numeral() { - symbol id; - rational r; - sort* s; - expr* n; - CHECK(parse_id(id)); - CHECK(parse_rational(r)); - CHECK(parse_ast(s, sort_coerce())); - CHECK(parse_eol()); - if (m_arith.is_int(s)) { - n = m_arith.mk_numeral(r, true); - } - else if (m_arith.is_real(s)) { - n = m_arith.mk_numeral(r, false); - } - else if (m_bv.is_bv_sort(s)) { - n = m_bv.mk_numeral(r, s); - } - else { - return false; - } - add_id(id, n); - return true; -} - - -bool z3_solver::parse_var() { - symbol id; - unsigned n; - sort* ty; - - CHECK(parse_id(id)); - CHECK(parse_unsigned(n)); - CHECK(parse_ast(ty,sort_coerce())); - CHECK(parse_eol()); - - var* v = m_manager.mk_var(n, ty); - add_id(id, v); - return true; -} - - -family_id z3_solver::get_family_id(char const* s) { - symbol sym(s); - if (sym == "null") { - return null_family_id; - } - else { - return m_manager.get_family_id(sym); - } - -} - -bool z3_solver::parse_info(scoped_ptr& info) { - bool is_assoc = false; - bool is_comm = false; - bool is_inj = false; - vector params; - family_id fid = null_family_id; - decl_kind kind = null_decl_kind; - - if (!try_parse("BUILTIN")) { - info = 0; - return true; - } - - fid = get_family_id(m_string.c_str()); - - CHECK(next_token()); - CHECK(parse_int(kind)); - - while (m_string[0] != '\n') { - std::string s; - - if (strcmp(m_string.c_str(), ":assoc") == 0) { - is_assoc = true; - } - else if (strcmp(m_string.c_str(), ":comm") == 0) { - is_comm = true; - } - else if (strcmp(m_string.c_str(), ":inj") == 0) { - is_inj = true; - } - else { - CHECK(parse_parameter(params)); - continue; - } - CHECK(next_token()); - } - - - info = alloc(func_decl_info, fid, kind, params.size(), params.c_ptr()); - info->set_associative(is_assoc); - info->set_commutative(is_comm); - info->set_injective(is_inj); - return true; -} - - -bool z3_solver::parse_info(scoped_ptr& info) { - vector params; - bool is_infinite = true; - rational num_elems; - family_id fid = null_family_id; - decl_kind kind = null_decl_kind; - - if (!try_parse("BUILTIN")) { - info = 0; - return true; - } - - fid = get_family_id(m_string.c_str()); - std::string th = m_string.c_str(); - - CHECK(next_token()); - CHECK(parse_int(kind)); - - if (try_parse("Size")) { - CHECK(parse_rational(num_elems)); - is_infinite = false; - } - - while (m_string[0] != '\n') { - CHECK(parse_parameter(params)); - } - - if (!is_infinite && num_elems.is_uint64()) { - info = alloc(sort_info, fid, kind, num_elems.get_uint64(), params.size(), params.c_ptr()); - } - else { - info = alloc(sort_info, fid, kind, params.size(), params.c_ptr()); - } - return true; -} - - -bool z3_solver::parse_nullary_const() { - func_decl* d = 0; - app* n = 0; - symbol id; - CHECK(parse_func_decl(id, d)); - SASSERT(d); - n = m_manager.mk_const(d); - CHECK(n); - add_id(id, n); - return true; - -} - -bool z3_solver::parse_func_decl() { - func_decl* d = 0; - symbol id; - CHECK(parse_func_decl(id, d)); - CHECK(d); - add_id(id, d); - return true; -} - -bool z3_solver::parse_func_decl(symbol& id, func_decl*& n) { - symbol name; - sort_ref_vector args(m_manager); - scoped_ptr info; - CHECK(parse_id(id)); - CHECK(parse_id(name)); - CHECK(parse_asts(args,sort_coerce())); - CHECK(parse_info(info)); - CHECK(parse_eol()); - if (args.size() == 0) { - warning_msg("line %d. Expecting more than 0 arguments", m_line); - return false; - } - unsigned dom_size = args.size()-1; - sort* rng = args[dom_size].get(); - - if (info.get()) { - n = m_manager.mk_func_decl( - info.get()->get_family_id(), - info.get()->get_decl_kind(), - info.get()->get_num_parameters(), - info.get()->get_parameters(), - dom_size, args.c_ptr()); - - // HACK: not all theories have name-less decl_kinds: - // constructors, tuples, marbles, etc. - if (!n) { - n = m_manager.mk_func_decl(name, dom_size, args.c_ptr(), rng, *info.get()); - } - } - else { - n = m_manager.mk_func_decl(name, dom_size, args.c_ptr(), rng); - } - CHECK(n); - add_id(id, n); - return true; -} - -bool z3_solver::parse_const() { - symbol id; - func_decl* d; - expr_ref_vector args(m_manager); - CHECK(parse_id(id)); - CHECK(parse_ast(d,func_decl_coerce())); - CHECK(parse_asts(args, expr_coerce())); - CHECK(parse_eol()); - app* n = m_manager.mk_app(d, args.size(), args.c_ptr()); - CHECK(n); - if (!m_manager.check_sorts(n)) - return false; - add_id(id, n); - return true; -} - - -// App n name [ params ] args - -bool z3_solver::find_builtin_op(symbol name, family_id & fid, decl_kind& kind) { - builtin_info bi; - CHECK(m_builtin_ops.find(name, bi)); - fid = bi.m_fid; - kind = bi.m_kind; - return true; -} - -bool z3_solver::find_builtin_type(symbol name, family_id & fid, decl_kind& kind) { - builtin_info bi; - if (!m_builtin_types.find(name, bi)) { - return false; - } - fid = bi.m_fid; - kind = bi.m_kind; - return true; -} - -void z3_solver::add_builtins(family_id fid) { - decl_plugin* plugin = m_manager.get_plugin(fid); - SASSERT(plugin); - if (!plugin) { - return; - } - svector op_names; - plugin->get_op_names(op_names); - for (unsigned i = 0; i < op_names.size(); ++i) { - m_builtin_ops.insert(op_names[i].m_name, builtin_info(fid, op_names[i].m_kind)); - } - - svector sort_names; - plugin->get_sort_names(sort_names); - for (unsigned i = 0; i < sort_names.size(); ++i) { - m_builtin_types.insert(sort_names[i].m_name, builtin_info(fid, sort_names[i].m_kind)); - } -} - - - -bool z3_solver::parse_parameter(vector& params) { - ast* a = 0; - int n; - if (check_int(n)) { - params.push_back(parameter(n)); - } - else if (m_table.find(symbol(m_string.c_str()), a)) { - params.push_back(parameter(a)); - } - else { - symbol sym; - if (!parse_id(sym)) { - return false; - } - params.push_back(parameter(sym)); - return true; - } - CHECK(next_token()); - return true; -} - - -bool z3_solver::parse_params(vector& params) { - if (strcmp(m_string.c_str(),"[") == 0) { - CHECK(next_token()); - while (strcmp(m_string.c_str(),"]") != 0) { - CHECK(parse_parameter(params)); - } - CHECK(next_token()); - } - return true; -} - - - -bool z3_solver::parse_builtin_const() { - symbol id, name; - vector params; - family_id fid; - decl_kind kind; - app* n = 0; - expr_ref_vector args(m_manager); - CHECK(parse_id(id)); - CHECK(parse_id(name)); - CHECK(parse_params(params)); - CHECK(parse_asts(args, expr_coerce())); - CHECK(parse_eol()); - - if (find_builtin_op(name, fid, kind)) { - n = m_manager.mk_app(fid, kind, - params.size(), params.c_ptr(), - args.size(), args.c_ptr()); - } - else { - func_decl* d = 0; - CHECK(parse_ast(name, d, func_decl_coerce())); - CHECK(d); - n = m_manager.mk_app(d, args.size(), args.c_ptr()); - } - - CHECK(n); - if (!m_manager.check_sorts(n)) - return false; - add_id(id, n); - return true; -} - - -bool z3_solver::parse_type() { - symbol id, name; - scoped_ptr info; - CHECK(parse_id(id)); - CHECK(parse_id(name)); - CHECK(parse_info(info)); - CHECK(parse_eol()); - sort* ty; - if (info.get()) { - ty = m_manager.mk_sort(name, *info.get()); - } - else { - ty = m_manager.mk_sort(name); - } - CHECK(ty); - add_id(id, ty); - return true; -} - - -bool z3_solver::parse_type_new() { - symbol id, name; - vector params; - CHECK(parse_id(id)); - CHECK(parse_id(name)); - CHECK(parse_params(params)); - CHECK(parse_eol()); - sort* ty; - family_id fid; - decl_kind kind; - if (find_builtin_type(name, fid, kind)) { - ty = m_manager.mk_sort(fid, kind, params.size(), params.c_ptr()); - } - else { - ty = m_manager.mk_sort(name); - } - CHECK(ty); - add_id(id, ty); - return true; -} - - -bool z3_solver::parse_label() { - symbol id, name; - std::string s; - expr* a; - CHECK(parse_id(id)); - CHECK(next_token()); - s = m_string; - CHECK(parse_id(name)); - CHECK(parse_ast(a, expr_coerce())); - CHECK(parse_eol()); - bool pos = (strcmp("LBLPOS",s.c_str()) == 0); - app* n = m_manager.mk_label(pos, name, a); - CHECK(n); - add_id(id, n); - return true; -} - -bool z3_solver::parse_quantifier() { - std::string s; - symbol id; - unsigned num_decls, num_patterns; - expr* body; - bool is_forall; - unsigned weight; - symbol skid, qid; - svector names; - ptr_vector types; - ptr_vector patterns; - - CHECK(parse_id(id)); - s = m_string; - CHECK(next_token()); - is_forall = (strcmp("FORALL",s.c_str()) == 0); - CHECK_P(parse_unsigned(weight), "Expected unsigned integer"); - CHECK_P(parse_id(skid), "Expected symbol identifier"); - CHECK_P(parse_id(qid), "Expected symbol identifier"); - CHECK_P(parse_unsigned(num_decls), "Expected unsigned integer for number of declarations"); - for (unsigned i = 0; i < num_decls; ++i) { - symbol name; - sort* ty; - CHECK_P(parse_id(name), "Expected identifier"); - CHECK_P(parse_ast(ty, sort_coerce()), "Expected sort"); - names.push_back(name); - types.push_back(ty); - } - CHECK_P(parse_unsigned(num_patterns), "Expected unsigned integer for number of patterns"); - for (unsigned i = 0; i < num_patterns; ++i) { - app* p; - CHECK_P(parse_ast(p, pattern_coerce(m_manager)), "Expected pattern"); - patterns.push_back(p); - } - CHECK_P(parse_ast(body, expr_coerce()), "Expected expression"); - CHECK(parse_eol()); - - CHECK_P(m_manager.is_bool(body), "Body of quantifier should be Boolean type"); - CHECK_P(!m_manager.is_pattern(body), "Body of quantifier cannot be a pattern"); - - -#if 0 - if (qid == symbol() && m_params.m_default_qid) { - qid = symbol(m_line); - } -#endif - if (num_decls > 0) { - quantifier* n = m_manager.mk_quantifier( - is_forall, - num_decls, types.c_ptr(), names.c_ptr(), body, - weight, qid, skid, - num_patterns, patterns.c_ptr() - ); - CHECK(n); - add_id(id, n); - } - else { - add_id(id, body); - } - return true; -} - - - -bool z3_solver::parse_pattern() { - symbol id; - app_ref_vector patterns(m_manager); - CHECK(parse_id(id)); - CHECK(parse_asts(patterns, app_coerce())); - CHECK(parse_eol()); - app* n = m_manager.mk_pattern(patterns.size(), patterns.c_ptr()); - CHECK(n); - add_id(id, n); - return true; -} - - - -bool z3_solver::parse_assert() -{ - expr* a = 0; - CHECK(parse_ast(a, expr_coerce())); - CHECK(parse_eol()); - if (m_params.m_ast_ll_pp) { - ast_ll_pp(m_out, m_manager, a, true); - m_out.flush(); - } - if (m_params.m_ast_smt_pp) { - for (unsigned i = 0; i < m_pinned_lim.size(); ++i) { - m_out << " "; - } - m_out << mk_pp(a, m_manager) << "\n"; - m_out.flush(); - } - if (m_is_active && m_context) { - Z3_assert_cnstr(m_context, reinterpret_cast(a)); - if (m_params.m_smtlib_trace_path.size() > 0) { - m_assumptions.push_back(a); - } - } - else { - m_assumptions.push_back(a); - } - return true; -} - - -bool z3_solver::parse_simplify() -{ - expr* a = 0; - CHECK(parse_ast(a, expr_coerce())); - CHECK(parse_eol()); - if (m_params.m_ast_ll_pp) { - ast_ll_pp(m_out, m_manager, a, true); - m_out.flush(); - } - if (m_params.m_ast_smt_pp) { - for (unsigned i = 0; i < m_pinned_lim.size(); ++i) { - m_out << " "; - } - m_out << mk_pp(a, m_manager) << "\n"; - m_out.flush(); - } - if (m_is_active && m_context) { - Z3_ast r = Z3_simplify(m_context, reinterpret_cast(a)); - m_out << mk_pp(reinterpret_cast(r), m_manager) << "\n"; - m_out.flush(); - } - return true; -} - - - -bool z3_solver::parse_check() -{ - CHECK(parse_eol()); - - if (!m_context || !m_is_active) { - return true; - } - - Z3_model m = 0; - Z3_ast pr = 0; - Z3_lbool result = Z3_check_assumptions(m_context, 0, 0, &m, &pr, 0, 0); - m_last_check_result = result; - - // display the model. - - if (m && m_params.m_model) { - char const* md = Z3_model_to_string(m_context, m); - if (md) { - m_out << md; - } - } - if (m) { - Z3_del_model(m_context, m); - } - - if (result == Z3_L_FALSE && pr != 0 && m_params.m_display_proof) { - m_out << mk_ll_pp(reinterpret_cast(pr), m_manager, true, false); - } - - switch(result) { - case l_false: m_out << "unsat\n"; break; - case l_true: m_out << "sat\n"; break; - case l_undef: m_out << "unknown\n"; break; - } - m_out.flush(); - - dump_smtlib_benchmark(0, 0, result); - return true; -} - -void z3_solver::dump_smtlib_benchmark(unsigned num_assumptions, expr* const* assumptions, Z3_lbool result) { - // - // Generate SMT-LIB benchmark from current set of assertions. - // - if (m_params.m_dump_goal_as_smt || m_params.m_smtlib_trace_path.size() > 0) { - ast_smt_pp pp(m_manager); - pp.set_logic(m_params.m_smtlib_logic.c_str()); - pp.set_source_info(m_params.m_smtlib_source_info.c_str()); - pp.set_category(m_params.m_smtlib_category.c_str()); - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - pp.add_assumption(m_assumptions[i].get()); - } - for (unsigned i = 0; i < num_assumptions; ++i) { - pp.add_assumption_star(assumptions[i]); - } - char const* status = (result == Z3_L_FALSE)?"unsat":((result == Z3_L_TRUE)?"sat":"unknown"); - pp.set_status(status); - std::ostringstream buffer; - if (m_params.m_smtlib_trace_path.size() > 0) { - buffer << m_params.m_smtlib_trace_path.c_str() << "_" << m_num_checks << ".smt2"; - } - else { - buffer << "query." << m_num_checks << ".smts"; - } - std::ofstream out(buffer.str().c_str()); - if (!out.fail() && !out.bad()) { - pp.display_smt2(out, m_manager.mk_true()); - } - m_num_checks++; - out.close(); - } - -} - - -bool z3_solver::parse_get_implied_equalities() -{ - expr_ref_vector args(m_manager); - unsigned_vector cls; - CHECK(parse_asts(args, expr_coerce())); - CHECK(parse_eol()); - cls.resize(args.size()); - - if (!m_context) { - return true; - } - - - TRACE("get_implied_equalities", tout << "checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";); - Z3_lbool result = Z3_get_implied_equalities(m_context, args.size(), reinterpret_cast(args.c_ptr()), cls.c_ptr()); - TRACE("get_implied_equalities", tout << "after checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";); - m_last_check_result = result; - - m_out << ";Implied Equality Classes: "; - for (unsigned i = 0; i < cls.size(); ++i) { - m_out << cls[i] << " "; - } - m_out << "\n"; - - m_out.flush(); - - return true; -} - - -bool z3_solver::parse_check_assumptions() -{ - expr_ref_vector args(m_manager); - CHECK(parse_asts(args, expr_coerce())); - CHECK(parse_eol()); - - if (!m_context) { - return true; - } - - Z3_model m = 0; - - Z3_ast pr = 0; - - TRACE("check_assumptions", tout << "checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";); - Z3_lbool result = Z3_check_assumptions(m_context, args.size(), reinterpret_cast(args.c_ptr()), &m, &pr, 0, 0); - TRACE("check_assumptions", tout << "after checking assumptions...\n" << Z3_context_to_string(m_context) << "\n";); - m_last_check_result = result; - - // display the model. - - if (m && m_params.m_model) { - char const* md = Z3_model_to_string(m_context, m); - if (md) { - m_out << md; - } - } - if (m) { - Z3_del_model(m_context, m); - } - - if (result == Z3_L_FALSE && pr != 0 && m_params.m_display_proof) { - m_out << mk_ll_pp(reinterpret_cast(pr), m_manager, true, false); - } - - switch(result) { - case l_false: m_out << "unsat\n"; break; - case l_true: m_out << "sat\n"; break; - case l_undef: m_out << "unknown\n"; break; - } - m_out.flush(); - - dump_smtlib_benchmark(args.size(), args.c_ptr(), result); - - return true; -} - -bool z3_solver::parse_dbg(bool expected_sat) { - CHECK(parse_eol()); - if (m_last_check_result == Z3_L_FALSE && expected_sat) { - m_out << "!!!!!!!!BUG FOUND!!!!!!!!!\n"; - throw z3_error(ERR_UNSOUNDNESS); - } - if (m_last_check_result == Z3_L_TRUE && !expected_sat) { - m_out << "!!!!!!!!BUG FOUND!!!!!!!!!\n"; - throw z3_error(ERR_INCOMPLETENESS); - } - if (m_last_check_result == Z3_L_UNDEF) { - throw z3_error(ERR_UNKNOWN_RESULT); - } - return true; -} - -bool z3_solver::parse_push() -{ - CHECK(parse_eol()); - if (m_context) { - Z3_push(m_context); - } - m_pinned_lim.push_back(m_pinned.size()); - m_assumptions_lim.push_back(m_assumptions.size()); - return true; -} - - -bool z3_solver::parse_pop() -{ - CHECK(parse_eol()); - if (m_context) { - Z3_pop(m_context, 1); - } - m_pinned.resize(m_pinned_lim.back()); - m_pinned_lim.pop_back(); - m_assumptions.resize(m_assumptions_lim.back()); - m_assumptions_lim.pop_back(); - return true; -} - - -bool z3_solver::parse_reset() -{ - CHECK(parse_eol()); - if (m_context) { - Z3_del_context(m_context); - Z3_config m_config = 0; // TBD. - m_context = Z3_mk_context(m_config); - } - return true; -} - -bool z3_solver::parse_echo() -{ - CHECK(parse_eol()); - // TBD - return true; -} - -bool z3_solver::parse_version() -{ - unsigned major, minor; - CHECK(parse_unsigned(major)); - CHECK(parse_unsigned(minor)); - CHECK(next_token()); // build date - CHECK(next_token()); // revision - CHECK(parse_eol()); - if (major != Z3_MAJOR_VERSION) { - warning_msg("Parser is incompatible. Major version %d has changed to %d", major, Z3_MAJOR_VERSION); - return false; - } - if (minor > Z3_MINOR_VERSION) { - warning_msg("Parser is incompatible. Minor version %d of parser is younger than %d", Z3_MINOR_VERSION, minor); - return false; - } - return true; -} - - -bool z3_solver::parse_solver() -{ - std::string s; - const char * str; - s = m_string; - CHECK(next_token()); - CHECK(parse_eol()); - str = s.c_str(); -#if 0 - if (!m_solver) { - - } - else if (strcmp(str,"LIA") == 0) { - m_solver->register_arith(unmanaged_wrapper::LIA); - } - else if (strcmp(str,"LRA") == 0) { - m_solver->register_arith(unmanaged_wrapper::MIA); - } - else if (strcmp(str,"BV") == 0) { - m_solver->register_bv(); - } -#endif - return true; -} - -bool z3_solver::parse() -{ - next_token(); - bool ok = true; - while (ok) { - switch(parse_kind()) { - case T_NUM: - ok = parse_numeral(); - break; - case T_VAR: - ok = parse_var(); - break; - case T_DEC: - ok = parse_func_decl(); - break; - case T_FUNCTION_CONST: - ok = parse_const(); - break; - case T_GET_IMPLIED_EQUALITIES: - ok = parse_get_implied_equalities(); - break; - case T_NULLARY_CONST: - ok = parse_nullary_const(); - break; - case T_BUILTIN_CONST: - ok = parse_builtin_const(); - break; - case T_TY: - ok = parse_type(); - break; - case T_TYPE: - ok = parse_type_new(); - break; - case T_QUA: - ok = parse_quantifier(); - break; - case T_LAB: - ok = parse_label(); - break; - case T_PAT: - ok = parse_pattern(); - break; - case T_ASSERT: - ok = parse_assert(); - break; - case T_SOLVER: - ok = parse_solver(); - break; - case T_SIMPLIFY: - ok = parse_simplify(); - break; - case T_PUSH: - ok = parse_push(); - break; - case T_CHECK: - ok = parse_check(); - break; - case T_CHECK_ASSUMPTIONS: - ok = parse_check_assumptions(); - break; - case T_DBG_SAT: - ok = parse_dbg(true); - break; - case T_DBG_UNSAT: - ok = parse_dbg(false); - break; - case T_POP: - ok = parse_pop(); - break; - case T_RESET: - ok = parse_reset(); - break; - case T_COMMENT: - ok = parse_comment(); - break; - case T_ECHO: - ok = parse_echo(); - break; - case T_VERSION: - ok = parse_version(); - break; - case T_EOF: - return true; - case T_ERR: - return false; - case T_CTX: - // [Leo]: this case is not handled. - break; - } - } - if (!ok) { - warning_msg("line %d. error encountered", m_line); - } - return ok; -} - -void z3_solver::display_statistics(std::ostream& out, bool istats) -{ - if (m_context) { - if (istats) { - Z3_display_istatistics(m_context, out); - } - else { - Z3_display_statistics(m_context, out); - } - } -} - -void z3_solver::add_id(symbol const& id, ast* n) { - m_table.insert(id, n); - m_pinned.push_back(n); -} - diff --git a/src/api/z3_solver.h b/src/api/z3_solver.h deleted file mode 100644 index 0876646ac..000000000 --- a/src/api/z3_solver.h +++ /dev/null @@ -1,1007 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - z3_solver.h - -Abstract: - - Native ast parser. - -Author: - - Nikolaj Bjorner (nbjorner) 2007-07-17 - -Revision History: - ---*/ - -/** - \defgroup z3native Z3 low level input format - - This format is mainly used for generating logs. These logs - capture the expressions created using the Z3 API, and - the main commands available there. - It is very low-level and follows - some of the conventions found in the DIMACS format for SAT problems - and by the Spear - input format. - - The format is extensible, as the grammar allows for - selecting solvers and adding \emph{semantic attachments} - with constructors. The SMT-LIB and Simplify text formats are easier to - write and read for a human consumer. - - Every line consists of a command that gets interpreted - as a declaration of a node in anbstract syntax tree, or as - a control instruction to Z3, such as to augment the current - context with constraints or check for satisfiability. - - \nicebox{ - command := - | ast - | control - | ; commented line - } - - - White spaces are implicit in the production rules. - The legal white-spaces have the ASCII representations - - \nicebox{ - ' ' | \ t | \ r - } - - Comment lines start with \c ;. - All characters up to the newline \ n are ignored. - - We use id for identifiers in general. - Identifiers associated with certain semantic categories, - such as \emph{ast} nodes, or \emph{type}s are - prefixed by the category and suffixed by \emph{id}. - For example, we have: - - \nicebox{ - ast-id - identifier for ast nodes - - type-id - identifier for type nodes - - parameter-id - identifier for ast - - name-id - identifier for a function/type name - - decl-id - identifier for declaration node - - context-id - identifier for Boolean context - } - - Identifiers can be any sequence of non-whitespace - and non-newline characters whose first character - is not one of the decimal digits. - Identifiers enclosed in quotes ''...'' - are treated specially: the quotes are stripped. - Thus, the identifier consisting of zero characters - is written ''''. The identifier ''null'' - is allowed for skolem-id and quant-id. - - \section nativecontrol Control commands - - To load a theory solver for integer linear arithmetic, - include a line of the form \ty{Solver LIA}. To load the - mixed integer/real solver include instead a line of the - form \ty{Solver LRA} - - Use \ty{Push} and \ty{Pop} to push/pop contexts - (constraints that are asserted - under a \ty{Push} are removed after a \ty{Pop}). - To reset the state entirely, use \ty{Reset}. - - To assert a constraint use \ty{Assert} \emph{ast-id}, - where the \emph{ast-id} is an identifier declared - for a boolean typed term. - - To check for satisfiability of all asserted constraints - use \ty{Check}. - - \nicebox{ - control := - | Solver solver - load specified theory solver - | Assert ast-id - assert constraint - | Check - check for satisfiability of asserts - | Push - push a context - | Pop - pop a context - | Version major minor build-number revision - specify Z3 version - - solver := - | LRA - mixed integer/real arithmetic - | LIA - integer arithmetic} - - \section z3nativeast Abstract syntax trees - - Every node in the abstract syntax trees understood by Z3 - is declared by using a syntax category identifier, followed - by a (unique) identifier that names the node. The - node identifier is followed by a description of the node. - - In overview abstract syntax tree nodes are declared using the commands: - - \nicebox{ - ast := - | Type id type - | Dec id declaration - | Const id constant - | Fun id function - | App id built-in - | Num id numeral - | Qua id quantifier - | Var id bound-variable - | Ctx id local-context - | Lab id label-term - | Pat id pattern - } - - \subsection z3nativetypes Types - - Types are created from a name and optional parameters. - A number of names are reserved for built-in theories. - These names are: - \nicebox{ - Int Real Bool bv array - } - When the name of a type is one of these, the type is automatically - associated with the respective theory. - The \ty{bv} type takes one numeric parameter (the bit-width of the - bit-vector), and \ty{array} takes n+1 parameters (the n - types for the domain of the array and the last parameter for the - range of the array. - - \nicebox{ - type := name '[' parameter* ']' - - parameter := number | ast-id | symbol - } - A parameter can either be an integer, an identifier used for - another defined term or type, or a symbol. Symbols are given as - strings. The parser first attempts to identify a parameter as - a previously defined term or type, and if there is no - such previously defined term/type, then it treats the string - as a symbol. - - \subsection nativez3Fuctions Function and constant declarations - In Z3, functions are constants that take more than zero arguments, - thus, everything is treated as a constant. - - Constant declarations comprise of a name, followed by - a non-empty list of types, all but the first types - are the domain of the function (there are no domain - types for 0-ary constants), the last type is the range. - A constant declaration is followed by optional - theory specific information. - - The codes used in the theory specific information is described under \ref theories - - The theory specific information indicates - whether the constant is associative/commutative/injective; - a list of parameters may also be used to indicate - auxiliary information for the constant declarations. - - \nicebox{ - declaration := name-id type-id* [const-info] - - const-info := BUILTIN theory kind-num (:assoc | :comm | :inj | parameter)* - - theory := - | basic - built-in types and operations - | arith - arithmetical - | bv - bit-vectors - | array - arrays - | datatype - datatypes - } - - - \subsection z3nativeterms Terms - - - Terms are built from constants, function applications, - labeling, context formation, quantification - and bound variables. - - A constant consists of a declarations, functions consist of - a declaration followed by a non-empty list of term identifiers. - All constants and function applications can be constructed using - the \ty{Fun} construct. However, two shortcuts are available. - -
    -
  • \ty{Const}: - Constants may be defined directly by supplying the name and the type of the constant. -
    • -
  • \ty{App}: - Built-in arithmetic, array, bit-vector, and Boolean operations may be applied directly - to their arguments without first providing function declarations. -
    • -
- - \nicebox{ - constant := name-id type-id - - function := decl-id ast-id* - - built-in := name-id [ [ parameter* ] ] ast-id* - } - - Labeled terms consist of a polarity (\ty{LBLPOS} for positive - context, \ty{LBLNEG} for negative contexts), a name, and a - term identifier. - - - \nicebox{ - label-term := (LBLPOS | LBLNEG) label-name ast-id - } - - Local contexts consist of an identifier for the underlying - term, followed by a predicate summarizing the context in - which the term is interpreted. - - \nicebox{ - local-context := ast-id context-id - } - - A quantifier consists of -
    -
  • -A number indiciating the -weight of the quantifier (for matching precedence), -
  • -A skolem identifier, used for Boogie quantifier instantiation, -
  • -A quantifier identifier, used for profiling instantiations, -
  • -A number indicating how many variables are bound by the quantifier, followed -by the bound variables, which are -
      -
    • A name for the bound variable. -
    • An identifier for the type of the bound variable. -
    -
  • -A number indicating how many patterns are associated with the quantifier, -followed by the patterns, which are -
      -
    • An identifier for the pattern. -
    -
  • An identifier for the body of the quantifier. -
- - \nicebox{ - quantifier := - (FORALL | EXISTS) - weight-num - skolem-id - quant-id - decls-num - (name-id type-id)* - pattern-num - pattern-id* - ast-id - } - -A bound variable consists of a de-Brujin index for the bound -variable together with the type of the bound variable. -While the type can be computed by matching the index of -the de-Brujin index with the associated quantifier, - -Patterns comprise of a list of terms. - - - \nicebox{ - bound-variable := index-num type-id - - numeral := rational type-id - - rational := number [/number] - - number := [0-9]+ - - pattern := id ast-id* - } - - -\section z3nativeexamples Examples - -\subsection z3nativearithmetic Integer Arithmetic - -Suppose we wish to check whether -\nicebox{ - z0 >= 0 && z1 >= 0 && z2 >= 1 && z1 >= z2 && z2 >= z0 -} -is satisfiable for 
z0, z1, z2
integers. -With the low-level input format, we may specify this by: - -\nicebox{ - Type INT Int - Type BOOL Bool - Const z0 z0 INT - Const z1 z1 INT - Const z2 z2 INT - Num 0 0 INT - Num 1 1 INT - App c0 >= z0 0 - Assert c0 - App c1 >= z1 0 - Assert c1 - App c2 >= z2 1 - Assert c2 - App c3 >= z1 z2 - Assert c3 - App c4 >= z2 z0 - Assert c4 - Check -} - - -Notice that the identifiers may be arbitrary strings, including numerals. -So for instance, we used 1 to represent integer 1. - -\subsection z3nativebv Bit-vectors - -We can check whether 32-bit addition is commutative. Z3 reports \ty{unsat} -in for the first check. The second satisfiable check illustrates the use of parameters -(\ty{extract} takes two integer parameters for the range of bits extracted -from the bit-vectors). - -\nicebox{ - Type bool Bool - Type bv32 bv [ 32 ] - Type bv64 bv [ 64 ] - Num 0 0 bv32 - Num 1 1 bv32 - Const x0 x0 bv32 - Const x1 x1 bv32 - Const x2 x2 bv64 - App a bvadd x0 x1 - App b bvadd x1 x0 - App eq = a b - App constraint1 not eq - Push - Assert constraint1 - Check - Pop - App c extract [ 31 0 ] x2 - App eq2 = a c - App constraint2 not eq2 - Push - Assert constraint2 - Check - Pop -} - -We added the declarations of bit-vector constants 0 and 1. Like integers, -these are also numerals, but with bit-vector type. - - -\subsection z3nativeexarray Arrays - -The low-level version of: -\nicebox{ - store(f1,i1,v1) = store(f2,i2,v2) && i1 != i3 && i2 != i3 && select(f1,i3) != select(f2,i3) -} -is: - -\nicebox{ - Type Index Index - Type Elem Elem - Type Array array [ Index Elem ] - Type bool Bool - Const i1 i1 Index - Const i2 i2 Index - Const i3 i3 Index - Const v1 v1 Elem - Const v2 v2 Elem - Const f1 f1 Array - Const f2 f2 Array - App n1 store f1 i1 v1 - App n2 store f2 i2 v2 - App n3 = n1 n2 - App n4 = i1 i3 - App n5 not n4 - App n6 = i2 i3 - App n7 not n6 - App n8 select f1 i3 - App n9 select f2 i3 - App n10 = n8 n9 - App n11 not n10 - Assert n3 - Assert n5 - Assert n7 - Assert n11 - Check -} - -\subsection z3nativeexdatatype Data-types - -To check projection over tuples -\nicebox{ - (= x (first (mk_tuple x y))) -} - -we write: -\nicebox{ - Type int Int - Type pair tuple [ mk_tuple first int second int ] - Const x x int - Const y y int - Const p p pair - App n1 mk_tuple x y - App n2 first n1 - App n3 = n2 x - App n4 not n3 - Assert n4 - Check -} - - -*/ - - /** - - \defgroup theories Z3 theories - - - \section theorisbasics Basics - -There is a single basic sort, \ty{bool}, which has op-code 0. -The basic operators are, listed with their codes in the table below. - - - - - - - - - - - - - - - - - - -
Op-codeMnmonicsDescription
0 \ty{true} the constant \emph{true}
1 \ty{false} the constant \emph{false}
2 \ty{=} equality
3 \ty{distinct} distincinctness
4 \ty{ite} if-then-else
5 \ty{and} n-ary conjunction
6 \ty{or} n-ary disjunction
7 \ty{iff} bi-impliciation
8 \ty{xor} exclusive or
9 \ty{not} negation
10 \ty{implies} implication
- - \section theoriesarithmetic Arithmetic - - \subsection tharithbuiltin Built-in operators - - Arithmetical expression can be built from reals or integers. - The arithmetical sorts are listed below - and the supported operations are listed in the table thereafter. - - - - - - - - - -
Op-codeMnmonicsDescription
0 \ty{real} sort of reals
1 \ty{int} sort of integers
- - - - - - - - - - - - - - - - - - - -
Op-codeMnmonicsDescription
0 \ty{<=} less-than or equal
1 \ty{>=} greater-than or equal
2 \ty{<} less-than
3 \ty{>} greater-than
4 \ty{+} n-ary addition
5 \ty{-} binary minus
6 \ty{~} unary minus
7 \ty{*} n-ary multiplication
8 \ty{/} rational division
9 \ty{div} integer division
10 \ty{rem} integer remainder
11 \ty{mod} integer modulus
- - \section theoriesbv Bit-vectors -To indicate the bit-vector length one adds a numeral parameter -with the number of bits the bit-vector holds. -For instance, a declaration of the form: - -\nicebox{ - Type $1 bv [ 32 ] -} - -declares a 32-bit bit-vector type. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Op-codeMnmonicsParametersDescription
0 \ty{bit1} constant comprising of a single bit set to 1
1 \ty{bit0} constant comprising of a single bit set to 0.
2 \ty{bvneg} Unary subtraction.
3 \ty{bvadd} addition.
4 \ty{bvsub} subtraction.
5 \ty{bvmul} multiplication.
6 \ty{bvsdiv} signed division.
7 \ty{bvudiv} unsigned division. -The operands are treated as unsigned numbers.
8 \ty{bvsrem} signed remainder.
9 \ty{bvurem} unsigned remainder.
10 \ty{bvsmod} signed modulus.
11 \ty{bvule} unsigned \ty{<=}.
12 \ty{bvsle} signed \ty{<=}.
13 \ty{bvuge} unsigned \ty{>=}.
14 \ty{bvsge} signed \ty{>=}.
15 \ty{bvult} unsigned \ty{<}.
16 \ty{bvslt} signed \ty{<}.
17 \ty{bvugt} unsigned \ty{>}.
18 \ty{bvsgt} signed \ty{>}.
19 \ty{bvand} n-ary (associative/commutative) bit-wise and.
20 \ty{bvor} n-ary (associative/commutative) bit-wise or.
21 \ty{bvnot} bit-wise not.
22 \ty{bvxor} n-ary bit-wise xor.
23 \ty{bvnand} bit-wise nand.
24 \ty{bvnor} bit-wise nor.
25 \ty{bvxnor} bit-wise exclusive nor.
26 \ty{concat} bit-vector concatentaion.
27 \ty{sign\_extend} \emph{n} \emph{n}-bit sign extension.
28 \ty{zero\_extend} \emph{n} \emph{n}-bit zero extension.
29 \ty{extract} \emph{hi:low} \emph{hi}-\emph{low} bit-extraction.
30 \ty{repeat} \emph{n} repeat $n$ times.
31 \ty{bvredor} or-reduction.
32 \ty{bvredand} and-reducdtion.
33 \ty{bvcomp} bit-vector comparison.
34 \ty{bvshl} shift-left.
35 \ty{bvlshr} logical shift-right.
36 \ty{bvrshr} arithmetical shift-right.
37 \ty{bvrotate\_left} \emph{n} \emph{n}-bit left rotation.
38 \ty{bvrotate\_right} \emph{n} \emph{n}-bit right rotation.
- -\section theoriesarrays Arrays - -\subsection tharraybuiltinops Built-in operators - - There is a single built-in sort constructor for arrays with code 0. - It is followed by a sequence of parameters indicating the domain - sorts and the range of the array. - - - - - - - - - - -
Op-codeMnmonicsDescription
0 \ty{store} array store
1 \ty{select} array select
- - In the low-level input format, array types - are accompanied by a sequence of identifiers corresponding - to the domain and range of the array the operations operate - upon. - In more detail, the contract is that the supplied parameters - to the type declaration of an array are of the form: - -
    -
  • parameter_0 - 1'st dimension -
  • parameter_{n-1} - n'th dimension -
  • parameter_n - range -
- - The constant array function symbol \ty{const} needs a parameter - in order to infer the types of the indices of the constant array. - We pass the array type as the parameter to \ty{const}. - The other array operations do not need parameters. - - We summarize the arities and semantics of the operators: - -
    -
  • \ty{store} - - -Updates an array at a given index with a value: - \ty{store}(A, i0, ... i_{n-1}, v) has the same contents as A, except on -index i0, ... , i_{n-1}, where the value is v. - -
  • \ty{select} - - - Selects the value from an array: - \ty{select}(A, i0, ... , i_{n-}) selects the value stored at - index i0, ... , i_{n-1}. -
- - - - - */ -#ifndef _Z3_SOLVER_H_ -#define _Z3_SOLVER_H_ - -#include "ast.h" -#include "symbol_table.h" -#include "stream_buffer.h" -#include "warning.h" -#include "front_end_params.h" -#include "arith_decl_plugin.h" -#include "bv_decl_plugin.h" -#include "z3.h" - - -class z3_solver { - - enum kind { - T_NUM, - T_VAR, - T_DEC, - T_FUNCTION_CONST, - T_GET_IMPLIED_EQUALITIES, - T_NULLARY_CONST, - T_BUILTIN_CONST, - T_TY, - T_TYPE, - T_QUA, - T_LAB, - T_CTX, - T_PAT, - - T_SOLVER, - T_SIMPLIFY, - - T_ASSERT, - T_CHECK, - T_CHECK_ASSUMPTIONS, - T_DBG_SAT, - T_DBG_UNSAT, - T_PUSH, - T_POP, - T_RESET, - T_ECHO, - T_VERSION, - - T_COMMENT, - - T_EOF, - T_ERR - }; - - struct builtin_info { - family_id m_fid; - decl_kind m_kind; - builtin_info(family_id fid, decl_kind k) : m_fid(fid), m_kind(k) {} - builtin_info(): m_fid(null_family_id), m_kind(null_decl_kind) {} - }; - - Z3_context m_context; - bool m_owns_context; - ast_manager& m_manager; - front_end_params& m_params; - symbol_table m_table; - stream_buffer m_in; - std::ostream& m_out; - bool m_is_active; - expr_ref_vector m_assumptions; - unsigned_vector m_assumptions_lim; - unsigned m_num_checks; - std::string m_string; - bool m_eof; - unsigned m_line; - symbol_table m_builtin_ops; - symbol_table m_builtin_types; - arith_util m_arith; - bv_util m_bv; - ast_ref_vector m_pinned; - unsigned_vector m_pinned_lim; - Z3_lbool m_last_check_result; - -public: - - z3_solver( - Z3_context c, - std::istream& is, - std::ostream& os, - front_end_params & params, - bool is_active = true - ); - - z3_solver( - ast_manager& m, - std::istream& is, - std::ostream& os, - front_end_params & params - ); - - ~z3_solver(); - - bool parse(); - - void get_assumptions(expr_ref_vector& v) { v.append(m_assumptions); } - - void display_statistics(std::ostream& out, bool istats); - - void set_error_handler(Z3_error_handler h) { - Z3_set_error_handler(m_context, h); - } - -private: - - template - struct coerce { - virtual ~coerce() {} - virtual T* operator()(ast* a) const = 0; - }; - - struct sort_coerce : public coerce { - virtual sort* operator()(ast* a) const { - if (!a || a->get_kind() != AST_SORT) { - return 0; - } - return to_sort(a); - } - }; - - struct func_decl_coerce : public coerce { - virtual func_decl* operator()(ast* a) const { - if (!a || a->get_kind() != AST_FUNC_DECL) { - return 0; - } - return to_func_decl(a); - } - }; - - struct pattern_coerce : public coerce { - ast_manager& m_manager; - pattern_coerce(ast_manager& m): m_manager(m) {} - virtual app* operator()(ast* a) const { - if (!a || a->get_kind() != AST_APP) { - return 0; - } - if (!m_manager.is_pattern(to_app(a))) { - return 0; - } - return to_app(a); - } - }; - - struct expr_coerce : public coerce { - virtual expr* operator()(ast* a) const { - if (!a) { - return 0; - } - ast_kind k = a->get_kind(); - switch(k) { - case AST_APP: - case AST_QUANTIFIER: - case AST_VAR: - return reinterpret_cast(a); - default: - return 0; - } - } - }; - - struct app_coerce : public coerce { - virtual app* operator()(ast* a) const { - if (!a) { - return 0; - } - if (a->get_kind() == AST_APP) { - return to_app(a); - } - return 0; - } - }; - - - template - bool parse_ast(symbol id, T*& n, const coerce& coerce) - { - ast* a; - if (!m_table.find(id, a)) { - warning_msg("line %d. Could not find id '%s'\n", - m_line, id.str().c_str()); - return false; - } - n = coerce(a); - if (n == 0) { - warning_msg("line %d. Wrong kind %d for %s\n", - m_line, a->get_kind(), id.str().c_str()); - return false; - } - return true; - } - - - template - bool parse_ast(T*& n, const coerce& coerce) - { - symbol id; - if (parse_id(id)) { - return parse_ast(id, n, coerce); - } - return false; - } - - - template - bool parse_asts(ref_vector& asts, const coerce& c) - { - symbol id; - T* n; - while (m_string[0] != '\n') { - if (strcmp(m_string.c_str(), "BUILTIN") == 0) { - return true; - } - if (!parse_ast(n,c)) { - return false; - } - asts.push_back(n); - } - return true; - } - - kind parse_kind(); - - bool next_token(); - - bool parse_id(symbol& id); - - bool parse_rational(rational& r); - - void skip_blank(); - - bool parse_eol(); - - bool parse_numeral(); - - bool parse_var(); - - bool parse_info(scoped_ptr& info); - - bool parse_info(scoped_ptr& info); - - bool parse_func_decl(); - - bool parse_func_decl(symbol& id, func_decl*& d); - - bool parse_nullary_const(); - - bool parse_const(); - - bool parse_builtin_const(); - - bool parse_type(); - - bool parse_type_new(); - - bool parse_label(); - - bool parse_quantifier(); - - bool parse_pattern(); - - bool parse_int(int& i); - - bool check_int(int& i); - - bool parse_unsigned(unsigned& i); - - bool check_unsigned(unsigned& i); - - bool try_parse(char const* token); - - bool parse_assert(); - - bool parse_simplify(); - - bool parse_check(); - - bool parse_check_assumptions(); - - bool parse_get_implied_equalities(); - - bool parse_dbg(bool expected_sat); - - bool parse_push(); - - bool parse_comment(); - - bool parse_pop(); - - bool parse_reset(); - - bool parse_echo(); - - bool parse_version(); - - bool parse_solver(); - - bool parse_parameter(vector& params); - - bool parse_params(vector& params); - - bool find_builtin_op(symbol name, family_id & fid, decl_kind& kind); - - bool find_builtin_type(symbol name, family_id & fid, decl_kind& kind); - - void add_builtins(family_id fid); - - void add_id(symbol const& id, ast* a); - - family_id get_family_id(char const* s); - - void dump_smtlib_benchmark(unsigned num_assumptions, expr* const* assumptions, Z3_lbool result); -}; - -#endif diff --git a/src/bindings/dotnet/Context.cs b/src/bindings/dotnet/Context.cs index 27bbf6d42..2aea1586c 100644 --- a/src/bindings/dotnet/Context.cs +++ b/src/bindings/dotnet/Context.cs @@ -2853,30 +2853,6 @@ namespace Microsoft.Z3 } #endregion - #region Native Parser - /// - /// Parse the given string using the Z3 native parser. - /// - /// A conjunction of asserts made in . - public Expr ParseZ3String(string str) - { - Contract.Ensures(Contract.Result() != null); - - return Expr.Create(this, Native.Z3_parse_z3_string(nCtx, str)); - } - - /// - /// Parse the given file using the Z3 native parser. - /// - /// A conjunction of asserts made in the file. - public Expr ParseZ3File(string fileName) - { - Contract.Ensures(Contract.Result() != null); - - return Expr.Create(this, Native.Z3_parse_z3_file(nCtx, fileName)); - } - #endregion - #region Goals /// /// Creates a new Goal.