triz_synthesize
Searches finite behavior and resource alternatives across declared holes on fixed wiring, returning only complete implementations that satisfy one shared engineering contract.
Instructions
Search finite behavior/resource alternatives jointly on fixed wiring. Optimized search uses coupled residuals; symbolic search composes typed joint finite maps across explicit wire permutations and reuses equivalent residual domains before union trace enumeration, with bounded fallback; exhaustive retains the reference search. Every surviving tuple meets one shared engineering contract. Capped search is undecided; impossibility is only within the declared library.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| holes | Yes | ||
| model | Yes | Fixed carriers, boxes, ports, and wires. Only listed holes' complete behavior/resource declarations are substituted | |
| contract | Yes | ||
| max_work | No | ||
| strategy | No | Symbolic checks and composes typed joint serial maps before union trace enumeration; optimized uses coupled residuals; exhaustive retains the reference Cartesian search | optimized |
| max_states | No | ||
| optimizations | No | Disable individual optimizations for differential checks and benchmarks | |
| implementation | Yes | ||
| max_pruning_work | No | Per compilation/propagation allowance within max_work, reserving at least three quarters of remaining work for validation; exhaustion falls back without speculative pruning | |
| max_symbolic_work | No | ||
| max_symbolic_cells | No | Maximum retained symbolic certificate, mask and residual-cache characters; exhaustion discards compilation or skips cache insertion | |
| include_symbolic_certificate | No | Attempt checked compilation even for small requests and return its DAG for independent local Lean checking |