Scope

ff-smt-unsafe is the execution-facing companion to ff-smt, coupling its formal SMT problem and statement representations to an external Z3 process during Agda type checking. Its Z3 module combines Agda reflection with executable invocation and the solver’s SMT-LIB input and output protocol, which is why the library flags include --allow-exec. The assumption modules apply that bridge to baseline, progressive, advanced, showcase, and systems examples. Covered problem families include linear and affine arithmetic, guarded and nested Boolean constraints, propositional patterns, queues, scheduling, and quorum conditions. A dedicated test hierarchy separates raw solver features from progressive, advanced, showcase, systems, and integration checks.

Most important results

The Z3 module supplies a reflected z3CheckedStatement macro backed by an executable solver invocation and explicit handling of process output. Progressive assumption modules specialize solver-checked statement types for linear transitivity, equality chains, affine monotonicity, guarded conditionals, and nested Boolean guards. Systems assumptions cover queue-bound preservation, nonoverlapping task schedules, and three-member quorum coverage. Sixteen checked modules, including raw-feature and integration tests, collectively exercise the unsafe bridge against its ff-smt dependency.