mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
e2ac8c73d9
commit
d2d4bf7f83
3 changed files with 87 additions and 81 deletions
|
|
@ -1866,11 +1866,7 @@ def mk_config():
|
|||
if GPROF:
|
||||
print('gprof: enabled')
|
||||
print('Python version: %s' % distutils.sysconfig.get_python_version())
|
||||
<<<<<<< HEAD
|
||||
print('ML API: %s' % is_ml_enabled())
|
||||
=======
|
||||
print 'ML API: %s' % is_ml_enabled()
|
||||
>>>>>>> Beginnings of a new ML API
|
||||
if is_java_enabled():
|
||||
print('JNI Bindings: %s' % JNI_HOME)
|
||||
print('Java Compiler: %s' % JAVAC)
|
||||
|
|
@ -2738,9 +2734,6 @@ def mk_z3consts_ml(api_files):
|
|||
if not os.path.exists(gendir):
|
||||
os.mkdir(gendir)
|
||||
|
||||
<<<<<<< HEAD
|
||||
<<<<<<< HEAD
|
||||
<<<<<<< HEAD
|
||||
efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
efile.write('(** The enumeration types of Z3. *)\n\n')
|
||||
|
|
@ -2822,23 +2815,7 @@ def mk_z3consts_ml(api_files):
|
|||
efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
efile.write('(** The enumeration types of Z3. *)\n\n')
|
||||
=======
|
||||
efile = open('%s.ml' % os.path.join(gendir, "z3_enums"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
# efile.write('module z3_enums = struct\n\n');
|
||||
|
||||
|
||||
>>>>>>> More new ML API
|
||||
=======
|
||||
efile = open('%s.ml' % os.path.join(gendir, "enumerations"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
efile.write('module Enumerations = struct\n')
|
||||
>>>>>>> More ML API
|
||||
=======
|
||||
efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
efile.write('module Z3enums = struct\n')
|
||||
>>>>>>> New native ML API layer.
|
||||
for api_file in api_files:
|
||||
api_file_c = ml.find_file(api_file, ml.name)
|
||||
api_file = os.path.join(api_file_c.src_dir, api_file)
|
||||
|
|
@ -2884,8 +2861,6 @@ def mk_z3consts_ml(api_files):
|
|||
if m:
|
||||
name = words[1]
|
||||
if name not in DeprecatedEnums:
|
||||
<<<<<<< HEAD
|
||||
<<<<<<< HEAD
|
||||
efile.write('(** %s *)\n' % name[3:])
|
||||
efile.write('type %s =\n' % name[3:]) # strip Z3_
|
||||
for k, i in decls.iteritems():
|
||||
|
|
@ -2896,17 +2871,10 @@ def mk_z3consts_ml(api_files):
|
|||
efile.write('(** Convert int to %s*)\n' % name[3:])
|
||||
efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
|
||||
efile.write('\n')
|
||||
=======
|
||||
efile.write('\n(* %s *)\n' % name)
|
||||
=======
|
||||
>>>>>>> More ML API
|
||||
efile.write('type %s =\n' % name[3:]) # strip Z3_
|
||||
for k, i in decls.iteritems():
|
||||
<<<<<<< HEAD
|
||||
efile.write(' | %s \n' % k[3:]) # strip Z3_
|
||||
>>>>>>> More new ML API
|
||||
=======
|
||||
efile.write(' | %s \n' % k[3:]) # strip Z3_
|
||||
efile.write('\n')
|
||||
efile.write('let %s2int x : int =\n' % (name[3:])) # strip Z3_
|
||||
efile.write(' match x with\n')
|
||||
|
|
@ -2919,7 +2887,6 @@ def mk_z3consts_ml(api_files):
|
|||
efile.write(' | %d -> %s\n' % (i, k[3:]))
|
||||
# use Z3.Exception?
|
||||
efile.write(' | _ -> raise (Failure "undefined enum value")\n\n')
|
||||
>>>>>>> More ML API
|
||||
mode = SEARCHING
|
||||
else:
|
||||
if words[2] != '':
|
||||
|
|
@ -2930,21 +2897,9 @@ def mk_z3consts_ml(api_files):
|
|||
decls[words[1]] = idx
|
||||
idx = idx + 1
|
||||
linenum = linenum + 1
|
||||
<<<<<<< HEAD
|
||||
<<<<<<< HEAD
|
||||
if VERBOSE:
|
||||
print "Generated '%s/z3enums.mli'" % ('%s' % gendir)
|
||||
=======
|
||||
efile.write('\n')
|
||||
# efile.write'end\n');
|
||||
if VERBOSE:
|
||||
print "Generated '%s/z3_enums.ml'" % ('%s' % gendir)
|
||||
>>>>>>> More new ML API
|
||||
=======
|
||||
efile.write('end\n')
|
||||
if VERBOSE:
|
||||
print "Generated '%s/enumerations.ml'" % ('%s' % gendir)
|
||||
>>>>>>> More ML API
|
||||
|
||||
def mk_gui_str(id):
|
||||
return '4D2F40D8-E5F9-473B-B548-%012d' % id
|
||||
|
|
|
|||
|
|
@ -159,7 +159,7 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I
|
|||
# Mapping to ML types
|
||||
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
|
||||
STRING : 'string', STRING_PTR : 'char**',
|
||||
BOOL : 'int', SYMBOL : 'symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
|
||||
BOOL : 'int', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
|
||||
|
||||
next_type_id = FIRST_OBJ_ID
|
||||
|
||||
|
|
@ -213,10 +213,7 @@ def type2javaw(ty):
|
|||
|
||||
def type2ml(ty):
|
||||
global Type2ML
|
||||
if (ty >= FIRST_OBJ_ID):
|
||||
return 'int'
|
||||
else:
|
||||
return Type2ML[ty]
|
||||
return Type2ML[ty]
|
||||
|
||||
def _in(ty):
|
||||
return (IN, ty);
|
||||
|
|
@ -1106,6 +1103,7 @@ def is_array_param(p):
|
|||
return False
|
||||
|
||||
def mk_ml():
|
||||
global Type2Str
|
||||
if not is_ml_enabled():
|
||||
return
|
||||
ml_dir = get_component('ml').src_dir
|
||||
|
|
@ -1114,29 +1112,12 @@ def mk_ml():
|
|||
ml_native = open(ml_nativef, 'w')
|
||||
ml_native.write('(* Automatically generated file *)\n\n')
|
||||
ml_native.write('open Z3enums\n\n')
|
||||
ml_native.write('module Z3native = struct\n\n')
|
||||
ml_native.write(' type context\n')
|
||||
ml_native.write(' and symbol\n')
|
||||
ml_native.write(' and ast\n')
|
||||
ml_native.write(' and sort = private ast\n')
|
||||
ml_native.write(' and func_decl = private ast\n')
|
||||
ml_native.write(' and app = private ast\n')
|
||||
ml_native.write(' and pattern = private ast\n')
|
||||
ml_native.write(' and params\n')
|
||||
ml_native.write(' and param_descrs\n')
|
||||
ml_native.write(' and model\n')
|
||||
ml_native.write(' and func_interp\n')
|
||||
ml_native.write(' and func_entry\n')
|
||||
ml_native.write(' and fixedpoint\n')
|
||||
ml_native.write(' and ast_vector\n')
|
||||
ml_native.write(' and ast_map\n')
|
||||
ml_native.write(' and goal\n')
|
||||
ml_native.write(' and tactic\n')
|
||||
ml_native.write(' and probe\n')
|
||||
ml_native.write(' and apply_result\n')
|
||||
ml_native.write(' and solver\n')
|
||||
ml_native.write(' and stats\n\n')
|
||||
ml_native.write(' exception Exception of string\n\n')
|
||||
ml_native.write('type ptr\n')
|
||||
ml_native.write('and z3_symbol = ptr\n')
|
||||
for k, v in Type2Str.iteritems():
|
||||
if is_obj(k):
|
||||
ml_native.write('and %s = ptr\n' % v.lower())
|
||||
ml_native.write('\nexception Exception of string\n\n')
|
||||
|
||||
# ML declarations
|
||||
ml_native.write(' module ML2C = struct\n\n')
|
||||
|
|
@ -1192,9 +1173,9 @@ def mk_ml():
|
|||
i = i + 1
|
||||
ml_native.write(') in\n')
|
||||
if len(params) > 0 and param_type(params[0]) == CONTEXT:
|
||||
ml_native.write(' let err = (Z3enums.int2error_code (ML2C.n_get_error_code a0)) in \n')
|
||||
ml_native.write(' if err <> Z3enums.OK then\n')
|
||||
ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (Z3enums.error_code2int err)))\n')
|
||||
ml_native.write(' let err = (int2error_code (ML2C.n_get_error_code a0)) in \n')
|
||||
ml_native.write(' if err <> OK then\n')
|
||||
ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (error_code2int err)))\n')
|
||||
ml_native.write(' else\n')
|
||||
if result == VOID:
|
||||
ml_native.write(' ()\n')
|
||||
|
|
@ -1202,8 +1183,6 @@ def mk_ml():
|
|||
ml_native.write(' res\n')
|
||||
ml_native.write('\n')
|
||||
|
||||
ml_native.write('end\n')
|
||||
|
||||
# C interface
|
||||
ml_wrapper = open(ml_wrapperf, 'w')
|
||||
ml_wrapper.write('// Automatically generated file\n\n')
|
||||
|
|
|
|||
|
|
@ -1,11 +1,83 @@
|
|||
(*
|
||||
Author: CM Wintersteiger
|
||||
(C) Microsoft Research, 2012
|
||||
*)
|
||||
*)
|
||||
|
||||
open Z3enums
|
||||
open Z3native
|
||||
|
||||
module Z3 = struct
|
||||
class context =
|
||||
object (self)
|
||||
val m_n_ctx : Z3native.z3_context option = None
|
||||
val mutable m_refCount : int = 0
|
||||
initializer Gc.finalise (fun self -> self#dispose ()) self
|
||||
method dispose () =
|
||||
Printf.printf "Disposing %d \n" (Oo.id self) ;
|
||||
match m_n_ctx with
|
||||
| Some(x) -> (del_context x)
|
||||
| None -> ()
|
||||
method sub_one_ctx_obj = m_refCount <- m_refCount - 1
|
||||
method add_one_ctx_obj = m_refCount <- m_refCount + 1
|
||||
end
|
||||
|
||||
class virtual z3object ctx_init obj_init =
|
||||
object (self)
|
||||
val mutable m_ctx : context option = ctx_init
|
||||
val mutable m_n_obj : Z3native.ptr option = obj_init
|
||||
|
||||
initializer
|
||||
(match m_n_obj with
|
||||
| Some (x) -> self#incref x;
|
||||
(match m_ctx with
|
||||
| Some(x) -> x#add_one_ctx_obj
|
||||
| None -> ()
|
||||
)
|
||||
| None -> ()
|
||||
);
|
||||
Gc.finalise (fun self -> self#dispose ()) self
|
||||
|
||||
method virtual incref : Z3native.ptr -> unit
|
||||
method virtual decref : Z3native.ptr -> unit
|
||||
|
||||
(*
|
||||
Disposes of the underlying native Z3 object.
|
||||
*)
|
||||
method dispose () =
|
||||
Printf.printf "Disposing %d \n" (Oo.id self) ;
|
||||
(match m_n_obj with
|
||||
| Some (x) -> self#decref x; m_n_obj <- None
|
||||
| None -> ()
|
||||
);
|
||||
(match m_ctx with
|
||||
| Some (x) -> x#sub_one_ctx_obj
|
||||
| None -> ()
|
||||
);
|
||||
m_ctx <- None
|
||||
|
||||
|
||||
method get_native_object = m_n_obj
|
||||
|
||||
method set_native_object x =
|
||||
(match x with
|
||||
| Some(x) -> self#incref x
|
||||
| None -> ()
|
||||
);
|
||||
(match m_n_obj with
|
||||
| Some(x) -> self#decref x
|
||||
| None -> ()
|
||||
);
|
||||
m_n_obj <- x
|
||||
|
||||
method get_context = m_ctx
|
||||
|
||||
method array_to_native a =
|
||||
let f e = e#get_native_object in
|
||||
(Array.map f a)
|
||||
|
||||
method array_length a =
|
||||
match a with
|
||||
| Some(x) -> (Array.length x)
|
||||
| None -> 0
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue