Module TermLib

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

| BV

Bit vectors

A feature of a logic fragment for terms

module FeatureSet : Stdlib.Set.S with type FeatureSet.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 : UfSymbol.t list -> 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 = [
| `None
| `Inferred of features
| `SMTLogic of string
]

Logic fragments for terms

val pp_print_logic : Stdlib.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.

val add_quantifiers : logic -> logic