From 5e2a7e06fd21ce14e3ff33042fbec7562307d3a4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 23 Apr 2014 15:25:08 +0100 Subject: [PATCH] ML API: added constructors for ast_map and ast_vector Signed-off-by: Christoph M. Wintersteiger --- src/api/ml/z3.ml | 31 ++++++++++++++++++++++--------- src/api/ml/z3.mli | 20 ++++++++++++-------- 2 files changed, 34 insertions(+), 17 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 3f40b288c..b48681b87 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 84f230d95..4347c7431 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -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