From 263fb481805f1a620a326e09c84ad38158872aec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 16:59:22 -0700 Subject: [PATCH 1/7] polishing VS build Signed-off-by: Leonardo de Moura --- scripts/config-vs-debug.mk | 2 +- src/test/imdd.cpp | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/scripts/config-vs-debug.mk b/scripts/config-vs-debug.mk index 8e0cdef58..1e2a8c58a 100644 --- a/scripts/config-vs-debug.mk +++ b/scripts/config-vs-debug.mk @@ -1,5 +1,5 @@ CXX=cl -CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /openmp /Gd /analyze- +CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /openmp /Gd /analyze- /arch:SSE2 CXX_OUT_FLAG=/Fo OBJ_EXT=.obj LIB_EXT=.lib diff --git a/src/test/imdd.cpp b/src/test/imdd.cpp index f59f87b4f..12d23993e 100644 --- a/src/test/imdd.cpp +++ b/src/test/imdd.cpp @@ -18,6 +18,8 @@ Revision History: --*/ #include"imdd.h" +#ifndef _AMD64_ + static void tst0() { std::cout << "--------------------------------\n"; imdd_manager m; @@ -607,3 +609,9 @@ void tst_imdd() { } +#else + +void tst_imdd() { +} + +#endif From 95a25265f26cc23bd952045e4ee947cab8e2eeb0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 17:18:41 -0700 Subject: [PATCH 2/7] 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. From 87681c9e85f61e58e506faa2c51a125dfb0b9ed4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 17:33:32 -0700 Subject: [PATCH 3/7] minimizing smt 1.0 parser dependencies Signed-off-by: Leonardo de Moura --- src/test/ast_pp.cpp | 59 -------- src/test/ast_smt_pp.cpp | 90 ------------- src/{dead/test => test/dead}/ackermanize.cpp | 0 src/{dead/test => test/dead}/core_theory.cpp | 0 src/{dead/test => test/dead}/dimacs.cpp | 0 src/{dead/test => test/dead}/distinct.cpp | 0 .../{ => dead}/expr_context_simplifier.cpp | 0 src/{dead/test => test/dead}/fingerprint.cpp | 0 src/{dead/test => test/dead}/gate.cpp | 0 .../dead}/interval_arithmetic.cpp | 0 src/test/{ => dead}/qe_defs.cpp | 0 src/test/{ => dead}/quant_elim.cpp | 0 src/{dead/test => test/dead}/relevancy.cpp | 0 src/{dead/test => test/dead}/sat.cpp | 0 .../test => test/dead}/simplex_polynomial.cpp | 0 src/test/{ => dead}/symmetry.cpp | 0 .../test => test/dead}/template_models.cpp | 0 .../test => test/dead}/th_propagation.cpp | 0 src/{dead/test => test/dead}/trail.cpp | 0 src/{dead/test => test/dead}/watch_list.cpp | 0 src/test/dl_rule_set.cpp | 118 ---------------- src/test/expr_delta.cpp | 127 ------------------ src/test/expr_pattern_match.cpp | 51 ------- src/test/grobner.cpp | 94 ------------- src/test/main.cpp | 13 -- src/test/smtparser.cpp | 52 ------- src/test/var_subst.cpp | 19 --- 27 files changed, 623 deletions(-) delete mode 100644 src/test/ast_pp.cpp delete mode 100644 src/test/ast_smt_pp.cpp rename src/{dead/test => test/dead}/ackermanize.cpp (100%) rename src/{dead/test => test/dead}/core_theory.cpp (100%) rename src/{dead/test => test/dead}/dimacs.cpp (100%) rename src/{dead/test => test/dead}/distinct.cpp (100%) rename src/test/{ => dead}/expr_context_simplifier.cpp (100%) rename src/{dead/test => test/dead}/fingerprint.cpp (100%) rename src/{dead/test => test/dead}/gate.cpp (100%) rename src/{dead/test => test/dead}/interval_arithmetic.cpp (100%) rename src/test/{ => dead}/qe_defs.cpp (100%) rename src/test/{ => dead}/quant_elim.cpp (100%) rename src/{dead/test => test/dead}/relevancy.cpp (100%) rename src/{dead/test => test/dead}/sat.cpp (100%) rename src/{dead/test => test/dead}/simplex_polynomial.cpp (100%) rename src/test/{ => dead}/symmetry.cpp (100%) rename src/{dead/test => test/dead}/template_models.cpp (100%) rename src/{dead/test => test/dead}/th_propagation.cpp (100%) rename src/{dead/test => test/dead}/trail.cpp (100%) rename src/{dead/test => test/dead}/watch_list.cpp (100%) delete mode 100644 src/test/dl_rule_set.cpp delete mode 100644 src/test/expr_delta.cpp delete mode 100644 src/test/expr_pattern_match.cpp delete mode 100644 src/test/grobner.cpp delete mode 100644 src/test/smtparser.cpp diff --git a/src/test/ast_pp.cpp b/src/test/ast_pp.cpp deleted file mode 100644 index 414b26411..000000000 --- a/src/test/ast_pp.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - tst_ast_pp.cpp - -Abstract: - - Test AST Pretty printing module - -Author: - - Nikolaj Bjorner (nbjorner) 2006-10-5 - -Revision History: - ---*/ -#include "ast.h" -#include "ast_pp.h" -#include "ast_dag_pp.h" -#include "smtparser.h" -#include - -void tst_ast_pp() -{ - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - - parser->initialize_smtlib(); - - - if (!parser->parse_string( - "(benchmark test :extrasorts (A B) :extrafuns ((f A A) (g A A A) (x A) (p A bool)) \n" - ":formula (p (f x))\n" - ":extrafuns ((x1 Int) (y1 Int))\n" - ":formula (<= 1 (+ x1 y1))\n" - ":formula (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (p (g x x))))))\n" - ":formula (p x)\n" - ")")) { - SASSERT(false); - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - - for (unsigned j = 0; j < b->get_num_assumptions(); ++j) { - expr* e = b->get_assumptions()[j]; - std::cout << mk_pp(e, m) << "\n"; - ast_dag_pp(std::cout, m, e); - } - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr* e = b->begin_formulas()[j]; - std::cout << mk_pp(e, m) << "\n"; - ast_dag_pp(std::cout, m, e); - } - dealloc(parser); -} diff --git a/src/test/ast_smt_pp.cpp b/src/test/ast_smt_pp.cpp deleted file mode 100644 index 05fd5748e..000000000 --- a/src/test/ast_smt_pp.cpp +++ /dev/null @@ -1,90 +0,0 @@ -/*++ -Copyright (c) 2008 Microsoft Corporation - -Module Name: - - tst_ast_smt_pp.cpp - -Abstract: - - Test AST Pretty printing module - -Author: - - Nikolaj Bjorner (nbjorner) 2008-09-04 - -Revision History: - ---*/ -#include "ast.h" -#include "ast_smt_pp.h" -#include "smtparser.h" -#include -#include - -void tst_ast_smt_pp() -{ - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - - parser->initialize_smtlib(); - - - if (!parser->parse_string( - "(benchmark test :extrasorts (A B) :extrafuns ((f A A) (g A A A) (x A) (p A bool)) \n" - ":extrafuns ((arg0 BitVec[8]) (arg1 BitVec[8]) (arg2 BitVec[8]))\n" - ":formula (p (f x))\n" - ":extrafuns ((x1 Int) (y1 Int))\n" - ":formula (<= 1 (+ x1 y1))\n" - ":formula (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (p (g x x))))))\n" - ":formula (p x)\n" - ":formula (bvsge (bvadd arg0 arg2) (extract[7:0] bv3[32]))\n" - ":formula (forall (x Int) (y Int) (z Int) (and (<= 1 x) (<= x y))) \n" - ":formula (forall (x Int) (y Int) (z Int) (and (<= 2 (ite (<= z 1) x (* 2 x))) (<= x y)))\n" - ":formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (<= z 1)) x (* 2 x))) (<= x y)))\n" - ":formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (or (> x y) (<= z 1))) x (* 2 x))) (<= x y)))\n" - ":extrafuns ((a1 Array))\n" - ":formula (= x1 (select (store a1 y1 y1) x1))\n" - ":extrafuns ((a2 Array[32:8]))\n" - ":formula (= arg0 (select a2 bv0[32]))\n" - ":datatypes ((list (cons (car Int) (cdr list)) nil))\n" - ":extrafuns ((a list) (b list) (c list))\n" - ":formula (is_nil nil)\n" - ":datatypes ((list1 (cons1 (car1 Int) (cdr1 list2)) nil1) (list2 (cons1 (car2 list) (cdr2 list1)) nil2) )\n" - ":formula (is_nil2 nil2)\n" - ")")) { - SASSERT(false); - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr* e = b->begin_formulas()[j]; - ast_smt_pp pp(m); - pp.display(std::cout, e); - } - - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr* e = b->begin_formulas()[j]; - - // print and parse formula again. - std::ostringstream buffer; - ast_smt_pp pp(m); - pp.display(buffer, e); - ast_manager m2; - smtlib::parser* parser2 = smtlib::parser::create(m2); - parser2->initialize_smtlib(); - if (!parser2->parse_string(buffer.str().c_str())) { - SASSERT(false); - dealloc(parser2); - return; - } - dealloc(parser2); - } - - - dealloc(parser); -} diff --git a/src/dead/test/ackermanize.cpp b/src/test/dead/ackermanize.cpp similarity index 100% rename from src/dead/test/ackermanize.cpp rename to src/test/dead/ackermanize.cpp diff --git a/src/dead/test/core_theory.cpp b/src/test/dead/core_theory.cpp similarity index 100% rename from src/dead/test/core_theory.cpp rename to src/test/dead/core_theory.cpp diff --git a/src/dead/test/dimacs.cpp b/src/test/dead/dimacs.cpp similarity index 100% rename from src/dead/test/dimacs.cpp rename to src/test/dead/dimacs.cpp diff --git a/src/dead/test/distinct.cpp b/src/test/dead/distinct.cpp similarity index 100% rename from src/dead/test/distinct.cpp rename to src/test/dead/distinct.cpp diff --git a/src/test/expr_context_simplifier.cpp b/src/test/dead/expr_context_simplifier.cpp similarity index 100% rename from src/test/expr_context_simplifier.cpp rename to src/test/dead/expr_context_simplifier.cpp diff --git a/src/dead/test/fingerprint.cpp b/src/test/dead/fingerprint.cpp similarity index 100% rename from src/dead/test/fingerprint.cpp rename to src/test/dead/fingerprint.cpp diff --git a/src/dead/test/gate.cpp b/src/test/dead/gate.cpp similarity index 100% rename from src/dead/test/gate.cpp rename to src/test/dead/gate.cpp diff --git a/src/dead/test/interval_arithmetic.cpp b/src/test/dead/interval_arithmetic.cpp similarity index 100% rename from src/dead/test/interval_arithmetic.cpp rename to src/test/dead/interval_arithmetic.cpp diff --git a/src/test/qe_defs.cpp b/src/test/dead/qe_defs.cpp similarity index 100% rename from src/test/qe_defs.cpp rename to src/test/dead/qe_defs.cpp diff --git a/src/test/quant_elim.cpp b/src/test/dead/quant_elim.cpp similarity index 100% rename from src/test/quant_elim.cpp rename to src/test/dead/quant_elim.cpp diff --git a/src/dead/test/relevancy.cpp b/src/test/dead/relevancy.cpp similarity index 100% rename from src/dead/test/relevancy.cpp rename to src/test/dead/relevancy.cpp diff --git a/src/dead/test/sat.cpp b/src/test/dead/sat.cpp similarity index 100% rename from src/dead/test/sat.cpp rename to src/test/dead/sat.cpp diff --git a/src/dead/test/simplex_polynomial.cpp b/src/test/dead/simplex_polynomial.cpp similarity index 100% rename from src/dead/test/simplex_polynomial.cpp rename to src/test/dead/simplex_polynomial.cpp diff --git a/src/test/symmetry.cpp b/src/test/dead/symmetry.cpp similarity index 100% rename from src/test/symmetry.cpp rename to src/test/dead/symmetry.cpp diff --git a/src/dead/test/template_models.cpp b/src/test/dead/template_models.cpp similarity index 100% rename from src/dead/test/template_models.cpp rename to src/test/dead/template_models.cpp diff --git a/src/dead/test/th_propagation.cpp b/src/test/dead/th_propagation.cpp similarity index 100% rename from src/dead/test/th_propagation.cpp rename to src/test/dead/th_propagation.cpp diff --git a/src/dead/test/trail.cpp b/src/test/dead/trail.cpp similarity index 100% rename from src/dead/test/trail.cpp rename to src/test/dead/trail.cpp diff --git a/src/dead/test/watch_list.cpp b/src/test/dead/watch_list.cpp similarity index 100% rename from src/dead/test/watch_list.cpp rename to src/test/dead/watch_list.cpp diff --git a/src/test/dl_rule_set.cpp b/src/test/dl_rule_set.cpp deleted file mode 100644 index d68bdc3c7..000000000 --- a/src/test/dl_rule_set.cpp +++ /dev/null @@ -1,118 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - dl_rule_set.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-18. - -Revision History: - ---*/ -#include"dl_context.h" -#include"dl_rule_set.h" -#include"dl_mk_filter_rules.h" -#include"dl_mk_simple_joins.h" -#include"smtparser.h" -#include"ast_pp.h" -#include -#include - -void tst_dl_rule_set() { - enable_trace("mk_filter_rules"); - front_end_params params; - ast_manager m; - smtlib::parser * parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - datalog::context ctx(m, params); - datalog::rule_set rs(ctx); - datalog::rule_manager& rm = ctx.get_rule_manager(); - datalog::rule_ref_vector rv(rm); - - - if (!parser->parse_string( - "(benchmark test\n" - ":extrapreds ((T Int Int) (Q Int Int) (R Int Int Int) (S Int Int Int) (DynActual Int Int Int) (GlobalSym Int Int) (HeapPointsTo Int Int Int) (Calls Int Int)) \n" - ":extrapreds ((Actual Int Int Int) (PointsTo Int Int) (PointsTo0 Int Int) (FuncDecl0 Int Int) (Assign Int Int) (Load Int Int Int))\n" - ":formula (forall (x Int) (=> (Q x 1) (T x x)))\n" - ":formula (forall (v Int) (h Int) (=> (PointsTo0 v h) (PointsTo v h)))\n" - ":formula (forall (v Int) (h Int) (=> (FuncDecl0 v h) (PointsTo v h)))\n" - ":formula (forall (v Int) (h Int) (=> (FuncDecl0 v h) (PointsTo v h)))\n" - ":formula (forall (v1 Int) (v2 Int) (h Int) (=> (and (PointsTo v2 h) (Assign v1 v2)) (PointsTo v1 h)))\n" - ":formula (forall (x Int) (y Int) (z Int) (=> (and (Q x y) (T y z)) (T x y)))\n" - ":formula (forall (i1 Int) (v Int) (fun Int) (c Int) (v1 Int) (h Int) (h1 Int) (=> (and (GlobalSym 0 fun) (HeapPointsTo fun 1 c) (Calls i1 c) (Actual i1 3 v1) (PointsTo v1 h) (HeapPointsTo h 0 h1) (PointsTo v h1)) (DynActual i1 2 v)))\n" - ":formula (forall (i1 Int) (v Int) (fun Int) (c Int) (v1 Int) (h Int) (h1 Int) (=> (and (GlobalSym 0 fun) (HeapPointsTo fun 1 c) (Calls i1 c) (Actual i1 3 v1) (PointsTo v1 h) (HeapPointsTo h 1 h1) (PointsTo v h1)) (DynActual i1 3 v)))\n" - ":formula (forall (i1 Int) (v Int) (fun Int) (c Int) (v1 Int) (h Int) (h1 Int) (=> (and (GlobalSym 0 fun) (HeapPointsTo fun 1 c) (Calls i1 c) (Actual i1 3 v1) (PointsTo v1 h) (HeapPointsTo h 2 h1) (PointsTo v h1)) (DynActual i1 4 v)))\n" - ":formula (forall (v1 Int) (v2 Int) (h1 Int) (h2 Int) (f Int) (=> (and (Load v2 v1 f) (PointsTo v1 h1) (HeapPointsTo h1 f h2)) (PointsTo v2 h1)))\n" - ":formula (forall (v1 Int) (v2 Int) (h1 Int) (h2 Int) (f Int) (=> (and (Load v2 v1 0) (HeapPointsTo h1 f h2)) (PointsTo v2 h1)))\n" - ":formula (forall (v1 Int) (v2 Int) (h1 Int) (h2 Int) (f Int) (=> (and (not (Load v2 v1 0)) (HeapPointsTo h1 f h2)) (PointsTo v2 h1)))\n" - ")")) { - SASSERT(false); - dealloc(parser); - return; - } - - smtlib::benchmark * b = parser->get_benchmark(); - - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr * e = b->begin_formulas()[j]; - ptr_vector todo; - todo.push_back(e); - while (!todo.empty()) { - e = todo.back(); - todo.pop_back(); - if (is_quantifier(e)) { - e = to_quantifier(e)->get_expr(); - todo.push_back(e); - } - else if (is_app(e)) { - app* a = to_app(e); - if (is_uninterp(e) && !ctx.is_predicate(a->get_decl())) { - std::cout << "registering " << a->get_decl()->get_name() << "\n"; - - ctx.register_predicate(a->get_decl()); - } - else { - todo.append(a->get_num_args(), a->get_args()); - } - } - } - } - - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr * e = b->begin_formulas()[j]; - if (is_quantifier(e)) { - try { - rm.mk_rule(e, rv); - } - catch(...) { - std::cerr << "ERROR: it is not a valid Datalog rule:\n" << mk_pp(e, m) << "\n"; - } - } - } - rs.add_rules(rv.size(), rv.c_ptr()); - rs.display(std::cout); - - datalog::mk_filter_rules p(ctx); - model_converter_ref mc; - proof_converter_ref pc; - datalog::rule_set * new_rs = p(rs, mc, pc); - std::cout << "\nAfter mk_filter:\n"; - new_rs->display(std::cout); - datalog::mk_simple_joins p2(ctx); - datalog::rule_set * new_rs2 = p2(*new_rs, mc, pc); - std::cout << "\nAfter mk_simple_joins:\n"; - new_rs2->display(std::cout); - dealloc(new_rs); - dealloc(new_rs2); - dealloc(parser); -} diff --git a/src/test/expr_delta.cpp b/src/test/expr_delta.cpp deleted file mode 100644 index fae80336d..000000000 --- a/src/test/expr_delta.cpp +++ /dev/null @@ -1,127 +0,0 @@ -#include "expr_delta.h" -#include "smtparser.h" -#include "ast_pp.h" -#include "ast_smt_pp.h" - -static void iterate_delta(ast_manager& m, expr_delta& delta) { - unsigned n = 0; - expr_ref_vector result(m); - std::cout << "Delta\n"; - while (true) { - result.reset(); - if (!delta.delta_dfs(n, result)) { - return; - } - std::cout << n << ": "; - for (unsigned i = 0; i < result.size(); ++i) { - std::cout << mk_pp(result[i].get(), m) << " "; - } - std::cout << "\n"; - n++; - } -} - -void tst_expr_delta1() { - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - - parser->parse_string( - "(benchmark samples :logic QF_LIA \n" - " :extrafuns ((a Int) (b Int) (c Int)) \n" - " :assumption (> a 0) \n" - " :assumption (> b 0) \n" - " :formula (forall (x Int) (y Int) (z Int) (and (<= 1 x) (<= x y))) \n" - " :formula (forall (x Int) (y Int) (z Int) (and (<= 2 (ite (<= z 1) x (* 2 x))) (<= x y)))\n" - " :formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (<= z 1)) x (* 2 x))) (<= x y)))\n" - " :formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (or (> x y) (<= z 1))) x (* 2 x))) (<= x y)))\n" - ")" - ); - - smtlib::benchmark* b = parser->get_benchmark(); - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr_delta delta(m); - - for (unsigned i = 0; i < b->get_num_assumptions(); ++i) { - delta.assert_cnstr(b->get_assumptions()[i]); - } - delta.assert_cnstr(b->begin_formulas()[j]); - iterate_delta(m, delta); - } - - dealloc(parser); -} - -static void get_expr_delta(unsigned position, char const* in, char const* out) { - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - - if (!parser->parse_file(in)) { - std::cout << "error parsing file\n"; - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - - SASSERT(b->get_num_formulas() == 1); - expr_delta delta(m); - - for (unsigned i = 0; i < b->get_num_assumptions(); ++i) { - delta.assert_cnstr(b->get_assumptions()[i]); - } - delta.assert_cnstr(b->begin_formulas()[0]); - - - expr_ref_vector result(m); - if (!delta.delta_dfs(position, result)) { - std::cout << "done\n"; - } - else { - ast_smt_pp pp(m); - std::ofstream outf(out); - if (outf.bad() || outf.fail()) { - std::cout << "Could not open output\n"; - } - else { - switch(b->get_status()) { - case smtlib::benchmark::UNKNOWN: - pp.set_status("unknown"); - break; - case smtlib::benchmark::SAT: - pp.set_status("sat"); - break; - case smtlib::benchmark::UNSAT: - pp.set_status("unsat"); - break; - } - pp.set_logic(b->get_logic().str().c_str()); - for (unsigned i = 0; i + 1 < result.size(); ++i) { - pp.add_assumption(result[i].get()); - } - pp.display(outf, result[result.size()-1].get()); - - std::cout << "ok\n"; - } - } - - dealloc(parser); -} - -void tst_expr_delta(char** argv, int argc, int& i) { - if (i + 3 >= argc) { - std::cout << "Usage: \n"; - return; - } - ++i; - unsigned position = atol(argv[i]); - ++i; - char const* in_file = argv[i]; - ++i; - char const* out_file = argv[i]; - - get_expr_delta(position, in_file, out_file); - -} diff --git a/src/test/expr_pattern_match.cpp b/src/test/expr_pattern_match.cpp deleted file mode 100644 index e7088913e..000000000 --- a/src/test/expr_pattern_match.cpp +++ /dev/null @@ -1,51 +0,0 @@ -#include "expr_pattern_match.h" -#include "smtparser.h" -#include "ast_pp.h" -#include "arith_decl_plugin.h" -#include "bv_decl_plugin.h" -#include "array_decl_plugin.h" -#include "reg_decl_plugins.h" - -void tst_expr_pattern_match() { - ast_manager manager; - reg_decl_plugins(manager); - - expr_pattern_match apm(manager); - - apm.display(std::cout); - - const char* test_string = "(benchmark patterns :status unknown :logic ALL \n" - ":extrasorts (S) \n" - ":extrafuns ((R S S bool)) \n" - ":formula (forall (x S) (y S) (z S) \n" - " (or (not (R x y)) (not (R y z)) (R x z)) \n" - " ; :pats { (R x y) (R y z) } \n" - " :weight { 2 } \n" - " )\n" - ")"; - smtlib::parser* parser = smtlib::parser::create(manager); - parser->initialize_smtlib(); - std::cout << "parsing test string\n"; - if (!parser->parse_string(test_string)) { - UNREACHABLE(); - } - std::cout << "test string parsed\n"; - smtlib::benchmark* bench = parser->get_benchmark(); - - for (unsigned i = 0; i < bench->get_num_formulas(); ++i) { - expr* fml = bench->begin_formulas()[i]; - SASSERT(fml->get_kind() == AST_QUANTIFIER); - quantifier* qf = to_quantifier(fml); - app_ref_vector patterns(manager); - unsigned weight = 0; - if (apm.match_quantifier(qf, patterns, weight)) { - std::cout << "Found pattern match\n"; - for (unsigned i = 0; i < patterns.size(); ++i) { - ast_pp(std::cout, patterns[i].get(), manager) << "\n"; - } - std::cout << "weight: " << weight << "\n"; - } - } - dealloc(parser); - -} diff --git a/src/test/grobner.cpp b/src/test/grobner.cpp deleted file mode 100644 index 89aea5049..000000000 --- a/src/test/grobner.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - grobner.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-12-05. - -Revision History: - ---*/ -#include"smtparser.h" -#include"ast_pp.h" -#include"arith_decl_plugin.h" -#include"simplifier.h" -#include"basic_simplifier_plugin.h" -#include"arith_simplifier_plugin.h" -#include"front_end_params.h" -#include"grobner.h" -#include"reg_decl_plugins.h" - -void display_eqs(grobner & gb, v_dependency_manager & dep_m) { - std::cerr << "RESULT:\n"; - ptr_vector eqs; - gb.get_equations(eqs); - ptr_vector::iterator it = eqs.begin(); - ptr_vector::iterator end = eqs.end(); - for (; it != end; ++it) { - grobner::equation * eq = *it; - ptr_vector exs; - v_dependency * d = eq->get_dependency(); - dep_m.linearize(d, exs); - std::cerr << "{"; - ptr_vector::iterator it2 = exs.begin(); - ptr_vector::iterator end2 = exs.end(); - for (bool first = true; it2 != end2; ++it2) { - if (first) first = false; else std::cerr << " "; - std::cerr << *it2; - } - std::cerr << "}, lc: " << eq->is_linear_combination() << ", "; - gb.display_equation(std::cerr, *eq); - } -} - -void tst_grobner(char ** argv, int argc, int & i) { - front_end_params params; - if (i + 1 < argc) { - char const* file_path = argv[i+1]; - - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - reg_decl_plugins(m); - parser->initialize_smtlib(); - - if (!parser->parse_file(file_path)) { - std::cout << "Could not parse file : " << file_path << std::endl; - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - simplifier simp(m); - basic_simplifier_plugin * bp = alloc(basic_simplifier_plugin, m); - simp.register_plugin(bp); - simp.register_plugin(alloc(arith_simplifier_plugin, m, *bp, params)); - arith_util util(m); - v_dependency_manager dep_m; - grobner gb(m, dep_m); - - ptr_vector::const_iterator it = b->begin_axioms(); - ptr_vector::const_iterator end = b->end_axioms(); - for (unsigned idx = 1; it != end; ++it, ++idx) { - expr * ax = *it; - expr_ref s_ax(m); - proof_ref pr(m); - simp(ax, s_ax, pr); - std::cerr << mk_pp(s_ax, m) << "\n"; - if (m.is_eq(s_ax)) - gb.assert_eq(s_ax, dep_m.mk_leaf(reinterpret_cast(idx))); - } - gb.display(std::cerr); - gb.compute_basis(1024); - display_eqs(gb, dep_m); - dealloc(parser); - } -} - diff --git a/src/test/main.cpp b/src/test/main.cpp index e99e96729..acbea0761 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -123,7 +123,6 @@ int main(int argc, char ** argv) { memory::initialize(0); bool do_display_usage = false; parse_cmd_line_args(argc, argv, do_display_usage); - TST_ARGV(grobner); TST(random); TST(vector); TST(symbol_table); @@ -131,23 +130,17 @@ int main(int argc, char ** argv) { TST(symbol); TST(heap); TST(hashtable); - TST_ARGV(smtparser); TST(rational); TST(inf_rational); TST(ast); TST(optional); TST(bit_vector); - TST(ast_pp); - TST(ast_smt_pp); - TST_ARGV(expr_delta); TST(string_buffer); TST(map); TST(diff_logic); TST(uint_set); TST_ARGV(expr_rand); - TST(expr_context_simplifier); TST(ini_file); - TST(expr_pattern_match); TST(list); TST(small_object_allocator); TST(timeout); @@ -157,9 +150,6 @@ int main(int argc, char ** argv) { TST(bit_blaster); TST(var_subst); TST(simple_parser); - TST(symmetry); - TST_ARGV(symmetry_parse); - TST_ARGV(symmetry_prove); TST(api); TST(old_interval); TST(interval_skip_list); @@ -167,10 +157,8 @@ int main(int argc, char ** argv) { TST(memory); TST(get_implied_equalities); TST(arith_simplifier_plugin); - TST(quant_elim); TST(matcher); TST(datalog_parser); - TST(dl_rule_set); TST_ARGV(datalog_parser_file); TST(object_allocator); TST(mpz); @@ -208,7 +196,6 @@ int main(int argc, char ** argv) { TST(prime_generator); TST(permutation); TST(nlsat); - TST(qe_defs); TST(ext_numeral); TST(interval); TST(quant_solve); diff --git a/src/test/smtparser.cpp b/src/test/smtparser.cpp deleted file mode 100644 index dc4f0eb74..000000000 --- a/src/test/smtparser.cpp +++ /dev/null @@ -1,52 +0,0 @@ -#ifdef _WINDOWS -#include -#include -#include -#include -#include "smtparser.h" -#include "for_each_file.h" -#include "array_decl_plugin.h" -#include "bv_decl_plugin.h" -#include "reg_decl_plugins.h" - -class for_each_file_smt : public for_each_file_proc { -public: - for_each_file_smt() {} - - bool operator()(char const * file_path) { - bool result = true; - std::cout << "Parsing: " << file_path << std::endl; - - ast_manager ast_manager; - smtlib::parser* parser = smtlib::parser::create(ast_manager); - reg_decl_plugins(ast_manager); - - parser->initialize_smtlib(); - - if (!parser->parse_file(file_path)) { - std::cout << "Could not parse file : " << file_path << std::endl; - result = false; - } - dealloc(parser); - return result; - } -}; - - -static bool test_directory(char const * base) { - for_each_file_smt foreach; - return for_each_file(foreach, base, "*.smt"); -} - -void tst_smtparser(char** argv, int argc, int & i) { - bool result = true; - if (i + 1 < argc) { - result = test_directory(argv[i+1]); - i += 1; - } - SASSERT(result); -} -#else -void tst_smtparser(char** argv, int argc, int & i) { -} -#endif diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp index efc4555fe..3e75d1527 100644 --- a/src/test/var_subst.cpp +++ b/src/test/var_subst.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include"var_subst.h" -#include"smtparser.h" #include"ast_pp.h" #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" @@ -104,22 +103,4 @@ void tst_var_subst() { ast_manager m; reg_decl_plugins(m); tst_subst(m); - - scoped_ptr parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - - parser->parse_string( - "(benchmark samples :logic AUFLIA\n" - " :extrafuns ((f Int Int) (g Int Int Int) (a Int) (b Int))\n" - " :formula (forall (x Int) (or (= (f x) x) (forall (y Int) (z Int) (= (g x y) (f z)))))\n" - " :formula (forall (x Int) (w Int) (or (= (f x) x) (forall (y Int) (z Int) (or (= (g x y) (g w z)) (forall (x1 Int) (= (f x1) (g x y)))))))\n" - ")" - ); - - smtlib::benchmark* b = parser->get_benchmark(); - - smtlib::theory::expr_iterator it = b->begin_formulas(); - smtlib::theory::expr_iterator end = b->end_formulas(); - for (; it != end; ++it) - tst_instantiate(m, *it); } From f1b6d1c7f33f344cc0f5f7a6101606250e2cf604 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 18:04:20 -0700 Subject: [PATCH 4/7] 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; }; }; From 566ed44033a96d538384b112254ffebd153fccba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 18:11:27 -0700 Subject: [PATCH 5/7] removing 'fat' from smt 1.0 parser Signed-off-by: Leonardo de Moura --- src/api/smtparser.cpp | 13 +------------ src/api/smtparser.h | 10 +++++----- 2 files changed, 6 insertions(+), 17 deletions(-) diff --git a/src/api/smtparser.cpp b/src/api/smtparser.cpp index f290c717b..53dffb28c 100644 --- a/src/api/smtparser.cpp +++ b/src/api/smtparser.cpp @@ -34,13 +34,11 @@ Revision History: #include"warning.h" #include"error_codes.h" #include"pattern_validation.h" -#include"timeit.h" #include"var_subst.h" #include"well_sorted.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 { symbol m_string; @@ -60,7 +58,7 @@ public: class proto_region { ptr_vector m_rationals; - ptr_vector< id_param_info > m_id_infos; + ptr_vector m_id_infos; region m_region; public: proto_region() { } @@ -562,7 +560,6 @@ class smtparser : public parser { bool m_ignore_user_patterns; unsigned m_binding_level; // scope level for bound vars benchmark m_benchmark; // currently parsed benchmark - sort_ref_vector m_pinned_sorts; typedef map op_map; op_map m_builtin_ops; @@ -580,11 +577,8 @@ class smtparser : public parser { symbol m_sorts; symbol m_funs; symbol m_preds; - symbol m_definition; symbol m_axioms; symbol m_notes; - symbol m_theory; - symbol m_language; symbol m_array; symbol m_bang; symbol m_underscore; @@ -610,7 +604,6 @@ public: m_ignore_user_patterns(ignore_user_patterns), m_binding_level(0), m_benchmark(m_manager, symbol("")), - m_pinned_sorts(m), m_let("let"), m_flet("flet"), m_forall("forall"), @@ -623,11 +616,8 @@ public: m_sorts("sorts"), m_funs("funs"), m_preds("preds"), - m_definition("definition"), m_axioms("axioms"), m_notes("notes"), - m_theory("theory"), - m_language("language"), m_array("array"), m_bang("!"), m_underscore("_"), @@ -661,7 +651,6 @@ public: } bool parse_file(char const * filename) { - timeit tt(get_verbosity_level() >= 100, "parsing file"); if (filename != 0) { std::ifstream stream(filename); if (!stream) { diff --git a/src/api/smtparser.h b/src/api/smtparser.h index d593f3f05..dde6068f9 100644 --- a/src/api/smtparser.h +++ b/src/api/smtparser.h @@ -19,11 +19,11 @@ Revision History: #ifndef _SMT_PARSER_H_ #define _SMT_PARSER_H_ -#include "ast.h" -#include "vector.h" -#include "smtlib.h" -#include "z3.h" -#include +#include +#include"ast.h" +#include"vector.h" +#include"smtlib.h" +#include"z3.h" namespace smtlib { class parser { From 1492b81290ef4dbb7a43823d42628ad5f4e6e8c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 18:21:17 -0700 Subject: [PATCH 6/7] moved smt 1.0 parser to its own module Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 3 ++- src/{api => smtparser}/smtlib.cpp | 0 src/{api => smtparser}/smtlib.h | 0 src/{api => smtparser}/smtlib_solver.cpp | 0 src/{api => smtparser}/smtlib_solver.h | 0 src/{api => smtparser}/smtparser.cpp | 0 src/{api => smtparser}/smtparser.h | 1 - 7 files changed, 2 insertions(+), 2 deletions(-) rename src/{api => smtparser}/smtlib.cpp (100%) rename src/{api => smtparser}/smtlib.h (100%) rename src/{api => smtparser}/smtlib_solver.cpp (100%) rename src/{api => smtparser}/smtlib_solver.h (100%) rename src/{api => smtparser}/smtparser.cpp (100%) rename src/{api => smtparser}/smtparser.h (98%) diff --git a/scripts/mk_make.py b/scripts/mk_make.py index e37013745..a79a0034f 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -59,7 +59,8 @@ add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') # TODO: delete SMT 1.0 frontend -add_lib('api', ['portfolio', 'user_plugin']) +add_lib('smtparser', ['portfolio']) +add_lib('api', ['portfolio', 'user_plugin', 'smtparser']) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3') API_files = ['z3_api.h'] diff --git a/src/api/smtlib.cpp b/src/smtparser/smtlib.cpp similarity index 100% rename from src/api/smtlib.cpp rename to src/smtparser/smtlib.cpp diff --git a/src/api/smtlib.h b/src/smtparser/smtlib.h similarity index 100% rename from src/api/smtlib.h rename to src/smtparser/smtlib.h diff --git a/src/api/smtlib_solver.cpp b/src/smtparser/smtlib_solver.cpp similarity index 100% rename from src/api/smtlib_solver.cpp rename to src/smtparser/smtlib_solver.cpp diff --git a/src/api/smtlib_solver.h b/src/smtparser/smtlib_solver.h similarity index 100% rename from src/api/smtlib_solver.h rename to src/smtparser/smtlib_solver.h diff --git a/src/api/smtparser.cpp b/src/smtparser/smtparser.cpp similarity index 100% rename from src/api/smtparser.cpp rename to src/smtparser/smtparser.cpp diff --git a/src/api/smtparser.h b/src/smtparser/smtparser.h similarity index 98% rename from src/api/smtparser.h rename to src/smtparser/smtparser.h index dde6068f9..c63f92664 100644 --- a/src/api/smtparser.h +++ b/src/smtparser/smtparser.h @@ -23,7 +23,6 @@ Revision History: #include"ast.h" #include"vector.h" #include"smtlib.h" -#include"z3.h" namespace smtlib { class parser { From ad9bad9cc1c22cf06d83678c2dd257038be539a0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 18:25:15 -0700 Subject: [PATCH 7/7] created parsers folder Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 6 +++--- src/{smtparser => parsers/smt}/smtlib.cpp | 0 src/{smtparser => parsers/smt}/smtlib.h | 0 src/{smtparser => parsers/smt}/smtlib_solver.cpp | 0 src/{smtparser => parsers/smt}/smtlib_solver.h | 0 src/{smtparser => parsers/smt}/smtparser.cpp | 0 src/{smtparser => parsers/smt}/smtparser.h | 0 src/{smt2parser => parsers/smt2}/smt2parser.cpp | 0 src/{smt2parser => parsers/smt2}/smt2parser.h | 0 src/{smt2parser => parsers/smt2}/smt2scanner.cpp | 0 src/{smt2parser => parsers/smt2}/smt2scanner.h | 0 src/{parser_util => parsers/util}/cost_parser.cpp | 0 src/{parser_util => parsers/util}/cost_parser.h | 0 src/{parser_util => parsers/util}/pattern_validation.cpp | 0 src/{parser_util => parsers/util}/pattern_validation.h | 0 src/{parser_util => parsers/util}/scanner.cpp | 0 src/{parser_util => parsers/util}/scanner.h | 0 src/{parser_util => parsers/util}/simple_parser.cpp | 0 src/{parser_util => parsers/util}/simple_parser.h | 0 19 files changed, 3 insertions(+), 3 deletions(-) rename src/{smtparser => parsers/smt}/smtlib.cpp (100%) rename src/{smtparser => parsers/smt}/smtlib.h (100%) rename src/{smtparser => parsers/smt}/smtlib_solver.cpp (100%) rename src/{smtparser => parsers/smt}/smtlib_solver.h (100%) rename src/{smtparser => parsers/smt}/smtparser.cpp (100%) rename src/{smtparser => parsers/smt}/smtparser.h (100%) rename src/{smt2parser => parsers/smt2}/smt2parser.cpp (100%) rename src/{smt2parser => parsers/smt2}/smt2parser.h (100%) rename src/{smt2parser => parsers/smt2}/smt2scanner.cpp (100%) rename src/{smt2parser => parsers/smt2}/smt2scanner.h (100%) rename src/{parser_util => parsers/util}/cost_parser.cpp (100%) rename src/{parser_util => parsers/util}/cost_parser.h (100%) rename src/{parser_util => parsers/util}/pattern_validation.cpp (100%) rename src/{parser_util => parsers/util}/pattern_validation.h (100%) rename src/{parser_util => parsers/util}/scanner.cpp (100%) rename src/{parser_util => parsers/util}/scanner.h (100%) rename src/{parser_util => parsers/util}/simple_parser.cpp (100%) rename src/{parser_util => parsers/util}/simple_parser.h (100%) diff --git a/scripts/mk_make.py b/scripts/mk_make.py index a79a0034f..1a3a6229a 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -30,8 +30,8 @@ add_lib('old_params', ['model', 'simplifier']) add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier']) add_lib('substitution', ['ast'], 'ast/substitution') add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms') -add_lib('parser_util', ['ast']) -add_lib('smt2parser', ['cmd_context', 'parser_util']) +add_lib('parser_util', ['ast'], 'parsers/util') +add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern') add_lib('macros', ['simplifier', 'old_params'], 'ast/macros') add_lib('grobner', ['ast'], 'math/grobner') @@ -59,7 +59,7 @@ add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') # TODO: delete SMT 1.0 frontend -add_lib('smtparser', ['portfolio']) +add_lib('smtparser', ['portfolio'], 'parsers/smt') add_lib('api', ['portfolio', 'user_plugin', 'smtparser']) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3') diff --git a/src/smtparser/smtlib.cpp b/src/parsers/smt/smtlib.cpp similarity index 100% rename from src/smtparser/smtlib.cpp rename to src/parsers/smt/smtlib.cpp diff --git a/src/smtparser/smtlib.h b/src/parsers/smt/smtlib.h similarity index 100% rename from src/smtparser/smtlib.h rename to src/parsers/smt/smtlib.h diff --git a/src/smtparser/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp similarity index 100% rename from src/smtparser/smtlib_solver.cpp rename to src/parsers/smt/smtlib_solver.cpp diff --git a/src/smtparser/smtlib_solver.h b/src/parsers/smt/smtlib_solver.h similarity index 100% rename from src/smtparser/smtlib_solver.h rename to src/parsers/smt/smtlib_solver.h diff --git a/src/smtparser/smtparser.cpp b/src/parsers/smt/smtparser.cpp similarity index 100% rename from src/smtparser/smtparser.cpp rename to src/parsers/smt/smtparser.cpp diff --git a/src/smtparser/smtparser.h b/src/parsers/smt/smtparser.h similarity index 100% rename from src/smtparser/smtparser.h rename to src/parsers/smt/smtparser.h diff --git a/src/smt2parser/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp similarity index 100% rename from src/smt2parser/smt2parser.cpp rename to src/parsers/smt2/smt2parser.cpp diff --git a/src/smt2parser/smt2parser.h b/src/parsers/smt2/smt2parser.h similarity index 100% rename from src/smt2parser/smt2parser.h rename to src/parsers/smt2/smt2parser.h diff --git a/src/smt2parser/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp similarity index 100% rename from src/smt2parser/smt2scanner.cpp rename to src/parsers/smt2/smt2scanner.cpp diff --git a/src/smt2parser/smt2scanner.h b/src/parsers/smt2/smt2scanner.h similarity index 100% rename from src/smt2parser/smt2scanner.h rename to src/parsers/smt2/smt2scanner.h diff --git a/src/parser_util/cost_parser.cpp b/src/parsers/util/cost_parser.cpp similarity index 100% rename from src/parser_util/cost_parser.cpp rename to src/parsers/util/cost_parser.cpp diff --git a/src/parser_util/cost_parser.h b/src/parsers/util/cost_parser.h similarity index 100% rename from src/parser_util/cost_parser.h rename to src/parsers/util/cost_parser.h diff --git a/src/parser_util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp similarity index 100% rename from src/parser_util/pattern_validation.cpp rename to src/parsers/util/pattern_validation.cpp diff --git a/src/parser_util/pattern_validation.h b/src/parsers/util/pattern_validation.h similarity index 100% rename from src/parser_util/pattern_validation.h rename to src/parsers/util/pattern_validation.h diff --git a/src/parser_util/scanner.cpp b/src/parsers/util/scanner.cpp similarity index 100% rename from src/parser_util/scanner.cpp rename to src/parsers/util/scanner.cpp diff --git a/src/parser_util/scanner.h b/src/parsers/util/scanner.h similarity index 100% rename from src/parser_util/scanner.h rename to src/parsers/util/scanner.h diff --git a/src/parser_util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp similarity index 100% rename from src/parser_util/simple_parser.cpp rename to src/parsers/util/simple_parser.cpp diff --git a/src/parser_util/simple_parser.h b/src/parsers/util/simple_parser.h similarity index 100% rename from src/parser_util/simple_parser.h rename to src/parsers/util/simple_parser.h