[−][src]Module gf::smt

🟢 SMT expressions, formulas, and satisfiability checking.

We use the QF_UFBV logic (quantifier-free bit vectors and uninterpreted functions).

Modules

⚪ Expression simplification.

EmptySolverModel	⚪ Implementation of `SolverModel` that returns `None` for any input expression.
Expr	🟢 Expression.
Formula	Formula, a collection of asserted expressions.
Sort	🟢 Sort.

ExprKind	🟢 Expression kind.
ExprValue	🟢 Expression value.
SolverResult	⚪ Result of a `SolverInstance::solve` invocation.
SortKind	🟢 Sort kind.

SolverInstance	⚪ An SMT solver instance.
SolverModel	⚪ A model generated for a satisfiable assertion set.