SMT Solving

SMT stands for Satisfiability Modulo Theories. It is a decision problem for logical formulas with respect to combinations of background theories.

This page gives the theory-level entry points. Specialized solver workflows, including parallel CDCL(T), are grouped alongside it in Logic and Solving.

Bit-Vectors, Floating Points, etc.

See bvfp_solver.py

Linear Arithmetic

See lira_solver.py

Strings

TBD