mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

More new OCaml API

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-14 19:56:22 +00:00
parent 824169da0a
commit b99fcb9c8a
6 changed files with 165 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
examples/ml/ml_example.ml
View file

@ -190,9 +190,10 @@ let basic_tests ( ctx : context ) =
(* Error handling test. *) (* Error handling test. *)
try ( try (
let i = Integer.mk_numeral_s ctx "1/2" in let i = Integer.mk_numeral_s ctx "1/2" in
raise (TestFailedException (numeral_to_string i)) (* unreachable *) Printf.printf "%s\n" (Expr.to_string i) ;
raise (TestFailedException "check")
) )
with Z3native.Exception(_) -> ( with Z3.Error(_) -> (
Printf.printf "Exception caught, OK.\n" Printf.printf "Exception caught, OK.\n"
) )
@ -342,7 +343,7 @@ let _ =
); );
Printf.printf "Exiting.\n" ; Printf.printf "Exiting.\n" ;
exit 0 exit 0
) with Z3native.Exception(msg) -> ( ) with Error(msg) -> (
Printf.printf "Z3 EXCEPTION: %s\n" msg ; Printf.printf "Z3 EXCEPTION: %s\n" msg ;
exit 1 exit 1
) )

25
scripts/mk_util.py
View file

@ -1797,6 +1797,12 @@ class MLComponent(Component):
if IS_WINDOWS: if IS_WINDOWS:
CP_CMD='copy' CP_CMD='copy'
OCAML_FLAGS = ''
if DEBUG_MODE:
OCAML_FLAGS += '-g'
OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
src_dir = self.to_src_dir src_dir = self.to_src_dir
mk_dir(os.path.join(BUILD_DIR, self.sub_dir)) mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
api_src = get_component(API_COMPONENT).to_src_dir api_src = get_component(API_COMPONENT).to_src_dir
@ -1818,7 +1824,7 @@ class MLComponent(Component):
z3dllso = get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)' z3dllso = get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)'
out.write('%s: %s %s\n' % (stubso, stubsc, z3dllso)) out.write('%s: %s %s\n' % (stubso, stubsc, z3dllso))
out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' % out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
(OCAMLC, OCAML_LIB, api_src, src_dir, stubso, stubsc)) (OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc))
cmos = '' cmos = ''
for m in self.modules: for m in self.modules:
@ -1831,9 +1837,9 @@ class MLComponent(Component):
if (os.path.exists(existing_mli[3:])): if (os.path.exists(existing_mli[3:])):
out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli)) out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli))
else: else:
out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLC, self.sub_dir, ml, mli)) out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLCF, self.sub_dir, ml, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, cmi, mli)) out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmi, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, cmo, ml)) out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmo, ml))
cmos = cmos + cmo + ' ' cmos = cmos + cmo + ' '
cmxs = '' cmxs = ''
@ -1841,17 +1847,20 @@ class MLComponent(Component):
ff = os.path.join(src_dir, m + '.ml') ff = os.path.join(src_dir, m + '.ml')
ft = os.path.join(self.sub_dir, m + '.cmx') ft = os.path.join(self.sub_dir, m + '.cmx')
out.write('%s: %s %s\n' % (ft, ff, cmos)) out.write('%s: %s %s\n' % (ft, ff, cmos))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPT, self.sub_dir, ft, ff)) out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPTF, self.sub_dir, ft, ff))
cmxs = cmxs + ' ' + ft cmxs = cmxs + ' ' + ft
OCAMLMKLIB = 'ocamlmklib'
if DEBUG_MODE:
OCAMLMKLIB += ' -g'
z3mls = os.path.join(self.sub_dir, 'z3ml') z3mls = os.path.join(self.sub_dir, 'z3ml')
out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso)) out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmos)) out.write('\t%s -o %s -I %s %s %s -L. -lz3\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos))
out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso)) out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmxs)) out.write('\t%s -o %s -I %s %s %s -L. -lz3\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs))
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls)) out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPT, z3mls, self.sub_dir, z3mls)) out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
out.write('\n') out.write('\n')
out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))

88
scripts/update_api.py
View file

@ -469,7 +469,7 @@ def mk_dotnet():
dotnet.write(' }\n') dotnet.write(' }\n')
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ]
Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ] Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
def mk_dotnet_wrappers(): def mk_dotnet_wrappers():
@ -1228,7 +1228,7 @@ def ml_plus_ops_type(ts):
if ml_has_plus_type(ts): if ml_has_plus_type(ts):
return ml_plus_type(ts) + '_custom_ops' return ml_plus_type(ts) + '_custom_ops'
else: else:
return 'Z3_default_custom_ops' return 'default_custom_ops'
def ml_has_plus_type(ts): def ml_has_plus_type(ts):
return ts != ml_plus_type(ts) return ts != ml_plus_type(ts)
@ -1268,9 +1268,8 @@ def ml_set_wrap(t, d, n):
elif t == STRING: elif t == STRING:
return d + ' = caml_copy_string((const char*) ' + n + ');' return d + ' = caml_copy_string((const char*) ' + n + ');'
else: else:
ts = type2str(t) pts = ml_plus_type(type2str(t))
pts = ml_plus_type(ts) return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';'
return 'memcpy(Data_custom_val(' + d + '), &' + n + ', sizeof(' + pts + '));'
def mk_z3native_ml(ml_dir): def mk_z3native_ml(ml_dir):
ml_nativef = os.path.join(ml_dir, 'z3native.ml') ml_nativef = os.path.join(ml_dir, 'z3native.ml')
@ -1332,13 +1331,8 @@ def mk_z3native_ml(ml_dir):
i = i + 1 i = i + 1
if len(ip) == 0: if len(ip) == 0:
ml_native.write('()') ml_native.write('()')
ml_native.write(' = \n') ml_native.write(' = ')
ml_native.write(' ') ml_native.write('ML2C.n_%s' % (ml_method_name(name)))
if result == VOID and len(op) == 0:
ml_native.write('let _ = ')
else:
ml_native.write('let res = ')
ml_native.write('(ML2C.n_%s' % (ml_method_name(name)))
if len(ip) == 0: if len(ip) == 0:
ml_native.write(' ()') ml_native.write(' ()')
first = True first = True
@ -1347,16 +1341,6 @@ def mk_z3native_ml(ml_dir):
if is_in_param(p): if is_in_param(p):
ml_native.write(' a%d' % i) ml_native.write(' a%d' % i)
i = i + 1 i = i + 1
ml_native.write(') in\n')
if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT:
ml_native.write(' let err = (error_code_of_int (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 a0 (int_of_error_code err)))\n')
ml_native.write(' else\n')
if result == VOID and len(op) == 0:
ml_native.write(' ()\n')
else:
ml_native.write(' res\n')
ml_native.write('\n') ml_native.write('\n')
ml_native.write('(**/**)\n') ml_native.write('(**/**)\n')
ml_native.close() ml_native.close()
@ -1427,11 +1411,13 @@ def mk_z3native_stubs_c(ml_dir): # C interface
ml_wrapper.write(' unsigned _i;\n') ml_wrapper.write(' unsigned _i;\n')
# declare locals, preprocess arrays, strings, in/out arguments # declare locals, preprocess arrays, strings, in/out arguments
have_context = False
i = 0 i = 0
for param in params: for param in params:
if param_type(param) == CONTEXT and i == 0: if param_type(param) == CONTEXT and i == 0:
ml_wrapper.write(' Z3_context_plus * ctx_p = (Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n') ml_wrapper.write(' Z3_context_plus * ctx_p = (Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n') ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n')
have_context = True
else: else:
k = param_kind(param) k = param_kind(param)
if k == OUT_ARRAY: if k == OUT_ARRAY:
@ -1468,20 +1454,14 @@ def mk_z3native_stubs_c(ml_dir): # C interface
i = i + 1 i = i + 1
ml_wrapper.write(' ') ml_wrapper.write(' ')
need_closing_paren = False
if result != VOID: if result != VOID:
ts = type2str(result) ts = type2str(result)
ml_wrapper.write('result = caml_alloc(%s, 0);\n' % ret_size)
if ml_has_plus_type(ts): if ml_has_plus_type(ts):
pts = ml_plus_type(ts) ml_wrapper.write(' %s z3rv_m = ' % ts)
ml_wrapper.write('result = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (ml_plus_ops_type(ts), pts))
if ts == 'Z3_context':
ml_wrapper.write(' %s z3rv = %s_mk(' % (pts, pts))
else:
ml_wrapper.write(' %s z3rv = %s_mk(ctx_p, (%s) ' % (pts, pts, ml_minus_type(ts)))
need_closing_paren = True
else: else:
ml_wrapper.write('result = caml_alloc(%s, 0);\n' % ret_size)
ml_wrapper.write(' %s z3rv = ' % ts) ml_wrapper.write(' %s z3rv = ' % ts)
elif len(op) != 0: elif len(op) != 0:
ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size) ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size)
@ -1500,35 +1480,51 @@ def mk_z3native_stubs_c(ml_dir): # C interface
else: else:
ml_wrapper.write('_a%i' % i) ml_wrapper.write('_a%i' % i)
i = i + 1 i = i + 1
ml_wrapper.write(')') ml_wrapper.write(');\n')
if need_closing_paren:
ml_wrapper.write(')'); if have_context and name not in Unwrapped:
ml_wrapper.write(';\n') ml_wrapper.write(' int ec = Z3_get_error_code(ctx_p->ctx);\n')
ml_wrapper.write(' if (ec != 0) {\n')
ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n')
ml_wrapper.write(' caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), msg);\n')
ml_wrapper.write(' }\n')
if result != VOID:
ts = type2str(result)
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
ml_wrapper.write(' result = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (ml_plus_ops_type(ts), pts))
if name in NULLWrapped:
ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts))
else:
ml_wrapper.write(' %s z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, pts, ml_minus_type(ts)))
# convert output params # convert output params
if len(op) > 0: if len(op) > 0:
i = 0 i = 0
for p in params: for p in params:
pt = param_type(p)
ts = type2str(pt)
if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY: if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p))) ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p)))
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(p)) ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(p))
if ml_has_plus_type(ts): pts = ml_plus_type(ts)
pts = ml_plus_type(ts) pops = ml_plus_ops_type(ts)
ml_wrapper.write(' value t;\n') ml_wrapper.write(' value t;\n')
ml_wrapper.write(' t = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (ml_plus_ops_type(ts), pts)) ml_wrapper.write(' t = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (pops, pts))
if ml_has_plus_type(ts):
ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i]);\n' % (pts, i, pts, ml_minus_type(ts), i)) ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i]);\n' % (pts, i, pts, ml_minus_type(ts), i))
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), 't', '_a%dp' % i)) ml_wrapper.write(' %s\n' % ml_set_wrap(pt, 't', '_a%dp' % i))
else: else:
ml_wrapper.write(' value t;\n') ml_wrapper.write(' %s\n' % ml_set_wrap(pt, 't', '_a%d[_i]' % i))
ml_wrapper.write(' t = caml_alloc_custom(&default_custom_ops, sizeof(%s), 0, 1);\n' % (ts))
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), 't', '_a%d[_i]' % i))
ml_wrapper.write(' Store_field(_a%s_val, _i, t);\n' % i) ml_wrapper.write(' Store_field(_a%s_val, _i, t);\n' % i)
ml_wrapper.write(' }\n') ml_wrapper.write(' }\n')
elif param_kind(p) == OUT_MANAGED_ARRAY: elif param_kind(p) == OUT_MANAGED_ARRAY:
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), '_a%d_val' % i, '_a%d' % i)) wrp = ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i)
wrp = wrp.replace('*)', '**)')
wrp = wrp.replace('_plus', '')
ml_wrapper.write(' %s\n' % wrp)
elif is_out_param(p): elif is_out_param(p):
pt = param_type(p)
ts = type2str(pt)
if ml_has_plus_type(ts): if ml_has_plus_type(ts):
pts = ml_plus_type(ts) pts = ml_plus_type(ts)
ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (pts, i, pts, ml_minus_type(ts), i)) ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (pts, i, pts, ml_minus_type(ts), i))

87
src/api/ml/z3.ml
View file

@ -7,7 +7,8 @@
open Z3enums open Z3enums
exception Error = Z3native.Exception exception Error of string
let _ = Callback.register_exception "Z3EXCEPTION" (Error "")
(* Some helpers. *) (* Some helpers. *)
let null = Z3native.mk_null() let null = Z3native.mk_null()
@ -90,7 +91,7 @@ end
module rec AST : module rec AST :
sig sig
type ast = Z3native.ast type ast = Z3native.ast
val gc:ast -> context val gc : ast -> context
module ASTVector : module ASTVector :
sig sig
type ast_vector = Z3native.ast_vector type ast_vector = Z3native.ast_vector
@ -225,7 +226,7 @@ end
and Sort : and Sort :
sig sig
type sort = Z3native.sort type sort = AST.ast
val gc : sort -> context val gc : sort -> context
val equal : sort -> sort -> bool val equal : sort -> sort -> bool
val get_id : sort -> int val get_id : sort -> int
@ -296,7 +297,7 @@ val gc : func_decl -> context
val get_parameters : func_decl -> Parameter.parameter list val get_parameters : func_decl -> Parameter.parameter list
val apply : func_decl -> Expr.expr list -> Expr.expr val apply : func_decl -> Expr.expr list -> Expr.expr
end = struct end = struct
type func_decl = Z3native.func_decl type func_decl = AST.ast
let gc (x:func_decl) = Z3native.context_of_ast x let gc (x:func_decl) = Z3native.context_of_ast x
module Parameter = module Parameter =
@ -323,37 +324,37 @@ end = struct
let get_int (x:parameter) = let get_int (x:parameter) =
match x with match x with
| P_Int(x) -> x | P_Int(x) -> x
| _ -> raise (Z3native.Exception "parameter is not an int") | _ -> raise (Error "parameter is not an int")
let get_float (x:parameter) = let get_float (x:parameter) =
match x with match x with
| P_Dbl(x) -> x | P_Dbl(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a float") | _ -> raise (Error "parameter is not a float")
let get_symbol (x:parameter) = let get_symbol (x:parameter) =
match x with match x with
| P_Sym(x) -> x | P_Sym(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a symbol") | _ -> raise (Error "parameter is not a symbol")
let get_sort (x:parameter) = let get_sort (x:parameter) =
match x with match x with
| P_Srt(x) -> x | P_Srt(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a sort") | _ -> raise (Error "parameter is not a sort")
let get_ast (x:parameter) = let get_ast (x:parameter) =
match x with match x with
| P_Ast(x) -> x | P_Ast(x) -> x
| _ -> raise (Z3native.Exception "parameter is not an ast") | _ -> raise (Error "parameter is not an ast")
let get_func_decl (x:parameter) = let get_func_decl (x:parameter) =
match x with match x with
| P_Fdl(x) -> x | P_Fdl(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a func_decl") | _ -> raise (Error "parameter is not a func_decl")
let get_rational (x:parameter) = let get_rational (x:parameter) =
match x with match x with
| P_Rat(x) -> x | P_Rat(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a rational string") | _ -> raise (Error "parameter is not a rational string")
end end
let mk_func_decl (ctx:context) (name:Symbol.symbol) (domain:Sort.sort list) (range:Sort.sort) = let mk_func_decl (ctx:context) (name:Symbol.symbol) (domain:Sort.sort list) (range:Sort.sort) =
@ -469,7 +470,7 @@ end
(** General expressions (terms) *) (** General expressions (terms) *)
and Expr : and Expr :
sig sig
type expr = Z3native.ast type expr = AST.ast
val gc : expr -> context val gc : expr -> context
val ast_of_expr : expr -> AST.ast val ast_of_expr : expr -> AST.ast
val expr_of_ast : AST.ast -> expr val expr_of_ast : AST.ast -> expr
@ -504,13 +505,13 @@ sig
val apply4 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr -> expr val apply4 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr -> expr
val compare : expr -> expr -> int val compare : expr -> expr -> int
end = struct end = struct
type expr = Z3native.ast type expr = AST.ast
let gc (e:expr) = Z3native.context_of_ast e let gc (e:expr) = Z3native.context_of_ast e
let expr_of_ast (a:AST.ast) : expr = let expr_of_ast (a:AST.ast) : expr =
let q = Z3enums.ast_kind_of_int (Z3native.get_ast_kind (gc a) a) in let q = Z3enums.ast_kind_of_int (Z3native.get_ast_kind (gc a) a) in
if (q != Z3enums.APP_AST && q != VAR_AST && q != QUANTIFIER_AST && q != NUMERAL_AST) then if (q != Z3enums.APP_AST && q != VAR_AST && q != QUANTIFIER_AST && q != NUMERAL_AST) then
raise (Z3native.Exception "Invalid coercion") raise (Error "Invalid coercion")
else else
a a
@ -540,13 +541,13 @@ end = struct
let update (x:expr) (args:expr list) = let update (x:expr) (args:expr list) =
if ((AST.is_app x) && (List.length args <> (get_num_args x))) then if ((AST.is_app x) && (List.length args <> (get_num_args x))) then
raise (Z3native.Exception "Number of arguments does not match") raise (Error "Number of arguments does not match")
else else
Z3native.update_term (gc x) x (List.length args) (Array.of_list args) Z3native.update_term (gc x) x (List.length args) (Array.of_list args)
let substitute (x:expr) (from:expr list) (to_:expr list) = let substitute (x:expr) (from:expr list) (to_:expr list) =
if (List.length from) <> (List.length to_) then if (List.length from) <> (List.length to_) then
raise (Z3native.Exception "Argument sizes do not match") raise (Error "Argument sizes do not match")
else else
Z3native.substitute (gc x) x (List.length from) (Array.of_list from) (Array.of_list to_) Z3native.substitute (gc x) x (List.length from) (Array.of_list from) (Array.of_list to_)
@ -620,7 +621,7 @@ end
module Quantifier = module Quantifier =
struct struct
type quantifier = Z3native.ast type quantifier = AST.ast
let gc (x:quantifier) = Z3native.context_of_ast x let gc (x:quantifier) = Z3native.context_of_ast x
let expr_of_quantifier (q:quantifier) : Expr.expr = q let expr_of_quantifier (q:quantifier) : Expr.expr = q
@ -628,7 +629,7 @@ struct
let quantifier_of_expr (e:Expr.expr) : quantifier = let quantifier_of_expr (e:Expr.expr) : quantifier =
let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (gc e) e)) in let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (gc e) e)) in
if (q != Z3enums.QUANTIFIER_AST) then if (q != Z3enums.QUANTIFIER_AST) then
raise (Z3native.Exception "Invalid coercion") raise (Error "Invalid coercion")
else else
e e
@ -650,7 +651,7 @@ struct
let get_index (x:expr) = let get_index (x:expr) =
if not (AST.is_var x) then if not (AST.is_var x) then
raise (Z3native.Exception "Term is not a bound variable.") raise (Error "Term is not a bound variable.")
else else
Z3native.get_index_value (gc x) x Z3native.get_index_value (gc x) x
@ -687,13 +688,13 @@ struct
let mk_pattern (ctx:context) (terms:expr list) = let mk_pattern (ctx:context) (terms:expr list) =
if (List.length terms) == 0 then if (List.length terms) == 0 then
raise (Z3native.Exception "Cannot create a pattern from zero terms") raise (Error "Cannot create a pattern from zero terms")
else else
Z3native.mk_pattern ctx (List.length terms) (Array.of_list terms) Z3native.mk_pattern ctx (List.length terms) (Array.of_list terms)
let mk_forall (ctx:context) (sorts:Sort.sort list) (names:Symbol.symbol list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = let mk_forall (ctx:context) (sorts:Sort.sort list) (names:Symbol.symbol list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) =
if (List.length sorts) != (List.length names) then if (List.length sorts) != (List.length names) then
raise (Z3native.Exception "Number of sorts does not match number of names") raise (Error "Number of sorts does not match number of names")
else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
Z3native.mk_quantifier ctx true Z3native.mk_quantifier ctx true
(match weight with | None -> 1 | Some(x) -> x) (match weight with | None -> 1 | Some(x) -> x)
@ -731,7 +732,7 @@ struct
let mk_exists (ctx:context) (sorts:Sort.sort list) (names:Symbol.symbol list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = let mk_exists (ctx:context) (sorts:Sort.sort list) (names:Symbol.symbol list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) =
if (List.length sorts) != (List.length names) then if (List.length sorts) != (List.length names) then
raise (Z3native.Exception "Number of sorts does not match number of names") raise (Error "Number of sorts does not match number of names")
else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
Z3native.mk_quantifier ctx false Z3native.mk_quantifier ctx false
(match weight with | None -> 1 | Some(x) -> x) (match weight with | None -> 1 | Some(x) -> x)
@ -856,7 +857,7 @@ struct
let get_size (x:Sort.sort) = let get_size (x:Sort.sort) =
let (r, v) = (Z3native.get_finite_domain_sort_size (Sort.gc x) x) in let (r, v) = (Z3native.get_finite_domain_sort_size (Sort.gc x) x) in
if r then v if r then v
else raise (Z3native.Exception "Conversion failed.") else raise (Error "Conversion failed.")
end end
@ -907,10 +908,10 @@ struct
let create (ctx:context) (name:Symbol.symbol) (recognizer:Symbol.symbol) (field_names:Symbol.symbol list) (sorts:Sort.sort option list) (sort_refs:int list) = let create (ctx:context) (name:Symbol.symbol) (recognizer:Symbol.symbol) (field_names:Symbol.symbol list) (sorts:Sort.sort option list) (sort_refs:int list) =
let n = (List.length field_names) in let n = (List.length field_names) in
if n != (List.length sorts) then if n != (List.length sorts) then
raise (Z3native.Exception "Number of field names does not match number of sorts") raise (Error "Number of field names does not match number of sorts")
else else
if n != (List.length sort_refs) then if n != (List.length sort_refs) then
raise (Z3native.Exception "Number of field names does not match number of sort refs") raise (Error "Number of field names does not match number of sort refs")
else else
let no = Z3native.mk_constructor ctx name let no = Z3native.mk_constructor ctx name
recognizer recognizer
@ -1098,14 +1099,14 @@ struct
let get_int (x:expr) = let get_int (x:expr) =
let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in
if r then v if r then v
else raise (Z3native.Exception "Conversion failed.") else raise (Error "Conversion failed.")
let get_big_int (x:expr) = let get_big_int (x:expr) =
if (is_int_numeral x) then if (is_int_numeral x) then
let s = (Z3native.get_numeral_string (Expr.gc x) x) in let s = (Z3native.get_numeral_string (Expr.gc x) x) in
Big_int.big_int_of_string s Big_int.big_int_of_string s
else else
raise (Z3native.Exception "Conversion failed.") raise (Error "Conversion failed.")
let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx)
@ -1129,7 +1130,7 @@ struct
let s = (Z3native.get_numeral_string (Expr.gc x) x) in let s = (Z3native.get_numeral_string (Expr.gc x) x) in
Ratio.ratio_of_string s Ratio.ratio_of_string s
else else
raise (Z3native.Exception "Conversion failed.") raise (Error "Conversion failed.")
let to_decimal_string (x:expr) (precision:int) = Z3native.get_numeral_decimal_string (Expr.gc x) x precision let to_decimal_string (x:expr) (precision:int) = Z3native.get_numeral_decimal_string (Expr.gc x) x precision
let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
@ -1137,7 +1138,7 @@ struct
let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name) let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name)
let mk_numeral_nd (ctx:context) (num:int) (den:int) = let mk_numeral_nd (ctx:context) (num:int) (den:int) =
if (den == 0) then if (den == 0) then
raise (Z3native.Exception "Denominator is zero") raise (Error "Denominator is zero")
else else
Z3native.mk_real ctx num den Z3native.mk_real ctx num den
@ -1228,7 +1229,7 @@ struct
let get_int (x:expr) = let get_int (x:expr) =
let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in
if r then v if r then v
else raise (Z3native.Exception "Conversion failed.") else raise (Error "Conversion failed.")
let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
let mk_const (ctx:context) (name:Symbol.symbol) (size:int) = let mk_const (ctx:context) (name:Symbol.symbol) (size:int) =
Expr.mk_const ctx name (mk_sort ctx size) Expr.mk_const ctx name (mk_sort ctx size)
@ -1490,7 +1491,7 @@ struct
Z3native.apply_result_inc_ref (gc x) arn ; Z3native.apply_result_inc_ref (gc x) arn ;
let sg = Z3native.apply_result_get_num_subgoals (gc x) arn in let sg = Z3native.apply_result_get_num_subgoals (gc x) arn in
let res = if sg == 0 then let res = if sg == 0 then
raise (Z3native.Exception "No subgoals") raise (Error "No subgoals")
else else
Z3native.apply_result_get_subgoal (gc x) arn 0 in Z3native.apply_result_get_subgoal (gc x) arn 0 in
Z3native.apply_result_dec_ref (gc x) arn ; Z3native.apply_result_dec_ref (gc x) arn ;
@ -1570,7 +1571,7 @@ struct
let get_const_interp (x:model) (f:func_decl) = let get_const_interp (x:model) (f:func_decl) =
if (FuncDecl.get_arity f) != 0 || if (FuncDecl.get_arity f) != 0 ||
(sort_kind_of_int (Z3native.get_sort_kind (FuncDecl.gc f) (Z3native.get_range (FuncDecl.gc f) f))) == ARRAY_SORT then (sort_kind_of_int (Z3native.get_sort_kind (FuncDecl.gc f) (Z3native.get_range (FuncDecl.gc f) f))) == ARRAY_SORT then
raise (Z3native.Exception "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.") raise (Error "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.")
else else
let np = Z3native.model_get_const_interp (gc x) x f in let np = Z3native.model_get_const_interp (gc x) x f in
if (Z3native.is_null np) then if (Z3native.is_null np) then
@ -1591,11 +1592,11 @@ struct
match sk with match sk with
| ARRAY_SORT -> | ARRAY_SORT ->
if not (Z3native.is_as_array (gc x) n) then if not (Z3native.is_as_array (gc x) n) then
raise (Z3native.Exception "Argument was not an array constant") raise (Error "Argument was not an array constant")
else else
let fd = Z3native.get_as_array_func_decl (gc x) n in let fd = Z3native.get_as_array_func_decl (gc x) n in
get_func_interp x fd get_func_interp x fd
| _ -> raise (Z3native.Exception "Constant functions do not have a function interpretation; use ConstInterp"); | _ -> raise (Error "Constant functions do not have a function interpretation; use ConstInterp");
else else
let n = Z3native.model_get_func_interp (gc x) x f in let n = Z3native.model_get_func_interp (gc x) x f in
if (Z3native.is_null n) then None else Some n if (Z3native.is_null n) then None else Some n
@ -1780,7 +1781,7 @@ struct
else if (is_float x) then else if (is_float x) then
string_of_float (get_float x) string_of_float (get_float x)
else else
raise (Z3native.Exception "Unknown statistical entry type") raise (Error "Unknown statistical entry type")
let to_string (x:statistics_entry) = (get_key x) ^ ": " ^ (to_string_value x) let to_string (x:statistics_entry) = (get_key x) ^ ": " ^ (to_string_value x)
end end
@ -1833,7 +1834,7 @@ struct
let assert_and_track_l (x:solver) (cs:expr list) (ps:expr list) = let assert_and_track_l (x:solver) (cs:expr list) (ps:expr list) =
if ((List.length cs) != (List.length ps)) then if ((List.length cs) != (List.length ps)) then
raise (Z3native.Exception "Argument size mismatch") raise (Error "Argument size mismatch")
else else
let f a b = Z3native.solver_assert_and_track (gc x) x a b in let f a b = Z3native.solver_assert_and_track (gc x) x a b in
ignore (List.iter2 f cs ps) ignore (List.iter2 f cs ps)
@ -2029,7 +2030,7 @@ struct
let cdn = (List.length decl_names) in let cdn = (List.length decl_names) in
let cd = (List.length decls) in let cd = (List.length decls) in
if (csn != cs || cdn != cd) then if (csn != cs || cdn != cd) then
raise (Z3native.Exception "Argument size mismatch") raise (Error "Argument size mismatch")
else else
Z3native.parse_smtlib_string ctx str Z3native.parse_smtlib_string ctx str
cs cs
@ -2045,7 +2046,7 @@ struct
let cdn = (List.length decl_names) in let cdn = (List.length decl_names) in
let cd = (List.length decls) in let cd = (List.length decls) in
if (csn != cs || cdn != cd) then if (csn != cs || cdn != cd) then
raise (Z3native.Exception "Argument size mismatch") raise (Error "Argument size mismatch")
else else
Z3native.parse_smtlib_file ctx file_name Z3native.parse_smtlib_file ctx file_name
cs cs
@ -2089,7 +2090,7 @@ struct
let cdn = (List.length decl_names) in let cdn = (List.length decl_names) in
let cd = (List.length decls) in let cd = (List.length decls) in
if (csn != cs || cdn != cd) then if (csn != cs || cdn != cd) then
raise (Z3native.Exception "Argument size mismatch") raise (Error "Argument size mismatch")
else else
Z3native.parse_smtlib2_string ctx str Z3native.parse_smtlib2_string ctx str
cs cs
@ -2105,7 +2106,7 @@ struct
let cdn = (List.length decl_names) in let cdn = (List.length decl_names) in
let cd = (List.length decls) in let cd = (List.length decls) in
if (csn != cs || cdn != cd) then if (csn != cs || cdn != cd) then
raise (Z3native.Exception "Argument size mismatch") raise (Error "Argument size mismatch")
else else
Z3native.parse_smtlib2_string ctx file_name Z3native.parse_smtlib2_string ctx file_name
cs cs
@ -2147,7 +2148,7 @@ struct
let read_interpolation_problem (ctx:context) (filename:string) = let read_interpolation_problem (ctx:context) (filename:string) =
let (r, num, cnsts, parents, error, num_theory, theory) = (Z3native.read_interpolation_problem ctx filename) in let (r, num, cnsts, parents, error, num_theory, theory) = (Z3native.read_interpolation_problem ctx filename) in
match r with match r with
| 0 -> raise (Z3native.Exception "Interpolation problem could not be read.") | 0 -> raise (Error "Interpolation problem could not be read.")
| _ -> | _ ->
let f1 i = Array.get cnsts i in let f1 i = Array.get cnsts i in
let f2 i = Array.get parents i in let f2 i = Array.get parents i in
@ -2165,8 +2166,8 @@ struct
num_theory num_theory
(Array.of_list theory) in (Array.of_list theory) in
match (lbool_of_int r) with match (lbool_of_int r) with
| L_UNDEF -> raise (Z3native.Exception "Interpolant could not be verified.") | L_UNDEF -> raise (Error "Interpolant could not be verified.")
| L_FALSE -> raise (Z3native.Exception "Interpolant could not be verified.") | L_FALSE -> raise (Error "Interpolant could not be verified.")
| _ -> () | _ -> ()
let write_interpolation_problem (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (filename:string) (num_theory:int) (theory:Expr.expr list) = let write_interpolation_problem (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (filename:string) (num_theory:int) (theory:Expr.expr list) =

1
src/api/ml/z3native.ml.pre
View file

@ -103,5 +103,4 @@ external context_of_fixedpoint : fixedpoint -> context
external context_of_optimize : optimize -> context external context_of_optimize : optimize -> context
= "n_context_of_optimize" = "n_context_of_optimize"
exception Exception of string

106
src/api/ml/z3native_stubs.c.pre
View file

@ -42,14 +42,14 @@ extern "C" {
CAMLxparam3(X6,X7,X8) CAMLxparam3(X6,X7,X8)
#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \ #define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam4(X6,X7,X8,X9) CAMLxparam4(X6,X7,X8,X9)
#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \ #define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam2(X11,X12) CAMLxparam2(X11,X12)
#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \ #define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
CAMLparam5(X1,X2,X3,X4,X5); \ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam3(X11,X12,X13) CAMLxparam3(X11,X12,X13)
@ -64,8 +64,15 @@ static struct custom_operations default_custom_ops = {
}; };
#define MK_CTX_OF(X) \ #define MK_CTX_OF(X) \
Z3_context_plus * n_context_of_ ## X(Z3_ ## X ## _plus * p) { return p->cp; } CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \
CAMLparam1(v); \
CAMLlocal1(result); \
Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \
result = caml_alloc(sizeof(Z3_context_plus), 0); \
*(Z3_context_plus*)Data_custom_val(result) = *p->cp; \
CAMLreturn(result); \
}
// Context objects // Context objects
@ -90,7 +97,10 @@ Z3_context Z3_context_plus_raw(Z3_context_plus * cp) {
void Z3_context_finalize(value v) { void Z3_context_finalize(value v) {
Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v); Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v);
printf("ctx--; cnt=%lu\n", cp->ast_count); printf("ctx--; cnt=%lu\n", cp->ast_count);
Z3_del_context(cp->ctx); if (cp->ast_count == 0)
Z3_del_context(cp->ctx);
else
printf("Leaking the context; context_plus pointers now invalid. \n");
} }
static struct custom_operations Z3_context_plus_custom_ops = { static struct custom_operations Z3_context_plus_custom_ops = {
@ -112,7 +122,7 @@ typedef struct {
} Z3_symbol_plus; } Z3_symbol_plus;
Z3_symbol_plus Z3_symbol_plus_mk(Z3_context_plus * cp, Z3_symbol s) { Z3_symbol_plus Z3_symbol_plus_mk(Z3_context_plus * cp, Z3_symbol s) {
Z3_symbol_plus r; Z3_symbol_plus r;
r.cp = cp; r.cp = cp;
r.s = s; r.s = s;
return r; return r;
@ -145,7 +155,7 @@ typedef struct {
Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus * cp, Z3_ast a) { Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus * cp, Z3_ast a) {
Z3_ast_plus r; Z3_ast_plus r;
r.cp = cp; r.cp = cp;
r.a = a; r.a = a;
printf("++\n"); printf("++\n");
Z3_inc_ref(cp->ctx, a); Z3_inc_ref(cp->ctx, a);
cp->ast_count++; cp->ast_count++;
@ -207,6 +217,7 @@ static struct custom_operations Z3_ast_plus_custom_ops = {
MK_CTX_OF(ast) MK_CTX_OF(ast)
// Constructor objects // Constructor objects
typedef struct { typedef struct {
@ -300,39 +311,39 @@ static struct custom_operations Z3_rcf_num_plus_custom_ops = {
MK_CTX_OF(rcf_num) MK_CTX_OF(rcf_num)
#define MK_PLUS_OBJ(X) \ #define MK_PLUS_OBJ(X) \
typedef struct { \ typedef struct { \
Z3_context_plus * cp; \ Z3_context_plus * cp; \
Z3_ ## X p; \ Z3_ ## X p; \
} Z3_ ## X ## _plus; \ } Z3_ ## X ## _plus; \
\ \
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \ Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \
Z3_ ## X ## _plus r; \ Z3_ ## X ## _plus r; \
r.cp = cp; \ r.cp = cp; \
r.p = p; \ r.p = p; \
Z3_ ## X ## _inc_ref(cp->ctx, p); \ Z3_ ## X ## _inc_ref(cp->ctx, p); \
return r; \ return r; \
} \ } \
\ \
Z3_ ## X Z3_ ## X ## _plus_raw(Z3_ ## X ## _plus * pp) { \ Z3_ ## X Z3_ ## X ## _plus_raw(Z3_ ## X ## _plus * pp) { \
return pp->p; \ return pp->p; \
} \ } \
\ \
void Z3_ ## X ## _finalize(value v) { \ void Z3_ ## X ## _finalize(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \ Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \
} \ } \
\ \
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \ (char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \ Z3_ ## X ## _finalize, \
custom_compare_default, \ custom_compare_default, \
custom_hash_default, \ custom_hash_default, \
custom_serialize_default, \ custom_serialize_default, \
custom_deserialize_default, \ custom_deserialize_default, \
custom_compare_ext_default, \ custom_compare_ext_default, \
}; \ }; \
\ \
MK_CTX_OF(X) MK_CTX_OF(X)
MK_PLUS_OBJ(params) MK_PLUS_OBJ(params)
@ -363,10 +374,9 @@ CAMLprim DLL_PUBLIC value n_is_null(value p) {
CAMLprim DLL_PUBLIC value n_mk_null( void ) { CAMLprim DLL_PUBLIC value n_mk_null( void ) {
CAMLparam0(); CAMLparam0();
CAMLlocal1(result); CAMLlocal1(result);
void * z3_result = 0; result = caml_alloc(1, 0);
result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1); result = Val_int(0);
memcpy( Data_custom_val(result), &z3_result, sizeof(void*));
CAMLreturn (result); CAMLreturn (result);
} }