Index of types

A
abstract [Sum]
answer [Sig]
atom [Enumsolver_types]
atom [Solver_types]
atom [Ptree]
C
cformula [Ptree]
check_strategy [Smt_sig.S]	Check sat strategy
clause [Enumsolver_types]
clause [Solver_types]
color [Util]
combinator [Smt_sig.S.Formula]	The type of operators
comparator [Smt_sig.S.Formula]	The type of comparators:
const [Types]	constant: it can be an integer, a real or a constant name
cst [Types]
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]
env [Enumerative]	The type of environments for enumerative explorations
error [Smt_sig.S]
error [Typing]
exp [Explanation]
F
formula [Ptree]
G
glob_update [Ast]
H
hash_consed [Hashcons]
I
ident [Enumsolver_types]
init_instance [Ast]	Type of instantiated initial formulas
input [Sig]
inst_trans [Forward]	the type of instantiated transitions
K
key [Hashcons.S_consed]
kind [Ast]	the kind of nodes
L
literal [Smt_sig.S.Formula]	The type of literals
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_sig.S.Term]	The type of operators
P
pdecl [Ptree]
pglob_update [Ptree]
poly [Types]
possible_result [Forward]
premise [Enumsolver_types]
premise [Solver_types]
pswts [Ptree]
psystem [Ptree]
ptransition [Ptree]
pupdate [Ptree]
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]
reset_memo [Pre]	Pre-image computation
result [Sig]
result [Bwd]
S
solver [Options]
sort [Types]	sort of single symbol
state [Enumsolver.Make]
state [Solver.Make]
state [Enumerative]	The type of states, we allow states to be constructed from the outside by calling the function `new_undef_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 [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 [Use.Make]
t [Use.ST]
t [Use.S]
t [Use.T]
t [Uf.S]
t [Ty]
t [Term]
t [Symbols]
t [Smt_sig.S.Formula]	The type of ground formulas
t [Smt_sig.S.Term]	The type of terms
t [Smt_sig.S.Symbol]	The type of function symbols
t [Smt_sig.S.Type]	The type of types in the solver
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 [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 [Types.Var]
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
term [Ptree]
term_or_formula [Ptree]
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]