mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Cleaned up #include<iostream> in api* objects.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-01-10 21:04:44 +00:00
parent 384468bc99
commit d8d869822f
12 changed files with 213 additions and 224 deletions
Download patch file Download diff file Expand all files Collapse all files

1
scripts/update_api.py
View file

@ -1574,6 +1574,7 @@ def write_log_h_preamble(log_h):
log_h.write('#define _Z3_UNUSED\n') log_h.write('#define _Z3_UNUSED\n')
log_h.write('#endif\n') log_h.write('#endif\n')
# #
log_h.write('#include<iostream>\n')
log_h.write('extern std::ostream * g_z3_log;\n') log_h.write('extern std::ostream * g_z3_log;\n')
log_h.write('extern bool g_z3_log_enabled;\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') 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')

39
src/api/api_algebraic.cpp
View file

@ -7,7 +7,7 @@ Module Name:
Abstract: Abstract:
Additional APIs for handling Z3 algebraic numbers encoded as Additional APIs for handling Z3 algebraic numbers encoded as
Z3_ASTs Z3_ASTs
Author: Author:
@ -15,9 +15,8 @@ Author:
Leonardo de Moura (leonardo) 2012-12-07 Leonardo de Moura (leonardo) 2012-12-07
Notes: Notes:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.h" #include"api_context.h"
@ -74,9 +73,9 @@ extern "C" {
bool Z3_algebraic_is_value_core(Z3_context c, Z3_ast a) { bool Z3_algebraic_is_value_core(Z3_context c, Z3_ast a) {
api::context * _c = mk_c(c); api::context * _c = mk_c(c);
return return
is_expr(a) && is_expr(a) &&
(_c->autil().is_numeral(to_expr(a)) || (_c->autil().is_numeral(to_expr(a)) ||
_c->autil().is_irrational_algebraic_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_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY; Z3_TRY;
LOG_Z3_algebraic_add(c, a, b); LOG_Z3_algebraic_add(c, a, b);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0); CHECK_IS_ALGEBRAIC_X(a, 0);
CHECK_IS_ALGEBRAIC_X(b, 0); CHECK_IS_ALGEBRAIC_X(b, 0);
BIN_OP(+,add); BIN_OP(+,add);
Z3_CATCH_RETURN(0); 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_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY; Z3_TRY;
LOG_Z3_algebraic_sub(c, a, b); LOG_Z3_algebraic_sub(c, a, b);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0); CHECK_IS_ALGEBRAIC_X(a, 0);
CHECK_IS_ALGEBRAIC_X(b, 0); CHECK_IS_ALGEBRAIC_X(b, 0);
BIN_OP(-,sub); BIN_OP(-,sub);
Z3_CATCH_RETURN(0); 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_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY; Z3_TRY;
LOG_Z3_algebraic_mul(c, a, b); LOG_Z3_algebraic_mul(c, a, b);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0); CHECK_IS_ALGEBRAIC_X(a, 0);
CHECK_IS_ALGEBRAIC_X(b, 0); CHECK_IS_ALGEBRAIC_X(b, 0);
BIN_OP(*,mul); BIN_OP(*,mul);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -219,8 +218,8 @@ extern "C" {
algebraic_numbers::manager & _am = am(c); algebraic_numbers::manager & _am = am(c);
scoped_anum _r(_am); scoped_anum _r(_am);
if (is_rational(c, a)) { if (is_rational(c, a)) {
scoped_anum av(_am); scoped_anum av(_am);
_am.set(av, get_rational(c, a).to_mpq()); _am.set(av, get_rational(c, a).to_mpq());
_am.root(av, k, _r); _am.root(av, k, _r);
} }
else { else {
@ -241,8 +240,8 @@ extern "C" {
algebraic_numbers::manager & _am = am(c); algebraic_numbers::manager & _am = am(c);
scoped_anum _r(_am); scoped_anum _r(_am);
if (is_rational(c, a)) { if (is_rational(c, a)) {
scoped_anum av(_am); scoped_anum av(_am);
_am.set(av, get_rational(c, a).to_mpq()); _am.set(av, get_rational(c, a).to_mpq());
_am.power(av, k, _r); _am.power(av, k, _r);
} }
else { else {
@ -328,7 +327,7 @@ extern "C" {
scoped_anum tmp(_am); scoped_anum tmp(_am);
for (unsigned i = 0; i < n; i++) { for (unsigned i = 0; i < n; i++) {
if (is_rational(c, a[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); as.push_back(tmp);
} }
else if (is_irrational(c, a[i])) { else if (is_irrational(c, a[i])) {

25
src/api/api_arith.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.h" #include"api_context.h"
@ -37,7 +36,7 @@ extern "C" {
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c) { Z3_sort Z3_API Z3_mk_real_sort(Z3_context c) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_real_sort(c); 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_ast Z3_API Z3_mk_real(Z3_context c, int num, int den) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_real(c, num, den); LOG_Z3_mk_real(c, num, den);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
if (den == 0) { if (den == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
@ -60,7 +59,7 @@ extern "C" {
RETURN_Z3(of_ast(a)); RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
MK_ARITH_OP(Z3_mk_add, OP_ADD); MK_ARITH_OP(Z3_mk_add, OP_ADD);
MK_ARITH_OP(Z3_mk_mul, OP_MUL); MK_ARITH_OP(Z3_mk_mul, OP_MUL);
MK_BINARY_ARITH_OP(Z3_mk_power, OP_POWER); 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_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast n1, Z3_ast n2) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_div(c, n1, n2); LOG_Z3_mk_div(c, n1, n2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
decl_kind k = OP_IDIV; decl_kind k = OP_IDIV;
sort* ty = mk_c(c)->m().get_sort(to_expr(n1)); 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); sort* real_ty = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT);
if (ty == real_ty) { if (ty == real_ty) {
k = OP_DIV; k = OP_DIV;
} }
expr * args[2] = { to_expr(n1), to_expr(n2) }; 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); 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); mk_c(c)->save_ast_trail(a);
check_sorts(c, a); check_sorts(c, a);
RETURN_Z3(of_ast(a)); RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -142,7 +141,7 @@ extern "C" {
rational l; rational l;
mk_c(c)->autil().am().get_lower(val, l, precision); mk_c(c)->autil().am().get_lower(val, l, precision);
expr * r = mk_c(c)->autil().mk_numeral(l, false); 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)); RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -160,7 +159,7 @@ extern "C" {
rational l; rational l;
mk_c(c)->autil().am().get_upper(val, l, precision); mk_c(c)->autil().am().get_upper(val, l, precision);
expr * r = mk_c(c)->autil().mk_numeral(l, false); 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)); RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -176,7 +175,7 @@ extern "C" {
RETURN_Z3(0); RETURN_Z3(0);
} }
expr * r = mk_c(c)->autil().mk_numeral(numerator(val), true); 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)); RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -192,7 +191,7 @@ extern "C" {
RETURN_Z3(0); RETURN_Z3(0);
} }
expr * r = mk_c(c)->autil().mk_numeral(denominator(val), true); 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)); RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }

31
src/api/api_array.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.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_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_array_sort(c, domain, range); 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)) }; 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); 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); mk_c(c)->save_ast_trail(ty);
@ -57,7 +56,7 @@ extern "C" {
RETURN_Z3(of_ast(r)); RETURN_Z3(of_ast(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) { Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_store(c, a, i, v); LOG_Z3_mk_store(c, a, i, v);
@ -82,7 +81,7 @@ extern "C" {
RETURN_Z3(of_ast(r)); RETURN_Z3(of_ast(r));
Z3_CATCH_RETURN(0); 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_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_map(c, f, n, args); LOG_Z3_mk_map(c, f, n, args);
@ -94,7 +93,7 @@ extern "C" {
ast_manager & m = mk_c(c)->m(); ast_manager & m = mk_c(c)->m();
func_decl* _f = to_func_decl(f); func_decl* _f = to_func_decl(f);
expr* const* _args = to_exprs(args); expr* const* _args = to_exprs(args);
ptr_vector<sort> domain; ptr_vector<sort> domain;
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
domain.push_back(m.get_sort(_args[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_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_const_array(c, domain, v); LOG_Z3_mk_const_array(c, domain, v);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m(); ast_manager & m = mk_c(c)->m();
expr * _v = to_expr(v); expr * _v = to_expr(v);
sort * _range = m.get_sort(_v); sort * _range = m.get_sort(_v);
@ -123,14 +122,14 @@ extern "C" {
app * r = m.mk_app(cd, 1, &_v); app * r = m.mk_app(cd, 1, &_v);
mk_c(c)->save_ast_trail(r); mk_c(c)->save_ast_trail(r);
check_sorts(c, r); check_sorts(c, r);
RETURN_Z3(of_ast(r)); RETURN_Z3(of_ast(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array) { Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_array_default(c, array); LOG_Z3_mk_array_default(c, array);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m(); ast_manager & m = mk_c(c)->m();
expr * _a = to_expr(array); expr * _a = to_expr(array);
@ -138,12 +137,12 @@ extern "C" {
app * r = m.mk_app(f, 1, &_a); app * r = m.mk_app(f, 1, &_a);
mk_c(c)->save_ast_trail(r); mk_c(c)->save_ast_trail(r);
check_sorts(c, r); check_sorts(c, r);
RETURN_Z3(of_ast(r)); RETURN_Z3(of_ast(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast mk_app_array_core(Z3_context c, Z3_sort domain, Z3_ast v) { 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(); ast_manager & m = mk_c(c)->m();
expr * _v = to_expr(v); expr * _v = to_expr(v);
sort * _range = m.get_sort(_v); sort * _range = m.get_sort(_v);
@ -178,7 +177,7 @@ extern "C" {
LOG_Z3_mk_full_set(c, domain); LOG_Z3_mk_full_set(c, domain);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
Z3_ast r = mk_app_array_core(c, domain, Z3_mk_true(c)); Z3_ast r = mk_app_array_core(c, domain, Z3_mk_true(c));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -205,8 +204,8 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_get_array_sort_domain(c, t); LOG_Z3_get_array_sort_domain(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_VALID_AST(t, 0); 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) { to_sort(t)->get_decl_kind() == ARRAY_SORT) {
Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(0).get_ast()); Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(0).get_ast());
RETURN_Z3(r); RETURN_Z3(r);
@ -215,13 +214,13 @@ extern "C" {
RETURN_Z3(0); RETURN_Z3(0);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t) { Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_array_sort_range(c, t); LOG_Z3_get_array_sort_range(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_VALID_AST(t, 0); 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) { to_sort(t)->get_decl_kind() == ARRAY_SORT) {
Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(1).get_ast()); Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(1).get_ast());
RETURN_Z3(r); RETURN_Z3(r);

37
src/api/api_bv.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.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_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_bv_sort(c, sz); LOG_Z3_mk_bv_sort(c, sz);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
if (sz == 0) { if (sz == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG); 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_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) #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_bvnot, OP_BNOT);
MK_BV_UNARY(Z3_mk_bvredand, OP_BREDAND); MK_BV_UNARY(Z3_mk_bvredand, OP_BREDAND);
MK_BV_UNARY(Z3_mk_bvredor, OP_BREDOR); MK_BV_UNARY(Z3_mk_bvredor, OP_BREDOR);
@ -75,11 +74,11 @@ extern "C" {
expr * _n = to_expr(n); expr * _n = to_expr(n);
parameter params[2] = { parameter(high), parameter(low) }; 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); 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); check_sorts(c, a);
return of_ast(a); return of_ast(a);
} }
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast n) { Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast n) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_extract(c, high, low, n); LOG_Z3_mk_extract(c, high, low, n);
@ -88,7 +87,7 @@ extern "C" {
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
#define MK_BV_PUNARY(NAME, OP) \ #define MK_BV_PUNARY(NAME, OP) \
Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY; \ 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_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast n, Z3_bool is_signed) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_bv2int(c, n, is_signed); LOG_Z3_mk_bv2int(c, n, is_signed);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
Z3_sort int_s = Z3_mk_int_sort(c); Z3_sort int_s = Z3_mk_int_sort(c);
if (is_signed) { if (is_signed) {
Z3_ast r = Z3_mk_bv2int(c, n, false); 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_inc_ref(c, bound);
Z3_ast zero = Z3_mk_int(c, 0, s); Z3_ast zero = Z3_mk_int(c, 0, s);
Z3_inc_ref(c, zero); 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); Z3_inc_ref(c, pred);
// if n <_sigend 0 then r - s^sz else r // if n <_sigend 0 then r - s^sz else r
Z3_ast args[2] = { r, bound }; 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); RETURN_Z3(res);
} }
else { else {
expr * _n = to_expr(n); expr * _n = to_expr(n);
parameter p(to_sort(int_s)); 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); 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); mk_c(c)->save_ast_trail(a);
check_sorts(c, a); check_sorts(c, a);
RETURN_Z3(of_ast(a)); RETURN_Z3(of_ast(a));
} }
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
/** /**
\brief Create a bit-vector of sort \s with 1 in the most significant bit position. \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. The sort \s must be a bit-vector sort.
This function is a shorthand for <tt>shl(1, N-1)</tt> This function is a shorthand for <tt>shl(1, N-1)</tt>
@ -343,7 +342,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
return Z3_mk_not(c, eq); return Z3_mk_not(c, eq);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
// only for signed machine integers // only for signed machine integers
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) { Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY; Z3_TRY;
@ -369,7 +368,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
return result; return result;
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast n1, Z3_ast n2) { Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast n1, Z3_ast n2) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_bvsub(c, n1, n2); 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) { unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_bv_sort_size(c, t); LOG_Z3_get_bv_sort_size(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_VALID_AST(t, 0); 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) { 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(); 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; return 0;
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
}; };

119
src/api/api_datatype.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.h" #include"api_context.h"
@ -24,16 +23,16 @@ Revision History:
extern "C" { 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, Z3_symbol name,
unsigned num_fields, unsigned num_fields,
Z3_symbol const field_names[], Z3_symbol const field_names[],
Z3_sort const field_sorts[], Z3_sort const field_sorts[],
Z3_func_decl * mk_tuple_decl, Z3_func_decl * mk_tuple_decl,
Z3_func_decl proj_decls[]) { Z3_func_decl proj_decls[]) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_tuple_sort(c, name, num_fields, field_names, field_sorts, mk_tuple_decl, proj_decls); 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(); mk_c(c)->reset_last_result();
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
datatype_util& dt_util = mk_c(c)->dtutil(); datatype_util& dt_util = mk_c(c)->dtutil();
@ -43,14 +42,14 @@ extern "C" {
std::string recognizer_s("is_"); std::string recognizer_s("is_");
recognizer_s += to_symbol(name).str(); recognizer_s += to_symbol(name).str();
symbol recognizer(recognizer_s.c_str()); symbol recognizer(recognizer_s.c_str());
ptr_vector<accessor_decl> acc; ptr_vector<accessor_decl> acc;
for (unsigned i = 0; i < num_fields; ++i) { 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])))); 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()) }; 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); 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); bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, tuples);
@ -63,7 +62,7 @@ extern "C" {
} }
// create tuple type // create tuple type
SASSERT(tuples.size() == 1); SASSERT(tuples.size() == 1);
tuple = tuples[0].get(); tuple = tuples[0].get();
mk_c(c)->save_multiple_ast_trail(tuple); mk_c(c)->save_multiple_ast_trail(tuple);
@ -72,9 +71,9 @@ extern "C" {
SASSERT(!dt_util.is_recursive(tuple)); SASSERT(!dt_util.is_recursive(tuple));
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple); ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple);
func_decl* decl = (*decls)[0]; 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); *mk_tuple_decl = of_func_decl(decl);
// Create projections // Create projections
ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl); ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl);
if (!accs) { if (!accs) {
@ -90,8 +89,8 @@ extern "C" {
RETURN_Z3_mk_tuple_sort(of_sort(tuple)); RETURN_Z3_mk_tuple_sort(of_sort(tuple));
Z3_CATCH_RETURN(0); 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, Z3_symbol name,
unsigned n, unsigned n,
Z3_symbol const enum_names[], Z3_symbol const enum_names[],
@ -106,7 +105,7 @@ extern "C" {
sort_ref_vector sorts(m); sort_ref_vector sorts(m);
sort* e; sort* e;
ptr_vector<constructor_decl> constrs; ptr_vector<constructor_decl> constrs;
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
symbol e_name(to_symbol(enum_names[i])); symbol e_name(to_symbol(enum_names[i]));
@ -128,9 +127,9 @@ extern "C" {
RETURN_Z3(0); RETURN_Z3(0);
} }
} }
// create enum type. // create enum type.
SASSERT(sorts.size() == 1); SASSERT(sorts.size() == 1);
e = sorts[0].get(); e = sorts[0].get();
mk_c(c)->save_multiple_ast_trail(e); mk_c(c)->save_multiple_ast_trail(e);
@ -141,10 +140,10 @@ extern "C" {
SASSERT(decls && decls->size() == n); SASSERT(decls && decls->size() == n);
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
func_decl* decl = (*decls)[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); enum_consts[i] = of_func_decl(decl);
decl = dt_util.get_constructor_recognizer(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); enum_testers[i] = of_func_decl(decl);
} }
@ -168,11 +167,11 @@ extern "C" {
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
mk_c(c)->reset_last_result(); mk_c(c)->reset_last_result();
datatype_util data_util(m); 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("head"), type_ref(to_sort(elem_sort))),
mk_accessor_decl(symbol("tail"), type_ref(0)) 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), mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, 0),
// Leo: SMT 2.0 document uses 'insert' instead of cons // Leo: SMT 2.0 document uses 'insert' instead of cons
mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail) mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail)
@ -197,22 +196,22 @@ extern "C" {
func_decl* f; func_decl* f;
if (nil_decl) { if (nil_decl) {
f = cnstrs[0]; 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); *nil_decl = of_func_decl(f);
} }
if (is_nil_decl) { if (is_nil_decl) {
f = data_util.get_constructor_recognizer(cnstrs[0]); 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); *is_nil_decl = of_func_decl(f);
} }
if (cons_decl) { if (cons_decl) {
f = cnstrs[1]; 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); *cons_decl = of_func_decl(f);
} }
if (is_cons_decl) { if (is_cons_decl) {
f = data_util.get_constructor_recognizer(cnstrs[1]); 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); *is_cons_decl = of_func_decl(f);
} }
if (head_decl) { if (head_decl) {
@ -220,7 +219,7 @@ extern "C" {
SASSERT(acc); SASSERT(acc);
SASSERT(acc->size() == 2); SASSERT(acc->size() == 2);
f = (*acc)[0]; 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); *head_decl = of_func_decl(f);
} }
if (tail_decl) { if (tail_decl) {
@ -228,7 +227,7 @@ extern "C" {
SASSERT(acc); SASSERT(acc);
SASSERT(acc->size() == 2); SASSERT(acc->size() == 2);
f = (*acc)[1]; 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); *tail_decl = of_func_decl(f);
} }
RETURN_Z3_mk_list_sort(of_sort(s)); RETURN_Z3_mk_list_sort(of_sort(s));
@ -255,7 +254,7 @@ extern "C" {
) { ) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_constructor(c, name, tester, num_fields, field_names, sorts, sort_refs); 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(); ast_manager& m = mk_c(c)->m();
constructor* cnstr = alloc(constructor, m); constructor* cnstr = alloc(constructor, m);
cnstr->m_name = to_symbol(name); cnstr->m_name = to_symbol(name);
@ -291,7 +290,7 @@ extern "C" {
if (!f) { if (!f) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return; return;
} }
if (constructor_decl) { if (constructor_decl) {
mk_c(c)->save_multiple_ast_trail(f); mk_c(c)->save_multiple_ast_trail(f);
*constructor_decl = of_func_decl(f); *constructor_decl = of_func_decl(f);
@ -301,15 +300,15 @@ extern "C" {
mk_c(c)->save_multiple_ast_trail(f2); mk_c(c)->save_multiple_ast_trail(f2);
*tester = of_func_decl(f2); *tester = of_func_decl(f2);
} }
ptr_vector<func_decl> const* accs = data_util.get_constructor_accessors(f); ptr_vector<func_decl> const* accs = data_util.get_constructor_accessors(f);
if (!accs && num_fields > 0) { if (!accs && num_fields > 0) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return; return;
} }
for (unsigned i = 0; i < num_fields; ++i) { for (unsigned i = 0; i < num_fields; ++i) {
func_decl* f2 = (*accs)[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); accessors[i] = of_func_decl(f2);
} }
RETURN_Z3_query_constructor; RETURN_Z3_query_constructor;
@ -324,7 +323,7 @@ extern "C" {
Z3_CATCH; Z3_CATCH;
} }
static datatype_decl* mk_datatype_decl(Z3_context c, static datatype_decl* mk_datatype_decl(Z3_context c,
Z3_symbol name, Z3_symbol name,
unsigned num_constructors, unsigned num_constructors,
Z3_constructor 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())); 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, Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
@ -352,9 +351,9 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_datatype(c, name, num_constructors, constructors); LOG_Z3_mk_datatype(c, name, num_constructors, constructors);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
datatype_util data_util(m); datatype_util data_util(m);
sort_ref_vector sorts(m); sort_ref_vector sorts(m);
{ {
datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors); datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors);
@ -370,7 +369,7 @@ extern "C" {
mk_c(c)->save_ast_trail(s); mk_c(c)->save_ast_trail(s);
ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s); ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s);
for (unsigned i = 0; i < num_constructors; ++i) { for (unsigned i = 0; i < num_constructors; ++i) {
constructor* cn = reinterpret_cast<constructor*>(constructors[i]); constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
cn->m_constructor = (*cnstrs)[i]; cn->m_constructor = (*cnstrs)[i];
@ -411,7 +410,7 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_datatypes(c, num_sorts, sort_names, sorts, constructor_lists); LOG_Z3_mk_datatypes(c, num_sorts, sort_names, sorts, constructor_lists);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
mk_c(c)->reset_last_result(); mk_c(c)->reset_last_result();
datatype_util data_util(m); datatype_util data_util(m);
@ -423,7 +422,7 @@ extern "C" {
sort_ref_vector _sorts(m); sort_ref_vector _sorts(m);
bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), _sorts); bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), _sorts);
del_datatype_decls(datas.size(), datas.c_ptr()); del_datatype_decls(datas.size(), datas.c_ptr());
if (!ok) { if (!ok) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return; return;
@ -437,8 +436,8 @@ extern "C" {
constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]); constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s); ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s);
for (unsigned j = 0; j < cl->size(); ++j) { for (unsigned j = 0; j < cl->size(); ++j) {
constructor* cn = (*cl)[j]; constructor* cn = (*cl)[j];
cn->m_constructor = (*cnstrs)[j]; cn->m_constructor = (*cnstrs)[j];
} }
} }
RETURN_Z3_mk_datatypes; RETURN_Z3_mk_datatypes;
@ -452,15 +451,15 @@ extern "C" {
CHECK_VALID_AST(t, 0); CHECK_VALID_AST(t, 0);
sort * _t = to_sort(t); sort * _t = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil(); datatype_util& dt_util = mk_c(c)->dtutil();
if (!dt_util.is_datatype(_t)) { if (!dt_util.is_datatype(_t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
if (!decls) { if (!decls) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
return decls->size(); return decls->size();
Z3_CATCH_RETURN(0); 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) { Z3_func_decl get_datatype_sort_constructor_core(Z3_context c, Z3_sort t, unsigned idx) {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_VALID_AST(t, 0); CHECK_VALID_AST(t, 0);
sort * _t = to_sort(t); sort * _t = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil(); datatype_util& dt_util = mk_c(c)->dtutil();
if (!dt_util.is_datatype(_t)) { 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_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_datatype_sort_recognizer(c, t, idx); LOG_Z3_get_datatype_sort_recognizer(c, t, idx);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
sort * _t = to_sort(t); sort * _t = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil(); datatype_util& dt_util = mk_c(c)->dtutil();
if (!dt_util.is_datatype(_t)) { if (!dt_util.is_datatype(_t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); 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_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a); LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
sort * _t = to_sort(t); sort * _t = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil(); datatype_util& dt_util = mk_c(c)->dtutil();
if (!dt_util.is_datatype(_t)) { if (!dt_util.is_datatype(_t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
if (!decls || idx_c >= decls->size()) { if (!decls || idx_c >= decls->size()) {
@ -536,24 +535,24 @@ extern "C" {
func_decl* decl = (*decls)[idx_c]; func_decl* decl = (*decls)[idx_c];
if (decl->get_arity() <= idx_a) { if (decl->get_arity() <= idx_a) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl); ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl);
SASSERT(accs && accs->size() == decl->get_arity()); SASSERT(accs && accs->size() == decl->get_arity());
if (!accs || accs->size() <= idx_a) { if (!accs || accs->size() <= idx_a) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
decl = (*accs)[idx_a]; decl = (*accs)[idx_a];
mk_c(c)->save_ast_trail(decl); mk_c(c)->save_ast_trail(decl);
RETURN_Z3(of_func_decl(decl)); RETURN_Z3(of_func_decl(decl));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t) { Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_tuple_sort_mk_decl(c, t); LOG_Z3_get_tuple_sort_mk_decl(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
sort * tuple = to_sort(t); sort * tuple = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil(); 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) { 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); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t) { unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_tuple_sort_num_fields(c, t); LOG_Z3_get_tuple_sort_num_fields(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
sort * tuple = to_sort(t); sort * tuple = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil(); 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) { 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); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple); ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple);
if (!decls || decls->size() != 1) { if (!decls || decls->size() != 1) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors((*decls)[0]); ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors((*decls)[0]);
if (!accs) { if (!accs) {
return 0; return 0;
} }
return accs->size(); return accs->size();
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i) { Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_tuple_sort_field_decl(c, t, i); LOG_Z3_get_tuple_sort_field_decl(c, t, i);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
sort * tuple = to_sort(t); sort * tuple = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil(); 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) { 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_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; Z3_TRY;
LOG_Z3_datatype_update_field(c, f, t, v); LOG_Z3_datatype_update_field(c, f, t, v);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m(); ast_manager & m = mk_c(c)->m();
func_decl* _f = to_func_decl(f); func_decl* _f = to_func_decl(f);
expr* _t = to_expr(t); expr* _t = to_expr(t);
expr* _v = to_expr(v); expr* _v = to_expr(v);
expr* args[2] = { _t, _v }; expr* args[2] = { _t, _v };
sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) }; sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) };
parameter param(_f); parameter param(_f);

5
src/api/api_interp.cpp
View file

@ -15,7 +15,6 @@
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include<sstream> #include<sstream>
#include<vector> #include<vector>
#include"z3.h" #include"z3.h"
@ -375,7 +374,7 @@ extern "C" {
for(int i = 0; i < num_theory; i++) for(int i = 0; i < num_theory; i++)
fmlas[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),fmlas[i]); fmlas[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),fmlas[i]);
std::copy(cnsts,cnsts+num,fmlas.begin()+num_theory); 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); std::ofstream f(filename);
if(num_theory) if(num_theory)
f << ";! THEORY=" << num_theory << "\n"; f << ";! THEORY=" << num_theory << "\n";
@ -469,7 +468,7 @@ extern "C" {
} }
f.close(); f.close();
#if 0 #if 0
if(!parents){ if(!parents){

1
src/api/api_log.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include<fstream> #include<fstream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"

16
src/api/api_pb.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.h" #include"api_context.h"
@ -23,8 +22,8 @@ Revision History:
#include"pb_decl_plugin.h" #include"pb_decl_plugin.h"
extern "C" { 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_ast const args[], unsigned k) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_atmost(c, num_args, args, k); LOG_Z3_mk_atmost(c, num_args, args, k);
@ -38,9 +37,8 @@ extern "C" {
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args,
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k) {
Z3_ast const args[], unsigned k) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_atmost(c, num_args, args, k); LOG_Z3_mk_atmost(c, num_args, args, k);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
@ -53,7 +51,7 @@ extern "C" {
Z3_CATCH_RETURN(0); 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[], Z3_ast const args[], int _coeffs[],
int k) { int k) {
Z3_TRY; Z3_TRY;
@ -71,7 +69,7 @@ extern "C" {
Z3_CATCH_RETURN(0); 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[], Z3_ast const args[], int _coeffs[],
int k) { int k) {
Z3_TRY; Z3_TRY;
@ -89,7 +87,7 @@ extern "C" {
Z3_CATCH_RETURN(0); 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[], Z3_ast const args[], int _coeffs[],
int k) { int k) {
Z3_TRY; Z3_TRY;

5
src/api/api_polynomial.cpp
View file

@ -14,9 +14,8 @@ Author:
Leonardo de Moura (leonardo) 2012-12-08 Leonardo de Moura (leonardo) 2012-12-08
Notes: Notes:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.h" #include"api_context.h"
@ -35,7 +34,7 @@ namespace api {
pmanager::~pmanager() { pmanager::~pmanager() {
} }
}; };
extern "C" { extern "C" {

121
src/api/api_quant.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.h" #include"api_context.h"
@ -26,17 +25,17 @@ Revision History:
extern "C" { extern "C" {
Z3_ast Z3_API Z3_mk_quantifier( Z3_ast Z3_API Z3_mk_quantifier(
Z3_context c, Z3_context c,
Z3_bool is_forall, Z3_bool is_forall,
unsigned weight, unsigned weight,
unsigned num_patterns, Z3_pattern const patterns[], unsigned num_patterns, Z3_pattern const patterns[],
unsigned num_decls, Z3_sort const sorts[], unsigned num_decls, Z3_sort const sorts[],
Z3_symbol const decl_names[], Z3_symbol const decl_names[],
Z3_ast body) Z3_ast body)
{ {
return Z3_mk_quantifier_ex( return Z3_mk_quantifier_ex(
c, c,
is_forall, is_forall,
weight, weight,
0, 0,
0, 0,
@ -50,15 +49,15 @@ extern "C" {
} }
Z3_ast mk_quantifier_ex_core( Z3_ast mk_quantifier_ex_core(
Z3_context c, Z3_context c,
Z3_bool is_forall, Z3_bool is_forall,
unsigned weight, unsigned weight,
Z3_symbol quantifier_id, Z3_symbol quantifier_id,
Z3_symbol skolem_id, Z3_symbol skolem_id,
unsigned num_patterns, Z3_pattern const patterns[], unsigned num_patterns, Z3_pattern const patterns[],
unsigned num_no_patterns, Z3_ast const no_patterns[], unsigned num_no_patterns, Z3_ast const no_patterns[],
unsigned num_decls, Z3_sort const sorts[], unsigned num_decls, Z3_sort const sorts[],
Z3_symbol const decl_names[], Z3_symbol const decl_names[],
Z3_ast body) { Z3_ast body) {
Z3_TRY; Z3_TRY;
RESET_ERROR_CODE(); RESET_ERROR_CODE();
@ -86,9 +85,9 @@ extern "C" {
expr_ref result(mk_c(c)->m()); expr_ref result(mk_c(c)->m());
if (num_decls > 0) { if (num_decls > 0) {
result = mk_c(c)->m().mk_quantifier( result = mk_c(c)->m().mk_quantifier(
(0 != is_forall), (0 != is_forall),
names.size(), ts, names.c_ptr(), to_expr(body), names.size(), ts, names.c_ptr(), to_expr(body),
weight, weight,
to_symbol(quantifier_id), to_symbol(quantifier_id),
to_symbol(skolem_id), to_symbol(skolem_id),
num_patterns, ps, num_patterns, ps,
@ -104,44 +103,44 @@ extern "C" {
} }
Z3_ast Z3_API Z3_mk_quantifier_ex( Z3_ast Z3_API Z3_mk_quantifier_ex(
Z3_context c, Z3_context c,
Z3_bool is_forall, Z3_bool is_forall,
unsigned weight, unsigned weight,
Z3_symbol quantifier_id, Z3_symbol quantifier_id,
Z3_symbol skolem_id, Z3_symbol skolem_id,
unsigned num_patterns, Z3_pattern const patterns[], unsigned num_patterns, Z3_pattern const patterns[],
unsigned num_no_patterns, Z3_ast const no_patterns[], unsigned num_no_patterns, Z3_ast const no_patterns[],
unsigned num_decls, Z3_sort const sorts[], unsigned num_decls, Z3_sort const sorts[],
Z3_symbol const decl_names[], Z3_symbol const decl_names[],
Z3_ast body) 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); 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); num_no_patterns, no_patterns, num_decls, sorts, decl_names, body);
RETURN_Z3(r); RETURN_Z3(r);
} }
Z3_ast Z3_API Z3_mk_forall(Z3_context c, Z3_ast Z3_API Z3_mk_forall(Z3_context c,
unsigned weight, unsigned weight,
unsigned num_patterns, Z3_pattern const patterns[], unsigned num_patterns, Z3_pattern const patterns[],
unsigned num_decls, Z3_sort const types[], unsigned num_decls, Z3_sort const types[],
Z3_symbol const decl_names[], Z3_symbol const decl_names[],
Z3_ast body) { Z3_ast body) {
return Z3_mk_quantifier(c, 1, weight, num_patterns, patterns, num_decls, types, decl_names, 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, Z3_ast Z3_API Z3_mk_exists(Z3_context c,
unsigned weight, unsigned weight,
unsigned num_patterns, Z3_pattern const patterns[], unsigned num_patterns, Z3_pattern const patterns[],
unsigned num_decls, Z3_sort const types[], unsigned num_decls, Z3_sort const types[],
Z3_symbol const decl_names[], Z3_symbol const decl_names[],
Z3_ast body) { Z3_ast body) {
return Z3_mk_quantifier(c, 0, weight, num_patterns, patterns, num_decls, types, decl_names, 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, Z3_bool is_forall,
unsigned weight, unsigned weight,
Z3_symbol quantifier_id, Z3_symbol quantifier_id,
@ -166,7 +165,7 @@ extern "C" {
} }
if (num_bound == 0) { if (num_bound == 0) {
SET_ERROR_CODE(Z3_INVALID_USAGE); SET_ERROR_CODE(Z3_INVALID_USAGE);
RETURN_Z3(0); RETURN_Z3(0);
} }
for (unsigned i = 0; i < num_bound; ++i) { for (unsigned i = 0; i < num_bound; ++i) {
app* a = to_app(bound[i]); app* a = to_app(bound[i]);
@ -191,7 +190,7 @@ extern "C" {
app* pat = to_pattern(patterns[i]); app* pat = to_pattern(patterns[i]);
SASSERT(mk_c(c)->m().is_pattern(pat)); SASSERT(mk_c(c)->m().is_pattern(pat));
expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.c_ptr(), pat, result); 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()); pinned.push_back(result.get());
SASSERT(mk_c(c)->m().is_pattern(result.get())); SASSERT(mk_c(c)->m().is_pattern(result.get()));
_patterns.push_back(of_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])); app* pat = to_app(to_expr(no_patterns[i]));
expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.c_ptr(), pat, result); 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()); pinned.push_back(result.get());
_no_patterns.push_back(of_ast(result.get())); _no_patterns.push_back(of_ast(result.get()));
} }
expr_ref abs_body(mk_c(c)->m()); 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); 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, quantifier_id,
skolem_id, skolem_id,
num_patterns, _patterns.c_ptr(), num_patterns, _patterns.c_ptr(),
num_no_patterns, _no_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())); of_ast(abs_body.get()));
RETURN_Z3(result); RETURN_Z3(result);
Z3_CATCH_RETURN(0); 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, Z3_bool is_forall,
unsigned weight, unsigned weight,
unsigned num_bound, unsigned num_bound,
@ -231,14 +230,14 @@ extern "C" {
unsigned num_patterns, unsigned num_patterns,
Z3_pattern const patterns[], Z3_pattern const patterns[],
Z3_ast body) { Z3_ast body) {
return Z3_mk_quantifier_const_ex(c, is_forall, weight, 0, 0, return Z3_mk_quantifier_const_ex(c, is_forall, weight, 0, 0,
num_bound, bound, num_bound, bound,
num_patterns, patterns, num_patterns, patterns,
0, 0, 0, 0,
body); 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 weight,
unsigned num_bound, unsigned num_bound,
Z3_app const 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); 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 weight,
unsigned num_bound, unsigned num_bound,
Z3_app const bound[], Z3_app const bound[],
@ -257,7 +256,7 @@ extern "C" {
Z3_ast body) { Z3_ast body) {
return Z3_mk_quantifier_const(c, false, weight, num_bound, bound, num_patterns, patterns, 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_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_pattern(c, num_patterns, terms); LOG_Z3_mk_pattern(c, num_patterns, terms);
@ -273,7 +272,7 @@ extern "C" {
RETURN_Z3(of_pattern(a)); RETURN_Z3(of_pattern(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty) { Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_bound(c, index, ty); LOG_Z3_mk_bound(c, index, ty);
@ -436,7 +435,7 @@ extern "C" {
else { else {
SET_ERROR_CODE(Z3_SORT_ERROR); SET_ERROR_CODE(Z3_SORT_ERROR);
return 0; return 0;
} }
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -450,7 +449,7 @@ extern "C" {
} }
else { else {
SET_ERROR_CODE(Z3_SORT_ERROR); SET_ERROR_CODE(Z3_SORT_ERROR);
return 0; return 0;
} }
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -471,13 +470,13 @@ extern "C" {
Z3_CATCH_RETURN(0); 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(); 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) { Z3_API char const * Z3_pattern_to_string(Z3_context c, Z3_pattern p) {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p)); return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p));
} }
}; };

37
src/api/api_seq.cpp
View file

@ -16,7 +16,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.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_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort domain) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_seq_sort(c, domain); 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)); sort * ty = mk_c(c)->sutil().str.mk_seq(to_sort(domain));
mk_c(c)->save_ast_trail(ty); mk_c(c)->save_ast_trail(ty);
RETURN_Z3(of_sort(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_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort domain) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_re_sort(c, domain); 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)); sort * ty = mk_c(c)->sutil().re.mk_re(to_sort(domain));
mk_c(c)->save_ast_trail(ty); mk_c(c)->save_ast_trail(ty);
RETURN_Z3(of_sort(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_ast Z3_API Z3_mk_string(Z3_context c, Z3_string str) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_string(c, str); LOG_Z3_mk_string(c, str);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
zstring s(str, zstring::ascii); zstring s(str, zstring::ascii);
app* a = mk_c(c)->sutil().str.mk_string(s); app* a = mk_c(c)->sutil().str.mk_string(s);
mk_c(c)->save_ast_trail(a); mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a)); RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) { Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_string_sort(c); LOG_Z3_mk_string_sort(c);
@ -71,8 +70,8 @@ extern "C" {
LOG_Z3_is_seq_sort(c, s); LOG_Z3_is_seq_sort(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().is_seq(to_sort(s)); bool result = mk_c(c)->sutil().is_seq(to_sort(s));
return result?Z3_TRUE:Z3_FALSE; return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE); Z3_CATCH_RETURN(Z3_FALSE);
} }
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) { 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); LOG_Z3_is_re_sort(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().is_re(to_sort(s)); bool result = mk_c(c)->sutil().is_re(to_sort(s));
return result?Z3_TRUE:Z3_FALSE; return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE); Z3_CATCH_RETURN(Z3_FALSE);
} }
Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) { 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); LOG_Z3_is_string_sort(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().is_string(to_sort(s)); bool result = mk_c(c)->sutil().is_string(to_sort(s));
return result?Z3_TRUE:Z3_FALSE; return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE); Z3_CATCH_RETURN(Z3_FALSE);
} }
Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) { 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); LOG_Z3_is_string(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().str.is_string(to_expr(s)); 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); Z3_CATCH_RETURN(Z3_FALSE);
} }
@ -125,7 +124,7 @@ extern "C" {
mk_c(c)->save_ast_trail(a); \ mk_c(c)->save_ast_trail(a); \
RETURN_Z3(of_ast(a)); \ RETURN_Z3(of_ast(a)); \
Z3_CATCH_RETURN(0); \ Z3_CATCH_RETURN(0); \
} }
MK_SORTED(Z3_mk_seq_empty, mk_c(c)->sutil().str.mk_empty); 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); 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_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_re_loop(c, r, lo, hi); LOG_Z3_mk_re_loop(c, r, lo, hi);
RESET_ERROR_CODE(); 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); 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); mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a)); RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP); MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP);