CozySynthesizer / cozy

The collection synthesizer
https://cozy.uwplse.org
Apache License 2.0
209 stars 18 forks source link

Add lets inlining before encoding in TreeMultiset #97

Closed izgzhen closed 5 years ago

izgzhen commented 5 years ago

Fixes #95

Test:

>>> from cozy.structures.treemultiset import *
>>> from cozy.syntax import *
>>> e = ETreeMultisetElems(ELet(EBool(True).with_type(TBool()), ELambda(EVar('_var1186096').with_type(TBool()), EMakeMaxTreeMultiset(EEmptyList().with_type(TBag(TInt()))).with_type(TMaxTreeMultiset(TInt())))).with_type(TMaxTreeMultiset(TInt()))).with_type(TList(TInt()))
>>> O = Ordereds()
>>> O.encode(e)
ESorted(EEmptyList().with_type(TBag(TInt())), EBool(False).with_type(TBool())).with_type(TList(TInt()))
izgzhen commented 5 years ago

despite the fix, I am never confident about why I need to do one step of simplification