Module z3tracer::syntax [−][src]
Expand description
Terms and data structures found in Z3 logs.
Structs
| Ident | An identifier such as |
| Literal | A literal (i.e. a signed identifier). |
| Meaning | Additional data attached to a term (e.g. integer values). |
| QiInstance | Data specific to an instance of a quantifier instantiation (i.e. gathered between [instance] and [end-instance]). |
| QiKey | The hexadecimal index of a quantifier instantiation (QI). |
| VarName | A parameter declaration. |
Enums
| Equality | Description of an E-matching step. |
| MatchedTerm | Description of a term matching a trigger in |
| QiFrame | A quantifier instantiation as declared by [inst-discovered] or [new-match]. |
| Term | Concrete representation of a term. |
Traits
| Visitor | Visitor trait for syntactic constructs. |