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. Values of an abstract type default to a canonical free constant of that type (see abstract_type_default). Array types do not have defaults. The function fails with Invalid_argument in this case.

val abstract_type_default : string -> Type.t -> Var.t

abstract_type_default name ty returns the canonical free constant used as the default value for the abstract type ty named name. The same constant is returned for every call with the same name (from any caller), and it must be declared as a free constant of the transition system by the front end that first introduces the abstract type.

Logic fragments

type feature =
  1. | Q
    (*

    Quantifiers

    *)
  2. | UF
    (*

    Equality over uninterpreted functions

    *)
  3. | A
    (*

    Arrays

    *)
  4. | DT
    (*

    Algebraic datatypes

    *)
  5. | IA
    (*

    Integer arithmetic

    *)
  6. | RA
    (*

    Real arithmetic

    *)
  7. | LA
    (*

    Linear arithmetic

    *)
  8. | NA
    (*

    Non-linear arithmetic

    *)
  9. | BV
    (*

    Bit vectors

    *)

A feature of a logic fragment for terms

module FeatureSet : Stdlib.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 : 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 = [
  1. | `None
  2. | `Inferred of features
  3. | `SMTLogic of string
]

Logic fragments for terms

val pp_print_logic : ?enforce_logic:bool -> Stdlib.Format.formatter -> logic -> unit

Print a logic

val string_of_logic : ?enforce_logic:bool -> 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