Module Smt.Variant

module Variant: sig .. end

The types of symbols (when they are enumerated data types) can be refined to substypes of their original type (i.e. a subset of their constructors).

val init : (Smt.Symbol.t * Smt.Type.t) list -> unit

init l where l is a list of pairs (s, ty) initializes the type (and associated constructors) of each s to its original type ty.

This function must be called with a list of all symbols before attempting to refine the types.

val close : unit -> unit

close () will compute the smallest type possible for each symbol.

This function must be called when all information has been added.

val assign_constr : Smt.Symbol.t -> Hstring.t -> unit

assign_constr s cstr will add the constraint that the constructor cstr must be in the type of s

val assign_var : Smt.Symbol.t -> Smt.Symbol.t -> unit

assign_var x y will add the constraint that the type of y is a subtype of x (use this function when x := y appear in your program

val print : unit -> unit

print () will output the computed refined types on std_err. This function is here only for debugging purposes. Use it afer close ().

val get_variants : Smt.Symbol.t -> Hstring.HSet.t

get_variants s returns a set of constructors, which is the refined type of s.