Solver Tools

This page documents the small command-line front-ends under tools/solver/.

OWL – SMT/Model Checking Front-End

owl is a lightweight front-end for feeding SMT-LIB2 problems to the configured SMT solver (Z3 in the default build).

Binary: owl Location: tools/solver/owl.cpp

Note: This tool is optional and must be enabled with BUILD_OWL=ON during CMake configuration.

Usage:

./build/bin/owl file.smt2

Example:

./build/bin/owl examples/solver/example.smt2

See SMT (Satisfiability Modulo Theories) for details about the solver stack.

SLOT – SMT-LIB to LLVM Translator

slot translates SMT-LIB2 formulas into LLVM IR and can optionally run a small optimization pipeline over the generated function.

Binary: slot

Source: tools/solver/slot.cpp

Basic usage:

./build/bin/slot -s query.smt2 -o query.ll
./build/bin/slot -s query.smt2 -o query.ll -pall

Important options:

  • -s <file> – input SMT-LIB2 file

  • -o <file> – output file

  • -lu <file> / -lo <file> – dump LLVM before or after optimization

  • -m – rewrite constant shifts as multiplication

  • -pall – run the built-in optimization pipeline

SLOT can also run individual LLVM passes such as -instcombine, -sccp, -dce, and -gvn.

STAUB – Bounded-Theory Conversion Front-End

staub rewrites unbounded SMT constraints into bounded encodings before translation or solving.

Binary: staub

Source: tools/solver/staub.cpp

Basic usage:

./build/bin/staub -s query.smt2 -i aix -o bounded.smt2
./build/bin/staub -s query.smt2 -r 8,24 -o bounded.smt2

Important options:

  • -s <file> – input SMT-LIB2 file

  • -o <file> – output transformed formula

  • -t <file> – write statistics

  • -l – emit output compatible with SLOT

  • -i <N|aix|aix2> – integer bounding mode

  • -r <ebits,sbits|aix|aix4> – floating-point bounding mode