mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
1579da02b0
commit
a40433aae8
3
.gitignore
vendored
3
.gitignore
vendored
|
|
@ -61,6 +61,7 @@ src/util/version.h
|
||||||
src/api/java/Native.cpp
|
src/api/java/Native.cpp
|
||||||
src/api/java/Native.java
|
src/api/java/Native.java
|
||||||
src/api/java/enumerations/*.java
|
src/api/java/enumerations/*.java
|
||||||
|
|
||||||
*.bak
|
*.bak
|
||||||
doc/api
|
doc/api
|
||||||
doc/code
|
doc/code
|
||||||
|
|
@ -76,4 +77,6 @@ src/api/ml/z3enums.ml
|
||||||
src/api/ml/z3.mllib
|
src/api/ml/z3.mllib
|
||||||
src/api/ml/z3_native.c
|
src/api/ml/z3_native.c
|
||||||
src/api/ml/z3_native.ml
|
src/api/ml/z3_native.ml
|
||||||
|
src/api/ml/native.c
|
||||||
|
src/api/ml/Z3.ml
|
||||||
src/api/ml/z3_enums.ml
|
src/api/ml/z3_enums.ml
|
||||||
|
|
|
||||||
|
|
@ -1430,9 +1430,9 @@ class MLComponent(Component):
|
||||||
out.write('\n\n')
|
out.write('\n\n')
|
||||||
mk_dir(os.path.join(BUILD_DIR, 'api', 'ml'))
|
mk_dir(os.path.join(BUILD_DIR, 'api', 'ml'))
|
||||||
libfile = '%s$(LIB_EXT)' % self.lib_name
|
libfile = '%s$(LIB_EXT)' % self.lib_name
|
||||||
out.write('%s: libz3$(SO_EXT) %s\n' % (libfile, os.path.join(self.to_src_dir, 'z3_native.c')))
|
out.write('%s: libz3$(SO_EXT) %s\n' % (libfile, os.path.join(self.to_src_dir, 'native.c')))
|
||||||
out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) %s/z3_native.c\n' % self.to_src_dir)
|
out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) -I%s %s/native.c\n' % (get_component(API_COMPONENT).to_src_dir, self.to_src_dir))
|
||||||
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'ml', 'z3_native'))
|
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'ml', 'native'))
|
||||||
out.write('ml: %s\n' % libfile)
|
out.write('ml: %s\n' % libfile)
|
||||||
out.write('\n')
|
out.write('\n')
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1075,12 +1075,12 @@ def mk_ml():
|
||||||
if not is_ml_enabled():
|
if not is_ml_enabled():
|
||||||
return
|
return
|
||||||
ml_dir = get_component('ml').src_dir
|
ml_dir = get_component('ml').src_dir
|
||||||
ml_nativef = os.path.join(ml_dir, 'z3_native.ml')
|
ml_nativef = os.path.join(ml_dir, 'Z3.ml')
|
||||||
ml_wrapperf = os.path.join(ml_dir, 'z3_native.c')
|
ml_wrapperf = os.path.join(ml_dir, 'native.c')
|
||||||
ml_native = open(ml_nativef, 'w')
|
ml_native = open(ml_nativef, 'w')
|
||||||
ml_native.write('(* Automatically generated file *)\n')
|
ml_native.write('(* Automatically generated file *)\n')
|
||||||
ml_native.write('\n')
|
ml_native.write('\n')
|
||||||
ml_native.write('module Z3 = struct\n\n')
|
ml_native.write('module Z3Native = struct\n\n')
|
||||||
ml_native.write('type context\n')
|
ml_native.write('type context\n')
|
||||||
ml_native.write('and symbol\n')
|
ml_native.write('and symbol\n')
|
||||||
ml_native.write('and ast\n')
|
ml_native.write('and ast\n')
|
||||||
|
|
@ -1166,101 +1166,118 @@ def mk_ml():
|
||||||
ml_wrapper.write('#ifdef Custom_tag\n')
|
ml_wrapper.write('#ifdef Custom_tag\n')
|
||||||
ml_wrapper.write('#include <caml/custom.h>\n')
|
ml_wrapper.write('#include <caml/custom.h>\n')
|
||||||
ml_wrapper.write('#include <caml/bigarray.h>\n')
|
ml_wrapper.write('#include <caml/bigarray.h>\n')
|
||||||
ml_wrapper.write('#endif\n')
|
ml_wrapper.write('#endif\n\n')
|
||||||
# for name, result, params in _dotnet_decls:
|
ml_wrapper.write('#include <z3.h>\n\n')
|
||||||
# java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
|
for name, result, params in _dotnet_decls:
|
||||||
# i = 0;
|
#return type = type2ml(result)
|
||||||
# for param in params:
|
ml_wrapper.write('CAMLprim value n_%s(' % ml_method_name(name))
|
||||||
# java_wrapper.write(', ')
|
first = True
|
||||||
# java_wrapper.write('%s a%d' % (param2javaw(param), i))
|
i = 0
|
||||||
# i = i + 1
|
for param in params:
|
||||||
# java_wrapper.write(') {\n')
|
if first:
|
||||||
# # preprocess arrays, strings, in/out arguments
|
first = False
|
||||||
# i = 0
|
else:
|
||||||
# for param in params:
|
ml_wrapper.write(', ')
|
||||||
# k = param_kind(param)
|
ml_wrapper.write('value a%d' % i)
|
||||||
# if k == OUT or k == INOUT:
|
# param type = param2ml(param)
|
||||||
# java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
|
i = i + 1
|
||||||
# elif k == IN_ARRAY or k == INOUT_ARRAY:
|
ml_wrapper.write(') {\n')
|
||||||
# if param_type(param) == INT or param_type(param) == UINT:
|
ml_wrapper.write(' CAMLparam%d(' % len(params))
|
||||||
# java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
|
i = 0
|
||||||
# else:
|
first = True
|
||||||
# java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
|
for param in params:
|
||||||
# elif k == OUT_ARRAY:
|
if first:
|
||||||
# java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)),
|
first = False
|
||||||
# i,
|
else:
|
||||||
# type2str(param_type(param)),
|
ml_wrapper.write(', ')
|
||||||
# param_array_capacity_pos(param),
|
ml_wrapper.write('a%d' % i)
|
||||||
# type2str(param_type(param))))
|
i = i + 1
|
||||||
# if param_type(param) == INT or param_type(param) == UINT:
|
ml_wrapper.write(');\n')
|
||||||
# java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
|
# preprocess arrays, strings, in/out arguments
|
||||||
# else:
|
i = 0
|
||||||
# java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
|
for param in params:
|
||||||
# elif k == IN and param_type(param) == STRING:
|
k = param_kind(param)
|
||||||
# java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i))
|
if k == OUT or k == INOUT:
|
||||||
# i = i + 1
|
ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
|
||||||
# # invoke procedure
|
elif k == IN_ARRAY or k == INOUT_ARRAY:
|
||||||
# java_wrapper.write(' ')
|
if param_type(param) == INT or param_type(param) == UINT:
|
||||||
# if result != VOID:
|
ml_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
|
||||||
# java_wrapper.write('%s result = ' % type2str(result))
|
else:
|
||||||
# java_wrapper.write('%s(' % name)
|
ml_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
|
||||||
# i = 0
|
elif k == OUT_ARRAY:
|
||||||
# first = True
|
ml_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)),
|
||||||
# for param in params:
|
i,
|
||||||
# if first:
|
type2str(param_type(param)),
|
||||||
# first = False
|
param_array_capacity_pos(param),
|
||||||
# else:
|
type2str(param_type(param))))
|
||||||
# java_wrapper.write(', ')
|
if param_type(param) == INT or param_type(param) == UINT:
|
||||||
# k = param_kind(param)
|
ml_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
|
||||||
# if k == OUT or k == INOUT:
|
else:
|
||||||
# java_wrapper.write('&_a%s' % i)
|
ml_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
|
||||||
# elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
|
elif k == IN and param_type(param) == STRING:
|
||||||
# java_wrapper.write('_a%s' % i)
|
ml_wrapper.write(' Z3_string _a%s = (Z3_string) String_val(a%s);\n' % (i, i))
|
||||||
# elif k == IN and param_type(param) == STRING:
|
i = i + 1
|
||||||
# java_wrapper.write('_a%s' % i)
|
# invoke procedure
|
||||||
# else:
|
ml_wrapper.write(' ')
|
||||||
# java_wrapper.write('(%s)a%i' % (param2str(param), i))
|
if result != VOID:
|
||||||
# i = i + 1
|
ml_wrapper.write('%s result = ' % type2str(result))
|
||||||
# java_wrapper.write(');\n')
|
ml_wrapper.write('%s(' % name)
|
||||||
# # cleanup
|
i = 0
|
||||||
# i = 0
|
first = True
|
||||||
# for param in params:
|
for param in params:
|
||||||
# k = param_kind(param)
|
if first:
|
||||||
# if k == OUT_ARRAY:
|
first = False
|
||||||
# if param_type(param) == INT or param_type(param) == UINT:
|
else:
|
||||||
# java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
|
ml_wrapper.write(', ')
|
||||||
# else:
|
k = param_kind(param)
|
||||||
# java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
|
if k == OUT or k == INOUT:
|
||||||
# java_wrapper.write(' free(_a%s);\n' % i)
|
ml_wrapper.write('&_a%s' % i)
|
||||||
# elif k == IN_ARRAY or k == OUT_ARRAY:
|
elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
|
||||||
# if param_type(param) == INT or param_type(param) == UINT:
|
ml_wrapper.write('_a%s' % i)
|
||||||
# java_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
|
elif k == IN and param_type(param) == STRING:
|
||||||
# else:
|
ml_wrapper.write('_a%s' % i)
|
||||||
# java_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
|
else:
|
||||||
|
ml_wrapper.write('(%s)a%i' % (param2str(param), i))
|
||||||
|
i = i + 1
|
||||||
|
ml_wrapper.write(');\n')
|
||||||
|
# cleanup
|
||||||
|
i = 0
|
||||||
|
for param in params:
|
||||||
|
k = param_kind(param)
|
||||||
|
if k == OUT_ARRAY:
|
||||||
|
if param_type(param) == INT or param_type(param) == UINT:
|
||||||
|
ml_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
|
||||||
|
else:
|
||||||
|
ml_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
|
||||||
|
ml_wrapper.write(' free(_a%s);\n' % i)
|
||||||
|
elif k == IN_ARRAY or k == OUT_ARRAY:
|
||||||
|
if param_type(param) == INT or param_type(param) == UINT:
|
||||||
|
ml_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
|
||||||
|
else:
|
||||||
|
ml_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
|
||||||
|
|
||||||
# elif k == OUT or k == INOUT:
|
elif k == OUT or k == INOUT:
|
||||||
# if param_type(param) == INT or param_type(param) == UINT:
|
if param_type(param) == INT or param_type(param) == UINT:
|
||||||
# java_wrapper.write(' {\n')
|
ml_wrapper.write(' {\n')
|
||||||
# java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
|
ml_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
|
||||||
# java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
|
ml_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
|
||||||
# java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
|
ml_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
|
||||||
# java_wrapper.write(' }\n')
|
ml_wrapper.write(' }\n')
|
||||||
# else:
|
else:
|
||||||
# java_wrapper.write(' {\n')
|
ml_wrapper.write(' {\n')
|
||||||
# java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
|
ml_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
|
||||||
# java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n')
|
ml_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n')
|
||||||
# java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i))
|
ml_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i))
|
||||||
# java_wrapper.write(' }\n')
|
ml_wrapper.write(' }\n')
|
||||||
# i = i + 1
|
i = i + 1
|
||||||
# # return
|
# return
|
||||||
# if result == STRING:
|
if result == STRING:
|
||||||
# java_wrapper.write(' return jenv->NewStringUTF(result);\n')
|
ml_wrapper.write(' return caml_copy_string(result);\n')
|
||||||
# elif result != VOID:
|
elif result == VOID:
|
||||||
# java_wrapper.write(' return (%s) result;\n' % type2javaw(result))
|
ml_wrapper.write(' CAMLreturn(Val_unit);\n')
|
||||||
# java_wrapper.write('}\n')
|
elif result != VOID:
|
||||||
# java_wrapper.write('#ifdef __cplusplus\n')
|
ml_wrapper.write(' return (value) result;\n')
|
||||||
# java_wrapper.write('}\n')
|
ml_wrapper.write('}\n\n')
|
||||||
# java_wrapper.write('#endif\n')
|
|
||||||
if is_verbose():
|
if is_verbose():
|
||||||
print "Generated '%s'" % ml_nativef
|
print "Generated '%s'" % ml_nativef
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,10 +0,0 @@
|
||||||
# This is a temporary support file for emacs annotations.
|
|
||||||
# It does not compile the Z3 ML API; this will be built
|
|
||||||
# in the top-level build directory.
|
|
||||||
|
|
||||||
all:
|
|
||||||
ocamlbuild -cflag -annot z3.cmxa
|
|
||||||
|
|
||||||
doc: *.ml
|
|
||||||
mkdir -p doc
|
|
||||||
ocamldoc -html -d doc -I _build -sort *.mli -hide Z3
|
|
||||||
Loading…
Reference in a new issue