diff --git a/cozy/codegen/cxx.py b/cozy/codegen/cxx.py index 1d3649a4..87bf9a4e 100644 --- a/cozy/codegen/cxx.py +++ b/cozy/codegen/cxx.py @@ -8,6 +8,7 @@ from cozy.syntax_tools import all_types, fresh_var, subst, free_vars, all_exps, break_seq, is_lvalue from cozy.typecheck import is_collection, is_scalar from cozy.structures import extension_handler +from cozy.structures.arrays import TArray, EArrayGet from .misc import * @@ -348,7 +349,9 @@ def visit_EListGet(self, e): evaluation.construct_value(e.type)).with_type(e.type))).with_type(e.type)) def visit_EArrayIndexOf(self, e): - assert isinstance(e.a, EVar) # TODO: make this fast when this is false + if isinstance(e.a, EVar): pass + elif isinstance(e.a, ETupleGet) and isinstance(e.a.e, EVar): pass + else: raise NotImplementedError("finding index of non-var array") # TODO: make this fast when this is false it = self.fv(TNative("{}::const_iterator".format(self.visit(e.a.type, "").strip())), "cursor") res = self.fv(INT, "index") self.visit(seq([ @@ -374,6 +377,9 @@ def visit_EMakeMap2(self, e): self.declare(m, e) return m.id + def visit_EArrayList(self, e): + return "(std::vector< {} >())".format(self.visit(e.type.elem_type, "")) + def visit_EHasKey(self, e): map = self.visit(e.map) key = self.visit(e.key) @@ -980,6 +986,12 @@ def setup_types(self, spec, state_exps, sharing): if t not in self.types and type(t) in [THandle, TRecord, TTuple, TEnum]: name = names.get(t, self.fn("Type")) self.types[t] = name + # add representation type for extension data structures + h = extension_handler(type(t)) + if t not in self.types and h is not None: + name = names.get(t, self.fn("Type")) + t = h.rep_type(t) + self.types[t] = name def visit_args(self, args): for (i, (v, t)) in enumerate(args): @@ -998,17 +1010,32 @@ def _hasher(self, t : Type) -> str: except KeyError: return "std::hash<{}>".format(self.visit(t, "")) - def compute_hash_1(self, e : Exp) -> Exp: + def compute_hash_scalar(self, e: Exp) -> Exp: return EEscape("{hasher}()({{e}})".format(hasher=self._hasher(e.type)), ("e",), (e,)).with_type(TNative("std::size_t")) + def compute_hash_1(self, hc: Exp, e : Exp) -> Stm: + if is_scalar(e.type): + return SAssign(hc, self.compute_hash_scalar(e)) + elif isinstance(e.type, TArray): + x = fresh_var(e.type.elem_type, "x") + s = SSeq(SAssign(hc, ZERO.with_type(hc.type)), + SForEach(x, e, + SAssign(hc, EEscape("({hc} * 31) ^ ({h})", ("hc", "h"), + (hc, self.compute_hash_scalar(x))).with_type(TNative("std::size_t"))))) + return s + else: + raise NotImplementedError("can't compute hash for type {}".format(e.type)) + def compute_hash(self, fields : [Exp]) -> Stm: hc = self.fv(TNative("std::size_t"), "hash_code") - s = SDecl(hc, ENum(0).with_type(hc.type)) + h = self.fv(TNative("std::size_t"), "hash_code") + s = SSeq(SDecl(hc, ENum(0).with_type(hc.type)), + SDecl(h, ENum(0).with_type(h.type))) for f in fields: - # return SAssign(out, ) - s = SSeq(s, SAssign(hc, - EEscape("({hc} * 31) ^ ({h})", ("hc", "h"), - (hc, self.compute_hash_1(f))).with_type(TNative("std::size_t")))) + s = seq([s, + self.compute_hash_1(h, f), + SAssign(hc, + EEscape("({hc} * 31) ^ ({h})", ("hc", "h"), (hc, h)).with_type(TNative("std::size_t")))]) s = SSeq(s, SEscape("{indent}return {e};\n", ("e",), (hc,))) return s diff --git a/cozy/codegen/java.py b/cozy/codegen/java.py index fff0ba5a..17e0d0a7 100644 --- a/cozy/codegen/java.py +++ b/cozy/codegen/java.py @@ -136,6 +136,9 @@ def body(x): self.end_statement() self.end_statement() + def visit_EArrayList(self, e): + return "(new {}[0])".format(self.visit(e.type.elem_type, "")) + def initialize_native_list(self, out): init = "new {};\n".format(self.visit(out.type, name="()")) return SEscape("{indent}{e} = " + init, ["e"], [out]) diff --git a/cozy/structures/arrays.py b/cozy/structures/arrays.py index da19d3c2..fc5558d0 100644 --- a/cozy/structures/arrays.py +++ b/cozy/structures/arrays.py @@ -2,6 +2,7 @@ from cozy.syntax import Type, Exp, Stm TArray = declare_case(Type, "TArray", ["elem_type"]) +EArrayList = declare_case(Exp, "EArrayList", []) EArrayCapacity = declare_case(Exp, "EArrayCapacity", ["e"]) EArrayLen = declare_case(Exp, "EArrayLen", ["e"]) EArrayGet = declare_case(Exp, "EArrayGet", ["a", "i"]) diff --git a/cozy/structures/heaps.py b/cozy/structures/heaps.py index 6d03412b..48a0e5b7 100644 --- a/cozy/structures/heaps.py +++ b/cozy/structures/heaps.py @@ -4,7 +4,7 @@ from cozy.syntax_tools import fresh_var, pprint, mk_lambda, alpha_equivalent from cozy.pools import Pool, RUNTIME_POOL, STATE_POOL -from .arrays import TArray, EArrayGet, EArrayIndexOf, SArrayAlloc, SEnsureCapacity, EArrayLen +from .arrays import TArray, EArrayGet, EArrayIndexOf, SArrayAlloc, SEnsureCapacity, EArrayLen, EArrayList TMinHeap = declare_case(Type, "TMinHeap", ["elem_type", "key_type"]) TMaxHeap = declare_case(Type, "TMaxHeap", ["elem_type", "key_type"]) @@ -14,8 +14,8 @@ EMakeMaxHeap = declare_case(Exp, "EMakeMaxHeap", ["e", "key_function"]) EHeapElems = declare_case(Exp, "EHeapElems", ["e"]) # all elements -EHeapPeek = declare_case(Exp, "EHeapPeek", ["e", "heap_length"]) # look at min -EHeapPeek2 = declare_case(Exp, "EHeapPeek2", ["e", "heap_length"]) # look at 2nd min +EHeapPeek = declare_case(Exp, "EHeapPeek", ["e"]) # look at min +EHeapPeek2 = declare_case(Exp, "EHeapPeek2", ["e"]) # look at 2nd min def to_heap(e : Exp) -> Exp: """Construct a heap that would be useful for evaluating `e`. @@ -90,10 +90,9 @@ def enumerate(self, context, size, pool, enumerate_subexps, enumerate_lambdas): t = e.type if isinstance(t, TMinHeap) or isinstance(t, TMaxHeap): elem_type = t.elem_type - n_elems = EStateVar(ELen(EHeapElems(e).with_type(TBag(elem_type)))).with_type(INT) # yielding EHeapElems would be redundant - yield EHeapPeek (EStateVar(e).with_type(e.type), n_elems).with_type(elem_type) - yield EHeapPeek2(EStateVar(e).with_type(e.type), n_elems).with_type(elem_type) + yield EHeapPeek (EStateVar(e).with_type(e.type)).with_type(elem_type) + yield EHeapPeek2(EStateVar(e).with_type(e.type)).with_type(elem_type) def default_value(self, t : Type, default_value) -> Exp: """Construct a default value of the given type. @@ -108,10 +107,6 @@ def default_value(self, t : Type, default_value) -> Exp: def check_wf(self, e : Exp, is_valid, state_vars : {EVar}, args : {EVar}, pool = RUNTIME_POOL, assumptions : Exp = ETRUE): """Return None or a string indicating a well-formedness error.""" - if (isinstance(e, EHeapPeek) or isinstance(e, EHeapPeek2)): - heap = e.e - if not is_valid(EEq(e.heap_length, ELen(EHeapElems(heap).with_type(TBag(heap.type.elem_type))))): - return "invalid `n` parameter" return None def possibly_useful(self, @@ -142,14 +137,10 @@ def typecheck(self, e : Exp, typecheck, report_err): e.type = TMinHeap(e.e.type.elem_type, e.key_function.body.type) elif isinstance(e, EHeapPeek) or isinstance(e, EHeapPeek2): typecheck(e.e) - typecheck(e.heap_length) ok = True if not (isinstance(e.e.type, TMinHeap) or isinstance(e.e.type, TMaxHeap)): report_err(e, "cannot peek a non-heap") ok = False - if e.heap_length.type != INT: - report_err(e, "length param is not an int") - ok = False if ok: e.type = e.e.type.elem_type elif isinstance(e, EHeapElems): @@ -269,7 +260,7 @@ def mutate_in_place(self, lval, e, op, assumptions, invariants, make_subgoal): SForEach(v, modified, SCall(lval, "update", (v, make_subgoal(new_v_key, a=[EIn(v, mod_spec)]))))]) def rep_type(self, t : Type) -> Type: - return TArray(t.elem_type) + return TTuple((INT, TArray(t.elem_type))) def codegen(self, e : Exp, concretization_functions : { str : Exp }, out : EVar) -> Stm: """Return statements that write the result of `e` to `out`. @@ -279,10 +270,10 @@ def codegen(self, e : Exp, concretization_functions : { str : Exp }, out : EVar) """ if isinstance(e, EMakeMinHeap) or isinstance(e, EMakeMaxHeap): out_raw = EVar(out.id).with_type(self.rep_type(e.type)) - l = fresh_var(INT, "alloc_len") + elem_type = e.type.elem_type return seq([ - SDecl(l, ELen(e.e)), - SArrayAlloc(out_raw, l), + SAssign(out_raw, ETuple([ELen(e.e), EArrayList().with_type(TArray(elem_type))]).with_type(self.rep_type(e.type))), + SArrayAlloc(ETupleGet(out_raw, 1).with_type(TArray(elem_type)), ELen(e.e)), SCall(out, "add_all", (ZERO, e.e))]) elif isinstance(e, EHeapElems): elem_type = e.type.elem_type @@ -292,8 +283,8 @@ def codegen(self, e : Exp, concretization_functions : { str : Exp }, out : EVar) i = fresh_var(INT, "i") # the array index return seq([ SDecl(i, ZERO), - SWhile(ELt(i, EArrayLen(e.e).with_type(INT)), seq([ - SCall(out, "add", (EArrayGet(e.e, i).with_type(elem_type),)), + SWhile(ELt(i, ETupleGet(e.e, 0).with_type(INT)), seq([ + SCall(out, "add", (EArrayGet(ETupleGet(e.e, 1), i).with_type(elem_type),)), SAssign(i, EBinOp(i, "+", ONE).with_type(INT))]))]) elif isinstance(e, EHeapPeek): raise NotImplementedError() @@ -301,11 +292,12 @@ def codegen(self, e : Exp, concretization_functions : { str : Exp }, out : EVar) from cozy.evaluation import construct_value best = EArgMin if isinstance(e.e.type, TMinHeap) else EArgMax f = heap_func(e.e, concretization_functions) - return SSwitch(e.heap_length, ( + return SSwitch(ETupleGet(e.e, 0), ( (ZERO, SAssign(out, construct_value(e.type))), (ONE, SAssign(out, construct_value(e.type))), - (TWO, SAssign(out, EArrayGet(e.e, ONE).with_type(e.type)))), - SAssign(out, best(EBinOp(ESingleton(EArrayGet(e.e, ONE).with_type(e.type)).with_type(TBag(out.type)), "+", ESingleton(EArrayGet(e.e, TWO).with_type(e.type)).with_type(TBag(out.type))).with_type(TBag(out.type)), f).with_type(out.type))) + (TWO, SAssign(out, EArrayGet(ETupleGet(e.e, 1), ONE).with_type(e.type)))), + SAssign(out, best(EBinOp(ESingleton(EArrayGet(ETupleGet(e.e, 1), ONE).with_type(e.type)).with_type(TBag(out.type)), "+", + ESingleton(EArrayGet(ETupleGet(e.e, 1), TWO).with_type(e.type)).with_type(TBag(out.type))).with_type(TBag(out.type)), f).with_type(out.type))) else: raise NotImplementedError(e) @@ -321,21 +313,24 @@ def implement_stmt(self, s : Stm, concretization_functions : { str : Exp }) -> S if isinstance(s, SCall): elem_type = s.target.type.elem_type target_raw = EVar(s.target.id).with_type(self.rep_type(s.target.type)) + target_len = ETupleGet(target_raw, 0).with_type(INT) + target_array = ETupleGet(target_raw, 1).with_type(TArray(elem_type)) if s.func == "add_all": size = fresh_var(INT, "heap_size") i = fresh_var(INT, "i") x = fresh_var(elem_type, "x") return seq([ SDecl(size, s.args[0]), - SEnsureCapacity(target_raw, EBinOp(size, "+", ELen(s.args[1])).with_type(INT)), + SEnsureCapacity(target_array, EBinOp(size, "+", ELen(s.args[1])).with_type(INT)), SForEach(x, s.args[1], seq([ - SAssign(EArrayGet(target_raw, size).with_type(elem_type), x), + SAssign(target_len, EBinOp(target_len, "+", ONE).with_type(INT)), + SAssign(EArrayGet(target_array, size).with_type(elem_type), x), SDecl(i, size), SWhile(EAll([ EBinOp(i, ">", ZERO).with_type(BOOL), - ENot(EBinOp(f.apply_to(EArrayGet(target_raw, _parent(i)).with_type(elem_type)), comparison_op, f.apply_to(EArrayGet(target_raw, i).with_type(elem_type))).with_type(BOOL))]), + ENot(EBinOp(f.apply_to(EArrayGet(target_array, _parent(i)).with_type(elem_type)), comparison_op, f.apply_to(EArrayGet(target_array, i).with_type(elem_type))).with_type(BOOL))]), seq([ - SSwap(EArrayGet(target_raw, _parent(i)).with_type(elem_type), EArrayGet(target_raw, i).with_type(elem_type)), + SSwap(EArrayGet(target_array, _parent(i)).with_type(elem_type), EArrayGet(target_array, i).with_type(elem_type)), SAssign(i, _parent(i))])), SAssign(size, EBinOp(size, "+", ONE).with_type(INT))]))]) elif s.func == "remove_all": @@ -348,19 +343,20 @@ def implement_stmt(self, s : Stm, concretization_functions : { str : Exp }) -> S return seq([ SDecl(size, s.args[0]), SForEach(x, s.args[1], seq([ + SAssign(target_len, EBinOp(target_len, "-", ONE).with_type(INT)), # find the element to remove - SDecl(i, EArrayIndexOf(target_raw, x).with_type(INT)), + SDecl(i, EArrayIndexOf(target_array, x).with_type(INT)), # swap with last element in heap - SSwap(EArrayGet(target_raw, i).with_type(elem_type), EArrayGet(target_raw, size_minus_one).with_type(elem_type)), + SSwap(EArrayGet(target_array, i).with_type(elem_type), EArrayGet(target_array, size_minus_one).with_type(elem_type)), # bubble down SEscapableBlock(label, SWhile(_has_left_child(i, size_minus_one), seq([ SDecl(child_index, _left_child(i)), - SIf(EAll([_has_right_child(i, size_minus_one), ENot(EBinOp(f.apply_to(EArrayGet(target_raw, _left_child(i)).with_type(elem_type)), comparison_op, f.apply_to(EArrayGet(target_raw, _right_child(i)).with_type(elem_type))))]), + SIf(EAll([_has_right_child(i, size_minus_one), ENot(EBinOp(f.apply_to(EArrayGet(target_array, _left_child(i)).with_type(elem_type)), comparison_op, f.apply_to(EArrayGet(target_array, _right_child(i)).with_type(elem_type))))]), SAssign(child_index, _right_child(i)), SNoOp()), - SIf(ENot(EBinOp(f.apply_to(EArrayGet(target_raw, i).with_type(elem_type)), comparison_op, f.apply_to(EArrayGet(target_raw, child_index).with_type(elem_type)))), + SIf(ENot(EBinOp(f.apply_to(EArrayGet(target_array, i).with_type(elem_type)), comparison_op, f.apply_to(EArrayGet(target_array, child_index).with_type(elem_type)))), seq([ - SSwap(EArrayGet(target_raw, i).with_type(elem_type), EArrayGet(target_raw, child_index).with_type(elem_type)), + SSwap(EArrayGet(target_array, i).with_type(elem_type), EArrayGet(target_array, child_index).with_type(elem_type)), SAssign(i, child_index)]), SEscapeBlock(label))]))), # dec. size diff --git a/cozy/synthesis/acceleration.py b/cozy/synthesis/acceleration.py index 4e59c545..f1856f3e 100644 --- a/cozy/synthesis/acceleration.py +++ b/cozy/synthesis/acceleration.py @@ -358,7 +358,7 @@ def optimized_best(xs, keyfunc, op, args): h = make_heap(bag.e, keyfunc).with_type(heap_type(elem_type, key_type)) for prev_min in optimized_best(bag.e, keyfunc, op, args=args): prev_min = EStateVar(prev_min).with_type(elem_type) - heap_peek = EHeapPeek2(EStateVar(h).with_type(h.type), EStateVar(ELen(bag.e)).with_type(INT)).with_type(elem_type) + heap_peek = EHeapPeek2(EStateVar(h).with_type(h.type)).with_type(elem_type) conds = [optimized_in(x, bag), optimized_eq(x, prev_min)] if isinstance(x, EUnaryOp) and x.op == UOp.The: conds = [optimized_exists(x.e)] + conds diff --git a/cozy/typecheck.py b/cozy/typecheck.py index 88ef9966..cc264925 100644 --- a/cozy/typecheck.py +++ b/cozy/typecheck.py @@ -13,6 +13,7 @@ from cozy.syntax import BOOL, INT, LONG, FLOAT, STRING from cozy.structures import extension_handler +from cozy.structures.arrays import TArray def typecheck( ast, @@ -100,7 +101,7 @@ def equality_implies_deep_equality(t : syntax.Type): return equality_implies_deep_equality(t.elem_type) return False -COLLECTION_TYPES = (syntax.TBag, syntax.TSet, syntax.TList) +COLLECTION_TYPES = (syntax.TBag, syntax.TSet, syntax.TList, TArray) def is_collection(t): return any(isinstance(t, ct) for ct in COLLECTION_TYPES) diff --git a/tests/codegen.py b/tests/codegen.py index 3b99c72f..a7f9d80c 100644 --- a/tests/codegen.py +++ b/tests/codegen.py @@ -40,10 +40,22 @@ def check(self, impl, state_map, share_info, codegen): assert res.returncode == 0 def test_regression01(self): - 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(EVar('_var164049'), ECall('_query763', (EVar('n').with_type(TInt()),)).with_type(TInt())), SDecl(EVar('_var164050'), ECall('_query2688', (EVar('n').with_type(TInt()),)).with_type(TBag(TInt())))), SSeq(SDecl(EVar('_var164051'), ECall('_query17927', ()).with_type(TInt())), SDecl(EVar('_var164052'), EBinOp(ECall('_query17927', ()).with_type(TInt()), '-', ECall('_query109248', (EVar('n').with_type(TInt()),)).with_type(TInt())).with_type(TInt())))), SSeq(SSeq(SDecl(EVar('_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(EVar('_var164054'), ECall('_query17927', ()).with_type(TInt())), SDecl(EVar('_var164055'), EBinOp(ECall('_query17927', ()).with_type(TInt()), '-', ECall('_query121063', ()).with_type(TInt())).with_type(TInt()))), SSeq(SDecl(EVar('_var164056'), ECall('_query6243', ()).with_type(TBag(TInt()))), SDecl(EVar('_var164057'), ECall('_query6243', ()).with_type(TBag(TInt()))))), SSeq(SSeq(SDecl(EVar('_var164058'), ECall('_query866', ()).with_type(TInt())), SDecl(EVar('_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())))))))), '')], '', '', '') + impl = Spec('MaxBag', [], [], [('_var656', TInt()), ('_var753', TMap(TInt(), TBool())), ('_var1653', TBool()), ('_var2642', TMaxHeap(TInt(), TInt())), ('_var4385', TInt())], (), (Query('get_max', 'pubilc', [], (), EVar('_var656').with_type(TInt()), ''), Op('add', [('x', TInt())], [], SSeq(SSeq(SDecl(EVar('_var32322').with_type(TInt()), ECond(EVar('_var1653').with_type(TBool()), EArgMax(EBinOp(ESingleton(EVar('_var656').with_type(TInt())).with_type(TBag(TInt())), '+', ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var662').with_type(TInt()), EVar('_var662').with_type(TInt()))).with_type(TInt()), EVar('x').with_type(TInt())).with_type(TInt())), SSeq(SDecl(EVar('_var32323').with_type(TInt()), EBinOp(EVar('_var4385').with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt())), SAssign(EVar('_var656').with_type(TInt()), EVar('_var32322').with_type(TInt())))), SSeq(SSeq(SAssign(EVar('_var1653').with_type(TBool()), EBool(True).with_type(TBool())), SSeq(SCall(EVar('_var2642').with_type(TMaxHeap(TInt(), TInt())), 'remove_all', (EVar('_var4385').with_type(TInt()), EEmptyList().with_type(TBag(TInt())))), SSeq(SCall(EVar('_var2642').with_type(TMaxHeap(TInt(), TInt())), 'add_all', (EVar('_var4385').with_type(TInt()), ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt())))), SForEach(EVar('_var3970').with_type(TInt()), EEmptyList().with_type(TBag(TInt())), SCall(EVar('_var2642').with_type(TMaxHeap(TInt(), TInt())), 'update', (EVar('_var3970').with_type(TInt()), EVar('_var3970').with_type(TInt()))))))), SSeq(SAssign(EVar('_var4385').with_type(TInt()), EVar('_var32323').with_type(TInt())), SSeq(SForEach(EVar('_var1135').with_type(TInt()), EEmptyList().with_type(TBag(TInt())), SMapDel(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('_var1135').with_type(TInt()))), SForEach(EVar('_var1135').with_type(TInt()), ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt())), SMapUpdate(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('_var1135').with_type(TInt()), EVar('_var1136').with_type(TBool()), SAssign(EVar('_var1136').with_type(TBool()), EBool(True).with_type(TBool())))))))), ''), Op('remove', [('x', TInt())], [], SSeq(SSeq(SSeq(SDecl(EVar('_var32324').with_type(TInt()), ECond(EBinOp(EVar('x').with_type(TInt()), '==', EVar('_var656').with_type(TInt())).with_type(TBool()), EHeapPeek2(EVar('_var2642').with_type(TMaxHeap(TInt(), TInt()))).with_type(TInt()), EVar('_var656').with_type(TInt())).with_type(TInt())), SDecl(EVar('_var32325').with_type(TInt()), EBinOp(EVar('_var4385').with_type(TInt()), '-', EUnaryOp('len', ECond(EHasKey(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('x').with_type(TInt())).with_type(TBool()), ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()))), SSeq(SDecl(EVar('_var32326').with_type(TBag(TInt())), ECond(EHasKey(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('x').with_type(TInt())).with_type(TBool()), ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))), SAssign(EVar('_var656').with_type(TInt()), EVar('_var32324').with_type(TInt())))), SSeq(SSeq(SAssign(EVar('_var1653').with_type(TBool()), EBinOp(EBinOp(EVar('_var4385').with_type(TInt()), '-', ECond(EHasKey(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('x').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())), SSeq(SCall(EVar('_var2642').with_type(TMaxHeap(TInt(), TInt())), 'remove_all', (EVar('_var4385').with_type(TInt()), ECond(EHasKey(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('x').with_type(TInt())).with_type(TBool()), ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())))), SSeq(SCall(EVar('_var2642').with_type(TMaxHeap(TInt(), TInt())), 'add_all', (EBinOp(EVar('_var4385').with_type(TInt()), '-', EUnaryOp('len', ECond(EHasKey(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('x').with_type(TInt())).with_type(TBool()), ESingleton(EVar('x').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), EEmptyList().with_type(TBag(TInt())))), SForEach(EVar('_var6136').with_type(TInt()), EEmptyList().with_type(TBag(TInt())), SCall(EVar('_var2642').with_type(TMaxHeap(TInt(), TInt())), 'update', (EVar('_var6136').with_type(TInt()), EVar('_var6136').with_type(TInt()))))))), SSeq(SAssign(EVar('_var4385').with_type(TInt()), EVar('_var32325').with_type(TInt())), SSeq(SForEach(EVar('_var2481').with_type(TInt()), EVar('_var32326').with_type(TBag(TInt())), SMapDel(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('_var2481').with_type(TInt()))), SForEach(EVar('_var2481').with_type(TInt()), EEmptyList().with_type(TBag(TInt())), SMapUpdate(EVar('_var753').with_type(TMap(TInt(), TBool())), EVar('_var2481').with_type(TInt()), EVar('_var2482').with_type(TBool()), SNoOp())))))), '')), '', '', '') print(pprint(impl)) for codegen in (CxxPrinter, JavaPrinter): - 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()))]) + state_map = OrderedDict([('_var656', EArgMax(EVar('l').with_type(TBag(TInt())), + ELambda(EVar('x').with_type(TInt()), + EVar('x').with_type(TInt()))).with_type(TInt())), ( + '_var753', EMakeMap2(EVar('l').with_type(TBag(TInt())), + ELambda(EVar('_var690').with_type(TInt()), + EBool(True).with_type(TBool()))).with_type( + TMap(TInt(), TBool()))), + ('_var1653', EUnaryOp('exists', EVar('l').with_type(TBag(TInt()))).with_type(TBool())), + ('_var2642', EMakeMaxHeap(EVar('l').with_type(TBag(TInt())), + ELambda(EVar('_var758').with_type(TInt()), + EVar('_var758').with_type(TInt()))).with_type( + TMaxHeap(TInt(), TInt()))), + ('_var4385', EUnaryOp('len', EVar('l').with_type(TBag(TInt()))).with_type(TInt()))]) share_info = defaultdict(list, {}) self.check(impl, state_map, share_info, lambda out: codegen(out=out)) diff --git a/tests/solver.py b/tests/solver.py index 20b61f80..05df5fcc 100644 --- a/tests/solver.py +++ b/tests/solver.py @@ -496,7 +496,7 @@ def test_heap_2ndmin(self): f = ELambda(x, x) for mkh in (EMakeMinHeap, EMakeMaxHeap): h = mkh(xs, f) - e = ENot(EEq(EHeapPeek(h, ELen(xs)), EHeapPeek2(h, ELen(xs)))) + e = ENot(EEq(EHeapPeek(h), EHeapPeek2(h))) assert retypecheck(e) assert satisfiable(e, validate_model=True) @@ -506,7 +506,7 @@ def test_to_heap(self): x = EVar("x").with_type(xs.type.elem_type) e = f(xs, ELambda(x, EUnaryOp("-", x))) assert retypecheck(e) - assert valid(EEq(e, EHeapPeek(to_heap(e), ELen(e)).with_type(INT))) + assert valid(EEq(e, EHeapPeek(to_heap(e)).with_type(INT))) def test_regression29(self): satisfy(EUnaryOp('not', EBinOp(EBool(True).with_type(TBool()), '=>', EBinOp(EArgMax(EBinOp(ESingleton(EBinOp(EUnaryOp('sum', EMap(ECond(EBinOp(EMapGet(EMakeMap2(EMap(EVar('xs').with_type(TList(TFloat())), ELambda(EVar('x').with_type(TFloat()), EBinOp(ECall('log', (EBinOp(ENum(1.0).with_type(TFloat()), '+', EVar('x').with_type(TFloat())).with_type(TFloat()),)).with_type(TFloat()), '+', ECall('log', (ENum(1.5).with_type(TFloat()),)).with_type(TFloat())).with_type(TFloat()))).with_type(TList(TFloat())), ELambda(EVar('_var77592').with_type(TFloat()), EUnaryOp('len', EFilter(EMap(EVar('xs').with_type(TList(TFloat())), ELambda(EVar('x').with_type(TFloat()), EBinOp(ECall('log', (EBinOp(ENum(1.0).with_type(TFloat()), '+', EVar('x').with_type(TFloat())).with_type(TFloat()),)).with_type(TFloat()), '+', ECall('log', (ENum(1.5).with_type(TFloat()),)).with_type(TFloat())).with_type(TFloat()))).with_type(TList(TFloat())), ELambda(EVar('_var77593').with_type(TFloat()), EBinOp(EVar('_var77592').with_type(TFloat()), '==', EVar('_var77593').with_type(TFloat())).with_type(TBool()))).with_type(TList(TFloat()))).with_type(TInt()))).with_type(TMap(TFloat(), TInt())), ENum(1.0).with_type(TFloat())).with_type(TInt()), '==', ENum(1).with_type(TInt())).with_type(TBool()), EEmptyList().with_type(TList(TFloat())), ESingleton(ENum(1.0).with_type(TFloat())).with_type(TList(TFloat()))).with_type(TList(TFloat())), ELambda(EVar('_var2195290').with_type(TFloat()), ENum(4).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(4).with_type(TInt())).with_type(TInt())).with_type(TBag(TInt())), '+', ESingleton(EBinOp(EUnaryOp('sum', EMap(ECond(EBinOp(EMapGet(EMakeMap2(EMap(EVar('xs').with_type(TList(TFloat())), ELambda(EVar('x').with_type(TFloat()), EBinOp(ECall('log', (EBinOp(ENum(1.0).with_type(TFloat()), '+', EVar('x').with_type(TFloat())).with_type(TFloat()),)).with_type(TFloat()), '+', ECall('log', (ENum(1.5).with_type(TFloat()),)).with_type(TFloat())).with_type(TFloat()))).with_type(TList(TFloat())), ELambda(EVar('_var77592').with_type(TFloat()), EUnaryOp('len', EFilter(EMap(EVar('xs').with_type(TList(TFloat())), ELambda(EVar('x').with_type(TFloat()), EBinOp(ECall('log', (EBinOp(ENum(1.0).with_type(TFloat()), '+', EVar('x').with_type(TFloat())).with_type(TFloat()),)).with_type(TFloat()), '+', ECall('log', (ENum(1.5).with_type(TFloat()),)).with_type(TFloat())).with_type(TFloat()))).with_type(TList(TFloat())), ELambda(EVar('_var77593').with_type(TFloat()), EBinOp(EVar('_var77592').with_type(TFloat()), '==', EVar('_var77593').with_type(TFloat())).with_type(TBool()))).with_type(TList(TFloat()))).with_type(TInt()))).with_type(TMap(TFloat(), TInt())), ENum(1.5).with_type(TFloat())).with_type(TInt()), '==', ENum(1).with_type(TInt())).with_type(TBool()), EEmptyList().with_type(TList(TFloat())), ESingleton(ENum(1.5).with_type(TFloat())).with_type(TList(TFloat()))).with_type(TList(TFloat())), ELambda(EVar('_var2195292').with_type(TFloat()), ENum(4).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(4).with_type(TInt())).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()), '>=', EBinOp(EUnaryOp('sum', EMap(ECond(EBinOp(EMapGet(EMakeMap2(EVar('xs').with_type(TList(TFloat())), ELambda(EVar('_var66768').with_type(TFloat()), EUnaryOp('len', EFilter(EVar('xs').with_type(TList(TFloat())), ELambda(EVar('_var66769').with_type(TFloat()), EBinOp(EVar('_var66768').with_type(TFloat()), '==', EVar('_var66769').with_type(TFloat())).with_type(TBool()))).with_type(TList(TFloat()))).with_type(TInt()))).with_type(TMap(TFloat(), TInt())), ENum(1.5).with_type(TFloat())).with_type(TInt()), '==', ENum(1).with_type(TInt())).with_type(TBool()), EEmptyList().with_type(TList(TFloat())), ESingleton(ENum(1.5).with_type(TFloat())).with_type(TList(TFloat()))).with_type(TList(TFloat())), ELambda(EVar('_var2195293').with_type(TFloat()), ENum(4).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', ENum(4).with_type(TInt())).with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool()), vars=OrderedSet([EVar('isDropped').with_type(TBool()), EVar('dropped').with_type(TInt()), EVar('xs').with_type(TList(TFloat())), EVar('_var155564').with_type(TFloat()), EVar('_var158099').with_type(TFloat()), EVar('_var159048').with_type(TFloat()), EVar('_var160499').with_type(TFloat()), EVar('x').with_type(TFloat())]), collection_depth=4, validate_model=True) diff --git a/tests/typecheck.py b/tests/typecheck.py index 0830182b..fc36cf22 100644 --- a/tests/typecheck.py +++ b/tests/typecheck.py @@ -54,7 +54,7 @@ def test_lambda_arg_inference(self): assert retypecheck(EMakeMap2(s, ELambda(x, x))) def test_heaps(self): - e = ECond(EBinOp(EBinOp(EMapGet(EStateVar(EMakeMap2(EVar('xs'), ELambda(EVar('_var39381'), EUnaryOp('len', EFilter(EVar('xs'), ELambda(EVar('_var39382'), EBinOp(EVar('_var39381'), '==', EVar('_var39382')))))))), ENum(0).with_type(INT)), '==', ENum(1).with_type(INT)), 'and', EBinOp(ENum(0).with_type(INT), '==', EStateVar(EArgMin(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501')))))), EHeapPeek2(EStateVar(EMakeMinHeap(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501')))), EStateVar(EUnaryOp('len', EVar('xs')))), EStateVar(EArgMin(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501'))))) + e = ECond(EBinOp(EBinOp(EMapGet(EStateVar(EMakeMap2(EVar('xs'), ELambda(EVar('_var39381'), EUnaryOp('len', EFilter(EVar('xs'), ELambda(EVar('_var39382'), EBinOp(EVar('_var39381'), '==', EVar('_var39382')))))))), ENum(0).with_type(INT)), '==', ENum(1).with_type(INT)), 'and', EBinOp(ENum(0).with_type(INT), '==', EStateVar(EArgMin(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501')))))), EHeapPeek2(EStateVar(EMakeMinHeap(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501'))))), EStateVar(EArgMin(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501'))))) assert retypecheck(e, env={ "xs": INT_BAG, "_var21501": INT}) diff --git a/tests/wf.py b/tests/wf.py index 1dc19777..d618ca8f 100644 --- a/tests/wf.py +++ b/tests/wf.py @@ -12,7 +12,7 @@ class TestWf(unittest.TestCase): def test_heap_wf(self): - e = EHeapPeek2(EStateVar(EMakeMinHeap(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501')))), EStateVar(EUnaryOp('len', EVar('xs')))) + e = EHeapPeek2(EStateVar(EMakeMinHeap(EVar('xs'), ELambda(EVar('_var21501'), EVar('_var21501'))))) assert retypecheck(e, env={ "xs": INT_BAG, "_var21501": INT})