search

muraliadithya / mini-sygus

a constraint-based syntax-guided synthesis (SyGuS) engine
9 stars 0 forks source link

Add support for infinite grammar in breadth_first branch #15

Open eionblanc opened 3 years ago

eionblanc commented 3 years ago

The breadth_first branch currently supports a max_depth specification for compute_constraint_encoding, unpacking the SyGuS grammar only up to the specified depth. This, I think, was the main hurdle toward supporting infinite grammars. The remaining issues that I'm aware of follow, all of which I suspect will not be too difficult:

  1. Enable function print ordering to be determined by dependence. For finite grammars, the nonterminals may be ordered by dependence of the replacement rules. For infinite grammars (with self-referential rules), this is no longer the case. So for the pretty_smt_encoding, we must print functions according to actual dependence of the nonterminal copies so that when the SMT file is passed to a solver, functions are defined in the correct order. For example, if B1_0 calls B2_0 which then calls B1_1, these need to be printed in reverse order to the SMT file and cannot be partitioned into a B1 block and a B2 block as has been our approach.
  2. Cosmetic checks. For example, removing the exception raised if is_finite returns False.
  3. Adjusting the call_solver and sygus_to_smt functions. To manage the actual breadth first search approach (necessary for infinite grammars), we have discussed an "outer loop" managing an incrementing max_depth parameter until the result is sat or a universal depth maximum (parameter) is hit.
eionblanc commented 3 years ago

All three components are now complete (changes made to engine.py's solve function rather than call_solver). The tests in tests/ output the same output as in the main branch, and results seem reasonable for some toy infinite grammars. More testing on actual infinite grammar examples is needed!