package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module defines the builtins that are defined by Dolmen.

Builtins are particularly used in typed expressions see Dolmen.Std.Expr, in order to give more information about constants which have builtin semantics.

Users are encouraged to match builtins rather than specific symbols when inspecting typed expressions, as this basically allows to match on the semantics of an identifier rather than matching on the syntaxic value of an identifier. For instance, equality can take an arbitrary number of arguments, and thus in order to have well-typed terms, each arity of equality gives rise to a different symbol (because the symbol's type depends on the arity desired), but all these symbols have the Equal builtin.

In the following we will use pseudo-code to describe the arity and actual type associated to builtins. These will follow ocaml's notation for types with an additional syntax using dots for arbitrary arity. Some examples:

  • ttype is a type constant
  • ttype -> ttype is a type constructor (e.g. list)
  • int is a constant of type int
  • float -> int is a unary function
  • 'a. 'a -> 'a is a polymorphic unary function
  • 'a. 'a -> ... -> Prop describes a family of functions that take a type and then an arbitrary number of arguments of that type, and return a proposition (this is for instance the type of equality).

Additionally, due to some languages having overloaded operators, and in order to not have too verbose names, some of these builtins may have overloaded signtures, such as comparisons on numbers which can operate on integers, rationals, or reals. Note that arbitrary arity operators (well family of operators) can be also be seen as overloaded operators. Overloaded types (particularly for numbers) are written:

  • {a=(Int|Rational|Real)} a -> a -> Prop, where the notable difference with polymorphic functions is that functions of this type does not take a type argument.

Type definition

type 'a t = .. constraint 'a = < .. >

Base Builtins

type t +=
  1. | Base
    (*

    The base builtin; it is the default builtin for identifiers.

    *)
type t +=
  1. | Wildcard : {
    1. ty : 'ty option ref;
    } -> < ty : 'ty.. > t
    (*

    Wildcards, currently used internally to represent implicit type variables during type-checking.

    *)
type t +=
  1. | Kind
    (*

    Used for the type of Type. It is an error to try and access the type of kind.

    *)
  2. | Type
    (*

    Builtin used to represent the type of types.

    *)
  3. | Prop
    (*

    Prop: ttype: the builtin type constant for the type of propositions / booleans.

    *)
type t +=
  1. | Unit
    (*

    The unit type, which has only one element (named void).

    *)
  2. | Univ
    (*

    Univ: ttype: a builtin type constant used for languages with a default type for elements (such as tptp's `$i`).

    *)
type t +=
  1. | Coercion
    (*

    Coercion: 'a 'b. 'a -> 'b: Coercion/cast operator, i.e. allows to cast values of some type to another type. This is a polymorphic operator that takes two type arguments a and b, a value of type a, and returns a value of type b. The interpretation/semantics of this cast can remain up to the user. This operator is currently mainly used to cast numeric types when this transormation is exact (i.e. an integer casted into a rational, which is always possible and exact, or the cast of a rational into an integer, as long as the cast is guarded by a clause verifying the rational is an integer).

    *)
type t +=
  1. | In_interval of bool * bool
    (*

    In_interval (b1, b2): Int -> Int -> Int -> Prop: Tests whether or not an interger is in an interval, b1 (resp. b2) determines if the interval is open on the lower bound (resp. upper bound).

    warning: It is an Alt-Ergo semantic trigger that should only be allowed inside theories.

    *)
  2. | Maps_to
    (*

    Maps_to: 'term_var -> 'term -> 'term: Used in semantic triggers for floating point arithmetic. See alt-ergo/src/preludes/fpa-theory-2017-01-04-16h00.ae.

    warning: It is an Alt-Ergo semantic trigger that should only be allowed inside theories.

    *)

Boolean Builtins

type t +=
  1. | True
    (*

    True: Prop: the true proposition.

    *)
  2. | False
    (*

    False: Prop: the false proposition.

    *)
  3. | Equal
    (*

    Equal: 'a. 'a -> ... -> Prop: equality beetween values.

    *)
  4. | Distinct
    (*

    Distinct: 'a. 'a -> ... -> Prop: pairwise dis-equality beetween arguments.

    *)
  5. | Neg
    (*

    Neg: Prop -> Prop: propositional negation.

    *)
  6. | And
    (*

    And: Prop -> Prop: propositional conjunction.

    *)
  7. | Or
    (*

    Or: Prop -> ... -> Prop: propositional disjunction.

    *)
  8. | Nand
    (*

    Nand: Prop -> Prop -> Prop: propositional negated conjunction.

    *)
  9. | Nor
    (*

    Nor: Prop -> Prop -> Prop: propositional negated disjunction.

    *)
  10. | Xor
    (*

    Xor: Prop -> Prop -> Prop: ppropositional exclusive disjunction.

    *)
  11. | Imply
    (*

    Imply: Prop -> Prop -> Prop: propositional implication.

    *)
  12. | Implied
    (*

    Implied: Prop -> Prop -> Prop: reverse propositional implication.

    *)
  13. | Equiv
    (*

    Equiv: Prop -> Prop -> Prop: propositional Equivalence.

    *)
type t +=
  1. | Ite
    (*

    Ite: 'a. Prop -> 'a -> 'a -> 'a: branching operator.

    *)
type t +=
  1. | Pi
    (*

    Pi: 'a. ('a -> Prop) -> Prop: higher-order encoding of universal quantification.

    *)
  2. | Sigma
    (*

    Sigma: 'a. ('a -> Prop) -> Prop: higher-order encoding of existencial quantification.

    *)

Algebraic datatype Builtins

type t +=
  1. | Tester : {
    1. adt : 'ty_cst;
    2. case : int;
    3. cstr : 'term_cst;
    } -> < ty_cst : 'ty_cst ; term_cst : 'term_cst.. > t
    (*

    Tester { adt; cstr; case; } is the tester of the case-th constructor of type adt which should be cstr.

    *)
  2. | Constructor : {
    1. adt : 'ty_cst;
    2. case : int;
    } -> < ty_cst : 'ty_cst.. > t
    (*

    Constructor { adt; case} is the case-th constructor of the algebraic datatype defined by adt.

    *)
  3. | Destructor : {
    1. adt : 'ty_cst;
    2. case : int;
    3. cstr : 'term_cst;
    4. field : int;
    } -> < ty_cst : 'ty_cst ; term_cst : 'term_cst.. > t
    (*

    Destructor { adt; cstr; case; field; } is the destructor returning the field-th argument of the case-th constructor of type adt which should be cstr.

    *)

Arithmetic Builtins

type t +=
  1. | Int
    (*

    Int: ttype the type for signed integers of arbitrary precision.

    *)
  2. | Integer of string
    (*

    Integer s: Int: integer litteral. The string s should be the decimal representation of an integer with arbitrary precision (hence the use of strings rather than the limited precision int).

    *)
  3. | Rat
    (*

    Rat: ttype the type for signed rationals.

    *)
  4. | Rational of string
    (*

    Rational s: Rational: rational litteral. The string s should be the decimal representation of a rational (see the various languages spec for more information).

    *)
  5. | Real
    (*

    Real: ttype the type for signed reals.

    *)
  6. | Decimal of string
    (*

    Decimal s: Real: real litterals. The string s should be a floating point representatoin of a real. Not however that reals here means the mathematical abstract notion of real numbers, including irrational, non-algebric numbers, and is thus not restricted to floating point numbers, although these are the only litterals supported.

    *)
  7. | Lt
    (*

    Lt: {a=(Int|Rational|Real)} a -> a -> Prop: strict comparison (less than) on numbers (whether integers, rationals, or reals).

    *)
  8. | Leq
    (*

    Leq:{a=(Int|Rational|Real)} a -> a -> Prop: large comparison (less or equal than) on numbers (whether integers, rationals, or reals).

    *)
  9. | Gt
    (*

    Gt:{a=(Int|Rational|Real)} a -> a -> Prop: strict comparison (greater than) on numbers (whether integers, rationals, or reals).

    *)
  10. | Geq
    (*

    Geq:{a=(Int|Rational|Real)} a -> a -> Prop: large comparison (greater or equal than) on numbers (whether integers, rationals, or reals).

    *)
  11. | Minus
    (*

    Minus:{a=(Int|Rational|Real)} a -> a: arithmetic unary negation/minus on numbers (whether integers, rationals, or reals).

    *)
  12. | Add
    (*

    Add:{a=(Int|Rational|Real)} a -> a -> a: arithmetic addition on numbers (whether integers, rationals, or reals).

    *)
  13. | Sub
    (*

    Sub:{a=(Int|Rational|Real)} a -> a -> a: arithmetic substraction on numbers (whether integers, rationals, or reals).

    *)
  14. | Mul
    (*

    Mul:{a=(Int|Rational|Real)} a -> a -> a: arithmetic multiplication on numbers (whether integers, rationals, or reals).

    *)
  15. | Pow
    (*

    Pow:{a=(Int|Rational|Real)} a -> a -> a: arithmetic exponentiation on numbers (whether integers, rationals, or reals).

    *)
  16. | Div
    (*

    Div:{a=(Rational|Real)} a -> a -> a: arithmetic exact division on numbers (rationals, or reals, but **not** integers).

    *)
  17. | Div_e
    (*

    Div_e:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer euclidian quotient (whether integers, rationals, or reals). If D is positive then Div_e (N,D) is the floor (in the type of N and D) of the real division N/D, and if D is negative then Div_e (N,D) is the ceiling of N/D.

    *)
  18. | Div_t
    (*

    Div_t:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer truncated quotient (whether integers, rationals, or reals). Div_t (N,D) is the truncation of the real division N/D.

    *)
  19. | Div_f
    (*

    Div_f:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer floor quotient (whether integers, rationals, or reals). Div_t (N,D) is the floor of the real division N/D.

    *)
  20. | Modulo_e
    (*

    Modulo_e:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer euclidian remainder (whether integers, rationals, or reals). It is defined by the following equation: Div_e (N, D) * D + Modulo(N, D) = N.

    *)
  21. | Modulo_t
    (*

    Modulo_t:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer truncated remainder (whether integers, rationals, or reals). It is defined by the following equation: Div_t (N, D) * D + Modulo_t(N, D) = N.

    *)
  22. | Modulo_f
    (*

    Modulo_f:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer floor remainder (whether integers, rationals, or reals). It is defined by the following equation: Div_f (N, D) * D + Modulo_f(N, D) = N.

    *)
  23. | Abs
    (*

    Abs: Int -> Int: absolute value on integers.

    *)
  24. | Divisible
    (*

    Divisible: Int -> Int -> Prop: divisibility predicate on integers. Smtlib restricts applications of this predicate to have a litteral integer for the divisor/second argument.

    *)
  25. | Is_int
    (*

    Is_int:{a=(Int|Rational|Real)} a -> Prop: integer predicate for numbers: is the given number an integer.

    *)
  26. | Is_rat
    (*

    Is_rat:{a=(Int|Rational|Real)} a -> Prop: rational predicate for numbers: is the given number an rational.

    *)
  27. | Floor
    (*

    Floor:{a=(Int|Rational|Real)} a -> a: floor function on numbers, defined in tptp as the largest integer not greater than the argument.

    *)
  28. | Floor_to_int
    (*

    Floor_to_int:{a=(Rational|Real)} a -> Int: floor and conversion to integers in a single funciton. Should return the greatest integer i such that the rational or real intepretation of i is less than, or equal to, the argument.

    *)
  29. | Ceiling
    (*

    Ceiling:{a=(Int|Rational|Real)} a -> a: ceiling function on numbers, defined in tptp as the smallest integer not less than the argument.

    *)
  30. | Truncate
    (*

    Truncate:{a=(Int|Rational|Real)} a -> a: ceiling function on numbers, defined in tptp as the nearest integer value with magnitude not greater than the absolute value of the argument.

    *)
  31. | Round
    (*

    Round:{a=(Int|Rational|Real)} a -> a: rounding function on numbers, defined in tptp as the nearest intger to the argument; when the argument is halfway between two integers, the nearest even integer to the argument.

    *)

Arrays Builtins

type t +=
  1. | Array
    (*

    Array: ttype -> ttype -> ttype: the type constructor for polymorphic functional arrays. An (src, dst) Array is an array from expressions of type src to expressions of type dst. Typically, such arrays are immutables.

    *)
  2. | Store
    (*

    Store: 'a 'b. ('a, 'b) Array -> 'a -> 'b -> ('a, 'b) Array: store operation on arrays. Returns a new array with the key bound to the given value (shadowing the previous value associated to the key).

    *)
  3. | Select
    (*

    Select: 'a 'b. ('a, 'b) Array -> 'a -> 'b: select operation on arrays. Returns the value associated to the given key. Typically, functional arrays are complete, i.e. all keys are mapped to a value.

    *)

Bitvectors Builtins

type t +=
  1. | Bitv of int
    (*

    Bitv n: ttype: type constructor for bitvectors of length n.

    *)
  2. | Bitvec of string
    (*

    Bitvec s: Bitv: bitvector litteral. The string s should be a binary representation of bitvectors using characters '0', and '1' (lsb last)

    *)
  3. | Bitv_concat of {
    1. n : int;
    2. m : int;
    }
    (*

    Bitv_concat(n,m): Bitv(n) -> Bitv(m) -> Bitv(n+m): concatenation operator on bitvectors.

    *)
  4. | Bitv_extract of {
    1. n : int;
    2. i : int;
    3. j : int;
    }
    (*

    Bitv_extract(n, i, j): Bitv(n) -> Bitv(i - j + 1): bitvector extraction, from index j up to i (both included).

    *)
  5. | Bitv_repeat of {
    1. n : int;
    2. k : int;
    }
    (*

    Bitv_repeat(n,k): Bitv(n) -> Bitv(n*k): bitvector repeatition.

    *)
  6. | Bitv_zero_extend of {
    1. n : int;
    2. k : int;
    }
    (*

    Bitv_zero_extend(n,k): Bitv(n) -> Bitv(n + k): zero extension for bitvectors (produces a representation of the same unsigned integer).

    *)
  7. | Bitv_sign_extend of {
    1. n : int;
    2. k : int;
    }
    (*

    Bitv_sign_extend(n,k): Bitv(n) -> Bitv(n + k): sign extension for bitvectors ((produces a representation of the same signed integer).

    *)
  8. | Bitv_rotate_right of {
    1. n : int;
    2. i : int;
    }
    (*

    Bitv_rotate_right(n,i): Bitv(n) -> Bitv(n): logical rotate right for bitvectors by i.

    *)
  9. | Bitv_rotate_left of {
    1. n : int;
    2. i : int;
    }
    (*

    Bitv_rotate_left(n,i): Bitv(n) -> Bitv(n): logical rotate left for bitvectors by i.

    *)
  10. | Bitv_not of int
    (*

    Bitv_not(n): Bitv(n) -> Bitv(n): bitwise negation for bitvectors.

    *)
  11. | Bitv_and of int
    (*

    Bitv_and(n): Bitv(n) -> Bitv(n) -> Bitv(n): bitwise conjunction for bitvectors.

    *)
  12. | Bitv_or of int
    (*

    bitv_or(n): Bitv(n) -> Bitv(n) -> Bitv(n): bitwise disjunction for bitvectors.

    *)
  13. | Bitv_nand of int
    (*

    Bitv_nand(n): Bitv(n) -> Bitv(n) -> Bitv(n): bitwise negated conjunction for bitvectors. Bitv_nand s t abbreviates Bitv_not (Bitv_and s t)).

    *)
  14. | Bitv_nor of int
    (*

    Bitv_nor(n): Bitv(n) -> Bitv(n) -> Bitv(n): bitwise negated disjunction for bitvectors. Bitv_nor s t abbreviates Bitv_not (Bitv_or s t)).

    *)
  15. | Bitv_xor of int
    (*

    Bitv_xor(n): Bitv(n) -> Bitv(n) -> Bitv(n): bitwise exclusive disjunction for bitvectors. Bitv_xor s t abbreviates Bitv_or (Bitv_and s (Bitv_not t)) (Bitv_and (Bitv_not s) t) .

    *)
  16. | Bitv_xnor of int
    (*

    Bitv_xnor(n): Bitv(n) -> Bitv(n) -> Bitv(n): bitwise negated exclusive disjunction for bitvectors. Bitv_xnor s t abbreviates Bitv_or (Bitv_and s t) (Bitv_and (Bitv_not s) (Bitv_not t)).

    *)
  17. | Bitv_comp of int
    (*

    Bitv_comp(n): Bitv(n) -> Bitv(n) -> Bitv(1): Returns the constant bitvector "1" is all bits are equal, and the bitvector "0" if not.

    *)
  18. | Bitv_neg of int
    (*

    Bitv_neg(n): Bitv(n) -> Bitv(n): 2's complement unary minus.

    *)
  19. | Bitv_add of int
    (*

    Bitv_add(n): Bitv(n) -> Bitv(n) -> Bitv(n): addition modulo 2^n.

    *)
  20. | Bitv_sub of int
    (*

    Bitv_sub(n): Bitv(n) -> Bitv(n) -> Bitv(n): 2's complement subtraction modulo 2^n.

    *)
  21. | Bitv_mul of int
    (*

    Bitv_mul(n): Bitv(n) -> Bitv(n) -> Bitv(n): multiplication modulo 2^n.

    *)
  22. | Bitv_udiv of int
    (*

    Bitv_udiv(n): Bitv(n) -> Bitv(n) -> Bitv(n): unsigned division, truncating towards 0.

    *)
  23. | Bitv_urem of int
    (*

    Bitv_urem(n): Bitv(n) -> Bitv(n) -> Bitv(n): unsigned remainder from truncating division.

    *)
  24. | Bitv_sdiv of int
    (*

    Bitv_sdiv(n): Bitv(n) -> Bitv(n) -> Bitv(n): 2's complement signed division.

    *)
  25. | Bitv_srem of int
    (*

    Bitv_srem(n): Bitv(n) -> Bitv(n) -> Bitv(n): 2's complement signed remainder (sign follows dividend).

    *)
  26. | Bitv_smod of int
    (*

    Bitv_smod(n): Bitv(n) -> Bitv(n) -> Bitv(n): 2's complement signed remainder (sign follows divisor).

    *)
  27. | Bitv_shl of int
    (*

    Bitv_shl(n): Bitv(n) -> Bitv(n) -> Bitv(n): shift left (equivalent to multiplication by 2^x where x is the value of the second argument).

    *)
  28. | Bitv_lshr of int
    (*

    Bitv_lshr(n): Bitv(n) -> Bitv(n) -> Bitv(n): logical shift right (equivalent to unsigned division by 2^x, where x is the value of the second argument).

    *)
  29. | Bitv_ashr of int
    (*

    Bitv_ashr(n): Bitv(n) -> Bitv(n) -> Bitv(n): Arithmetic shift right, like logical shift right except that the most significant bits of the result always copy the most significant bit of the first argument.

    *)
  30. | Bitv_ult of int
    (*

    Bitv_ult(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for unsigned less-than.

    *)
  31. | Bitv_ule of int
    (*

    Bitv_ule(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for unsigned less than or equal.

    *)
  32. | Bitv_ugt of int
    (*

    Bitv_ugt(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for unsigned greater-than.

    *)
  33. | Bitv_uge of int
    (*

    Bitv_uge(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for unsigned greater than or equal.

    *)
  34. | Bitv_slt of int
    (*

    Bitv_slt(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for signed less-than.

    *)
  35. | Bitv_sle of int
    (*

    Bitv_sle(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for signed less than or equal.

    *)
  36. | Bitv_sgt of int
    (*

    Bitv_sgt(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for signed greater-than.

    *)
  37. | Bitv_sge of int
    (*

    Bitv_sge(n): Bitv(n) -> Bitv(n) -> Prop: binary predicate for signed greater than or equal.

    *)

Floats Builtins

type t +=
  1. | RoundingMode
    (*

    RoundingMode: ttype: type for enumerated type of rounding modes.

    *)
  2. | RoundNearestTiesToEven
    (*

    RoundNearestTiesToEven : RoundingMode:

    *)
  3. | RoundNearestTiesToAway
    (*

    RoundNearestTiesToAway : RoundingMode:

    *)
  4. | RoundTowardPositive
    (*

    RoundTowardPositive : RoundingMode

    *)
  5. | RoundTowardNegative
    (*

    RoundTowardNegative : RoundingMode

    *)
  6. | RoundTowardZero
    (*

    RoundTowardZero : RoundingMode

    *)
  7. | Float of int * int
    (*

    Float(e,s): ttype: type constructor for floating point of exponent of size e and significand of size s (hidden bit included). Those size are greater than 1

    *)
  8. | Fp of int * int
    (*

    Fp(e, s): Bitv(1) -> Bitv(e) -> Bitv(s-1) -> Fp(e,s): bitvector literal. The IEEE-format is used for the conversion sb^se^ss. All the NaN are converted to the same value.

    *)
  9. | Plus_infinity of int * int
    (*

    Plus_infinity(s,e) : Fp(s,e)

    *)
  10. | Minus_infinity of int * int
    (*

    Minus_infinity(s,e) : Fp(s,e)

    *)
  11. | Plus_zero of int * int
    (*

    Plus_zero(s,e) : Fp(s,e)

    *)
  12. | Minus_zero of int * int
    (*

    Minus_zero(s,e) : Fp(s,e)

    *)
  13. | NaN of int * int
    (*

    NaN(s,e) : Fp(s,e)

    *)
  14. | Fp_abs of int * int
    (*

    Fp_abs(s,e): Fp(s,e) -> Fp(s,e): absolute value

    *)
  15. | Fp_neg of int * int
    (*

    Fp_neg(s,e): Fp(s,e) -> Fp(s,e): negation

    *)
  16. | Fp_add of int * int
    (*

    Fp_add(s,e): RoundingMode -> Fp(s,e) -> Fp(s,e) -> Fp(s,e): addition

    *)
  17. | Fp_sub of int * int
    (*

    Fp_sub(s,e): RoundingMode -> Fp(s,e) -> Fp(s,e) -> Fp(s,e): subtraction

    *)
  18. | Fp_mul of int * int
    (*

    Fp_mul(s,e): RoundingMode -> Fp(s,e) -> Fp(s,e) -> Fp(s,e): multiplication

    *)
  19. | Fp_div of int * int
    (*

    Fp_div(s,e): RoundingMode -> Fp(s,e) -> Fp(s,e) -> Fp(s,e): division

    *)
  20. | Fp_fma of int * int
    (*

    Fp_fma(s,e): RoundingMode -> Fp(s,e) -> Fp(s,e): fuse multiply add

    *)
  21. | Fp_sqrt of int * int
    (*

    Fp_sqrt(s,e): RoundingMode -> Fp(s,e) -> Fp(s,e): square root

    *)
  22. | Fp_rem of int * int
    (*

    Fp_rem(s,e): Fp(s,e) -> Fp(s,e) -> Fp(s,e): remainder

    *)
  23. | Fp_roundToIntegral of int * int
    (*

    Fp_roundToIntegral(s,e): RoundingMode -> Fp(s,e) -> Fp(s,e): round to integral

    *)
  24. | Fp_min of int * int
    (*

    Fp_min(s,e): Fp(s,e) -> Fp(s,e) -> Fp(s,e): minimum

    *)
  25. | Fp_max of int * int
    (*

    Fp_max(s,e): Fp(s,e) -> Fp(s,e) -> Fp(s,e): maximum

    *)
  26. | Fp_leq of int * int
    (*

    Fp_leq(s,e): Fp(s,e) -> Fp(s,e) -> Prop: IEEE less or equal

    *)
  27. | Fp_lt of int * int
    (*

    Fp_lt(s,e): Fp(s,e) -> Fp(s,e) -> Prop: IEEE less than

    *)
  28. | Fp_geq of int * int
    (*

    Fp_geq(s,e): Fp(s,e) -> Fp(s,e) -> Prop: IEEE greater or equal

    *)
  29. | Fp_gt of int * int
    (*

    Fp_gt(s,e): Fp(s,e) -> Fp(s,e) -> Prop: IEEE greater than

    *)
  30. | Fp_eq of int * int
    (*

    Fp_eq(s,e): Fp(s,e) -> Fp(s,e) -> Prop: IEEE equality

    *)
  31. | Fp_isNormal of int * int
    (*

    Fp_isNormal(s,e): Fp(s,e) -> Prop: test if it is a normal floating point

    *)
  32. | Fp_isSubnormal of int * int
    (*

    Fp_isSubnormal(s,e): Fp(s,e) -> Prop: test if it is a subnormal floating point

    *)
  33. | Fp_isZero of int * int
    (*

    Fp_isZero(s,e): Fp(s,e) -> Prop: test if it is a zero

    *)
  34. | Fp_isInfinite of int * int
    (*

    Fp_isInfinite(s,e): Fp(s,e) -> Prop: test if it is an infinite

    *)
  35. | Fp_isNaN of int * int
    (*

    Fp_isNaN(s,e): Fp(s,e) -> Prop: test if it is Not a Number

    *)
  36. | Fp_isNegative of int * int
    (*

    Fp_isNegative(s,e): Fp(s,e) -> Prop: test if it is negative

    *)
  37. | Fp_isPositive of int * int
    (*

    Fp_isPositive(s,e): Fp(s,e) -> Prop: test if it is positive

    *)
  38. | Ieee_format_to_fp of int * int
    (*

    Ieee_format_to_fp(s,e): Bv(s+e) -> Fp(s,e): Convert from IEEE interchange format

    *)
  39. | Fp_to_fp of int * int * int * int
    (*

    Fp_to_fp(s1,e1,s2,e2): RoundingMode -> Fp(s1,e1) -> Fp(s2,e2): Convert from another floating point format

    *)
  40. | Real_to_fp of int * int
    (*

    Real_to_fp(s,e): RoundingMode -> Real -> Fp(s,e): Convert from a real

    *)
  41. | Sbv_to_fp of int * int * int
    (*

    Sbv_to_fp(m,s,e): RoundingMode -> Bitv(m) -> Fp(s,e): Convert from a signed integer

    *)
  42. | Ubv_to_fp of int * int * int
    (*

    Ubv_to_fp(m,s,e): RoundingMode -> Bitv(m) -> Fp(s,e): Convert from a unsigned integer

    *)
  43. | To_ubv of int * int * int
    (*

    To_ubv(s,e,m): RoundingMode -> Fp(s,e) -> Bitv(m): Convert to an unsigned integer

    *)
  44. | To_sbv of int * int * int
    (*

    To_ubv(s,e,m): RoundingMode -> Fp(s,e) -> Bitv(m): Convert to an signed integer

    *)
  45. | To_real of int * int
    (*

    To_real(s,e): Fp(s,e) -> Real: Convert to real

    *)

String and Regexp Builtins

type t +=
  1. | String
    (*

    String: ttype: type constructor for strings.

    *)
  2. | Str of string
    (*

    Str s: String: string literals.

    *)
  3. | Str_length
    (*

    Str_length: String -> Int: string length.

    *)
  4. | Str_at
    (*

    Str_at: String -> Int -> String: Singleton string containing a character at given position or empty string when position is out of range. The leftmost position is 0.

    *)
  5. | Str_to_code
    (*

    Str_to_code: String -> Int: Str_to_code s is the code point of the only character of s, if s is a singleton string; otherwise, it is -1.

    *)
  6. | Str_of_code
    (*

    Str_of_code: Int -> String: Str_of_code n is the singleton string whose only character is code point n if n is in the range 0, 196607; otherwise, it is the empty string.

    *)
  7. | Str_is_digit
    (*

    Str_is_digit: String -> Prop: Digit check Str.is_digit s is true iff s consists of a single character which is a decimal digit, that is, a code point in the range 0x0030 ... 0x0039.

    *)
  8. | Str_to_int
    (*

    Str_to_int: String -> Int: Conversion to integers Str.to_int s with s consisting of digits (in the sense of str.is_digit) evaluates to the positive integer denoted by s when seen as a number in base 10 (possibly with leading zeros). It evaluates to -1 if s is empty or contains non-digits.

    *)
  9. | Str_of_int
    (*

    Str_of_int : Int -> String: Conversion from integers. Str.from_int n with n non-negative is the corresponding string in decimal notation, with no leading zeros. If n < 0, it is the empty string.

    *)
  10. | Str_concat
    (*

    Str_concat: String -> String -> String: string concatenation.

    *)
  11. | Str_sub
    (*

    Str_sub: String -> Int -> Int -> String: Str_sub s i n evaluates to the longest (unscattered) substring of s of length at most n starting at position i. It evaluates to the empty string if n is negative or i is not in the interval 0,l-1 where l is the length of s.

    *)
  12. | Str_index_of
    (*

    Str_index_of: String -> String -> Int -> Int: Index of first occurrence of second string in first one starting at the position specified by the third argument. Str_index_of s t i, with 0 <= i <= |s| is the position of the first occurrence of t in s at or after position i, if any. Otherwise, it is -1. Note that the result is i whenever i is within the range 0, |s| and t is empty.

    *)
  13. | Str_replace
    (*

    Str_replace: String -> String -> String -> String: Replace Str_replace s t t' is the string obtained by replacing the first occurrence of t in s, if any, by t'. Note that if t is empty, the result is to prepend t' to s; also, if t does not occur in s then the result is s.

    *)
  14. | Str_replace_all
    (*

    Str_replace_all: String -> String -> String -> String: Str_replace_all s t t’ is s if t is the empty string. Otherwise, it is the string obtained from s by replacing all occurrences of t in s by t’, starting with the first occurrence and proceeding in left-to-right order.

    *)
  15. | Str_replace_re
    (*

    Str_replace_re: String -> String_RegLan -> String -> String: Str_replace_re s r t is the string obtained by replacing the shortest leftmost non-empty match of r in s, if any, by t. Note that if t is empty, the result is to prepend t to s.

    *)
  16. | Str_replace_re_all
    (*

    Str_replace_re_all: String -> String_RegLan -> String -> String: Str_replace_re_all s r t is the string obtained by replacing, left-to right, each shortest *non-empty* match of r in s by t.

    *)
  17. | Str_is_prefix
    (*

    Str_is_prefix: String -> String -> Prop: Prefix check Str_is_prefix s t is true iff s is a prefix of t.

    *)
  18. | Str_is_suffix
    (*

    Str_is_suffix: String -> String -> Prop: Suffix check Str_is_suffix s t is true iff s is a suffix of t.

    *)
  19. | Str_contains
    (*

    Str_contains: String -> String -> Prop: Inclusion check Str_contains s t is true iff s contains t.

    *)
  20. | Str_lexicographic_strict
    (*

    Str_lexicographic_strict: String -> String -> Prop: lexicographic ordering (strict).

    *)
  21. | Str_lexicographic_large
    (*

    Str_lexicographic_large: String -> String -> Prop: reflexive closure of the lexicographic ordering.

    *)
  22. | Str_in_re
    (*

    Str_in_re: String -> String_RegLan -> Prop: set membership.

    *)
type t +=
  1. | String_RegLan
    (*

    String_RegLan: ttype: type constructor for Regular languages over strings.

    *)
  2. | Re_empty
    (*

    Re_empty: String_RegLan: the empty language.

    *)
  3. | Re_all
    (*

    Re_all: String_RegLan: the language of all strings.

    *)
  4. | Re_allchar
    (*

    Re_allchar: String_RegLan: the language of all singleton strings.

    *)
  5. | Re_of_string
    (*

    Re_of_string: String -> String_RegLan: the singleton language with a single string.

    *)
  6. | Re_range
    (*

    Re_range: String -> String -> String_RegLan: Language range Re_range s1 s2 is the set of all *singleton* strings s such that Str_lexicographic_large s1 s s2 provided s1 and s1 are singleton. Otherwise, it is the empty language.

    *)
  7. | Re_concat
    (*

    Re_concat: String_RegLan -> String_RegLan -> String_RegLan: language concatenation.

    *)
  8. | Re_union
    (*

    Re_union: String_RegLan -> String_RegLan -> String_RegLan: language union.

    *)
  9. | Re_inter
    (*

    Re_inter: String_RegLan -> String_RegLan -> String_RegLan: language intersection.

    *)
  10. | Re_star
    (*

    Re_star: String_RegLan -> String_RegLan: Kleen star.

    *)
  11. | Re_cross
    (*

    Re_cross: String_RegLan -> String_RegLan: Kleen cross.

    *)
  12. | Re_complement
    (*

    Re_complement: String_RegLan -> String_RegLan: language complement.

    *)
  13. | Re_diff
    (*

    Re_diff: String_RegLan -> String_RegLan -> String_RegLan: language difference.

    *)
  14. | Re_option
    (*

    Re_option: String_RegLan -> String_RegLan: language option Re_option e abbreviates Re_union e (Str_to_re "").

    *)
  15. | Re_power of int
    (*

    Re_power(n): String_RegLan -> String_RegLan: Re_power(n) e is the nth power of e:

    • Re_power(0) e is Str_to_re ""
    • Re_power(n+1) e is Re_concat e (Re_power(n) e)
    *)
  16. | Re_loop of int * int
    (*

    Re_loop(n1,n2): String_RegLan -> String_RegLan: Defined as:

    • Re_loop(n₁, n₂) e is Re_empty if n₁ > n₂
    • Re_loop(n₁, n₂) e is Re_power(n₁) e if n₁ = n₂
    • Re_loop(n₁, n₂) e is Re_union ((Re_power(n₁) e) ... (Re_power(n₂) e)) if n₁ < n₂
    *)