search

muraliadithya / mini-sygus

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

Optimise SMT encoding in cleanup branch #11

Closed muraliadithya closed 3 years ago

muraliadithya commented 3 years ago

The SMT encoding in the cleanup branch does not optimise for nonterminals with only one production rule. This leads to many more booleans being created than are actually necessary.

muraliadithya commented 3 years ago

Closed with commit e1d358c493423c5125268193bf11a0fc31eb7b77