Index of modules


A
A [Strategy]
Abbrev [Term]
Actlit
Creates a fresh actlit as a bool UF constant.
Analysis
Interface between strategy and low-level 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 / k-induction 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 k-induction
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 equivalence-only 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
Property-directed 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 model-checker.
Kind2Config
Kind2Flow
Runs the analyses produced by the strategy module.

L
Lib
General-purpose 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 S-expressions 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 higher-order 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
Low-level 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 post-analysis 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
S-Expressions
SExprLexer
Lexer: Lexer Specification for S-expressions
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
High-level 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