From d8d869822fbe4026e7e9311a6bac8f0a62fdf091 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 10 Jan 2017 21:04:44 +0000 Subject: [PATCH] Cleaned up #include in api* objects. --- scripts/update_api.py | 1 + src/api/api_algebraic.cpp | 39 ++++++------ src/api/api_arith.cpp | 25 ++++---- src/api/api_array.cpp | 31 +++++----- src/api/api_bv.cpp | 37 ++++++------ src/api/api_datatype.cpp | 119 ++++++++++++++++++------------------ src/api/api_interp.cpp | 5 +- src/api/api_log.cpp | 1 - src/api/api_pb.cpp | 16 +++-- src/api/api_polynomial.cpp | 5 +- src/api/api_quant.cpp | 121 ++++++++++++++++++------------------- src/api/api_seq.cpp | 37 ++++++------ 12 files changed, 213 insertions(+), 224 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index e531a103c..b8978ff21 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1574,6 +1574,7 @@ def write_log_h_preamble(log_h): log_h.write('#define _Z3_UNUSED\n') log_h.write('#endif\n') # + log_h.write('#include\n') log_h.write('extern std::ostream * g_z3_log;\n') log_h.write('extern bool g_z3_log_enabled;\n') log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx():m_prev(g_z3_log_enabled) { g_z3_log_enabled = false; } ~z3_log_ctx() { g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n') diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index 2e14a1bd8..c4e4dac5d 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - Additional APIs for handling Z3 algebraic numbers encoded as + Additional APIs for handling Z3 algebraic numbers encoded as Z3_ASTs Author: @@ -15,9 +15,8 @@ Author: Leonardo de Moura (leonardo) 2012-12-07 Notes: - + --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -74,9 +73,9 @@ extern "C" { bool Z3_algebraic_is_value_core(Z3_context c, Z3_ast a) { api::context * _c = mk_c(c); - return - is_expr(a) && - (_c->autil().is_numeral(to_expr(a)) || + return + is_expr(a) && + (_c->autil().is_numeral(to_expr(a)) || _c->autil().is_irrational_algebraic_numeral(to_expr(a))); } @@ -162,9 +161,9 @@ extern "C" { Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b) { Z3_TRY; LOG_Z3_algebraic_add(c, a, b); - RESET_ERROR_CODE(); - CHECK_IS_ALGEBRAIC_X(a, 0); - CHECK_IS_ALGEBRAIC_X(b, 0); + RESET_ERROR_CODE(); + CHECK_IS_ALGEBRAIC_X(a, 0); + CHECK_IS_ALGEBRAIC_X(b, 0); BIN_OP(+,add); Z3_CATCH_RETURN(0); } @@ -172,9 +171,9 @@ extern "C" { Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b) { Z3_TRY; LOG_Z3_algebraic_sub(c, a, b); - RESET_ERROR_CODE(); - CHECK_IS_ALGEBRAIC_X(a, 0); - CHECK_IS_ALGEBRAIC_X(b, 0); + RESET_ERROR_CODE(); + CHECK_IS_ALGEBRAIC_X(a, 0); + CHECK_IS_ALGEBRAIC_X(b, 0); BIN_OP(-,sub); Z3_CATCH_RETURN(0); } @@ -182,9 +181,9 @@ extern "C" { Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b) { Z3_TRY; LOG_Z3_algebraic_mul(c, a, b); - RESET_ERROR_CODE(); - CHECK_IS_ALGEBRAIC_X(a, 0); - CHECK_IS_ALGEBRAIC_X(b, 0); + RESET_ERROR_CODE(); + CHECK_IS_ALGEBRAIC_X(a, 0); + CHECK_IS_ALGEBRAIC_X(b, 0); BIN_OP(*,mul); Z3_CATCH_RETURN(0); } @@ -219,8 +218,8 @@ extern "C" { algebraic_numbers::manager & _am = am(c); scoped_anum _r(_am); if (is_rational(c, a)) { - scoped_anum av(_am); - _am.set(av, get_rational(c, a).to_mpq()); + scoped_anum av(_am); + _am.set(av, get_rational(c, a).to_mpq()); _am.root(av, k, _r); } else { @@ -241,8 +240,8 @@ extern "C" { algebraic_numbers::manager & _am = am(c); scoped_anum _r(_am); if (is_rational(c, a)) { - scoped_anum av(_am); - _am.set(av, get_rational(c, a).to_mpq()); + scoped_anum av(_am); + _am.set(av, get_rational(c, a).to_mpq()); _am.power(av, k, _r); } else { @@ -328,7 +327,7 @@ extern "C" { scoped_anum tmp(_am); for (unsigned i = 0; i < n; i++) { if (is_rational(c, a[i])) { - _am.set(tmp, get_rational(c, a[i]).to_mpq()); + _am.set(tmp, get_rational(c, a[i]).to_mpq()); as.push_back(tmp); } else if (is_irrational(c, a[i])) { diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index dcd250c98..51aea9676 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -15,7 +15,6 @@ Author: Revision History: --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -37,7 +36,7 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(0); } - + Z3_sort Z3_API Z3_mk_real_sort(Z3_context c) { Z3_TRY; LOG_Z3_mk_real_sort(c); @@ -50,7 +49,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den) { Z3_TRY; LOG_Z3_mk_real(c, num, den); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); if (den == 0) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); @@ -60,7 +59,7 @@ extern "C" { RETURN_Z3(of_ast(a)); Z3_CATCH_RETURN(0); } - + MK_ARITH_OP(Z3_mk_add, OP_ADD); MK_ARITH_OP(Z3_mk_mul, OP_MUL); MK_BINARY_ARITH_OP(Z3_mk_power, OP_POWER); @@ -70,17 +69,17 @@ extern "C" { Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast n1, Z3_ast n2) { Z3_TRY; LOG_Z3_mk_div(c, n1, n2); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); decl_kind k = OP_IDIV; sort* ty = mk_c(c)->m().get_sort(to_expr(n1)); sort* real_ty = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); if (ty == real_ty) { k = OP_DIV; } - expr * args[2] = { to_expr(n1), to_expr(n2) }; - ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), k, 0, 0, 2, args); - mk_c(c)->save_ast_trail(a); - check_sorts(c, a); + expr * args[2] = { to_expr(n1), to_expr(n2) }; + ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), k, 0, 0, 2, args); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); RETURN_Z3(of_ast(a)); Z3_CATCH_RETURN(0); } @@ -142,7 +141,7 @@ extern "C" { rational l; mk_c(c)->autil().am().get_lower(val, l, precision); expr * r = mk_c(c)->autil().mk_numeral(l, false); - mk_c(c)->save_ast_trail(r); + mk_c(c)->save_ast_trail(r); RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(0); } @@ -160,7 +159,7 @@ extern "C" { rational l; mk_c(c)->autil().am().get_upper(val, l, precision); expr * r = mk_c(c)->autil().mk_numeral(l, false); - mk_c(c)->save_ast_trail(r); + mk_c(c)->save_ast_trail(r); RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(0); } @@ -176,7 +175,7 @@ extern "C" { RETURN_Z3(0); } expr * r = mk_c(c)->autil().mk_numeral(numerator(val), true); - mk_c(c)->save_ast_trail(r); + mk_c(c)->save_ast_trail(r); RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(0); } @@ -192,7 +191,7 @@ extern "C" { RETURN_Z3(0); } expr * r = mk_c(c)->autil().mk_numeral(denominator(val), true); - mk_c(c)->save_ast_trail(r); + mk_c(c)->save_ast_trail(r); RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(0); } diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index d3dda5d9d..ed431882e 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -15,7 +15,6 @@ Author: Revision History: --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -27,7 +26,7 @@ extern "C" { Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range) { Z3_TRY; LOG_Z3_mk_array_sort(c, domain, range); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); parameter params[2] = { parameter(to_sort(domain)), parameter(to_sort(range)) }; sort * ty = mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, 2, params); mk_c(c)->save_ast_trail(ty); @@ -57,7 +56,7 @@ extern "C" { RETURN_Z3(of_ast(r)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) { Z3_TRY; LOG_Z3_mk_store(c, a, i, v); @@ -82,7 +81,7 @@ extern "C" { RETURN_Z3(of_ast(r)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) { Z3_TRY; LOG_Z3_mk_map(c, f, n, args); @@ -94,7 +93,7 @@ extern "C" { ast_manager & m = mk_c(c)->m(); func_decl* _f = to_func_decl(f); expr* const* _args = to_exprs(args); - + ptr_vector domain; for (unsigned i = 0; i < n; ++i) { domain.push_back(m.get_sort(_args[i])); @@ -111,7 +110,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v) { Z3_TRY; LOG_Z3_mk_const_array(c, domain, v); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); expr * _v = to_expr(v); sort * _range = m.get_sort(_v); @@ -123,14 +122,14 @@ extern "C" { app * r = m.mk_app(cd, 1, &_v); mk_c(c)->save_ast_trail(r); check_sorts(c, r); - RETURN_Z3(of_ast(r)); + RETURN_Z3(of_ast(r)); Z3_CATCH_RETURN(0); } Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array) { Z3_TRY; LOG_Z3_mk_array_default(c, array); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); expr * _a = to_expr(array); @@ -138,12 +137,12 @@ extern "C" { app * r = m.mk_app(f, 1, &_a); mk_c(c)->save_ast_trail(r); check_sorts(c, r); - RETURN_Z3(of_ast(r)); + RETURN_Z3(of_ast(r)); Z3_CATCH_RETURN(0); } Z3_ast mk_app_array_core(Z3_context c, Z3_sort domain, Z3_ast v) { - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); expr * _v = to_expr(v); sort * _range = m.get_sort(_v); @@ -178,7 +177,7 @@ extern "C" { LOG_Z3_mk_full_set(c, domain); RESET_ERROR_CODE(); Z3_ast r = mk_app_array_core(c, domain, Z3_mk_true(c)); - RETURN_Z3(r); + RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -205,8 +204,8 @@ extern "C" { Z3_TRY; LOG_Z3_get_array_sort_domain(c, t); RESET_ERROR_CODE(); - CHECK_VALID_AST(t, 0); - if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && + CHECK_VALID_AST(t, 0); + if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && to_sort(t)->get_decl_kind() == ARRAY_SORT) { Z3_sort r = reinterpret_cast(to_sort(t)->get_parameter(0).get_ast()); RETURN_Z3(r); @@ -215,13 +214,13 @@ extern "C" { RETURN_Z3(0); Z3_CATCH_RETURN(0); } - + Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t) { Z3_TRY; LOG_Z3_get_array_sort_range(c, t); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); CHECK_VALID_AST(t, 0); - if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && + if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() && to_sort(t)->get_decl_kind() == ARRAY_SORT) { Z3_sort r = reinterpret_cast(to_sort(t)->get_parameter(1).get_ast()); RETURN_Z3(r); diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 353cf913c..ff090ef54 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -15,7 +15,6 @@ Author: Revision History: --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -27,7 +26,7 @@ extern "C" { Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz) { Z3_TRY; LOG_Z3_mk_bv_sort(c, sz); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); if (sz == 0) { SET_ERROR_CODE(Z3_INVALID_ARG); } @@ -39,7 +38,7 @@ extern "C" { #define MK_BV_UNARY(NAME, OP) MK_UNARY(NAME, mk_c(c)->get_bv_fid(), OP, SKIP) #define MK_BV_BINARY(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_bv_fid(), OP, SKIP) - + MK_BV_UNARY(Z3_mk_bvnot, OP_BNOT); MK_BV_UNARY(Z3_mk_bvredand, OP_BREDAND); MK_BV_UNARY(Z3_mk_bvredor, OP_BREDOR); @@ -75,11 +74,11 @@ extern "C" { expr * _n = to_expr(n); parameter params[2] = { parameter(high), parameter(low) }; expr * a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_EXTRACT, 2, params, 1, &_n); - mk_c(c)->save_ast_trail(a); + mk_c(c)->save_ast_trail(a); check_sorts(c, a); return of_ast(a); } - + Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast n) { Z3_TRY; LOG_Z3_mk_extract(c, high, low, n); @@ -88,7 +87,7 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(0); } - + #define MK_BV_PUNARY(NAME, OP) \ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_TRY; \ @@ -113,7 +112,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast n, Z3_bool is_signed) { Z3_TRY; LOG_Z3_mk_bv2int(c, n, is_signed); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); Z3_sort int_s = Z3_mk_int_sort(c); if (is_signed) { Z3_ast r = Z3_mk_bv2int(c, n, false); @@ -125,7 +124,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_inc_ref(c, bound); Z3_ast zero = Z3_mk_int(c, 0, s); Z3_inc_ref(c, zero); - Z3_ast pred = Z3_mk_bvslt(c, n, zero); + Z3_ast pred = Z3_mk_bvslt(c, n, zero); Z3_inc_ref(c, pred); // if n <_sigend 0 then r - s^sz else r Z3_ast args[2] = { r, bound }; @@ -140,19 +139,19 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ RETURN_Z3(res); } else { - expr * _n = to_expr(n); - parameter p(to_sort(int_s)); - ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_BV2INT, 1, &p, 1, &_n); - mk_c(c)->save_ast_trail(a); - check_sorts(c, a); - RETURN_Z3(of_ast(a)); + expr * _n = to_expr(n); + parameter p(to_sort(int_s)); + ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_BV2INT, 1, &p, 1, &_n); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); + RETURN_Z3(of_ast(a)); } Z3_CATCH_RETURN(0); } /** \brief Create a bit-vector of sort \s with 1 in the most significant bit position. - + The sort \s must be a bit-vector sort. This function is a shorthand for shl(1, N-1) @@ -343,7 +342,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ return Z3_mk_not(c, eq); Z3_CATCH_RETURN(0); } - + // only for signed machine integers Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) { Z3_TRY; @@ -369,7 +368,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ return result; Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast n1, Z3_ast n2) { Z3_TRY; LOG_Z3_mk_bvsub(c, n1, n2); @@ -389,7 +388,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t) { Z3_TRY; LOG_Z3_get_bv_sort_size(c, t); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); CHECK_VALID_AST(t, 0); if (to_sort(t)->get_family_id() == mk_c(c)->get_bv_fid() && to_sort(t)->get_decl_kind() == BV_SORT) { return to_sort(t)->get_parameter(0).get_int(); @@ -398,5 +397,5 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ return 0; Z3_CATCH_RETURN(0); } - + }; diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 706ba9d89..5096c8e80 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -15,7 +15,6 @@ Author: Revision History: --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -24,16 +23,16 @@ Revision History: extern "C" { - Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, + Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol name, - unsigned num_fields, + unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl * mk_tuple_decl, Z3_func_decl proj_decls[]) { Z3_TRY; LOG_Z3_mk_tuple_sort(c, name, num_fields, field_names, field_sorts, mk_tuple_decl, proj_decls); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); mk_c(c)->reset_last_result(); ast_manager& m = mk_c(c)->m(); datatype_util& dt_util = mk_c(c)->dtutil(); @@ -43,14 +42,14 @@ extern "C" { std::string recognizer_s("is_"); recognizer_s += to_symbol(name).str(); symbol recognizer(recognizer_s.c_str()); - + ptr_vector acc; for (unsigned i = 0; i < num_fields; ++i) { acc.push_back(mk_accessor_decl(to_symbol(field_names[i]), type_ref(to_sort(field_sorts[i])))); } constructor_decl* constrs[1] = { mk_constructor_decl(to_symbol(name), recognizer, acc.size(), acc.c_ptr()) }; - + { datatype_decl * dt = mk_datatype_decl(to_symbol(name), 1, constrs); bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, tuples); @@ -63,7 +62,7 @@ extern "C" { } // create tuple type - SASSERT(tuples.size() == 1); + SASSERT(tuples.size() == 1); tuple = tuples[0].get(); mk_c(c)->save_multiple_ast_trail(tuple); @@ -72,9 +71,9 @@ extern "C" { SASSERT(!dt_util.is_recursive(tuple)); ptr_vector const * decls = dt_util.get_datatype_constructors(tuple); func_decl* decl = (*decls)[0]; - mk_c(c)->save_multiple_ast_trail(decl); + mk_c(c)->save_multiple_ast_trail(decl); *mk_tuple_decl = of_func_decl(decl); - + // Create projections ptr_vector const * accs = dt_util.get_constructor_accessors(decl); if (!accs) { @@ -90,8 +89,8 @@ extern "C" { RETURN_Z3_mk_tuple_sort(of_sort(tuple)); Z3_CATCH_RETURN(0); } - - Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, + + Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], @@ -106,7 +105,7 @@ extern "C" { sort_ref_vector sorts(m); sort* e; - + ptr_vector constrs; for (unsigned i = 0; i < n; ++i) { symbol e_name(to_symbol(enum_names[i])); @@ -128,9 +127,9 @@ extern "C" { RETURN_Z3(0); } } - + // create enum type. - SASSERT(sorts.size() == 1); + SASSERT(sorts.size() == 1); e = sorts[0].get(); mk_c(c)->save_multiple_ast_trail(e); @@ -141,10 +140,10 @@ extern "C" { SASSERT(decls && decls->size() == n); for (unsigned i = 0; i < n; ++i) { func_decl* decl = (*decls)[i]; - mk_c(c)->save_multiple_ast_trail(decl); + mk_c(c)->save_multiple_ast_trail(decl); enum_consts[i] = of_func_decl(decl); decl = dt_util.get_constructor_recognizer(decl); - mk_c(c)->save_multiple_ast_trail(decl); + mk_c(c)->save_multiple_ast_trail(decl); enum_testers[i] = of_func_decl(decl); } @@ -168,11 +167,11 @@ extern "C" { ast_manager& m = mk_c(c)->m(); mk_c(c)->reset_last_result(); datatype_util data_util(m); - accessor_decl* head_tail[2] = { + accessor_decl* head_tail[2] = { mk_accessor_decl(symbol("head"), type_ref(to_sort(elem_sort))), mk_accessor_decl(symbol("tail"), type_ref(0)) }; - constructor_decl* constrs[2] = { + constructor_decl* constrs[2] = { mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, 0), // Leo: SMT 2.0 document uses 'insert' instead of cons mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail) @@ -197,22 +196,22 @@ extern "C" { func_decl* f; if (nil_decl) { f = cnstrs[0]; - mk_c(c)->save_multiple_ast_trail(f); + mk_c(c)->save_multiple_ast_trail(f); *nil_decl = of_func_decl(f); } if (is_nil_decl) { f = data_util.get_constructor_recognizer(cnstrs[0]); - mk_c(c)->save_multiple_ast_trail(f); + mk_c(c)->save_multiple_ast_trail(f); *is_nil_decl = of_func_decl(f); } if (cons_decl) { f = cnstrs[1]; - mk_c(c)->save_multiple_ast_trail(f); + mk_c(c)->save_multiple_ast_trail(f); *cons_decl = of_func_decl(f); } if (is_cons_decl) { f = data_util.get_constructor_recognizer(cnstrs[1]); - mk_c(c)->save_multiple_ast_trail(f); + mk_c(c)->save_multiple_ast_trail(f); *is_cons_decl = of_func_decl(f); } if (head_decl) { @@ -220,7 +219,7 @@ extern "C" { SASSERT(acc); SASSERT(acc->size() == 2); f = (*acc)[0]; - mk_c(c)->save_multiple_ast_trail(f); + mk_c(c)->save_multiple_ast_trail(f); *head_decl = of_func_decl(f); } if (tail_decl) { @@ -228,7 +227,7 @@ extern "C" { SASSERT(acc); SASSERT(acc->size() == 2); f = (*acc)[1]; - mk_c(c)->save_multiple_ast_trail(f); + mk_c(c)->save_multiple_ast_trail(f); *tail_decl = of_func_decl(f); } RETURN_Z3_mk_list_sort(of_sort(s)); @@ -255,7 +254,7 @@ extern "C" { ) { Z3_TRY; LOG_Z3_mk_constructor(c, name, tester, num_fields, field_names, sorts, sort_refs); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); constructor* cnstr = alloc(constructor, m); cnstr->m_name = to_symbol(name); @@ -291,7 +290,7 @@ extern "C" { if (!f) { SET_ERROR_CODE(Z3_INVALID_ARG); return; - } + } if (constructor_decl) { mk_c(c)->save_multiple_ast_trail(f); *constructor_decl = of_func_decl(f); @@ -301,15 +300,15 @@ extern "C" { mk_c(c)->save_multiple_ast_trail(f2); *tester = of_func_decl(f2); } - + ptr_vector const* accs = data_util.get_constructor_accessors(f); if (!accs && num_fields > 0) { SET_ERROR_CODE(Z3_INVALID_ARG); - return; + return; } for (unsigned i = 0; i < num_fields; ++i) { func_decl* f2 = (*accs)[i]; - mk_c(c)->save_multiple_ast_trail(f2); + mk_c(c)->save_multiple_ast_trail(f2); accessors[i] = of_func_decl(f2); } RETURN_Z3_query_constructor; @@ -324,7 +323,7 @@ extern "C" { Z3_CATCH; } - static datatype_decl* mk_datatype_decl(Z3_context c, + static datatype_decl* mk_datatype_decl(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[]) { @@ -342,7 +341,7 @@ extern "C" { } constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.c_ptr())); } - return mk_datatype_decl(to_symbol(name), num_constructors, constrs.c_ptr()); + return mk_datatype_decl(to_symbol(name), num_constructors, constrs.c_ptr()); } Z3_sort Z3_API Z3_mk_datatype(Z3_context c, @@ -352,9 +351,9 @@ extern "C" { Z3_TRY; LOG_Z3_mk_datatype(c, name, num_constructors, constructors); RESET_ERROR_CODE(); - ast_manager& m = mk_c(c)->m(); + ast_manager& m = mk_c(c)->m(); datatype_util data_util(m); - + sort_ref_vector sorts(m); { datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors); @@ -370,7 +369,7 @@ extern "C" { mk_c(c)->save_ast_trail(s); ptr_vector const* cnstrs = data_util.get_datatype_constructors(s); - + for (unsigned i = 0; i < num_constructors; ++i) { constructor* cn = reinterpret_cast(constructors[i]); cn->m_constructor = (*cnstrs)[i]; @@ -411,7 +410,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_datatypes(c, num_sorts, sort_names, sorts, constructor_lists); RESET_ERROR_CODE(); - ast_manager& m = mk_c(c)->m(); + ast_manager& m = mk_c(c)->m(); mk_c(c)->reset_last_result(); datatype_util data_util(m); @@ -423,7 +422,7 @@ extern "C" { sort_ref_vector _sorts(m); bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), _sorts); del_datatype_decls(datas.size(), datas.c_ptr()); - + if (!ok) { SET_ERROR_CODE(Z3_INVALID_ARG); return; @@ -437,8 +436,8 @@ extern "C" { constructor_list* cl = reinterpret_cast(constructor_lists[i]); ptr_vector const* cnstrs = data_util.get_datatype_constructors(s); for (unsigned j = 0; j < cl->size(); ++j) { - constructor* cn = (*cl)[j]; - cn->m_constructor = (*cnstrs)[j]; + constructor* cn = (*cl)[j]; + cn->m_constructor = (*cnstrs)[j]; } } RETURN_Z3_mk_datatypes; @@ -452,15 +451,15 @@ extern "C" { CHECK_VALID_AST(t, 0); sort * _t = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); - + if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); - return 0; + return 0; } ptr_vector const * decls = dt_util.get_datatype_constructors(_t); if (!decls) { SET_ERROR_CODE(Z3_INVALID_ARG); - return 0; + return 0; } return decls->size(); Z3_CATCH_RETURN(0); @@ -468,7 +467,7 @@ extern "C" { Z3_func_decl get_datatype_sort_constructor_core(Z3_context c, Z3_sort t, unsigned idx) { RESET_ERROR_CODE(); - CHECK_VALID_AST(t, 0); + CHECK_VALID_AST(t, 0); sort * _t = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { @@ -497,10 +496,10 @@ extern "C" { Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx) { Z3_TRY; LOG_Z3_get_datatype_sort_recognizer(c, t, idx); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); sort * _t = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); - + if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); @@ -520,13 +519,13 @@ extern "C" { Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a) { Z3_TRY; LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); sort * _t = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); - + if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); + RETURN_Z3(0); } ptr_vector const * decls = dt_util.get_datatype_constructors(_t); if (!decls || idx_c >= decls->size()) { @@ -536,24 +535,24 @@ extern "C" { func_decl* decl = (*decls)[idx_c]; if (decl->get_arity() <= idx_a) { SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); + RETURN_Z3(0); } ptr_vector const * accs = dt_util.get_constructor_accessors(decl); SASSERT(accs && accs->size() == decl->get_arity()); if (!accs || accs->size() <= idx_a) { SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); + RETURN_Z3(0); } decl = (*accs)[idx_a]; mk_c(c)->save_ast_trail(decl); - RETURN_Z3(of_func_decl(decl)); + RETURN_Z3(of_func_decl(decl)); Z3_CATCH_RETURN(0); } Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t) { Z3_TRY; LOG_Z3_get_tuple_sort_mk_decl(c, t); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); sort * tuple = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { @@ -564,34 +563,34 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(0); } - + unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t) { Z3_TRY; LOG_Z3_get_tuple_sort_num_fields(c, t); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); sort * tuple = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); - return 0; + return 0; } ptr_vector const * decls = dt_util.get_datatype_constructors(tuple); if (!decls || decls->size() != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); - return 0; + return 0; } ptr_vector const * accs = dt_util.get_constructor_accessors((*decls)[0]); if (!accs) { - return 0; + return 0; } return accs->size(); Z3_CATCH_RETURN(0); } - + Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i) { Z3_TRY; LOG_Z3_get_tuple_sort_field_decl(c, t, i); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); sort * tuple = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { @@ -619,14 +618,14 @@ extern "C" { } Z3_ast Z3_datatype_update_field( - Z3_context c, Z3_func_decl f, Z3_ast t, Z3_ast v) { + Z3_context c, Z3_func_decl f, Z3_ast t, Z3_ast v) { Z3_TRY; LOG_Z3_datatype_update_field(c, f, t, v); RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); func_decl* _f = to_func_decl(f); expr* _t = to_expr(t); - expr* _v = to_expr(v); + expr* _v = to_expr(v); expr* args[2] = { _t, _v }; sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) }; parameter param(_f); diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index b14f3db72..10aa06568 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -15,7 +15,6 @@ Revision History: --*/ -#include #include #include #include"z3.h" @@ -375,7 +374,7 @@ extern "C" { for(int i = 0; i < num_theory; i++) fmlas[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),fmlas[i]); std::copy(cnsts,cnsts+num,fmlas.begin()+num_theory); - Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"none","AUFLIA","unknown","",num_fmlas-1,&fmlas[0],fmlas[num_fmlas-1]); + Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"none","AUFLIA","unknown","",num_fmlas-1,&fmlas[0],fmlas[num_fmlas-1]); std::ofstream f(filename); if(num_theory) f << ";! THEORY=" << num_theory << "\n"; @@ -469,7 +468,7 @@ extern "C" { } f.close(); -#if 0 +#if 0 if(!parents){ diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 43cb607c8..43ed98986 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -15,7 +15,6 @@ Author: Revision History: --*/ -#include #include #include"z3.h" #include"api_log_macros.h" diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp index ee504146f..f19fd8661 100644 --- a/src/api/api_pb.cpp +++ b/src/api/api_pb.cpp @@ -15,7 +15,6 @@ Author: Revision History: --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -23,8 +22,8 @@ Revision History: #include"pb_decl_plugin.h" extern "C" { - - Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, + + Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k) { Z3_TRY; LOG_Z3_mk_atmost(c, num_args, args, k); @@ -38,9 +37,8 @@ extern "C" { Z3_CATCH_RETURN(0); } - - Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, - Z3_ast const args[], unsigned k) { + Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, + Z3_ast const args[], unsigned k) { Z3_TRY; LOG_Z3_mk_atmost(c, num_args, args, k); RESET_ERROR_CODE(); @@ -53,7 +51,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, + Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int _coeffs[], int k) { Z3_TRY; @@ -71,7 +69,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, + Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int _coeffs[], int k) { Z3_TRY; @@ -89,7 +87,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, + Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int _coeffs[], int k) { Z3_TRY; diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 979d2ea50..eebe36717 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -14,9 +14,8 @@ Author: Leonardo de Moura (leonardo) 2012-12-08 Notes: - + --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -35,7 +34,7 @@ namespace api { pmanager::~pmanager() { } - + }; extern "C" { diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index ddcd90cca..bf64aa571 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -15,7 +15,6 @@ Author: Revision History: --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -26,17 +25,17 @@ Revision History: extern "C" { Z3_ast Z3_API Z3_mk_quantifier( - Z3_context c, - Z3_bool is_forall, - unsigned weight, - unsigned num_patterns, Z3_pattern const patterns[], - unsigned num_decls, Z3_sort const sorts[], - Z3_symbol const decl_names[], - Z3_ast body) + Z3_context c, + Z3_bool is_forall, + unsigned weight, + unsigned num_patterns, Z3_pattern const patterns[], + unsigned num_decls, Z3_sort const sorts[], + Z3_symbol const decl_names[], + Z3_ast body) { return Z3_mk_quantifier_ex( - c, - is_forall, + c, + is_forall, weight, 0, 0, @@ -50,15 +49,15 @@ extern "C" { } Z3_ast mk_quantifier_ex_core( - Z3_context c, - Z3_bool is_forall, - unsigned weight, + Z3_context c, + Z3_bool is_forall, + unsigned weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, - unsigned num_patterns, Z3_pattern const patterns[], - unsigned num_no_patterns, Z3_ast const no_patterns[], - unsigned num_decls, Z3_sort const sorts[], - Z3_symbol const decl_names[], + unsigned num_patterns, Z3_pattern const patterns[], + unsigned num_no_patterns, Z3_ast const no_patterns[], + unsigned num_decls, Z3_sort const sorts[], + Z3_symbol const decl_names[], Z3_ast body) { Z3_TRY; RESET_ERROR_CODE(); @@ -86,9 +85,9 @@ extern "C" { expr_ref result(mk_c(c)->m()); if (num_decls > 0) { result = mk_c(c)->m().mk_quantifier( - (0 != is_forall), - names.size(), ts, names.c_ptr(), to_expr(body), - weight, + (0 != is_forall), + names.size(), ts, names.c_ptr(), to_expr(body), + weight, to_symbol(quantifier_id), to_symbol(skolem_id), num_patterns, ps, @@ -104,44 +103,44 @@ extern "C" { } Z3_ast Z3_API Z3_mk_quantifier_ex( - Z3_context c, - Z3_bool is_forall, - unsigned weight, + Z3_context c, + Z3_bool is_forall, + unsigned weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, - unsigned num_patterns, Z3_pattern const patterns[], - unsigned num_no_patterns, Z3_ast const no_patterns[], - unsigned num_decls, Z3_sort const sorts[], - Z3_symbol const decl_names[], + unsigned num_patterns, Z3_pattern const patterns[], + unsigned num_no_patterns, Z3_ast const no_patterns[], + unsigned num_decls, Z3_sort const sorts[], + Z3_symbol const decl_names[], Z3_ast body) { - LOG_Z3_mk_quantifier_ex(c, is_forall, weight, quantifier_id, skolem_id, num_patterns, patterns, + LOG_Z3_mk_quantifier_ex(c, is_forall, weight, quantifier_id, skolem_id, num_patterns, patterns, num_no_patterns, no_patterns, num_decls, sorts, decl_names, body); - Z3_ast r = mk_quantifier_ex_core(c, is_forall, weight, quantifier_id, skolem_id, num_patterns, patterns, + Z3_ast r = mk_quantifier_ex_core(c, is_forall, weight, quantifier_id, skolem_id, num_patterns, patterns, num_no_patterns, no_patterns, num_decls, sorts, decl_names, body); RETURN_Z3(r); } - - Z3_ast Z3_API Z3_mk_forall(Z3_context c, - unsigned weight, - unsigned num_patterns, Z3_pattern const patterns[], - unsigned num_decls, Z3_sort const types[], - Z3_symbol const decl_names[], + + Z3_ast Z3_API Z3_mk_forall(Z3_context c, + unsigned weight, + unsigned num_patterns, Z3_pattern const patterns[], + unsigned num_decls, Z3_sort const types[], + Z3_symbol const decl_names[], Z3_ast body) { return Z3_mk_quantifier(c, 1, weight, num_patterns, patterns, num_decls, types, decl_names, body); } - - Z3_ast Z3_API Z3_mk_exists(Z3_context c, - unsigned weight, - unsigned num_patterns, Z3_pattern const patterns[], - unsigned num_decls, Z3_sort const types[], - Z3_symbol const decl_names[], + + Z3_ast Z3_API Z3_mk_exists(Z3_context c, + unsigned weight, + unsigned num_patterns, Z3_pattern const patterns[], + unsigned num_decls, Z3_sort const types[], + Z3_symbol const decl_names[], Z3_ast body) { return Z3_mk_quantifier(c, 0, weight, num_patterns, patterns, num_decls, types, decl_names, body); } - Z3_ast Z3_API Z3_mk_quantifier_const_ex(Z3_context c, + Z3_ast Z3_API Z3_mk_quantifier_const_ex(Z3_context c, Z3_bool is_forall, unsigned weight, Z3_symbol quantifier_id, @@ -166,7 +165,7 @@ extern "C" { } if (num_bound == 0) { SET_ERROR_CODE(Z3_INVALID_USAGE); - RETURN_Z3(0); + RETURN_Z3(0); } for (unsigned i = 0; i < num_bound; ++i) { app* a = to_app(bound[i]); @@ -191,7 +190,7 @@ extern "C" { app* pat = to_pattern(patterns[i]); SASSERT(mk_c(c)->m().is_pattern(pat)); expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.c_ptr(), pat, result); - SASSERT(result.get()->get_kind() == AST_APP); + SASSERT(result.get()->get_kind() == AST_APP); pinned.push_back(result.get()); SASSERT(mk_c(c)->m().is_pattern(result.get())); _patterns.push_back(of_pattern(result.get())); @@ -205,25 +204,25 @@ extern "C" { } app* pat = to_app(to_expr(no_patterns[i])); expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.c_ptr(), pat, result); - SASSERT(result.get()->get_kind() == AST_APP); + SASSERT(result.get()->get_kind() == AST_APP); pinned.push_back(result.get()); _no_patterns.push_back(of_ast(result.get())); } expr_ref abs_body(mk_c(c)->m()); expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.c_ptr(), to_expr(body), abs_body); - Z3_ast result = mk_quantifier_ex_core(c, is_forall, weight, + Z3_ast result = mk_quantifier_ex_core(c, is_forall, weight, quantifier_id, skolem_id, - num_patterns, _patterns.c_ptr(), + num_patterns, _patterns.c_ptr(), num_no_patterns, _no_patterns.c_ptr(), - names.size(), types.c_ptr(), names.c_ptr(), + names.size(), types.c_ptr(), names.c_ptr(), of_ast(abs_body.get())); RETURN_Z3(result); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_quantifier_const(Z3_context c, + Z3_ast Z3_API Z3_mk_quantifier_const(Z3_context c, Z3_bool is_forall, unsigned weight, unsigned num_bound, @@ -231,14 +230,14 @@ extern "C" { unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body) { - return Z3_mk_quantifier_const_ex(c, is_forall, weight, 0, 0, - num_bound, bound, + return Z3_mk_quantifier_const_ex(c, is_forall, weight, 0, 0, + num_bound, bound, num_patterns, patterns, 0, 0, body); } - Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, + Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], @@ -248,7 +247,7 @@ extern "C" { return Z3_mk_quantifier_const(c, true, weight, num_bound, bound, num_patterns, patterns, body); } - Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, + Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], @@ -257,7 +256,7 @@ extern "C" { Z3_ast body) { return Z3_mk_quantifier_const(c, false, weight, num_bound, bound, num_patterns, patterns, body); } - + Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]) { Z3_TRY; LOG_Z3_mk_pattern(c, num_patterns, terms); @@ -273,7 +272,7 @@ extern "C" { RETURN_Z3(of_pattern(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_bound(c, index, ty); @@ -436,7 +435,7 @@ extern "C" { else { SET_ERROR_CODE(Z3_SORT_ERROR); return 0; - } + } Z3_CATCH_RETURN(0); } @@ -450,7 +449,7 @@ extern "C" { } else { SET_ERROR_CODE(Z3_SORT_ERROR); - return 0; + return 0; } Z3_CATCH_RETURN(0); } @@ -471,13 +470,13 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p) { + Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p) { RESET_ERROR_CODE(); - return (Z3_ast)(p); - } + return (Z3_ast)(p); + } Z3_API char const * Z3_pattern_to_string(Z3_context c, Z3_pattern p) { return Z3_ast_to_string(c, reinterpret_cast(p)); } - + }; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 138ea6fb0..478ee6274 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -16,7 +16,6 @@ Author: Revision History: --*/ -#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -28,7 +27,7 @@ extern "C" { Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort domain) { Z3_TRY; LOG_Z3_mk_seq_sort(c, domain); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); sort * ty = mk_c(c)->sutil().str.mk_seq(to_sort(domain)); mk_c(c)->save_ast_trail(ty); RETURN_Z3(of_sort(ty)); @@ -38,7 +37,7 @@ extern "C" { Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort domain) { Z3_TRY; LOG_Z3_mk_re_sort(c, domain); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); sort * ty = mk_c(c)->sutil().re.mk_re(to_sort(domain)); mk_c(c)->save_ast_trail(ty); RETURN_Z3(of_sort(ty)); @@ -48,14 +47,14 @@ extern "C" { Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string str) { Z3_TRY; LOG_Z3_mk_string(c, str); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); zstring s(str, zstring::ascii); app* a = mk_c(c)->sutil().str.mk_string(s); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_ast(a)); Z3_CATCH_RETURN(0); } - + Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) { Z3_TRY; LOG_Z3_mk_string_sort(c); @@ -71,8 +70,8 @@ extern "C" { LOG_Z3_is_seq_sort(c, s); RESET_ERROR_CODE(); bool result = mk_c(c)->sutil().is_seq(to_sort(s)); - return result?Z3_TRUE:Z3_FALSE; - Z3_CATCH_RETURN(Z3_FALSE); + return result?Z3_TRUE:Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); } Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) { @@ -80,8 +79,8 @@ extern "C" { LOG_Z3_is_re_sort(c, s); RESET_ERROR_CODE(); bool result = mk_c(c)->sutil().is_re(to_sort(s)); - return result?Z3_TRUE:Z3_FALSE; - Z3_CATCH_RETURN(Z3_FALSE); + return result?Z3_TRUE:Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); } Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) { @@ -89,8 +88,8 @@ extern "C" { LOG_Z3_is_string_sort(c, s); RESET_ERROR_CODE(); bool result = mk_c(c)->sutil().is_string(to_sort(s)); - return result?Z3_TRUE:Z3_FALSE; - Z3_CATCH_RETURN(Z3_FALSE); + return result?Z3_TRUE:Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); } Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) { @@ -98,7 +97,7 @@ extern "C" { LOG_Z3_is_string(c, s); RESET_ERROR_CODE(); bool result = mk_c(c)->sutil().str.is_string(to_expr(s)); - return result?Z3_TRUE:Z3_FALSE; + return result?Z3_TRUE:Z3_FALSE; Z3_CATCH_RETURN(Z3_FALSE); } @@ -125,7 +124,7 @@ extern "C" { mk_c(c)->save_ast_trail(a); \ RETURN_Z3(of_ast(a)); \ Z3_CATCH_RETURN(0); \ - } + } MK_SORTED(Z3_mk_seq_empty, mk_c(c)->sutil().str.mk_empty); @@ -143,13 +142,13 @@ extern "C" { MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP); Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) { - Z3_TRY; - LOG_Z3_mk_re_loop(c, r, lo, hi); - RESET_ERROR_CODE(); + Z3_TRY; + LOG_Z3_mk_re_loop(c, r, lo, hi); + RESET_ERROR_CODE(); app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_ast(a)); - Z3_CATCH_RETURN(0); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); } MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP);