From 98147b0fc95937d358c5aa0af2f81e2ba2e89513 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Oct 2012 18:55:17 -0700 Subject: [PATCH] Disabled (extra) internal python API for testing. Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 2 +- scripts/update_api.py | 1 - src/api/api_ast.cpp | 1 - src/api/api_poly.cpp | 78 ---------------------------------- src/api/api_poly.h | 40 ----------------- src/api/z3.h | 1 - src/api/z3_internal.h | 40 ----------------- src/api/z3_internal_types.h | 34 --------------- src/api/z3_poly.h | 72 ------------------------------- src/bindings/python/z3types.py | 11 ----- 10 files changed, 1 insertion(+), 279 deletions(-) delete mode 100644 src/api/api_poly.cpp delete mode 100644 src/api/api_poly.h delete mode 100644 src/api/z3_internal.h delete mode 100644 src/api/z3_internal_types.h delete mode 100644 src/api/z3_poly.h diff --git a/scripts/mk_make.py b/scripts/mk_make.py index ab0a9ab0f..cc7f650cb 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -62,7 +62,7 @@ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', add_lib('api', ['portfolio', 'user_plugin']) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3') -API_files = ['z3_api.h', 'z3_poly.h', 'z3_internal_types.h'] +API_files = ['z3_api.h'] add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3', export_files=API_files) add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet/Microsoft.Z3', dll_name='Microsoft.Z3', assembly_info_dir='Properties') add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_name='Microsoft.Z3V3') diff --git a/scripts/update_api.py b/scripts/update_api.py index d516bf55e..a5a218d3c 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -41,7 +41,6 @@ log_c.write('#include\"z3_logger.h\"\n') ## exe_c.write('// Automatically generated file\n') exe_c.write('#include\"z3.h\"\n') -exe_c.write('#include\"z3_internal.h\"\n') exe_c.write('#include\"z3_replayer.h\"\n') ## log_h.write('extern std::ostream * g_z3_log;\n') diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 925e69e1f..aeddf63c3 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -16,7 +16,6 @@ Revision History: --*/ #include -#include"z3_internal.h" #include"api_log_macros.h" #include"api_context.h" #include"api_util.h" diff --git a/src/api/api_poly.cpp b/src/api/api_poly.cpp deleted file mode 100644 index 5b4a9d58b..000000000 --- a/src/api/api_poly.cpp +++ /dev/null @@ -1,78 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - api_poly.cpp - -Abstract: - - External API for polynomial package - -Author: - - Leonardo de Moura (leonardo) 2012-10-18. - -Revision History: - ---*/ -#include"z3.h" -#include"z3_internal.h" -#include"api_context.h" -#include"api_poly.h" -#include"api_util.h" -#include"api_log_macros.h" - -Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context c) { - Z3_TRY; - LOG_Z3_mk_polynomial_manager(c); - RESET_ERROR_CODE(); - _Z3_polynomial_manager * m = alloc(_Z3_polynomial_manager); - RETURN_Z3(of_poly_manager(m)); - Z3_CATCH_RETURN(0); -} - -void Z3_del_polynomial_manager(Z3_context c, Z3_polynomial_manager m) { - Z3_TRY; - LOG_Z3_del_polynomial_manager(c, m); - RESET_ERROR_CODE(); - dealloc(to_poly_manager(m)); - Z3_CATCH; -} - -Z3_polynomial Z3_mk_zero_polynomial(Z3_context c, Z3_polynomial_manager m) { - Z3_TRY; - LOG_Z3_mk_zero_polynomial(c, m); - RESET_ERROR_CODE(); - polynomial::polynomial * r = to_poly_manager(m)->m_manager.mk_zero(); - to_poly_manager(m)->m_result = r; - RETURN_Z3(of_poly(r)); - Z3_CATCH_RETURN(0); -} - -void Z3_polynomial_inc_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) { - Z3_TRY; - LOG_Z3_polynomial_inc_ref(c, m, p); - RESET_ERROR_CODE(); - to_poly_manager(m)->m_manager.inc_ref(to_poly(p)); - Z3_CATCH; -} - -void Z3_polynomial_dec_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) { - Z3_TRY; - LOG_Z3_polynomial_inc_ref(c, m, p); - RESET_ERROR_CODE(); - to_poly_manager(m)->m_manager.dec_ref(to_poly(p)); - Z3_CATCH; -} - -Z3_string Z3_polynomial_to_string(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) { - Z3_TRY; - LOG_Z3_polynomial_to_string(c, m, p); - RESET_ERROR_CODE(); - std::ostringstream buffer; - to_poly_manager(m)->m_manager.display(buffer, to_poly(p)); - return mk_c(c)->mk_external_string(buffer.str()); - Z3_CATCH_RETURN(""); -} - diff --git a/src/api/api_poly.h b/src/api/api_poly.h deleted file mode 100644 index 943c506fd..000000000 --- a/src/api/api_poly.h +++ /dev/null @@ -1,40 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - api_poly.h - -Abstract: - External API for polynomial package - -Author: - - Leonardo de Moura (leonardo) 2012-10-18. - -Revision History: - ---*/ -#ifndef _API_POLY_H_ -#define _API_POLY_H_ - -#include"polynomial.h" - -struct _Z3_polynomial_manager { - unsynch_mpz_manager m_num_manager; - polynomial::manager m_manager; - polynomial_ref m_result; - - _Z3_polynomial_manager(): - m_manager(m_num_manager), - m_result(m_manager) { - } -}; - -inline _Z3_polynomial_manager * to_poly_manager(Z3_polynomial_manager m) { return reinterpret_cast<_Z3_polynomial_manager*>(m); } -inline Z3_polynomial_manager of_poly_manager(_Z3_polynomial_manager * m) { return reinterpret_cast(m); } - -inline polynomial::polynomial * to_poly(Z3_polynomial p) { return reinterpret_cast(p); } -inline Z3_polynomial of_poly(polynomial::polynomial * p) { return reinterpret_cast(p); } - -#endif diff --git a/src/api/z3.h b/src/api/z3.h index 76fe91ce1..8df894f40 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -24,7 +24,6 @@ Notes: #include #include"z3_macros.h" #include"z3_api.h" -#include"z3_internal_types.h" #undef __in #undef __out diff --git a/src/api/z3_internal.h b/src/api/z3_internal.h deleted file mode 100644 index cbff085e8..000000000 --- a/src/api/z3_internal.h +++ /dev/null @@ -1,40 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - z3_internal.h - -Abstract: - - Z3 internal API for C and Python. - It provides access to internal Z3 components. - It should only be used by advanced users. - We used it to build regression tests in Python. - -Author: - - Leonardo de Moura (leonardo) 2012-10-18 - -Notes: - ---*/ -#ifndef _Z3_INTERNAL_H_ -#define _Z3_INTERNAL_H_ - -#include"z3_macros.h" -#include"z3_api.h" -#include"z3_internal_types.h" -#include"z3_poly.h" - -#undef __in -#undef __out -#undef __inout -#undef __in_z -#undef __out_z -#undef __ecount -#undef __in_ecount -#undef __out_ecount -#undef __inout_ecount - -#endif diff --git a/src/api/z3_internal_types.h b/src/api/z3_internal_types.h deleted file mode 100644 index 7fb7b4038..000000000 --- a/src/api/z3_internal_types.h +++ /dev/null @@ -1,34 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - z3_internal_types.h - -Abstract: - - Z3 internal API type declarations. - -Author: - - Leonardo de Moura (leonardo) 2012-10-18 - -Notes: - ---*/ -#ifndef _Z3_INTERNAL_TYPES_H_ -#define _Z3_INTERNAL_TYPES_H_ - -DEFINE_TYPE(Z3_polynomial_manager); -DEFINE_TYPE(Z3_polynomial); -DEFINE_TYPE(Z3_monomial); - -/* - Definitions for update_api.py - - def_Type('POLYNOMIAL_MANAGER', 'Z3_polynomial_manager', 'PolynomialManagerObj') - def_Type('POLYNOMIAL', 'Z3_polynomial', 'PolynomialObj') - def_Type('MONOMIAL', 'Z3_monomial', 'MonomialObj') -*/ - -#endif diff --git a/src/api/z3_poly.h b/src/api/z3_poly.h deleted file mode 100644 index 4e3e99d53..000000000 --- a/src/api/z3_poly.h +++ /dev/null @@ -1,72 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - z3_poly.h - -Abstract: - - Z3 multivariate polynomial API. - -Author: - - Leonardo de Moura (leonardo) 2012-10-18 - -Notes: - ---*/ -#ifndef _Z3_POLY_H_ -#define _Z3_POLY_H_ - -#ifdef __cplusplus -extern "C" { -#endif // __cplusplus - - /** - \brief Create a new polynomial manager. - - def_API('Z3_mk_polynomial_manager', POLYNOMIAL_MANAGER, (_in(CONTEXT),)) - */ - Z3_polynomial_manager Z3_API Z3_mk_polynomial_manager(__in Z3_context c); - - /** - \brief Delete the given polynomial manager. - - def_API('Z3_del_polynomial_manager', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER))) - */ - void Z3_API Z3_del_polynomial_manager(__in Z3_context c, __in Z3_polynomial_manager m); - - /** - \brief Return the zero polynomial. - - def_API('Z3_mk_zero_polynomial', POLYNOMIAL, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER))) - */ - Z3_polynomial Z3_API Z3_mk_zero_polynomial(__in Z3_context c, __in Z3_polynomial_manager m); - - /** - \brief Increment p's reference counter - - def_API('Z3_polynomial_inc_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL))) - */ - void Z3_API Z3_polynomial_inc_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p); - - /** - \brief Decrement p's reference counter. - - def_API('Z3_polynomial_dec_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL))) - */ - void Z3_API Z3_polynomial_dec_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p); - - /** - \brief Convert the given polynomial into a string. - - def_API('Z3_polynomial_to_string', STRING, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL))) - */ - Z3_string Z3_API Z3_polynomial_to_string(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p); - -#ifdef __cplusplus -}; -#endif // __cplusplus - -#endif diff --git a/src/bindings/python/z3types.py b/src/bindings/python/z3types.py index b91a80aae..3a2449203 100644 --- a/src/bindings/python/z3types.py +++ b/src/bindings/python/z3types.py @@ -106,14 +106,3 @@ class FuncEntryObj(ctypes.c_void_p): def __init__(self, e): self._as_parameter_ = e def from_param(obj): return obj -class PolynomialManagerObj(ctypes.c_void_p): - def __init__(self, e): self._as_parameter_ = e - def from_param(obj): return obj - -class PolynomialObj(ctypes.c_void_p): - def __init__(self, e): self._as_parameter_ = e - def from_param(obj): return obj - -class MonomialObj(ctypes.c_void_p): - def __init__(self, e): self._as_parameter_ = e - def from_param(obj): return obj