Theories

Alt-Ergo has built-in support for many different theories.

Those theories allow to reason about values of various types. To learn more about the syntax and semantic of those types, as well as operators defined on them, please refer to section Types.

Native theories

Alt-Ergo works using a polymorphic first-order logic. A precise definition of what is meant here by ‘theory’ can be found in the second chapter of this thesis.

Alt-Ergo currently provides built-in support for the following theories.

  • The free theory of equality with uninterpreted symbols

  • Associative and commutative (AC) symbols

  • Linear arithmetic over integers and rationals

  • (Fragment of) non-linear arithmetic

  • Floating-point arithmetic (as an extension)

  • Enumerated datatypes

  • Record datatypes

  • Polymorphic functional arrays

  • Fixed-size bitvectors

Theories that can be built upon in user-defined extensions are named in the following way. All theories are always considered modulo equality.

  • SUM: Enumerated datatypes

  • Adt: Algebraic datatypes

  • Arrays: Polymorphic functional arrays

  • Records: Record datatypes

  • Bitv: Fixed-size bitvectors

  • LIA: Linear arithmetic over integers

  • LRA: Linear arithmetic over rationals

  • NIA: Non-linear arithmetic over integers

  • NRA: Non-linear arithmetic over rationals

  • FPA: Floating-point arithmetic

About floating-point arithmetic

Floating-point arithmetic (FPA) is a recent addition to Alt-Ergo, and is not documented here. To use it, it is necessary to load the corresponding prelude. The strategy used to handle FPA is based on over-approximation by intervals of reals, and roundings. More information on this strategy and the language extension can be found in this article.

User-defined extensions of theories

[TODO: document]

theory [...] extends [...] = [...] end

case_split

Semantic triggers

In addition to syntactic triggers (or triggers) and interval triggers (or filters) defined in section Axioms, additional triggers are available inside theories. Those additional triggers are called semantic triggers.

They correspond to the following constructs.

Syntax

<semantic_trigger>    ::= <in_interval_trigger> | <maps_to_trigger>
(* [COMMENT/TODO: seems to always be paired with 'interval triggers'/filters *)
<in_interval_trigger> ::= <id> 'in' <square_bracket> <bound> ',' <bound> <square_bracket>
(* [COMMENT/TODO: probably there to shorten axioms] *)
<maps_to_trigger>     ::= <alias_id> '|->' <expr>

[TODO: complete this explanation]