A  
abstr [Flags.IC3] 
Legal abstraction mechanisms for in IC3.

actlit [TestgenLib]  
actlit_type [Clause] 
Type of activation literal

any_input [Kind2]  
assumptions [Analysis] 
Type of scopewise assumptions.

atom [SExprBase.S] 
Atom in an Sexpression

attr [Ltree.BaseTypes] 
Attribute

attr [Ltree.S] 
Attribute

auto_returns [LustreAst]  
automaton_transition [LustreAst]  
B  
base [LockStepDriver] 
The base checker is used to check whether some candidate invariants hold
k steps away from the initial state.

bound_or_fixed [LustreExpr] 
Type of index in an equation for an array

C  
call_cond [LustreNode] 
Call condition: activate or restart

cformula [Poly] 
cformula is a list of Presburger Atom conjuncted together

check_sat_response [SolverResponse] 
Type of reponses for checksat commands

clock_expr [LustreAst] 
A clock expression

clocked_typed_decl [LustreAst] 
An identifier with a type and a clock as used for the type of variables

const_clocked_typed_decl [LustreAst] 
An identifier, possibly flagged as constant, with a type and a
clock as used for the type of variables

const_decl [LustreAst] 
A constant declaration

context [TestgenLib] 
Gathers the contracts, the actions a strategy can perform on the
underlying smt solver used for test generation, and some data a
strategy generates tests from.

context [TestgenStrategies] 
Gathers the contracts, the actions a strategy can perform on the
underlying smt solver used for test generation, and some data a
strategy generates tests from.

contract [LustreNode] 
A contract.

contract [LustreAst]  
contract_assume [LustreAst]  
contract_call [LustreAst]  
contract_ensure [LustreAst]  
contract_ghost_const [LustreAst]  
contract_ghost_var [LustreAst]  
contract_guarantee [LustreAst]  
contract_mode [LustreAst]  
contract_node_decl [LustreAst] 
A contract node declaration as a tuple of

contract_node_equation [LustreAst]  
contract_require [LustreAst]  
contract_testcase [TestgenLib] 
A contract test case is a list of numeral / term pairs such that the list is sorted by descending numerals,, two succeeding pairs (k2, contracts2) and (k1, contracts1) represent
the fact that contracts1 hold from k1 to k2 (exclusive), at which point
contracts2 hold.

contract_testcases [TestgenLib] 
A map from actlits to contract test cases.

control_message [Messaging.S] 
A message internal to the messaging system

ctx [Messaging.S] 
Messaging context

custom_arg [SMTExpr] 
Arguments to a custom command

custom_response [SolverResponse] 
Type of reponses for custom commands

D  
data [TestgenStrategies.Sig] 
Type for the data of the strategy.

decl_response [SolverResponse] 
Type of reponses for declaration and definition commands

declaration [LustreAst] 
A declaration of a type, a constant, a node, a function or an
instance of a parametric node

depth [TestgenTree] 
A depth is just a numeral.

E  
enable [Flags] 
The Kind modules enabled is a list of
kind_module s.

eq_lhs [LustreAst] 
The lefthand side of an equation

equation [LustreNode] 
An equation is a tuple
(eqlhs, expr) that defines a possibly indexed
state variable as an expression.

equation_lhs [LustreNode] 
Type of left hand side of equations.

error_response [SolverResponse] 
Type of reponses for errors

event [Event]  
expr [LustreExpr] 
A
Term.t representing a Lustre expression, state variable
offsets refer to the current and the previous instant.

expr [LustreAst] 
A Lustre expression

expr_of_string_sexpr_conv [GenericSMTLIBDriver]  
extract [Flags.IC3] 
Legal heuristics for extraction of implicants in IC3.

F  
feature [TermLib] 
A feature of a logic fragment for terms

features [TermLib] 
Logic fragments for terms

flat [Ltree.S] 
Term over symbols, variables and sort of the types given where
the topmost symbol is not a binding

float_item [Stat] 
A float statistics item

G  
get_model_response [SolverResponse] 
Type of reponses for getmodel commands.

get_unsat_core_response [SolverResponse] 
Type of reponses for getunsatcore commands.

get_value_response [SolverResponse] 
Type of reponses for getvalue commands.

graph [InvGenGraph.Graph] 
A graph.

H  
hash_consed [Hashcons]  
I  
ident [LustreAst] 
An identifier

index [LustreIndex] 
A sequence of indexes

index [LustreAst] 
A single index

info [Analysis] 
Information for the creation of a transition system

info [Strategy] 
Information used by the strategy module.

input_format [Flags] 
Format of input file

instance [TransSys] 
Instance of a subsystem

int_item [Stat] 
An integer statistics item

int_list_item [Stat] 
An integer statistics list

interpreted_symbol [Symbol] 
The interpreted symbols

invariant [Certificate]  
K  
k [TestgenLib]  
key [Hashcons.S]  
key [Trie.S] 
Type of keys in the trie

kind_module [Lib] 
Kind modules

kindtype [Type] 
Type of an expression

L  
label_or_index [LustreAst] 
A record field or an array or tuple index

lambda [Term] 
Terms are hashconsed abstract syntax trees

lambda [Ltree.S] 
Hashconsed lambda abstraction

lambda_node [Ltree.S] 
Lambda abstraction over symbols, variables and sort of the types
given.

log_format [Log.Sig] 
Format of log messages

log_level [Lib] 
Levels of log messages

log_printer [Log.Sig]  
logic [TermLib] 
Logic fragments for terms

logic [Flags.Smt] 
Logic sendable to the SMT solver.

lustre_type [LustreAst] 
A Lustre type

M  
m_log_printer [Log.Sig]  
map [InvGenGraph] 
Set of terms.

message [Messaging.S] 
A message

messaging_setup [Event] 
Setup of the messaging system

mininvs [Flags.Certif] 
Minimization stragegy for invariants

mink [Flags.Certif] 
Minimization stragegy for k

mode [TestgenTree] 
A
mode is just its name.

mode [TestgenModes]  
mode [LustreContract] 
Type of modes.

mode_conj [TestgenTree] 
A conjunction of modes.

mode_path [TestgenTree] 
A
mode_path stores the modes activated by the path in reverse order.

mode_tree [LustreContract.ModeTrace] 
A mode tree: hierarchical organization of modes.

model [TestgenLib]  
model [TestgenTree]  
modes [TestgenModes]  
mthread [Event] 
Background thread of the messaging system

N  
no_response [SolverResponse]  
node_call [LustreNode] 
A call to a node

node_decl [LustreAst] 
Declaration of a node or function as a tuple of

node_equation [LustreAst] 
An equation or assertion in the node body

node_item [LustreAst] 
An item in a node declaration

node_local_decl [LustreAst] 
A local constant or variable declaration of a node

node_param [LustreAst] 
A type parameter of a node

node_param_inst [LustreAst] 
An instance of a parametric node as a tuple of the identifier for
the instance, the identifier of the parametric node and the list of
type parameters

num [TestgenTree]  
O  
one_index [LustreIndex] 
An index element

out [Certificate] 
The type of certificates outputs, these are file names for the intermediate
SMTLIB 2 certificates

output_message [Messaging.S] 
A message to be output to the user

P  
param [Analysis] 
Parameter of an analysis.

path [Model] 
A path is a map of state variables to assignments

poly [Poly] 
poly is a list of psummands

position [Lib] 
A position in the input

preAtom [Poly] 
For a polynomial p and integer i, a Presburger Atom could be p > 0, p = 0, p != 0, i  p, i ! p

pred_def [TransSys] 
Predicate definition

prop [Hashcons.HashedType]  
prop [Hashcons.S]  
prop_set [Clause] 
Set of properties

prop_source [Property] 
Source of a property

prop_status [Property]  
pruning [LockStepDriver] 
Used to check whether some invariants are implied by the transition
relation alone.

psummand [Poly] 
psummand is a constant or a variable with coefficient

Q  
qe [Flags.IC3] 
Algorithm usable for quantifier elimination in IC3.

R  
rangekind [Type] 
Tells if the range actually encodes an enumerated datatype

relay_message [Messaging.S]  
res [Res]  
response [SolverResponse] 
Type of all possible responses of a solver

result [Analysis] 
Result of analysing a transistion system

results [Analysis] 
Map from
Scope.t to result storing the results found this far.

S  
sat_or_unsat [SMTSolver] 
Alternative between type 'a and 'b

set [InvGenGraph]  
socket [Messaging.S] 
Socket

solver [Flags.Smt] 
Legal SMT solvers.

sort [SMTExpr] 
An SMT sort is of type
Type.t

sort [Ltree.BaseTypes] 
Sort

sort [Ltree.S] 
Sort

source [Clause] 
Origin of clause

stat_item [Stat] 
An generic statistics item

state [LustreAst]  
state_var [StateVar] 
State variable

state_var_instance [LustreNode] 
Instance of state vars as streams with their position

state_var_source [LustreNode] 
Source of a state variable

step [LockStepDriver] 
The step checker is used to check whether some candidate invariants hold in
the
k inductive step instance.

struct_item [LustreAst] 
Structural assignment on the lefthand side of an equation

svar [TestgenLib]  
svar [LustreContract]  
symbol [Symbol] 
Adding uninterpreted function symbols separately for conversions
from expressions in the SMT solver interface

symbol [Ltree.BaseTypes] 
Symbol

symbol [Ltree.S] 
Symbol

symbols [Certificate]  
sys [TestgenLib]  
sys [TestgenModes]  
sys_modes [TestgenModes]  
system [Certificate]  
T  
t [Certificate] 
The type of certificates

t [TestgenTree] 
Stores the witnesses and the reversed tree.

t [TestgenSolver]  
t [TestgenModes]  
t [TestgenIO] 
Stores IO things to log testcases to xml.

t [SExprBase.SExprAtom]  
t [Numeral] 
Type of arbitrary precision numerals

t [Messaging.RelayMessage] 
Message

t [SExprBase.S] 
Sexpression is either an atom or a list of Sexpressions

t [HStringSExpr.HStringAtom]  
t [HString] 
Hashconsed string

t [Hashcons.HashedType]  
t [Hashcons.S]  
t [Hashcons]  
t [Decimal] 
Type of arbitrary precision rational numbers

t [Debug] 
Types of debug functions

t [SMTSolver] 
Type of a solver instance

t [SMTExpr] 
An SMT expression is of type
Term.t

t [LustreContract] 
Type of contracts.

t [LustreContext] 
Context

t [LustreNode] 
A Lustre node

t [LustreExpr] 
A Lustre expression

t [LustreIdent] 
An identifier is a string with integer indexes

t [LustreAst] 
A Lustre program as a list of declarations

t [InvGenDomain.Domain] 
Value formatter.

t [Trie.S] 
Type of the trie

t [Clause] 
Clause

t [TransSys] 
The transition system

t [SubSystem] 
A system parameterized by its actual source

t [Property] 
A property of a transition system

t [Var] 
Hashconsed variable

t [UfSymbol] 
Hashconsed uninterpreted symbol

t [Type] 
Hashconsed type

t [Term] 
Terms are hashconsed abstract syntax trees

t [TermAttr] 
Hashconsed attribute

t [Symbol] 
Hashconsed symbol

t [StateVar] 
Hashconsed state variable

t [Scope] 
Scope as a sequence of identifiers

t [Model] 
A model is a list of variables and assignemnts

t [Ltree.S] 
Hashconsed abstract syntax term

t [Ident] 
Identifier

t [InputSystem]  
t_node [Ltree.S] 
Abstract syntax term over symbols, variables and sort of the
types given.

t_prop [Ltree.S] 
Properties of a term

term [TestgenLib]  
term [TestgenTree]  
term [InvGenGraph] 
Term.

thread [Messaging.S] 
Thread

token [LustreParser]  
transition_branch [LustreAst]  
transition_to [LustreAst]  
tree [TestgenLib] 
Tree structure to display the tree of activable modes.

type_decl [LustreAst] 
A declaration of an alias or free type

typed_ident [LustreAst] 
An identifier with a type

U  
uf_symbol [UfSymbol] 
Uninterpreted symbol are just strings of their name

V  
value [Model] 
Term or lambda expression

value [Eval] 
Type of value of a term

values [TestgenLib]  
var [SMTExpr] 
An SMT variable is of type
Var.t

var [Ltree.BaseTypes] 
Variable

var [Ltree.S] 
Variable

Y  
yices_id [YicesResponse]  
yices_resp_p [YicesResponse] 