mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +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 1c34842ca6
commit ce94a8b2e0
2 changed files with 34 additions and 17 deletions
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
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 ;
m_n_obj = null ;
inc_ref = Z3native.ast_vector_inc_ref ;
@ -223,6 +223,8 @@ struct
(z3obj_create res) ;
res
let mk_ast_vector ( ctx : context ) = (create ctx (Z3native.mk_ast_vector (context_gno ctx)))
let get_size ( x : ast_vector ) =
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)
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 ) =
Z3native.ast_vector_to_string (z3obj_gnc x) (z3obj_gno x)
@ -248,7 +250,18 @@ struct
module ASTMap =
struct
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 res : ast_map = { m_ctx = ctx ;
m_n_obj = null ;
@ -277,7 +290,7 @@ struct
Z3native.ast_map_size (z3obj_gnc x) (z3obj_gno x)
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
mk_list f (ASTVector.get_size av)
@ -2061,7 +2074,7 @@ struct
mk_list f n
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 f i = (AST.ASTVector.get n_univ i) in
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)
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)
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 f i = (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in
mk_list f n
@ -2423,7 +2436,7 @@ struct
Some (expr_of_ptr (z3obj_gc x) q)
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 f i = (AST.ASTVector.get cn i) in
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))
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 f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in
mk_list f n
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 f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in
mk_list f n

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

@ -107,10 +107,9 @@ sig
(** A string representation of the symbol. *)
val to_string : symbol -> string
(** 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. *)
(** 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
(** Creates a new symbol using a string. *)
@ -132,12 +131,14 @@ sig
module ASTVector :
sig
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.
(** Retrieves the i-th object in the vector.
@return An AST *)
val get : ast_vector -> int -> ast
@ -162,7 +163,10 @@ sig
(** Map from AST to AST *)
module ASTMap :
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.
@return True if the key in the map, false otherwise. *)
@ -2297,7 +2301,7 @@ sig
(** 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