Scope

ff-smt formalizes a typed language for satisfiability-modulo-theories problems over Booleans and integers. Its core covers sorts, declaration contexts, typed variables, environments, expressions, evaluation, rendered solver scripts, and problems assembled from assertions and a conclusion. The syntax and derived layers add readable logical connectives, integer relations, conditionals, interval predicates, and aggregate Boolean constraints. The semantic layer connects computed truth values with propositions for holding and refuting formulas, then lifts that account to statements and counterexamples. Progressive, advanced, showcase, and systems examples are paired with rendering-focused tests that exercise the language across increasingly structured problems.

Most important results

Context- and sort-indexed expressions ensure that variables and operators can only be combined at compatible types. The core supplies total evaluation together with renderers for declarations, expressions, assertions, counterexample checks, and counterexample queries. The semantics establishes both directions between evaluation and the holding or refuting interpretation, including soundness and completeness results for integer comparisons and Boolean connectives. Counterexample records yield refutations of statements, while the derived layer packages reusable constructions such as bounds, minima, maxima, clamping, cardinality constraints, and Boolean indicators.