Solvers

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

The available backends include BDD (CUDD), SMT (Z3-based), weighted pushdown systems (WPDS), string constraint solving (Stingx), fixed-point equation solving (FPsolve), and experimental solver tooling (SLOT, STAUB, SymAbs, SMTSampler).

• 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
• Stingx — String Constraint Solver
  • Overview
  • Directory Structure
  • Build and Run
• E-Graph Quantifier Simplification (EGraphsSimp)
  • Overview
  • Key Components
  • Main Functions
  • Algorithms
  • Use Cases
  • Related Components
• FPsolve — Fixed-Point Equation Solver
  • Overview
  • Semiring Domains
  • Directory Structure
  • Build and Run

Third-Party Libraries

Additional vendored libraries in third-party/ that are not currently integrated:

• MDE (third-party/mde/) — Multilevel Deduplication Engine for caching set operations in dataflow analyses. Currently not compiled or linked (commented out in third-party/CMakeLists.txt).