SMT Samplers

This section documents the SMT sampling utilities in Lotus for extracting diverse satisfying assignments (models) from SMT formulas.

Overview

The SMTSampler library provides multiple algorithms for sampling from the solution space of SMT formulas. These samplers are useful for test case generation, solution space exploration, and analyzing formula sensitivity.

Location: lib/Solvers/SMT/SMTSampler/

Library: SMTSampler

Dependencies: - SymAbs (symbolic abstraction library) - Z3 SMT solver

Samplers

QuickSampler

A mutation-based approach for generating diverse models from CNF formulas.

Input: CNF in DIMACS format with optional c ind lines for independent variables

Output: <input>.samples - one line per sample in format <mutations>: <bitstring>

Algorithm: Uses genetic mutation operators to explore the solution space, stopping on time or sample limits.

Related Work: Based on ICSE 18 paper “Efficient Sampling of SAT Solutions for Testing”

IntervalSampler

Computes per-variable bounds using Z3’s optimize commands and samples uniformly within those bounds.

Input: SMT-LIB bit-vector formulas (single file or directory)

Output: res.log (append-only summary statistics)

Algorithm: 1. Use Z3 optimize to find variable bounds 2. Sample uniformly from computed intervals 3. Validate samples against original formula

RegionSampler (PolySampler)

Geometry-based sampling from convex polytopes defined by linear constraints. Uses the SymAbs library to build linear abstractions (Zone or Octagon domains).

Input: SMT-LIB bit-vector formulas

Output: <input>.abs.samples with first line as variable name header

Algorithm: 1. Build linear abstraction (Zone or Octagon) from formula 2. Use hit-and-run (or other) random walk to propose samples 3. Validate proposed samples against original formula

Available Walks: - HitAndRun - default, geometric random walk - BallWalk - ball-based random walk - DikinWalk - Dikin walk for log-concave distributions - CoordinateWalk - coordinate axis random walk - ConstraintWalk - constraint-based random walk

QuickSampler Usage

Command-line interface (if built as a tool):

quicksampler input.cnf -samples 100 -timeout 60

Output Format:

3: 1010110101
5: 0011101010
...

Each line: <number_of_mutations>: <bitstring>

IntervalSampler Usage

intervalsampler input.smt2 -samples 1000

RegionSampler Usage

regionsampler input.smt2 -domain zone -walk hitandrun -samples 500

Options: - -domain: zone or octagon - -walk: hitandrun, ballwalk, diknwalk, coordinate, constraint - -samples: Number of samples to generate

C++ API Usage

#include "Solvers/SMT/SMTSampler/SMTSampler.h"

using namespace z3;

context ctx;
expr x = ctx.bv_const("x", 8);
expr y = ctx.bv_const("y", 8);
expr phi = (x > 0) && (y < 10) && (x + y < 20);

// Create and use sampler
auto sampler = createQuickSampler(ctx);
auto samples = sampler->sample(phi, 100);