LIBSMT — SMT Solver Abstraction Layer

A unified abstraction layer over multiple SMT solver backends.

Headers: include/Solvers/SMT/LIBSMT/

Implementation: lib/Solvers/SMT/LIBSMT/

Build target: CanarySMT

Overview

LIBSMT provides a solver-agnostic interface for SMT (Satisfiability Modulo Theories) solving. It abstracts over solver-specific details (Z3, etc.) so that Lotus analyses can issue SMT queries without depending on any single solver backend.

Components

SMTSolver

Abstract base class defining the solver interface:

push() / pop() — Assertion stack management.
assertExpr(SMTExpr) — Add a formula to the solver context.
check() — Check satisfiability of the current context.
getModel() — Retrieve a satisfying model.
reset() — Clear all assertions.

SMTExpr and SMTObject

Expression tree representation used to build formulas:

SMTExpr — Typed expression with a solver-specific handle.
SMTObject — Base class for all SMT entities (sorts, functions, variables).

SMTFactory

Factory for creating SMT sorts, variables, and expressions:

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

auto &factory = SMTFactory::instance();
auto intSort  = factory.getSort("Int");
auto x        = factory.makeVariable(intSort, "x");
auto y        = factory.makeVariable(intSort, "y");
auto expr     = factory.makeEQ(x, y);

Z3Expr and Z3Plus

Z3-specific expression handling and extended operations (quantifier support, optimisation queries, model parsing).

CNF and SATSolver

CNF formula representation and SAT solver interface for boolean-level reasoning:

CNF — Conjunctive normal form representation.
SATSolver — SAT solver wrapper (useful for eager bit-blasting).

SMTModel

Represents a satisfying assignment from a solver query, providing value lookup by variable name.

SMTConfigure

Configuration and option management for solver backends.

Usage

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

auto &factory = SMTFactory::instance();
auto solver   = factory.createSolver();

auto intSort = factory.getSort("Int");
auto x       = factory.makeVariable(intSort, "x");
auto gt      = factory.makeGT(x, factory.makeIntVal(0));

solver->assertExpr(gt);
auto result = solver->check();

if (result == SmtResult::Sat) {
  auto model = solver->getModel();
  auto val   = model->getValue(x);
  // ...
}