Expand description
This module contains the definition of an smt_encoder which is used to check if a steady error path is spurious or not. It stores and manages all the smt variables that are constructed for the smt solver.
Structs§
- IndexedSMT
Context 🔒 - An indexed SMT Context which creates and manages smt variables for parameters and indexed smt variables for Locations, Variables and Rules
- SMTEncoder
Steady - Type representing an SMT Encoder which is used to encode a steady error path and checking it for spuriousness.
- Spurious
Result - Custom struct that stores the result of the Spurious Check
- _Replacing
Context 🔒 - This context allows to use a custom SMT expression instead of a variable when encoding expressions into SMT
Enums§
- SMTEncoder
Error 🔒 - Custom Error type to indicate an error
when calling the
SMTEncoder