From 563f830ac8770c7a1b528548d86719989721d23e Mon Sep 17 00:00:00 2001 From: Zhen Zhang Date: Thu, 3 Oct 2019 14:40:36 -0700 Subject: [PATCH] heuristic based expression solving by random assignments --- cozy/random_assignment.py | 158 +++++++++++++++++++++++++++++++++++++ cozy/synthesis/core.py | 23 +++++- examples/.gitignore | 1 + examples/Makefile | 6 ++ examples/select.cpp | 21 +++++ tests/random_assignment.py | 94 ++++++++++++++++++++++ tests/synthesis.py | 19 ++--- 7 files changed, 311 insertions(+), 11 deletions(-) create mode 100644 cozy/random_assignment.py create mode 100644 examples/select.cpp create mode 100644 tests/random_assignment.py diff --git a/cozy/random_assignment.py b/cozy/random_assignment.py new file mode 100644 index 00000000..bcc5de31 --- /dev/null +++ b/cozy/random_assignment.py @@ -0,0 +1,158 @@ +import random +import string +from itertools import product + +from cozy.common import FrozenDict +from cozy.syntax import * +from cozy.syntax_tools import free_vars +from cozy.evaluation import eval, mkval +from cozy.target_syntax import EFlatMap, EFilter, EMap, EStateVar +from cozy.value_types import Bag + + +def random_value(t): + """ + Construct a stream of values in type t + """ + if isinstance(t, TBag): + yield Bag() + for v in random_value(t.elem_type): + yield Bag((v,)) + for v1 in random_value(t.elem_type): + for v2 in random_value(t.elem_type): + yield Bag((v1, v2)) + elif isinstance(t, TInt): + yield random.randint(0, 100) + yield 0 + elif isinstance(t, TNative): + yield (t.name, 0) + elif isinstance(t, TFloat): + yield random.randint(0, 100) / 100.0 + yield 0.0 + elif isinstance(t, TBool): + yield True + yield False + elif isinstance(t, TString): + yield ''.join(random.choice(string.ascii_letters) for _ in range(8)) + elif isinstance(t, TRecord): + iterables = [random_value(ty) for _, ty in t.fields] + for vs in product(*iterables): + yield FrozenDict({field[0]: v for v, field in zip(vs, t.fields)}) + else: + raise Exception("Unknown type for random value construction: {}".format(t)) + + +def get_pulled(e): + """ + Strip EStateVar from a pulled expression in list comprehension + """ + if isinstance(e, EStateVar): + return e.e + return e + + +def extract_listcomp(e): + """ + Extract list comprehension components from its desugared form + :param e: list comprehension expression + :return: list comprehension structure { "P": ..., "C": ..., "V": ... }. + "P" is pulled expressions, "C" is condition, "V" is returned value. + In the written form, it is { V(p0, ..., pn) | p0 <- P_0, ..., pn <- P_n, C(p0, ..., pn)}. + Notice that all V and C already have free variables p0 to pn. + If the structure doesn't follow our assumption, return None + """ + if isinstance(e, EFlatMap): + pulled = e.e + f = e.transform_function + var = f.arg + ebody = f.body + lc = extract_listcomp(ebody) + if lc is not None: + lc["P"][var] = get_pulled(pulled) + return lc + elif isinstance(e, EMap): + f = e.transform_function + ebody = f.body + lc = extract_listcomp(e.e) + if lc is not None: + lc["V"] = ebody + return lc + elif isinstance(e, EFilter): + lc = {"C": e.predicate.body, "P": {e.predicate.arg: get_pulled(e.e)}} + return lc + return None + + +def get_cond(lc): + """ + Turn list comprehension structure into a conjunctive formula that specifies each pulled collection expression + is a singleton and all individual elements in singletons satisfy the condition + """ + singletons = [EEq(ESingleton(var).with_type(TBag(var.type)), p) for var, p in lc["P"].items()] + return EAll([lc["C"]] + singletons) + + +def unsatisfiable(e): + """ + Heuristic to decide whether e is unsatisfiable quickly. + it is a partial procedure: the possible outputs are True (indicating unsatisfiability) and None (indicating unknown). + """ + # It is unsatisfiable that two structurally equivalent list comprehensions are not semantically equivalent + if isinstance(e, EUnaryOp) and e.op == "not" and isinstance(e.e, EBinOp) and e.e.op == "==": + e1 = e.e.e1 + e2 = e.e.e2 + while isinstance(e1, EStateVar): + e1 = e1.e + while isinstance(e2, EStateVar): + e2 = e2.e + if isinstance(e1, EFlatMap) and isinstance(e2, EFlatMap): + lc1 = extract_listcomp(e1) + lc2 = extract_listcomp(e2) + if lc1 is not None and lc2 is not None: + if lc1 == lc2: + return True + return False + + +def _satisfy(e, solver): + """ + Heuristic to decide whether e is satisfiable quickly. + it is a partial procedure: the possible outputs are a satisfying assignment or None (indicating unknown) + it is allowed to indicate unknown with an arbitrary exception + (in which case falling back to the symbolic solver is a reasonable choice) + """ + if isinstance(e, EUnaryOp) and e.op == "not" and isinstance(e.e, EBinOp) and e.e.op == "==": + e1 = e.e.e1 + e2 = e.e.e2 + if isinstance(e1, EFlatMap) and isinstance(e2, EFlatMap): + lc1 = extract_listcomp(e1) + lc2 = extract_listcomp(e2) + if lc1 is not None and lc2 is not None: + cond1 = get_cond(lc1) + cond2 = get_cond(lc2) + sat1 = solver.satisfy(cond1) + sat2 = solver.satisfy(cond2) + if sat1 is None and sat2 is not None: + return {k: v for k, v in sat2.items() if k not in lc2["P"]} + if sat1 is not None and sat2 is None: + return {k: v for k, v in sat1.items() if k not in lc1["P"]} + + iterables = [random_value(v.type) for v in free_vars(e)] + ids = [v.id for v in free_vars(e)] + for vs in product(*iterables): + assignments = {} + for id_, val in zip(ids, vs): + assignments[id_] = val + sat = eval(e, assignments) + if sat: + return assignments + return None + + +def satisfy(e, solver): + assignments = _satisfy(e, solver) + if assignments is not None: + for v in solver.vars: + if v.id not in assignments: + assignments[v.id] = mkval(v.type) + return assignments diff --git a/cozy/synthesis/core.py b/cozy/synthesis/core.py index 5292fdfe..7a086e91 100644 --- a/cozy/synthesis/core.py +++ b/cozy/synthesis/core.py @@ -18,6 +18,7 @@ from multiprocessing import Value +from cozy import random_assignment from cozy.syntax import ( INT, BOOL, TMap, Op, @@ -30,7 +31,7 @@ from cozy.typecheck import is_collection, is_scalar from cozy.syntax_tools import subst, pprint, free_vars, fresh_var, alpha_equivalent, strip_EStateVar, freshen_binders, wrap_naked_statevars, break_conj, inline_lets from cozy.wf import exp_wf -from cozy.common import No, OrderedSet, unique, OrderedSet, StopException +from cozy.common import No, unique, OrderedSet, StopException from cozy.solver import valid, solver_for_context, ModelCachingSolver from cozy.evaluation import construct_value from cozy.cost_model import CostModel, Order, LINEAR_TIME_UOPS @@ -96,6 +97,9 @@ description="Applies a limit to the number of improvements cozy will run" + "on the specification. (-1) means no limit.") +allow_random_assignment_heuristic = Option("allow-random-assignment-heuristic", bool, True, + description="Use a random assignment heuristic instead of solver to solve sat/unsat problem") + def never_stop(): """Takes no arguments, always returns False.""" return False @@ -242,7 +246,22 @@ def improve( # 2. check with task("verifying candidate"): - counterexample = solver.satisfy(ENot(EEq(target, new_target))) + # try heuristic based solving first + e = ENot(EEq(target, new_target)) + if allow_random_assignment_heuristic.value: + if random_assignment.unsatisfiable(e): + counterexample = None + else: + try: + counterexample = random_assignment.satisfy(e, solver) + except Exception: + counterexample = None + if counterexample is None: + event("failed assignmnents: for %s\n" % e) + counterexample = solver.satisfy(e) + event("counter-example: for %s\n" % counterexample) + else: + counterexample = solver.satisfy(e) if counterexample is not None: if counterexample in examples: diff --git a/examples/.gitignore b/examples/.gitignore index f14e9564..0969f036 100644 --- a/examples/.gitignore +++ b/examples/.gitignore @@ -3,3 +3,4 @@ *.jar *.synthesized listcomp +select diff --git a/examples/Makefile b/examples/Makefile index b4452375..179da431 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -22,8 +22,14 @@ listcomp.h: listcomp-flatmap.ds select.h: select-flatmap.ds cozy -t $(TIMEOUT) --allow-big-sets select-flatmap.ds --c++ select.h -p 8080 --verbose --save select.synthesized +select: select.cpp select.h + g++ -std=c++11 -O3 -Werror '$<' -o '$@' + listcomp: listcomp.cpp listcomp.h g++ -std=c++11 -O3 -Werror '$<' -o '$@' +run-select: select + time ./select + run-listcomp: listcomp time ./listcomp diff --git a/examples/select.cpp b/examples/select.cpp new file mode 100644 index 00000000..bb3dac61 --- /dev/null +++ b/examples/select.cpp @@ -0,0 +1,21 @@ +#include "select.h" +#include + +void query(SelectFlatmap::_Type3508 elem) { + std::cout << "Found elem(" << elem._0 << "," << + elem._1 << "," << elem._2 << "," << elem._3 << ")" << std::endl; +} + +int main() { + SelectFlatmap::R r(15, "hello"); + std::vector Rs; + Rs.push_back(r); + + SelectFlatmap::W w("world", 100); + std::vector Ws; + Ws.push_back(w); + + SelectFlatmap m(Rs, Ws, Ws, Ws); + m.q(query); + return 0; +} \ No newline at end of file diff --git a/tests/random_assignment.py b/tests/random_assignment.py new file mode 100644 index 00000000..5feb229b --- /dev/null +++ b/tests/random_assignment.py @@ -0,0 +1,94 @@ +import unittest +from fractions import Fraction + +from cozy.syntax import * +from cozy.target_syntax import * +from cozy.value_types import * +from cozy.contexts import RootCtx +from cozy.solver import ExtractedFunc, solver_for_context +from cozy.structures.treemultiset import * +from cozy.random_assignment import * + +tests = [ + (EBinOp(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt())), {'l': Bag(()), 'n': 0}), + (EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(ENum(0).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag((0, 3, 2)), 'n': 2}), + (EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), {'l': Bag(()), 'n': 0}), + (ECond(EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('n').with_type(TInt())).with_type(TBool()), ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ECond(EUnaryOp('exists', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag((3,)), 'n': 2}), + (EBinOp(EMapKeys(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), '-', EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EMapKeys(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), '-', EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(ENum(0).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag((0, 3)), 'n': 3}), + (EBinOp(EMapKeys(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), '-', EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag((2, 2)), 'n': 2}), + (EFilter(EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var484').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var484').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var484').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ECond(EBinOp(EBool(True).with_type(TBool()), 'or', EBinOp(EVar('_var484').with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), EBool(True).with_type(TBool()), EBinOp(EBool(True).with_type(TBool()), '==', EBool(False).with_type(TBool())).with_type(TBool())).with_type(TBool()), EBinOp(EUnaryOp('not', EBinOp(EBool(False).with_type(TBool()), 'or', EBinOp(EVar('_var484').with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool())).with_type(TBool()), 'or', EBinOp(EBool(False).with_type(TBool()), '==', EBool(True).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EFilter(EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(ENum(0).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var484').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var484').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var484').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ECond(EBinOp(EBool(True).with_type(TBool()), 'or', EBinOp(EVar('_var484').with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), EBool(True).with_type(TBool()), EBinOp(EBool(True).with_type(TBool()), '==', EBool(False).with_type(TBool())).with_type(TBool())).with_type(TBool()), EBinOp(EUnaryOp('not', EBinOp(EBool(False).with_type(TBool()), 'or', EBinOp(EVar('_var484').with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool())).with_type(TBool()), 'or', EBinOp(EBool(False).with_type(TBool()), '==', EBool(True).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), {'l': Bag((3, 2)), 'n': 2}), + (EFilter(EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var484').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var484').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var484').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), ECond(EBinOp(EBool(True).with_type(TBool()), 'or', EBinOp(EVar('_var484').with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), EBool(True).with_type(TBool()), EBinOp(EBool(True).with_type(TBool()), '==', EBool(False).with_type(TBool())).with_type(TBool())).with_type(TBool()), EBinOp(EUnaryOp('not', EBinOp(EBool(False).with_type(TBool()), 'or', EBinOp(EVar('_var484').with_type(TInt()), 'in', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool())).with_type(TBool()), 'or', EBinOp(EBool(False).with_type(TBool()), '==', EBool(True).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt())), {'l': Bag(()), 'n': 0}), + (EFilter(EFilter(EMapKeys(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var2266').with_type(TInt()), EBinOp(EVar('_var2266').with_type(TInt()), '==', EVar('n').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var2266').with_type(TInt()), EBinOp(EMapGet(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var2266').with_type(TInt())).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), EFilter(ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), ELambda(EVar('_var2266').with_type(TInt()), EBinOp(EMapGet(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var2266').with_type(TInt())).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), {'l': Bag(()), 'n': 0}), + (EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt()), ENum(0).with_type(TInt()), {'l': Bag((3, 3)), 'n': 3, '_var6084': 3, '_var6085': 2}), + (EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var2779').with_type(TInt())).with_type(TInt()), ENum(0).with_type(TInt()), {'l': Bag((4, 4, 5, 6)), 'n': 4, '_var2779': 4, '_var2780': 2}), + (EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt()), ENum(1).with_type(TInt()), {'l': Bag((2, 2, 2, 2)), 'n': 2, '_var6084': 2, '_var6085': 4}), + (EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var6084').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var6084').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var6084').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt())).with_type(TBool()), EBinOp(ENum(0).with_type(TInt()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(ENum(0).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var6084').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var6084').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var6084').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt())).with_type(TBool()), EBinOp(ENum(0).with_type(TInt()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), {'l': Bag((2, 3)), 'n': 2, '_var2267': 0}), + (EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var6084').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var6084').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var6084').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt())).with_type(TBool()), EBinOp(ENum(0).with_type(TInt()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt())), {'l': Bag((2, 2, 3, 3)), 'n': 2, '_var2267': 0}), + (EMapGet(ELet(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var8978').with_type(TBag(TInt())), EMakeMap2(EVar('_var8978').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EFilter(EVar('_var8978').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt()), EMapGet(ELet(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var8978').with_type(TBag(TInt())), EMakeMap2(EVar('_var8978').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EUnaryOp('len', EVar('_var8978').with_type(TBag(TInt()))).with_type(TInt()))).with_type(TMap(TInt(), TInt())))).with_type(TMap(TInt(), TInt())), EVar('_var6084').with_type(TInt())).with_type(TInt()), {'l': Bag((4, 5, 4, 4)), 'n': 4, '_var6084': 4, '_var6085': 3, '_var2267': 5}), + (EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool()), EBool(True).with_type(TBool()), {'l': Bag((3, 4, 5, 6)), 'n': 3, '_var12007': 3, '_var12008': True}), + (EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool()), EBool(False).with_type(TBool()), {'l': Bag(()), 'n': 4, '_var12007': 4, '_var12008': False}), + (EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var17313').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var17313').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var17313').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(ENum(0).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var17313').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var17313').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var17313').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), {'l': Bag((0, 2)), 'n': 2, '_var2267': 0}), + (EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var12007').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var12007').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var12007').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(ENum(0).with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var12007').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var12007').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var12007').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), {'l': Bag((0, 5)), 'n': 3, '_var2267': 0}), + (EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var17313').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var17313').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var17313').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var17313').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt())), {'l': Bag((4, 4)), 'n': 4, '_var2267': 0}), + (EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var12007').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var12007').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var12007').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), {'l': Bag((4, 4)), 'n': 4, '_var2267': 0}), + (EFilter(EFilter(EMapKeys(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var2266').with_type(TInt()), EBinOp(EVar('_var2266').with_type(TInt()), '==', EVar('n').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var2266').with_type(TInt()), EMapGet(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var2266').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), EMap(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var11251').with_type(TInt()), EBinOp(EVar('_var11251').with_type(TInt()), '!=', EVar('n').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var62637').with_type(TInt()), EVar('n').with_type(TInt()))).with_type(TBag(TInt())), {'l': Bag((3, 4, 5)), 'n': 0, '_var2267': 3}), + (ECond(EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var427').with_type(TInt()), EBool(True).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('n').with_type(TInt())).with_type(TBool()), ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ECond(EStateVar(EBinOp(ENum(0).with_type(TInt()), 'in', EVar('l').with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag((0,)), 'n': 2, '_var427': 0}), + (EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var12007').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var12007').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBinOp(EBinOp(EUnaryOp('len', EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var12007').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), EFilter(EMapKeys(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var12007').with_type(TInt()), EBinOp(EUnaryOp('not', EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'or', EUnaryOp('not', ECond(EBinOp(EVar('_var12007').with_type(TInt()), 'in', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBool()), EBool(True).with_type(TBool()), EBinOp(EBool(False).with_type(TBool()), '==', EMapGet(EMakeMap2(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2267').with_type(TInt()), EBinOp(EUnaryOp('len', EFilter(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('n').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var2268').with_type(TInt()), EBinOp(EVar('_var2267').with_type(TInt()), '==', EVar('_var2268').with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TInt()), '<=', ENum(1).with_type(TInt())).with_type(TBool()))).with_type(TMap(TInt(), TBool())), EVar('_var12007').with_type(TInt())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TInt())), {'l': Bag((3, 5, 4)), 'n': 3, '_var2267': 0, '_var71738': 0, '_var73145': 0, '_var73375': 0}), + (EBinOp(EBinOp(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), '+', ESingleton(EVar('v').with_type(TFloat())).with_type(TBag(TFloat()))).with_type(TBag(TFloat())), '-', EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat()))).with_type(TBag(TFloat())), EEmptyList().with_type(TBag(TFloat())), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag(()), 'v': Fraction(0, 1)}), + (EBinOp(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), '-', EBinOp(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), '-', ESingleton(EVar('v').with_type(TFloat())).with_type(TBag(TFloat()))).with_type(TBag(TFloat()))).with_type(TBag(TFloat())), EEmptyList().with_type(TBag(TFloat())), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag((Fraction(0, 1), Fraction(2, 1), Fraction(1, 1), Fraction(0, 1))), 'v': Fraction(0, 1)}), + (ESorted(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), EVar('asc').with_type(TBool())).with_type(TList(TFloat())), ESorted(EEmptyList().with_type(TBag(TFloat())), EVar('asc').with_type(TBool())).with_type(TList(TFloat())), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag((Fraction(0, 1), Fraction(1, 1), Fraction(0, 1), Fraction(-1, 1))), 'asc': True}), + (EListGet(ESorted(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), EVar('asc').with_type(TBool())).with_type(TList(TFloat())), EVar('i').with_type(TInt())).with_type(TFloat()), EListGet(ESorted(EEmptyList().with_type(TBag(TFloat())), EVar('asc').with_type(TBool())).with_type(TList(TFloat())), EVar('i').with_type(TInt())).with_type(TFloat()), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag((Fraction(-1, 1), Fraction(-2, 1))), 'asc': True, 'i': 1}), + (EBinOp(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), '-', EBinOp(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), '-', ESingleton(EVar('v').with_type(TFloat())).with_type(TBag(TFloat()))).with_type(TBag(TFloat()))).with_type(TBag(TFloat())), ESingleton(EVar('v').with_type(TFloat())).with_type(TBag(TFloat())), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag(()), 'v': Fraction(0, 1)}), + (ECond(EHasKey(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TFloat())), ELambda(EVar('_var409').with_type(TFloat()), EBool(True).with_type(TBool()))).with_type(TMap(TFloat(), TBool()))).with_type(TMap(TFloat(), TBool())), EVar('v').with_type(TFloat())).with_type(TBool()), ESingleton(EVar('v').with_type(TFloat())).with_type(TBag(TFloat())), EEmptyList().with_type(TBag(TFloat()))).with_type(TBag(TFloat())), ECond(EUnaryOp('exists', EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat()))).with_type(TBool()), ESingleton(EVar('v').with_type(TFloat())).with_type(TBag(TFloat())), EEmptyList().with_type(TBag(TFloat()))).with_type(TBag(TFloat())), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag((Fraction(1, 1),)), 'v': Fraction(0, 1)}), + (EBinOp(EMapKeys(EStateVar(EMakeMap2(EVar('l').with_type(TBag(TFloat())), ELambda(EVar('_var409').with_type(TFloat()), EBool(True).with_type(TBool()))).with_type(TMap(TFloat(), TBool()))).with_type(TMap(TFloat(), TBool()))).with_type(TBag(TFloat())), '-', EUnaryOp('distinct', EBinOp(EStateVar(EVar('l').with_type(TBag(TFloat()))).with_type(TBag(TFloat())), '-', ESingleton(EVar('v').with_type(TFloat())).with_type(TBag(TFloat()))).with_type(TBag(TFloat()))).with_type(TBag(TFloat()))).with_type(TBag(TFloat())), EEmptyList().with_type(TBag(TFloat())), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag((Fraction(0, 1),)), 'v': Fraction(0, 1)}), + (ECond(EVar('asc').with_type(TBool()), ETreeMultisetElems(EStateVar(EMakeMinTreeMultiset(EVar('l').with_type(TBag(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TList(TFloat())), ETreeMultisetElems(EStateVar(EMakeMaxTreeMultiset(EVar('l').with_type(TBag(TFloat()))).with_type(TMaxTreeMultiset(TFloat()))).with_type(TMaxTreeMultiset(TFloat()))).with_type(TList(TFloat()))).with_type(TList(TFloat())), ETreeMultisetElems(EStateVar(EMakeMinTreeMultiset(EVar('l').with_type(TBag(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TList(TFloat())), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag((Fraction(0, 1), Fraction(4, 1))), 'asc': False}), + (EListGet(ECond(EVar('asc').with_type(TBool()), ETreeMultisetElems(EStateVar(EMakeMinTreeMultiset(EVar('l').with_type(TBag(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TList(TFloat())), ETreeMultisetElems(EStateVar(EMakeMaxTreeMultiset(EVar('l').with_type(TBag(TFloat()))).with_type(TMaxTreeMultiset(TFloat()))).with_type(TMaxTreeMultiset(TFloat()))).with_type(TList(TFloat()))).with_type(TList(TFloat())), EVar('i').with_type(TInt())).with_type(TFloat()), EListGet(ETreeMultisetElems(EStateVar(EMakeMinTreeMultiset(EVar('l').with_type(TBag(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TMinTreeMultiset(TFloat()))).with_type(TList(TFloat())), EVar('i').with_type(TInt())).with_type(TFloat()), {'get_ith_escaped': ExtractedFunc(cases={}, default=Fraction(0, 1)), 'l': Bag((Fraction(-2, 1), Fraction(-1, 1))), 'asc': False, 'i': 0}), + (EUnaryOp('sum', EMap(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('i').with_type(TInt()), EVar('i').with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), ENum(0).with_type(TInt()), {'l': Bag((0, 1236, -1237))}), + (EUnaryOp('sum', EMap(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('i').with_type(TInt()), EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('i').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), ENum(0).with_type(TInt()), {'l': Bag((11, 0, 10, 11))}), + (EBinOp(EBinOp(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), '+', ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt())), {'l': Bag(()), 'i': 0}), + (EStateVar(EUnaryOp('sum', EVar('l').with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), EUnaryOp('-', ENum(1).with_type(TInt())).with_type(TInt()), {'l': Bag(())}), + (EBinOp(EUnaryOp('sum', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', EVar('i').with_type(TInt())).with_type(TInt()), ENum(0).with_type(TInt()), {'l': Bag((0, -2438, 2437)), 'i': 0}), + (EBinOp(EBinOp(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var372').with_type(TInt()), EBinOp(EVar('_var372').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), '+', ECond(EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var492').with_type(TInt()), EBinOp(EVar('_var492').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EBinOp(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var372').with_type(TInt()), EBinOp(EVar('_var372').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), '+', ECond(EBool(True).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var492').with_type(TInt()), EBinOp(EVar('_var492').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag(()), 'i': 0}), + (EBinOp(EUnaryOp('sum', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', EVar('i').with_type(TInt())).with_type(TInt()), EUnaryOp('sum', EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), {'l': Bag((0, 0, 0)), 'i': 1}), + (EBinOp(EUnaryOp('sum', EMap(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', EUnaryOp('sum', EMap(ECond(EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), EBinOp(EUnaryOp('sum', EMap(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', EUnaryOp('sum', EMap(ECond(EBool(True).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), {'l': Bag(()), 'i': 0}), + (EBinOp(EUnaryOp('sum', EMap(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', EUnaryOp('sum', EMap(ECond(EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), EBinOp(EUnaryOp('sum', EMap(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', EUnaryOp('sum', EMap(ECond(EBool(False).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), {'l': Bag(()), 'i': 11}), + (EBinOp(EUnaryOp('sum', EMap(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt()), '+', EUnaryOp('sum', EMap(ECond(EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), EBinOp(ENum(0).with_type(TInt()), '+', EUnaryOp('sum', EMap(ECond(EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var900').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), {'l': Bag((11, 0, 10, 10)), 'i': 0}), + (EBinOp(EBinOp(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), '+', ECond(EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EBinOp(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), '+', ECond(EBool(True).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag(()), 'i': 0}), + (EBinOp(EBinOp(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), '+', ECond(EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), EBinOp(EBinOp(EFilter(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), '+', ECond(EBool(False).with_type(TBool()), ESingleton(EVar('i').with_type(TInt())).with_type(TBag(TInt())), EEmptyList().with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), '-', EStateVar(EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('_var899').with_type(TInt()), EBinOp(EVar('_var899').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt()))).with_type(TBag(TInt()))).with_type(TBag(TInt())), {'l': Bag((-1, 0)), 'i': 11}), + (EStateVar(EUnaryOp('sum', EMap(EFilter(EVar('l').with_type(TBag(TInt())), ELambda(EVar('i').with_type(TInt()), EBinOp(EVar('i').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TInt())), ELambda(EVar('i').with_type(TInt()), ENum(1).with_type(TInt()))).with_type(TBag(TInt()))).with_type(TInt())).with_type(TInt()), EBinOp(ENum(1).with_type(TInt()), '+', ENum(1).with_type(TInt())).with_type(TInt()), {'l': Bag(())}) ] + +tests2 = [ + EUnaryOp('not', EBinOp(EFlatMap(EStateVar(EVar('Rs').with_type(TBag(TRecord((('A', TInt()), ('B', TString())))))).with_type(TBag(TRecord((('A', TInt()), ('B', TString()))))), ELambda(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), EFlatMap(EStateVar(EVar('Ss').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), EFlatMap(EStateVar(EVar('Qs').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), EMap(EFilter(EStateVar(EVar('Ws').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), EBinOp(EBinOp(EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), '==', EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString())).with_type(TBool()), 'and', EBinOp(EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), '==', ENum(15).with_type(TInt())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), ETuple((EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), EGetField(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()), EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()))).with_type(TTuple((TInt(), TInt(), TString(), TInt()))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))), '==', EFlatMap(EEmptyList().with_type(TBag(TRecord((('A', TInt()), ('B', TString()))))), ELambda(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), EFlatMap(EStateVar(EVar('Ss').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), EFlatMap(EStateVar(EVar('Qs').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), EMap(EFilter(EStateVar(EVar('Ws').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), EBinOp(EBinOp(EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), '==', EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString())).with_type(TBool()), 'and', EBinOp(EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), '==', ENum(15).with_type(TInt())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), ETuple((EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), EGetField(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()), EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()))).with_type(TTuple((TInt(), TInt(), TString(), TInt()))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt()))))).with_type(TBool())).with_type(TBool()) +] + +tests3 = [ + EUnaryOp('not', EBinOp(EFlatMap(EStateVar(EVar('Rs').with_type(TBag(TRecord((('A', TInt()), ('B', TString())))))).with_type(TBag(TRecord((('A', TInt()), ('B', TString()))))), ELambda(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), EFlatMap(EStateVar(EVar('Ss').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), EFlatMap(EStateVar(EVar('Qs').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), EMap(EFilter(EStateVar(EVar('Ws').with_type(TBag(TRecord((('B', TString()), ('C', TInt())))))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), EBinOp(EBinOp(EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), '==', EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString())).with_type(TBool()), 'and', EBinOp(EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), '==', ENum(15).with_type(TInt())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), ETuple((EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), EGetField(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()), EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()))).with_type(TTuple((TInt(), TInt(), TString(), TInt()))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))), '==', EStateVar(EFlatMap(EVar('Rs').with_type(TBag(TRecord((('A', TInt()), ('B', TString()))))), ELambda(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), EFlatMap(EVar('Ss').with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), EFlatMap(EVar('Qs').with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), EMap(EFilter(EVar('Ws').with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), EBinOp(EBinOp(EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), '==', EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString())).with_type(TBool()), 'and', EBinOp(EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), '==', ENum(15).with_type(TInt())).with_type(TBool())).with_type(TBool()))).with_type(TBag(TRecord((('B', TString()), ('C', TInt()))))), ELambda(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), ETuple((EGetField(EVar('r').with_type(TRecord((('A', TInt()), ('B', TString())))), 'A').with_type(TInt()), EGetField(EVar('s').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()), EGetField(EVar('q').with_type(TRecord((('B', TString()), ('C', TInt())))), 'B').with_type(TString()), EGetField(EVar('w').with_type(TRecord((('B', TString()), ('C', TInt())))), 'C').with_type(TInt()))).with_type(TTuple((TInt(), TInt(), TString(), TInt()))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt())))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt()))))).with_type(TBag(TTuple((TInt(), TInt(), TString(), TInt()))))).with_type(TBool())).with_type(TBool()) +] + +def init_solver(): + context = RootCtx() + return solver_for_context(context) + +class TestRandomAssignment(unittest.TestCase): + def test_satisfy_regression(self): + for target, new_target, expected in tests: + solver = init_solver() + e = ENot(EEq(target, new_target)) + actual = satisfy(e, solver) + assert eval(e, expected) + if actual is None: + print("missed solution: %s\nfor: %s\n" % (expected, pprint(e))) + elif actual.keys() != expected.keys(): + print("different solution: \n actual: %s \n expected: %s\n for: %s\n" % (expected, actual, pprint(e))) + else: + print("Found solution\n") + + def test_satisfy_true(self): + for test in tests2: + solver = init_solver() + assert satisfy(test, solver), pprint(test) + + def test_unsatisfiable_true(self): + for test in tests3: + solver = init_solver() + assert unsatisfiable(test), pprint(test) diff --git a/tests/synthesis.py b/tests/synthesis.py index 1ffcad91..86b6bc84 100644 --- a/tests/synthesis.py +++ b/tests/synthesis.py @@ -9,7 +9,7 @@ from cozy.evaluation import mkval from cozy.cost_model import CostModel from cozy.synthesis import construct_initial_implementation, improve_implementation -from cozy.synthesis.core import improve +from cozy.synthesis.core import improve, allow_random_assignment_heuristic from cozy.synthesis.enumeration import Enumerator, Fingerprint from cozy.parse import parse_spec from cozy.solver import valid, satisfy @@ -42,14 +42,15 @@ def check_discovery(spec, expected, state_vars=[], args=[], examples=[], assumpt class TestSynthesisCore(unittest.TestCase): def test_easy_synth(self): - res = None - x = EVar("x").with_type(BOOL) - xs = EVar("xs").with_type(TBag(BOOL)) - target = EFilter(EStateVar(xs), ELambda(x, x)) - assumptions = EUnaryOp(UOp.All, xs) - assert retypecheck(target) - assert retypecheck(assumptions) - assert check_discovery(target, EStateVar(EVar("xs")), args=[x], state_vars=[xs], assumptions=assumptions) + with save_property(allow_random_assignment_heuristic, "value"): + allow_random_assignment_heuristic.value = False + x = EVar("x").with_type(BOOL) + xs = EVar("xs").with_type(TBag(BOOL)) + target = EFilter(EStateVar(xs), ELambda(x, x)) + assumptions = EUnaryOp(UOp.All, xs) + assert retypecheck(target) + assert retypecheck(assumptions) + assert check_discovery(target, EStateVar(EVar("xs")), args=[x], state_vars=[xs], assumptions=assumptions) def test_bag_plus_minus(self): t = THandle("H", INT)