mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

style

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-04 17:07:20 +00:00
parent c9a5676346
commit 61525b9f5e
1 changed files with 116 additions and 130 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ end
let mk_list (f:int -> 'a) (n:int) = let mk_list (f:int -> 'a) (n:int) =
let rec mk_list' (f:int -> 'a) (i:int) (n:int) (tail:'a list ):'a list = let rec mk_list' (f:int -> 'a) (i:int) (n:int) (tail:'a list):'a list =
if (i >= n) then if (i >= n) then
tail tail
else else
@ -69,8 +69,8 @@ struct
let is_int_symbol (o:symbol) = (kind o) == INT_SYMBOL let is_int_symbol (o:symbol) = (kind o) == INT_SYMBOL
let is_string_symbol (o:symbol) = (kind o) == STRING_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_int (o:symbol) = (Z3native.get_symbol_int (gc o) o)
let get_string (o:symbol ) = (Z3native.get_symbol_string (gc o) o) let get_string (o:symbol) = (Z3native.get_symbol_string (gc o) o)
let to_string (o:symbol ) = let to_string (o:symbol) =
match (kind o) with match (kind o) with
| INT_SYMBOL -> (string_of_int (Z3native.get_symbol_int (gc o) o)) | INT_SYMBOL -> (string_of_int (Z3native.get_symbol_int (gc o) o))
| STRING_SYMBOL -> (Z3native.get_symbol_string (gc o) o) | STRING_SYMBOL -> (Z3native.get_symbol_string (gc o) o)
@ -79,12 +79,10 @@ struct
let mk_string (ctx:context) (s:string) = (Z3native.mk_string_symbol ctx s) let mk_string (ctx:context) (s:string) = (Z3native.mk_string_symbol ctx s)
let mk_ints (ctx:context) (names:int list) = let mk_ints (ctx:context) (names:int list) =
let f elem = mk_int (ctx:context ) elem in List.map (fun x -> mk_int ctx x) names
(List.map f names)
let mk_strings (ctx:context) (names:string list) = let mk_strings (ctx:context) (names:string list) =
let f elem = mk_string (ctx:context) elem in List.map (fun x -> mk_string ctx x) names
(List.map f names)
end end
@ -148,19 +146,19 @@ end = struct
let set (x:ast_vector) (i:int) (value:ast) = Z3native.ast_vector_set (gc x) x i value let set (x:ast_vector) (i:int) (value:ast) = Z3native.ast_vector_set (gc x) x i value
let resize (x:ast_vector) (new_size:int) = Z3native.ast_vector_resize (gc x) x new_size let resize (x:ast_vector) (new_size:int) = Z3native.ast_vector_resize (gc x) x new_size
let push (x:ast_vector) (a:ast) = Z3native.ast_vector_push (gc x) x a let push (x:ast_vector) (a:ast) = Z3native.ast_vector_push (gc x) x a
let translate (x:ast_vector ) (to_ctx:context ) = Z3native.ast_vector_translate (gc x) x to_ctx let translate (x:ast_vector) (to_ctx:context) = Z3native.ast_vector_translate (gc x) x to_ctx
let to_list (x:ast_vector ) = let to_list (x:ast_vector) =
let xs = (get_size x) in let xs = (get_size x) in
let f i = (get x i) in let f i = (get x i) in
mk_list f xs mk_list f xs
let to_expr_list (x:ast_vector ) = 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 let f i = get x i in
mk_list f xs mk_list f xs
let to_string (x:ast_vector ) = Z3native.ast_vector_to_string (gc x) x let to_string (x:ast_vector) = Z3native.ast_vector_to_string (gc x) x
end end
module ASTMap = module ASTMap =
@ -217,7 +215,7 @@ end = struct
if (get_id a) > (get_id b) then 1 else if (get_id a) > (get_id b) then 1 else
0 0
let translate (x:ast) (to_ctx:context ) = let translate (x:ast) (to_ctx:context) =
if (gc x) == to_ctx then if (gc x) == to_ctx then
x x
else else
@ -311,7 +309,7 @@ end = struct
| P_Fdl of func_decl | P_Fdl of func_decl
| P_Rat of string | P_Rat of string
let get_kind (x:parameter ) = let get_kind (x:parameter) =
(match x with (match x with
| P_Int(_) -> PARAMETER_INT | P_Int(_) -> PARAMETER_INT
| P_Dbl(_) -> PARAMETER_DOUBLE | P_Dbl(_) -> PARAMETER_DOUBLE
@ -375,7 +373,7 @@ end = struct
let mk_fresh_const_decl (ctx:context) (prefix:string) (range:Sort.sort) = let mk_fresh_const_decl (ctx:context) (prefix:string) (range:Sort.sort) =
Z3native.mk_fresh_func_decl ctx prefix 0 [||] range Z3native.mk_fresh_func_decl ctx prefix 0 [||] range
let equal (a:func_decl ) (b:func_decl ) = let equal (a:func_decl) (b:func_decl) =
(a == b) || (a == b) ||
(if (gc a) != (gc b) then (if (gc a) != (gc b) then
false false
@ -406,8 +404,7 @@ end = struct
| PARAMETER_SORT -> Parameter.P_Srt (Z3native.get_decl_sort_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_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_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) | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gc x) x i)) in
) in
mk_list f n mk_list f n
let apply (x:func_decl) (args:Expr.expr list) = Expr.expr_of_func_app (gc x) x args let apply (x:func_decl) (args:Expr.expr list) = Expr.expr_of_func_app (gc x) x args
@ -925,7 +922,7 @@ struct
let get_num_fields (x:constructor) = FieldNumTable.find _field_nums x let get_num_fields (x:constructor) = FieldNumTable.find _field_nums x
let get_constructor_decl (x:constructor ) = let get_constructor_decl (x:constructor) =
let (a, _, _) = (Z3native.query_constructor (gc x) x (get_num_fields x)) in let (a, _, _) = (Z3native.query_constructor (gc x) x (get_num_fields x)) in
a a
@ -937,7 +934,6 @@ struct
let (_, _, c) = (Z3native.query_constructor (gc x) x (get_num_fields x)) in let (_, _, c) = (Z3native.query_constructor (gc x) x (get_num_fields x)) in
let f i = Array.get c i in let f i = Array.get c i in
mk_list f (Array.length c) mk_list f (Array.length c)
end end
module ConstructorList = module ConstructorList =
@ -970,12 +966,7 @@ struct
mk_list g (Array.length r) mk_list g (Array.length r)
let mk_sorts_s (ctx:context) (names:string list) (c:Constructor.constructor list list) = let mk_sorts_s (ctx:context) (names:string list) (c:Constructor.constructor list list) =
mk_sorts ctx mk_sorts ctx (List.map (fun x -> Symbol.mk_string ctx x) names) c
(
let f e = (Symbol.mk_string ctx e) in
List.map f names
)
c
let get_num_constructors (x:Sort.sort) = Z3native.get_datatype_sort_num_constructors (Sort.gc x) x let get_num_constructors (x:Sort.sort) = Z3native.get_datatype_sort_num_constructors (Sort.gc x) x
@ -995,8 +986,7 @@ struct
let fd = Z3native.get_datatype_sort_constructor (Sort.gc x) x i in let fd = Z3native.get_datatype_sort_constructor (Sort.gc x) x i in
let ds = Z3native.get_domain_size (FuncDecl.gc fd) fd in let ds = Z3native.get_domain_size (FuncDecl.gc fd) fd in
let g j = Z3native.get_datatype_sort_constructor_accessor (Sort.gc x) x i j in let g j = Z3native.get_datatype_sort_constructor_accessor (Sort.gc x) x i j in
mk_list g ds mk_list g ds) in
) in
mk_list f n mk_list f n
end end
@ -1318,7 +1308,7 @@ struct
let mk_inf (ctx:context) (s:Sort.sort) (negative:bool) = Z3native.mk_fpa_inf ctx s negative 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_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_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_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 (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_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 mk_numeral_s (ctx:context) (v:string) (s:Sort.sort) = Z3native.mk_numeral ctx v s
@ -1563,8 +1553,7 @@ struct
(List.fold_right (List.fold_right
g g
(FuncEntry.get_args c) (FuncEntry.get_args c)
((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", ")) ((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", "))) in
) in
List.fold_right f (get_entries x) ("else -> " ^ (Expr.to_string (get_else x)) ^ "]") List.fold_right f (get_entries x) ("else -> " ^ (Expr.to_string (get_else x)) ^ "]")
end end
@ -1579,10 +1568,9 @@ struct
else else
Some np Some np
let get_const_interp_e (x:model ) (a:expr) = get_const_interp x (Expr.get_func_decl a) let get_const_interp_e (x:model) (a:expr) = get_const_interp x (Expr.get_func_decl a)
let rec get_func_interp (x:model) (f:func_decl) =
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 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 let n = Z3native.model_get_const_interp (gc x) x f in
@ -1602,28 +1590,28 @@ struct
if (Z3native.is_null n) then None else Some n if (Z3native.is_null n) then None else Some n
(** The number of constants that have an interpretation in the model. *) (** The number of constants that have an interpretation in the model. *)
let get_num_consts (x:model ) = Z3native.model_get_num_consts (gc x) x let get_num_consts (x:model) = Z3native.model_get_num_consts (gc x) x
let get_const_decls (x:model ) = let get_const_decls (x:model) =
let n = (get_num_consts x) in let n = (get_num_consts x) in
let f i = Z3native.model_get_const_decl (gc x) x i in let f i = Z3native.model_get_const_decl (gc x) x i in
mk_list f n mk_list f n
let get_num_funcs (x:model ) = Z3native.model_get_num_funcs (gc x) x let get_num_funcs (x:model) = Z3native.model_get_num_funcs (gc x) x
let get_func_decls (x:model ) = let get_func_decls (x:model) =
let n = (get_num_funcs x) in let n = (get_num_funcs x) in
let f i = Z3native.model_get_func_decl (gc x) x i in let f i = Z3native.model_get_func_decl (gc x) x i in
mk_list f n mk_list f n
let get_decls (x:model ) = let get_decls (x:model) =
let n_funcs = (get_num_funcs x) in let n_funcs = (get_num_funcs x) in
let n_consts = (get_num_consts x ) in let n_consts = (get_num_consts x) in
let f i = Z3native.model_get_func_decl (gc x) x i 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 let g i = Z3native.model_get_const_decl (gc x) x i in
(mk_list f n_funcs) @ (mk_list g n_consts) (mk_list f n_funcs) @ (mk_list g n_consts)
let eval (x:model ) (t:expr) (completion:bool) = let eval (x:model) (t:expr) (completion:bool) =
let (r, v) = Z3native.model_eval (gc x) x t completion in let (r, v) = Z3native.model_eval (gc x) x t completion in
if not r then None else Some v if not r then None else Some v
@ -1647,7 +1635,7 @@ module Probe =
struct struct
type probe = Z3native.probe type probe = Z3native.probe
let apply (x:probe ) (g:Goal.goal) = Z3native.probe_apply (gc x) x g 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 (ctx:context) = Z3native.get_num_probes ctx
let get_probe_names (ctx:context) = let get_probe_names (ctx:context) =
@ -1665,7 +1653,7 @@ struct
let eq (ctx:context) (p1:probe) (p2:probe) = Z3native.probe_eq 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 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 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 not_ (ctx:context) (p:probe) = Z3native.probe_not ctx p
end end
@ -1681,7 +1669,7 @@ struct
let get_num_subgoals (x:apply_result) = Z3native.apply_result_get_num_subgoals (gc x) x let get_num_subgoals (x:apply_result) = Z3native.apply_result_get_num_subgoals (gc x) x
let get_subgoals (x:apply_result ) = let get_subgoals (x:apply_result) =
let n = get_num_subgoals x in let n = get_num_subgoals x in
let f i = Z3native.apply_result_get_subgoal (gc x) x i in let f i = Z3native.apply_result_get_subgoal (gc x) x i in
mk_list f n mk_list f n
@ -1743,7 +1731,7 @@ struct
module Entry = module Entry =
struct struct
type statistics_entry = { type statistics_entry = {
mutable m_key:string; mutable m_key:string ;
mutable m_is_int:bool ; mutable m_is_int:bool ;
mutable m_is_float:bool ; mutable m_is_float:bool ;
mutable m_int:int ; mutable m_int:int ;
@ -1769,7 +1757,6 @@ struct
} in } in
res res
let get_key (x:statistics_entry) = x.m_key let get_key (x:statistics_entry) = x.m_key
let get_int (x:statistics_entry) = x.m_int let get_int (x:statistics_entry) = x.m_int
let get_float (x:statistics_entry) = x.m_float let get_float (x:statistics_entry) = x.m_float
@ -1803,7 +1790,7 @@ struct
let f i = Z3native.stats_get_key (gc x) x i in let f i = Z3native.stats_get_key (gc x) x i in
mk_list f n mk_list f n
let get (x:statistics) (key:string ) = let get (x:statistics) (key:string) =
let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in
List.fold_left f None (get_entries x) List.fold_left f None (get_entries x)
end end
@ -1855,8 +1842,7 @@ struct
if ((List.length assumptions) == 0) then if ((List.length assumptions) == 0) then
lbool_of_int (Z3native.solver_check (gc x) x) lbool_of_int (Z3native.solver_check (gc x) x)
else else
let f x = x in lbool_of_int (Z3native.solver_check_assumptions (gc x) x (List.length assumptions) (Array.of_list assumptions))
lbool_of_int (Z3native.solver_check_assumptions (gc x) x (List.length assumptions) (Array.of_list (List.map f assumptions)))
in in
match r with match r with
| L_TRUE -> SATISFIABLE | L_TRUE -> SATISFIABLE
@ -1964,11 +1950,11 @@ struct
let mk_fixedpoint (ctx:context) = Z3native.mk_fixedpoint ctx let mk_fixedpoint (ctx:context) = Z3native.mk_fixedpoint ctx
let get_statistics (x:fixedpoint) = Z3native.fixedpoint_get_statistics (gc x) x let get_statistics (x:fixedpoint) = Z3native.fixedpoint_get_statistics (gc x) x
let parse_string (x:fixedpoint) (s:string ) = let parse_string (x:fixedpoint) (s:string) =
let av = Z3native.fixedpoint_from_string (gc x) x s in let av = Z3native.fixedpoint_from_string (gc x) x s in
AST.ASTVector.to_expr_list av AST.ASTVector.to_expr_list av
let parse_file (x:fixedpoint) (filename:string ) = let parse_file (x:fixedpoint) (filename:string) =
let av = Z3native.fixedpoint_from_file (gc x) x filename in let av = Z3native.fixedpoint_from_file (gc x) x filename in
AST.ASTVector.to_expr_list av AST.ASTVector.to_expr_list av
end end
@ -2121,7 +2107,7 @@ module Interpolation =
struct struct
let mk_interpolant (ctx:context) (a:expr) = Z3native.mk_interpolant ctx a let mk_interpolant (ctx:context) (a:expr) = Z3native.mk_interpolant ctx a
let mk_interpolation_context (settings:(string * string ) list) = let mk_interpolation_context (settings:(string * string) list) =
let cfg = Z3native.mk_config () in let cfg = Z3native.mk_config () in
let f e = Z3native.set_param_value cfg (fst e) (snd e) in let f e = Z3native.set_param_value cfg (fst e) (snd e) in
(List.iter f settings) ; (List.iter f settings) ;
@ -2135,7 +2121,7 @@ struct
let av = Z3native.get_interpolant ctx pf pat p in let av = Z3native.get_interpolant ctx pf pat p in
AST.ASTVector.to_expr_list av AST.ASTVector.to_expr_list av
let compute_interpolant (ctx:context) (pat:expr) (p:Params.params ) = let compute_interpolant (ctx:context) (pat:expr) (p:Params.params) =
let (r, interp, model) = Z3native.compute_interpolant ctx pat p in 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 match res with