Module smtgen
Expand description
Provides Z3Model and ConcreteZ3Model, SMT models that can be generated for uninstantiated encodings.
Z3Model uses part indices in its representation,
while ConcreteZ3Model uses a bitvector representation of the instruction to translate part mappings into SMT expressions.
Structs§
- Concrete
Output - An SMT computation for a concrete output of an encoding.
- Concrete
Z3Model - A concrete SMT model of an encoding’s semantics, where all outputs have been instantiated and no longer contain any references to encoding parts.
- Intermediate
Output - The output of a dataflow, which might still depend on the value of a part.
- Part
Index - The index of a part in an encoding.
- Part
Name - The name of a part
- Sizes
- The bit sizes of the parts in an encoding.
- Storage
Locations - A container that maps storage locations to SMT solver bitvectors.
- Z3Model
- An SMT solver mode of an encoding’s semantics.
Enums§
- Filled
Location - A storage location, which might be a concrete
Locationor a location that depends on a part in the instruction bitstring. - Filled
Output - An output, which might be a concrete
Destor a target that depends on a part in the instruction bitstring.