Module TermLib

module TermLib: sig .. end
Utilty functions for transition systems

Functions that use term data structures and can be used by any module above TransSys go here.



Default values


val default_of_type : Type.t -> Term.t
Return the default value of the type:

By default, a Boolean value is false, integer and real values are zero, values in a range are equal to the lower bound of the range. Array scalar types do not have defaults. The function fails with Invalid_argument in this case.


Logic fragments


type feature = 
| Q (*
Quantifiers
*)
| UF (*
Equality over uninterpreted functions
*)
| A (*
Arrays
*)
| IA (*
Integer arithmetic
*)
| RA (*
Real arithmetic
*)
| LA (*
Linear arithmetic
*)
| NA (*
Non-linear arithmetic
*)
A feature of a logic fragment for terms
module FeatureSet: Set.S  with type elt = feature
Set of features
type features = FeatureSet.t 
Logic fragments for terms
val sup_logics : features list -> features
Returns the sup of the logics given as arguments
val logic_of_term : Term.t -> features
Returns the logic fragment used by a term
val logic_of_sort : Type.t -> features
Returns the logic fragment of a type
type logic = [ `Inferred of features | `None | `SMTLogic of string ] 
Logic fragments for terms
val pp_print_logic : Format.formatter -> logic -> unit
Print a logic
val string_of_logic : logic -> string
String correspinding to a logic
val logic_allow_arrays : logic -> bool
Returns true if the logic potentially has arrays
module Signals: sig .. end
Gathers signal related stuff.