mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
Disabled (extra) internal python API for testing.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
d6e8096a61
commit
98147b0fc9
|
@ -62,7 +62,7 @@ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe',
|
||||||
add_lib('api', ['portfolio', 'user_plugin'])
|
add_lib('api', ['portfolio', 'user_plugin'])
|
||||||
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
||||||
add_exe('test', ['api', 'fuzzing'], exe_name='test-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_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('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')
|
add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_name='Microsoft.Z3V3')
|
||||||
|
|
|
@ -41,7 +41,6 @@ log_c.write('#include\"z3_logger.h\"\n')
|
||||||
##
|
##
|
||||||
exe_c.write('// Automatically generated file\n')
|
exe_c.write('// Automatically generated file\n')
|
||||||
exe_c.write('#include\"z3.h\"\n')
|
exe_c.write('#include\"z3.h\"\n')
|
||||||
exe_c.write('#include\"z3_internal.h\"\n')
|
|
||||||
exe_c.write('#include\"z3_replayer.h\"\n')
|
exe_c.write('#include\"z3_replayer.h\"\n')
|
||||||
##
|
##
|
||||||
log_h.write('extern std::ostream * g_z3_log;\n')
|
log_h.write('extern std::ostream * g_z3_log;\n')
|
||||||
|
|
|
@ -16,7 +16,6 @@ Revision History:
|
||||||
|
|
||||||
--*/
|
--*/
|
||||||
#include<iostream>
|
#include<iostream>
|
||||||
#include"z3_internal.h"
|
|
||||||
#include"api_log_macros.h"
|
#include"api_log_macros.h"
|
||||||
#include"api_context.h"
|
#include"api_context.h"
|
||||||
#include"api_util.h"
|
#include"api_util.h"
|
||||||
|
|
|
@ -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("");
|
|
||||||
}
|
|
||||||
|
|
|
@ -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<Z3_polynomial_manager>(m); }
|
|
||||||
|
|
||||||
inline polynomial::polynomial * to_poly(Z3_polynomial p) { return reinterpret_cast<polynomial::polynomial*>(p); }
|
|
||||||
inline Z3_polynomial of_poly(polynomial::polynomial * p) { return reinterpret_cast<Z3_polynomial>(p); }
|
|
||||||
|
|
||||||
#endif
|
|
|
@ -24,7 +24,6 @@ Notes:
|
||||||
#include<stdio.h>
|
#include<stdio.h>
|
||||||
#include"z3_macros.h"
|
#include"z3_macros.h"
|
||||||
#include"z3_api.h"
|
#include"z3_api.h"
|
||||||
#include"z3_internal_types.h"
|
|
||||||
|
|
||||||
#undef __in
|
#undef __in
|
||||||
#undef __out
|
#undef __out
|
||||||
|
|
|
@ -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
|
|
|
@ -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
|
|
|
@ -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
|
|
|
@ -106,14 +106,3 @@ class FuncEntryObj(ctypes.c_void_p):
|
||||||
def __init__(self, e): self._as_parameter_ = e
|
def __init__(self, e): self._as_parameter_ = e
|
||||||
def from_param(obj): return obj
|
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
|
|
||||||
|
|
Loading…
Reference in a new issue