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

ML API: added constructors for ast_map and ast_vector

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-04-23 15:25:08 +01:00
parent 9160925c28
commit 5e2a7e06fd
2 changed files with 34 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -214,7 +214,7 @@ struct
struct struct
type ast_vector = z3_native_object type ast_vector = z3_native_object
let ast_vector_of_ptr ( ctx : context ) ( no : Z3native.ptr ) = let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : ast_vector = { m_ctx = ctx ; let res : ast_vector = { m_ctx = ctx ;
m_n_obj = null ; m_n_obj = null ;
inc_ref = Z3native.ast_vector_inc_ref ; inc_ref = Z3native.ast_vector_inc_ref ;
@ -223,6 +223,8 @@ struct
(z3obj_create res) ; (z3obj_create res) ;
res res
let mk_ast_vector ( ctx : context ) = (create ctx (Z3native.mk_ast_vector (context_gno ctx)))
let get_size ( x : ast_vector ) = let get_size ( x : ast_vector ) =
Z3native.ast_vector_size (z3obj_gnc x) (z3obj_gno x) Z3native.ast_vector_size (z3obj_gnc x) (z3obj_gno x)
@ -239,7 +241,7 @@ struct
Z3native.ast_vector_push (z3obj_gnc x) (z3obj_gno x) (z3obj_gno a) Z3native.ast_vector_push (z3obj_gnc x) (z3obj_gno x) (z3obj_gno a)
let translate ( x : ast_vector ) ( to_ctx : context ) = let translate ( x : ast_vector ) ( to_ctx : context ) =
ast_vector_of_ptr to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) create to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx))
let to_string ( x : ast_vector ) = let to_string ( x : ast_vector ) =
Z3native.ast_vector_to_string (z3obj_gnc x) (z3obj_gno x) Z3native.ast_vector_to_string (z3obj_gnc x) (z3obj_gno x)
@ -248,7 +250,18 @@ struct
module ASTMap = module ASTMap =
struct struct
type ast_map = z3_native_object type ast_map = z3_native_object
let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : ast_map = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = Z3native.ast_map_inc_ref ;
dec_ref = Z3native.ast_map_dec_ref } in
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
let mk_ast_map ( ctx : context ) = (create ctx (Z3native.mk_ast_map (context_gno ctx)))
let astmap_of_ptr ( ctx : context ) ( no : Z3native.ptr ) = let astmap_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let res : ast_map = { m_ctx = ctx ; let res : ast_map = { m_ctx = ctx ;
m_n_obj = null ; m_n_obj = null ;
@ -277,7 +290,7 @@ struct
Z3native.ast_map_size (z3obj_gnc x) (z3obj_gno x) Z3native.ast_map_size (z3obj_gnc x) (z3obj_gno x)
let get_keys ( x : ast_map ) = let get_keys ( x : ast_map ) =
let av = ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x)) in let av = ASTVector.create (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x)) in
let f i = (ASTVector.get av i) in let f i = (ASTVector.get av i) in
mk_list f (ASTVector.get_size av) mk_list f (ASTVector.get_size av)
@ -2061,7 +2074,7 @@ struct
mk_list f n mk_list f n
let sort_universe ( x : model ) ( s : sort ) = let sort_universe ( x : model ) ( s : sort ) =
let n_univ = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in let n_univ = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in
let n = (AST.ASTVector.get_size n_univ) in let n = (AST.ASTVector.get_size n_univ) in
let f i = (AST.ASTVector.get n_univ i) in let f i = (AST.ASTVector.get n_univ i) in
mk_list f n mk_list f n
@ -2386,11 +2399,11 @@ struct
Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Expr.gno c) (Expr.gno p) Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Expr.gno c) (Expr.gno p)
let get_num_assertions ( x : solver ) = let get_num_assertions ( x : solver ) =
let a = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in
(AST.ASTVector.get_size a) (AST.ASTVector.get_size a)
let get_assertions ( x : solver ) = let get_assertions ( x : solver ) =
let a = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in
let n = (AST.ASTVector.get_size a) in let n = (AST.ASTVector.get_size a) in
let f i = (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in let f i = (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in
mk_list f n mk_list f n
@ -2423,7 +2436,7 @@ struct
Some (expr_of_ptr (z3obj_gc x) q) Some (expr_of_ptr (z3obj_gc x) q)
let get_unsat_core ( x : solver ) = let get_unsat_core ( x : solver ) =
let cn = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in let cn = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in
let n = (AST.ASTVector.get_size cn) in let n = (AST.ASTVector.get_size cn) in
let f i = (AST.ASTVector.get cn i) in let f i = (AST.ASTVector.get cn i) in
mk_list f n mk_list f n
@ -2545,13 +2558,13 @@ struct
Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (List.length queries) (Array.of_list (List.map f queries)) Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (List.length queries) (Array.of_list (List.map f queries))
let get_rules ( x : fixedpoint ) = let get_rules ( x : fixedpoint ) =
let v = (AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in
let n = (AST.ASTVector.get_size v) in let n = (AST.ASTVector.get_size v) in
let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in
mk_list f n mk_list f n
let get_assertions ( x : fixedpoint ) = let get_assertions ( x : fixedpoint ) =
let v = (AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in
let n = (AST.ASTVector.get_size v) in let n = (AST.ASTVector.get_size v) in
let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in
mk_list f n mk_list f n

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

@ -107,10 +107,9 @@ sig
(** A string representation of the symbol. *) (** A string representation of the symbol. *)
val to_string : symbol -> string 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.
Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1. *)
The legal range of unsigned integers is 0 to 2^30-1. *)
val mk_int : context -> int -> symbol val mk_int : context -> int -> symbol
(** Creates a new symbol using a string. *) (** Creates a new symbol using a string. *)
@ -132,12 +131,14 @@ sig
module ASTVector : module ASTVector :
sig sig
type ast_vector type ast_vector
(** Create an empty AST vector *)
val mk_ast_vector : context -> ast_vector
(** The size of the vector *) (** The size of the vector *)
val get_size : ast_vector -> int val get_size : ast_vector -> int
(** (** Retrieves the i-th object in the vector.
Retrieves the i-th object in the vector.
@return An AST *) @return An AST *)
val get : ast_vector -> int -> ast val get : ast_vector -> int -> ast
@ -162,7 +163,10 @@ sig
(** Map from AST to AST *) (** Map from AST to AST *)
module ASTMap : module ASTMap :
sig sig
type ast_map type ast_map
(** Create an empty mapping from AST to AST *)
val mk_ast_map : context -> ast_map
(** Checks whether the map contains a key. (** 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. *)
@ -2297,7 +2301,7 @@ sig
(** Creates a new 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. *) the fourth argument is set to true here. *)
val mk_goal : context -> bool -> bool -> bool -> goal val mk_goal : context -> bool -> bool -> bool -> goal