[][src]Module gf::smt

🟢 SMT expressions, formulas, and satisfiability checking.

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

Modules

simplifier

⚪ Expression simplification.

Structs

EmptySolverModel

⚪ Implementation of SolverModel that returns None for any input expression.

Expr

🟢 Expression.

Formula

Formula, a collection of asserted expressions.

Sort

🟢 Sort.

Enums

ExprKind

🟢 Expression kind.

ExprValue

🟢 Expression value.

SolverResult

⚪ Result of a SolverInstance::solve invocation.

SortKind

🟢 Sort kind.

Traits

SolverInstance

⚪ An SMT solver instance.

SolverModel

⚪ A model generated for a satisfiable assertion set.