module DE = Dolmen.Std.ExprThe purpose of this module is to construct an appropriate total order on constructors of a given ADT to ensure the termination of model generation for this theory.
For each ADT type, we generate a minimal perfect hash function for its set of constructors, that is a bijection between this set on the integer between 0 and n exclusive, where n denotes the number of constructors. The total order on ADT constructors is given by the hash function.
val attach_orders : DE.ty_def list -> unitattach_orders defs generate and attach orders on the constructors for each ADT of defs.
Note: assume that defs is a list of definitions of a complete nest (in any order). By nest, we mean the set of all the constructors in a mutually recursive definition of ADTs.
val perfect_hash : Uid.term_cst -> intperfect_hash u returns an integer between 0 and n exclusive where u is a constructor and n is the number of constructors of the ADT of u.
Invalid_arg if u is not a constructor.