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 canonical_array_value : Type.t -> Term.t -> Term.t

canonical_array_value ty t is the array value t, a constant array with stores of constant indices and values, as solvers give the value of an array, in a canonical form for the array type ty: two values are equal exactly if their canonical forms are the same term.

A store that an outer store of the same index overrides is dropped, and so is a store of the value of the constant array. Over a finite index type whose indices the stores cover at least half of, the value of the constant array is the most frequent value of the elements. The stores are in the order of their indices. The indices and values are of the types of ty, a range of integers or an enumeration being an integer, as for the solvers: they do not tell signed and unsigned bit-vectors apart. Raises Not_found for a term of another form.

val is_array_value : Term.t -> bool

Whether a term is an array value: a constant array with stores of constant indices and values

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. | RF
    (*

    Recursive function definitions

    *)
  3. | UF
    (*

    Equality over uninterpreted functions

    *)
  4. | A
    (*

    Arrays

    *)
  5. | DT
    (*

    Algebraic datatypes

    *)
  6. | IA
    (*

    Integer arithmetic

    *)
  7. | RA
    (*

    Real arithmetic

    *)
  8. | LA
    (*

    Linear arithmetic

    *)
  9. | NA
    (*

    Non-linear arithmetic

    *)
  10. | 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