SMT solving
Logic fragment
A named restriction on the terms allowed in a solver query.
Definition
Logic fragment
A logic fragment identifies a combination of theories and syntactic restrictions.
The fragment name lets users and solvers state the intended problem class. QF means quantifier-free; the remaining letters identify theories such as bit-vectors or integer arithmetic.
01
Example
QF_BV permits quantifier-free formulas over fixed-width bit-vectors.
02
Important distinction
Two fragments can share operators while requiring different decision procedures or completeness claims.
After reading this article, you should be able to
- Define Logic fragment in the sense used on this site.
- Decode the main parts of a common SMT-LIB logic name.