Skip to content

UnderstandingSMT

Jump to bottom
Kassing edited this page Mar 30, 2026 · 1 revision

SMT

AProVE has three distinct, mostly non-overlapping solver abstraction layers. Which one you encounter depends on the analysis component you are working in.

Layer Base type Used by Protocol
Engine layer Engine / SatEngine / SMTEngine (aprove.solver, aprove.solver.Engines) POLO, MATRO, KBO, Arctic polynomial coefficient search Single-shot: write full problem, call solver, read result
IDP LIA layer ISMTChecker (aprove.verification.idpframework) BigIntSMTEngine inside the IDP framework Single-shot QF_LIA via stdin/stdout

1. Engine Layer (aprove.solver / aprove.solver.Engines)

This is the layer most processors interact with when they need a SAT or SMT solver to find polynomial coefficients or matrix entries.

Base classes

Engine — abstract root, implements SATCheckerFactory. Subclasses either:

  • Override getSATChecker() (SAT path, via SatEngine), or
  • Override getSearchAlgorithm(ranges) (non-SAT/non-SMT path).

SatEngine — abstract, extends Engine. Handles formula construction parameters (simplify, sharing, orMode, andMode, nodeLimit, xorClauses). Subclasses only need to implement getSATChecker(). The returned SATChecker is consumed by a SatSearch loop that encodes polynomial constraints as CNF via a DiophantineSATConverter.

SMTEngine — abstract, extends Engine directly. Core API:

YNM satisfiable(List<Formula<SMTLIBTheoryAtom>>, SMTLogic, Abortion)
Pair<YNM, Map<String,String>> solve(List<Formula<SMTLIBTheoryAtom>>, SMTLogic, Abortion)
Pair<YNM, Map<String,String>> solve(String smtString, SMTLogic, Abortion)

Supported logics (enum SMTEngine.SMTLogic): QF_BV, QF_LIA, QF_NIA, QF_LRA, QF_NRA, QF_RA.

SMT engines bypass the Boolean encoding entirely — constraints go directly as SMTLIB2 to the solver. getSearchAlgorithm(ranges) wraps the engine in a DioSMTConverter+SMTSearch so it plugs into the same coefficient-search loop as SAT engines.

WrongLogicException is thrown when the formula's arithmetic exceeds what the chosen solver supports. Callers handle this by falling back or returning YNM.MAYBE.

SAT engines (all in aprove.solver.Engines, all extend SatEngine)

The only job of each SAT engine is returning the right SATChecker from getSATChecker().

Class Backing solver Notes
SAT4JEngine SAT4J (in-JVM Java) Default across most of AProVE. No subprocess, always available.
MINISATEngine MiniSAT (v1/v2/v2.1) Used in MATROFactory, some PADPProblem processors. Supports optional SatELite preprocessing and XOR clauses.
GlucoseEngine Glucose Requires glucose in $PATH.
CryptoMiniSATEngine CryptoMiniSAT Requires cryptominisat in $PATH.
PICOSATEngine PicoSAT Requires picosat in $PATH.
PrecosatEngine PrecoSAT Requires precosat in $PATH.
ManySATEngine ManySAT 1.1 Requires manysat11 in $PATH.
ClaspEngine Clasp 1.3.4 Requires clasp in $PATH.
RSATEngine RSAT File-based I/O.
SapperlotEngine Sapperlot File-based I/O.
MiniSAT09ZEngine MiniSAT 09z
MINISAT2IncrementalEngine MiniSAT 2 incremental
MINISATPEngine MinisatP CPU-prefetch variant; techniques from LPAR-17.
HeuristicMINISATEngine Heuristic MiniSAT Takes a node limit parameter.
YicesSATEngine Yices (SAT mode) Distinct from YicesEngine (SMT mode).
ExternalSATEngine Any external solver Strategy-configurable: takes a command and output pattern.
SATRaceEngine Any SAT Race-format solver Uses SAT Competition 2009 I/O format.
SATDumpEngine Wraps another engine Dumps CNF to disk while solving; debugging tool.
MultiSATEngine Up to 4 SAT engines Portfolio: runs multiple checkers in parallel.
MiniMaxSATEngine MiniMaxSAT Also implements MaxSATCheckerFactory; used with MaxSatSearch.

SMT engines (all in aprove.solver.Engines, all extend SMTEngine)

Class Backing solver Notes
YicesEngine Yices 1.x Default for LinearPOLOFactory, KBOPOLOFactory, ArcticPOLOFactory. Uses Yices 1 native format (not SMTLIB2). Throws WrongLogicException for QF_NIA. Writes to temp file, invokes yices -e.
SMTLIBEngine Any SMTLIB2 solver (default: Z3) Used by ItpfPolyDiophantineSmtSolver for QF_NIA. Writes SMTLIB2 to a temp file, invokes a configurable command.
SMTInterpolEngine SMTInterpol (in-JVM) Supported logics: QF_LIA, QF_LRA, QF_UF, UFLIA/UFLRA. No subprocess. Communicates via SMTLIB2 string through ParseEnvironment.

Non-SAT/non-SMT "search" engines (direct subclasses of Engine)

These implement getSearchAlgorithm(ranges) and bypass the SAT/SMT machinery entirely.

Class Backend
APROVEEngine AProVE itself (via named FIFOs), recursive self-call as Diophantine solver
CIMEEngine CIME (rewriting tool)
FDSEARCHEngine Finite-domain bounded enumeration
PBSEARCHEngine Pseudo-Boolean solvers (Pueblo, MiniSAT+, or external)
RatSolverEngine RatSolver (rational arithmetic)
SICSTUSEngine SICStus Prolog (CLP)
MultiSolverEngine Valencia backend
DYNAMICNEGPOLOEngine Marker class — flags dynamic negative POLO mode
YNMPEVLEngine Marker class — flags YNM-PEVL evaluation mode

Utility: ExecHelper (aprove.solver.Engines)

Shared subprocess launcher used by SMTLIBEngine, YicesEngine, and several SAT checkers. Runs a command via ProcessBuilder, drains stdout and stderr concurrently, and respects the Abortion signal via TrackerFactory.process(aborter, process). Returns Pair<List<String>, List<String>> (stdout lines, stderr lines).

2. IDP LIA Layer (aprove.verification.idpframework.Processors.Poly)

A separate, smaller SMT abstraction used only inside the IDP (Innermost Dependency Pairs) framework. Not connected to the Engine hierarchy.

IDPSMTEngine<C> (interface) — operates on ItpfConjClause (conjunction of polynomial constraints) and PolyInterpretation. Key methods:

  • getVarSignum(...) — determines the sign (pos/neg/zero/unknown/contradiction) of each variable algebraically.
  • isUnsolvable(...) — tests for contradictions.
  • getLinearSolvableClauses(...) / isLinearPartSolvable(...) — filters to the linear subproblem and checks satisfiability via a true SMT solver.

BigIntSMTEngine implements IDPSMTEngine<BigInt>:

  • Non-linear part: pure sign-propagation algebra, no SMT call.
  • Linear part: converts to LIAConstraint objects (QF_LIA) and delegates to an ISMTChecker.

ISMTChecker (interface): YNM isSatisfiable(ImmutableBoolOp<LIAConstraint> formula, Abortion aborter).

YicesChecker (in aprove.verification.dpframework.DPProblem.SMT_LIA.SMTLIB) — default ISMTChecker. Invokes yices -smt as a subprocess via stdin, using SMTLIB1 format. This is distinct from YicesEngine in the engine layer (different format, different I/O method).

QActiveSolver

These live in aprove.verification.dpframework.DPProblem and are used for usable-rules and active-constraint solving in the DP framework. They are not part of the engine layer above.

  • ImprovedQActiveSolver
    • QDPPoloSolver
    • QDPNegPoloSolver
  • PMatroArcticSMTSolver
  • QDPKBOSMTSolver
  • QCSDPNegCoeffPoloSolver
  • GPoloNatSolver

AbortableConstraintSolver

  • KBOSMTSolver

Clone this wiki locally