SMT (Satisfiability Modulo Theories)

SMT solving infrastructure with Z3 integration and theory solvers.

Overview

Lotus provides SMT solving capabilities for constraint checking, invariant synthesis, symbolic execution, and formula simplification.

Location: lib/Solvers/SMT/

Capabilities

  • Direct Z3 integration as the primary SMT backend.

  • Theory support for bit-vectors, integer and real arithmetic, arrays, and uninterpreted functions.

  • Solver abstraction layer (LIBSMT — SMT Solver Abstraction Layer) providing backend-agnostic formula construction.

  • Specialized formula abstraction, normalization, and simplification modules.

Typical Use Cases

  • Verification condition checking and safety property validation.

  • Solving constrained Horn clauses (CHCs) in verification pipelines.

  • Path feasibility checking in symbolic execution.

  • Symbolic abstraction of bit-vector constraints.

Basic Usage (C++)

Analyses in Lotus typically interact with SMT solvers either via direct Z3:

#include <z3++.h>

z3::context ctx;
z3::solver solver(ctx);

z3::expr x = ctx.bv_const("x", 32);
z3::expr y = ctx.bv_const("y", 32);
solver.add(x + y == ctx.bv_val(10, 32));

if (solver.check() == z3::sat) {
  z3::model model = solver.get_model();
  // ...
}

or via the solver-agnostic abstraction layer LIBSMT — SMT Solver Abstraction Layer:

#include "Solvers/SMT/LIBSMT/SMTFactory.h"
#include "Solvers/SMT/LIBSMT/SMTSolver.h"

SMTFactory factory;
SMTSolver solver = factory.createSMTSolver();

SMTExpr x    = factory.createBitVecConst("x", 32);
SMTExpr zero = factory.createBitVecVal(0, 32);

solver.add(x > zero);
auto result = solver.check();   // SMTSolver::SMTRT_Sat, ...

Submodules

The lib/Solvers/SMT/ directory contains several specialized libraries:

See Also