Expand description
World-based inverse reasoning for Lemma rules
Determines what inputs produce desired outputs through world enumeration. A “world” is a complete assignment of which branch is active for each rule.
The main entry point is invert(), which returns an InversionResponse
containing all valid solutions with their domains.
Structs§
- Inversion
Response - Response from inversion containing all valid solutions
- Solution
- A single solution from inversion
- Target
- Desired outcome for an inversion query
- World
- A world assigns each rule to one of its branch indices
Enums§
- Bound
- Bound specification for ranges
- Domain
- Domain specification for valid values
- Target
Op - Comparison operators for targets
Functions§
- extract_
domains_ from_ constraint - Extract domains for all facts mentioned in a constraint
- invert
- Invert a rule to find input domains that produce a desired outcome.