Module smtgen

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

• ConcreteOutput
  An SMT computation for a concrete output of an encoding.
• ConcreteZ3Model
  A concrete SMT model of an encoding’s semantics, where all outputs have been instantiated and no longer contain any references to encoding parts.
• IntermediateOutput
  The output of a dataflow, which might still depend on the value of a part.
• PartIndex
  The index of a part in an encoding.
• PartName
  The name of a part
• Sizes
  The bit sizes of the parts in an encoding.
• StorageLocations
  A container that maps storage locations to SMT solver bitvectors.
• Z3Model
  An SMT solver mode of an encoding’s semantics.

Enums

• FilledLocation
  A storage location, which might be a concrete Location or a location that depends on a part in the instruction bitstring.
• FilledOutput
  An output, which might be a concrete Dest or a target that depends on a part in the instruction bitstring.