diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 86ed05d98..c780d8cf5 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -216,6 +216,8 @@ sig val to_string : sort -> string val mk_uninterpreted : context -> Symbol.symbol -> sort val mk_uninterpreted_s : context -> string -> sort + val mk_type_variable : context -> Symbol.symbol -> sort + val mk_type_variable_s : context -> string -> sort end = struct type sort = Z3native.sort let gc a = Z3native.context_of_ast a @@ -228,6 +230,8 @@ end = struct let to_string (x:sort) = Z3native.sort_to_string (gc x) x let mk_uninterpreted ctx s = Z3native.mk_uninterpreted_sort ctx s let mk_uninterpreted_s (ctx:context) (s:string) = mk_uninterpreted ctx (Symbol.mk_string ctx s) + let mk_type_variable ctx s = Z3native.mk_type_variable ctx s + let mk_type_variable_s (ctx:context) (s:string) = mk_type_variable ctx (Symbol.mk_string ctx s) end and FuncDecl : @@ -908,6 +912,13 @@ struct let mk_sort_s (ctx:context) (name:string) (constructors:Constructor.constructor list) = mk_sort ctx (Symbol.mk_string ctx name) constructors + let mk_polymorphic_sort (ctx:context) (name:Symbol.symbol) (type_params:Sort.sort list) (constructors:Constructor.constructor list) = + let (x,_) = Z3native.mk_polymorphic_datatype ctx name (List.length type_params) type_params (List.length constructors) constructors in + x + + let mk_polymorphic_sort_s (ctx:context) (name:string) (type_params:Sort.sort list) (constructors:Constructor.constructor list) = + mk_polymorphic_sort ctx (Symbol.mk_string ctx name) type_params constructors + let mk_sort_ref (ctx: context) (name:Symbol.symbol) = Z3native.mk_datatype_sort ctx name 0 [] diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 6764b0e2d..203f8f8cb 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -290,6 +290,12 @@ sig (** Create a new uninterpreted sort. *) val mk_uninterpreted_s : context -> string -> sort + + (** Create a type variable sort for use in polymorphic datatypes. *) + val mk_type_variable : context -> Symbol.symbol -> sort + + (** Create a type variable sort for use in polymorphic datatypes. *) + val mk_type_variable_s : context -> string -> sort end (** Function declarations *) @@ -1099,6 +1105,14 @@ sig (** Create a new datatype sort. *) val mk_sort_s : context -> string -> Constructor.constructor list -> Sort.sort + (** Create a new polymorphic datatype sort with type parameters. + Type parameters should be created using Sort.mk_type_variable. *) + val mk_polymorphic_sort : context -> Symbol.symbol -> Sort.sort list -> Constructor.constructor list -> Sort.sort + + (** Create a new polymorphic datatype sort with type parameters. + Type parameters should be created using Sort.mk_type_variable. *) + val mk_polymorphic_sort_s : context -> string -> Sort.sort list -> Constructor.constructor list -> Sort.sort + (** Create mutually recursive datatypes. *) val mk_sorts : context -> Symbol.symbol list -> Constructor.constructor list list -> Sort.sort list