[][src]Module gf::smt

SMT formulas and solvers.

Structs

BoundExpr

Bound expression.

ConstExpr

Expression that can be evaluated to a constant value.

ConstFn

Function expression that can be evaluated to a constant value given values of its arguments.

Expr

SMT expression.

Sort

SMT sort.

Enums

BoundExprError

Bound expression evaluation error.

ExprError

Expression construction or evaluation error.

ExprKind

Expression kind.

ExprValue

Expression value.

SortKind

Sort kind.

Traits

Binding

A binding in a BoundExpr.