From 94a8c271d4fb3c47086dacc27ae789e80867d951 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 24 Jul 2014 19:29:06 +0100 Subject: [PATCH] ML API bugfix for datatype module (Issue #120). Thanks to user Elarnon for reporting this! Signed-off-by: Christoph M. Wintersteiger --- src/api/ml/z3.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index f34ce0ca7..013101398 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -277,7 +277,7 @@ struct 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)) - 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) let erase ( x : ast_map ) ( key : ast ) = @@ -1259,7 +1259,13 @@ struct struct 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 n = (List.length field_names) in @@ -1283,10 +1289,10 @@ struct (z3obj_create no) ; let f = fun o -> Z3native.del_constructor (z3obj_gnc o) (z3obj_gno o) in Gc.finalise f no ; - Hashtbl.add _sizes no n ; + FieldNumTable.add _field_nums no n ; 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 (a, _, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in