diff --git a/scripts/update_api.py b/scripts/update_api.py
index f1a06a63da7..909f324f014 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1208,9 +1208,9 @@ def mk_ml(ml_dir):
ml_native.write(s);
ml_pref.close()
- ml_native.write('module ML2C = struct\n\n')
+ ml_native.write('\n')
for name, result, params in _dotnet_decls:
- ml_native.write(' external n_%s : ' % ml_method_name(name))
+ ml_native.write('external %s : ' % ml_method_name(name))
ip = inparams(params)
op = outparams(params)
if len(ip) == 0:
@@ -1231,55 +1231,20 @@ def mk_ml(ml_dir):
ml_native.write('%s' % param2ml(p))
if len(op) > 0:
ml_native.write(')')
- ml_native.write('\n')
if len(ip) > 5:
- ml_native.write(' = "n_%s_bytecode"\n' % ml_method_name(name))
- ml_native.write(' "n_%s"\n' % ml_method_name(name))
+ ml_native.write(' = "n_%s_bytecode" "n_%s"\n' % (ml_method_name(name), ml_method_name(name)))
else:
- ml_native.write(' = "n_%s"\n' % ml_method_name(name))
- ml_native.write('\n')
- ml_native.write(' end\n\n')
-
- # Exception wrappers
- for name, result, params in _dotnet_decls:
- ip = inparams(params)
- op = outparams(params)
- ml_native.write(' let %s ' % ml_method_name(name))
-
- first = True
- i = 0
- for p in params:
- if is_in_param(p):
- if first:
- first = False
- else:
- ml_native.write(' ')
- ml_native.write('a%d' % i)
- i = i + 1
- if len(ip) == 0:
- ml_native.write('()')
- ml_native.write(' = ')
- ml_native.write('ML2C.n_%s' % (ml_method_name(name)))
- if len(ip) == 0:
- ml_native.write(' ()')
- first = True
- i = 0
- for p in params:
- if is_in_param(p):
- ml_native.write(' a%d' % i)
- i = i + 1
+ ml_native.write(' = "n_%s"\n' % ml_method_name(name))
ml_native.write('\n')
- ml_native.write('\n')
-
# null pointer helpers
for type_id in Type2Str:
type_name = Type2Str[type_id]
if ml_has_plus_type(type_name) and not type_name in ['Z3_context', 'Z3_sort', 'Z3_func_decl', 'Z3_app', 'Z3_pattern']:
ml_name = type2ml(type_id)
- ml_native.write(' external context_of_%s : %s -> context = "n_context_of_%s"\n' % (ml_name, ml_name, ml_name))
- ml_native.write(' external is_null_%s : %s -> bool = "n_is_null_%s"\n' % (ml_name, ml_name, ml_name))
- ml_native.write(' external mk_null_%s : context -> %s = "n_mk_null_%s"\n\n' % (ml_name, ml_name, ml_name))
+ ml_native.write('external context_of_%s : %s -> context = "n_context_of_%s"\n' % (ml_name, ml_name, ml_name))
+ ml_native.write('external is_null_%s : %s -> bool = "n_is_null_%s"\n' % (ml_name, ml_name, ml_name))
+ ml_native.write('external mk_null_%s : context -> %s = "n_mk_null_%s"\n\n' % (ml_name, ml_name, ml_name))
ml_native.write('(**/**)\n')
ml_native.close()
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index e6e8325727d..3a797e5d8d9 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -14,74 +14,65 @@ 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
module Version =
struct
- let major = let (x, _, _, _) = Z3native.get_version () in x
- let minor = let (_, x, _, _) = Z3native.get_version () in x
- let build = let (_, _, x, _) = Z3native.get_version () in x
- let revision = let (_, _, _, x) = Z3native.get_version () in x
+ let (major, minor, build, revision) = Z3native.get_version ()
+
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 major ^ "." ^
+ string_of_int minor ^ "." ^
+ string_of_int build ^ "." ^
+ string_of_int revision
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
-
-
module Symbol =
struct
type symbol = Z3native.symbol
- let gc (o:symbol) = (Z3native.context_of_symbol 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)
-
- 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 gc = Z3native.context_of_symbol
+
+ let kind o = symbol_kind_of_int (Z3native.get_symbol_kind (gc o) o)
+ let is_int_symbol o = kind o = INT_SYMBOL
+ let is_string_symbol o = kind o = STRING_SYMBOL
+ let get_int o = Z3native.get_symbol_int (gc o) o
+ let get_string o = Z3native.get_symbol_string (gc o) o
+ let to_string 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 = Z3native.mk_int_symbol
+ let mk_string = Z3native.mk_string_symbol
+
+ let mk_ints ctx names = List.map (mk_int ctx) names
+ let mk_strings ctx names = List.map (mk_string ctx) names
end
-
module rec AST :
sig
type ast = Z3native.ast
@@ -129,14 +120,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,24 +136,24 @@ 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
- let to_string (x:ast_vector) = Z3native.ast_vector_to_string (gc x) x
+ let to_string x = Z3native.ast_vector_to_string (gc x) x
end
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 +162,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 +215,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 +271,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,60 +284,54 @@ 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_int (x:parameter) =
- match x with
- | 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_symbol (x:parameter) =
- match x with
- | 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_ast (x:parameter) =
- match x with
- | 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_rational (x:parameter) =
- match x with
- | P_Rat(x) -> x
- | _ -> raise (Error "parameter is not a rational string")
+ 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 = function
+ | P_Int x -> x
+ | _ -> raise (Error "parameter is not an int")
+
+ let get_float = function
+ | P_Dbl x -> x
+ | _ -> raise (Error "parameter is not a float")
+
+ let get_symbol = function
+ | P_Sym x -> x
+ | _ -> raise (Error "parameter is not a symbol")
+
+ let get_sort = function
+ | P_Srt x -> x
+ | _ -> raise (Error "parameter is not a sort")
+
+ let get_ast = function
+ | P_Ast x -> x
+ | _ -> raise (Error "parameter is not an ast")
+
+ let get_func_decl = function
+ | P_Fdl x -> x
+ | _ -> raise (Error "parameter is not a func_decl")
+
+ 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) =
- Z3native.mk_func_decl ctx name (List.length domain) (Array.of_list domain) range
+ let dom_arr = Array.of_list domain in
+ Z3native.mk_func_decl ctx name (Array.length dom_arr) dom_arr range
let mk_func_decl_s (ctx:context) (name:string) (domain:Sort.sort list) (range:Sort.sort) =
mk_func_decl ctx (Symbol.mk_string ctx name) domain range
let mk_fresh_func_decl (ctx:context) (prefix:string) (domain:Sort.sort list) (range:Sort.sort) =
- Z3native.mk_fresh_func_decl ctx prefix (List.length domain) (Array.of_list domain) range
+ let dom_arr = Array.of_list domain in
+ Z3native.mk_fresh_func_decl ctx prefix (Array.length dom_arr) dom_arr range
let mk_const_decl (ctx:context) (name:Symbol.symbol) (range:Sort.sort) =
Z3native.mk_func_decl ctx name 0 [||] range
@@ -369,12 +342,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 +350,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 +360,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 +400,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)
@@ -492,63 +462,59 @@ sig
val mk_numeral_string : context -> string -> Sort.sort -> expr
val mk_numeral_int : context -> int -> Sort.sort -> expr
val equal : expr -> expr -> bool
- val apply1 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr
- val apply2 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr
- val apply3 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr
- val apply4 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr -> expr
val compare : expr -> expr -> int
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 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 ast_of_expr e = e
- let apply1 ctx f t = f ctx t
- let apply2 ctx f t1 t2 = f ctx t1 t2
- let apply3 ctx f t1 t2 t3 = f ctx t1 t2 t3
- let apply4 ctx f t1 t2 t3 t4 = f ctx t1 t2 t3 t4
+ 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 simplify (x:expr) (p:Params.params option) =
match p with
| 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 +524,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,68 +544,78 @@ 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
- let mk_iff (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_iff t1 t2
- let mk_implies (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_implies t1 t2
- let mk_xor (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_xor t1 t2
- let mk_and (ctx:context) (args:expr list) = Z3native.mk_and ctx (List.length args) (Array.of_list args)
- let mk_or (ctx:context) (args:expr list) = Z3native.mk_or ctx (List.length args) (Array.of_list args)
- let mk_eq (ctx:context) (x:expr) (y:expr) = apply2 ctx Z3native.mk_eq x y
- 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_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 mk_not = Z3native.mk_not
+ let mk_ite = Z3native.mk_ite
+ let mk_iff = Z3native.mk_iff
+ let mk_implies = Z3native.mk_implies
+ let mk_xor = Z3native.mk_xor
+
+ let mk_and ctx args =
+ let arg_arr = Array.of_list args in
+ Z3native.mk_and ctx (Array.length arg_arr) arg_arr
+
+ let mk_or ctx args =
+ let arg_arr = Array.of_list args in
+ Z3native.mk_or ctx (Array.length arg_arr) arg_arr
+
+ let mk_eq = Z3native.mk_eq
+ let mk_distinct ctx args =
+ let arg_arr = Array.of_list args in
+ Z3native.mk_distinct ctx (Array.length arg_arr) arg_arr
+
+ let get_bool_value x = lbool_of_int (Z3native.get_bool_value (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 = 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
-
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
+ let get_num_terms x = Z3native.get_pattern_num_terms (gc x) x
- let get_terms (x:pattern) =
- let n = (get_num_terms x) in
+ let get_terms x =
+ let n = get_num_terms x in
let f i = Z3native.get_pattern (gc x) x i in
mk_list f n
- let to_string (x:pattern) = Z3native.pattern_to_string (gc x) x
+ let to_string x = Z3native.pattern_to_string (gc x) x
end
let get_index (x:expr) =
@@ -648,232 +624,212 @@ struct
else
Z3native.get_index_value (gc x) x
- let is_universal (x:quantifier) = Z3native.is_quantifier_forall (gc x) x
- let is_existential (x:quantifier) = not (is_universal x)
- 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 is_universal x = Z3native.is_quantifier_forall (gc x) x
+ let is_existential x = not (is_universal x)
+ let get_weight x = Z3native.get_quantifier_weight (gc x) x
+ let get_num_patterns x = Z3native.get_quantifier_num_patterns (gc x) x
+ let get_patterns x =
+ 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_num_no_patterns x = Z3native.get_quantifier_num_no_patterns (gc x) x
- let get_no_patterns (x:quantifier) =
- let n = (get_num_patterns x) in
+ let get_no_patterns x =
+ 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_num_bound x = Z3native.get_quantifier_num_bound (gc x) x
- let get_bound_variable_names (x:quantifier) =
- let n = (get_num_bound x) in
+ let get_bound_variable_names x =
+ 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 get_bound_variable_sorts x =
+ let n = get_num_bound x in
let f i = Z3native.get_quantifier_bound_sort (gc x) x i in
mk_list f n
- let get_body (x:quantifier) = Z3native.get_quantifier_body (gc x) x
- let mk_bound (ctx:context) (index:int) (ty:Sort.sort) = Z3native.mk_bound ctx index ty
+ let get_body x = Z3native.get_quantifier_body (gc x) x
+ let mk_bound = Z3native.mk_bound
- let mk_pattern (ctx:context) (terms:expr list) =
- if (List.length terms) == 0 then
+ let mk_pattern ctx terms =
+ let terms_arr = Array.of_list terms in
+ if Array.length terms_arr = 0 then
raise (Error "Cannot create a pattern from zero terms")
else
- Z3native.mk_pattern ctx (List.length terms) (Array.of_list terms)
+ Z3native.mk_pattern ctx (Array.length terms_arr) terms_arr
- let mk_forall (ctx:context) (sorts:Sort.sort list) (names:Symbol.symbol list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) =
- if (List.length sorts) != (List.length names) then
- raise (Error "Number of sorts does not match number of names")
- else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
- Z3native.mk_quantifier ctx true
- (match weight with | None -> 1 | Some(x) -> x)
- (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
-
- 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
- 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
- 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
-
- 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
+ let _internal_mk_quantifier ~universal ctx sorts names body weight patterns nopatterns quantifier_id skolem_id =
+ let sorts_arr = Array.of_list sorts in
+ let names_arr = Array.of_list names in
+ if Array.length sorts_arr <> Array.length names_arr 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
- 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
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
-
- 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
- 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
+ let patterns_arr = Array.of_list patterns in
+ match nopatterns, quantifier_id, skolem_id with
+ | [], None, None ->
+ Z3native.mk_quantifier ctx universal
+ (match weight with | None -> 1 | Some x -> x)
+ (Array.length patterns_arr) patterns_arr
+ (Array.length sorts_arr) sorts_arr
+ names_arr body
+ | _ ->
+ let nopatterns_arr = Array.of_list nopatterns in
+ Z3native.mk_quantifier_ex ctx universal
+ (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)
+ (Array.length patterns_arr) patterns_arr
+ (Array.length nopatterns_arr) nopatterns_arr
+ (Array.length sorts_arr) sorts_arr
+ names_arr body
+
+ let _internal_mk_quantifier_const ~universal ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id =
+ let patterns_arr = Array.of_list patterns in
+ let bound_constants_arr = Array.of_list bound_constants in
+ match nopatterns, quantifier_id, skolem_id with
+ | [], None, None ->
+ Z3native.mk_quantifier_const ctx universal
+ (match weight with | None -> 1 | Some x -> x)
+ (Array.length bound_constants_arr) bound_constants_arr
+ (Array.length patterns_arr) patterns_arr
+ body
+ | _ ->
+ let nopatterns_arr = Array.of_list nopatterns in
+ Z3native.mk_quantifier_const_ex ctx universal
+ (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)
+ (Array.length bound_constants_arr) bound_constants_arr
+ (Array.length patterns_arr) patterns_arr
+ (Array.length nopatterns_arr) nopatterns_arr
+ body
+
+ let mk_forall = _internal_mk_quantifier ~universal:true
+ let mk_forall_const = _internal_mk_quantifier_const ~universal:true
+ let mk_exists = _internal_mk_quantifier ~universal:false
+ let mk_exists_const = _internal_mk_quantifier_const ~universal:false
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
+ if universal then
mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id
else
mk_exists ctx sorts names body weight patterns nopatterns quantifier_id skolem_id
let mk_quantifier (ctx:context) (universal:bool) (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 (universal) then
+ if universal then
mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id
else
mk_exists_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id
- let to_string (x:quantifier) = Expr.to_string x
+ let to_string x = Expr.to_string x
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_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)
-
- 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
-
- let mk_const (ctx:context) (name:Symbol.symbol) (domain:Sort.sort) (range:Sort.sort) =
- Expr.mk_const ctx name (mk_sort ctx domain range)
-
- let mk_const_s (ctx:context) (name:string) (domain:Sort.sort) (range:Sort.sort) =
- mk_const ctx (Symbol.mk_string ctx name) domain range
-
- let mk_select (ctx:context) (a:expr) (i:expr) = apply2 ctx Z3native.mk_select a i
- let mk_store (ctx:context) (a:expr) (i:expr) (v:expr) = apply3 ctx Z3native.mk_store a i v
- let mk_const_array (ctx:context) (domain:Sort.sort) (v:expr) = Z3native.mk_const_array ctx domain v
- let mk_map (ctx:context) (f:func_decl) (args:expr list) = Z3native.mk_map ctx f (List.length args) (Array.of_list args)
- let mk_term_array (ctx:context) (arg:expr) = apply1 ctx Z3native.mk_array_default arg
- let mk_array_ext (ctx:context) (arg1:expr) (arg2:expr) = apply2 ctx Z3native.mk_array_ext arg1 arg2
+ let mk_sort = Z3native.mk_array_sort
+ let is_store x = AST.is_app x && FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_STORE
+ let is_select x = AST.is_app x && FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_SELECT
+ let is_constant_array x = AST.is_app x && FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_CONST_ARRAY
+ let is_default_array x = AST.is_app x && FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ARRAY_DEFAULT
+ let is_array_map x = AST.is_app x && FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ARRAY_MAP
+ let is_as_array x = AST.is_app x && FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_AS_ARRAY
+
+ let is_array x =
+ 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
+
+ let get_domain x = Z3native.get_array_sort_domain (Sort.gc x) x
+ let get_range x = Z3native.get_array_sort_range (Sort.gc x) x
+
+ let mk_const ctx name domain range = Expr.mk_const ctx name (mk_sort ctx domain range)
+
+ let mk_const_s ctx name domain range = mk_const ctx (Symbol.mk_string ctx name) domain range
+
+ let mk_select = Z3native.mk_select
+ let mk_store = Z3native.mk_store
+ let mk_const_array = Z3native.mk_const_array
+
+ let mk_map ctx f args =
+ let args_arr = Array.of_list args in
+ Z3native.mk_map ctx f (Array.length args_arr) args_arr
+
+ let mk_term_array = Z3native.mk_array_default
+ let mk_array_ext = Z3native.mk_array_ext
end
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 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
- let mk_set_add (ctx:context) (set:expr) (element:expr) = apply2 ctx Z3native.mk_set_add set element
- let mk_del (ctx:context) (set:expr) (element:expr) = apply2 ctx Z3native.mk_set_del set element
- let mk_union (ctx:context) (args:expr list) = Z3native.mk_set_union ctx (List.length args) (Array.of_list args)
-
- let mk_intersection (ctx:context) (args:expr list) =
- Z3native.mk_set_intersect ctx (List.length args) (Array.of_list args)
-
- let mk_difference (ctx:context) (arg1:expr) (arg2:expr) = apply2 ctx Z3native.mk_set_difference arg1 arg2
- let mk_complement (ctx:context) (arg:expr) = apply1 ctx Z3native.mk_set_complement arg
- let mk_membership (ctx:context) (elem:expr) (set:expr) = apply2 ctx Z3native.mk_set_member elem set
- let mk_subset (ctx:context) (arg1:expr) (arg2:expr) = apply2 ctx Z3native.mk_set_subset arg1 arg2
+ let mk_sort = Z3native.mk_set_sort
+
+ 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 = Z3native.mk_empty_set
+ let mk_full = Z3native.mk_full_set
+ let mk_set_add = Z3native.mk_set_add
+ let mk_del = Z3native.mk_set_del
+ let mk_union ctx args =
+ let args_arr = Array.of_list args in
+ Z3native.mk_set_union ctx (Array.length args_arr) args_arr
+
+ let mk_intersection ctx args =
+ let args_arr = Array.of_list args in
+ Z3native.mk_set_intersect ctx (Array.length args_arr) args_arr
+
+ let mk_difference = Z3native.mk_set_difference
+ let mk_complement = Z3native.mk_set_complement
+ let mk_membership = Z3native.mk_set_member
+ let mk_subset = Z3native.mk_set_subset
end
module FiniteDomain =
struct
- let mk_sort (ctx:context) (name:Symbol.symbol) (size:int) = Z3native.mk_finite_domain_sort ctx name size
- let mk_sort_s (ctx:context) (name:string) (size:int) = mk_sort ctx (Symbol.mk_string ctx name) size
+ let mk_sort = Z3native.mk_finite_domain_sort
+ let mk_sort_s ctx name size = mk_sort ctx (Symbol.mk_string ctx name) size
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)
+ 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
- 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
- if r then v
- else raise (Error "Conversion failed.")
+ let get_size x =
+ match Z3native.get_finite_domain_sort_size (Sort.gc x) x with
+ | true, v -> v
+ | false, _ -> raise (Error "Conversion failed.")
end
module Relation =
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))
-
- 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_relation x =
+ 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
+
+ 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 +847,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,40 +1011,40 @@ 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)
-
- 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)
+ ((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_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
module Integer =
struct
- let mk_sort (ctx:context) = Z3native.mk_int_sort ctx
+ let mk_sort = Z3native.mk_int_sort
- let get_int (x:expr) =
- let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in
- if r then v
- else raise (Error "Conversion failed.")
+ let get_int x =
+ match Z3native.get_numeral_int (Expr.gc x) x with
+ | true, v -> v
+ | false, _ -> raise (Error "Conversion failed.")
let get_big_int (x:expr) =
- if (is_int_numeral x) then
+ if is_int_numeral x then
let s = (Z3native.get_numeral_string (Expr.gc x) x) in
Big_int.big_int_of_string s
else
@@ -1097,23 +1053,23 @@ struct
let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx)
let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name)
- let mk_mod (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_mod t1 t2
- let mk_rem (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_rem t1 t2
+ let mk_mod = Z3native.mk_mod
+ let mk_rem = Z3native.mk_rem
let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx)
let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx)
- let mk_int2real (ctx:context) (t:expr) = apply1 ctx Z3native.mk_int2real t
- let mk_int2bv (ctx:context) (n:int) (t:expr) = Z3native.mk_int2bv ctx n t
+ let mk_int2real = Z3native.mk_int2real
+ let mk_int2bv = Z3native.mk_int2bv
end
module Real =
struct
- let mk_sort (ctx:context) = Z3native.mk_real_sort ctx
- let get_numerator (x:expr) = apply1 (Expr.gc x) Z3native.get_numerator x
- let get_denominator (x:expr) = apply1 (Expr.gc x) Z3native.get_denominator x
+ let mk_sort = Z3native.mk_real_sort
+ let get_numerator x = Z3native.get_numerator (Expr.gc x) x
+ let get_denominator x = Z3native.get_denominator (Expr.gc x) x
- let get_ratio (x:expr) =
- if (is_rat_numeral x) then
- let s = (Z3native.get_numeral_string (Expr.gc x) x) in
+ let get_ratio x =
+ if is_rat_numeral x then
+ let s = Z3native.get_numeral_string (Expr.gc x) x in
Ratio.ratio_of_string s
else
raise (Error "Conversion failed.")
@@ -1123,15 +1079,15 @@ 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
let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx)
let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx)
- let mk_is_integer (ctx:context) (t:expr) = apply1 ctx Z3native.mk_is_int t
- let mk_real2int (ctx:context) (t:expr) = apply1 ctx Z3native.mk_real2int t
+ let mk_is_integer = Z3native.mk_is_int
+ let mk_real2int = Z3native.mk_real2int
module AlgebraicNumber =
struct
@@ -1142,16 +1098,25 @@ struct
end
end
- let mk_add (ctx:context) (t:expr list) = Z3native.mk_add ctx (List.length t) (Array.of_list t)
- let mk_mul (ctx:context) (t:expr list) = Z3native.mk_mul ctx (List.length t) (Array.of_list t)
- let mk_sub (ctx:context) (t:expr list) = Z3native.mk_sub ctx (List.length t) (Array.of_list t)
- let mk_unary_minus (ctx:context) (t:expr) = apply1 ctx Z3native.mk_unary_minus t
- let mk_div (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_div t1 t2
- let mk_power (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_power t1 t2
- let mk_lt (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_lt t1 t2
- let mk_le (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_le t1 t2
- let mk_gt (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_gt t1 t2
- let mk_ge (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_ge t1 t2
+ let mk_add (ctx:context) (t:expr list) =
+ let t_arr = Array.of_list t in
+ Z3native.mk_add ctx (Array.length t_arr) t_arr
+
+ let mk_mul (ctx:context) (t:expr list) =
+ let t_arr = Array.of_list t in
+ Z3native.mk_mul ctx (Array.length t_arr) t_arr
+
+ let mk_sub (ctx:context) (t:expr list) =
+ let t_arr = Array.of_list t in
+ Z3native.mk_sub ctx (Array.length t_arr) t_arr
+
+ let mk_unary_minus = Z3native.mk_unary_minus
+ let mk_div = Z3native.mk_div
+ let mk_power = Z3native.mk_power
+ let mk_lt = Z3native.mk_lt
+ let mk_le = Z3native.mk_le
+ let mk_gt = Z3native.mk_gt
+ let mk_ge = Z3native.mk_ge
end
@@ -1159,116 +1124,118 @@ 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
- if r then v
- else raise (Error "Conversion failed.")
+ match Z3native.get_numeral_int (Expr.gc x) x with
+ | true, v -> v
+ | false, _ -> raise (Error "Conversion failed.")
+
let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
let mk_const (ctx:context) (name:Symbol.symbol) (size:int) =
Expr.mk_const ctx name (mk_sort ctx size)
let mk_const_s (ctx:context) (name:string) (size:int) =
mk_const ctx (Symbol.mk_string ctx name) size
- let mk_not (ctx:context) (t:expr) = apply1 ctx Z3native.mk_bvnot t
- let mk_redand (ctx:context) (t:expr) = apply1 ctx Z3native.mk_bvredand t
- let mk_redor (ctx:context) (t:expr) = apply1 ctx Z3native.mk_bvredor t
- let mk_and (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvand t1 t2
- let mk_or (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvor t1 t2
- let mk_xor (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvxor t1 t2
- let mk_nand (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvnand t1 t2
- let mk_nor (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvnor t1 t2
- let mk_xnor (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvxnor t1 t2
- let mk_neg (ctx:context) (t:expr) = apply1 ctx Z3native.mk_bvneg t
- let mk_add (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvadd t1 t2
- let mk_sub (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsub t1 t2
- let mk_mul (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvmul t1 t2
- let mk_udiv (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvudiv t1 t2
- let mk_sdiv (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsdiv t1 t2
- let mk_urem (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvurem t1 t2
- let mk_srem (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsrem t1 t2
- let mk_smod (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsmod t1 t2
- let mk_ult (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvult t1 t2
- let mk_slt (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvslt t1 t2
- let mk_ule (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvule t1 t2
- let mk_sle (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsle t1 t2
- let mk_uge (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvuge t1 t2
- let mk_sge (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsge t1 t2
- let mk_ugt (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvugt t1 t2
- let mk_sgt (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsgt t1 t2
- let mk_concat (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_concat t1 t2
- let mk_extract (ctx:context) (high:int) (low:int) (t:expr) = Z3native.mk_extract ctx high low t
- let mk_sign_ext (ctx:context) (i:int) (t:expr) = Z3native.mk_sign_ext ctx i t
- let mk_zero_ext (ctx:context) (i:int) (t:expr) = Z3native.mk_zero_ext ctx i t
- let mk_repeat (ctx:context) (i:int) (t:expr) = Z3native.mk_repeat ctx i t
- let mk_shl (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvshl t1 t2
- let mk_lshr (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvlshr t1 t2
- let mk_ashr (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvashr t1 t2
- let mk_rotate_left (ctx:context) (i:int) (t:expr) = Z3native.mk_rotate_left ctx i t
- let mk_rotate_right (ctx:context) (i:int) (t:expr) = Z3native.mk_rotate_right ctx i t
- let mk_ext_rotate_left (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_ext_rotate_left t1 t2
- let mk_ext_rotate_right (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_ext_rotate_right t1 t2
- let mk_bv2int (ctx:context) (t:expr) (signed:bool) = Z3native.mk_bv2int ctx t signed
- let mk_add_no_overflow (ctx:context) (t1:expr) (t2:expr) (signed:bool) = Z3native.mk_bvadd_no_overflow ctx t1 t2 signed
- let mk_add_no_underflow (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvadd_no_underflow t1 t2
- let mk_sub_no_overflow (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsub_no_overflow t1 t2
- let mk_sub_no_underflow (ctx:context) (t1:expr) (t2:expr) (signed:bool) = Z3native.mk_bvsub_no_underflow ctx t1 t2 signed
- let mk_sdiv_no_overflow (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvsdiv_no_overflow t1 t2
- let mk_neg_no_overflow (ctx:context) (t:expr) = apply1 ctx Z3native.mk_bvneg_no_overflow t
- let mk_mul_no_overflow (ctx:context) (t1:expr) (t2:expr) (signed:bool) = Z3native.mk_bvmul_no_overflow ctx t1 t2 signed
- let mk_mul_no_underflow (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_bvmul_no_underflow t1 t2
- let mk_numeral (ctx:context) (v:string) (size:int) = Z3native.mk_numeral ctx v (mk_sort ctx size)
+ let mk_not = Z3native.mk_bvnot
+ let mk_redand = Z3native.mk_bvredand
+ let mk_redor = Z3native.mk_bvredor
+ let mk_and = Z3native.mk_bvand
+ let mk_or = Z3native.mk_bvor
+ let mk_xor = Z3native.mk_bvxor
+ let mk_nand = Z3native.mk_bvnand
+ let mk_nor = Z3native.mk_bvnor
+ let mk_xnor = Z3native.mk_bvxnor
+ let mk_neg = Z3native.mk_bvneg
+ let mk_add = Z3native.mk_bvadd
+ let mk_sub = Z3native.mk_bvsub
+ let mk_mul = Z3native.mk_bvmul
+ let mk_udiv = Z3native.mk_bvudiv
+ let mk_sdiv = Z3native.mk_bvsdiv
+ let mk_urem = Z3native.mk_bvurem
+ let mk_srem = Z3native.mk_bvsrem
+ let mk_smod = Z3native.mk_bvsmod
+ let mk_ult = Z3native.mk_bvult
+ let mk_slt = Z3native.mk_bvslt
+ let mk_ule = Z3native.mk_bvule
+ let mk_sle = Z3native.mk_bvsle
+ let mk_uge = Z3native.mk_bvuge
+ let mk_sge = Z3native.mk_bvsge
+ let mk_ugt = Z3native.mk_bvugt
+ let mk_sgt = Z3native.mk_bvsgt
+ let mk_concat = Z3native.mk_concat
+ let mk_extract = Z3native.mk_extract
+ let mk_sign_ext = Z3native.mk_sign_ext
+ let mk_zero_ext = Z3native.mk_zero_ext
+ let mk_repeat = Z3native.mk_repeat
+ let mk_shl = Z3native.mk_bvshl
+ let mk_lshr = Z3native.mk_bvlshr
+ let mk_ashr = Z3native.mk_bvashr
+ let mk_rotate_left = Z3native.mk_rotate_left
+ let mk_rotate_right = Z3native.mk_rotate_right
+ let mk_ext_rotate_left = Z3native.mk_ext_rotate_left
+ let mk_ext_rotate_right = Z3native.mk_ext_rotate_right
+ let mk_bv2int = Z3native.mk_bv2int
+ let mk_add_no_overflow = Z3native.mk_bvadd_no_overflow
+ let mk_add_no_underflow = Z3native.mk_bvadd_no_underflow
+ let mk_sub_no_overflow = Z3native.mk_bvsub_no_overflow
+ let mk_sub_no_underflow = Z3native.mk_bvsub_no_underflow
+ let mk_sdiv_no_overflow = Z3native.mk_bvsdiv_no_overflow
+ let mk_neg_no_overflow = Z3native.mk_bvneg_no_overflow
+ let mk_mul_no_overflow = Z3native.mk_bvmul_no_overflow
+ let mk_mul_no_underflow = Z3native.mk_bvmul_no_underflow
+ let mk_numeral ctx v size = Z3native.mk_numeral ctx v (mk_sort ctx size)
end
@@ -1276,181 +1243,178 @@ module FloatingPoint =
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 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
- let mk_rna (ctx:context) = Z3native.mk_fpa_rna ctx
- let mk_round_toward_positive (ctx:context) = Z3native.mk_fpa_round_toward_positive ctx
- let mk_rtp (ctx:context) = Z3native.mk_fpa_rtp ctx
- let mk_round_toward_negative (ctx:context) = Z3native.mk_fpa_round_toward_negative ctx
- let mk_rtn (ctx:context) = Z3native.mk_fpa_rtn ctx
- let mk_round_toward_zero (ctx:context) = Z3native.mk_fpa_round_toward_zero ctx
- let mk_rtz (ctx:context) = Z3native.mk_fpa_rtz ctx
+ let mk_sort = Z3native.mk_fpa_rounding_mode_sort
+ let is_fprm x = Sort.get_sort_kind (Expr.get_sort x) = ROUNDING_MODE_SORT
+ let mk_round_nearest_ties_to_even = Z3native.mk_fpa_round_nearest_ties_to_even
+ let mk_rne = Z3native.mk_fpa_rne
+ let mk_round_nearest_ties_to_away = Z3native.mk_fpa_round_nearest_ties_to_away
+ let mk_rna = Z3native.mk_fpa_rna
+ let mk_round_toward_positive = Z3native.mk_fpa_round_toward_positive
+ let mk_rtp = Z3native.mk_fpa_rtp
+ let mk_round_toward_negative = Z3native.mk_fpa_round_toward_negative
+ let mk_rtn = Z3native.mk_fpa_rtn
+ let mk_round_toward_zero = Z3native.mk_fpa_round_toward_zero
+ let mk_rtz = Z3native.mk_fpa_rtz
end
- let mk_sort (ctx:context) (ebits:int) (sbits:int) = Z3native.mk_fpa_sort ctx ebits sbits
- let mk_sort_half (ctx:context) = Z3native.mk_fpa_sort_half ctx
- let mk_sort_16 (ctx:context) = Z3native.mk_fpa_sort_16 ctx
- let mk_sort_single (ctx:context) = Z3native.mk_fpa_sort_single ctx
- let mk_sort_32 (ctx:context) = Z3native.mk_fpa_sort_32 ctx
- let mk_sort_double (ctx:context) = Z3native.mk_fpa_sort_double ctx
- let mk_sort_64 (ctx:context) = Z3native.mk_fpa_sort_64 ctx
- let mk_sort_quadruple (ctx:context) = Z3native.mk_fpa_sort_quadruple ctx
- let mk_sort_128 (ctx:context) = Z3native.mk_fpa_sort_128 ctx
-
- let mk_nan (ctx:context) (s:Sort.sort) = Z3native.mk_fpa_nan ctx s
- let mk_inf (ctx:context) (s:Sort.sort) (negative:bool) = Z3native.mk_fpa_inf ctx s negative
- let mk_zero (ctx:context) (s:Sort.sort) (negative:bool) = Z3native.mk_fpa_zero ctx s negative
- let mk_fp (ctx:context) (sign:expr) (exponent:expr) (significand:expr) = apply3 ctx Z3native.mk_fpa_fp sign exponent significand
- let mk_numeral_f (ctx:context) (value:float) (s:Sort.sort) = Z3native.mk_fpa_numeral_double ctx value s
- let mk_numeral_i (ctx:context) (value:int) (s:Sort.sort) = Z3native.mk_fpa_numeral_int ctx value s
- 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 mk_sort = Z3native.mk_fpa_sort
+ let mk_sort_half = Z3native.mk_fpa_sort_half
+ let mk_sort_16 = Z3native.mk_fpa_sort_16
+ let mk_sort_single = Z3native.mk_fpa_sort_single
+ let mk_sort_32 = Z3native.mk_fpa_sort_32
+ let mk_sort_double = Z3native.mk_fpa_sort_double
+ let mk_sort_64 = Z3native.mk_fpa_sort_64
+ let mk_sort_quadruple = Z3native.mk_fpa_sort_quadruple
+ let mk_sort_128 = Z3native.mk_fpa_sort_128
+
+ let mk_nan = Z3native.mk_fpa_nan
+ let mk_inf = Z3native.mk_fpa_inf
+ let mk_zero = Z3native.mk_fpa_zero
+ let mk_fp = Z3native.mk_fpa_fp
+ let mk_numeral_f = Z3native.mk_fpa_numeral_double
+ let mk_numeral_i = Z3native.mk_fpa_numeral_int
+ let mk_numeral_i_u = Z3native.mk_fpa_numeral_int64_uint64
+ let mk_numeral_s = Z3native.mk_numeral
+
+ 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) =
- Expr.mk_const ctx name s
- let mk_const_s (ctx:context) (name:string) (s:Sort.sort) =
- mk_const ctx (Symbol.mk_string ctx name) s
-
- let mk_abs (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_abs t
- let mk_neg (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_neg t
- let mk_add (ctx:context) (rm:expr) (t1:expr) (t2:expr) = apply3 ctx Z3native.mk_fpa_add rm t1 t2
- let mk_sub (ctx:context) (rm:expr) (t1:expr) (t2:expr) = apply3 ctx Z3native.mk_fpa_sub rm t1 t2
- let mk_mul (ctx:context) (rm:expr) (t1:expr) (t2:expr) = apply3 ctx Z3native.mk_fpa_mul rm t1 t2
- let mk_div (ctx:context) (rm:expr) (t1:expr) (t2:expr) = apply3 ctx Z3native.mk_fpa_div rm t1 t2
- let mk_fma (ctx:context) (rm:expr) (t1:expr) (t2:expr) (t3:expr) = apply4 ctx Z3native.mk_fpa_fma rm t1 t2 t3
- let mk_sqrt (ctx:context) (rm:expr) (t:expr) = apply2 ctx Z3native.mk_fpa_sqrt rm t
- let mk_rem (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_rem t1 t2
- let mk_round_to_integral (ctx:context) (rm:expr) (t:expr) = apply2 ctx Z3native.mk_fpa_round_to_integral rm t
- let mk_min (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_min t1 t2
- let mk_max (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_max t1 t2
- let mk_leq (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_leq t1 t2
- let mk_lt (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_lt t1 t2
- let mk_geq (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_geq t1 t2
- let mk_gt (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_gt t1 t2
- let mk_eq (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_fpa_eq t1 t2
- let mk_is_normal (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_is_normal t
- let mk_is_subnormal (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_is_subnormal t
- let mk_is_zero (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_is_zero t
- let mk_is_infinite (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_is_infinite t
- let mk_is_nan (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_is_nan t
- let mk_is_negative (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_is_negative t
- let mk_is_positive (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_is_positive t
- let mk_to_fp_bv (ctx:context) (t:expr) (s:Sort.sort) = Z3native.mk_fpa_to_fp_bv ctx t s
- let mk_to_fp_float (ctx:context) (rm:expr) (t:expr) (s:Sort.sort) = Z3native.mk_fpa_to_fp_float ctx rm t s
- let mk_to_fp_real (ctx:context) (rm:expr) (t:expr) (s:Sort.sort) = Z3native.mk_fpa_to_fp_real ctx rm t s
- let mk_to_fp_signed (ctx:context) (rm:expr) (t:expr) (s:Sort.sort) = Z3native.mk_fpa_to_fp_signed ctx rm t s
- let mk_to_fp_unsigned (ctx:context) (rm:expr) (t:expr) (s:Sort.sort) = Z3native.mk_fpa_to_fp_unsigned ctx rm t s
- let mk_to_ubv (ctx:context) (rm:expr) (t:expr) (size:int) = Z3native.mk_fpa_to_ubv ctx rm t size
- let mk_to_sbv (ctx:context) (rm:expr) (t:expr) (size:int) = Z3native.mk_fpa_to_sbv ctx rm t size
- let mk_to_real (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_to_real t
- let get_ebits (ctx:context) (s:Sort.sort) = Z3native.fpa_get_ebits ctx s
- let get_sbits (ctx:context) (s:Sort.sort) = Z3native.fpa_get_sbits ctx s
- let get_numeral_sign (ctx:context) (t:expr) = Z3native.fpa_get_numeral_sign ctx t
- let get_numeral_significand_string (ctx:context) (t:expr) = Z3native.fpa_get_numeral_significand_string ctx t
- let get_numeral_significand_uint (ctx:context) (t:expr) = Z3native.fpa_get_numeral_significand_uint64 ctx t
- let get_numeral_exponent_string (ctx:context) (t:expr) = Z3native.fpa_get_numeral_exponent_string ctx t
- let get_numeral_exponent_int (ctx:context) (t:expr) = Z3native.fpa_get_numeral_exponent_int64 ctx t
- let mk_to_ieee_bv (ctx:context) (t:expr) = Z3native.mk_fpa_to_ieee_bv ctx t
- let mk_to_fp_int_real (ctx:context) (rm:expr) (exponent:expr) (significand:expr) (s:Sort.sort) = Z3native.mk_fpa_to_fp_int_real ctx rm exponent significand s
- let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
+
+ let mk_const = Expr.mk_const
+ let mk_const_s = Expr.mk_const_s
+
+ let mk_abs = Z3native.mk_fpa_abs
+ let mk_neg = Z3native.mk_fpa_neg
+ let mk_add = Z3native.mk_fpa_add
+ let mk_sub = Z3native.mk_fpa_sub
+ let mk_mul = Z3native.mk_fpa_mul
+ let mk_div = Z3native.mk_fpa_div
+ let mk_fma = Z3native.mk_fpa_fma
+ let mk_sqrt = Z3native.mk_fpa_sqrt
+ let mk_rem = Z3native.mk_fpa_rem
+ let mk_round_to_integral = Z3native.mk_fpa_round_to_integral
+ let mk_min = Z3native.mk_fpa_min
+ let mk_max = Z3native.mk_fpa_max
+ let mk_leq = Z3native.mk_fpa_leq
+ let mk_lt = Z3native.mk_fpa_lt
+ let mk_geq = Z3native.mk_fpa_geq
+ let mk_gt = Z3native.mk_fpa_gt
+ let mk_eq = Z3native.mk_fpa_eq
+ let mk_is_normal = Z3native.mk_fpa_is_normal
+ let mk_is_subnormal = Z3native.mk_fpa_is_subnormal
+ let mk_is_zero = Z3native.mk_fpa_is_zero
+ let mk_is_infinite = Z3native.mk_fpa_is_infinite
+ let mk_is_nan = Z3native.mk_fpa_is_nan
+ let mk_is_negative = Z3native.mk_fpa_is_negative
+ let mk_is_positive = Z3native.mk_fpa_is_positive
+ let mk_to_fp_bv = Z3native.mk_fpa_to_fp_bv
+ let mk_to_fp_float = Z3native.mk_fpa_to_fp_float
+ let mk_to_fp_real = Z3native.mk_fpa_to_fp_real
+ let mk_to_fp_signed = Z3native.mk_fpa_to_fp_signed
+ let mk_to_fp_unsigned = Z3native.mk_fpa_to_fp_unsigned
+ let mk_to_ubv = Z3native.mk_fpa_to_ubv
+ let mk_to_sbv = Z3native.mk_fpa_to_sbv
+ let mk_to_real = Z3native.mk_fpa_to_real
+ let get_ebits = Z3native.fpa_get_ebits
+ let get_sbits = Z3native.fpa_get_sbits
+ let get_numeral_sign = Z3native.fpa_get_numeral_sign
+ let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string
+ let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64
+ let get_numeral_exponent_string = Z3native.fpa_get_numeral_exponent_string
+ let get_numeral_exponent_int = Z3native.fpa_get_numeral_exponent_int64
+ let mk_to_ieee_bv = Z3native.mk_fpa_to_ieee_bv
+ let mk_to_fp_int_real = Z3native.mk_fpa_to_fp_int_real
+ let numeral_to_string x = Z3native.get_numeral_string (Expr.gc x) x
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 +1433,47 @@ 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)
+ match get_size x with
+ | 0 -> Boolean.mk_true (gc x)
+ | 1 -> List.hd (get_formulas x)
+ | _ -> 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 +1504,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 +1528,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 +1561,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 +1593,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 +1642,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
-
- 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
+ Z3native.tactic_and_then ctx t1 o
+
+ 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 +1706,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 +1720,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 +1735,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 +1744,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 +1759,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 +1840,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
+ 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_relations (gc x) x (List.length relations) (Array.of_list relations)) 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 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:fixedpoint) =
+ 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 +1903,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 +1932,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 +1944,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
@@ -2067,50 +2008,48 @@ struct
mk_list f n
let parse_smtlib2_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
- raise (Error "Argument size mismatch")
+ let sort_names_arr = Array.of_list sort_names in
+ let sorts_arr = Array.of_list sorts in
+ let decl_names_arr = Array.of_list decl_names in
+ let decls_arr = Array.of_list decls in
+ let csn = Array.length sort_names_arr in
+ let cs = Array.length sorts_arr in
+ let cdn = Array.length decl_names_arr in
+ let cd = Array.length decls_arr in
+ 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 sort_names_arr sorts_arr cd decl_names_arr decls_arr
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
+ let sort_names_arr = Array.of_list sort_names in
+ let sorts_arr = Array.of_list sorts in
+ let decl_names_arr = Array.of_list decl_names in
+ let decls_arr = Array.of_list decls in
+ let csn = Array.length sort_names_arr in
+ let cs = Array.length sorts_arr in
+ let cdn = Array.length decl_names_arr in
+ let cd = Array.length decls_arr in
+ 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 sort_names_arr sorts_arr cd decl_names_arr decls_arr
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) =
@@ -2119,62 +2058,56 @@ struct
let compute_interpolant (ctx:context) (pat:expr) (p:Params.params) =
let (r, interp, model) = Z3native.compute_interpolant ctx pat p in
- let res = (lbool_of_int r) 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 555e25bc049..9104b308021 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
+
+ (** Function interpretations entries
- An Entry object represents an element in the finite map used to a function interpretation. *)
+ 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
- (** Tactic application results
-
- ApplyResult objects represent the result of an application of a
+ 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 *)
+(** 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
-
- (** 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
+
+ (** 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 c726d967fbc..02bafeef60d 100644
--- a/src/api/ml/z3native_stubs.c.pre
+++ b/src/api/ml/z3native_stubs.c.pre
@@ -24,32 +24,32 @@ extern "C" {
#include
#include
-#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \
- CAMLlocal5(X1,X2,X3,X4,X5); \
+#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \
+ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal1(X6)
-#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \
- CAMLlocal5(X1,X2,X3,X4,X5); \
+#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \
+ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal2(X6,X7)
-#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \
- CAMLlocal5(X1,X2,X3,X4,X5); \
+#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \
+ CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal3(X6,X7,X8)
-#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \
- CAMLparam5(X1,X2,X3,X4,X5); \
+#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam2(X6,X7)
-#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \
- CAMLparam5(X1,X2,X3,X4,X5); \
+#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam3(X6,X7,X8)
-#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
- CAMLparam5(X1,X2,X3,X4,X5); \
+#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam4(X6,X7,X8,X9)
-#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
- CAMLparam5(X1,X2,X3,X4,X5); \
- CAMLxparam5(X6,X7,X8,X9,X10); \
+#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
+ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam2(X11,X12)
-#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
- CAMLparam5(X1,X2,X3,X4,X5); \
- CAMLxparam5(X6,X7,X8,X9,X10); \
+#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
+ CAMLparam5(X1,X2,X3,X4,X5); \
+ CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam3(X11,X12,X13)
@@ -63,36 +63,44 @@ 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) { \
CAMLparam1(v); \
CAMLlocal1(result); \
- Z3_context_plus cp; \
+ Z3_context_plus cp; \
Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \
- cp = p->cp; \
+ cp = p->cp; \
result = caml_alloc_custom(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), 0, 1); \
- *(Z3_context_plus *)Data_custom_val(result) = cp; \
+ *(Z3_context_plus *)Data_custom_val(result) = cp; \
/* We increment the usage counter of the context, as we just \
created a second custom block holding that context */ \
- cp->obj_count++; \
+ cp->obj_count++; \
CAMLreturn(result); \
- } \
- \
- CAMLprim value DLL_PUBLIC n_is_null_ ## X (value v) { \
- CAMLparam1(v); \
- Z3_ ## X ## _plus* pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
- CAMLreturn(Val_bool(pp->p == NULL)); \
- } \
- \
- CAMLprim value DLL_PUBLIC n_mk_null_ ## X (value v) { \
- CAMLparam1(v); \
- CAMLlocal1(result); \
- Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \
- Z3_ ## X ## _plus a = Z3_ ## X ## _plus_mk(cp, NULL); \
+ } \
+ \
+ CAMLprim value DLL_PUBLIC n_is_null_ ## X (value v) { \
+ CAMLparam1(v); \
+ Z3_ ## X ## _plus* pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
+ CAMLreturn(Val_bool(pp->p == NULL)); \
+ } \
+ \
+ CAMLprim value DLL_PUBLIC n_mk_null_ ## X (value v) { \
+ CAMLparam1(v); \
+ CAMLlocal1(result); \
+ Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \
+ Z3_ ## X ## _plus a = Z3_ ## X ## _plus_mk(cp, NULL); \
result = caml_alloc_custom(&Z3_ ## X ## _plus_custom_ops, sizeof(Z3_ ## X ## _plus), 0, 1); \
- *(Z3_ ## X ## _plus*)(Data_custom_val(result)) = a; \
- CAMLreturn(result); \
+ *(Z3_ ## X ## _plus*)(Data_custom_val(result)) = a; \
+ CAMLreturn(result); \
}
@@ -150,14 +158,38 @@ void Z3_context_finalize(value v) {
try_to_delete_context(cp);
}
+int Z3_context_compare(value v1, value v2) {
+ /* As each context created within the OCaml bindings has a unique
+ Z3_context_plus_data allocated to store the handle and the ref counters,
+ we can just compare pointers here. This suffices to test for (in)equality
+ and induces an arbitrary (but fixed) ordering. */
+ 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) {
+ /* We use the address of the context's Z3_context_plus_data structure
+ as a hash value */
+ 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 +227,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)
@@ -274,15 +314,34 @@ MK_CTX_OF(ast)
pp->cp->obj_count--; \
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)
@@ -298,7 +357,7 @@ MK_CTX_OF(ast)
r.cp = cp; \
r.p = p; \
r.cp->obj_count++; \
- if (p != NULL) \
+ if (p != NULL) \
Z3_ ## X ## _inc_ref(cp->ctx, p); \
return r; \
} \
@@ -309,20 +368,39 @@ MK_CTX_OF(ast)
\
void Z3_ ## X ## _finalize(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
- if (pp->p != NULL) \
+ if (pp->p != NULL) \
Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \
pp->cp->obj_count--; \
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)
@@ -347,7 +425,6 @@ MK_PLUS_OBJ(ast_vector)
MK_PLUS_OBJ(fixedpoint)
MK_PLUS_OBJ(optimize)
-
#ifdef __cplusplus
extern "C" {
#endif