mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fixed update_api.py

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-17 23:13:43 -07:00
parent 15fb18c65d
commit 9cb29777e2
4 changed files with 515 additions and 474 deletions
Download patch file Download diff file Expand all files Collapse all files

22
Microsoft.Z3/Native.cs
View file

@ -862,6 +862,15 @@ namespace Microsoft.Z3
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
public extern static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2); public extern static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2);
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
public extern static int Z3_open_log(string a0);
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
public extern static void Z3_append_log(string a0);
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
public extern static void Z3_close_log();
[DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
public extern static void Z3_toggle_warning_messages(int a0); public extern static void Z3_toggle_warning_messages(int a0);
@ -3608,6 +3617,19 @@ namespace Microsoft.Z3
return r; return r;
} }
public static int Z3_open_log(string a0) {
int r = LIB.Z3_open_log(a0);
return r;
}
public static void Z3_append_log(string a0) {
LIB.Z3_append_log(a0);
}
public static void Z3_close_log() {
LIB.Z3_close_log();
}
public static void Z3_toggle_warning_messages(int a0) { public static void Z3_toggle_warning_messages(int a0) {
LIB.Z3_toggle_warning_messages(a0); LIB.Z3_toggle_warning_messages(a0);
} }

8
lib/z3_api.h
View file

@ -1160,7 +1160,7 @@ typedef enum
Definitions for update_api.py Definitions for update_api.py
def_Type('CONFIG', 'Z3_config', 'Config') def_Type('CONFIG', 'Z3_config', 'Config')
def_Type('CONTEXT', 'Z3_context', 'Context') def_Type('CONTEXT', 'Z3_context', 'ContextObj')
def_Type('AST', 'Z3_ast', 'Ast') def_Type('AST', 'Z3_ast', 'Ast')
def_Type('APP', 'Z3_app', 'Ast') def_Type('APP', 'Z3_app', 'Ast')
def_Type('SORT', 'Z3_sort', 'Sort') def_Type('SORT', 'Z3_sort', 'Sort')
@ -4683,7 +4683,7 @@ END_MLAPI_EXCLUDE
/** /**
\brief Log interaction to a file. \brief Log interaction to a file.
extra_def_API('Z3_open_log', INT, (_in(STRING),)) extra_API('Z3_open_log', INT, (_in(STRING),))
*/ */
Z3_bool Z3_API Z3_open_log(__in Z3_string filename); Z3_bool Z3_API Z3_open_log(__in Z3_string filename);
@ -4694,14 +4694,14 @@ END_MLAPI_EXCLUDE
It contains the formulas that are checked using Z3. It contains the formulas that are checked using Z3.
You can use this command to append comments, for instance. You can use this command to append comments, for instance.
extra_def_API('Z3_append_log', VOID, (_in(STRING),)) extra_API('Z3_append_log', VOID, (_in(STRING),))
*/ */
void Z3_API Z3_append_log(__in Z3_string string); void Z3_API Z3_append_log(__in Z3_string string);
/** /**
\brief Close interaction log. \brief Close interaction log.
extra_def_API('Z3_close_log', VOID, ()) extra_API('Z3_close_log', VOID, ())
*/ */
void Z3_API Z3_close_log(); void Z3_API Z3_close_log();

954
python/z3core.py
View file

File diff suppressed because it is too large Load diff

5
update_api.py
View file

@ -446,6 +446,7 @@ def mk_py_binding(name, result, params):
core_py.write("]\n") core_py.write("]\n")
def extra_API(name, result, params): def extra_API(name, result, params):
print 'extra_API(%s)' % name
mk_py_binding(name, result, params) mk_py_binding(name, result, params)
reg_dotnet(name, result, params) reg_dotnet(name, result, params)
@ -848,12 +849,16 @@ def mk_bindings():
# Collect API(...) commands from # Collect API(...) commands from
def def_APIs(): def def_APIs():
pat1 = re.compile(" *def_API.*") pat1 = re.compile(" *def_API.*")
pat2 = re.compile(" *extra_API.*")
for api_file in API_FILES: for api_file in API_FILES:
api = open(api_file, 'r') api = open(api_file, 'r')
for line in api: for line in api:
m = pat1.match(line) m = pat1.match(line)
if m: if m:
eval(line) eval(line)
m = pat2.match(line)
if m:
eval(line)
mk_z3consts_donet() mk_z3consts_donet()
mk_z3consts_py() mk_z3consts_py()