search

CozySynthesizer / cozy

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

what is the use of to_heap in structures/heaps.py? #54

Closed izgzhen closed 6 years ago

Calvin-L commented 6 years ago

Given an EArgMin or EArgMax expression tree, to_heap outputs an expression that computes a heap that would be useful to implement the expression.

That is, EHeapPeek(to_heap(e)) should produce an expression that is semantically equivalent to e.

We should describe this in to_heap's docstring, which is very terse right now. Thanks for asking!

izgzhen commented 6 years ago

Oh I see, that's why I only saw it being used in tests:

cozy/structures/heaps.py:def to_heap(e : Exp) -> Exp:
tests/solver.py:    def test_to_heap(self):
tests/solver.py:            assert valid(EEq(e, EHeapPeek(to_heap(e), ELen(e)).with_type(INT)))