Synquid Improvement

We are trying to figure out ways to optimize the performance of enumeration in Synquid.

We have tried:

• Extend the succinct type system to support datatypes and refinement measures
• Build finite succinct type graph 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