mirror of
https://github.com/Z3Prover/z3
synced 2025-05-02 13:27:01 +00:00
Regenerate ml api
This commit is contained in:
Josh Berdine
parent
79be6ee6c2
commit
6a5de3384c
3 changed files with 1196 additions and 3107 deletions
404
src/api/ml/z3.ml
404
src/api/ml/z3.ml
|
|
@ -293,13 +293,12 @@ let reset_memory () = ()
|
|||
|
||||
(** Exceptions raised by Z3. It is safe to continue interacting with Z3 after
|
||||
catching [Error] exceptions.
|
||||
|
||||
- {b See also}: {!get_error_msg}
|
||||
*)
|
||||
exception Error of context * error_code
|
||||
|
||||
|
||||
|
||||
(* Register dynamically-generated exception tag for use from C *)
|
||||
let _ = Callback.register_exception "Z3.Error" (Error (Obj.magic None, OK))
|
||||
|
||||
external mk_context: (string * string) list -> context = "caml_z3_mk_context"
|
||||
|
|
@ -349,7 +348,6 @@ external param_descrs_to_string : context -> param_descrs -> string
|
|||
|
||||
(**
|
||||
Refined view of a {!symbol}.
|
||||
|
||||
- {b See also}: {!mk_symbol}
|
||||
- {b See also}: {!symbol_refine}
|
||||
*)
|
||||
|
|
@ -368,33 +366,28 @@ external mk_string_symbol : context -> string -> symbol
|
|||
A datatype constructor descriptor.
|
||||
*)
|
||||
type datatype_constructor_desc = {
|
||||
constructor_desc : symbol; (** name of the constructor function *)
|
||||
recognizer_desc : symbol; (** name of the recognizer function *)
|
||||
accessor_descs : (symbol * sort) array; (** names and sorts of the fields *)
|
||||
constructor_desc : symbol; (** name of the constructor function *)
|
||||
recognizer_desc : symbol; (** name of the recognizer function *)
|
||||
accessor_descs : (symbol * sort) array; (** names and sorts of the fields *)
|
||||
}
|
||||
|
||||
(**
|
||||
A datatype is described by a name and constructor descriptors.
|
||||
*)
|
||||
type datatype_desc = symbol * datatype_constructor_desc array
|
||||
|
||||
(**
|
||||
A datatype constructor representation.
|
||||
*)
|
||||
type datatype_constructor = {
|
||||
constructor : func_decl; (** constructor function *)
|
||||
recognizer : func_decl; (** recognizer function *)
|
||||
accessors : func_decl array; (** field accessor functions *)
|
||||
constructor : func_decl; (** constructor function *)
|
||||
recognizer : func_decl; (** recognizer function *)
|
||||
accessors : func_decl array; (** field accessor functions *)
|
||||
}
|
||||
|
||||
(**
|
||||
A datatype is represented by a sort and constructors.
|
||||
*)
|
||||
type datatype = sort * datatype_constructor array
|
||||
|
||||
(**
|
||||
Refined view of a {!sort}.
|
||||
|
||||
- {b See also}: {!mk_sort}
|
||||
- {b See also}: {!sort_refine}
|
||||
*)
|
||||
|
|
@ -751,9 +744,9 @@ external mk_set_subset : context -> ast -> ast -> ast
|
|||
Summary: \[ [ numeral_refined ] \] is the refined view of a numeral .
|
||||
*)
|
||||
type numeral_refined =
|
||||
| Numeral_int of int * sort
|
||||
| Numeral_int64 of int64 * sort
|
||||
| Numeral_large of string * sort
|
||||
| Numeral_int of int * sort
|
||||
| Numeral_int64 of int64 * sort
|
||||
| Numeral_large of string * sort
|
||||
| Numeral_rational of numeral_refined * numeral_refined
|
||||
|
||||
external mk_numeral : context -> string -> sort -> ast
|
||||
|
|
@ -930,21 +923,18 @@ external get_app_arg : context -> app -> int -> ast
|
|||
|
||||
(**
|
||||
Summary: \[ [ binder_type ] \] is a universal or existential quantifier.
|
||||
|
||||
- {b See also}: {!term_refined}
|
||||
*)
|
||||
type binder_type = Forall | Exists
|
||||
|
||||
(**
|
||||
Summary: \[ [ term_refined ] \] is the refinement of a {!ast} .
|
||||
|
||||
- {b See also}: {!term_refine}
|
||||
*)
|
||||
type term_refined =
|
||||
| Term_numeral of numeral_refined
|
||||
| Term_app of decl_kind * func_decl * ast array
|
||||
| Term_numeral of numeral_refined
|
||||
| Term_app of decl_kind * func_decl * ast array
|
||||
| Term_quantifier of binder_type * int * ast array array * (symbol * sort) array * ast
|
||||
| Term_var of int * sort
|
||||
| Term_var of int * sort
|
||||
|
||||
external is_eq_ast : context -> ast -> ast -> bool
|
||||
= "camlidl_z3_Z3_is_eq_ast"
|
||||
|
|
@ -1220,12 +1210,6 @@ external get_smtlib_sort : context -> int -> sort
|
|||
external get_smtlib_error : context -> string
|
||||
= "camlidl_z3_Z3_get_smtlib_error"
|
||||
|
||||
external parse_z3_string : context -> string -> ast
|
||||
= "camlidl_z3_Z3_parse_z3_string"
|
||||
|
||||
external parse_z3_file : context -> string -> ast
|
||||
= "camlidl_z3_Z3_parse_z3_file"
|
||||
|
||||
external set_error : context -> error_code -> unit
|
||||
= "camlidl_z3_Z3_set_error"
|
||||
|
||||
|
|
@ -1235,6 +1219,12 @@ external get_error_msg_ex : context -> error_code -> string
|
|||
external get_version : unit -> int * int * int * int
|
||||
= "camlidl_z3_Z3_get_version"
|
||||
|
||||
external enable_trace : string -> unit
|
||||
= "camlidl_z3_Z3_enable_trace"
|
||||
|
||||
external disable_trace : string -> unit
|
||||
= "camlidl_z3_Z3_disable_trace"
|
||||
|
||||
external mk_fixedpoint : context -> fixedpoint
|
||||
= "camlidl_z3_Z3_mk_fixedpoint"
|
||||
|
||||
|
|
@ -1280,8 +1270,11 @@ external fixedpoint_register_relation : context -> fixedpoint -> func_decl -> un
|
|||
external fixedpoint_set_predicate_representation : context -> fixedpoint -> func_decl -> symbol array -> unit
|
||||
= "camlidl_z3_Z3_fixedpoint_set_predicate_representation"
|
||||
|
||||
external fixedpoint_simplify_rules : context -> fixedpoint -> ast array -> func_decl array -> ast_vector
|
||||
= "camlidl_z3_Z3_fixedpoint_simplify_rules"
|
||||
external fixedpoint_get_rules : context -> fixedpoint -> ast_vector
|
||||
= "camlidl_z3_Z3_fixedpoint_get_rules"
|
||||
|
||||
external fixedpoint_get_assertions : context -> fixedpoint -> ast_vector
|
||||
= "camlidl_z3_Z3_fixedpoint_get_assertions"
|
||||
|
||||
external fixedpoint_set_params : context -> fixedpoint -> params -> unit
|
||||
= "camlidl_z3_Z3_fixedpoint_set_params"
|
||||
|
|
@ -1295,6 +1288,12 @@ external fixedpoint_get_param_descrs : context -> fixedpoint -> param_descrs
|
|||
external fixedpoint_to_string : context -> fixedpoint -> ast array -> string
|
||||
= "camlidl_z3_Z3_fixedpoint_to_string"
|
||||
|
||||
external fixedpoint_from_string : context -> fixedpoint -> string -> ast_vector
|
||||
= "camlidl_z3_Z3_fixedpoint_from_string"
|
||||
|
||||
external fixedpoint_from_file : context -> fixedpoint -> string -> ast_vector
|
||||
= "camlidl_z3_Z3_fixedpoint_from_file"
|
||||
|
||||
external fixedpoint_push : context -> fixedpoint -> unit
|
||||
= "camlidl_z3_Z3_fixedpoint_push"
|
||||
|
||||
|
|
@ -1544,6 +1543,9 @@ external solver_get_num_scopes : context -> solver -> int
|
|||
external solver_assert : context -> solver -> ast -> unit
|
||||
= "camlidl_z3_Z3_solver_assert"
|
||||
|
||||
external solver_assert_and_track : context -> solver -> ast -> ast -> unit
|
||||
= "camlidl_z3_Z3_solver_assert_and_track"
|
||||
|
||||
external solver_get_assertions : context -> solver -> ast_vector
|
||||
= "camlidl_z3_Z3_solver_get_assertions"
|
||||
|
||||
|
|
@ -1597,18 +1599,15 @@ external stats_get_double_value : context -> stats -> int -> float
|
|||
= "camlidl_z3_Z3_stats_get_double_value"
|
||||
|
||||
|
||||
|
||||
(* Internal auxiliary functions: *)
|
||||
(*
|
||||
(* Transform a pair of arrays into an array of pairs *)
|
||||
let array_combine a b =
|
||||
if Array.length a <> Array.length b then raise (Invalid_argument "array_combine");
|
||||
Array.init (Array.length a) (fun i -> (a.(i), b.(i)))
|
||||
|
||||
(* [a |> b] is the pipeline operator for [b(a)] *)
|
||||
let ( |> ) x f = f x
|
||||
*)
|
||||
|
||||
(* Find the index of an element in an array, raises Not_found is missing *)
|
||||
let find equal x a =
|
||||
let len = Array.length a in
|
||||
|
|
@ -1622,24 +1621,17 @@ let find equal x a =
|
|||
find_ (i+1)
|
||||
in
|
||||
find_ 0
|
||||
|
||||
|
||||
(* Symbols *)
|
||||
|
||||
let symbol_refine c s =
|
||||
match get_symbol_kind c s with
|
||||
| INT_SYMBOL -> Symbol_int (get_symbol_int c s)
|
||||
| STRING_SYMBOL -> Symbol_string (get_symbol_string c s)
|
||||
|
||||
let mk_symbol c = function
|
||||
| Symbol_int(i) -> mk_int_symbol c i
|
||||
| Symbol_string(s) -> mk_string_symbol c s
|
||||
|
||||
|
||||
(* Sorts *)
|
||||
|
||||
let get_datatype_sort c s =
|
||||
Array.init (get_datatype_sort_num_constructors c s) (fun i ->
|
||||
let get_datatype_sort c s =
|
||||
Array.init (get_datatype_sort_num_constructors c s) (fun i ->
|
||||
let constructor = get_datatype_sort_constructor c s i in
|
||||
let recognizer = get_datatype_sort_recognizer c s i in
|
||||
let accessors =
|
||||
|
|
@ -1648,7 +1640,6 @@ let get_datatype_sort c s =
|
|||
) in
|
||||
{constructor; recognizer; accessors}
|
||||
)
|
||||
|
||||
let sort_refine c s =
|
||||
match get_sort_kind c s with
|
||||
| UNINTERPRETED_SORT -> Sort_uninterpreted (get_sort_name c s)
|
||||
|
|
@ -1665,7 +1656,6 @@ let sort_refine c s =
|
|||
| DATATYPE_SORT -> Sort_datatype (get_datatype_sort c s)
|
||||
| RELATION_SORT -> Sort_relation (Array.init (get_relation_arity c s) (fun i -> get_relation_column c s i))
|
||||
| UNKNOWN_SORT -> Sort_unknown
|
||||
|
||||
let mk_sort c = function
|
||||
| Sort_uninterpreted(s) -> mk_uninterpreted_sort c s
|
||||
| Sort_bool -> mk_bool_sort c
|
||||
|
|
@ -1677,10 +1667,7 @@ let mk_sort c = function
|
|||
| Sort_datatype(constructors) -> get_range c constructors.(0).constructor
|
||||
| Sort_relation(_) -> invalid_arg "Z3.mk_sort: cannot construct relation sorts"
|
||||
| Sort_unknown(_) -> invalid_arg "Z3.mk_sort: cannot construct unknown sorts"
|
||||
|
||||
|
||||
(* Replacement datatypes creation API *)
|
||||
|
||||
let mk_datatypes ctx generator =
|
||||
let usort0 = mk_uninterpreted_sort ctx (mk_int_symbol ctx 0)
|
||||
in
|
||||
|
|
@ -1749,19 +1736,16 @@ let mk_datatypes ctx generator =
|
|||
) ctorss
|
||||
;
|
||||
datatypes
|
||||
|
||||
|
||||
(* Numerals *)
|
||||
|
||||
let rec numeral_refine c t =
|
||||
assert( get_ast_kind c t = NUMERAL_AST );
|
||||
let sort = get_sort c t in
|
||||
let is_int, i = get_numeral_int c t in
|
||||
if is_int then
|
||||
if is_int then
|
||||
Numeral_int (i, sort)
|
||||
else
|
||||
let is_int64, i = get_numeral_int64 c t in
|
||||
if is_int64 then
|
||||
if is_int64 then
|
||||
Numeral_int64 (i, sort)
|
||||
else
|
||||
if get_sort_kind c sort <> REAL_SORT then
|
||||
|
|
@ -1770,14 +1754,11 @@ let rec numeral_refine c t =
|
|||
let n = numeral_refine c (get_numerator c t) in
|
||||
let d = numeral_refine c (get_denominator c t) in
|
||||
Numeral_rational (n, d)
|
||||
|
||||
|
||||
let to_real c x =
|
||||
if get_sort_kind c (get_sort c x) = REAL_SORT then
|
||||
x
|
||||
else
|
||||
mk_int2real c x
|
||||
|
||||
let rec embed_numeral c = function
|
||||
| Numeral_int (i, s) -> mk_int c i s
|
||||
| Numeral_int64 (i, s) -> mk_int64 c i s
|
||||
|
|
@ -1790,21 +1771,14 @@ let rec embed_numeral c = function
|
|||
let d_str = get_numeral_string c (embed_numeral c d) in
|
||||
mk_numeral c (n_str ^ " / " ^ d_str) (mk_real_sort c)
|
||||
*)
|
||||
|
||||
(* Terms *)
|
||||
|
||||
let get_app_args c a =
|
||||
Array.init (get_app_num_args c a) (get_app_arg c a);;
|
||||
|
||||
let get_domains c d =
|
||||
Array.init (get_domain_size c d) (get_domain c d);;
|
||||
|
||||
|
||||
let get_pattern_terms c p =
|
||||
let get_pattern_terms c p =
|
||||
Array.init (get_pattern_num_terms c p) (get_pattern c p)
|
||||
|
||||
|
||||
let term_refine c t =
|
||||
let term_refine c t =
|
||||
match get_ast_kind c t with
|
||||
| NUMERAL_AST ->
|
||||
Term_numeral (numeral_refine c t)
|
||||
|
|
@ -1815,35 +1789,29 @@ let term_refine c t =
|
|||
let args = Array.init num_args (get_app_arg c t') in
|
||||
let k = get_decl_kind c f in
|
||||
Term_app (k, f, args)
|
||||
| QUANTIFIER_AST ->
|
||||
| QUANTIFIER_AST ->
|
||||
let bt = if is_quantifier_forall c t then Forall else Exists in
|
||||
let w = get_quantifier_weight c t in
|
||||
let np = get_quantifier_num_patterns c t in
|
||||
let pats = Array.init np (get_quantifier_pattern_ast c t) in
|
||||
let pats = Array.map (get_pattern_terms c) pats in
|
||||
let nb = get_quantifier_num_bound c t in
|
||||
let w = get_quantifier_weight c t in
|
||||
let np = get_quantifier_num_patterns c t in
|
||||
let pats = Array.init np (get_quantifier_pattern_ast c t) in
|
||||
let pats = Array.map (get_pattern_terms c) pats in
|
||||
let nb = get_quantifier_num_bound c t in
|
||||
let bound =
|
||||
Array.init nb (fun i ->
|
||||
(get_quantifier_bound_name c t i, get_quantifier_bound_sort c t i)
|
||||
) in
|
||||
let body = get_quantifier_body c t in
|
||||
Term_quantifier (bt, w, pats, bound, body)
|
||||
| VAR_AST ->
|
||||
| VAR_AST ->
|
||||
Term_var (get_index_value c t, get_sort c t)
|
||||
| _ ->
|
||||
assert false
|
||||
|
||||
|
||||
(* let mk_term c = function *)
|
||||
(* | Term_numeral (numeral, sort) -> mk_numeral c numeral sort *)
|
||||
(* | Term_app (kind, decl, args) -> *)
|
||||
(* | Term_quantifier (strength, weight, pats, bound, body) -> *)
|
||||
(* | Term_var (index, sort) -> *)
|
||||
|
||||
|
||||
|
||||
(* | Term_numeral (numeral, sort) -> mk_numeral c numeral sort *)
|
||||
(* | Term_app (kind, decl, args) -> *)
|
||||
(* | Term_quantifier (strength, weight, pats, bound, body) -> *)
|
||||
(* | Term_var (index, sort) -> *)
|
||||
(* Refined model API *)
|
||||
|
||||
let model_refine c m =
|
||||
let num_sorts = model_get_num_sorts c m in
|
||||
let sorts = Hashtbl.create num_sorts in
|
||||
|
|
@ -1903,49 +1871,33 @@ let model_refine c m =
|
|||
()
|
||||
done;
|
||||
{sorts; consts; arrays; funcs}
|
||||
|
||||
|
||||
(* Extended parser API *)
|
||||
|
||||
let get_smtlib_formulas c =
|
||||
let get_smtlib_formulas c =
|
||||
Array.init (get_smtlib_num_formulas c) (get_smtlib_formula c)
|
||||
|
||||
let get_smtlib_assumptions c =
|
||||
let get_smtlib_assumptions c =
|
||||
Array.init (get_smtlib_num_assumptions c) (get_smtlib_assumption c)
|
||||
|
||||
let get_smtlib_decls c =
|
||||
Array.init (get_smtlib_num_decls c) (get_smtlib_decl c)
|
||||
|
||||
let get_smtlib_parse_results c =
|
||||
(get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c)
|
||||
|
||||
let parse_smtlib_string_x c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_string_x c a1 a2 a3 a4 a5 =
|
||||
parse_smtlib_string c a1 a2 a3 a4 a5 ;
|
||||
get_smtlib_parse_results c
|
||||
|
||||
let parse_smtlib_file_x c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_file_x c a1 a2 a3 a4 a5 =
|
||||
parse_smtlib_file c a1 a2 a3 a4 a5 ;
|
||||
get_smtlib_parse_results c
|
||||
|
||||
let parse_smtlib_string_formula c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_string_formula c a1 a2 a3 a4 a5 =
|
||||
parse_smtlib_string c a1 a2 a3 a4 a5 ;
|
||||
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith "Z3: parse_smtlib_string_formula"
|
||||
|
||||
let parse_smtlib_file_formula c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_file_formula c a1 a2 a3 a4 a5 =
|
||||
parse_smtlib_file c a1 a2 a3 a4 a5 ;
|
||||
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith "Z3: parse_smtlib_file_formula"
|
||||
|
||||
|
||||
(* Error handling *)
|
||||
|
||||
let get_error_msg c e =
|
||||
match e with
|
||||
| PARSER_ERROR -> (get_error_msg_ex c e) ^ ": " ^ (get_smtlib_error c)
|
||||
| _ -> get_error_msg_ex c e
|
||||
|
||||
|
||||
(* Refined stats API *)
|
||||
|
||||
let stats_refine c s =
|
||||
let num_stats = stats_size c s in
|
||||
let tbl = Hashtbl.create num_stats in
|
||||
|
|
@ -1970,7 +1922,7 @@ let _ =
|
|||
|
||||
module V3 = struct
|
||||
|
||||
(* File generated from z3.idl *)
|
||||
(* File generated from z3V3.idl *)
|
||||
|
||||
type symbol
|
||||
and literals
|
||||
|
|
@ -2205,6 +2157,15 @@ and ast_print_mode =
|
|||
| PRINT_SMTLIB2_COMPLIANT
|
||||
|
||||
|
||||
external global_param_set : string -> string -> unit
|
||||
= "camlidl_z3V3_Z3_global_param_set"
|
||||
|
||||
external global_param_reset_all : unit -> unit
|
||||
= "camlidl_z3V3_Z3_global_param_reset_all"
|
||||
|
||||
external global_param_get : string -> string option
|
||||
= "camlidl_z3V3_Z3_global_param_get"
|
||||
|
||||
external mk_config : unit -> config
|
||||
= "camlidl_z3V3_Z3_mk_config"
|
||||
|
||||
|
|
@ -2263,7 +2224,7 @@ external mk_list_sort : context -> symbol -> sort -> sort * func_decl * func_dec
|
|||
= "camlidl_z3V3_Z3_mk_list_sort"
|
||||
|
||||
external mk_constructor : context -> symbol -> symbol -> symbol array -> sort array -> int array -> constructor
|
||||
= "camlidl_z3_Z3_mk_constructor_bytecode" "camlidl_z3V3_Z3_mk_constructor"
|
||||
= "camlidl_z3V3_Z3_mk_constructor_bytecode" "camlidl_z3V3_Z3_mk_constructor"
|
||||
|
||||
external del_constructor : context -> constructor -> unit
|
||||
= "camlidl_z3V3_Z3_del_constructor"
|
||||
|
|
@ -2587,16 +2548,16 @@ external mk_bound : context -> int -> sort -> ast
|
|||
= "camlidl_z3V3_Z3_mk_bound"
|
||||
|
||||
external mk_forall : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast
|
||||
= "camlidl_z3_Z3_mk_forall_bytecode" "camlidl_z3V3_Z3_mk_forall"
|
||||
= "camlidl_z3V3_Z3_mk_forall_bytecode" "camlidl_z3V3_Z3_mk_forall"
|
||||
|
||||
external mk_exists : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast
|
||||
= "camlidl_z3_Z3_mk_exists_bytecode" "camlidl_z3V3_Z3_mk_exists"
|
||||
= "camlidl_z3V3_Z3_mk_exists_bytecode" "camlidl_z3V3_Z3_mk_exists"
|
||||
|
||||
external mk_quantifier : context -> bool -> int -> pattern array -> sort array -> symbol array -> ast -> ast
|
||||
= "camlidl_z3_Z3_mk_quantifier_bytecode" "camlidl_z3V3_Z3_mk_quantifier"
|
||||
= "camlidl_z3V3_Z3_mk_quantifier_bytecode" "camlidl_z3V3_Z3_mk_quantifier"
|
||||
|
||||
external mk_quantifier_ex : context -> bool -> int -> symbol -> symbol -> pattern array -> ast array -> sort array -> symbol array -> ast -> ast
|
||||
= "camlidl_z3_Z3_mk_quantifier_ex_bytecode" "camlidl_z3V3_Z3_mk_quantifier_ex"
|
||||
= "camlidl_z3V3_Z3_mk_quantifier_ex_bytecode" "camlidl_z3V3_Z3_mk_quantifier_ex"
|
||||
|
||||
external mk_forall_const : context -> int -> app array -> pattern array -> ast -> ast
|
||||
= "camlidl_z3V3_Z3_mk_forall_const"
|
||||
|
|
@ -2605,10 +2566,10 @@ external mk_exists_const : context -> int -> app array -> pattern array -> ast -
|
|||
= "camlidl_z3V3_Z3_mk_exists_const"
|
||||
|
||||
external mk_quantifier_const : context -> bool -> int -> app array -> pattern array -> ast -> ast
|
||||
= "camlidl_z3_Z3_mk_quantifier_const_bytecode" "camlidl_z3V3_Z3_mk_quantifier_const"
|
||||
= "camlidl_z3V3_Z3_mk_quantifier_const_bytecode" "camlidl_z3V3_Z3_mk_quantifier_const"
|
||||
|
||||
external mk_quantifier_const_ex : context -> bool -> int -> symbol -> symbol -> app array -> pattern array -> ast array -> ast -> ast
|
||||
= "camlidl_z3_Z3_mk_quantifier_const_ex_bytecode" "camlidl_z3V3_Z3_mk_quantifier_const_ex"
|
||||
= "camlidl_z3V3_Z3_mk_quantifier_const_ex_bytecode" "camlidl_z3V3_Z3_mk_quantifier_const_ex"
|
||||
|
||||
external get_symbol_kind : context -> symbol -> symbol_kind
|
||||
= "camlidl_z3V3_Z3_get_symbol_kind"
|
||||
|
|
@ -2890,19 +2851,19 @@ external model_to_string : context -> model -> string
|
|||
= "camlidl_z3V3_Z3_model_to_string"
|
||||
|
||||
external benchmark_to_smtlib_string : context -> string -> string -> string -> string -> ast array -> ast -> string
|
||||
= "camlidl_z3_Z3_benchmark_to_smtlib_string_bytecode" "camlidl_z3V3_Z3_benchmark_to_smtlib_string"
|
||||
= "camlidl_z3V3_Z3_benchmark_to_smtlib_string_bytecode" "camlidl_z3V3_Z3_benchmark_to_smtlib_string"
|
||||
|
||||
external parse_smtlib2_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast
|
||||
= "camlidl_z3_Z3_parse_smtlib2_string_bytecode" "camlidl_z3V3_Z3_parse_smtlib2_string"
|
||||
= "camlidl_z3V3_Z3_parse_smtlib2_string_bytecode" "camlidl_z3V3_Z3_parse_smtlib2_string"
|
||||
|
||||
external parse_smtlib2_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast
|
||||
= "camlidl_z3_Z3_parse_smtlib2_file_bytecode" "camlidl_z3V3_Z3_parse_smtlib2_file"
|
||||
= "camlidl_z3V3_Z3_parse_smtlib2_file_bytecode" "camlidl_z3V3_Z3_parse_smtlib2_file"
|
||||
|
||||
external parse_smtlib_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit
|
||||
= "camlidl_z3_Z3_parse_smtlib_string_bytecode" "camlidl_z3V3_Z3_parse_smtlib_string"
|
||||
= "camlidl_z3V3_Z3_parse_smtlib_string_bytecode" "camlidl_z3V3_Z3_parse_smtlib_string"
|
||||
|
||||
external parse_smtlib_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit
|
||||
= "camlidl_z3_Z3_parse_smtlib_file_bytecode" "camlidl_z3V3_Z3_parse_smtlib_file"
|
||||
= "camlidl_z3V3_Z3_parse_smtlib_file_bytecode" "camlidl_z3V3_Z3_parse_smtlib_file"
|
||||
|
||||
external get_smtlib_num_formulas : context -> int
|
||||
= "camlidl_z3V3_Z3_get_smtlib_num_formulas"
|
||||
|
|
@ -2931,15 +2892,15 @@ external get_smtlib_sort : context -> int -> sort
|
|||
external get_smtlib_error : context -> string
|
||||
= "camlidl_z3V3_Z3_get_smtlib_error"
|
||||
|
||||
external parse_z3_string : context -> string -> ast
|
||||
= "camlidl_z3_Z3_parse_z3V3_string"
|
||||
|
||||
external parse_z3_file : context -> string -> ast
|
||||
= "camlidl_z3_Z3_parse_z3V3_file"
|
||||
|
||||
external get_version : unit -> int * int * int * int
|
||||
= "camlidl_z3V3_Z3_get_version"
|
||||
|
||||
external enable_trace : string -> unit
|
||||
= "camlidl_z3V3_Z3_enable_trace"
|
||||
|
||||
external disable_trace : string -> unit
|
||||
= "camlidl_z3V3_Z3_disable_trace"
|
||||
|
||||
external reset_memory : unit -> unit
|
||||
= "camlidl_z3V3_Z3_reset_memory"
|
||||
|
||||
|
|
@ -3121,114 +3082,85 @@ external get_context_assignment : context -> ast
|
|||
= "camlidl_z3V3_Z3_get_context_assignment"
|
||||
|
||||
|
||||
|
||||
|
||||
(* Internal auxillary functions: *)
|
||||
|
||||
(* Transform a pair of arrays into an array of pairs *)
|
||||
let array_combine a b =
|
||||
if Array.length a <> Array.length b then raise (Invalid_argument "array_combine");
|
||||
Array.init (Array.length a) (fun i->(a.(i),b.(i)));;
|
||||
|
||||
(* [a |> b] is the pipeline operator for [b(a)] *)
|
||||
let ( |> ) x f = f x;;
|
||||
|
||||
|
||||
(* Extensions, except for refinement: *)
|
||||
let mk_context_x configs =
|
||||
let mk_context_x configs =
|
||||
let config = mk_config() in
|
||||
let f(param_id,param_value) = set_param_value config param_id param_value in
|
||||
Array.iter f configs;
|
||||
let context = mk_context config in
|
||||
del_config config;
|
||||
context;;
|
||||
|
||||
let get_app_args c a =
|
||||
Array.init (get_app_num_args c a) (get_app_arg c a);;
|
||||
|
||||
let get_domains c d =
|
||||
Array.init (get_domain_size c d) (get_domain c d);;
|
||||
|
||||
let get_array_sort c t = (get_array_sort_domain c t, get_array_sort_range c t);;
|
||||
|
||||
let get_tuple_sort c ty =
|
||||
let get_tuple_sort c ty =
|
||||
(get_tuple_sort_mk_decl c ty,
|
||||
Array.init (get_tuple_sort_num_fields c ty) (get_tuple_sort_field_decl c ty));;
|
||||
|
||||
type datatype_constructor_refined = {
|
||||
constructor : func_decl;
|
||||
recognizer : func_decl;
|
||||
accessors : func_decl array
|
||||
type datatype_constructor_refined = {
|
||||
constructor : func_decl;
|
||||
recognizer : func_decl;
|
||||
accessors : func_decl array
|
||||
}
|
||||
|
||||
let get_datatype_sort c ty =
|
||||
let get_datatype_sort c ty =
|
||||
Array.init (get_datatype_sort_num_constructors c ty)
|
||||
(fun idx_c ->
|
||||
(fun idx_c ->
|
||||
let constr = get_datatype_sort_constructor c ty idx_c in
|
||||
let recog = get_datatype_sort_recognizer c ty idx_c in
|
||||
let recog = get_datatype_sort_recognizer c ty idx_c in
|
||||
let num_acc = get_domain_size c constr in
|
||||
{ constructor = constr;
|
||||
recognizer = recog;
|
||||
accessors = Array.init num_acc (get_datatype_sort_constructor_accessor c ty idx_c);
|
||||
})
|
||||
|
||||
let get_model_constants c m =
|
||||
Array.init (get_model_num_constants c m) (get_model_constant c m);;
|
||||
|
||||
|
||||
let get_model_func_entry c m i j =
|
||||
(Array.init
|
||||
(get_model_func_entry_num_args c m i j)
|
||||
(get_model_func_entry_arg c m i j),
|
||||
get_model_func_entry_value c m i j);;
|
||||
|
||||
let get_model_func_entries c m i =
|
||||
Array.init (get_model_func_num_entries c m i) (get_model_func_entry c m i);;
|
||||
|
||||
let get_model_funcs c m =
|
||||
Array.init (get_model_num_funcs c m)
|
||||
(fun i->(get_model_func_decl c m i |> get_decl_name c,
|
||||
get_model_func_entries c m i,
|
||||
get_model_func_else c m i));;
|
||||
|
||||
let get_smtlib_formulas c =
|
||||
let get_smtlib_formulas c =
|
||||
Array.init (get_smtlib_num_formulas c) (get_smtlib_formula c);;
|
||||
|
||||
let get_smtlib_assumptions c =
|
||||
let get_smtlib_assumptions c =
|
||||
Array.init (get_smtlib_num_assumptions c) (get_smtlib_assumption c);;
|
||||
|
||||
let get_smtlib_decls c =
|
||||
Array.init (get_smtlib_num_decls c) (get_smtlib_decl c);;
|
||||
|
||||
let get_smtlib_parse_results c =
|
||||
(get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c);;
|
||||
|
||||
let parse_smtlib_string_formula c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_string_formula c a1 a2 a3 a4 a5 =
|
||||
(parse_smtlib_string c a1 a2 a3 a4 a5;
|
||||
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith "Z3: parse_smtlib_string_formula");;
|
||||
|
||||
let parse_smtlib_file_formula c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_file_formula c a1 a2 a3 a4 a5 =
|
||||
(parse_smtlib_file c a1 a2 a3 a4 a5;
|
||||
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith "Z3: parse_smtlib_file_formula");;
|
||||
|
||||
let parse_smtlib_string_x c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_string_x c a1 a2 a3 a4 a5 =
|
||||
(parse_smtlib_string c a1 a2 a3 a4 a5; get_smtlib_parse_results c);;
|
||||
|
||||
let parse_smtlib_file_x c a1 a2 a3 a4 a5 =
|
||||
let parse_smtlib_file_x c a1 a2 a3 a4 a5 =
|
||||
(parse_smtlib_file c a1 a2 a3 a4 a5; get_smtlib_parse_results c);;
|
||||
|
||||
(* Refinement: *)
|
||||
|
||||
type symbol_refined =
|
||||
| Symbol_int of int
|
||||
| Symbol_string of string
|
||||
| Symbol_unknown;;
|
||||
|
||||
let symbol_refine c s =
|
||||
match get_symbol_kind c s with
|
||||
| INT_SYMBOL -> Symbol_int (get_symbol_int c s)
|
||||
| STRING_SYMBOL -> Symbol_string (get_symbol_string c s);;
|
||||
|
||||
type sort_refined =
|
||||
| Sort_uninterpreted of symbol
|
||||
| Sort_bool
|
||||
|
|
@ -3240,7 +3172,6 @@ type sort_refined =
|
|||
| Sort_relation
|
||||
| Sort_finite_domain
|
||||
| Sort_unknown of symbol;;
|
||||
|
||||
let sort_refine c ty =
|
||||
match get_sort_kind c ty with
|
||||
| UNINTERPRETED_SORT -> Sort_uninterpreted (get_sort_name c ty)
|
||||
|
|
@ -3250,56 +3181,50 @@ let sort_refine c ty =
|
|||
| BV_SORT -> Sort_bv (get_bv_sort_size c ty)
|
||||
| ARRAY_SORT -> Sort_array (get_array_sort_domain c ty, get_array_sort_range c ty)
|
||||
| DATATYPE_SORT -> Sort_datatype (get_datatype_sort c ty)
|
||||
| RELATION_SORT -> Sort_relation
|
||||
| RELATION_SORT -> Sort_relation
|
||||
| FINITE_DOMAIN_SORT -> Sort_finite_domain
|
||||
| UNKNOWN_SORT -> Sort_unknown (get_sort_name c ty);;
|
||||
|
||||
let get_pattern_terms c p =
|
||||
let get_pattern_terms c p =
|
||||
Array.init (get_pattern_num_terms c p) (get_pattern c p)
|
||||
|
||||
type binder_type = | Forall | Exists
|
||||
|
||||
type numeral_refined =
|
||||
| Numeral_small of int64 * int64
|
||||
| Numeral_large of string
|
||||
|
||||
type term_refined =
|
||||
| Term_app of decl_kind * func_decl * ast array
|
||||
type binder_type = | Forall | Exists
|
||||
type numeral_refined =
|
||||
| Numeral_small of int64 * int64
|
||||
| Numeral_large of string
|
||||
type term_refined =
|
||||
| Term_app of decl_kind * func_decl * ast array
|
||||
| Term_quantifier of binder_type * int * ast array array * (symbol *sort) array * ast
|
||||
| Term_numeral of numeral_refined * sort
|
||||
| Term_var of int * sort
|
||||
|
||||
let term_refine c t =
|
||||
| Term_numeral of numeral_refined * sort
|
||||
| Term_var of int * sort
|
||||
let term_refine c t =
|
||||
match get_ast_kind c t with
|
||||
| NUMERAL_AST ->
|
||||
| NUMERAL_AST ->
|
||||
let (is_small, n, d) = get_numeral_small c t in
|
||||
if is_small then
|
||||
Term_numeral(Numeral_small(n,d), get_sort c t)
|
||||
if is_small then
|
||||
Term_numeral(Numeral_small(n,d), get_sort c t)
|
||||
else
|
||||
Term_numeral(Numeral_large(get_numeral_string c t), get_sort c t)
|
||||
| APP_AST ->
|
||||
Term_numeral(Numeral_large(get_numeral_string c t), get_sort c t)
|
||||
| APP_AST ->
|
||||
let t' = to_app c t in
|
||||
let f = get_app_decl c t' in
|
||||
let f = get_app_decl c t' in
|
||||
let num_args = get_app_num_args c t' in
|
||||
let args = Array.init num_args (get_app_arg c t') in
|
||||
let k = get_decl_kind c f in
|
||||
Term_app (k, f, args)
|
||||
| QUANTIFIER_AST ->
|
||||
| QUANTIFIER_AST ->
|
||||
let bt = if is_quantifier_forall c t then Forall else Exists in
|
||||
let w = get_quantifier_weight c t in
|
||||
let np = get_quantifier_num_patterns c t in
|
||||
let pats = Array.init np (get_quantifier_pattern_ast c t) in
|
||||
let pats = Array.map (get_pattern_terms c) pats in
|
||||
let nb = get_quantifier_num_bound c t in
|
||||
let bound = Array.init nb
|
||||
(fun i -> (get_quantifier_bound_name c t i, get_quantifier_bound_sort c t i)) in
|
||||
let w = get_quantifier_weight c t in
|
||||
let np = get_quantifier_num_patterns c t in
|
||||
let pats = Array.init np (get_quantifier_pattern_ast c t) in
|
||||
let pats = Array.map (get_pattern_terms c) pats in
|
||||
let nb = get_quantifier_num_bound c t in
|
||||
let bound = Array.init nb
|
||||
(fun i -> (get_quantifier_bound_name c t i, get_quantifier_bound_sort c t i)) in
|
||||
let body = get_quantifier_body c t in
|
||||
Term_quantifier(bt, w, pats, bound, body)
|
||||
| VAR_AST ->
|
||||
| VAR_AST ->
|
||||
Term_var(get_index_value c t, get_sort c t)
|
||||
| _ -> assert false
|
||||
|
||||
type theory_callbacks =
|
||||
type theory_callbacks =
|
||||
{
|
||||
mutable delete_theory : unit -> unit;
|
||||
mutable reduce_eq : ast -> ast -> ast option;
|
||||
|
|
@ -3318,8 +3243,7 @@ type theory_callbacks =
|
|||
mutable new_assignment: ast -> bool -> unit;
|
||||
mutable new_relevant : ast -> unit;
|
||||
}
|
||||
|
||||
let mk_theory_callbacks() =
|
||||
let mk_theory_callbacks() =
|
||||
{
|
||||
delete_theory = (fun () -> ());
|
||||
reduce_eq = (fun _ _ -> None);
|
||||
|
|
@ -3338,8 +3262,6 @@ let mk_theory_callbacks() =
|
|||
new_assignment = (fun _ _ -> ());
|
||||
new_relevant = (fun _ -> ());
|
||||
}
|
||||
|
||||
|
||||
external get_theory_callbacks : theory -> theory_callbacks = "get_theory_callbacks"
|
||||
external mk_theory_register : context -> string -> theory_callbacks -> theory = "mk_theory_register"
|
||||
external set_delete_callback_register : theory -> unit = "set_delete_callback_register"
|
||||
|
|
@ -3358,146 +3280,116 @@ external set_new_eq_callback_register : theory -> unit = "set_new_eq_callback_re
|
|||
external set_new_diseq_callback_register : theory -> unit = "set_new_diseq_callback_register"
|
||||
external set_new_assignment_callback_register : theory -> unit = "set_new_assignment_callback_register"
|
||||
external set_new_relevant_callback_register : theory -> unit = "set_new_relevant_callback_register"
|
||||
|
||||
let is_some opt =
|
||||
let is_some opt =
|
||||
match opt with
|
||||
| Some v -> true
|
||||
| None -> false
|
||||
|
||||
let get_some opt =
|
||||
| None -> false
|
||||
let get_some opt =
|
||||
match opt with
|
||||
| Some v -> v
|
||||
| None -> failwith "None unexpected"
|
||||
|
||||
|
||||
|
||||
|
||||
| None -> failwith "None unexpected"
|
||||
let apply_delete (th:theory_callbacks) = th.delete_theory ()
|
||||
let set_delete_callback th cb =
|
||||
let set_delete_callback th cb =
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.delete_theory <- cb;
|
||||
set_delete_callback_register th
|
||||
|
||||
let mk_theory context name =
|
||||
let mk_theory context name =
|
||||
Callback.register "is_some" is_some;
|
||||
Callback.register "get_some" get_some;
|
||||
Callback.register "apply_delete" apply_delete;
|
||||
let cbs = mk_theory_callbacks() in
|
||||
mk_theory_register context name cbs
|
||||
|
||||
|
||||
let apply_reduce_app (th:theory_callbacks) f args = th.reduce_app f args
|
||||
let set_reduce_app_callback th cb =
|
||||
let set_reduce_app_callback th cb =
|
||||
Callback.register "apply_reduce_app" apply_reduce_app;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.reduce_app <- cb;
|
||||
set_reduce_app_callback_register th
|
||||
|
||||
let apply_reduce_eq (th:theory_callbacks) a b = th.reduce_eq a b
|
||||
let set_reduce_eq_callback th cb =
|
||||
let set_reduce_eq_callback th cb =
|
||||
Callback.register "apply_reduce_eq" apply_reduce_eq;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.reduce_eq <- cb;
|
||||
set_reduce_eq_callback_register th
|
||||
|
||||
let apply_reduce_distinct (th:theory_callbacks) args = th.reduce_distinct args
|
||||
let set_reduce_distinct_callback th cb =
|
||||
let set_reduce_distinct_callback th cb =
|
||||
Callback.register "apply_reduce_distinct" apply_reduce_distinct;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.reduce_distinct <- cb;
|
||||
set_reduce_distinct_callback_register th
|
||||
|
||||
|
||||
let apply_new_app (th:theory_callbacks) a = th.new_app a
|
||||
let set_new_app_callback th cb =
|
||||
let set_new_app_callback th cb =
|
||||
Callback.register "apply_new_app" apply_new_app;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.new_app <- cb;
|
||||
set_new_app_callback_register th
|
||||
|
||||
let apply_new_elem (th:theory_callbacks) a = th.new_elem a
|
||||
let set_new_elem_callback th cb =
|
||||
let set_new_elem_callback th cb =
|
||||
Callback.register "apply_new_elem" apply_new_elem;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.new_elem <- cb;
|
||||
set_new_elem_callback_register th
|
||||
|
||||
|
||||
let apply_init_search (th:theory_callbacks) = th.init_search()
|
||||
let set_init_search_callback th cb =
|
||||
let set_init_search_callback th cb =
|
||||
Callback.register "apply_init_search" apply_init_search;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.init_search <- cb;
|
||||
set_init_search_callback_register th
|
||||
|
||||
|
||||
let apply_push (th:theory_callbacks) = th.push()
|
||||
let set_push_callback th cb =
|
||||
let set_push_callback th cb =
|
||||
Callback.register "apply_push" apply_push;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.push <- cb;
|
||||
set_push_callback_register th
|
||||
|
||||
let apply_pop (th:theory_callbacks) = th.pop()
|
||||
let set_pop_callback th cb =
|
||||
let set_pop_callback th cb =
|
||||
Callback.register "apply_pop" apply_pop;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.pop <- cb;
|
||||
set_pop_callback_register th
|
||||
|
||||
|
||||
let apply_restart (th:theory_callbacks) = th.restart()
|
||||
let set_restart_callback th cb =
|
||||
let set_restart_callback th cb =
|
||||
Callback.register "apply_restart" apply_restart;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.restart <- cb;
|
||||
set_restart_callback_register th
|
||||
|
||||
|
||||
let apply_reset (th:theory_callbacks) = th.reset()
|
||||
let set_reset_callback th cb =
|
||||
let set_reset_callback th cb =
|
||||
Callback.register "apply_reset" apply_reset;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.reset <- cb;
|
||||
set_reset_callback_register th
|
||||
|
||||
let apply_final_check (th:theory_callbacks) = th.final_check()
|
||||
let set_final_check_callback th cb =
|
||||
let set_final_check_callback th cb =
|
||||
Callback.register "apply_final_check" apply_final_check;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.final_check <- cb;
|
||||
set_final_check_callback_register th
|
||||
|
||||
let apply_new_eq (th:theory_callbacks) a b = th.new_eq a b
|
||||
let set_new_eq_callback th cb =
|
||||
let set_new_eq_callback th cb =
|
||||
Callback.register "apply_new_eq" apply_new_eq;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.new_eq <- cb;
|
||||
set_new_eq_callback_register th
|
||||
|
||||
|
||||
let apply_new_diseq (th:theory_callbacks) a b = th.new_diseq a b
|
||||
let set_new_diseq_callback th cb =
|
||||
let set_new_diseq_callback th cb =
|
||||
Callback.register "apply_new_diseq" apply_new_diseq;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.new_diseq <- cb;
|
||||
set_new_diseq_callback_register th
|
||||
|
||||
let apply_new_assignment (th:theory_callbacks) a b = th.new_assignment a b
|
||||
let set_new_assignment_callback th cb =
|
||||
let set_new_assignment_callback th cb =
|
||||
Callback.register "apply_new_assignment" apply_new_assignment;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.new_assignment <- cb;
|
||||
set_new_assignment_callback_register th
|
||||
|
||||
let apply_new_relevant (th:theory_callbacks) a = th.new_relevant a
|
||||
let set_new_relevant_callback th cb =
|
||||
let set_new_relevant_callback th cb =
|
||||
Callback.register "apply_new_relevant" apply_new_relevant;
|
||||
let cbs = get_theory_callbacks th in
|
||||
cbs.new_relevant <- cb;
|
||||
set_new_relevant_callback_register th
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue