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 bugfix for datatype module (Issue #120). Thanks to user Elarnon for reporting this!

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-07-24 19:29:06 +01:00
parent 84b7644305
commit 94a8c271d4
1 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -277,7 +277,7 @@ struct
let find ( x : ast_map ) ( key : ast ) = let find ( x : ast_map ) ( key : ast ) =
ast_of_ptr (z3obj_gc x) (Z3native.ast_map_find (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key)) ast_of_ptr (z3obj_gc x) (Z3native.ast_map_find (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key))
let insert ( x : ast_map ) ( key : ast ) ( value : ast) = let insert ( x : ast_map ) ( key : ast ) ( value : ast ) =
Z3native.ast_map_insert (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) (z3obj_gno value) Z3native.ast_map_insert (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) (z3obj_gno value)
let erase ( x : ast_map ) ( key : ast ) = let erase ( x : ast_map ) ( key : ast ) =
@ -1259,7 +1259,13 @@ struct
struct struct
type constructor = z3_native_object type constructor = z3_native_object
let _sizes = Hashtbl.create 0 module FieldNumTable = Hashtbl.Make(struct
type t = AST.ast
let equal x y = AST.compare x y = 0
let hash = AST.hash
end)
let _field_nums = FieldNumTable.create 0
let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) = let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
let n = (List.length field_names) in let n = (List.length field_names) in
@ -1283,10 +1289,10 @@ struct
(z3obj_create no) ; (z3obj_create no) ;
let f = fun o -> Z3native.del_constructor (z3obj_gnc o) (z3obj_gno o) in let f = fun o -> Z3native.del_constructor (z3obj_gnc o) (z3obj_gno o) in
Gc.finalise f no ; Gc.finalise f no ;
Hashtbl.add _sizes no n ; FieldNumTable.add _field_nums no n ;
no no
let get_num_fields ( x : constructor ) = Hashtbl.find _sizes x let get_num_fields ( x : constructor ) = FieldNumTable.find _field_nums x
let get_constructor_decl ( x : constructor ) = let get_constructor_decl ( x : constructor ) =
let (a, _, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in let (a, _, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in