We are trying to figure out ways to optimize the performance of enumeration in Synquid.
We have tried:
- Extend the
succinct type systemto support datatypes and refinement measures - Build finite
succinct typegraph for polymorphic types - Search expressions by traversal in the weighted, directed graph with heuristic ranking function
- Wisely keep search state after branch abduction
We will try:
- Add symmetric reduction