Structs§
- Bind
Power Pair - Child
Index - Child
Path - Child
Range - DeParse
- Fallback
Formatter - Formatter
- Formatter
Const - Match
Result - Matcher
- Matcher
Const - Parse
Error - Parse
Error Const - Regex
Matcher - SubFormatter
Repeat - SubFormatter
Repeat Const - SubFormatter
Repeat Separator - SubFormatter
Single - SubFormatter
String - Term
Display - Term
Display Const - Term
Display Context
Enums§
- Conversion
Error - Either
Error - Fallback
Parse Error - Formatter
Error - Matcher
Error - Matcher
Kind - Matcher
Kind Const - SubFormatter
- SubFormatter
Const - TdcError
Constants§
- BINARY_
OP - I’m not sure all of these are necessary since z3 generally breaks up terms,
e.g.
(>= _ _)into(and (= _ _) (< _ _)), or(=> _ _)into(or (not _) _). - CONTROL_
CHARACTER - DEFAULT_
BIND_ POWER - DEFAULT_
FORMATTER - IF
- NEG
- QUANT_
BIND - SEPARATOR_
CHARACTER - S_
EXPRESSION - S_
EXPRESSION_ LEAF - S_
EXPRESSION_ PATTERN - TRIGGER
- UNARY_
OP