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

ML API fix for datatype construction (Issue #121). Thanks to Elarnon for reporting this one!

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-07-24 18:59:03 +01:00
parent a8f703e034
commit 7ec8c81c33
2 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -374,6 +374,10 @@ struct
let sort_lton ( a : sort list ) =
let f ( e : sort ) = match e with Sort(a) -> (AST.ptr_of_ast a) in
Array.of_list (List.map f a)
let sort_option_lton ( a : sort option list ) =
let f ( e : sort option ) = match e with None -> null | Some(Sort(a)) -> (AST.ptr_of_ast a) in
Array.of_list (List.map f a)
let equal : sort -> sort -> bool = fun a b ->
(a == b) ||
@ -1257,7 +1261,7 @@ struct
let _sizes = Hashtbl.create 0
let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort 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
if n != (List.length sorts) then
raise (Z3native.Exception "Number of field names does not match number of sorts")
@ -1269,7 +1273,7 @@ struct
(Symbol.gno recognizer)
n
(Symbol.symbol_lton field_names)
(sort_lton sorts)
(sort_option_lton sorts)
(Array.of_list sort_refs)) in
let no : constructor = { m_ctx = ctx ;
m_n_obj = null ;
@ -1316,11 +1320,11 @@ struct
res
end
let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort list ) ( sort_refs : int list ) =
let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
Constructor.create ctx name recognizer field_names sorts sort_refs
let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort list ) ( sort_refs : int list ) =
let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs
let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : Constructor.constructor list ) =

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

@ -1053,12 +1053,12 @@ sig
(** Create a datatype constructor.
if the corresponding sort reference is 0, then the value in sort_refs should be an index
referring to one of the recursive datatypes that is declared. *)
val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol list -> Sort.sort list -> int list -> Constructor.constructor
val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
(** Create a datatype constructor.
if the corresponding sort reference is 0, then the value in sort_refs should be an index
referring to one of the recursive datatypes that is declared. *)
val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort list -> int list -> Constructor.constructor
val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
(** Create a new datatype sort. *)
val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort