mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
ML API: bug and build fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
e40b69d97f
commit
544a74f034
4 changed files with 40 additions and 26 deletions
|
|
@ -1350,26 +1350,30 @@ class MLComponent(Component):
|
|||
mk_dir(os.path.join(BUILD_DIR, sub_dir))
|
||||
api_src = get_component(API_COMPONENT).to_src_dir
|
||||
for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)):
|
||||
out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f))
|
||||
str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f)
|
||||
if IS_WINDOWS: str = str.replace('/','\\')
|
||||
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
|
||||
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
|
||||
out.write(str)
|
||||
for f in filter(lambda f: f.endswith('.mli'), os.listdir(self.src_dir)):
|
||||
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
|
||||
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
|
||||
out.write(str)
|
||||
for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)):
|
||||
out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f))
|
||||
str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f)
|
||||
if IS_WINDOWS: str = str.replace('/','\\')
|
||||
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
|
||||
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
|
||||
out.write(str)
|
||||
modules = ["z3enums", "z3native", "z3"] # dependencies in this order!
|
||||
prev = ''
|
||||
for m in modules:
|
||||
out.write('%s/%s.mli: %s/%s.ml %s\n' % (sub_dir,m,sub_dir,m,prev))
|
||||
out.write('\t%s -I %s -i -c %s/%s.ml > %s/%s.mli\n' % (OCAMLC,sub_dir,sub_dir,m,sub_dir,m))
|
||||
prev = prev + ' ' + sub_dir + '/' + m + '.mli'
|
||||
fn = os.path.join(self.src_dir, ('%s.mli' % m))
|
||||
if not os.path.exists(fn):
|
||||
out.write('%s.mli: %s.ml %s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m),prev))
|
||||
out.write('\t%s -I %s -i -c %s.ml > %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir, m),os.path.join(sub_dir, m)))
|
||||
prev = prev + ' ' + os.path.join(sub_dir, m) + '.mli'
|
||||
cmis = ''
|
||||
for m in modules:
|
||||
out.write('%s/%s.cmi: %s/%s.mli\n' % (sub_dir,m,sub_dir,m))
|
||||
out.write('\t%s -I %s -c %s/%s.mli\n' % (OCAMLC,sub_dir,sub_dir,m))
|
||||
cmis = cmis + ' ' + sub_dir + '/' + m + '.cmi'
|
||||
out.write('%s.cmi: %s.mli\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m)))
|
||||
out.write('\t%s -I %s -c %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir,m)))
|
||||
cmis = cmis + ' ' + os.path.join(sub_dir,m) + '.cmi'
|
||||
out.write('api/ml/libz3ml$(LIB_EXT): api/ml/z3native.c %s$(SO_EXT)\n' % get_component(Z3_DLL_COMPONENT).dll_name)
|
||||
out.write('\t$(CXX) $(CXXFLAGS) -I %s -I %s %s/z3native.c $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT)\n' % (OCAML_LIB, api_src, sub_dir))
|
||||
out.write('\t$(AR) $(AR_FLAGS) $(AR_OUTFLAG)api/ml/libz3ml$(LIB_EXT) api/ml/z3native$(OBJ_EXT)\n')
|
||||
|
|
|
|||
|
|
@ -1185,7 +1185,8 @@ def mk_ml():
|
|||
ip = inparams(params)
|
||||
op = outparams(params)
|
||||
if len(ip) == 0:
|
||||
ml_native.write(' unit -> ')
|
||||
ml_native.write(' unit -> ')
|
||||
ml_i.write(' unit -> ')
|
||||
for p in ip:
|
||||
ml_native.write('%s -> ' % param2ml(p))
|
||||
ml_i.write('%s -> ' % param2ml(p))
|
||||
|
|
@ -1233,6 +1234,8 @@ def mk_ml():
|
|||
ml_native.write(' ')
|
||||
ml_native.write('a%d' % i)
|
||||
i = i + 1
|
||||
if len(ip) == 0:
|
||||
ml_native.write('()')
|
||||
ml_native.write(' = \n')
|
||||
ml_native.write(' ')
|
||||
if result == VOID and len(op) == 0:
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ struct
|
|||
)
|
||||
|
||||
let create_context settings =
|
||||
let cfg = Z3native.mk_config in
|
||||
let cfg = Z3native.mk_config () in
|
||||
let f e = (Z3native.set_param_value cfg (fst e) (snd e)) in
|
||||
(List.iter f settings) ;
|
||||
let v = Z3native.mk_context_rc cfg in
|
||||
|
|
@ -101,12 +101,12 @@ end
|
|||
|
||||
module Version =
|
||||
struct
|
||||
let major = let (x, _, _, _) = Z3native.get_version in x
|
||||
let minor = let (_, x, _, _) = Z3native.get_version in x
|
||||
let build = let (_, _, x, _) = Z3native.get_version in x
|
||||
let revision = let (_, _, _, x) = Z3native.get_version in x
|
||||
let major = let (x, _, _, _) = Z3native.get_version () in x
|
||||
let minor = let (_, x, _, _) = Z3native.get_version () in x
|
||||
let build = let (_, _, x, _) = Z3native.get_version () in x
|
||||
let revision = let (_, _, _, x) = Z3native.get_version () in x
|
||||
let to_string =
|
||||
let (mj, mn, bld, rev) = Z3native.get_version in
|
||||
let (mj, mn, bld, rev) = Z3native.get_version () in
|
||||
string_of_int mj ^ "." ^
|
||||
string_of_int mn ^ "." ^
|
||||
string_of_int bld ^ "." ^
|
||||
|
|
@ -609,6 +609,10 @@ sig
|
|||
val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
|
||||
val mk_params : context -> params
|
||||
val to_string : params -> string
|
||||
|
||||
val update_param_value : context -> string -> string -> unit
|
||||
val get_param_value : context -> string -> string option
|
||||
val set_print_mode : context -> Z3enums.ast_print_mode -> unit
|
||||
end = struct
|
||||
type params = z3_native_object
|
||||
|
||||
|
|
@ -1099,7 +1103,7 @@ struct
|
|||
end
|
||||
|
||||
|
||||
module Array =
|
||||
module Z3Array =
|
||||
struct
|
||||
let mk_sort ( ctx : context ) ( domain : sort ) ( range : sort ) =
|
||||
sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range))
|
||||
|
|
@ -1382,7 +1386,7 @@ struct
|
|||
end
|
||||
|
||||
|
||||
module List =
|
||||
module Z3List =
|
||||
struct
|
||||
let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : sort ) =
|
||||
let (r, _, _, _, _, _, _) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) (Sort.gno elem_sort)) in
|
||||
|
|
@ -2038,7 +2042,7 @@ struct
|
|||
if not r then
|
||||
None
|
||||
else
|
||||
expr_of_ptr (z3obj_gc x) v
|
||||
Some(expr_of_ptr (z3obj_gc x) v)
|
||||
|
||||
let evaluate ( x : model ) ( t : expr ) ( completion : bool ) =
|
||||
eval x t completion
|
||||
|
|
@ -2331,7 +2335,7 @@ struct
|
|||
if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then
|
||||
(Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i))
|
||||
else
|
||||
(Entry.create_sd k (Z3native.stats_get_float_value (z3obj_gnc x) (z3obj_gno x) i))
|
||||
(Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i))
|
||||
) in
|
||||
mk_list f n
|
||||
|
||||
|
|
@ -2667,3 +2671,6 @@ let global_param_reset_all =
|
|||
let toggle_warning_messages ( enabled: bool ) =
|
||||
Z3native.toggle_warning_messages enabled
|
||||
|
||||
|
||||
module Array = Z3Array
|
||||
module List = Z3List
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@
|
|||
(** General Z3 exceptions
|
||||
|
||||
Many functions in this API may throw an exception; if they do, it is this one.*)
|
||||
exception Error
|
||||
exception Error of string
|
||||
|
||||
(** Context objects.
|
||||
|
||||
|
|
@ -55,11 +55,11 @@ module Log :
|
|||
sig
|
||||
(** Open an interaction log file.
|
||||
@return True if opening the log file succeeds, false otherwise. *)
|
||||
(* CMW: "open" seems to be a reserved keyword? *)
|
||||
(* CMW: "open" is a reserved keyword. *)
|
||||
val open_ : string -> bool
|
||||
|
||||
(** Closes the interaction log. *)
|
||||
val close : unit
|
||||
val close : unit -> unit
|
||||
|
||||
(** Appends a user-provided string to the interaction log. *)
|
||||
val append : string -> unit
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue