Solvers

This section documents the solver frameworks, constraint solving backends, and SMT-based model checking components used throughout Lotus.

• CUDD (Binary Decision Diagrams)
  • Overview
  • Typical Use Cases
  • Basic Usage (C++)
  • Features
  • Integration Notes
• SMT (Satisfiability Modulo Theories)
  • Overview
  • Typical Use Cases
  • Basic Usage (C++)
  • Features
  • SymAbs: SMT Formula Abstraction Library
  • Integration Notes
• WPDS (Weighted Pushdown Systems)
  • Overview
  • Typical Use Cases
  • Basic Usage (C++)
  • Features
  • Integration Notes
• SMT Samplers
  • Overview
  • Samplers
  • QuickSampler Usage
  • IntervalSampler Usage
  • RegionSampler Usage
  • C++ API Usage
  • Related Work
  • See Also
• SMT Formula Abstraction (SymAbs)
  • Overview
  • Key Differences
  • Why Linear Integer Approximation?
  • Abstract Domains
  • Key Algorithms
  • C++ API Usage
  • When to Use SymAbs
  • Related Components
• SMT-LIB to LLVM Translation (SLOT)
  • Overview
  • Purpose
  • Key Components
  • Supported SMT-LIB Constructs
  • Example
  • Related Components
• SMT Theory Arbitrage (STAUB)
  • Overview
  • Key Concept
  • Components
  • Usage Example
  • Workflow
  • Related Work
  • See Also
• E-Graph Quantifier Simplification (EGraphsSimp)
  • Overview
  • Key Components
  • Main Functions
  • Algorithms
  • Use Cases
  • Related Components