Builtin types
AltErgo’s native language includes the following builtin types. Creation and manipulation of values having those types are covered in builtin operators.
Boolean types
bool
, the preferred type to represent propositional variables. Boolean constants aretrue
andfalse
.prop
, an historical type still supported in AltErgo 2.3.0.
The historical separation comes from AltErgo origins in the Coq ecosystem: in Coq,prop
is much richer thanbool
.
In AltErgo 2.3.0,prop
andbool
have been merged in order to simplify interactions with the SMTLIB standard.
More information on thebool
/prop
conflict can be found in this section.
Numeric types
int
for (arbitrary large) integers.real
for reals. This type actually represents the smallest extension of the rationals which is algebraically closed and closed by exponentiation. Rationals with arbitrary precision are used under the hood.
Unit type
unit
is AltErgo native language’s unit type.
Bitvectors
bitv
are fixedsize binary words of arbitrary length.
There exists a bitvector type bitv[n]
for each nonzero positive integer n
. For example, bitv[8]
is a bitvector of length 8
.
Type variables
AltErgo’s native language’s type system supports prenex polymorphism. This allows efficient reasoning about generic data structure.
Type variables can be created implicitly, and are implicitly universally quantified in all formulas. Any formula which requires a type can accept a type variable.
Type variable may be used to parametrize datatypes, as we will see when we will create new types, or in the following example of farray
.
Type variables are indicated by an apostrophe '
. For example, 'a
is a type variable.
Polymorphic functional arrays
AltErgo’s native language includes functional polymorphic arrays, represented by the farray
type, and has a builtin theory to reason about them.
The farray
is parametrized by two types: the type of their indexes (default is int
) and the type of their values (no default).
Array can be accessed using any index of valid type.
Functional polymorphic arrays are persistent structures: they may be updated, but only for the scope of an expression.
Builtin operators
Logical operators
Operation 
Notation 
Type(s) 

Negation 


Conjonction 


Disjonction 


Implication 


Equivalence 


Exclusive or 


For all those operators, bool
and prop
are fully interchangeable.
The bool
/prop
conflict
Prior to AltErgo 2.3.0, AltErgo’s native language handled differently boolean variables bool
and propositional variables prop
.
The two keywords still exist in AltErgo 2.3.0, but those two types have been made fully compatible: any function or operator taking a bool
or a prop
as an argument accepts both.
The historical separation comes from AltErgo origins in the Coq ecosystem: in Coq, prop
is much richer than bool
.
In AltErgo 2.3.0, prop
and bool
have been merged in order to simplify interactions with the SMTLIB standard.
Note that bool
can be used in more syntactic constructs than prop
.
prop
cannot be the input or output type of a interpreted function (function
keyword), whereasbool
can.prop
cannot be used in the declaration of new types (type
keyword), whereasbool
can.prop
cannot be used as the value of a type variable, whereasbool
can.prop
cannot be the input of an uninterpreted function (logic
keyword), whereasbool
can. In all other cases, it is advised the useprop
rather thanbool
, because it is better handled internally by AltErgo. However, usingbool
would be correct.prop
andbool
can be the output type of an uninterpreted function (logic
keyword).prop
andbool
can be the type of an uninterpreted variable (logic
keyword). Note that apredicate
hasprop
output type.
Examples
(* Correct example *)
logic A,B,C: prop
axiom a1: A > B
axiom a2: B > C
goal g: (B>A) and (C>B) > (A <> C)
(* Equivalent example using bool *)
logic A,B,C: bool
axiom a1: A > B
axiom a2: B > C
goal g: (B>A) and (C>B) > (A <> C)
Numeric operators
Operation 
Notation 
Type(s) 

Unary negative 


Addition 


Subtraction 


Multiplication 


Division 


Remainder 


Exponentiation ( 


Exponentiation ( 


Comparisons
Operation 
Notation 
Type(s) 
Notes 

Equality 



Inequality 


Syntactic sugar for 
All distinct 


Can be used on any number of operands. 
Strictly less than 



Lesser than or equal to 



Strictly greater than 



Greater than or equal to 


Note that binary comparisons operators can be chained: if op1
, op2
, … are binary comparisons operators, than x0 op1 x1 op2 x2 ...
has the same semantic as (x0 op1 x1) and (x1 op2 x2) and ...
.
One use of this is the creation of intervals, as in the following example.
(* Linear arithmetic over integers *)
goal g:
forall x,y,z,t:int.
0 <= y + z <= 1 >
x + t + y + z = 1 >
y + z <> 0 >
x + t = 0
Additional numeric primitives
AltErgo provides builtin primitives for mixed integers and real problems, along with some limited reasoning support, typically restricted to constants. These primitives are only available in the native input format.
Conversion between integers and reals
logic real_of_int : int > real
real_of_int
converts an integer into its representation as a real number.
Note: real_of_int
is also available in the smtlib2 format as the to_real
function from the Reals_Ints
theory.
logic int_floor : real > int
logic int_ceil : real > int
logic real_is_int : real > bool
int_floor
and int_ceil
implement the usual floor
and ceil
functions.
They compute the greatest integer less than a real and the least integer
greater than a real, respectively.
real_is_int
is true for reals that are exact integers, and false otherwise.
Note: int_floor
and real_is_int
are also available in the smtlib2 format
as the to_int
and is_int
functions from the Reals_Ints
theory
respectively.
Square root
logic sqrt_real : real > real
The sqrt_real
function denotes the square root of a real number.
Internal primitives
AltErgo also implements additional primitives that are tuned for specific internal use cases. They are only listed here for completeness and adventurous users, but their use should be avoided. Support for these primitives may be removed without notice in future versions of AltErgo.
In particular, the abs_real
, abs_int
, max_real
, max_int
and min_int
functions were introduced prior to if .. then .. else ..
statements in
AltErgo. They are preserved due to being used internally for floatingpoint
reasoning, but should not be used outside of the solver. Prefer defining these
functions using if .. then .. else ..
instead.
logic abs_real : real > real
logic abs_int : int > int
logic max_real : real, real > real
logic max_int : int, int > int
logic min_int : int, int > int
logic sqrt_real_default : real > real
logic sqrt_real_excess : real > real
logic integer_log2 : real > int
Bitvectors
Remember that bitvectors are fixedsize binary words: vectors of 0
and 1
.
There exists a bitvector type bitv[n]
for each fixed nonzero positive integer n
. For example, bitv[8]
is a bitvector.
Note that bitvectors are indexed from right to left.
Operation 
Notation 
Type 

Explicit declaration 
`[ 

Concatenation 

bitv[n], bitv[m] > bitv[n+m] 
Extraction of contiguous bits 


Examples
(** Usage of bitv types *)
logic register: bitv[8]
(** Explicit declaration *)
axiom a: register = [00101010]
(** Concatenation
Both goals are valid *)
goal g1:
forall x,y:bitv[16]. x@y=y@x > x = y
goal g2:
forall x,y:bitv[3]. x@[101] = [000101] > x=[000]
(** Extraction of contiguous bits *
All goals are valid)
goal g3:
[010]^{0,1}=[1100]^{1,2}
goal g4:
forall x:bitv[4]. forall y:bitv[2].
x=y@[10] >
x^{2,3}=[11] >
x=[1110]
goal g5 :
forall x:bitv[32]. forall y:bitv[32]. forall s:bitv[32].
s = y^{0,15} @ x^{16,31} >
(s^{16,31} = y^{0,15} and s^{0,15} = x^{16,31})
Type variables
As type variables and polymorphism have already been described, let’s just look at the following example.
logic f: 'a>'b
logic g: 'b>'b
axiom a1: forall x:'a. g(f(x))=f(x)
axiom a2: forall x:int. f(x)=0
goal g1:
(* Valid *)
g(f(0.01)) = f(0.01)
goal g2:
(* Valid *)
g(f(1)) = g(0)
goal g3:
(* I don't know *)
g(f(0.01)) = g(0)
Polymorphic functional arrays
[TODO: add table?]
Remember that farray
are parametrized by two types: the type of their indexes (default is int
) and the type of their values (no default).
Syntax
(* Instantiation of a farray type *)
<farray_type> ::= <value_type> 'farray'
 '(' <index_type> ',' <value_type> ')' 'farray'
(* Access  this expression is of type (value_type) *)
<farray_access_expr> ::= <array_id> '[' <index> ']'
(* Update  this expression is of type ((index_type) (value_type) farray) *)
<farray_update_expr> ::= <array_id> '[' <index> '<' <new_value> ( ',' <index> '<' <new_value> )* ']'
Examples
(* arr1 is a general polymorphic farray *)
logic arr1: ('a, 'b) farray
(* arr2 is a polymorphic farray whose indexes are int *)
logic arr2: 'b farray
(* arr3 is a farray whose indexes are int and whose values are real *)
logic arr3: real farray
(* arr4 is a farray whose indexes are parametrized by 'a and whose values are real *)
logic arr4: ('a, real) farray
(* arr5 is a farray whose indexes and values are real *)
logic arr5: (real, real) farray
(* Accessing and updating farrays *)
goal g1:
forall i,j,k:int.
forall v,w:'a.
forall b:'a farray.
b = b[j<b[i],k<w] >
i = 1 > j = 2 > k = 1 >
b[i] = b[j]
(* Using farrays with custom types for indexes and values *)
type t = A  B  C  D
type t2 = E  F  G  H
goal g2:
forall a : (t,t2) farray.
a[B < E][A] <> E >
a[C < F][A] <> F >
a[D < G][A] <> G >
a[A] = H