Crate aws_smt_ir
source · [−]Expand description
Intermediate representation for SMT-LIB formulas.
Re-exports
Modules
Representations of SMT-LIB logics.
Intermediate representation for SMT-LIB terms.
Macros
Unwraps a ControlFlow
or propagates its Break
value.
This replaces the Try
implementation that would be used
with std::ops::ControlFlow
.
Structs
Ctx
tracks the global context of a script (e.g. defined sorts and functions), along with local
context inside of terms (e.g. variables bound by let
, forall
, exists
).
Script
represents an entire SMT-LIB script i.e. sequence of commands.
Enums
Functions
Applies each
to each adjacent pair of arguments in args
, corresponding to the :chainable
SMT-LIB attribute.
Applies each
to each distinct pair of arguments in args
, corresponding to the :pairwise
SMT-LIB attribute.
Parses an SMT-LIB file, returning an iterator of parsed SMT-LIB commands.
Applies a fallible function to each adjacent pair of arguments in args
, corresponding to the
:chainable
SMT-LIB attribute.
Applies a fallible function to each distinct pair of arguments in args
, corresponding to the
:pairwise
SMT-LIB attribute.
Type Definitions
An uninhabited type, useful for defining theories that contain no operations beyond those in SMT-LIB’s Core theory.