From b99fcb9c8abd343ca31fea8b2bb24e777e7ddce5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 14 Feb 2016 19:56:22 +0000 Subject: [PATCH] More new OCaml API --- examples/ml/ml_example.ml | 7 ++- scripts/mk_util.py | 25 +++++--- scripts/update_api.py | 88 +++++++++++++------------- src/api/ml/z3.ml | 87 +++++++++++++------------- src/api/ml/z3native.ml.pre | 1 - src/api/ml/z3native_stubs.c.pre | 106 +++++++++++++++++--------------- 6 files changed, 165 insertions(+), 149 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index 5b1c05069..bab0ba2fc 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -190,9 +190,10 @@ let basic_tests ( ctx : context ) = (* Error handling test. *) try ( 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" ) @@ -342,7 +343,7 @@ let _ = ); Printf.printf "Exiting.\n" ; exit 0 - ) with Z3native.Exception(msg) -> ( + ) with Error(msg) -> ( Printf.printf "Z3 EXCEPTION: %s\n" msg ; exit 1 ) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5df823ae2..4b724705c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1797,6 +1797,12 @@ class MLComponent(Component): if IS_WINDOWS: 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 mk_dir(os.path.join(BUILD_DIR, self.sub_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)' 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' % - (OCAMLC, OCAML_LIB, api_src, src_dir, stubso, stubsc)) + (OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc)) cmos = '' for m in self.modules: @@ -1831,9 +1837,9 @@ class MLComponent(Component): if (os.path.exists(existing_mli[3:])): out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli)) else: - out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLC, 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' % (OCAMLC, self.sub_dir, cmo, ml)) + 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' % (OCAMLCF, self.sub_dir, cmi, mli)) + out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmo, ml)) cmos = cmos + cmo + ' ' cmxs = '' @@ -1841,17 +1847,20 @@ class MLComponent(Component): ff = os.path.join(src_dir, m + '.ml') ft = os.path.join(self.sub_dir, m + '.cmx') 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 + OCAMLMKLIB = 'ocamlmklib' + if DEBUG_MODE: + OCAMLMKLIB += ' -g' z3mls = os.path.join(self.sub_dir, 'z3ml') 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('\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('\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('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) diff --git a/scripts/update_api.py b/scripts/update_api.py index b3c7d7072..05489c1d1 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -469,7 +469,7 @@ def mk_dotnet(): 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' ] def mk_dotnet_wrappers(): @@ -1228,7 +1228,7 @@ def ml_plus_ops_type(ts): if ml_has_plus_type(ts): return ml_plus_type(ts) + '_custom_ops' else: - return 'Z3_default_custom_ops' + return 'default_custom_ops' def ml_has_plus_type(ts): return ts != ml_plus_type(ts) @@ -1268,9 +1268,8 @@ def ml_set_wrap(t, d, n): elif t == STRING: return d + ' = caml_copy_string((const char*) ' + n + ');' else: - ts = type2str(t) - pts = ml_plus_type(ts) - return 'memcpy(Data_custom_val(' + d + '), &' + n + ', sizeof(' + pts + '));' + pts = ml_plus_type(type2str(t)) + return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';' def mk_z3native_ml(ml_dir): ml_nativef = os.path.join(ml_dir, 'z3native.ml') @@ -1332,13 +1331,8 @@ def mk_z3native_ml(ml_dir): i = i + 1 if len(ip) == 0: ml_native.write('()') - ml_native.write(' = \n') - ml_native.write(' ') - 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))) + ml_native.write(' = ') + ml_native.write('ML2C.n_%s' % (ml_method_name(name))) if len(ip) == 0: ml_native.write(' ()') first = True @@ -1347,16 +1341,6 @@ def mk_z3native_ml(ml_dir): if is_in_param(p): ml_native.write(' a%d' % i) 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.close() @@ -1427,11 +1411,13 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' unsigned _i;\n') # declare locals, preprocess arrays, strings, in/out arguments + have_context = False i = 0 for param in params: 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 _a0 = ctx_p->ctx;\n') + have_context = True else: k = param_kind(param) if k == OUT_ARRAY: @@ -1468,20 +1454,14 @@ def mk_z3native_stubs_c(ml_dir): # C interface i = i + 1 ml_wrapper.write(' ') - need_closing_paren = False if result != VOID: ts = type2str(result) + ml_wrapper.write('result = caml_alloc(%s, 0);\n' % ret_size) 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 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 + ml_wrapper.write(' %s z3rv_m = ' % ts) else: - ml_wrapper.write('result = caml_alloc(%s, 0);\n' % ret_size) ml_wrapper.write(' %s z3rv = ' % ts) + elif len(op) != 0: 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: ml_wrapper.write('_a%i' % i) i = i + 1 - ml_wrapper.write(')') - if need_closing_paren: - ml_wrapper.write(')'); - ml_wrapper.write(';\n') + ml_wrapper.write(');\n') + + if have_context and name not in Unwrapped: + 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 if len(op) > 0: i = 0 for p in params: + pt = param_type(p) + ts = type2str(pt) 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(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(p)) - if ml_has_plus_type(ts): - pts = ml_plus_type(ts) - 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)) + pts = ml_plus_type(ts) + pops = ml_plus_ops_type(ts) + ml_wrapper.write(' value t;\n') + 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\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: - ml_wrapper.write(' value t;\n') - 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(' %s\n' % ml_set_wrap(pt, 't', '_a%d[_i]' % i)) ml_wrapper.write(' Store_field(_a%s_val, _i, t);\n' % i) ml_wrapper.write(' }\n') 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): - pt = param_type(p) - ts = type2str(pt) if ml_has_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)) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 92155380c..b9af37faa 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -7,7 +7,8 @@ open Z3enums -exception Error = Z3native.Exception +exception Error of string +let _ = Callback.register_exception "Z3EXCEPTION" (Error "") (* Some helpers. *) let null = Z3native.mk_null() @@ -90,7 +91,7 @@ end module rec AST : sig type ast = Z3native.ast - val gc:ast -> context + val gc : ast -> context module ASTVector : sig type ast_vector = Z3native.ast_vector @@ -225,7 +226,7 @@ end and Sort : sig - type sort = Z3native.sort + type sort = AST.ast val gc : sort -> context val equal : sort -> sort -> bool val get_id : sort -> int @@ -296,7 +297,7 @@ val gc : func_decl -> context val get_parameters : func_decl -> Parameter.parameter list val apply : func_decl -> Expr.expr list -> Expr.expr end = struct - type func_decl = Z3native.func_decl + type func_decl = AST.ast let gc (x:func_decl) = Z3native.context_of_ast x module Parameter = @@ -323,37 +324,37 @@ end = struct let get_int (x:parameter) = match x with | P_Int(x) -> x - | _ -> raise (Z3native.Exception "parameter is not an int") + | _ -> raise (Error "parameter is not an int") let get_float (x:parameter) = match x with | P_Dbl(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a float") + | _ -> raise (Error "parameter is not a float") let get_symbol (x:parameter) = match x with | P_Sym(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a symbol") + | _ -> raise (Error "parameter is not a symbol") let get_sort (x:parameter) = match x with | P_Srt(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a sort") + | _ -> raise (Error "parameter is not a sort") let get_ast (x:parameter) = match x with | 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) = match x with | 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) = match x with | P_Rat(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a rational string") + | _ -> raise (Error "parameter is not a rational string") end let mk_func_decl (ctx:context) (name:Symbol.symbol) (domain:Sort.sort list) (range:Sort.sort) = @@ -469,7 +470,7 @@ end (** General expressions (terms) *) and Expr : sig - type expr = Z3native.ast + type expr = AST.ast val gc : expr -> context val ast_of_expr : expr -> AST.ast 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 compare : expr -> expr -> int end = struct - type expr = Z3native.ast + type expr = AST.ast let gc (e:expr) = Z3native.context_of_ast e let expr_of_ast (a:AST.ast) : expr = 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 - raise (Z3native.Exception "Invalid coercion") + raise (Error "Invalid coercion") else a @@ -540,13 +541,13 @@ end = struct let update (x:expr) (args:expr list) = 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 Z3native.update_term (gc x) x (List.length args) (Array.of_list args) let substitute (x:expr) (from:expr list) (to_:expr list) = if (List.length from) <> (List.length to_) then - raise (Z3native.Exception "Argument sizes do not match") + raise (Error "Argument sizes do not match") else Z3native.substitute (gc x) x (List.length from) (Array.of_list from) (Array.of_list to_) @@ -620,7 +621,7 @@ end module Quantifier = struct - type quantifier = Z3native.ast + type quantifier = AST.ast let gc (x:quantifier) = Z3native.context_of_ast x let expr_of_quantifier (q:quantifier) : Expr.expr = q @@ -628,7 +629,7 @@ struct let quantifier_of_expr (e:Expr.expr) : quantifier = let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (gc e) e)) in if (q != Z3enums.QUANTIFIER_AST) then - raise (Z3native.Exception "Invalid coercion") + raise (Error "Invalid coercion") else e @@ -650,7 +651,7 @@ struct let get_index (x:expr) = 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 Z3native.get_index_value (gc x) x @@ -687,13 +688,13 @@ struct let mk_pattern (ctx:context) (terms:expr list) = 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 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) = 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 Z3native.mk_quantifier ctx true (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) = 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 Z3native.mk_quantifier ctx false (match weight with | None -> 1 | Some(x) -> x) @@ -856,7 +857,7 @@ struct let get_size (x:Sort.sort) = let (r, v) = (Z3native.get_finite_domain_sort_size (Sort.gc x) x) in if r then v - else raise (Z3native.Exception "Conversion failed.") + else raise (Error "Conversion failed.") 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 n = (List.length field_names) in 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 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 let no = Z3native.mk_constructor ctx name recognizer @@ -1098,14 +1099,14 @@ struct let get_int (x:expr) = let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in if r then v - else raise (Z3native.Exception "Conversion failed.") + else raise (Error "Conversion failed.") let get_big_int (x:expr) = if (is_int_numeral x) then let s = (Z3native.get_numeral_string (Expr.gc x) x) in Big_int.big_int_of_string s 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 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 Ratio.ratio_of_string s 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 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_numeral_nd (ctx:context) (num:int) (den:int) = if (den == 0) then - raise (Z3native.Exception "Denominator is zero") + raise (Error "Denominator is zero") else Z3native.mk_real ctx num den @@ -1228,7 +1229,7 @@ struct let get_int (x:expr) = let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in 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 mk_const (ctx:context) (name:Symbol.symbol) (size:int) = Expr.mk_const ctx name (mk_sort ctx size) @@ -1490,7 +1491,7 @@ struct Z3native.apply_result_inc_ref (gc x) arn ; let sg = Z3native.apply_result_get_num_subgoals (gc x) arn in let res = if sg == 0 then - raise (Z3native.Exception "No subgoals") + raise (Error "No subgoals") else Z3native.apply_result_get_subgoal (gc x) arn 0 in Z3native.apply_result_dec_ref (gc x) arn ; @@ -1570,7 +1571,7 @@ struct let get_const_interp (x:model) (f:func_decl) = 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 - 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 let np = Z3native.model_get_const_interp (gc x) x f in if (Z3native.is_null np) then @@ -1591,11 +1592,11 @@ struct match sk with | ARRAY_SORT -> 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 let fd = Z3native.get_as_array_func_decl (gc x) n in 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 let n = Z3native.model_get_func_interp (gc x) x f in if (Z3native.is_null n) then None else Some n @@ -1780,7 +1781,7 @@ struct else if (is_float x) then string_of_float (get_float x) 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) end @@ -1833,7 +1834,7 @@ struct let assert_and_track_l (x:solver) (cs:expr list) (ps:expr list) = if ((List.length cs) != (List.length ps)) then - raise (Z3native.Exception "Argument size mismatch") + raise (Error "Argument size mismatch") else let f a b = Z3native.solver_assert_and_track (gc x) x a b in ignore (List.iter2 f cs ps) @@ -2029,7 +2030,7 @@ struct let cdn = (List.length decl_names) in let cd = (List.length decls) in if (csn != cs || cdn != cd) then - raise (Z3native.Exception "Argument size mismatch") + raise (Error "Argument size mismatch") else Z3native.parse_smtlib_string ctx str cs @@ -2045,7 +2046,7 @@ struct let cdn = (List.length decl_names) in let cd = (List.length decls) in if (csn != cs || cdn != cd) then - raise (Z3native.Exception "Argument size mismatch") + raise (Error "Argument size mismatch") else Z3native.parse_smtlib_file ctx file_name cs @@ -2089,7 +2090,7 @@ struct let cdn = (List.length decl_names) in let cd = (List.length decls) in if (csn != cs || cdn != cd) then - raise (Z3native.Exception "Argument size mismatch") + raise (Error "Argument size mismatch") else Z3native.parse_smtlib2_string ctx str cs @@ -2105,7 +2106,7 @@ struct let cdn = (List.length decl_names) in let cd = (List.length decls) in if (csn != cs || cdn != cd) then - raise (Z3native.Exception "Argument size mismatch") + raise (Error "Argument size mismatch") else Z3native.parse_smtlib2_string ctx file_name cs @@ -2147,7 +2148,7 @@ struct let read_interpolation_problem (ctx:context) (filename:string) = let (r, num, cnsts, parents, error, num_theory, theory) = (Z3native.read_interpolation_problem ctx filename) in 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 f2 i = Array.get parents i in @@ -2165,8 +2166,8 @@ struct num_theory (Array.of_list theory) in match (lbool_of_int r) with - | L_UNDEF -> raise (Z3native.Exception "Interpolant could not be verified.") - | L_FALSE -> raise (Z3native.Exception "Interpolant could not be verified.") + | L_UNDEF -> raise (Error "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) = diff --git a/src/api/ml/z3native.ml.pre b/src/api/ml/z3native.ml.pre index 60afeea84..28c6c7d91 100644 --- a/src/api/ml/z3native.ml.pre +++ b/src/api/ml/z3native.ml.pre @@ -103,5 +103,4 @@ external context_of_fixedpoint : fixedpoint -> context external context_of_optimize : optimize -> context = "n_context_of_optimize" -exception Exception of string diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index 1f9ea2aff..6755e9be9 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -42,14 +42,14 @@ extern "C" { CAMLxparam3(X6,X7,X8) #define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \ CAMLparam5(X1,X2,X3,X4,X5); \ - CAMLxparam4(X6,X7,X8,X9) -#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \ - CAMLparam5(X1,X2,X3,X4,X5); \ - CAMLxparam5(X6,X7,X8,X9,X10); \ + CAMLxparam4(X6,X7,X8,X9) +#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \ + CAMLparam5(X1,X2,X3,X4,X5); \ + CAMLxparam5(X6,X7,X8,X9,X10); \ CAMLxparam2(X11,X12) -#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \ - CAMLparam5(X1,X2,X3,X4,X5); \ - CAMLxparam5(X6,X7,X8,X9,X10); \ +#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \ + CAMLparam5(X1,X2,X3,X4,X5); \ + CAMLxparam5(X6,X7,X8,X9,X10); \ CAMLxparam3(X11,X12,X13) @@ -64,8 +64,15 @@ static struct custom_operations default_custom_ops = { }; -#define MK_CTX_OF(X) \ - Z3_context_plus * n_context_of_ ## X(Z3_ ## X ## _plus * p) { return p->cp; } +#define MK_CTX_OF(X) \ + 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 @@ -90,7 +97,10 @@ Z3_context Z3_context_plus_raw(Z3_context_plus * cp) { void Z3_context_finalize(value v) { Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v); 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 = { @@ -112,7 +122,7 @@ typedef struct { } Z3_symbol_plus; 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.s = s; 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 r; r.cp = cp; - r.a = a; + r.a = a; printf("++\n"); Z3_inc_ref(cp->ctx, a); cp->ast_count++; @@ -207,6 +217,7 @@ static struct custom_operations Z3_ast_plus_custom_ops = { MK_CTX_OF(ast) + // Constructor objects typedef struct { @@ -300,39 +311,39 @@ static struct custom_operations Z3_rcf_num_plus_custom_ops = { MK_CTX_OF(rcf_num) -#define MK_PLUS_OBJ(X) \ - typedef struct { \ - Z3_context_plus * cp; \ - Z3_ ## X p; \ - } Z3_ ## X ## _plus; \ - \ +#define MK_PLUS_OBJ(X) \ + typedef struct { \ + Z3_context_plus * cp; \ + Z3_ ## X p; \ + } Z3_ ## X ## _plus; \ + \ Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \ - Z3_ ## X ## _plus r; \ - r.cp = cp; \ - r.p = p; \ - Z3_ ## X ## _inc_ref(cp->ctx, p); \ - return r; \ - } \ - \ - Z3_ ## X Z3_ ## X ## _plus_raw(Z3_ ## X ## _plus * pp) { \ - return pp->p; \ - } \ - \ - void Z3_ ## X ## _finalize(value v) { \ - Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ - Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \ - } \ - \ - static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ - (char*) "Z3_" #X " ops", \ - Z3_ ## X ## _finalize, \ - custom_compare_default, \ - custom_hash_default, \ - custom_serialize_default, \ - custom_deserialize_default, \ - custom_compare_ext_default, \ - }; \ - \ + Z3_ ## X ## _plus r; \ + r.cp = cp; \ + r.p = p; \ + Z3_ ## X ## _inc_ref(cp->ctx, p); \ + return r; \ + } \ + \ + Z3_ ## X Z3_ ## X ## _plus_raw(Z3_ ## X ## _plus * pp) { \ + return pp->p; \ + } \ + \ + void Z3_ ## X ## _finalize(value v) { \ + Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ + Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \ + } \ + \ + static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ + (char*) "Z3_" #X " ops", \ + Z3_ ## X ## _finalize, \ + custom_compare_default, \ + custom_hash_default, \ + custom_serialize_default, \ + custom_deserialize_default, \ + custom_compare_ext_default, \ + }; \ + \ MK_CTX_OF(X) 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 ) { CAMLparam0(); - CAMLlocal1(result); - void * z3_result = 0; - result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1); - memcpy( Data_custom_val(result), &z3_result, sizeof(void*)); + CAMLlocal1(result); + result = caml_alloc(1, 0); + result = Val_int(0); CAMLreturn (result); }