Expand description
Terms are the building blocks for constructing the mathematical expressions
used in assertions with Solver.
They are a statically-typed and ergonomic layer on top of
smtlib_lowlevel::ast::Term, which provides a more Rust-like API.
Structs§
- Const
- This struct wraps specific instances of other terms to indicate that they
are constant. Constants are named terms whose value can be extracted from a
model using
Model::eval. - Dynamic
- This type wraps terms loosing all static type information. It is particular useful when constructing terms dynamically.
- Label
- Labels are annotations that can be put on expressions to track their satisfiability.
- STerm
- A smtlib term with its associated storage.
Traits§
- IntoS
Term - Construct a
STermwith the presence ofStorage - Into
With Storage - Construct a
STermwith the presence ofStorage - Quantifier
Vars - This trait is implemented for types and sequences which can be used as
quantified variables in
forallandexists. - Sorted
- An trait for typing STM-LIB terms.
- Static
Sorted - A trait for statically typing STM-LIB terms.