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 |

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: |

U | |

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

V | |

var [Enumsolver_types] | |

var [Solver_types] | |

view [Term] | |

view [Literal] | |

viz_prog [Options] |