A  
A [Strategy]  
Abbrev [Term]  
Actlit 
Creates a fresh actlit as a bool UF constant.

Analysis 
Interface between strategy and lowlevel analysis

Arrays [Flags] 
Arrays flags

AttrHashtbl [TermAttr] 
Hash table over attributes

AttrMap [TermAttr] 
Map over attributes

AttrSet [TermAttr] 
Set over attributes

B  
Base 
Clean up before exit

BmcKind [Flags] 
BMC / kinduction flags

Bool [InvGenGraph.EqOnly] 
Graph of booleans.

Bool [InvGenGraph] 
Graph of booleans with implication.

Bool [InvGenDomain] 
Boolean domain with implication.

Bool [InvGenMiner] 
Bool candidate term miner.

BoolInvGen [InvGen.EqOnly] 
Graph of booleans.

BoolInvGen [InvGen] 
Boolean invariant generation module.

C  
C2I [Flags] 
C2I flags

CVC4Driver  
Certif [Flags] 
Certificates and Proofs

Certificate 
Certificates for Kind 2.

Clause 
Clause, properties and activation literals for IC3

ClauseTrie [Clause] 
A trie of literals

Compress 
Path compression for kinduction

Contracts [Flags] 
Contracts flags

Conv [SolverSig.Inst]  
Converter [SMTExpr]  
CooperQE 
Cooper quantifier elimination

Create [SolverSig.S] 
The functor
Create creates a new instance of the SMT solver with
paramters passed as its arguments.

D  
Debug 
Debug ouput, controlled by
Flags .

Decimal 
Arbitrary precision real numbers

Domain [InvGenGraph.Graph] 
Domain with an order relation.

E  
EqOnly [InvGen] 
Graph modules for equivalenceonly invgen.

EqOnly [InvGenGraph] 
Graph modules for equivalence only.

Eval 
Term evaluator

Event 
Event logging and communication

ExitCodes [Lib] 
Exit codes.

Extract 
Extract an active path from a formula given a model

F  
FeatureSet [TermLib] 
Set of features

Flags 
Parsing of command line arguments

G  
GenericSMTLIBDriver  
H  
HString 
Perfect shared strings by hashconsing

HStringAtom [HStringSExpr]  
HStringHashtbl [HString] 
Hash table over hashconsed strings

HStringMap [HString] 
Map over hashconsed strings

HStringSExpr  
HStringSExpr  
HStringSet [HString] 
Set over hashconsed strings

Hashcons 
Hash tables for hash consing

Hashtbl [LustreIdent] 
Hash table over identifiers

Hashtbl [TransSys] 
Hash table over transition systems.

I  
IC3 
Propertydirected reachability (aka IC3)

IC3 [Flags] 
IC3 flags

Ident 
Managing of identifier to avoid clashes

IdentMap [Ident] 
Map of identifiers

IdentSet [Ident] 
Set of identifiers

InputParser 
Parser for a CSV input file

InputSystem 
Delegate to concrete functions for input formats.

Int [InvGenGraph.EqOnly] 
Graph of integers.

Int [InvGenGraph] 
Graph of integers with less than or equal.

Int [InvGenDomain] 
Integer domain with less than or equal to.

Int [InvGenMiner] 
Real candidate term miner.

IntInvGen [InvGen.EqOnly] 
Graph of integers.

IntInvGen [InvGen] 
Int invariant generation module.

IntegerHashtbl [Lib] 
Hashtable of integers

IntegerSet [Lib] 
Sets of integers

Interpreter 
Interpreter for Lustre programs

Interpreter [Flags] 
Interpreter flags

InvGen 
Generic invariant generation.

InvGenDomain 
Exception thrown when a domain is asked to build a trivial implication.

InvGenGraph 
Graph representing equivalence classes and ordering between some terms.

InvGenMiner 
Module generating candidate terms for invariant generation.

InvarManager 
Invariant manager

Invgen [Flags] 
Invgen flags

K  
Kind2 
Top level of the Kind 2 modelchecker.

Kind2Config  
Kind2Flow 
Runs the analyses produced by the strategy module.

L  
Lib 
Generalpurpose library functions

LockStepDriver 
Lock Step Driver (LSD).

Log 
Logging and messaging

Lsd [InvGenGraph] 
LSD module.

Ltree 
Abstract syntax trees with binders and quantifiers

LustreAst 
Minimally simplified Lustre abstract syntax tree

LustreContext 
Context information used in and obtained from parsing

LustreContract 
Wraps a state variable for use in a contract.

LustreDeclarations 
Convert a Lustre abstract syntax tree to an intermediate Lustre model

LustreExpr 
Internal reperesentation of a Lustre expression

LustreExprHashtbl [LustreExpr] 
Hash table over Lustre expressions

LustreIdent 
Lustre identifier

LustreIndex 
Indexes for lists, records, tuples and arrays in Lustre

LustreInput 
Parse Lustre input into the intermediate Lustre format

LustreLexer 
Lexer for Lustre input

LustreNode 
Internal representation of a Lustre node

LustreParser  
LustrePath 
Conversion of a counterexample to a Lustre model

LustreSimplify 
Simplify a Lustre AST to normalized Lustre nodes

LustreSlicing 
Cone of influence reduction and dependency ordering of equations

LustreToRust 
Compilation from
LustreNode.t to Rust.

LustreTransSys 
Convert a Lustre node to a transition system

M  
MIL [Model]  
Make [Trie] 
Trie over sequences of keys of map

Make [SExprBase] 
Functor to make Sexpressions of atoms of type
atom

Make [Messaging] 
Functor to instantiate the messaging system with a type of messages

Make [Hashcons]  
Make [SMTLIBSolver]  
Make [Ltree] 
Functor to create a higherorder abstract syntax tree module

Make [Log] 
Create a logging module parameterized by a relay function

Map [LustreIdent] 
Map of identifiers

Map [Scope] 
Map of scopes

Messaging 
Lowlevel handling of messages

ModeTrace [LustreContract] 
Mode traces as cex.

Model 
Term or lambda expression

N  
Names [Lib] 
File names.

NativeInput 
Parse a file in native input format into a transition system

Numeral 
Arbitrary precision integers

P  
Paths [Lib] 
Paths Kind 2 can write some files.

Poly 
Polynomials

PostAnalysis 
Signature of modules for postanalysis treatment.

Presburger 
Conversions from and to Presburger arithmetic formulas

Pretty 
Functions for pretty ascii output (colors, etc.)

Property 
Current status of a property

Q  
QE 
Quantifier elimination

QE [Flags] 
QE flags

R  
Real [InvGenGraph.EqOnly] 
Graph of reals.

Real [InvGenGraph] 
Graph of reals with less than or equal.

Real [InvGenDomain] 
Real domain with less than or equal to.

Real [InvGenMiner]  
RealInvGen [InvGen.EqOnly] 
Graph of reals.

RealInvGen [InvGen] 
Real invariant generation module.

Res 
A result for some type.

ReservedIds [Lib] 
Reserved identifiers.

RunCertif [PostAnalysis]  
RunContractGen [PostAnalysis]  
RunInvLog [PostAnalysis]  
RunRustGen [PostAnalysis]  
RunTestGen [PostAnalysis]  
S  
SExprBase 
SExpressions

SExprLexer 
Lexer: Lexer Specification for Sexpressions

SI [LustreAst]  
SMTExpr 
Datatypes and helper function for the SMT solver interface

SMTLIBSolver 
An interface to any SMT solver that accepts the SMTLIB2 command
language

SMTSolver 
Highlevel methods for an SMT solver

Scope 
Managing of scopes to avoid clashes

Set [LustreIdent] 
Set of identifiers

Set [Scope] 
Set of scopes

Signals [TermLib] 
Gathers signal related stuff.

Signals [Kind2]  
Simplify 
Term simplifier

Smt [Flags] 
SMT solver flags

SolverDriver 
Solver configuration options

SolverResponse 
Solver commands and responses

SolverSig 
Solver paramters

Stat 
Statistics

StateVar 
State variables

StateVarHashtbl [StateVar] 
Hash table over state variables

StateVarMap [StateVar] 
Map over state variables

StateVarSet [StateVar] 
Set over state variables

Step 
Clean up before exit

Strategy 
A strategy returns an
Analysis.param option which is None if done.

SubSystem 
Abstract system

Symbol 
Kind's symbols

SymbolHashtbl [Symbol] 
Hash table over symbols

SymbolMap [Symbol] 
Map over symbols

SymbolSet [Symbol] 
Set over symbols

Sys [TestgenModes]  
T  
T [Term]  
Term 
Term representation

TermAttr 
Attributes for annotated terms

TermHashtbl [Term] 
Hash table over terms

TermLib 
Utilty functions for transition systems

TermMap [Term] 
Map over terms

TermSet [Term] 
Set over terms

Testgen [Flags]  
TestgenDF 
Prefix for logging testgen related things.

TestgenIO 
Stores IO things to log testcases to xml.

TestgenLib 
Turns an actlit uf in a term.

TestgenModes  
TestgenSolver 
Wraps a solver and provides a convenient interface for test generation.

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.

TestgenTree 
A depth is just a numeral.

TransSys 
Representation of a transition system

Trie 
Trie over lists of values

Type 
Types of terms

TypeHashtbl [Type] 
Hash table over types

TypeMap [Type] 
Map over types

TypeSet [Type] 
Set over types

U  
UfSymbol 
Uninterpreted function symbols

UfSymbolHashtbl [UfSymbol] 
Hash table over uninterpreted function symbols

UfSymbolMap [UfSymbol] 
Map over uninterpreted function symbols

UfSymbolSet [UfSymbol] 
Set over uninterpreted function symbols

Unroller 
Very basic helper functions for unrolling.

V  
Var 
Variables in terms

VarHashtbl [Var] 
Hash table over variables

VarMap [Var] 
Map over variables

VarSet [Var] 
Set over variables

Version 
Static and autoconfigured defaults

Y  
Yices2SMT2Driver  
YicesDriver  
YicesLexer  
YicesNative 
An interface to the Yices SMT solver in native format.

YicesResponse  
Z  
Z3Driver 