From 71f991c5dff3ab224e2c87ae6a434dee07558fbf Mon Sep 17 00:00:00 2001 From: martin-neuhaeusser Date: Tue, 5 Apr 2016 12:51:03 +0200 Subject: [PATCH] Avoid using physical equality checks in OCaml bindings (z3.ml) This patch avoids the use of physical equality wherever possible and improves some details of the OCaml implementation. --- src/api/ml/z3.ml | 1256 +++++++++++++++---------------- src/api/ml/z3.mli | 1015 +++++++++++++------------ src/api/ml/z3native_stubs.c.pre | 92 ++- 3 files changed, 1192 insertions(+), 1171 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index e6e832572..c558038ca 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -14,9 +14,10 @@ type context = Z3native.context module Log = struct - let open_ filename = ((lbool_of_int (Z3native.open_log filename)) == L_TRUE) + let open_ filename = + lbool_of_int (Z3native.open_log filename) = L_TRUE let close = Z3native.close_log - let append s = Z3native.append_log s + let append = Z3native.append_log end @@ -29,29 +30,28 @@ struct let to_string = let (mj, mn, bld, rev) = Z3native.get_version () in string_of_int mj ^ "." ^ - string_of_int mn ^ "." ^ - string_of_int bld ^ "." ^ - string_of_int rev + string_of_int mn ^ "." ^ + string_of_int bld ^ "." ^ + string_of_int rev end - -let mk_list (f:int -> 'a) (n:int) = - let rec mk_list' (f:int -> 'a) (i:int) (n:int) (tail:'a list):'a list = - if (i >= n) then - tail +let mk_list f n = + let rec mk_list' i accu = + if i >= n then + List.rev accu else - (f i) :: (mk_list' f (i+1) n tail) + mk_list' (i + 1) ((f i)::accu) in - mk_list' f 0 n [] + mk_list' 0 [] let mk_context (settings:(string * string) list) = let cfg = Z3native.mk_config () in let f e = Z3native.set_param_value cfg (fst e) (snd e) in - (List.iter f settings) ; + (List.iter f settings); let res = Z3native.mk_context_rc cfg in - Z3native.del_config(cfg) ; - Z3native.set_ast_print_mode res (Z3enums.int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ; - Z3native.set_internal_error_handler res ; + Z3native.del_config(cfg); + Z3native.set_ast_print_mode res (Z3enums.int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT); + Z3native.set_internal_error_handler res; res @@ -59,26 +59,22 @@ let mk_context (settings:(string * string) list) = module Symbol = struct type symbol = Z3native.symbol - let gc (o:symbol) = (Z3native.context_of_symbol o) + let gc = Z3native.context_of_symbol - let kind (o:symbol) = (symbol_kind_of_int (Z3native.get_symbol_kind (gc o) o)) - let is_int_symbol (o:symbol) = (kind o) == INT_SYMBOL - let is_string_symbol (o:symbol) = (kind o) == STRING_SYMBOL - let get_int (o:symbol) = (Z3native.get_symbol_int (gc o) o) - let get_string (o:symbol) = (Z3native.get_symbol_string (gc o) o) + let kind (o:symbol) = symbol_kind_of_int (Z3native.get_symbol_kind (gc o) o) + let is_int_symbol (o:symbol) = (kind o) = INT_SYMBOL + let is_string_symbol (o:symbol) = (kind o) = STRING_SYMBOL + let get_int (o:symbol) = Z3native.get_symbol_int (gc o) o + let get_string (o:symbol) = Z3native.get_symbol_string (gc o) o let to_string (o:symbol) = - match (kind o) with - | INT_SYMBOL -> (string_of_int (Z3native.get_symbol_int (gc o) o)) - | STRING_SYMBOL -> (Z3native.get_symbol_string (gc o) o) + match kind o with + | INT_SYMBOL -> string_of_int (Z3native.get_symbol_int (gc o) o) + | STRING_SYMBOL -> Z3native.get_symbol_string (gc o) o - let mk_int (ctx:context) (i:int) = (Z3native.mk_int_symbol ctx i) - let mk_string (ctx:context) (s:string) = (Z3native.mk_string_symbol ctx s) - - let mk_ints (ctx:context) (names:int list) = - List.map (fun x -> mk_int ctx x) names - - let mk_strings (ctx:context) (names:string list) = - List.map (fun x -> mk_string ctx x) names + let mk_int = Z3native.mk_int_symbol + let mk_string = Z3native.mk_string_symbol + let mk_ints (ctx:context) (names:int list) = List.map (mk_int ctx) names + let mk_strings (ctx:context) (names:string list) = List.map (mk_string ctx) names end @@ -129,14 +125,14 @@ sig val translate : ast -> context -> ast end = struct type ast = Z3native.ast - let gc (x:ast) = Z3native.context_of_ast x + let gc = Z3native.context_of_ast module ASTVector = struct type ast_vector = Z3native.ast_vector - let gc (x:ast_vector) = Z3native.context_of_ast_vector x + let gc = Z3native.context_of_ast_vector - let mk_ast_vector (ctx:context) = Z3native.mk_ast_vector ctx + let mk_ast_vector = Z3native.mk_ast_vector let get_size (x:ast_vector) = Z3native.ast_vector_size (gc x) x let get (x:ast_vector) (i:int) = Z3native.ast_vector_get (gc x) x i let set (x:ast_vector) (i:int) (value:ast) = Z3native.ast_vector_set (gc x) x i value @@ -145,12 +141,12 @@ end = struct let translate (x:ast_vector) (to_ctx:context) = Z3native.ast_vector_translate (gc x) x to_ctx let to_list (x:ast_vector) = - let xs = (get_size x) in - let f i = (get x i) in + let xs = get_size x in + let f i = get x i in mk_list f xs let to_expr_list (x:ast_vector) = - let xs = (get_size x) in + let xs = get_size x in let f i = get x i in mk_list f xs @@ -160,9 +156,9 @@ end = struct module ASTMap = struct type ast_map = Z3native.ast_map - let gc (x:ast_map) = Z3native.context_of_ast_map x + let gc = Z3native.context_of_ast_map - let mk_ast_map (ctx:context) = Z3native.mk_ast_map ctx + let mk_ast_map = Z3native.mk_ast_map let contains (x:ast_map) (key:ast) = Z3native.ast_map_contains (gc x) x key let find (x:ast_map) (key:ast) = Z3native.ast_map_find (gc x) x key let insert (x:ast_map) (key:ast) (value:ast) = Z3native.ast_map_insert (gc x) x key value @@ -171,48 +167,41 @@ end = struct let get_size (x:ast_map) = Z3native.ast_map_size (gc x) x let get_keys (x:ast_map) = - let av = (Z3native.ast_map_keys (gc x) x) in - (ASTVector.to_list av) + let av = Z3native.ast_map_keys (gc x) x in + ASTVector.to_list av let to_string (x:ast_map) = Z3native.ast_map_to_string (gc x) x end let hash (x:ast) = Z3native.get_ast_hash (gc x) x let get_id (x:ast) = Z3native.get_ast_id (gc x) x - let get_ast_kind (x:ast) = (ast_kind_of_int (Z3native.get_ast_kind (gc x) x)) + let get_ast_kind (x:ast) = ast_kind_of_int (Z3native.get_ast_kind (gc x) x) let is_expr (x:ast) = - match get_ast_kind (x:ast) with + match get_ast_kind x with | APP_AST | NUMERAL_AST | QUANTIFIER_AST | VAR_AST -> true | _ -> false - let is_app (x:ast) = (get_ast_kind x) == APP_AST - let is_var (x:ast) = (get_ast_kind x) == VAR_AST - let is_quantifier (x:ast) = (get_ast_kind x) == QUANTIFIER_AST - let is_sort (x:ast) = (get_ast_kind x) == SORT_AST - let is_func_decl (x:ast) = (get_ast_kind x) == FUNC_DECL_AST + let is_app (x:ast) = get_ast_kind x = APP_AST + let is_var (x:ast) = get_ast_kind x = VAR_AST + let is_quantifier (x:ast) = get_ast_kind x = QUANTIFIER_AST + let is_sort (x:ast) = get_ast_kind x = SORT_AST + let is_func_decl (x:ast) = get_ast_kind x = FUNC_DECL_AST let to_string (x:ast) = Z3native.ast_to_string (gc x) x let to_sexpr (x:ast) = Z3native.ast_to_string (gc x) x + (* The built-in equality uses the custom operations of the C layer *) + let equal = (=) - let equal (a:ast) (b:ast) = - (a == b) || - (if (gc a) != (gc b) then - false - else - Z3native.is_eq_ast (gc a) a b) - - let compare a b = - if (get_id a) < (get_id b) then -1 else - if (get_id a) > (get_id b) then 1 else - 0 + (* The standard comparison uses the custom operations of the C layer *) + let compare = Pervasives.compare let translate (x:ast) (to_ctx:context) = - if (gc x) == to_ctx then + if gc x = to_ctx then x else Z3native.translate (gc x) x to_ctx @@ -231,31 +220,26 @@ sig val mk_uninterpreted_s : context -> string -> sort end = struct type sort = Z3native.sort - let gc (x:sort) = Z3native.context_of_ast x + let gc = Z3native.context_of_ast - let equal:sort -> sort -> bool = fun a b -> - (a == b) || - (if (gc a) != (gc b) then - false - else - Z3native.is_eq_sort (gc a) a b) + let equal a b = (a = b) || (gc a = gc b && Z3native.is_eq_sort (gc a) a b) let get_id (x:sort) = Z3native.get_sort_id (gc x) x let get_sort_kind (x:sort) = sort_kind_of_int (Z3native.get_sort_kind (gc x) x) let get_name (x:sort) = Z3native.get_sort_name (gc x) x let to_string (x:sort) = Z3native.sort_to_string (gc x) x - let mk_uninterpreted (ctx:context) (s:Symbol.symbol) = Z3native.mk_uninterpreted_sort ctx s + let mk_uninterpreted = Z3native.mk_uninterpreted_sort let mk_uninterpreted_s (ctx:context) (s:string) = mk_uninterpreted ctx (Symbol.mk_string ctx s) end and FuncDecl : sig type func_decl = Z3native.func_decl -val gc : func_decl -> context + val gc : func_decl -> context module Parameter : sig type parameter = - P_Int of int + P_Int of int | P_Dbl of float | P_Sym of Symbol.symbol | P_Srt of Sort.sort @@ -292,7 +276,7 @@ val gc : func_decl -> context val apply : func_decl -> Expr.expr list -> Expr.expr end = struct type func_decl = AST.ast - let gc (x:func_decl) = Z3native.context_of_ast x + let gc = Z3native.context_of_ast module Parameter = struct @@ -305,50 +289,42 @@ end = struct | P_Fdl of func_decl | P_Rat of string - let get_kind (x:parameter) = - (match x with - | P_Int(_) -> PARAMETER_INT - | P_Dbl(_) -> PARAMETER_DOUBLE - | P_Sym(_) -> PARAMETER_SYMBOL - | P_Srt(_) -> PARAMETER_SORT - | P_Ast(_) -> PARAMETER_AST - | P_Fdl(_) -> PARAMETER_FUNC_DECL - | P_Rat(_) -> PARAMETER_RATIONAL) + let get_kind = function + | P_Int _ -> PARAMETER_INT + | P_Dbl _ -> PARAMETER_DOUBLE + | P_Sym _ -> PARAMETER_SYMBOL + | P_Srt _ -> PARAMETER_SORT + | P_Ast _ -> PARAMETER_AST + | P_Fdl _ -> PARAMETER_FUNC_DECL + | P_Rat _ -> PARAMETER_RATIONAL - let get_int (x:parameter) = - match x with - | P_Int(x) -> x - | _ -> raise (Error "parameter is not an int") + let get_int = function + | P_Int x -> x + | _ -> raise (Error "parameter is not an int") - let get_float (x:parameter) = - match x with - | P_Dbl(x) -> x - | _ -> raise (Error "parameter is not a float") + let get_float = function + | P_Dbl x -> x + | _ -> raise (Error "parameter is not a float") - let get_symbol (x:parameter) = - match x with - | P_Sym(x) -> x - | _ -> raise (Error "parameter is not a symbol") + let get_symbol = function + | P_Sym x -> x + | _ -> raise (Error "parameter is not a symbol") - let get_sort (x:parameter) = - match x with - | P_Srt(x) -> x - | _ -> raise (Error "parameter is not a sort") + let get_sort = function + | P_Srt x -> x + | _ -> raise (Error "parameter is not a sort") - let get_ast (x:parameter) = - match x with - | P_Ast(x) -> x - | _ -> raise (Error "parameter is not an ast") + let get_ast = function + | P_Ast x -> x + | _ -> raise (Error "parameter is not an ast") - let get_func_decl (x:parameter) = - match x with - | P_Fdl(x) -> x - | _ -> raise (Error "parameter is not a func_decl") + let get_func_decl = function + | P_Fdl x -> x + | _ -> raise (Error "parameter is not a func_decl") - let get_rational (x:parameter) = - match x with - | P_Rat(x) -> x - | _ -> raise (Error "parameter is not a rational string") + let get_rational = function + | P_Rat x -> x + | _ -> 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) = @@ -369,12 +345,7 @@ end = struct let mk_fresh_const_decl (ctx:context) (prefix:string) (range:Sort.sort) = Z3native.mk_fresh_func_decl ctx prefix 0 [||] range - let equal (a:func_decl) (b:func_decl) = - (a == b) || - (if (gc a) != (gc b) then - false - else - Z3native.is_eq_func_decl (gc a) a b) + let equal a b = (a = b) || (gc a = gc b && Z3native.is_eq_func_decl (gc a) a b) let to_string (x:func_decl) = Z3native.func_decl_to_string (gc x) x let get_id (x:func_decl) = Z3native.get_func_decl_id (gc x) x @@ -382,7 +353,7 @@ end = struct let get_domain_size (x:func_decl) = Z3native.get_domain_size (gc x) x let get_domain (x:func_decl) = - let n = (get_domain_size x) in + let n = get_domain_size x in let f i = Z3native.get_domain (gc x) x i in mk_list f n @@ -392,15 +363,17 @@ end = struct let get_num_parameters (x:func_decl) = Z3native.get_decl_num_parameters (gc x) x let get_parameters (x:func_decl) = - let n = (get_num_parameters x) in - let f i = (match (parameter_kind_of_int (Z3native.get_decl_parameter_kind (gc x) x i)) with + let n = get_num_parameters x in + let f i = + match parameter_kind_of_int (Z3native.get_decl_parameter_kind (gc x) x i) with | PARAMETER_INT -> Parameter.P_Int (Z3native.get_decl_int_parameter (gc x) x i) | PARAMETER_DOUBLE -> Parameter.P_Dbl (Z3native.get_decl_double_parameter (gc x) x i) | PARAMETER_SYMBOL-> Parameter.P_Sym (Z3native.get_decl_symbol_parameter (gc x) x i) | PARAMETER_SORT -> Parameter.P_Srt (Z3native.get_decl_sort_parameter (gc x) x i) | PARAMETER_AST -> Parameter.P_Ast (Z3native.get_decl_ast_parameter (gc x) x i) | PARAMETER_FUNC_DECL -> Parameter.P_Fdl (Z3native.get_decl_func_decl_parameter (gc x) x i) - | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gc x) x i)) in + | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gc x) x i) + in mk_list f n let apply (x:func_decl) (args:Expr.expr list) = Expr.expr_of_func_app (gc x) x args @@ -430,12 +403,12 @@ sig val set_print_mode : context -> Z3enums.ast_print_mode -> unit end = struct type params = Z3native.params - let gc (x:params) = Z3native.context_of_params x + let gc = Z3native.context_of_params module ParamDescrs = struct type param_descrs = Z3native.param_descrs - let gc (x:param_descrs) = Z3native.context_of_param_descrs x + let gc = Z3native.context_of_param_descrs let validate (x:param_descrs) (p:params) = Z3native.params_validate (gc x) p x let get_kind (x:param_descrs) (name:Symbol.symbol) = param_kind_of_int (Z3native.param_descrs_get_kind (gc x) x name) @@ -499,19 +472,20 @@ sig val compare : expr -> expr -> int end = struct type expr = AST.ast - let gc (e:expr) = Z3native.context_of_ast e + let gc = Z3native.context_of_ast - let expr_of_ast (a:AST.ast) : expr = + let expr_of_ast a = 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 (Error "Invalid coercion") else a - let ast_of_expr (e:expr) : AST.ast = e + let ast_of_expr e = e - let expr_of_func_app:context -> FuncDecl.func_decl -> expr list -> expr = - fun ctx f args -> (Z3native.mk_app ctx f (List.length args) (Array.of_list args)) + let expr_of_func_app ctx f args = + let arg_array = Array.of_list args in + Z3native.mk_app ctx f (Array.length arg_array) arg_array let apply1 ctx f t = f ctx t let apply2 ctx f t1 t2 = f ctx t1 t2 @@ -523,32 +497,36 @@ end = struct | None -> Z3native.simplify (gc x) x | Some pp -> Z3native.simplify_ex (gc x) x pp - let get_simplify_help (ctx:context) = Z3native.simplify_get_help ctx - let get_simplify_parameter_descrs (ctx:context) = Z3native.simplify_get_param_descrs ctx + let get_simplify_help = Z3native.simplify_get_help + let get_simplify_parameter_descrs = Z3native.simplify_get_param_descrs let get_func_decl (x:expr) = Z3native.get_app_decl (gc x) x let get_num_args (x:expr) = Z3native.get_app_num_args (gc x) x let get_args (x:expr) = - let n = (get_num_args x) in + let n = get_num_args x in let f i = Z3native.get_app_arg (gc x) x i in mk_list f n 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 (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 + let from_array = Array.of_list from in + let to_array = Array.of_list to_ in + if Array.length from_array <> Array.length to_array then raise (Error "Argument sizes do not match") else - Z3native.substitute (gc x) x (List.length from) (Array.of_list from) (Array.of_list to_) + Z3native.substitute (gc x) x (Array.length from_array) from_array to_array - let substitute_one (x:expr) (from:expr) (to_:expr) = substitute (x:expr) [ from ] [ to_ ] - let substitute_vars (x:expr) (to_:expr list) = Z3native.substitute_vars (gc x) x (List.length to_) (Array.of_list to_) + let substitute_one x from to_ = substitute x [ from ] [ to_ ] + let substitute_vars x to_ = + let to_array = Array.of_list to_ in + Z3native.substitute_vars (gc x) x (Array.length to_array) to_array let translate (x:expr) to_ctx = - if (gc x) == to_ctx then + if gc x = to_ctx then x else Z3native.translate (gc x) x to_ctx @@ -558,9 +536,9 @@ end = struct let is_well_sorted (x:expr) = Z3native.is_well_sorted (gc x) x let get_sort (x:expr) = Z3native.get_sort (gc x) x let is_const (x:expr) = - (AST.is_app x) && - (get_num_args x) == 0 && - (FuncDecl.get_domain_size (get_func_decl x)) == 0 + AST.is_app x + && get_num_args x = 0 + && FuncDecl.get_domain_size (get_func_decl x) = 0 let mk_const (ctx:context) (name:Symbol.symbol) (range:Sort.sort) = Z3native.mk_const ctx name range let mk_const_s (ctx:context) (name:string) (range:Sort.sort) = mk_const ctx (Symbol.mk_string ctx name) range @@ -578,11 +556,11 @@ open Expr module Boolean = struct - let mk_sort (ctx:context) = Z3native.mk_bool_sort ctx + let mk_sort = Z3native.mk_bool_sort let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name) - let mk_true (ctx:context) = Z3native.mk_true ctx - let mk_false (ctx:context) = Z3native.mk_false ctx + let mk_true = Z3native.mk_true + let mk_false = Z3native.mk_false let mk_val (ctx:context) (value:bool) = if value then mk_true ctx else mk_false ctx let mk_not (ctx:context) (a:expr) = apply1 ctx Z3native.mk_not a let mk_ite (ctx:context) (t1:expr) (t2:expr) (t3:expr) = apply3 ctx Z3native.mk_ite t1 t2 t3 @@ -595,33 +573,34 @@ struct let mk_distinct (ctx:context) (args:expr list) = Z3native.mk_distinct ctx (List.length args) (Array.of_list args) let get_bool_value (x:expr) = lbool_of_int (Z3native.get_bool_value (gc x) x) - let is_bool (x:expr) = - (AST.is_expr x) && (Z3native.is_eq_sort (gc x) (Z3native.mk_bool_sort (gc x)) (Z3native.get_sort (gc x) x)) + let is_bool x = + AST.is_expr x + && Z3native.is_eq_sort (gc x) (Z3native.mk_bool_sort (gc x)) (Z3native.get_sort (gc x) x) - let is_true (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_TRUE) - let is_false (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_FALSE) - let is_eq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_EQ) - let is_distinct (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_DISTINCT) - let is_ite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_ITE) - let is_and (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_AND) - let is_or (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_OR) - let is_iff (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_IFF) - let is_xor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR) - let is_not (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_NOT) - let is_implies (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES) + let is_true x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_TRUE + let is_false x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_FALSE + let is_eq x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_EQ + let is_distinct x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_DISTINCT + let is_ite x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_ITE + let is_and x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_AND + let is_or x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_OR + let is_iff x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_IFF + let is_xor x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_XOR + let is_not x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_NOT + let is_implies x = AST.is_app x && FuncDecl.get_decl_kind (get_func_decl x) = OP_IMPLIES end module Quantifier = struct type quantifier = AST.ast - let gc (x:quantifier) = Z3native.context_of_ast x + let gc = Z3native.context_of_ast - let expr_of_quantifier (q:quantifier) : Expr.expr = q + let expr_of_quantifier q = q - 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 + let quantifier_of_expr e = + let q = Z3enums.ast_kind_of_int (Z3native.get_ast_kind (gc e) e) in + if q <> Z3enums.QUANTIFIER_AST then raise (Error "Invalid coercion") else e @@ -630,7 +609,7 @@ struct module Pattern = struct type pattern = Z3native.pattern - let gc (x:pattern) = Z3native.context_of_ast x + let gc = Z3native.context_of_ast let get_num_terms (x:pattern) = Z3native.get_pattern_num_terms (gc x) x @@ -653,26 +632,26 @@ struct let get_weight (x:quantifier) = Z3native.get_quantifier_weight (gc x) x let get_num_patterns (x:quantifier) = Z3native.get_quantifier_num_patterns (gc x) x let get_patterns (x:quantifier) = - let n = (get_num_patterns x) in + let n = get_num_patterns x in let f i = Z3native.get_quantifier_pattern_ast (gc x) x i in mk_list f n let get_num_no_patterns (x:quantifier) = Z3native.get_quantifier_num_no_patterns (gc x) x let get_no_patterns (x:quantifier) = - let n = (get_num_patterns x) in + let n = get_num_patterns x in let f i = Z3native.get_quantifier_no_pattern_ast (gc x) x i in mk_list f n let get_num_bound (x:quantifier) = Z3native.get_quantifier_num_bound (gc x) x let get_bound_variable_names (x:quantifier) = - let n = (get_num_bound x) in + let n = get_num_bound x in let f i = Z3native.get_quantifier_bound_name (gc x) x i in mk_list f n let get_bound_variable_sorts (x:quantifier) = - let n = (get_num_bound x) in + let n = get_num_bound x in let f i = Z3native.get_quantifier_bound_sort (gc x) x i in mk_list f n @@ -680,86 +659,86 @@ struct let mk_bound (ctx:context) (index:int) (ty:Sort.sort) = Z3native.mk_bound ctx index ty let mk_pattern (ctx:context) (terms:expr list) = - if (List.length terms) == 0 then + if List.length terms = 0 then 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 + if (List.length sorts) <> (List.length names) then 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 - (match weight with | None -> 1 | Some(x) -> x) - (List.length patterns) (Array.of_list patterns) - (List.length sorts) (Array.of_list sorts) - (Array.of_list names) - body + (match weight with | None -> 1 | Some(x) -> x) + (List.length patterns) (Array.of_list patterns) + (List.length sorts) (Array.of_list sorts) + (Array.of_list names) + body else Z3native.mk_quantifier_ex ctx true - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (List.length patterns) (Array.of_list patterns) - (List.length nopatterns) (Array.of_list nopatterns) - (List.length sorts) (Array.of_list sorts) - (Array.of_list names) - body + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (List.length patterns) (Array.of_list patterns) + (List.length nopatterns) (Array.of_list nopatterns) + (List.length sorts) (Array.of_list sorts) + (Array.of_list names) + body let mk_forall_const (ctx:context) (bound_constants:expr 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 nopatterns) == 0 && quantifier_id == None && skolem_id == None) then + if ((List.length nopatterns) = 0 && quantifier_id = None && skolem_id = None) then Z3native.mk_quantifier_const ctx true - (match weight with | None -> 1 | Some(x) -> x) - (List.length bound_constants) (Array.of_list bound_constants) - (List.length patterns) (Array.of_list patterns) - body + (match weight with | None -> 1 | Some(x) -> x) + (List.length bound_constants) (Array.of_list bound_constants) + (List.length patterns) (Array.of_list patterns) + body else Z3native.mk_quantifier_const_ex ctx true - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (List.length bound_constants) (Array.of_list bound_constants) - (List.length patterns) (Array.of_list patterns) - (List.length nopatterns) (Array.of_list nopatterns) - body + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (List.length bound_constants) (Array.of_list bound_constants) + (List.length patterns) (Array.of_list patterns) + (List.length nopatterns) (Array.of_list nopatterns) + body 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 (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 - (match weight with | None -> 1 | Some(x) -> x) - (List.length patterns) (Array.of_list patterns) - (List.length sorts) (Array.of_list sorts) - (Array.of_list names) - body + (match weight with | None -> 1 | Some(x) -> x) + (List.length patterns) (Array.of_list patterns) + (List.length sorts) (Array.of_list sorts) + (Array.of_list names) + body else Z3native.mk_quantifier_ex ctx false - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (List.length patterns) (Array.of_list patterns) - (List.length nopatterns) (Array.of_list nopatterns) - (List.length sorts) (Array.of_list sorts) - (Array.of_list names) - body + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (List.length patterns) (Array.of_list patterns) + (List.length nopatterns) (Array.of_list nopatterns) + (List.length sorts) (Array.of_list sorts) + (Array.of_list names) + body let mk_exists_const (ctx:context) (bound_constants:expr 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 nopatterns) == 0 && quantifier_id == None && skolem_id == None) then + if ((List.length nopatterns) = 0 && quantifier_id = None && skolem_id = None) then Z3native.mk_quantifier_const ctx false - (match weight with | None -> 1 | Some(x) -> x) - (List.length bound_constants) (Array.of_list bound_constants) - (List.length patterns) (Array.of_list patterns) - body -else - Z3native.mk_quantifier_const_ex ctx false - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) - (List.length bound_constants) (Array.of_list bound_constants) - (List.length patterns) (Array.of_list patterns) - (List.length nopatterns) (Array.of_list nopatterns) - body + (match weight with | None -> 1 | Some(x) -> x) + (List.length bound_constants) (Array.of_list bound_constants) + (List.length patterns) (Array.of_list patterns) + body + else + Z3native.mk_quantifier_const_ex ctx false + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some(x) -> x) + (List.length bound_constants) (Array.of_list bound_constants) + (List.length patterns) (Array.of_list patterns) + (List.length nopatterns) (Array.of_list nopatterns) + body let mk_quantifier (ctx:context) (universal:bool) (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 (universal) then @@ -780,16 +759,16 @@ end module Z3Array = struct let mk_sort (ctx:context) (domain:Sort.sort) (range:Sort.sort) = Z3native.mk_array_sort ctx domain range - let is_store (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) - let is_select (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SELECT) - let is_constant_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONST_ARRAY) - let is_default_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_DEFAULT) - let is_array_map (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_MAP) - let is_as_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) + let is_store (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_STORE) + let is_select (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SELECT) + let is_constant_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_CONST_ARRAY) + let is_default_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ARRAY_DEFAULT) + let is_array_map (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ARRAY_MAP) + let is_as_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_AS_ARRAY) let is_array (x:expr) = (Z3native.is_app (Expr.gc x) x) && - ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == ARRAY_SORT) + ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = ARRAY_SORT) let get_domain (x:Sort.sort) = Z3native.get_array_sort_domain (Sort.gc x) x let get_range (x:Sort.sort) = Z3native.get_array_sort_range (Sort.gc x) x @@ -813,11 +792,11 @@ module Set = struct let mk_sort (ctx:context) (ty:Sort.sort) = Z3native.mk_set_sort ctx ty - let is_union (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) - let is_intersect (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) - let is_difference (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) - let is_complement (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) - let is_subset (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) + let is_union (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SET_UNION) + let is_intersect (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SET_INTERSECT) + let is_difference (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SET_DIFFERENCE) + let is_complement (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SET_COMPLEMENT) + let is_subset (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SET_SUBSET) let mk_empty (ctx:context) (domain:Sort.sort) = Z3native.mk_empty_set ctx domain let mk_full (ctx:context) (domain:Sort.sort) = Z3native.mk_full_set ctx domain @@ -843,9 +822,9 @@ struct let is_finite_domain (x:expr) = let nc = (Expr.gc x) in (Z3native.is_app nc x) && - (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc x)) == FINITE_DOMAIN_SORT) + (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc x)) = FINITE_DOMAIN_SORT) - let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT) + let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FD_LT) let get_size (x:Sort.sort) = let (r, v) = (Z3native.get_finite_domain_sort_size (Sort.gc x) x) in @@ -859,21 +838,21 @@ struct let is_relation (x:expr) = let nc = (Expr.gc x) in ((Z3native.is_app nc x) && - (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc x)) == RELATION_SORT)) + (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc x)) = RELATION_SORT)) - let is_store (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_STORE) - let is_empty (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_EMPTY) - let is_is_empty (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_IS_EMPTY) - let is_join (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_JOIN) - let is_union (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_UNION) - let is_widen (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_WIDEN) - let is_project (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_PROJECT) - let is_filter (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_FILTER) - let is_negation_filter (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_NEGATION_FILTER) - let is_rename (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_RENAME) - let is_complement (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_COMPLEMENT) - let is_select (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT) - let is_clone (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_CLONE) + let is_store (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_STORE) + let is_empty (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_EMPTY) + let is_is_empty (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_IS_EMPTY) + let is_join (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_JOIN) + let is_union (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_UNION) + let is_widen (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_WIDEN) + let is_project (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_PROJECT) + let is_filter (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_FILTER) + let is_negation_filter (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_NEGATION_FILTER) + let is_rename (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_RENAME) + let is_complement (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_COMPLEMENT) + let is_select (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_SELECT) + let is_clone (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_RA_CLONE) let get_arity (x:Sort.sort) = Z3native.get_relation_arity (Sort.gc x) x @@ -891,30 +870,30 @@ struct type constructor = Z3native.constructor module FieldNumTable = Hashtbl.Make(struct - type t = AST.ast - let equal x y = AST.compare x y = 0 - let hash = AST.hash - end) + type t = AST.ast + let equal x y = AST.compare x y = 0 + let hash = AST.hash + end) let _field_nums = FieldNumTable.create 0 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 + if n <> (List.length sorts) then raise (Error "Number of field names does not match number of sorts") else - if n != (List.length sort_refs) then - raise (Error "Number of field names does not match number of sort refs") - else - let no = Z3native.mk_constructor ctx name - recognizer - n - (Array.of_list field_names) - (let f x = match x with None -> Z3native.mk_null_ast ctx | Some s -> s in - Array.of_list (List.map f sorts)) - (Array.of_list sort_refs) in - FieldNumTable.add _field_nums no n ; - no + if n <> (List.length sort_refs) then + raise (Error "Number of field names does not match number of sort refs") + else + let no = Z3native.mk_constructor ctx name + recognizer + n + (Array.of_list field_names) + (let f x = match x with None -> Z3native.mk_null_ast ctx | Some s -> s in + Array.of_list (List.map f sorts)) + (Array.of_list sort_refs) in + FieldNumTable.add _field_nums no n; + no let get_num_fields (x:constructor) = FieldNumTable.find _field_nums x @@ -1055,25 +1034,25 @@ end module Arithmetic = struct let is_int (x:expr) = - ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == INT_SORT) + ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = INT_SORT) - let is_arithmetic_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM) - let is_le (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE) - let is_ge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE) - let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LT) - let is_gt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GT) - let is_add (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ADD) - let is_sub (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SUB) - let is_uminus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UMINUS) - let is_mul (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MUL) - let is_div (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_DIV) - let is_idiv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IDIV) - let is_remainder (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REM) - let is_modulus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD) - let is_int2real (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL) - let is_real2int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT) - let is_real_is_int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT) - let is_real (x:expr) = ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == REAL_SORT) + let is_arithmetic_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ANUM) + let is_le (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_LE) + let is_ge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_GE) + let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_LT) + let is_gt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_GT) + let is_add (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ADD) + let is_sub (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SUB) + let is_uminus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_UMINUS) + let is_mul (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_MUL) + let is_div (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_DIV) + let is_idiv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_IDIV) + let is_remainder (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_REM) + let is_modulus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_MOD) + let is_int2real (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_TO_REAL) + let is_real2int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_TO_INT) + let is_real_is_int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_IS_INT) + let is_real (x:expr) = ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = REAL_SORT) let is_int_numeral (x:expr) = (Expr.is_numeral x) && (is_int x) let is_rat_numeral (x:expr) = (Expr.is_numeral x) && (is_real x) let is_algebraic_number (x:expr) = Z3native.is_algebraic_number (Expr.gc x) x @@ -1123,7 +1102,7 @@ struct let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) 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 + if (den = 0) then raise (Error "Denominator is zero") else Z3native.mk_real ctx num den @@ -1159,58 +1138,58 @@ module BitVector = struct let mk_sort (ctx:context) size = Z3native.mk_bv_sort ctx size let is_bv (x:expr) = - ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == BV_SORT) - let is_bv_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNUM) - let is_bv_bit1 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT1) - let is_bv_bit0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT0) - let is_bv_uminus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNEG) - let is_bv_add (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BADD) - let is_bv_sub (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSUB) - let is_bv_mul (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BMUL) - let is_bv_sdiv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV) - let is_bv_udiv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV) - let is_bv_SRem (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM) - let is_bv_urem (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM) - let is_bv_smod (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD) - let is_bv_sdiv0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV0) - let is_bv_udiv0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV0) - let is_bv_srem0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM0) - let is_bv_urem0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM0) - let is_bv_smod0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD0) - let is_bv_ule (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULEQ) - let is_bv_sle (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLEQ) - let is_bv_uge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGEQ) - let is_bv_sge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGEQ) - let is_bv_ult (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULT) - let is_bv_slt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLT) - let is_bv_ugt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGT) - let is_bv_sgt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGT) - let is_bv_and (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BAND) - let is_bv_or (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BOR) - let is_bv_not (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOT) - let is_bv_xor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXOR) - let is_bv_nand (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNAND) - let is_bv_nor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOR) - let is_bv_xnor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXNOR) - let is_bv_concat (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONCAT) - let is_bv_signextension (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SIGN_EXT) - let is_bv_zeroextension (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ZERO_EXT) - let is_bv_extract (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXTRACT) - let is_bv_repeat (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REPEAT) - let is_bv_reduceor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDOR) - let is_bv_reduceand (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDAND) - let is_bv_comp (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BCOMP) - let is_bv_shiftleft (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSHL) - let is_bv_shiftrightlogical (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BLSHR) - let is_bv_shiftrightarithmetic (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BASHR) - let is_bv_rotateleft (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_LEFT) - let is_bv_rotateright (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_RIGHT) - let is_bv_rotateleftextended (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_LEFT) - let is_bv_rotaterightextended (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) - let is_int2bv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV) - let is_bv2int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT) - let is_bv_carry (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY) - let is_bv_xor3 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3) + ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = BV_SORT) + let is_bv_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNUM) + let is_bv_bit1 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BIT1) + let is_bv_bit0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BIT0) + let is_bv_uminus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNEG) + let is_bv_add (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BADD) + let is_bv_sub (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSUB) + let is_bv_mul (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BMUL) + let is_bv_sdiv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSDIV) + let is_bv_udiv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BUDIV) + let is_bv_SRem (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSREM) + let is_bv_urem (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BUREM) + let is_bv_smod (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSMOD) + let is_bv_sdiv0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSDIV0) + let is_bv_udiv0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BUDIV0) + let is_bv_srem0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSREM0) + let is_bv_urem0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BUREM0) + let is_bv_smod0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSMOD0) + let is_bv_ule (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ULEQ) + let is_bv_sle (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SLEQ) + let is_bv_uge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_UGEQ) + let is_bv_sge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SGEQ) + let is_bv_ult (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ULT) + let is_bv_slt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SLT) + let is_bv_ugt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_UGT) + let is_bv_sgt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SGT) + let is_bv_and (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BAND) + let is_bv_or (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BOR) + let is_bv_not (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNOT) + let is_bv_xor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BXOR) + let is_bv_nand (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNAND) + let is_bv_nor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNOR) + let is_bv_xnor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BXNOR) + let is_bv_concat (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_CONCAT) + let is_bv_signextension (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SIGN_EXT) + let is_bv_zeroextension (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ZERO_EXT) + let is_bv_extract (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_EXTRACT) + let is_bv_repeat (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_REPEAT) + let is_bv_reduceor (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BREDOR) + let is_bv_reduceand (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BREDAND) + let is_bv_comp (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BCOMP) + let is_bv_shiftleft (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BSHL) + let is_bv_shiftrightlogical (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BLSHR) + let is_bv_shiftrightarithmetic (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BASHR) + let is_bv_rotateleft (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ROTATE_LEFT) + let is_bv_rotateright (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ROTATE_RIGHT) + let is_bv_rotateleftextended (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_EXT_ROTATE_LEFT) + let is_bv_rotaterightextended (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_EXT_ROTATE_RIGHT) + let is_int2bv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_INT2BV) + let is_bv2int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BV2INT) + let is_bv_carry (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_CARRY) + let is_bv_xor3 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_XOR3) let get_size (x:Sort.sort) = Z3native.get_bv_sort_size (Sort.gc x) x let get_int (x:expr) = let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in @@ -1277,7 +1256,7 @@ struct module RoundingMode = struct let mk_sort (ctx:context) = Z3native.mk_fpa_rounding_mode_sort ctx - let is_fprm (x:expr) = (Sort.get_sort_kind (Expr.get_sort(x))) == ROUNDING_MODE_SORT + let is_fprm (x:expr) = (Sort.get_sort_kind (Expr.get_sort(x))) = ROUNDING_MODE_SORT let mk_round_nearest_ties_to_even (ctx:context) = Z3native.mk_fpa_round_nearest_ties_to_even ctx let mk_rne (ctx:context) = Z3native.mk_fpa_rne ctx let mk_round_nearest_ties_to_away (ctx:context) = Z3native.mk_fpa_round_nearest_ties_to_away ctx @@ -1309,37 +1288,37 @@ struct let mk_numeral_i_u (ctx:context) (sign:bool) (exponent:int) (significand:int) (s:Sort.sort) = Z3native.mk_fpa_numeral_int64_uint64 ctx sign exponent significand s let mk_numeral_s (ctx:context) (v:string) (s:Sort.sort) = Z3native.mk_numeral ctx v s - let is_fp (x:expr) = (Sort.get_sort_kind (Expr.get_sort x)) == FLOATING_POINT_SORT - let is_abs (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_ABS) - let is_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_NEG) - let is_add (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_ADD) - let is_sub (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_SUB) - let is_mul (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_MUL) - let is_div (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_DIV) - let is_fma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_FMA) - let is_sqrt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_SQRT) - let is_rem (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_REM) - let is_round_to_integral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_ROUND_TO_INTEGRAL) - let is_min (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_MIN) - let is_max (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_MAX) - let is_leq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_LE) - let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_LT) - let is_geq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_GE) - let is_gt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_GT) - let is_eq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_EQ) - let is_is_normal (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_NORMAL) - let is_is_subnormal (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_SUBNORMAL) - let is_is_zero (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_ZERO) - let is_is_infinite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_INF) - let is_is_nan (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_NAN) - let is_is_negative (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_NEGATIVE) - let is_is_positive (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_IS_POSITIVE) - let is_to_fp (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_FP) - let is_to_fp_unsigned (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_FP_UNSIGNED) - let is_to_ubv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_UBV) - let is_to_sbv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_SBV) - let is_to_real (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_REAL) - let is_to_ieee_bv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_IEEE_BV) + let is_fp (x:expr) = (Sort.get_sort_kind (Expr.get_sort x)) = FLOATING_POINT_SORT + let is_abs (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_ABS) + let is_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_NEG) + let is_add (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_ADD) + let is_sub (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_SUB) + let is_mul (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_MUL) + let is_div (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_DIV) + let is_fma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_FMA) + let is_sqrt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_SQRT) + let is_rem (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_REM) + let is_round_to_integral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_ROUND_TO_INTEGRAL) + let is_min (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_MIN) + let is_max (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_MAX) + let is_leq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_LE) + let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_LT) + let is_geq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_GE) + let is_gt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_GT) + let is_eq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_EQ) + let is_is_normal (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_IS_NORMAL) + let is_is_subnormal (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_IS_SUBNORMAL) + let is_is_zero (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_IS_ZERO) + let is_is_infinite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_IS_INF) + let is_is_nan (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_IS_NAN) + let is_is_negative (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_IS_NEGATIVE) + let is_is_positive (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_IS_POSITIVE) + let is_to_fp (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_TO_FP) + let is_to_fp_unsigned (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_TO_FP_UNSIGNED) + let is_to_ubv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_TO_UBV) + let is_to_sbv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_TO_SBV) + let is_to_real (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_TO_REAL) + let is_to_ieee_bv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_FPA_TO_IEEE_BV) let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x let mk_const (ctx:context) (name:Symbol.symbol) (s:Sort.sort) = @@ -1394,63 +1373,61 @@ end module Proof = struct - let is_true (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE) - let is_asserted (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ASSERTED) - let is_goal (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_GOAL) - let is_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_OEQ) - let is_modus_ponens (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS) - let is_reflexivity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REFLEXIVITY) - let is_symmetry (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SYMMETRY) - let is_transitivity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY) - let is_Transitivity_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY_STAR) - let is_monotonicity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MONOTONICITY) - let is_quant_intro (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INTRO) - let is_distributivity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DISTRIBUTIVITY) - let is_and_elimination (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_AND_ELIM) - let is_or_elimination (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NOT_OR_ELIM) - let is_rewrite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE) - let is_rewrite_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE_STAR) - let is_pull_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT) - let is_pull_quant_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT_STAR) - let is_push_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PUSH_QUANT) - let is_elim_unused_vars (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ELIM_UNUSED_VARS) - let is_der (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DER) - let is_quant_inst (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INST) - let is_hypothesis (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_HYPOTHESIS) - let is_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_LEMMA) - let is_unit_resolution (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_UNIT_RESOLUTION) - let is_iff_true (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_TRUE) - let is_iff_false (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_FALSE) - let is_commutativity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_COMMUTATIVITY) (* *) - let is_def_axiom (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_AXIOM) - let is_def_intro (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_INTRO) - let is_apply_def (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_APPLY_DEF) - let is_iff_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_OEQ) - let is_nnf_pos (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_POS) - let is_nnf_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_NEG) - let is_nnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_STAR) - let is_cnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_CNF_STAR) - let is_skolemize (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SKOLEMIZE) - let is_modus_ponens_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS_OEQ) - let is_theory_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TH_LEMMA) + let is_true (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TRUE) + let is_asserted (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_ASSERTED) + let is_goal (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_GOAL) + let is_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_OEQ) + let is_modus_ponens (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MODUS_PONENS) + let is_reflexivity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REFLEXIVITY) + let is_symmetry (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_SYMMETRY) + let is_transitivity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TRANSITIVITY) + let is_Transitivity_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TRANSITIVITY_STAR) + let is_monotonicity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MONOTONICITY) + let is_quant_intro (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_QUANT_INTRO) + let is_distributivity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DISTRIBUTIVITY) + let is_and_elimination (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_AND_ELIM) + let is_or_elimination (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NOT_OR_ELIM) + let is_rewrite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE) + let is_rewrite_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE_STAR) + let is_pull_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT) + let is_pull_quant_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT_STAR) + let is_push_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PUSH_QUANT) + let is_elim_unused_vars (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_ELIM_UNUSED_VARS) + let is_der (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DER) + let is_quant_inst (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_QUANT_INST) + let is_hypothesis (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_HYPOTHESIS) + let is_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_LEMMA) + let is_unit_resolution (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_UNIT_RESOLUTION) + let is_iff_true (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_TRUE) + let is_iff_false (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_FALSE) + let is_commutativity (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_COMMUTATIVITY) (* *) + let is_def_axiom (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DEF_AXIOM) + let is_def_intro (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DEF_INTRO) + let is_apply_def (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_APPLY_DEF) + let is_iff_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_OEQ) + let is_nnf_pos (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_POS) + let is_nnf_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_NEG) + let is_nnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_STAR) + let is_cnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_CNF_STAR) + let is_skolemize (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_SKOLEMIZE) + let is_modus_ponens_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MODUS_PONENS_OEQ) + let is_theory_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TH_LEMMA) end module Goal = struct type goal = Z3native.goal - let gc (x:goal) = Z3native.context_of_goal x + let gc = Z3native.context_of_goal let get_precision (x:goal) = goal_prec_of_int (Z3native.goal_precision (gc x) x) - let is_precise (x:goal) = (get_precision x) == GOAL_PRECISE - let is_underapproximation (x:goal) = (get_precision x) == GOAL_UNDER - let is_overapproximation (x:goal) = (get_precision x) == GOAL_OVER - let is_garbage (x:goal) = (get_precision x) == GOAL_UNDER_OVER + let is_precise (x:goal) = (get_precision x) = GOAL_PRECISE + let is_underapproximation (x:goal) = (get_precision x) = GOAL_UNDER + let is_overapproximation (x:goal) = (get_precision x) = GOAL_OVER + let is_garbage (x:goal) = (get_precision x) = GOAL_UNDER_OVER - let add (x:goal) (constraints:expr list) = - let f e = Z3native.goal_assert (gc x) x e in - ignore (List.map f constraints) ; - () + let add x constraints = + List.iter (Z3native.goal_assert (gc x) x) constraints let is_inconsistent (x:goal) = Z3native.goal_inconsistent (gc x) x let get_depth (x:goal) = Z3native.goal_depth (gc x) x @@ -1469,51 +1446,50 @@ struct let simplify (x:goal) (p:Params.params option) = let tn = Z3native.mk_tactic (gc x) "simplify" in - Z3native.tactic_inc_ref (gc x) tn ; + Z3native.tactic_inc_ref (gc x) tn; let arn = match p with | None -> Z3native.tactic_apply (gc x) tn x - | Some(pn) -> Z3native.tactic_apply_ex (gc x) tn x pn + | Some pn -> Z3native.tactic_apply_ex (gc x) tn x pn in - 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 res = if sg == 0 then - raise (Error "No subgoals") - else - Z3native.apply_result_get_subgoal (gc x) arn 0 in - Z3native.apply_result_dec_ref (gc x) arn ; - Z3native.tactic_dec_ref (gc x) tn ; + let res = if sg = 0 then + raise (Error "No subgoals") + else + Z3native.apply_result_get_subgoal (gc x) arn 0 in + Z3native.apply_result_dec_ref (gc x) arn; + Z3native.tactic_dec_ref (gc x) tn; res - let mk_goal (ctx:context) (models:bool) (unsat_cores:bool) (proofs:bool) = - Z3native.mk_goal ctx models unsat_cores proofs + let mk_goal = Z3native.mk_goal let to_string (x:goal) = Z3native.goal_to_string (gc x) x let as_expr (x:goal) = - let n = get_size x in - if n = 0 then - Boolean.mk_true (gc x) - else if n = 1 then - List.hd (get_formulas x) - else - Boolean.mk_and (gc x) (get_formulas x) + let n = get_size x in + if n = 0 then + Boolean.mk_true (gc x) + else if n = 1 then + List.hd (get_formulas x) + else + Boolean.mk_and (gc x) (get_formulas x) end module Model = struct type model = Z3native.model - let gc (x:model) = Z3native.context_of_model x + let gc = Z3native.context_of_model module FuncInterp = struct type func_interp = Z3native.func_interp - let gc (x:func_interp) = Z3native.context_of_func_interp x + let gc = Z3native.context_of_func_interp module FuncEntry = struct type func_entry = Z3native.func_entry - let gc (x:func_entry) = Z3native.context_of_func_entry x + let gc = Z3native.context_of_func_entry let get_value (x:func_entry) = Z3native.func_entry_get_value (gc x) x let get_num_args (x:func_entry) = Z3native.func_entry_get_num_args (gc x) x @@ -1544,18 +1520,18 @@ struct let f c p = ( let n = FuncEntry.get_num_args c in p ^ - let g c p = (p ^ (Expr.to_string c) ^ ", ") in - (if n > 1 then "[" else "") ^ - (List.fold_right - g - (FuncEntry.get_args c) - ((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", "))) in + let g c p = (p ^ (Expr.to_string c) ^ ", ") in + (if n > 1 then "[" else "") ^ + (List.fold_right + g + (FuncEntry.get_args c) + ((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", "))) in List.fold_right f (get_entries x) ("else -> " ^ (Expr.to_string (get_else x)) ^ "]") end 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 + 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 (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 @@ -1568,18 +1544,18 @@ struct let rec get_func_interp (x:model) (f:func_decl) = let sk = sort_kind_of_int (Z3native.get_sort_kind (gc x) (Z3native.get_range (FuncDecl.gc f) f)) in - if (FuncDecl.get_arity f) == 0 then + if FuncDecl.get_arity f = 0 then let n = Z3native.model_get_const_interp (gc x) x f in if Z3native.is_null_ast n then None else match sk with | ARRAY_SORT -> - if not (Z3native.is_as_array (gc x) n) then - 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 + if not (Z3native.is_as_array (gc x) n) then + 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 (Error "Constant functions do not have a function interpretation; use ConstInterp"); else let n = Z3native.model_get_func_interp (gc x) x f in @@ -1601,17 +1577,18 @@ struct mk_list f n let get_decls (x:model) = - let n_funcs = (get_num_funcs x) in - let n_consts = (get_num_consts x) in + let n_funcs = get_num_funcs x in + let n_consts = get_num_consts x in let f i = Z3native.model_get_func_decl (gc x) x i in let g i = Z3native.model_get_const_decl (gc x) x i in (mk_list f n_funcs) @ (mk_list g n_consts) let eval (x:model) (t:expr) (completion:bool) = - let (r, v) = Z3native.model_eval (gc x) x t completion in - if not r then None else Some v + match Z3native.model_eval (gc x) x t completion with + | (false, _) -> None + | (true, v) -> Some v - let evaluate (x:model) (t:expr) (completion:bool) = eval x t completion + let evaluate = eval let get_num_sorts (x:model) = Z3native.model_get_num_sorts (gc x) x let get_sorts (x:model) = @@ -1632,36 +1609,36 @@ struct type probe = Z3native.probe let apply (x:probe) (g:Goal.goal) = Z3native.probe_apply (gc x) x g - let get_num_probes (ctx:context) = Z3native.get_num_probes ctx + let get_num_probes = Z3native.get_num_probes let get_probe_names (ctx:context) = let n = get_num_probes ctx in let f i = Z3native.get_probe_name ctx i in mk_list f n - let get_probe_description (ctx:context) (name:string) = Z3native.probe_get_descr ctx name - let mk_probe (ctx:context) (name:string) = Z3native.mk_probe ctx name - let const (ctx:context) (v:float) = Z3native.probe_const ctx v - let lt (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_lt ctx p1 p2 - let gt (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_gt ctx p1 p2 - let le (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_le ctx p1 p2 - let ge (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_ge ctx p1 p2 - let eq (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_eq ctx p1 p2 - let and_ (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_and ctx p1 p2 - let or_ (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_or ctx p1 p2 - let not_ (ctx:context) (p:probe) = Z3native.probe_not ctx p + let get_probe_description = Z3native.probe_get_descr + let mk_probe = Z3native.mk_probe + let const = Z3native.probe_const + let lt = Z3native.probe_lt + let gt = Z3native.probe_gt + let le = Z3native.probe_le + let ge = Z3native.probe_ge + let eq = Z3native.probe_eq + let and_ = Z3native.probe_and + let or_ = Z3native.probe_or + let not_ = Z3native.probe_not end module Tactic = struct type tactic = Z3native.tactic - let gc (x:tactic) = Z3native.context_of_tactic x + let gc = Z3native.context_of_tactic module ApplyResult = struct type apply_result = Z3native.apply_result - let gc (x:apply_result) = Z3native.context_of_apply_result x + let gc = Z3native.context_of_apply_result let get_num_subgoals (x:apply_result) = Z3native.apply_result_get_num_subgoals (gc x) x @@ -1681,77 +1658,63 @@ struct let apply (x:tactic) (g:Goal.goal) (p:Params.params option) = match p with | None -> Z3native.tactic_apply (gc x) x g - | Some (pn) -> Z3native.tactic_apply_ex (gc x) x g pn + | Some pn -> Z3native.tactic_apply_ex (gc x) x g pn - let get_num_tactics (ctx:context) = Z3native.get_num_tactics ctx + let get_num_tactics = Z3native.get_num_tactics let get_tactic_names (ctx:context) = let n = get_num_tactics ctx in let f i = Z3native.get_tactic_name ctx i in mk_list f n - let get_tactic_description (ctx:context) (name:string) = Z3native.tactic_get_descr ctx name - let mk_tactic (ctx:context) (name:string) = Z3native.mk_tactic ctx name + let get_tactic_description = Z3native.tactic_get_descr + let mk_tactic = Z3native.mk_tactic let and_then (ctx:context) (t1:tactic) (t2:tactic) (ts:tactic list) = let f p c = (match p with - | None -> Some c - | Some(x) -> Some (Z3native.tactic_and_then ctx c x)) in + | None -> Some c + | Some(x) -> Some (Z3native.tactic_and_then ctx c x)) in match (List.fold_left f None ts) with | None -> Z3native.tactic_and_then ctx t1 t2 | Some(x) -> let o = Z3native.tactic_and_then ctx t2 x in - Z3native.tactic_and_then ctx t1 o + Z3native.tactic_and_then ctx t1 o - let or_else (ctx:context) (t1:tactic) (t2:tactic) = Z3native.tactic_or_else ctx t1 t2 - let try_for (ctx:context) (t:tactic) (ms:int) = Z3native.tactic_try_for ctx t ms - let when_ (ctx:context) (p:Probe.probe) (t:tactic) = Z3native.tactic_when ctx p t - let cond (ctx:context) (p:Probe.probe) (t1:tactic) (t2:tactic) = Z3native.tactic_cond ctx p t1 t2 - let repeat (ctx:context) (t:tactic) (max:int) = Z3native.tactic_repeat ctx t max - let skip (ctx:context) = Z3native.tactic_skip ctx - let fail (ctx:context) = Z3native.tactic_fail ctx - let fail_if (ctx:context) (p:Probe.probe) = Z3native.tactic_fail_if ctx p - let fail_if_not_decided (ctx:context) = Z3native.tactic_fail_if_not_decided ctx - let using_params (ctx:context) (t:tactic) (p:Params.params) = Z3native.tactic_using_params ctx t p - let with_ (ctx:context) (t:tactic) (p:Params.params) = using_params ctx t p + let or_else = Z3native.tactic_or_else + let try_for = Z3native.tactic_try_for + let when_ = Z3native.tactic_when + let cond = Z3native.tactic_cond + let repeat = Z3native.tactic_repeat + let skip = Z3native.tactic_skip + let fail = Z3native.tactic_fail + let fail_if = Z3native.tactic_fail_if + let fail_if_not_decided = Z3native.tactic_fail_if_not_decided + let using_params = Z3native.tactic_using_params + let with_ = using_params let par_or (ctx:context) (t:tactic list) = Z3native.tactic_par_or ctx (List.length t) (Array.of_list t) - let par_and_then (ctx:context) (t1:tactic) (t2:tactic) = Z3native.tactic_par_and_then ctx t1 t2 - let interrupt (ctx:context) = Z3native.interrupt ctx + let par_and_then = Z3native.tactic_par_and_then + let interrupt = Z3native.interrupt end module Statistics = struct type statistics = Z3native.stats - let gc (x:statistics) = Z3native.context_of_stats x + let gc = Z3native.context_of_stats module Entry = struct type statistics_entry = { - mutable m_key:string ; - mutable m_is_int:bool ; - mutable m_is_float:bool ; - mutable m_int:int ; - mutable m_float:float } + m_key:string; + m_is_int:bool; + m_is_float:bool; + m_int:int; + m_float:float } let create_si k v = - let res:statistics_entry = { - m_key = k ; - m_is_int = true ; - m_is_float = false ; - m_int = v ; - m_float = 0.0 - } in - res + { m_key = k; m_is_int = true; m_is_float = false; m_int = v; m_float = 0.0 } let create_sd k v = - let res:statistics_entry = { - m_key = k ; - m_is_int = false ; - m_is_float = true ; - m_int = 0 ; - m_float = v - } in - res + { m_key = k; m_is_int = false; m_is_float = true; m_int = 0; m_float = v } let get_key (x:statistics_entry) = x.m_key let get_int (x:statistics_entry) = x.m_int @@ -1759,9 +1722,9 @@ struct let is_int (x:statistics_entry) = x.m_is_int let is_float (x:statistics_entry) = x.m_is_float let to_string_value (x:statistics_entry) = - if (is_int x) then + if is_int x then string_of_int (get_int x) - else if (is_float x) then + else if is_float x then string_of_float (get_float x) else raise (Error "Unknown statistical entry type") @@ -1773,12 +1736,13 @@ struct let get_entries (x:statistics) = let n = get_size x in - let f i = ( + let f i = let k = Z3native.stats_get_key (gc x) x i in - if (Z3native.stats_is_uint (gc x) x i) then - (Entry.create_si k (Z3native.stats_get_uint_value (gc x) x i)) + if Z3native.stats_is_uint (gc x) x i then + Entry.create_si k (Z3native.stats_get_uint_value (gc x) x i) else - (Entry.create_sd k (Z3native.stats_get_double_value (gc x) x i))) in + Entry.create_sd k (Z3native.stats_get_double_value (gc x) x i) + in mk_list f n let get_keys (x:statistics) = @@ -1787,8 +1751,8 @@ struct mk_list f n let get (x:statistics) (key:string) = - let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in - List.fold_left f None (get_entries x) + try Some(List.find (fun c -> Entry.get_key c = key) (get_entries x)) with + | Not_found -> None end @@ -1796,7 +1760,7 @@ module Solver = struct type solver = Z3native.solver type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE - let gc (x:solver) = Z3native.context_of_solver x + let gc = Z3native.context_of_solver let string_of_status (s:status) = match s with | UNSATISFIABLE -> "unsatisfiable" @@ -1811,83 +1775,77 @@ struct let pop (x:solver) (n:int) = Z3native.solver_pop (gc x) x n let reset (x:solver) = Z3native.solver_reset (gc x) x - let add (x:solver) (constraints:expr list) = - let f e = (Z3native.solver_assert (gc x) x e) in - ignore (List.map f constraints) + let add x constraints = + List.iter (Z3native.solver_assert (gc x) x) constraints - let assert_and_track_l (x:solver) (cs:expr list) (ps:expr list) = - if ((List.length cs) != (List.length ps)) then - 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) + let assert_and_track_l x cs ps = + try List.iter2 (Z3native.solver_assert_and_track (gc x) x) cs ps with + | Invalid_argument _ -> raise (Error "Argument size mismatch") - let assert_and_track (x:solver) (c:expr) (p:expr) = - Z3native.solver_assert_and_track (gc x) x c p + let assert_and_track x = Z3native.solver_assert_and_track (gc x) x - let get_num_assertions (x:solver) = + let get_num_assertions x = let a = Z3native.solver_get_assertions (gc x) x in AST.ASTVector.get_size a - let get_assertions (x:solver) = + let get_assertions x = let av = Z3native.solver_get_assertions (gc x) x in AST.ASTVector.to_expr_list av let check (x:solver) (assumptions:expr list) = - let r = - if ((List.length assumptions) == 0) then - lbool_of_int (Z3native.solver_check (gc x) x) - else - lbool_of_int (Z3native.solver_check_assumptions (gc x) x (List.length assumptions) (Array.of_list assumptions)) + let result = + match assumptions with + | [] -> Z3native.solver_check (gc x) x + | _::_ -> + let assumption_array = Array.of_list assumptions in + Z3native.solver_check_assumptions (gc x) x (Array.length assumption_array) assumption_array in - match r with + match lbool_of_int result with | L_TRUE -> SATISFIABLE | L_FALSE -> UNSATISFIABLE | _ -> UNKNOWN - let get_model (x:solver) = + let get_model x = let q = Z3native.solver_get_model (gc x) x in if Z3native.is_null_model q then None else Some q - let get_proof (x:solver) = + let get_proof x = let q = Z3native.solver_get_proof (gc x) x in if Z3native.is_null_ast q then None else Some q - let get_unsat_core (x:solver) = + let get_unsat_core x = let av = Z3native.solver_get_unsat_core (gc x) x in AST.ASTVector.to_expr_list av - let get_reason_unknown (x:solver) = Z3native.solver_get_reason_unknown (gc x) x - let get_statistics (x:solver) = Z3native.solver_get_statistics (gc x) x + let get_reason_unknown x = Z3native.solver_get_reason_unknown (gc x) x + let get_statistics x = Z3native.solver_get_statistics (gc x) x - let mk_solver (ctx:context) (logic:Symbol.symbol option) = + let mk_solver ctx logic = match logic with | None -> Z3native.mk_solver ctx - | Some (x) -> Z3native.mk_solver_for_logic ctx x + | Some x -> Z3native.mk_solver_for_logic ctx x - let mk_solver_s (ctx:context) (logic:string) = mk_solver ctx (Some (Symbol.mk_string ctx logic)) - let mk_simple_solver (ctx:context) = Z3native.mk_simple_solver ctx - let mk_solver_t (ctx:context) (t:Tactic.tactic) = Z3native.mk_solver_from_tactic ctx t - let translate (x:solver) (to_ctx:context) = Z3native.solver_translate (gc x) x to_ctx - let to_string (x:solver) = Z3native.solver_to_string (gc x) x + let mk_solver_s ctx logic = mk_solver ctx (Some (Symbol.mk_string ctx logic)) + let mk_simple_solver = Z3native.mk_simple_solver + let mk_solver_t = Z3native.mk_solver_from_tactic + let translate x = Z3native.solver_translate (gc x) x + let to_string x = Z3native.solver_to_string (gc x) x end module Fixedpoint = struct type fixedpoint = Z3native.fixedpoint - let gc (x:fixedpoint) = Z3native.context_of_fixedpoint x + let gc = Z3native.context_of_fixedpoint - let get_help (x:fixedpoint) = Z3native.fixedpoint_get_help (gc x) x - let set_parameters (x:fixedpoint) (p:Params.params) = Z3native.fixedpoint_set_params (gc x) x p - let get_param_descrs (x:fixedpoint) = Z3native.fixedpoint_get_param_descrs (gc x) x + let get_help x = Z3native.fixedpoint_get_help (gc x) x + let set_parameters x = Z3native.fixedpoint_set_params (gc x) x + let get_param_descrs x = Z3native.fixedpoint_get_param_descrs (gc x) x - let add (x:fixedpoint) (constraints:expr list) = - let f e = Z3native.fixedpoint_assert (gc x) x e in - ignore (List.map f constraints) ; - () + let add x constraints = + List.iter (Z3native.fixedpoint_assert (gc x) x) constraints - let register_relation (x:fixedpoint) (f:func_decl) = Z3native.fixedpoint_register_relation (gc x) x f + let register_relation x = Z3native.fixedpoint_register_relation (gc x) x let add_rule (x:fixedpoint) (rule:expr) (name:Symbol.symbol option) = match name with @@ -1898,27 +1856,27 @@ struct Z3native.fixedpoint_add_fact (gc x) x pred (List.length args) (Array.of_list args) let query (x:fixedpoint) (query:expr) = - match (lbool_of_int (Z3native.fixedpoint_query (gc x) x query)) with - | L_TRUE -> Solver.SATISFIABLE - | L_FALSE -> Solver.UNSATISFIABLE - | _ -> Solver.UNKNOWN - - let query_r (x:fixedpoint) (relations:func_decl list) = - match (lbool_of_int (Z3native.fixedpoint_query_relations (gc x) x (List.length relations) (Array.of_list relations))) with + match lbool_of_int (Z3native.fixedpoint_query (gc x) x query) with | L_TRUE -> Solver.SATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE | _ -> Solver.UNKNOWN - let push (x:fixedpoint) = Z3native.fixedpoint_push (gc x) x - let pop (x:fixedpoint) = Z3native.fixedpoint_pop (gc x) x - let update_rule (x:fixedpoint) (rule:expr) (name:Symbol.symbol) = Z3native.fixedpoint_update_rule (gc x) x rule name + let query_r (x:fixedpoint) (relations:func_decl list) = + match lbool_of_int (Z3native.fixedpoint_query_relations (gc x) x (List.length relations) (Array.of_list relations)) with + | L_TRUE -> Solver.SATISFIABLE + | L_FALSE -> Solver.UNSATISFIABLE + | _ -> Solver.UNKNOWN - let get_answer (x:fixedpoint) = + let push x = Z3native.fixedpoint_push (gc x) x + let pop x = Z3native.fixedpoint_pop (gc x) x + let update_rule x = Z3native.fixedpoint_update_rule (gc x) x + + let get_answer x = let q = Z3native.fixedpoint_get_answer (gc x) x in if Z3native.is_null_ast q then None else Some q - let get_reason_unknown (x:fixedpoint) = Z3native.fixedpoint_get_reason_unknown (gc x) x - let get_num_levels (x:fixedpoint) (predicate:func_decl) = Z3native.fixedpoint_get_num_levels (gc x) x predicate + let get_reason_unknown x = Z3native.fixedpoint_get_reason_unknown (gc x) x + let get_num_levels x = Z3native.fixedpoint_get_num_levels (gc x) x let get_cover_delta (x:fixedpoint) (level:int) (predicate:func_decl) = let q = Z3native.fixedpoint_get_cover_delta (gc x) x level predicate in @@ -1961,16 +1919,15 @@ struct type optimize = Z3native.optimize type handle = { opt:optimize; h:int } - let mk_handle (x:optimize) h = { opt = x; h = h } + let mk_handle opt h = { opt; h } let mk_opt (ctx:context) = Z3native.mk_optimize ctx let get_help (x:optimize) = Z3native.optimize_get_help (gc x) x let set_parameters (x:optimize) (p:Params.params) = Z3native.optimize_set_params (gc x) x p let get_param_descrs (x:optimize) = Z3native.optimize_get_param_descrs (gc x) x - let add (x:optimize) (constraints:expr list) = - let f e = Z3native.optimize_assert (gc x) x e in - List.iter f constraints + let add x constraints = + List.iter (Z3native.optimize_assert (gc x) x) constraints let add_soft (x:optimize) (e:Expr.expr) (w:string) (s:Symbol.symbol) = mk_handle x (Z3native.optimize_assert_soft (gc x) x e w s) @@ -1991,7 +1948,7 @@ struct let get_lower (x:handle) (idx:int) = Z3native.optimize_get_lower (gc x.opt) x.opt idx let get_upper (x:handle) (idx:int) = Z3native.optimize_get_upper (gc x.opt) x.opt idx - let push (x:optimize) = Z3native.optimize_push (gc x) x + let push (x:optimize) = Z3native.optimize_push (gc x) x let pop (x:optimize) = Z3native.optimize_pop (gc x) x let get_reason_unknown (x:optimize) = Z3native.optimize_get_reason_unknown (gc x) x let to_string (x:optimize) = Z3native.optimize_to_string (gc x) x @@ -2003,40 +1960,40 @@ module SMT = struct let benchmark_to_smtstring (ctx:context) (name:string) (logic:string) (status:string) (attributes:string) (assumptions:expr list) (formula:expr) = Z3native.benchmark_to_smtlib_string ctx name logic status attributes - (List.length assumptions) (Array.of_list assumptions) - formula + (List.length assumptions) (Array.of_list assumptions) + formula let parse_smtlib_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = let csn = (List.length sort_names) in let cs = (List.length sorts) in let cdn = (List.length decl_names) in let cd = (List.length decls) in - if (csn != cs || cdn != cd) then + if (csn <> cs || cdn <> cd) then raise (Error "Argument size mismatch") else Z3native.parse_smtlib_string ctx str - cs - (Array.of_list sort_names) - (Array.of_list sorts) - cd - (Array.of_list decl_names) - (Array.of_list decls) + cs + (Array.of_list sort_names) + (Array.of_list sorts) + cd + (Array.of_list decl_names) + (Array.of_list decls) let parse_smtlib_file (ctx:context) (file_name:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = let csn = (List.length sort_names) in let cs = (List.length sorts) in let cdn = (List.length decl_names) in let cd = (List.length decls) in - if (csn != cs || cdn != cd) then + if (csn <> cs || cdn <> cd) then raise (Error "Argument size mismatch") else Z3native.parse_smtlib_file ctx file_name - cs - (Array.of_list sort_names) - (Array.of_list sorts) - cd - (Array.of_list decl_names) - (Array.of_list decls) + cs + (Array.of_list sort_names) + (Array.of_list sorts) + cd + (Array.of_list decl_names) + (Array.of_list decls) let get_num_smtlib_formulas (ctx:context) = Z3native.get_smtlib_num_formulas ctx @@ -2071,46 +2028,46 @@ struct let cs = (List.length sorts) in let cdn = (List.length decl_names) in let cd = (List.length decls) in - if (csn != cs || cdn != cd) then - raise (Error "Argument size mismatch") + if (csn <> cs || cdn <> cd) then + raise (Error "Argument size mismatch") else Z3native.parse_smtlib2_string ctx str - cs - (Array.of_list sort_names) - (Array.of_list sorts) - cd - (Array.of_list decl_names) - (Array.of_list decls) + cs + (Array.of_list sort_names) + (Array.of_list sorts) + cd + (Array.of_list decl_names) + (Array.of_list decls) let parse_smtlib2_file (ctx:context) (file_name:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = let csn = (List.length sort_names) in let cs = (List.length sorts) in let cdn = (List.length decl_names) in let cd = (List.length decls) in - if (csn != cs || cdn != cd) then + if (csn <> cs || cdn <> cd) then raise (Error "Argument size mismatch") else - Z3native.parse_smtlib2_string ctx file_name - cs - (Array.of_list sort_names) - (Array.of_list sorts) - cd - (Array.of_list decl_names) - (Array.of_list decls) + Z3native.parse_smtlib2_string ctx file_name + cs + (Array.of_list sort_names) + (Array.of_list sorts) + cd + (Array.of_list decl_names) + (Array.of_list decls) end module Interpolation = struct - let mk_interpolant (ctx:context) (a:expr) = Z3native.mk_interpolant ctx a + let mk_interpolant = Z3native.mk_interpolant let mk_interpolation_context (settings:(string * string) list) = let cfg = Z3native.mk_config () in let f e = Z3native.set_param_value cfg (fst e) (snd e) in - (List.iter f settings) ; + List.iter f settings; let res = Z3native.mk_interpolation_context cfg in - Z3native.del_config(cfg) ; - Z3native.set_ast_print_mode res (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ; - Z3native.set_internal_error_handler res ; + Z3native.del_config cfg; + Z3native.set_ast_print_mode res (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT); + Z3native.set_internal_error_handler res; res let get_interpolant (ctx:context) (pf:expr) (pat:expr) (p:Params.params) = @@ -2121,60 +2078,55 @@ struct let (r, interp, model) = Z3native.compute_interpolant ctx pat p in let res = (lbool_of_int r) in match res with - | L_TRUE -> (res, None, Some(model)) - | L_FALSE -> (res, Some(AST.ASTVector.to_expr_list interp), None) + | L_TRUE -> (res, None, Some model) + | L_FALSE -> (res, Some (AST.ASTVector.to_expr_list interp), None) | _ -> (res, None, None) - let get_interpolation_profile (ctx:context) = Z3native.interpolation_profile ctx + let get_interpolation_profile = Z3native.interpolation_profile 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 | 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 - let f3 i = Array.get theory i in - ((mk_list f1 num), - (mk_list f2 num), - (mk_list f3 num_theory)) + let f1 i = Array.get cnsts i in + let f2 i = Array.get parents i in + let f3 i = Array.get theory i in + (mk_list f1 num, + mk_list f2 num, + mk_list f3 num_theory) let check_interpolant (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (interps:Expr.expr list) (num_theory:int) (theory:Expr.expr list) = let (r, str) = Z3native.check_interpolant ctx - num - (Array.of_list cnsts) - (Array.of_list parents) - (Array.of_list interps) - num_theory - (Array.of_list theory) in + num + (Array.of_list cnsts) + (Array.of_list parents) + (Array.of_list interps) + num_theory + (Array.of_list theory) in match (lbool_of_int r) with | 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) = - (Z3native.write_interpolation_problem ctx num (Array.of_list cnsts) (Array.of_list parents) filename num_theory (Array.of_list theory)) ; + (Z3native.write_interpolation_problem ctx num (Array.of_list cnsts) (Array.of_list parents) filename num_theory (Array.of_list theory)); () end -let set_global_param (id:string) (value:string) = - (Z3native.global_param_set id value) +let set_global_param = Z3native.global_param_set -let get_global_param (id:string) = - let (r, v) = (Z3native.global_param_get id) in - if not r then - None - else - Some v +let get_global_param id = + match Z3native.global_param_get id with + | (false, _) -> None + | (true, v) -> Some v -let global_param_reset_all = - Z3native.global_param_reset_all +let global_param_reset_all = Z3native.global_param_reset_all -let toggle_warning_messages (enabled:bool) = - Z3native.toggle_warning_messages enabled +let toggle_warning_messages = Z3native.toggle_warning_messages -let enable_trace (tag:string) = - (Z3native.enable_trace tag) +let enable_trace = Z3native.enable_trace -let disable_trace (tag:string) = - (Z3native.enable_trace tag) +let disable_trace = Z3native.enable_trace diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 555e25bc0..02d6a8b2a 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -5,19 +5,19 @@ @author CM Wintersteiger (cwinter) 2012-12-17 *) -(** General Z3 exceptions +(** General Z3 exceptions Many functions in this API may throw an exception; if they do, it is this one.*) exception Error of string (** Context objects. - Most interactions with Z3 are interpreted in some context; many users will only - require one such object, but power users may require more than one. To start using - Z3, do + Most interactions with Z3 are interpreted in some context; many users will only + require one such object, but power users may require more than one. To start using + Z3, do - let ctx = (mk_context []) in + let ctx = (mk_context []) in (...) @@ -26,17 +26,17 @@ exception Error of string let cfg = [("model", "true"); ("...", "...")] in - let ctx = (mk_context cfg) in + let ctx = (mk_context cfg) in (...) *) type context -(** Create a context object +(** Create a context object The following parameters can be set: - + - proof (Boolean) Enable proof generation - - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting + - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting - trace (Boolean) Tracing support for VCC - trace_file_name (String) Trace out file for VCC traces - timeout (unsigned) default timeout (in milliseconds) used for solvers @@ -44,16 +44,16 @@ type context - auto_config use heuristics to automatically select solver and configure it - model model generation for solvers, this parameter can be overwritten when creating a solver - model_validate validate models produced by solvers - - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver *) val mk_context : (string * string) list -> context (** Interaction logging for Z3 - Note that this is a global, static log and if multiple Context + Note that this is a global, static log and if multiple Context objects are created, it logs the interaction with all of them. *) module Log : sig - (** Open an interaction log file. + (** Open an interaction log file. @return True if opening the log file succeeds, false otherwise. *) (* CMW: "open" is a reserved keyword. *) val open_ : string -> bool @@ -107,7 +107,7 @@ sig (** A string representation of the symbol. *) val to_string : symbol -> string - (** Creates a new symbol using an integer. + (** Creates a new symbol using an integer. Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1. *) val mk_int : context -> int -> symbol @@ -125,21 +125,21 @@ end (** The abstract syntax tree (AST) module *) module rec AST : sig - type ast + type ast (** Vectors of ASTs *) module ASTVector : sig - type ast_vector + type ast_vector (** Create an empty AST vector *) val mk_ast_vector : context -> ast_vector - + (** The size of the vector *) val get_size : ast_vector -> int (** Retrieves the i-th object in the vector. - @return An AST *) + @return An AST *) val get : ast_vector -> int -> ast (** Sets the i-th object in the vector. *) @@ -149,11 +149,11 @@ sig val resize : ast_vector -> int -> unit (** Add an ast to the back of the vector. The size - is increased by 1. *) + is increased by 1. *) val push : ast_vector -> ast -> unit (** Translates all ASTs in the vector to another context. - @return A new ASTVector *) + @return A new ASTVector *) val translate : ast_vector -> context -> ast_vector (** Translates the ASTVector into an (Ast.ast list) *) @@ -173,13 +173,13 @@ sig (** Create an empty mapping from AST to AST *) val mk_ast_map : context -> ast_map - + (** Checks whether the map contains a key. - @return True if the key in the map, false otherwise. *) + @return True if the key in the map, false otherwise. *) val contains : ast_map -> ast -> bool (** Finds the value associated with the key. - This function signs an error when the key is not a key in the map. *) + This function signs an error when the key is not a key in the map. *) val find : ast_map -> ast -> ast (** Stores or replaces a new key/value pair in the map. *) @@ -208,7 +208,7 @@ sig (** A unique identifier for the AST (unique among all ASTs). *) val get_id : ast -> int - (** The kind of the AST. *) + (** The kind of the AST. *) val get_ast_kind : ast -> Z3enums.ast_kind (** Indicates whether the AST is an Expr *) @@ -233,7 +233,7 @@ sig val to_sexpr : ast -> string (** Comparison operator. - @return True if the two ast's are from the same context + @return True if the two ast's are from the same context and represent the same sort; false otherwise. *) val equal : ast -> ast -> bool @@ -252,7 +252,7 @@ sig type sort (** Comparison operator. - @return True if the two sorts are from the same context + @return True if the two sorts are from the same context and represent the same sort; false otherwise. *) val equal : sort -> sort -> bool @@ -285,14 +285,14 @@ sig sig (** Parameters of func_decls *) type parameter = - P_Int of int + P_Int of int | P_Dbl of float | P_Sym of Symbol.symbol | P_Srt of Sort.sort | P_Ast of AST.ast | P_Fdl of func_decl | P_Rat of string - + (** The kind of the parameter. *) val get_kind : parameter -> Z3enums.parameter_kind @@ -354,10 +354,10 @@ sig (** The size of the domain of the function declaration {!get_arity} *) val get_domain_size : func_decl -> int - + (** The domain of the function declaration *) val get_domain : func_decl -> Sort.sort list - + (** The range of the function declaration *) val get_range : func_decl -> Sort.sort @@ -373,7 +373,7 @@ sig (** The parameters of the function declaration *) val get_parameters : func_decl -> Parameter.parameter list - (** Create expression that applies function to arguments. *) + (** Create expression that applies function to arguments. *) val apply : func_decl -> Expr.expr list -> Expr.expr end @@ -387,7 +387,7 @@ sig (** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *) module ParamDescrs : sig - type param_descrs + type param_descrs (** Validate a set of parameters. *) val validate : param_descrs -> params -> unit @@ -424,19 +424,19 @@ sig val to_string : params -> string (** Update a mutable configuration parameter. - + The list of all configuration parameters can be obtained using the Z3 executable: [z3.exe -p] Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter. *) val update_param_value : context -> string -> string -> unit - + (** Selects the format used for pretty-printing expressions. - + The default mode for pretty printing expressions is to produce - SMT-LIB style output where common subexpressions are printed + SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called PRINT_SMTLIB_FULL. - To print shared common subexpressions only once, + To print shared common subexpressions only once, use the PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT. @@ -471,7 +471,7 @@ sig (** The number of arguments of the expression. *) val get_num_args : Expr.expr -> int - (** The arguments of the expression. *) + (** The arguments of the expression. *) val get_args : Expr.expr -> Expr.expr list (** Update the arguments of the expression using an array of expressions. @@ -479,9 +479,9 @@ sig val update : Expr.expr -> Expr.expr list -> expr (** Substitute every occurrence of [from[i]] in the expression with [to[i]], for [i] smaller than [num_exprs]. - + The result is the new expression. The arrays [from] and [to] must have size [num_exprs]. - For every [i] smaller than [num_exprs], we must have that + For every [i] smaller than [num_exprs], we must have that sort of [from[i]] must be equal to sort of [to[i]]. *) val substitute : Expr.expr -> Expr.expr list -> Expr.expr list -> expr @@ -498,14 +498,14 @@ sig @return A copy of the term which is associated with the other context *) val translate : Expr.expr -> context -> expr - (** Returns a string representation of the expression. *) + (** Returns a string representation of the expression. *) val to_string : Expr.expr -> string (** Indicates whether the term is a numeral *) val is_numeral : Expr.expr -> bool (** Indicates whether the term is well-sorted. - @return True if the term is well-sorted, false otherwise. *) + @return True if the term is well-sorted, false otherwise. *) val is_well_sorted : Expr.expr -> bool (** The Sort of the term. *) @@ -513,31 +513,31 @@ sig (** Indicates whether the term represents a constant. *) val is_const : Expr.expr -> bool - + (** Creates a new constant. *) val mk_const : context -> Symbol.symbol -> Sort.sort -> expr - + (** Creates a new constant. *) val mk_const_s : context -> string -> Sort.sort -> expr - + (** Creates a constant from the func_decl. *) val mk_const_f : context -> FuncDecl.func_decl -> expr - + (** Creates a fresh constant with a name prefixed with a string. *) val mk_fresh_const : context -> string -> Sort.sort -> expr - + (** Create a new function application. *) val mk_app : context -> FuncDecl.func_decl -> Expr.expr list -> expr - - (** Create a numeral of a given sort. + + (** Create a numeral of a given sort. @return A Term with the given value and sort *) val mk_numeral_string : context -> string -> Sort.sort -> expr - + (** Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer. - It is slightly faster than [MakeNumeral] since it is not necessary to parse a string. + It is slightly faster than [MakeNumeral] since it is not necessary to parse a string. @return A Term with the given value and sort *) val mk_numeral_int : context -> int -> Sort.sort -> expr - + (** Comparison operator. @return True if the two expr's are equal; false otherwise. *) val equal : expr -> expr -> bool @@ -553,22 +553,22 @@ sig (** Create a Boolean sort *) val mk_sort : context -> Sort.sort - (** Create a Boolean constant. *) + (** Create a Boolean constant. *) val mk_const : context -> Symbol.symbol -> Expr.expr - (** Create a Boolean constant. *) + (** Create a Boolean constant. *) val mk_const_s : context -> string -> Expr.expr - (** The true Term. *) + (** The true Term. *) val mk_true : context -> Expr.expr - (** The false Term. *) + (** The false Term. *) val mk_false : context -> Expr.expr - (** Creates a Boolean value. *) + (** Creates a Boolean value. *) val mk_val : context -> bool -> Expr.expr - (** Mk an expression representing [not(a)]. *) + (** Mk an expression representing [not(a)]. *) val mk_not : context -> Expr.expr -> Expr.expr (** Create an expression representing an if-then-else: [ite(t1, t2, t3)]. *) @@ -665,7 +665,7 @@ sig (** The de-Burijn index of a bound variable. - + Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format. @@ -696,19 +696,19 @@ sig (** The patterns. *) val get_patterns : quantifier -> Pattern.pattern list - + (** The number of no-patterns. *) val get_num_no_patterns : quantifier -> int - + (** The no-patterns. *) val get_no_patterns : quantifier -> Pattern.pattern list (** The number of bound variables. *) val get_num_bound : quantifier -> int - + (** The symbols for the bound variables. *) val get_bound_variable_names : quantifier -> Symbol.symbol list - + (** The sorts of the bound variables. *) val get_bound_variable_sorts : quantifier -> Sort.sort list @@ -735,7 +735,7 @@ sig (** Create a Quantifier. *) val mk_quantifier : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier - + (** Create a Quantifier. *) val mk_quantifier : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier @@ -749,28 +749,28 @@ sig (** Create a new array sort. *) val mk_sort : context -> Sort.sort -> Sort.sort -> Sort.sort - (** Indicates whether the term is an array store. - It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). + (** Indicates whether the term is an array store. + It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). Array store takes at least 3 arguments. *) val is_store : Expr.expr -> bool (** Indicates whether the term is an array select. *) val is_select : Expr.expr -> bool - (** Indicates whether the term is a constant array. + (** Indicates whether the term is a constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary. *) val is_constant_array : Expr.expr -> bool - (** Indicates whether the term is a default array. + (** Indicates whether the term is a default array. For example default(const(v)) = v. The function is unary. *) val is_default_array : Expr.expr -> bool - (** Indicates whether the term is an array map. + (** Indicates whether the term is an array map. It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. *) val is_array_map : Expr.expr -> bool - (** Indicates whether the term is an as-array term. - An as-array term is n array value that behaves as the function graph of the + (** Indicates whether the term is an as-array term. + An as-array term is n array value that behaves as the function graph of the function passed as parameter. *) val is_as_array : Expr.expr -> bool @@ -779,54 +779,54 @@ sig (** The domain of the array sort. *) val get_domain : Sort.sort -> Sort.sort - + (** The range of the array sort. *) val get_range : Sort.sort -> Sort.sort - - (** Create an array constant. *) + + (** Create an array constant. *) val mk_const : context -> Symbol.symbol -> Sort.sort -> Sort.sort -> Expr.expr - - (** Create an array constant. *) + + (** Create an array constant. *) val mk_const_s : context -> string -> Sort.sort -> Sort.sort -> Expr.expr - - (** Array read. - - The argument [a] is the array and [i] is the index - of the array that gets read. - - The node [a] must have an array sort [[domain -> range]], + + (** Array read. + + The argument [a] is the array and [i] is the index + of the array that gets read. + + The node [a] must have an array sort [[domain -> range]], and [i] must have the sort [domain]. The sort of the result is [range]. {!Z3Array.mk_sort} {!mk_store} *) val mk_select : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Array update. - - The node [a] must have an array sort [[domain -> range]], + (** Array update. + + The node [a] must have an array sort [[domain -> range]], [i] must have sort [domain], [v] must have sort range. The sort of the result is [[domain -> range]]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. - The result of this function is an array that is equal to [a] + The result of this function is an array that is equal to [a] (with respect to [select]) - on all indices except for [i], where it maps to [v] - (and the [select] of [a] with + on all indices except for [i], where it maps to [v] + (and the [select] of [a] with respect to [i] may be a different value). {!Z3Array.mk_sort} {!mk_select} *) val mk_store : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr (** Create a constant array. - - The resulting term is an array, such that a [select]on an arbitrary index + + The resulting term is an array, such that a [select]on an arbitrary index produces the value [v]. {!Z3Array.mk_sort} {!mk_select} *) val mk_const_array : context -> Sort.sort -> Expr.expr -> Expr.expr (** Maps f on the argument arrays. - + Eeach element of [args] must be of an array sort [[domain_i -> range_i]]. The function declaration [f] must have type [ range_1 .. range_n -> range]. [v] must have sort range. The sort of the result is [[domain_i -> range]]. @@ -836,12 +836,12 @@ sig val mk_map : context -> FuncDecl.func_decl -> Expr.expr list -> Expr.expr (** Access the array default value. - - Produces the default range value, for arrays that can be represented as + + Produces the default range value, for arrays that can be represented as finite maps with a default range value. *) val mk_term_array : context -> Expr.expr -> Expr.expr - (** Create array extensionality index given two arrays with the same sort. + (** Create array extensionality index given two arrays with the same sort. The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B)) *) @@ -928,9 +928,9 @@ sig val is_relation : Expr.expr -> bool (** Indicates whether the term is an relation store - + Insert a record into a relation. - The function takes [n+1] arguments, where the first argument is the relation and the remaining [n] elements + The function takes [n+1] arguments, where the first argument is the relation and the remaining [n] elements correspond to the [n] columns of the relation. *) val is_store : Expr.expr -> bool @@ -943,7 +943,7 @@ sig (** Indicates whether the term is a relational join *) val is_join : Expr.expr -> bool - (** Indicates whether the term is the union or convex hull of two relations. + (** Indicates whether the term is the union or convex hull of two relations. The function takes two arguments. *) val is_union : Expr.expr -> bool @@ -956,29 +956,29 @@ sig val is_project : Expr.expr -> bool (** Indicates whether the term is a relation filter - + Filter (restrict) a relation with respect to a predicate. - The first argument is a relation. + The first argument is a relation. The second argument is a predicate with free de-Brujin indices corresponding to the columns of the relation. So the first column in the relation has index 0. *) val is_filter : Expr.expr -> bool (** Indicates whether the term is an intersection of a relation with the negation of another. - + Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function - + target = filter_by_negation(pos, neg, columns) - + where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with ( x : expr ) on the columns c1, d1, .., cN, dN. *) val is_negation_filter : Expr.expr -> bool (** Indicates whether the term is the renaming of a column in a relation - + The function takes one argument. The parameters contain the renaming as a cycle. *) val is_rename : Expr.expr -> bool @@ -987,18 +987,18 @@ sig val is_complement : Expr.expr -> bool (** Indicates whether the term is a relational select - + Check if a record is an element of the relation. The function takes [n+1] arguments, where the first argument is a relation, and the remaining [n] arguments correspond to a record. *) val is_select : Expr.expr -> bool (** Indicates whether the term is a relational clone (copy) - - Create a fresh copy (clone) of a relation. + + Create a fresh copy (clone) of a relation. The function is logically the identity, but - in the context of a register machine allows - for terms of kind {!is_union} + in the context of a register machine allows + for terms of kind {!is_union} to perform destructive updates to the first argument. *) val is_clone : Expr.expr -> bool @@ -1019,24 +1019,24 @@ sig (** The number of fields of the constructor. *) val get_num_fields : constructor -> int - + (** The function declaration of the constructor. *) val get_constructor_decl : constructor -> FuncDecl.func_decl (** The function declaration of the tester. *) val get_tester_decl : constructor -> FuncDecl.func_decl - + (** The function declarations of the accessors *) val get_accessor_decls : constructor -> FuncDecl.func_decl list end (** Create a datatype constructor. - if the corresponding sort reference is 0, then the value in sort_refs should be an index + if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. *) val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor (** Create a datatype constructor. - if the corresponding sort reference is 0, then the value in sort_refs should be an index + if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. *) val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor @@ -1057,7 +1057,7 @@ sig (** The constructors. *) val get_constructors : Sort.sort -> FuncDecl.func_decl list - + (** The recognizers. *) val get_recognizers : Sort.sort -> FuncDecl.func_decl list @@ -1127,7 +1127,7 @@ end (** Functions to manipulate Tuple expressions *) module Tuple : sig - (** Create a new tuple sort. *) + (** Create a new tuple sort. *) val mk_sort : context -> Symbol.symbol -> Symbol.symbol list -> Sort.sort list -> Sort.sort (** The constructor function of the tuple. *) @@ -1146,7 +1146,7 @@ sig (** Integer Arithmetic *) module Integer : sig - (** Create a new integer sort. *) + (** Create a new integer sort. *) val mk_sort : context -> Sort.sort (** Retrieve the int value. *) @@ -1158,7 +1158,7 @@ sig (** Returns a string representation of a numeral. *) val numeral_to_string : Expr.expr -> string - (** Creates an integer constant. *) + (** Creates an integer constant. *) val mk_const : context -> Symbol.symbol -> Expr.expr (** Creates an integer constant. *) @@ -1179,21 +1179,21 @@ sig @return A Term with the given value and sort Integer *) val mk_numeral_i : context -> int -> Expr.expr - (** Coerce an integer to a real. - + (** Coerce an integer to a real. + There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard. - + You can take the floor of a real by creating an auxiliary integer Term [k] and and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1]. The argument must be of integer sort. *) val mk_int2real : context -> Expr.expr -> Expr.expr - (** Create an n-bit bit-vector from an integer argument. - - NB. This function is essentially treated as uninterpreted. + (** Create an n-bit bit-vector from an integer argument. + + NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function. - + The argument must be of integer sort. *) val mk_int2bv : context -> int -> Expr.expr -> Expr.expr end @@ -1201,7 +1201,7 @@ sig (** Real Arithmetic *) module Real : sig - (** Create a real sort. *) + (** Create a real sort. *) val mk_sort : context -> Sort.sort (** The numerator of a rational numeral. *) @@ -1213,7 +1213,7 @@ sig (** Get a ratio from a real numeral *) val get_ratio : Expr.expr -> Ratio.ratio - (** Returns a string representation in decimal notation. + (** Returns a string representation in decimal notation. The result has at most as many decimal places as indicated by the int argument.*) val to_decimal_string : Expr.expr-> int -> string @@ -1226,7 +1226,7 @@ sig (** Creates a real constant. *) val mk_const_s : context -> string -> Expr.expr - (** Create a real numeral from a fraction. + (** Create a real numeral from a fraction. @return A Term with rational value and sort Real {!mk_numeral_s} *) val mk_numeral_nd : context -> int -> int -> Expr.expr @@ -1247,26 +1247,26 @@ sig The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort. *) val mk_real2int : context -> Expr.expr -> Expr.expr - + (** Algebraic Numbers *) module AlgebraicNumber : sig - (** Return a upper bound for a given real algebraic number. + (** Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^precision. - {!is_algebraic_number} + {!is_algebraic_number} @return A numeral Expr of sort Real *) val to_upper : Expr.expr -> int -> Expr.expr - - (** Return a lower bound for the given real algebraic number. + + (** Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. {!is_algebraic_number} @return A numeral Expr of sort Real *) val to_lower : Expr.expr -> int -> Expr.expr - - (** Returns a string representation in decimal notation. + + (** Returns a string representation in decimal notation. The result has at most as many decimal places as the int argument provided.*) val to_decimal_string : Expr.expr -> int -> string - + (** Returns a string representation of a numeral. *) val numeral_to_string : Expr.expr -> string end @@ -1335,34 +1335,34 @@ sig (** Indicates whether the term is an algebraic number *) val is_algebraic_number : Expr.expr -> bool - (** Create an expression representing [t[0] + t[1] + ...]. *) + (** Create an expression representing [t[0] + t[1] + ...]. *) val mk_add : context -> Expr.expr list -> Expr.expr - (** Create an expression representing [t[0] * t[1] * ...]. *) + (** Create an expression representing [t[0] * t[1] * ...]. *) val mk_mul : context -> Expr.expr list -> Expr.expr - (** Create an expression representing [t[0] - t[1] - ...]. *) + (** Create an expression representing [t[0] - t[1] - ...]. *) val mk_sub : context -> Expr.expr list -> Expr.expr - (** Create an expression representing [-t]. *) + (** Create an expression representing [-t]. *) val mk_unary_minus : context -> Expr.expr -> Expr.expr - (** Create an expression representing [t1 / t2]. *) + (** Create an expression representing [t1 / t2]. *) val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Create an expression representing [t1 ^ t2]. *) + (** Create an expression representing [t1 ^ t2]. *) val mk_power : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Create an expression representing [t1 < t2] *) + (** Create an expression representing [t1 < t2] *) val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Create an expression representing [t1 <= t2] *) + (** Create an expression representing [t1 <= t2] *) val mk_le : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Create an expression representing [t1 > t2] *) + (** Create an expression representing [t1 > t2] *) val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Create an expression representing [t1 >= t2] *) + (** Create an expression representing [t1 >= t2] *) val mk_ge : context -> Expr.expr -> Expr.expr -> Expr.expr end @@ -1517,22 +1517,22 @@ sig (** Indicates whether the term is a bit-vector rotate right (extended) Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. *) val is_bv_rotaterightextended : Expr.expr -> bool - + (** Indicates whether the term is a coercion from bit-vector to integer - This function is not supported by the decision procedures. Only the most + This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function. *) val is_int2bv : Expr.expr -> bool (** Indicates whether the term is a coercion from integer to bit-vector - This function is not supported by the decision procedures. Only the most + This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function. *) val is_bv2int : Expr.expr -> bool (** Indicates whether the term is a bit-vector carry - Compute the carry bit in a full-adder. The meaning is given by the + Compute the carry bit in a full-adder. The meaning is given by the equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) *) val is_bv_carry : Expr.expr -> bool - + (** Indicates whether the term is a bit-vector ternary XOR The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) *) val is_bv_xor3 : Expr.expr -> bool @@ -1542,7 +1542,7 @@ sig (** Retrieve the int value. *) val get_int : Expr.expr -> int - + (** Returns a string representation of a numeral. *) val numeral_to_string : Expr.expr -> string @@ -1605,7 +1605,7 @@ sig val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr (** Unsigned division. - + It is defined as the floor of [t1/t2] if \c t2 is different from zero. If [t2] is zero, then the result is undefined. @@ -1613,7 +1613,7 @@ sig val mk_udiv : context -> Expr.expr -> Expr.expr -> Expr.expr (** Signed division. - + It is defined in the following way: - The \c floor of [t1/t2] if \c t2 is different from zero, and [t1*t2 >= 0]. @@ -1625,14 +1625,14 @@ sig val mk_sdiv : context -> Expr.expr -> Expr.expr -> Expr.expr (** Unsigned remainder. - - It is defined as [t1 - (t1 /u t2) * t2], where [/u] represents unsigned division. + + It is defined as [t1 - (t1 /u t2) * t2], where [/u] represents unsigned division. If [t2] is zero, then the result is undefined. The arguments must have the same bit-vector sort. *) val mk_urem : context -> Expr.expr -> Expr.expr -> Expr.expr (** Signed remainder. - + It is defined as [t1 - (t1 /s t2) * t2], where [/s] represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of \c t1. @@ -1641,63 +1641,63 @@ sig val mk_srem : context -> Expr.expr -> Expr.expr -> Expr.expr (** Two's complement signed remainder (sign follows divisor). - + If [t2] is zero, then the result is undefined. The arguments must have the same bit-vector sort. *) val mk_smod : context -> Expr.expr -> Expr.expr -> Expr.expr (** Unsigned less-than - + The arguments must have the same bit-vector sort. *) val mk_ult : context -> Expr.expr -> Expr.expr -> Expr.expr (** Two's complement signed less-than - + The arguments must have the same bit-vector sort. *) val mk_slt : context -> Expr.expr -> Expr.expr -> Expr.expr (** Unsigned less-than or equal to. - + The arguments must have the same bit-vector sort. *) val mk_ule : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Two's complement signed less-than or equal to. - + The arguments must have the same bit-vector sort. *) val mk_sle : context -> Expr.expr -> Expr.expr -> Expr.expr (** Unsigned greater than or equal to. - + The arguments must have the same bit-vector sort. *) val mk_uge : context -> Expr.expr -> Expr.expr -> Expr.expr (** Two's complement signed greater than or equal to. - + The arguments must have the same bit-vector sort. *) val mk_sge : context -> Expr.expr -> Expr.expr -> Expr.expr (** Unsigned greater-than. - + The arguments must have the same bit-vector sort. *) val mk_ugt : context -> Expr.expr -> Expr.expr -> Expr.expr (** Two's complement signed greater-than. - + The arguments must have the same bit-vector sort. *) val mk_sgt : context -> Expr.expr -> Expr.expr -> Expr.expr (** Bit-vector concatenation. - + The arguments must have a bit-vector sort. - @return - The result is a bit-vector of size [n1+n2], where [n1] ([n2]) + @return + The result is a bit-vector of size [n1+n2], where [n1] ([n2]) is the size of [t1] ([t2]). *) val mk_concat : context -> Expr.expr -> Expr.expr -> Expr.expr (** Bit-vector extraction. - + Extract the bits between two limits from a bitvector of - size [m] to yield a new bitvector of size [n], where + size [m] to yield a new bitvector of size [n], where [n = high - low + 1]. *) val mk_extract : context -> int -> int -> Expr.expr -> Expr.expr @@ -1713,38 +1713,38 @@ sig bitvector of size [m+i], where \c m is the size of the given bit-vector. *) val mk_zero_ext : context -> int -> Expr.expr -> Expr.expr - + (** Bit-vector repetition. *) val mk_repeat : context -> int -> Expr.expr -> Expr.expr (** Shift left. It is equivalent to multiplication by [2^x] where \c x is the value of third argument. - - NB. The semantics of shift operations varies between environments. This - definition does not necessarily capture directly the semantics of the + + NB. The semantics of shift operations varies between environments. This + definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.*) val mk_shl : context -> Expr.expr -> Expr.expr -> Expr.expr (** Logical shift right - + It is equivalent to unsigned division by [2^x] where \c x is the value of the third argument. - NB. The semantics of shift operations varies between environments. This - definition does not necessarily capture directly the semantics of the + NB. The semantics of shift operations varies between environments. This + definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling. The arguments must have a bit-vector sort. *) val mk_lshr : context -> Expr.expr -> Expr.expr -> Expr.expr (** Arithmetic shift right - + It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument. - NB. The semantics of shift operations varies between environments. This - definition does not necessarily capture directly the semantics of the + NB. The semantics of shift operations varies between environments. This + definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling. The arguments must have a bit-vector sort. *) @@ -1754,70 +1754,70 @@ sig Rotate bits of \c t to the left \c i times. *) val mk_rotate_left : context -> int -> Expr.expr -> Expr.expr - (** Rotate Right. + (** Rotate Right. Rotate bits of \c t to the right \c i times.*) val mk_rotate_right : context -> int -> Expr.expr -> Expr.expr - (** Rotate Left. + (** Rotate Left. Rotate bits of the second argument to the left.*) val mk_ext_rotate_left : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Rotate Right. + (** Rotate Right. Rotate bits of the second argument to the right. *) val mk_ext_rotate_right : context -> Expr.expr -> Expr.expr -> Expr.expr - (** Create an integer from the bit-vector argument - - If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. - So the result is non-negative and in the range [[0..2^N-1]], where + (** Create an integer from the bit-vector argument + + If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. + So the result is non-negative and in the range [[0..2^N-1]], where N are the number of bits in the argument. If \c is_signed is true, \c t1 is treated as a signed bit-vector. - - NB. This function is essentially treated as uninterpreted. + + NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.*) val mk_bv2int : context -> Expr.expr -> bool -> Expr.expr - + (** Create a predicate that checks that the bit-wise addition does not overflow. - + The arguments must be of bit-vector sort. *) val mk_add_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr (** Create a predicate that checks that the bit-wise addition does not underflow. - + The arguments must be of bit-vector sort. *) val mk_add_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create a predicate that checks that the bit-wise subtraction does not overflow. - + The arguments must be of bit-vector sort. *) val mk_sub_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create a predicate that checks that the bit-wise subtraction does not underflow. - + The arguments must be of bit-vector sort. *) val mk_sub_no_underflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr (** Create a predicate that checks that the bit-wise signed division does not overflow. - + The arguments must be of bit-vector sort. *) val mk_sdiv_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr (** Create a predicate that checks that the bit-wise negation does not overflow. - - The arguments must be of bit-vector sort. *) + + The arguments must be of bit-vector sort. *) val mk_neg_no_overflow : context -> Expr.expr -> Expr.expr (** Create a predicate that checks that the bit-wise multiplication does not overflow. - + The arguments must be of bit-vector sort. *) val mk_mul_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr (** Create a predicate that checks that the bit-wise multiplication does not underflow. - + The arguments must be of bit-vector sort. *) val mk_mul_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Create a bit-vector numeral. *) val mk_numeral : context -> string -> int -> Expr.expr end @@ -1826,7 +1826,7 @@ end module FloatingPoint : sig - (** Rounding Modes *) + (** Rounding Modes *) module RoundingMode : sig (** Create the RoundingMode sort. *) @@ -1837,47 +1837,47 @@ sig (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) val mk_round_nearest_ties_to_even : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) val mk_rne : context -> Expr.expr (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) val mk_round_nearest_ties_to_away : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) val mk_rna : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) val mk_round_toward_positive : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) val mk_rtp : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) val mk_round_toward_negative : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) val mk_rtn : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) val mk_round_toward_zero : context -> Expr.expr - + (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) val mk_rtz : context -> Expr.expr end (** Create a FloatingPoint sort. *) val mk_sort : context -> int -> int -> Sort.sort - - (** Create the half-precision (16-bit) FloatingPoint sort.*) + + (** Create the half-precision (16-bit) FloatingPoint sort.*) val mk_sort_half : context -> Sort.sort - + (** Create the half-precision (16-bit) FloatingPoint sort. *) val mk_sort_16 : context -> Sort.sort (** Create the single-precision (32-bit) FloatingPoint sort.*) val mk_sort_single : context -> Sort.sort - + (** Create the single-precision (32-bit) FloatingPoint sort. *) val mk_sort_32 : context -> Sort.sort @@ -1886,7 +1886,7 @@ sig (** Create the double-precision (64-bit) FloatingPoint sort. *) val mk_sort_64 : context -> Sort.sort - + (** Create the quadruple-precision (128-bit) FloatingPoint sort. *) val mk_sort_quadruple : context -> Sort.sort @@ -1902,11 +1902,11 @@ sig (** Create a floating-point zero of a given FloatingPoint sort. *) val mk_zero : context -> Sort.sort -> bool -> Expr.expr - (** Create an expression of FloatingPoint sort from three bit-vector expressions. + (** Create an expression of FloatingPoint sort from three bit-vector expressions. This is the operator named `fp' in the SMT FP theory definition. - Note that \c sign is required to be a bit-vector of size 1. Significand and exponent - are required to be greater than 1 and 2 respectively. The FloatingPoint sort + Note that \c sign is required to be a bit-vector of size 1. Significand and exponent + are required to be greater than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. *) val mk_fp : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr @@ -1919,16 +1919,16 @@ sig (** Create a numeral of FloatingPoint sort from a signed integer. *) val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr - + (** Create a numeral of FloatingPoint sort from a sign bit and two integers. *) val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr (** Create a numeral of FloatingPoint sort from a string *) val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr - + (** Indicates whether the terms is of floating-point sort. *) val is_fp : Expr.expr -> bool - + (** Indicates whether an expression is a floating-point abs expression *) val is_abs : Expr.expr -> bool @@ -1938,7 +1938,7 @@ sig (** Indicates whether an expression is a floating-point add expression *) val is_add : Expr.expr -> bool - + (** Indicates whether an expression is a floating-point sub expression *) val is_sub : Expr.expr -> bool @@ -1995,7 +1995,7 @@ sig (** Indicates whether an expression is a floating-point is_nan expression *) val is_is_nan : Expr.expr -> bool - + (** Indicates whether an expression is a floating-point is_negative expression *) val is_is_negative : Expr.expr -> bool @@ -2050,16 +2050,16 @@ sig (** Floating-point fused multiply-add. *) val mk_fma : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point square root *) val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr (** Floating-point remainder *) val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr - - (** Floating-point roundToIntegral. - Rounds a floating-point number to the closest integer, + (** Floating-point roundToIntegral. + + Rounds a floating-point number to the closest integer, again represented as a floating-point number. *) val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr @@ -2068,16 +2068,16 @@ sig (** Maximum of floating-point numbers. *) val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point less than or equal. *) val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point less than. *) val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr (** Floating-point greater than or equal. *) val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr - + (** Floating-point greater than. *) val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr @@ -2122,27 +2122,27 @@ sig (** C1onversion of a floating-point term into an unsigned bit-vector. *) val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr - + (** Conversion of a floating-point term into a signed bit-vector. *) val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr (** Conversion of a floating-point term into a real-numbered term. *) val mk_to_real : context -> Expr.expr -> Expr.expr - + (** Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. *) val get_ebits : context -> Sort.sort -> int (** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *) val get_sbits : context -> Sort.sort -> int - + (** Retrieves the sign of a floating-point literal. *) val get_numeral_sign : context -> Expr.expr -> bool * int (** Return the significand value of a floating-point numeral as a string. *) val get_numeral_significand_string : context -> Expr.expr -> string - (** Return the significand value of a floating-point numeral as a uint64. - Remark: This function extracts the significand bits, without the + (** Return the significand value of a floating-point numeral as a uint64. + Remark: This function extracts the significand bits, without the hidden bit or normalization. Throws an exception if the significand does not fit into a uint64. *) val get_numeral_significand_uint : context -> Expr.expr -> bool * int @@ -2152,7 +2152,7 @@ sig (** Return the exponent value of a floating-point numeral as a signed integer *) val get_numeral_exponent_int : context -> Expr.expr -> bool * int - + (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr @@ -2176,13 +2176,13 @@ sig (** Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. *) val is_goal : Expr.expr -> bool - (** Indicates whether the term is a binary equivalence modulo namings. + (** Indicates whether the term is a binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings. *) val is_oeq : Expr.expr -> bool (** Indicates whether the term is proof via modus ponens - + Given a proof for p and a proof for (implies p q), produces a proof for q. T1: p T2: (implies p q) @@ -2191,14 +2191,14 @@ sig val is_modus_ponens : Expr.expr -> bool (** Indicates whether the term is a proof for (R t t), where R is a reflexive relation. - This proof object has no antecedents. - The only reflexive relations that are used are + This proof object has no antecedents. + The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'. *) val is_reflexivity : Expr.expr -> bool (** Indicates whether the term is proof by symmetricity of a relation - + Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) @@ -2206,51 +2206,51 @@ sig val is_symmetry : Expr.expr -> bool (** Indicates whether the term is a proof by transitivity of a relation - - Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof - for (R t u). + + Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof + for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: (R t u) *) val is_transitivity : Expr.expr -> bool (** Indicates whether the term is a proof by condensed transitivity of a relation - + Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. - It combines several symmetry and transitivity proofs. + It combines several symmetry and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) - [trans* T1 T2 T3]: (R a d) + [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation. - + Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) - using the antecedents, symmetry and transitivity. That is, + using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b. *) val is_Transitivity_star : Expr.expr -> bool (** Indicates whether the term is a monotonicity proof object. - + T1: (R t_1 s_1) ... Tn: (R t_n s_n) - [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) + [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are supressed to save space. *) val is_monotonicity : Expr.expr -> bool - (** Indicates whether the term is a quant-intro proof - + (** Indicates whether the term is a quant-intro proof + Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) *) val is_quant_intro : Expr.expr -> bool - (** Indicates whether the term is a distributivity proof object. - + (** Indicates whether the term is a distributivity proof object. + Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) @@ -2258,36 +2258,36 @@ sig (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments. - + This proof object has no antecedents. - Remark. This rule is used by the CNF conversion pass and + Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and. *) val is_distributivity : Expr.expr -> bool (** Indicates whether the term is a proof by elimination of AND - + Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and l_1 ... l_n) [and-elim T1]: l_i *) val is_and_elimination : Expr.expr -> bool (** Indicates whether the term is a proof by eliminiation of not-or - + Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) *) val is_or_elimination : Expr.expr -> bool (** Indicates whether the term is a proof by rewriting - + A proof for a local rewriting step (= t s). The head function symbol of t is interpreted. - + This proof object has no antecedents. - The conclusion of a rewrite rule is either an equality (= t s), + The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff. - + Examples: (= (+ ( x : expr ) 0) x) (= (+ ( x : expr ) 1 2) (+ 3 x)) @@ -2295,7 +2295,7 @@ sig val is_rewrite : Expr.expr -> bool (** Indicates whether the term is a proof by rewriting - + A proof for rewriting an expression t into an expression s. This proof object is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. @@ -2308,49 +2308,49 @@ sig val is_rewrite_star : Expr.expr -> bool (** Indicates whether the term is a proof for pulling quantifiers out. - + A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *) val is_pull_quant : Expr.expr -> bool (** Indicates whether the term is a proof for pulling quantifiers out. - - A proof for (iff P Q) where Q is in prenex normal form. - This proof object is only used if the parameter PROOF_MODE is 1. + + A proof for (iff P Q) where Q is in prenex normal form. + This proof object is only used if the parameter PROOF_MODE is 1. This proof object has no antecedents *) val is_pull_quant_star : Expr.expr -> bool (** Indicates whether the term is a proof for pushing quantifiers in. - + A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) - ... - (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) + ... + (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no antecedents *) val is_push_quant : Expr.expr -> bool (** Indicates whether the term is a proof for elimination of unused variables. - + A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) - (forall (x_1 ... x_n) p[x_1 ... x_n])) - + (forall (x_1 ... x_n) p[x_1 ... x_n])) + It is used to justify the elimination of unused variables. This proof object has no antecedents. *) val is_elim_unused_vars : Expr.expr -> bool (** Indicates whether the term is a proof for destructive equality resolution - + A proof for destructive equality resolution: (iff (forall (x) (or (not (= ( x : expr ) t)) P[x])) P[t]) if ( x : expr ) does not occur in t. - + This proof object has no antecedents. - + Several variables can be eliminated simultaneously. *) val is_der : Expr.expr -> bool - + (** Indicates whether the term is a proof for quantifier instantiation - + A proof of (or (not (forall (x) (P x))) (P a)) *) val is_quant_inst : Expr.expr -> bool @@ -2359,17 +2359,17 @@ sig val is_hypothesis : Expr.expr -> bool (** Indicates whether the term is a proof by lemma - + T1: false [lemma T1]: (or (not l_1) ... (not l_n)) - + This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n. *) val is_lemma : Expr.expr -> bool (** Indicates whether the term is a proof by unit resolution - + T1: (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... @@ -2378,31 +2378,31 @@ sig val is_unit_resolution : Expr.expr -> bool (** Indicates whether the term is a proof by iff-true - + T1: p [iff-true T1]: (iff p true) *) val is_iff_true : Expr.expr -> bool (** Indicates whether the term is a proof by iff-false - + T1: (not p) [iff-false T1]: (iff p false) *) val is_iff_false : Expr.expr -> bool (** Indicates whether the term is a proof by commutativity - + [comm]: (= (f a b) (f b a)) - + f is a commutative operator. - + This proof object has no antecedents. Remark: if f is bool, then = is iff. *) val is_commutativity : Expr.expr -> bool (** Indicates whether the term is a proof for Tseitin-like axioms - + Proof object used to justify Tseitin's like axioms: - + (or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) @@ -2423,7 +2423,7 @@ sig (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a) - + This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. @@ -2433,56 +2433,56 @@ sig val is_def_axiom : Expr.expr -> bool (** Indicates whether the term is a proof for introduction of a name - + Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are: - + When e is of Boolean type: [def-intro]: (and (or n (not e)) (or (not n) e)) - + or: [def-intro]: (or (not n) e) when e only occurs positively. - + When e is of the form (ite cond th el): [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el))) - + Otherwise: [def-intro]: (= n e) *) val is_def_intro : Expr.expr -> bool (** Indicates whether the term is a proof for application of a definition - + [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F. *) val is_apply_def : Expr.expr -> bool (** Indicates whether the term is a proof iff-oeq - + T1: (iff p q) [iff~ T1]: (~ p q) *) val is_iff_oeq : Expr.expr -> bool (** Indicates whether the term is a proof for a positive NNF step - + Proof for a (positive) NNF step. Example: - + T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) (and (or r_1 r_2') (or r_1' r_2))) - + The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: (a) When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example - T1: q ~ q_new + T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new)) - + (b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. @@ -2491,9 +2491,9 @@ sig val is_nnf_pos : Expr.expr -> bool (** Indicates whether the term is a proof for a negative NNF step - + Proof for a (negative) NNF step. Examples: - + T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n @@ -2513,33 +2513,33 @@ sig val is_nnf_neg : Expr.expr -> bool (** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. - + A proof for (~ P Q) where Q is in negation normal form. - - This proof object is only used if the parameter PROOF_MODE is 1. - + + This proof object is only used if the parameter PROOF_MODE is 1. + This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *) val is_nnf_star : Expr.expr -> bool (** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. - + A proof for (~ P Q) where Q is in conjunctive normal form. - This proof object is only used if the parameter PROOF_MODE is 1. + This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *) val is_cnf_star : Expr.expr -> bool (** Indicates whether the term is a proof for a Skolemization step - - Proof for: - + + Proof for: + [sk]: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y))) [sk]: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y)) - + This proof object has no antecedents. *) val is_skolemize : Expr.expr -> bool (** Indicates whether the term is a proof by modus ponens for equi-satisfiability. - + Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q) @@ -2547,32 +2547,32 @@ sig val is_modus_ponens_oeq : Expr.expr -> bool (** Indicates whether the term is a proof for theory lemma - + Generic proof for theory lemmas. - + The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for - checking the theory lemma. + checking the theory lemma. The hints for arithmetic are: - farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. - - triangle-eq - Indicates a lemma related to the equivalence: + - triangle-eq - Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. *) val is_theory_lemma : Expr.expr -> bool end -(** Goals +(** Goals - A goal (aka problem). A goal is essentially a + A goal (aka problem). A goal is essentially a of formulas, that can be solved and/or transformed using tactics and solvers. *) module Goal : sig - type goal + type goal - (** The precision of the goal. + (** The precision of the goal. Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. @@ -2593,11 +2593,11 @@ sig (** Adds the constraints to the given goal. *) val add : goal -> Expr.expr list -> unit - + (** Indicates whether the goal contains `false'. *) val is_inconsistent : goal -> bool - - (** The depth of the goal. + + (** The depth of the goal. This tracks how many transformations were applied to it. *) val get_depth : goal -> int @@ -2626,8 +2626,8 @@ sig val simplify : goal -> Params.params option -> goal (** Creates a new Goal. - - Note that the Context must have been created with proof generation support if + + Note that the Context must have been created with proof generation support if the fourth argument is set to true here. *) val mk_goal : context -> bool -> bool -> bool -> goal @@ -2643,25 +2643,25 @@ end A Model contains interpretations (assignments) of constants and functions. *) module Model : sig - type model + type model - (** Function interpretations + (** Function interpretations A function interpretation is represented as a finite map and an 'else'. - Each entry in the finite map represents the value of a function given a set of arguments. *) + Each entry in the finite map represents the value of a function given a set of arguments. *) module FuncInterp : sig - type func_interp - - (** Function interpretations entries + type func_interp - An Entry object represents an element in the finite map used to a function interpretation. *) + (** Function interpretations entries + + An Entry object represents an element in the finite map used to a function interpretation. *) module FuncEntry : sig - type func_entry + type func_entry (** Return the (symbolic) value of this entry. - *) + *) val get_value : func_entry -> Expr.expr (** The number of arguments of the entry. @@ -2689,26 +2689,26 @@ sig (** The arity of the function interpretation *) val get_arity : func_interp -> int - (** A string representation of the function interpretation. *) + (** A string representation of the function interpretation. *) val to_string : func_interp -> string end - (** Retrieves the interpretation (the assignment) of a func_decl in the model. + (** Retrieves the interpretation (the assignment) of a func_decl in the model. @return An expression if the function has an interpretation in the model, null otherwise. *) val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option - (** Retrieves the interpretation (the assignment) of an expression in the model. + (** Retrieves the interpretation (the assignment) of an expression in the model. @return An expression if the constant has an interpretation in the model, null otherwise. *) val get_const_interp_e : model -> Expr.expr -> Expr.expr option - (** Retrieves the interpretation (the assignment) of a non-constant func_decl in the model. + (** Retrieves the interpretation (the assignment) of a non-constant func_decl in the model. @return A FunctionInterpretation if the function has an interpretation in the model, null otherwise. *) val get_func_interp : model -> FuncDecl.func_decl -> FuncInterp.func_interp option (** The number of constant interpretations in the model. *) val get_num_consts : model -> int - (** The function declarations of the constants in the model. *) + (** The function declarations of the constants in the model. *) val get_const_decls : model -> FuncDecl.func_decl list (** The number of function interpretations in the model. *) @@ -2721,8 +2721,8 @@ sig val get_decls : model -> FuncDecl.func_decl list (** Evaluates an expression in the current model. - - This function may fail if the argument contains quantifiers, + + This function may fail if the argument contains quantifiers, is partial (MODEL_PARTIAL enabled), or if it is not well-sorted. In this case a [ModelEvaluationFailedException] is thrown. *) @@ -2734,8 +2734,8 @@ sig (** The number of uninterpreted sorts that the model has an interpretation for. *) val get_num_sorts : model -> int - (** The uninterpreted sorts that the model has an interpretation for. - + (** The uninterpreted sorts that the model has an interpretation for. + Z3 also provides an intepretation for uninterpreted sorts used in a formula. The interpretation for a sort is a finite set of distinct values. We say this finite set is the "universe" of the sort. @@ -2743,17 +2743,17 @@ sig {!sort_universe} *) val get_sorts : model -> Sort.sort list - (** The finite set of distinct values that represent the interpretation of a sort. + (** The finite set of distinct values that represent the interpretation of a sort. {!get_sorts} @return A list of expressions, where each is an element of the universe of the sort *) val sort_universe : model -> Sort.sort -> Expr.expr list - - (** Conversion of models to strings. + + (** Conversion of models to strings. @return A string representation of the model. *) val to_string : model -> string end -(** Probes +(** Probes Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. @@ -2763,9 +2763,9 @@ end *) module Probe : sig - type probe + type probe - (** Execute the probe over the goal. + (** Execute the probe over the goal. @return A probe always produce a float value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. *) val apply : probe -> Goal.goal -> float @@ -2779,7 +2779,7 @@ sig (** Returns a string containing a description of the probe with the given name. *) val get_probe_description : context -> string -> string - (** Creates a new Probe. *) + (** Creates a new Probe. *) val mk_probe : context -> string -> probe (** Create a probe that always evaluates to a float value. *) @@ -2819,21 +2819,21 @@ end (** Tactics Tactics are the basic building block for creating custom solvers for specific problem domains. - The complete list of tactics may be obtained using [Context.get_num_tactics] + The complete list of tactics may be obtained using [Context.get_num_tactics] and [Context.get_tactic_names]. It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end. *) module Tactic : sig - type tactic + type tactic - (** Tactic application results - - ApplyResult objects represent the result of an application of a + (** Tactic application results + + ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. *) module ApplyResult : sig - type apply_result + type apply_result (** The number of Subgoals. *) val get_num_subgoals : apply_result -> int @@ -2844,8 +2844,8 @@ sig (** Retrieves a subgoal from the apply_result. *) val get_subgoal : apply_result -> int -> Goal.goal - (** Convert a model for a subgoal into a model for the original - goal [g], that the ApplyResult was obtained from. + (** Convert a model for a subgoal into a model for the original + goal [g], that the ApplyResult was obtained from. #return A model for [g] *) val convert_model : apply_result -> int -> Model.model -> Model.model @@ -2871,7 +2871,7 @@ sig (** Returns a string containing a description of the tactic with the given name. *) val get_tactic_description : context -> string -> string - (** Creates a new Tactic. *) + (** Creates a new Tactic. *) val mk_tactic : context -> string -> tactic (** Create a tactic that applies one tactic to a Goal and @@ -2882,22 +2882,22 @@ sig if it fails then returns the result of another tactic applied to the Goal. *) val or_else : context -> tactic -> tactic -> tactic - (** Create a tactic that applies one tactic to a goal for some time (in milliseconds). - + (** Create a tactic that applies one tactic to a goal for some time (in milliseconds). + If the tactic does not terminate within the timeout, then it fails. *) val try_for : context -> tactic -> int -> tactic - (** Create a tactic that applies one tactic to a given goal if the probe - evaluates to true. - + (** Create a tactic that applies one tactic to a given goal if the probe + evaluates to true. + If the probe evaluates to false, then the new tactic behaves like the [skip] tactic. *) val when_ : context -> Probe.probe -> tactic -> tactic - (** Create a tactic that applies a tactic to a given goal if the probe + (** Create a tactic that applies a tactic to a given goal if the probe evaluates to true and another tactic otherwise. *) val cond : context -> Probe.probe -> tactic -> tactic -> tactic - (** Create a tactic that keeps applying one tactic until the goal is not + (** Create a tactic that keeps applying one tactic until the goal is not modified anymore or the maximum number of iterations is reached. *) val repeat : context -> tactic -> int -> tactic @@ -2928,7 +2928,7 @@ sig to every subgoal produced by the first one. The subgoals are processed in parallel. *) val par_and_then : context -> tactic -> tactic -> tactic - (** Interrupt the execution of a Z3 procedure. + (** Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics. *) val interrupt : context -> unit end @@ -2936,37 +2936,37 @@ end (** Objects that track statistical information. *) module Statistics : sig - type statistics - + type statistics + (** Statistical data is organized into pairs of \[Key, Entry\], where every Entry is either a floating point or integer value. *) module Entry : sig type statistics_entry - + (** The key of the entry. *) val get_key : statistics_entry -> string - + (** The int-value of the entry. *) val get_int : statistics_entry -> int - + (** The float-value of the entry. *) val get_float : statistics_entry -> float - + (** True if the entry is uint-valued. *) val is_int : statistics_entry -> bool - + (** True if the entry is float-valued. *) val is_float : statistics_entry -> bool - + (** The string representation of the the entry's value. *) val to_string_value : statistics_entry -> string - + (** The string representation of the entry (key and value) *) val to_string : statistics_entry -> string end - (** A string representation of the statistical data. *) + (** A string representation of the statistical data. *) val to_string : statistics -> string (** The number of statistical data. *) @@ -2978,16 +2978,16 @@ sig (** The statistical counters. *) val get_keys : statistics -> string list - (** The value of a particular statistical counter. *) + (** The value of a particular statistical counter. *) val get : statistics -> string -> Entry.statistics_entry option end (** Solvers *) module Solver : sig - type solver + type solver type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE - + val string_of_status : status -> string (** A string that describes all available solver parameters. *) @@ -3017,7 +3017,7 @@ sig This removes all assertions from the solver. *) val reset : solver -> unit - (** Assert a constraint (or multiple) into the solver. *) + (** Assert a constraint (or multiple) into the solver. *) val add : solver -> Expr.expr list -> unit (** * Assert multiple constraints (cs) into the solver, and track them (in the @@ -3035,7 +3035,7 @@ sig (** * Assert a constraint (c) into the solver, and track it (in the unsat) core * using the Boolean constant p. - * + * * This API is an alternative to {!check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a @@ -3052,26 +3052,26 @@ sig val get_assertions : solver -> Expr.expr list (** Checks whether the assertions in the solver are consistent or not. - + {!Model} {!get_unsat_core} {!Proof} *) val check : solver -> Expr.expr list -> status (** The model of the last [Check]. - + The result is [None] if [Check] was not invoked before, if its results was not [SATISFIABLE], or if model production is not enabled. *) val get_model : solver -> Model.model option (** The proof of the last [Check]. - + The result is [null] if [Check] was not invoked before, if its results was not [UNSATISFIABLE], or if proof production is disabled. *) val get_proof : solver -> Expr.expr option (** The unsat core of the last [Check]. - + The unsat core is a subset of [Assertions] The result is empty if [Check] was not invoked before, if its results was not [UNSATISFIABLE], or if core production is disabled. *) @@ -3083,26 +3083,26 @@ sig (** Solver statistics. *) val get_statistics : solver -> Statistics.statistics - (** Creates a new (incremental) solver. - - This solver also uses a set of builtin tactics for handling the first - check-sat command, and check-sat commands that take more than a given - number of milliseconds to be solved. *) + (** Creates a new (incremental) solver. + + This solver also uses a set of builtin tactics for handling the first + check-sat command, and check-sat commands that take more than a given + number of milliseconds to be solved. *) val mk_solver : context -> Symbol.symbol option -> solver (** Creates a new (incremental) solver. - {!mk_solver} *) + {!mk_solver} *) val mk_solver_s : context -> string -> solver (** Creates a new (incremental) solver. *) val mk_simple_solver : context -> solver (** Creates a solver that is implemented using the given tactic. - + The solver supports the commands [Push] and [Pop], but it will always solve each check from scratch. *) val mk_solver_t : context -> Tactic.tactic -> solver - + (** Create a clone of the current solver with respect to a context. *) val translate : solver -> context -> solver @@ -3113,8 +3113,8 @@ end (** Fixedpoint solving *) module Fixedpoint : sig - type fixedpoint - + type fixedpoint + (** A string that describes all available fixedpoint solver parameters. *) val get_help : fixedpoint -> string @@ -3124,28 +3124,28 @@ sig (** Retrieves parameter descriptions for Fixedpoint solver. *) val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs - (** Assert a constraints into the fixedpoint solver. *) + (** Assert a constraints into the fixedpoint solver. *) val add : fixedpoint -> Expr.expr list -> unit - (** Register predicate as recursive relation. *) + (** Register predicate as recursive relation. *) val register_relation : fixedpoint -> FuncDecl.func_decl -> unit - (** Add rule into the fixedpoint solver. *) + (** Add rule into the fixedpoint solver. *) val add_rule : fixedpoint -> Expr.expr -> Symbol.symbol option -> unit - (** Add table fact to the fixedpoint solver. *) + (** Add table fact to the fixedpoint solver. *) val add_fact : fixedpoint -> FuncDecl.func_decl -> int list -> unit (** Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the recursively defined relations. The query is satisfiable if there is an instance of the query variables and a derivation for it. - The query is unsatisfiable if there are no derivations satisfying the query variables. *) + The query is unsatisfiable if there are no derivations satisfying the query variables. *) val query : fixedpoint -> Expr.expr -> Solver.status (** Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is an instance of some relation that is non-empty. - The query is unsatisfiable if there are no derivations satisfying any of the relations. *) + The query is unsatisfiable if there are no derivations satisfying any of the relations. *) val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status (** Creates a backtracking point. @@ -3158,39 +3158,39 @@ sig {!push} *) val pop : fixedpoint -> unit - (** Update named rule into in the fixedpoint solver. *) + (** Update named rule into in the fixedpoint solver. *) val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit - (** Retrieve satisfying instance or instances of solver, - or definitions for the recursive predicates that show unsatisfiability. *) + (** Retrieve satisfying instance or instances of solver, + or definitions for the recursive predicates that show unsatisfiability. *) val get_answer : fixedpoint -> Expr.expr option - (** Retrieve explanation why fixedpoint engine returned status Unknown. *) + (** Retrieve explanation why fixedpoint engine returned status Unknown. *) val get_reason_unknown : fixedpoint -> string - (** Retrieve the number of levels explored for a given predicate. *) + (** Retrieve the number of levels explored for a given predicate. *) val get_num_levels : fixedpoint -> FuncDecl.func_decl -> int - (** Retrieve the cover of a predicate. *) + (** Retrieve the cover of a predicate. *) val get_cover_delta : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr option (** Add property about the predicate. - The property is added at level. *) + The property is added at level. *) val add_cover : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr -> unit (** Retrieve internal string representation of fixedpoint object. *) val to_string : fixedpoint -> string - (** Instrument the Datalog engine on which table representation to use for recursive predicate. *) + (** Instrument the Datalog engine on which table representation to use for recursive predicate. *) val set_predicate_representation : fixedpoint -> FuncDecl.func_decl -> Symbol.symbol list -> unit - (** Convert benchmark given as set of axioms, rules and queries to a string. *) + (** Convert benchmark given as set of axioms, rules and queries to a string. *) val to_string_q : fixedpoint -> Expr.expr list -> string - (** Retrieve set of rules added to fixedpoint context. *) + (** Retrieve set of rules added to fixedpoint context. *) val get_rules : fixedpoint -> Expr.expr list - (** Retrieve set of assertions added to fixedpoint context. *) + (** Retrieve set of assertions added to fixedpoint context. *) val get_assertions : fixedpoint -> Expr.expr list (** Create a Fixedpoint context. *) @@ -3199,83 +3199,83 @@ sig (** Retrieve statistics information from the last call to #Z3_fixedpoint_query. *) val get_statistics : fixedpoint -> Statistics.statistics - (** Parse an SMT-LIB2 string with fixedpoint rules. - Add the rules to the current fixedpoint context. + (** Parse an SMT-LIB2 string with fixedpoint rules. + Add the rules to the current fixedpoint context. Return the set of queries in the string. *) val parse_string : fixedpoint -> string -> Expr.expr list - (** Parse an SMT-LIB2 file with fixedpoint rules. - Add the rules to the current fixedpoint context. + (** Parse an SMT-LIB2 file with fixedpoint rules. + Add the rules to the current fixedpoint context. Return the set of queries in the file. *) val parse_file : fixedpoint -> string -> Expr.expr list end -(** Optimization *) -module Optimize : -sig - type optimize - type handle - - (** Create a Optimize context. *) - val mk_opt : context -> optimize - - (** A string that describes all available optimize solver parameters. *) - val get_help : optimize -> string - - (** Sets the optimize solver parameters. *) - val set_parameters : optimize -> Params.params -> unit - - (** Retrieves parameter descriptions for Optimize solver. *) - val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs - - (** Assert a constraints into the optimize solver. *) - val add : optimize -> Expr.expr list -> unit - - (** Asssert a soft constraint. - Supply integer weight and string that identifies a group - of soft constraints. - *) - val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle - - (** Add maximization objective. - *) - val maximize : optimize -> Expr.expr -> handle - - (** Add minimization objective. - *) - val minimize : optimize -> Expr.expr -> handle - - (** Checks whether the assertions in the context are satisfiable and solves objectives. - *) - val check : optimize -> Solver.status - - (** Retrieve model from satisfiable context *) - val get_model : optimize -> Model.model option - - (** Retrieve lower bound in current model for handle *) - val get_lower : handle -> int -> Expr.expr - - (** Retrieve upper bound in current model for handle *) - val get_upper : handle -> int -> Expr.expr - - (** Creates a backtracking point. - {!pop} *) - val push : optimize -> unit +(** Optimization *) +module Optimize : +sig + type optimize + type handle - (** Backtrack one backtracking point. - Note that an exception is thrown if Pop is called without a corresponding [Push] - {!push} *) - val pop : optimize -> unit - - (** Retrieve explanation why optimize engine returned status Unknown. *) - val get_reason_unknown : optimize -> string - - (** Retrieve SMT-LIB string representation of optimize object. *) - val to_string : optimize -> string - - (** Retrieve statistics information from the last call to check *) - val get_statistics : optimize -> Statistics.statistics -end + (** Create a Optimize context. *) + val mk_opt : context -> optimize + + (** A string that describes all available optimize solver parameters. *) + val get_help : optimize -> string + + (** Sets the optimize solver parameters. *) + val set_parameters : optimize -> Params.params -> unit + + (** Retrieves parameter descriptions for Optimize solver. *) + val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs + + (** Assert a constraints into the optimize solver. *) + val add : optimize -> Expr.expr list -> unit + + (** Asssert a soft constraint. + Supply integer weight and string that identifies a group + of soft constraints. + *) + val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle + + (** Add maximization objective. + *) + val maximize : optimize -> Expr.expr -> handle + + (** Add minimization objective. + *) + val minimize : optimize -> Expr.expr -> handle + + (** Checks whether the assertions in the context are satisfiable and solves objectives. + *) + val check : optimize -> Solver.status + + (** Retrieve model from satisfiable context *) + val get_model : optimize -> Model.model option + + (** Retrieve lower bound in current model for handle *) + val get_lower : handle -> int -> Expr.expr + + (** Retrieve upper bound in current model for handle *) + val get_upper : handle -> int -> Expr.expr + + (** Creates a backtracking point. + {!pop} *) + val push : optimize -> unit + + (** Backtrack one backtracking point. + Note that an exception is thrown if Pop is called without a corresponding [Push] + {!push} *) + val pop : optimize -> unit + + (** Retrieve explanation why optimize engine returned status Unknown. *) + val get_reason_unknown : optimize -> string + + (** Retrieve SMT-LIB string representation of optimize object. *) + val to_string : optimize -> string + + (** Retrieve statistics information from the last call to check *) + val get_statistics : optimize -> Statistics.statistics +end (** Functions for handling SMT and SMT2 expressions and files *) @@ -3286,16 +3286,16 @@ sig @return A string representation of the benchmark. *) val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string - (** Parse the given string using the SMT-LIB parser. - - The symbol table of the parser can be initialized using the given sorts and declarations. - The symbols in the arrays in the third and fifth argument - don't need to match the names of the sorts and declarations in the arrays in the fourth - and sixth argument. This is a useful feature since we can use arbitrary names to + (** Parse the given string using the SMT-LIB parser. + + The symbol table of the parser can be initialized using the given sorts and declarations. + The symbols in the arrays in the third and fifth argument + don't need to match the names of the sorts and declarations in the arrays in the fourth + and sixth argument. This is a useful feature since we can use arbitrary names to reference sorts and declarations. *) val parse_smtlib_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit - (** Parse the given file using the SMT-LIB parser. + (** Parse the given file using the SMT-LIB parser. {!parse_smtlib_string} *) val parse_smtlib_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit @@ -3323,13 +3323,13 @@ sig (** The sort declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *) val get_smtlib_sorts : context -> Sort.sort list - (** Parse the given string using the SMT-LIB2 parser. + (** Parse the given string using the SMT-LIB2 parser. {!parse_smtlib_string} @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *) val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr - (** Parse the given file using the SMT-LIB2 parser. + (** Parse the given file using the SMT-LIB2 parser. {!parse_smtlib2_string} *) val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr end @@ -3341,7 +3341,7 @@ sig (** Create an AST node marking a formula position for interpolation. The expression must have Boolean sort. *) val mk_interpolant : context -> Expr.expr -> Expr.expr - + (** The interpolation context is suitable for generation of interpolants. For more information on interpolation please refer too the C/C++ API, which is well documented. *) @@ -3361,12 +3361,12 @@ sig For more information on interpolation please refer too the C/C++ API, which is well documented. *) val get_interpolation_profile : context -> string - + (** Read an interpolation problem from file. For more information on interpolation please refer too the C/C++ API, which is well documented. *) val read_interpolation_problem : context -> string -> (Expr.expr list * int list * Expr.expr list) - + (** Check the correctness of an interpolant. For more information on interpolation please refer too the C/C++ API, which is well documented. *) @@ -3381,10 +3381,10 @@ sig end (** Set a global (or module) parameter, which is shared by all Z3 contexts. - + When a Z3 module is initialized it will use the value of these parameters when Z3_params objects are not provided. - The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. + The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. The character '.' is a delimiter (more later). The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". @@ -3397,7 +3397,7 @@ end val set_global_param : string -> string -> unit (** Get a global (or module) parameter. - + Returns None if the parameter does not exist. The caller must invoke #Z3_global_param_del_value to delete the value returned at param_value. This function cannot be invoked simultaneously from different threads without synchronization. @@ -3406,32 +3406,29 @@ val set_global_param : string -> string -> unit val get_global_param : string -> string option (** Restore the value of all global (and module) parameters. - + This command will not affect already created objects (such as tactics and solvers) {!set_global_param} *) val global_param_reset_all : unit -> unit - + (** Enable/disable printing of warning messages to the console. - - Note that this function is static and effects the behaviour of + + Note that this function is static and effects the behaviour of all contexts globally. *) val toggle_warning_messages : bool -> unit (** Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode. - - Remarks: It is a NOOP otherwise. + + Remarks: It is a NOOP otherwise. *) val enable_trace : string -> unit (** - Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode. + Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode. Remarks: It is a NOOP otherwise. *) val disable_trace : string -> unit - - - diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index c726d967f..5fe0da62c 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -63,6 +63,14 @@ static struct custom_operations default_custom_ops = { custom_compare_ext_default, }; +inline int compare_pointers(void* pt1, void* pt2) { + if (pt1 == pt2) + return 0; + else if ((intnat)pt1 < (intnat)pt2) + return -1; + else + return +1; +} #define MK_CTX_OF(X) \ CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \ @@ -150,14 +158,32 @@ void Z3_context_finalize(value v) { try_to_delete_context(cp); } +int Z3_context_compare(value v1, value v2) { + Z3_context_plus cp1 = *(Z3_context_plus*)Data_custom_val(v1); + Z3_context_plus cp2 = *(Z3_context_plus*)Data_custom_val(v2); + return compare_pointers(cp1, cp2); +} + +int Z3_context_compare_ext(value v1, value v2) { + Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v1); + return compare_pointers(cp, (void*)Val_int(v2)); +} + +/* We use the pointer to the Z3_context_plus_data structure as + a hash value; it is unique, at least. */ +intnat Z3_context_hash(value v) { + Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v); + return (intnat)cp; +} + static struct custom_operations Z3_context_plus_custom_ops = { (char*) "Z3_context ops", Z3_context_finalize, - custom_compare_default, - custom_hash_default, + Z3_context_compare, + Z3_context_hash, custom_serialize_default, custom_deserialize_default, - custom_compare_ext_default, + Z3_context_compare_ext }; @@ -195,13 +221,21 @@ void Z3_ast_finalize(value v) { int Z3_ast_compare(value v1, value v2) { Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1); Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2); - assert(a1->cp->ctx == a2->cp->ctx); + + /* if the two ASTs belong to different contexts, we take + their contexts' addresses to order them (arbitrarily, but fixed) */ + if (a1->cp->ctx != a2->cp->ctx) + return compare_pointers(a1->cp->ctx, a2->cp->ctx); + + /* handling of NULL pointers */ if (a1->p == NULL && a2->p == NULL) return 0; if (a1->p == NULL) return -1; if (a2->p == NULL) return +1; + + /* Comparison according to AST ids. */ unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p); unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p); if (id1 == id2) @@ -275,14 +309,33 @@ MK_CTX_OF(ast) try_to_delete_context(pp->cp); \ } \ \ + int Z3_ ## X ## _compare(value v1, value v2) { \ + Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \ + Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \ + if (pp1->cp != pp2->cp) \ + return compare_pointers(pp1->cp, pp2->cp); \ + else \ + return compare_pointers(pp1->p, pp2->p); \ + } \ + \ + intnat Z3_ ## X ## _hash(value v) { \ + Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ + return (intnat)pp->p; \ + } \ + \ + int Z3_ ## X ## _compare_ext(value v1, value v2) { \ + Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \ + return compare_pointers(pp->p, (void*)Val_int(v2)); \ + } \ + \ static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ (char*) "Z3_" #X " ops", \ Z3_ ## X ## _finalize, \ - custom_compare_default, \ - custom_hash_default, \ + Z3_ ## X ## _compare, \ + Z3_ ## X ## _hash, \ custom_serialize_default, \ custom_deserialize_default, \ - custom_compare_ext_default, \ + Z3_ ## X ## _compare_ext \ }; \ \ MK_CTX_OF(X) @@ -315,14 +368,33 @@ MK_CTX_OF(ast) try_to_delete_context(pp->cp); \ } \ \ + int Z3_ ## X ## _compare(value v1, value v2) { \ + Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \ + Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \ + if (pp1->cp != pp2->cp) \ + return compare_pointers(pp1->cp, pp2->cp); \ + else \ + return compare_pointers(pp1->p, pp2->p); \ + } \ + \ + intnat Z3_ ## X ## _hash(value v) { \ + Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ + return (intnat)pp->p; \ + } \ + \ + int Z3_ ## X ## _compare_ext(value v1, value v2) { \ + Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \ + return compare_pointers(pp->p, (void*)Val_int(v2)); \ + } \ + \ static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ (char*) "Z3_" #X " ops", \ Z3_ ## X ## _finalize, \ - custom_compare_default, \ - custom_hash_default, \ + Z3_ ## X ## _compare, \ + Z3_ ## X ## _hash, \ custom_serialize_default, \ custom_deserialize_default, \ - custom_compare_ext_default, \ + Z3_ ## X ## _compare_ext \ }; \ \ MK_CTX_OF(X)