search

CozySynthesizer / cozy

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

priority queue errors with NotImplementedError #32

Closed sasha-s closed 6 years ago

sasha-s commented 6 years ago

Tried to generate code for the following definition:

Q:

    state l : Bag<Int>

    invariant true;

    op add(n : Int)
        l.add(n);

    query get_min()
        min l

    op extract_min()
      let x = min l;
      l.remove(x);

python3 -m cozy q.ds --c++ q.h crashes ... with heaps.py", line 174, in codegen raise NotImplementedError()

codegen.py is:

impl = Spec('Q', [], [], [('_var29', TBag(TInt())), ('_var724', TInt()), ('_var1831', TMap(TInt(), TBool())), ('_var6402', TBool()), ('_var10567', TMinHeap(TInt(), TInt())), ('_var10570', TInt()), ('_var22411', TBool()), ('_var32734', TBag(TInt())), ('_var51043', TInt()), ('_var80254', TMap(TInt(), TInt())), ('_var109036', TMinHeap(TInt(), TInt())), ('_var146605', TInt())], [], [Query('min_elt', 'public', [], (), EVar('_var724').with_type(TInt()), ''), Query('_query44', 'internal', [('n', TInt())], (), ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), '[add] additions to _var29'), Query('_query45', 'internal', [('n', TInt())], (), EEmptyList().with_type(TBag(TInt())), '[add] deletions from _var29'), Query('_query94', 'internal', [], (), EEmptyList().with_type(TBag(TInt())), '[extract_min] additions to _var29'), Query('_query95', 'internal', [], (), EBinOp(ECond(EHasKey(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var724').with_type(TInt())).with_type(TBool()), ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EBinOp(ECond(EHasKey(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var724').with_type(TInt())).with_type(TBool()), ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EArgMin(ECond(EHasKey(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var724').with_type(TInt())).with_type(TBool()), ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '[extract_min] deletions from _var29'), Query('_query763', 'internal', [('n', TInt())], (), ECond(EVar('_var6402').with_type(TBool()), EArgMin(EBinOp(ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), EVar('n').with_type(TInt())).with_type(TInt()), '[add] new value for _var724'), Query('_query866', 'internal', [], (), EHeapPeek2(EVar('_var10567').with_type(TMinHeap(TInt(), TInt())), EVar('_var10570').with_type(TInt())).with_type(TInt()), '[extract_min] new value for _var724'), Query('_query2688', 'internal', [('n', TInt())], (), EFilter(ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), ELambda(EVar('_var2466').with_type(TInt()), EUnaryOp('not', EHasKey(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var2466').with_type(TInt())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), '[add] new or modified keys from _var1831'), Query('_query6243', 'internal', [], (), EFilter(EVar('_var32734').with_type(TBag(TInt())), ELambda(EVar('_var61201').with_type(TInt()), EUnaryOp('not', ECond(EBool(True).with_type(TBool()), EBinOp(EMapGet(EVar('_var80254').with_type(TMap(TInt(), TInt())), EVar('_var61201').with_type(TInt())).with_type(TInt()), '>', ENum(1).with_type(TInt())).with_type(TBool()), EHasKey(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var61201').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), '[extract_min] keys removed from _var1831'), Query('_query7077', 'internal', [('n', TInt())], (), EBool(True).with_type(TBool()), '[add] new value for _var6402'), Query('_query7187', 'internal', [], (), EVar('_var22411').with_type(TBool()), '[extract_min] new value for _var6402'), Query('_query11276', 'internal', [], (), EVar('_var10570').with_type(TInt()), '[add] None'), Query('_query11282', 'internal', [('n', TInt())], (), ENum(0).with_type(TInt()), '[add] None'), Query('_query11300', 'internal', [('_var11293', TInt()), ('n', TInt())], (), ENum(0).with_type(TInt()), '[add] None'), Query('_query17696', 'internal', [('n', TInt())], (), EBinOp(EVar('_var10570').with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()), '[add] new value for _var10570'), Query('_query17927', 'internal', [], (), EUnaryOp('len', EBinOp(EHeapElems(EVar('_var109036').with_type(TMinHeap(TInt(), TInt()))).with_type(TBag(TInt())), '-', EHeapElems(EMakeMinHeap(EBinOp(EVar('_var32734').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var32734').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var790').with_type(TInt()), EVar('_var790').with_type(TInt()))).with_type(TMinHeap(TInt(), TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '[extract_min] None'), Query('_query17964', 'internal', [('_var17933', TInt())], (), ENum(0).with_type(TInt()), '[extract_min] None'), Query('_query23035', 'internal', [], (), EVar('_var51043').with_type(TInt()), '[extract_min] new value for _var10570'), Query('_query35412', 'internal', [('n', TInt())], (), EBinOp(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EVar('_var29').with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()), '-', ENum(1).with_type(TInt())).with_type(TInt()), EBinOp(EBinOp(EUnaryOp('len', EVar('_var29').with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()), '-', ENum(0).with_type(TInt())).with_type(TInt())).with_type(TInt()), '>', ENum(0).with_type(TInt())).with_type(TBool()), '[add] new value for _var22411'), Query('_query36133', 'internal', [], (), EBinOp(ECond(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var35638').with_type(TInt()), EVar('_var35638').with_type(TInt()))).with_type(TInt()), 'in', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EUnaryOp('len', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '-', ENum(1).with_type(TInt())).with_type(TInt()), EBinOp(EUnaryOp('len', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '-', ENum(0).with_type(TInt())).with_type(TInt())).with_type(TInt()), '>', ENum(0).with_type(TInt())).with_type(TBool()), '[extract_min] new value for _var22411'), Query('_query38230', 'internal', [('n', TInt())], (), ECond(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), ECond(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), EBinOp(ESingleton(EArgMin(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), '-', ESingleton(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(ESingleton(EArgMin(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), '-', EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ECond(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), EBinOp(EEmptyList().with_type(TBag(TInt())), '-', ESingleton(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EEmptyList().with_type(TBag(TInt())), '-', EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '[add] additions to _var32734'), Query('_query38240', 'internal', [('n', TInt())], (), ECond(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), ECond(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), EBinOp(ESingleton(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), '-', ESingleton(EArgMin(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(ESingleton(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), '-', EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ECond(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), EBinOp(EEmptyList().with_type(TBag(TInt())), '-', ESingleton(EArgMin(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EEmptyList().with_type(TBag(TInt())), '-', EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '[add] deletions from _var32734'), Query('_query45518', 'internal', [], (), ECond(ECond(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44087').with_type(TInt()), EVar('_var44087').with_type(TInt()))).with_type(TInt()), 'in', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44097').with_type(TInt()), EVar('_var44097').with_type(TInt()))).with_type(TInt()), 'in', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44109').with_type(TInt()), EVar('_var44109').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44117').with_type(TInt()), EVar('_var44117').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44122').with_type(TInt()), EVar('_var44122').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), ECond(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), EBinOp(ESingleton(EArgMin(ECond(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44128').with_type(TInt()), EVar('_var44128').with_type(TInt()))).with_type(TInt()), 'in', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44153').with_type(TInt()), EVar('_var44153').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44158').with_type(TInt()), EVar('_var44158').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), '-', ESingleton(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(ESingleton(EArgMin(ECond(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44128').with_type(TInt()), EVar('_var44128').with_type(TInt()))).with_type(TInt()), 'in', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44153').with_type(TInt()), EVar('_var44153').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var44158').with_type(TInt()), EVar('_var44158').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), '-', EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ECond(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), EBinOp(EEmptyList().with_type(TBag(TInt())), '-', ESingleton(EArgMin(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EEmptyList().with_type(TBag(TInt())), '-', EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '[extract_min] additions to _var32734'), Query('_query58222', 'internal', [('n', TInt())], (), ECond(EBool(True).with_type(TBool()), EVar('_var10570').with_type(TInt()), EBinOp(EVar('_var146605').with_type(TInt()), '-', ENum(0).with_type(TInt())).with_type(TInt())).with_type(TInt()), '[add] new value for _var51043'), Query('_query58811', 'internal', [], (), ECond(EUnaryOp('exists', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EUnaryOp('len', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '-', ENum(1).with_type(TInt())).with_type(TInt()), EBinOp(EUnaryOp('len', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EVar('_var724').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '-', ENum(0).with_type(TInt())).with_type(TInt())).with_type(TInt()), '[extract_min] new value for _var51043'), Query('_query84333', 'internal', [('n', TInt()), ('_var83413', TInt()), ('_var83414', TInt())], (), EBinOp(EUnaryOp('len', EFilter(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('_var61214').with_type(TInt()), EBinOp(EVar('_var83413').with_type(TInt()), '==', EVar('_var61214').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '+', ECond(EBinOp(EVar('_var83413').with_type(TInt()), '==', EVar('n').with_type(TInt())).with_type(TBool()), ENum(1).with_type(TInt()), ENum(0).with_type(TInt())).with_type(TInt())).with_type(TInt()), '[add] new value for _var83414'), Query('_query97908', 'internal', [('_var96625', TInt()), ('_var96632', TInt())], (), EUnaryOp('len', EFilter(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var61214').with_type(TInt()), EBinOp(EVar('_var96625').with_type(TInt()), '==', EVar('_var61214').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '[extract_min] new value for _var96632'), Query('_query97917', 'internal', [], (), EFilter(EUnaryOp('distinct', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var96625').with_type(TInt()), EBinOp(EUnaryOp('not', EBinOp(EVar('_var96625').with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', EBinOp(EUnaryOp('len', EFilter(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('_var61214').with_type(TInt()), EBinOp(EVar('_var96625').with_type(TInt()), '==', EVar('_var61214').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '==', EUnaryOp('len', EFilter(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var61214').with_type(TInt()), EBinOp(EVar('_var96625').with_type(TInt()), '==', EVar('_var61214').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), '[extract_min] new or modified keys from _var80254'), Query('_query109248', 'internal', [('n', TInt())], (), EUnaryOp('len', EBinOp(EHeapElems(EMakeMinHeap(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var790').with_type(TInt()), EVar('_var790').with_type(TInt()))).with_type(TMinHeap(TInt(), TInt()))).with_type(TBag(TInt())), '-', EHeapElems(EMakeMinHeap(ECond(EBinOp(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), 'or', EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var790').with_type(TInt()), EVar('_var790').with_type(TInt()))).with_type(TMinHeap(TInt(), TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '[add] None'), Query('_query109256', 'internal', [('_var109253', TInt()), ('n', TInt())], (), ENum(0).with_type(TInt()), '[add] None'), Query('_query121063', 'internal', [], (), EUnaryOp('len', EBinOp(EHeapElems(EMakeMinHeap(ECond(EBinOp(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), 'in', EVar('_var29').with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var790').with_type(TInt()), EVar('_var790').with_type(TInt()))).with_type(TMinHeap(TInt(), TInt()))).with_type(TBag(TInt())), '-', EHeapElems(EMakeMinHeap(ECond(EBinOp(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var121024').with_type(TInt()), EVar('_var121024').with_type(TInt()))).with_type(TInt()), 'in', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EArgMin(EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var121024').with_type(TInt()), EVar('_var121024').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var790').with_type(TInt()), EVar('_var790').with_type(TInt()))).with_type(TMinHeap(TInt(), TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '[extract_min] None'), Query('_query121109', 'internal', [('_var121085', TInt())], (), ENum(0).with_type(TInt()), '[extract_min] None'), Query('_query146856', 'internal', [('n', TInt())], (), EBinOp(EBinOp(EUnaryOp('len', EVar('_var29').with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()), '[add] new value for _var146605'), Query('_query147362', 'internal', [], (), EBinOp(EUnaryOp('len', EBinOp(EVar('_var29').with_type(TBag(TInt())), '-', ESingleton(EArgMin(EVar('_var29').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()), '[extract_min] new value for _var146605'), Op('add', [('n', TInt())], [], SSeq(SSeq(SSeq(SSeq(SDecl('_var164049', ECall('_query763', (EVar('n').with_type(TInt()),)).with_type(TInt())), SDecl('_var164050', ECall('_query2688', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())))), SSeq(SDecl('_var164051', ECall('_query17927', ()).with_type(TInt())), SDecl('_var164052', EBinOp(ECall('_query17927', ()).with_type(TInt()), '-', ECall('_query109248', (EVar('n').with_type(TInt()),)).with_type(TInt())).with_type(TInt())))), SSeq(SSeq(SDecl('_var164053', ECall('_query17696', (EVar('n').with_type(TInt()),)).with_type(TInt())), SAssign(EVar('_var6402').with_type(TBool()), ECall('_query7077', (EVar('n').with_type(TInt()),)).with_type(TBool()))), SSeq(SSeq(SCall(EVar('_var10567').with_type(TMinHeap(TInt(), TInt())), 'remove_all', (ECall('_query11276', ()).with_type(TInt()), ECall('_query45', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())))), SSeq(SCall(EVar('_var10567').with_type(TMinHeap(TInt(), TInt())), 'add_all', (EBinOp(ECall('_query11276', ()).with_type(TInt()), '-', ECall('_query11282', (EVar('n').with_type(TInt()),)).with_type(TInt())).with_type(TInt()), ECall('_query44', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())))), SForEach(EVar('_var11293').with_type(TInt()), ECall('_query45', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SCall(EVar('_var10567').with_type(TMinHeap(TInt(), TInt())), 'update', (EVar('_var11293').with_type(TInt()), ECall('_query11300', (EVar('_var11293').with_type(TInt()), EVar('n').with_type(TInt()))).with_type(TInt())))))), SAssign(EVar('_var146605').with_type(TInt()), ECall('_query146856', (EVar('n').with_type(TInt()),)).with_type(TInt()))))), SSeq(SSeq(SSeq(SAssign(EVar('_var22411').with_type(TBool()), ECall('_query35412', (EVar('n').with_type(TInt()),)).with_type(TBool())), SAssign(EVar('_var10570').with_type(TInt()), EVar('_var164053').with_type(TInt()))), SSeq(SSeq(SCall(EVar('_var109036').with_type(TMinHeap(TInt(), TInt())), 'remove_all', (EVar('_var164051').with_type(TInt()), ECall('_query38240', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())))), SSeq(SCall(EVar('_var109036').with_type(TMinHeap(TInt(), TInt())), 'add_all', (EVar('_var164052').with_type(TInt()), ECall('_query38230', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())))), SForEach(EVar('_var109253').with_type(TInt()), ECall('_query45', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SCall(EVar('_var109036').with_type(TMinHeap(TInt(), TInt())), 'update', (EVar('_var109253').with_type(TInt()), ECall('_query109256', (EVar('_var109253').with_type(TInt()), EVar('n').with_type(TInt()))).with_type(TInt())))))), SAssign(EVar('_var51043').with_type(TInt()), ECall('_query58222', (EVar('n').with_type(TInt()),)).with_type(TInt())))), SSeq(SSeq(SSeq(SForEach(EVar('_var83413').with_type(TInt()), ECall('_query45', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SMapDel(EVar('_var80254').with_type(TMap(TInt(), TInt())), EVar('_var83413').with_type(TInt()))), SForEach(EVar('_var83413').with_type(TInt()), ECall('_query44', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SMapUpdate(EVar('_var80254').with_type(TMap(TInt(), TInt())), EVar('_var83413').with_type(TInt()), EVar('_var83414').with_type(TInt()), SAssign(EVar('_var83414').with_type(TInt()), ECall('_query84333', (EVar('n').with_type(TInt()), EVar('_var83413').with_type(TInt()), EVar('_var83414').with_type(TInt()))).with_type(TInt()))))), SSeq(SForEach(EVar('_var38247').with_type(TInt()), ECall('_query38240', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SCall(EVar('_var32734').with_type(TBag(TInt())), 'remove', (EVar('_var38247').with_type(TInt()),))), SForEach(EVar('_var38247').with_type(TInt()), ECall('_query38230', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SCall(EVar('_var32734').with_type(TBag(TInt())), 'add', (EVar('_var38247').with_type(TInt()),))))), SSeq(SSeq(SForEach(EVar('_var46').with_type(TInt()), ECall('_query45', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SCall(EVar('_var29').with_type(TBag(TInt())), 'remove', (EVar('_var46').with_type(TInt()),))), SForEach(EVar('_var46').with_type(TInt()), ECall('_query44', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SCall(EVar('_var29').with_type(TBag(TInt())), 'add', (EVar('_var46').with_type(TInt()),)))), SSeq(SAssign(EVar('_var724').with_type(TInt()), EVar('_var164049').with_type(TInt())), SSeq(SForEach(EVar('_var2466').with_type(TInt()), ECall('_query45', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())), SMapDel(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var2466').with_type(TInt()))), SForEach(EVar('_var2466').with_type(TInt()), EVar('_var164050').with_type(TBag(TInt())), SMapUpdate(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var2466').with_type(TInt()), EVar('_var2467').with_type(TBool()), SNoOp())))))))), ''), Op('extract_min', [], [], SSeq(SSeq(SSeq(SSeq(SDecl('_var164054', ECall('_query17927', ()).with_type(TInt())), SDecl('_var164055', EBinOp(ECall('_query17927', ()).with_type(TInt()), '-', ECall('_query121063', ()).with_type(TInt())).with_type(TInt()))), SSeq(SDecl('_var164056', ECall('_query6243', ()).with_type(TBag(TInt()))), SDecl('_var164057', ECall('_query6243', ()).with_type(TBag(TInt()))))), SSeq(SSeq(SDecl('_var164058', ECall('_query866', ()).with_type(TInt())), SDecl('_var164059', ECall('_query6243', ()).with_type(TBag(TInt())))), SSeq(SAssign(EVar('_var6402').with_type(TBool()), ECall('_query7187', ()).with_type(TBool())), SSeq(SSeq(SCall(EVar('_var10567').with_type(TMinHeap(TInt(), TInt())), 'remove_all', (ECall('_query11276', ()).with_type(TInt()), ECall('_query95', ()).with_type(TBag(TInt())))), SSeq(SCall(EVar('_var10567').with_type(TMinHeap(TInt(), TInt())), 'add_all', (EBinOp(ECall('_query11276', ()).with_type(TInt()), '-', ECall('_query17927', ()).with_type(TInt())).with_type(TInt()), ECall('_query94', ()).with_type(TBag(TInt())))), SForEach(EVar('_var17933').with_type(TInt()), ECall('_query94', ()).with_type(TBag(TInt())), SCall(EVar('_var10567').with_type(TMinHeap(TInt(), TInt())), 'update', (EVar('_var17933').with_type(TInt()), ECall('_query17964', (EVar('_var17933').with_type(TInt()),)).with_type(TInt())))))), SAssign(EVar('_var146605').with_type(TInt()), ECall('_query147362', ()).with_type(TInt())))))), SSeq(SSeq(SSeq(SAssign(EVar('_var22411').with_type(TBool()), ECall('_query36133', ()).with_type(TBool())), SAssign(EVar('_var10570').with_type(TInt()), ECall('_query23035', ()).with_type(TInt()))), SSeq(SSeq(SCall(EVar('_var109036').with_type(TMinHeap(TInt(), TInt())), 'remove_all', (EVar('_var164054').with_type(TInt()), ECall('_query6243', ()).with_type(TBag(TInt())))), SSeq(SCall(EVar('_var109036').with_type(TMinHeap(TInt(), TInt())), 'add_all', (EVar('_var164055').with_type(TInt()), ECall('_query45518', ()).with_type(TBag(TInt())))), SForEach(EVar('_var121085').with_type(TInt()), ECall('_query94', ()).with_type(TBag(TInt())), SCall(EVar('_var109036').with_type(TMinHeap(TInt(), TInt())), 'update', (EVar('_var121085').with_type(TInt()), ECall('_query121109', (EVar('_var121085').with_type(TInt()),)).with_type(TInt())))))), SAssign(EVar('_var51043').with_type(TInt()), ECall('_query58811', ()).with_type(TInt())))), SSeq(SSeq(SSeq(SForEach(EVar('_var96625').with_type(TInt()), EVar('_var164056').with_type(TBag(TInt())), SMapDel(EVar('_var80254').with_type(TMap(TInt(), TInt())), EVar('_var96625').with_type(TInt()))), SForEach(EVar('_var96625').with_type(TInt()), ECall('_query97917', ()).with_type(TBag(TInt())), SMapUpdate(EVar('_var80254').with_type(TMap(TInt(), TInt())), EVar('_var96625').with_type(TInt()), EVar('_var96632').with_type(TInt()), SAssign(EVar('_var96632').with_type(TInt()), ECall('_query97908', (EVar('_var96625').with_type(TInt()), EVar('_var96632').with_type(TInt()))).with_type(TInt()))))), SSeq(SForEach(EVar('_var45536').with_type(TInt()), EVar('_var164057').with_type(TBag(TInt())), SCall(EVar('_var32734').with_type(TBag(TInt())), 'remove', (EVar('_var45536').with_type(TInt()),))), SForEach(EVar('_var45536').with_type(TInt()), ECall('_query45518', ()).with_type(TBag(TInt())), SCall(EVar('_var32734').with_type(TBag(TInt())), 'add', (EVar('_var45536').with_type(TInt()),))))), SSeq(SSeq(SForEach(EVar('_var96').with_type(TInt()), ECall('_query95', ()).with_type(TBag(TInt())), SCall(EVar('_var29').with_type(TBag(TInt())), 'remove', (EVar('_var96').with_type(TInt()),))), SForEach(EVar('_var96').with_type(TInt()), ECall('_query94', ()).with_type(TBag(TInt())), SCall(EVar('_var29').with_type(TBag(TInt())), 'add', (EVar('_var96').with_type(TInt()),)))), SSeq(SAssign(EVar('_var724').with_type(TInt()), EVar('_var164058').with_type(TInt())), SSeq(SForEach(EVar('_var6241').with_type(TInt()), EVar('_var164059').with_type(TBag(TInt())), SMapDel(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var6241').with_type(TInt()))), SForEach(EVar('_var6241').with_type(TInt()), ECall('_query94', ()).with_type(TBag(TInt())), SMapUpdate(EVar('_var1831').with_type(TMap(TInt(), TBool())), EVar('_var6241').with_type(TInt()), EVar('_var6242').with_type(TBool()), SNoOp())))))))), '')], '', '', '')
state_map = OrderedDict([('_var29', EVar('l').with_type(TBag(TInt()))), ('_var724', EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())), ('_var1831', EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var657').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))), ('_var6402', EUnaryOp('exists', EVar('l').with_type(TBag(TInt()))).with_type(TBool())), ('_var10567', EMakeMinHeap(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var790').with_type(TInt()), EVar('_var790').with_type(TInt()))).with_type(TMinHeap(TInt(), TInt()))), ('_var10570', EUnaryOp('len', EVar('l').with_type(TBag(TInt()))).with_type(TInt())), ('_var22411', EBinOp(EBinOp(EUnaryOp('len', EVar('l').with_type(TBag(TInt()))).with_type(TInt()), '-', ECond(EHasKey(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var19933').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), ENum(1).with_type(TInt()), ENum(0).with_type(TInt())).with_type(TInt())).with_type(TInt()), '>', ENum(0).with_type(TInt())).with_type(TBool())), ('_var32734', ECond(ECond(EHasKey(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var657').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBinOp(EArgMin(ECond(EHasKey(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var657').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), ESingleton(EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()), '==', EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool())).with_type(TBool()), ESingleton(EArgMin(ECond(EHasKey(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var657').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBool()), ESingleton(EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))), ('_var51043', EBinOp(EUnaryOp('len', EVar('l').with_type(TBag(TInt()))).with_type(TInt()), '-', ECond(EUnaryOp('exists', EVar('l').with_type(TBag(TInt()))).with_type(TBool()), ENum(1).with_type(TInt()), ENum(0).with_type(TInt())).with_type(TInt())).with_type(TInt())), ('_var80254', EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var61207').with_type(TInt()), EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var61214').with_type(TInt()), EBinOp(EVar('_var61207').with_type(TInt()), '==', EVar('_var61214').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))), ('_var109036', EMakeMinHeap(EMapGet(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_key54901').with_type(TInt()), ESingleton(EVar('_key54901').with_type(TInt())).with_type(TBag(TInt())))).with_type(TMap(TInt(), TBag(TInt()))), EArgMin(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TBag(TInt())), ELambda(EVar('_var790').with_type(TInt()), EVar('_var790').with_type(TInt()))).with_type(TMinHeap(TInt(), TInt()))), ('_var146605', EBinOp(EUnaryOp('len', EVar('l').with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()))])
share_info = defaultdict(<class 'list'>, {})
Calvin-L commented 6 years ago

Thanks for reporting this!

Heaps are currently a beta feature in Cozy, and there are still several unimplemented or untested cases. Please get in touch if you encounter any more problems.