Kind 2 Developer's Documentation
Developers' Documentation
Overall system architecture.
Configuration
Communication and Logging
LogEvent
Analysis and Strategies
Terms
Transition System Construction
Verification Engines
k-induction
IC3
Invariant Generators
Implication Graph-based Invariant Generation
C2I (machine-learning based invariant generation)
Interpreter
Input Modules
Lustre
Source files live in the subdirectory lustre
Dependency graph of modules 
LustreLexerLustreParserLustreAstLustreIdentLustreIndexLustreExprLustreNodeLustreContextLustreContractLustreDeclarationsLustreSimplifyLustreSlicingLustreTransSysLustreInputLustrePath
Native
Source files live in subdirectory nativeInput
SMT Solver Interface
Source files live in subdirectory SMTSolver
SMTLIB Interface
CVC4DriverGenericSMTLIBDriverMathSAT5DriverZ3Driver
Yices Interface
Lustre to Rust
Test generation
TestgenDFTestgenIOTestgenModesTestgenSolverTestgenStrategiesTestgenTreeTestgenLib
Utilities
LibResDebugDecimalHashconsHStringHStringSExprKind2ConfigMessagingNumeralPrettySExprBaseSExprLexerStatTermLibTrieVersionUnroller
Howto
Documentation
Edit this file doc/doc_into.txt and add the module to one section above in, then add it to kind2.odocl.
Add a new subdirectory
To add a new subdirectory feature edit the _tags file to include the line
<feature>: includeIndexes
indexlist