Index of types


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 scope-wise assumptions.
atom [SExprBase.S]
Atom in an S-expression
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 check-sat 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_modules.
eq_lhs [LustreAst]
The left-hand 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 get-model commands.
get_unsat_core_response [SolverResponse]
Type of reponses for get-unsat-core commands.
get_value_response [SolverResponse]
Type of reponses for get-value 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 SMT-LIB 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 left-hand 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]
S-expression is either an atom or a list of S-expressions
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]