mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

ML API: proper use of datatype API for list/enum/constructor.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-02-20 19:49:09 +00:00
parent 6842acbea8
commit dc03e2903f
3 changed files with 27 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/ml/Makefile
View file

@ -7,4 +7,4 @@ all:
doc: *.ml
mkdir -p doc
ocamldoc -html -d doc -I ../../../bld_dbg/api/ml -sort *.mli -hide Z3
ocamldoc -html -d doc -I _build -sort *.mli -hide Z3

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

@ -2159,15 +2159,10 @@ end
module Enumeration =
struct
type enum_sort = EnumSort of sort
let _constdecls = Hashtbl.create 0
let _testerdecls = Hashtbl.create 0
let sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) ( cdecls : Z3native.z3_func_decl array ) ( tdecls : Z3native.z3_func_decl array ) =
let s = (sort_of_ptr ctx no) in
let res = EnumSort(s) in
Hashtbl.add _constdecls res (let f e = func_decl_of_ptr ctx e in (Array.map f cdecls)) ;
Hashtbl.add _testerdecls res (let f e = func_decl_of_ptr ctx e in (Array.map f tdecls)) ;
res
let sort_of_enum_sort s = match s with EnumSort(x) -> x
@ -2191,33 +2186,27 @@ struct
mk_sort ctx (Symbol.mk_string ctx name) (Symbol.mk_strings ctx enum_names)
(** The function declarations of the constants in the enumeration. *)
let get_const_decls ( x : enum_sort ) = Hashtbl.find _constdecls x
let get_const_decls ( x : enum_sort ) =
let n = Z3native.get_datatype_sort_num_constructors (sgnc x) (sgno x) in
let f i = (func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) i)) in
Array.init n f
(** The test predicates for the constants in the enumeration. *)
let get_tester_decls ( x : enum_sort ) = Hashtbl.find _testerdecls x
let get_tester_decls ( x : enum_sort ) =
let n = Z3native.get_datatype_sort_num_constructors (sgnc x) (sgno x) in
let f i = (func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) i)) in
Array.init n f
end
(** Functions to manipulate List expressions *)
module List_ =
struct
type list_sort = ListSort of sort
let _nildecls = Hashtbl.create 0
let _is_nildecls = Hashtbl.create 0
let _consdecls = Hashtbl.create 0
let _is_consdecls = Hashtbl.create 0
let _headdecls = Hashtbl.create 0
let _taildecls = Hashtbl.create 0
let sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) ( nildecl : Z3native.ptr ) ( is_nildecl : Z3native.ptr ) ( consdecl : Z3native.ptr ) ( is_consdecl : Z3native.ptr ) ( headdecl : Z3native.ptr ) ( taildecl : Z3native.ptr ) =
let s = (sort_of_ptr ctx no) in
let res = ListSort(s) in
Hashtbl.add _nildecls res (func_decl_of_ptr ctx nildecl) ;
Hashtbl.add _is_nildecls res (func_decl_of_ptr ctx is_nildecl) ;
Hashtbl.add _consdecls res (func_decl_of_ptr ctx consdecl) ;
Hashtbl.add _is_consdecls res (func_decl_of_ptr ctx is_consdecl) ;
Hashtbl.add _headdecls res (func_decl_of_ptr ctx headdecl) ;
Hashtbl.add _taildecls res (func_decl_of_ptr ctx taildecl) ;
res
let sort_of_list_sort s = match s with ListSort(x) -> x
@ -2237,22 +2226,28 @@ struct
mk_sort ctx (Symbol.mk_string ctx name) elem_sort
(** The declaration of the nil function of this list sort. *)
let get_nil_decl ( x : list_sort ) = (Hashtbl.find _nildecls x)
let get_nil_decl ( x : list_sort ) =
func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) 0)
(** The declaration of the isNil function of this list sort. *)
let get_is_nil_decl ( x : list_sort ) = (Hashtbl.find _is_nildecls x)
let get_is_nil_decl ( x : list_sort ) =
func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) 0)
(** The declaration of the cons function of this list sort. *)
let get_cons_decl ( x : list_sort ) = (Hashtbl.find _consdecls x)
let get_cons_decl ( x : list_sort ) =
func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) 1)
(** The declaration of the isCons function of this list sort. *)
let get_is_cons_decl ( x : list_sort ) = (Hashtbl.find _is_consdecls x)
let get_is_cons_decl ( x : list_sort ) =
func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) 1)
(** The declaration of the head function of this list sort. *)
let get_head_decl ( x : list_sort ) = (Hashtbl.find _headdecls x)
let get_head_decl ( x : list_sort ) =
func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor_accessor (sgnc x) (sgno x) 1 0)
(** The declaration of the tail function of this list sort. *)
let get_tail_decl ( x : list_sort ) = (Hashtbl.find _taildecls x)
let get_tail_decl ( x : list_sort ) =
func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor_accessor (sgnc x) (sgno x) 1 1)
(** The empty list. *)
let nil ( x : list_sort ) = expr_of_func_app (sgc x) (get_nil_decl x) [||]

7
src/api/ml/z3.mli
View file

@ -5,9 +5,9 @@
@author CM Wintersteiger (cwinter) 2012-12-17
*)
type context
(** Create a context object.
(** 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
@ -27,6 +27,9 @@ type context
(...)
</code>
*)
type context
(** Create a context object *)
val mk_context : (string * string) list -> context