Index of types


A
abstract [Sum]
answer [Sig]
atom [Enumsolver_types]
atom [Solver_types]

C
clause [Enumsolver_types]
clause [Solver_types]
color [Util]
combinator [Smt.Formula]
The type of operators
comparator [Smt.Formula]
The type of comparators:
const [Types]
constant: it can be an integer, a real or a constant name

D
dnf [Ast]
Disjunctive normal form: each element of the list is a disjunct

E
elem [Heap.S]
elt [Use.ST]
elt [Use]
elt [Literal.S]
error [Smt]
error [Typing]
exp [Explanation]

G
glob_update [Ast]

H
hash_consed [Hashcons]

I
ident [Enumsolver_types]
input [Sig]
inst_trans [Forward]
the type of instantiated transitions

K
key [Hashcons.S_consed]
kind [Ast]
the kind of nodes

L
literal [Sig]
loc [Util]
Location in file

N
name_kind [Symbols]
node_cube [Ast]
the type of nodes, i.e.

O
op_comp [Types]
comparison operators for litterals
operator [Symbols]
operator [Smt.Term]
The type of operators

P
possible_result [Forward]
premise [Enumsolver_types]
premise [Solver_types]

R
r [Sig.C]
r [Sig.X]
r [Sig.COMBINATOR]
r [Polynome.S]
r [Sig.RELATION]
r [Sig.THEORY]
Type of representants of terms of the theory
r [Polynome.T]
reason [Enumsolver_types]
reason [Solver_types]
result [Sig]
result [Bwd]

S
sort [Types]
sort of single symbol
state [Enumsolver.Make]
state [Solver.Make]
state [Smt.Solver]
The type of the internal state of the solver (see Smt.Solver.save_state and Smt.Solver.restore_state).
subst [Variable]
the type of variable substitutions
swts [Ast]
The type of case switches case | c1 : t1 | c2 : t2 | _ : tn
system [Ast]
type of untyped transition systems constructed by parsing

T
t [Use.Make]
t [Use.ST]
t [Use.S]
t [Use.T]
t [Uf.S]
t [Ty]
t [Term]
t [Symbols]
t [Smt.Formula]
The type of ground formulas
t [Smt.Term]
The type of terms
t [Smt.Symbol]
The type of function symbols
t [Smt.Type]
The type of types in Alt-Ergo light
t [Sig.C]
t [Literal.OrderedType]
t [Literal.S]
t [Intervals]
t [Explanation]
t [Cc.S]
t [Sig.RELATION]
t [Sig.THEORY]
Type of terms of the theory
t [Polynome.T]
t [Bitv]
t [Vec]
t [Iheap]
t [Hstring]
The type of Hash-consed string
t [Heap.OrderType]
t [Heap.S]
t [Hashcons.HashedType_consed]
t [Hashcons.HashedType]
t [Hashcons.S]
t [Variable]
the type of variables
t [Types.ArrayAtom]
values of this type should be constructed with the invariant that the array must be sorted at all times
t [Types.Atom]
the type of atoms
t [Types.Term]
t [Node]
the type of nodes constructed during the search
t [Cubetrie]
Trie, mapping sets of atoms (i.e.
t [Cube]
the type of cubes, i.e.
t [Bwd.PriorityNodeQueue]
t_system [Ast]
type of typed transition systems
term [Types]
the type of terms
th [Sig.COMBINATOR]
trace [Options]
trace [Ast]
type of error traces, also the type of history of nodes
trace_step [Ast]
type of elementary steps of error traces
transition [Ast]
type of parameterized transitions with function
transition_func [Ast]
functionnal form, computed during typing phase
transition_info [Ast]
type of parameterized transitions
type_constructors [Ast]
Type and constructors declaration: ("t", ["A";"B"]) represents the declaration of type t with two constructors A and B.

U
update [Ast]
conditionnal updates with cases, ex.

V
var [Enumsolver_types]
var [Solver_types]
view [Term]
view [Literal]
viz_prog [Options]