search

CozySynthesizer / cozy

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

NotImplementedError raised on maxbag.ds #95

Closed anhnamtran closed 5 years ago

anhnamtran commented 5 years ago

Currently maxbag.ds raises a NotImplementedError on line 120 of structures/treemultiset.py.

The error is not reproducible on Ubuntu 16.08LTS.

System that the error appeared on: UW CSE Attu (6)

Steps to reproduce:

cd /tmp
git clone git@github.com:CozySynthesizer/cozy
cd cozy && virtualenv -p python3.6 venv
source venv/bin/activate
pip install .
cozy example/maxbag.ds -t 300

This should run for a while then produce multiple failed jobs. The stack trace should show the NotImplementedError.

izgzhen commented 5 years ago

You can try to run longer/shorted time in your Ubuntu

izgzhen commented 5 years ago

This runs on my MacBook fine, and in the end Number of improvements done: 60

izgzhen commented 5 years ago 
Traceback (most recent call last):
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/jobs.py", line 29, in _run
    self.run()
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/synthesis/high_level_interface.py", line 89, in run
    improve_count=self.improve_count)):
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/synthesis/core.py", line 223, in improve
    blacklist=blacklist):
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/synthesis/core.py", line 382, in search_for_improvements
    for info in enum.enumerate_with_info(size=size, context=ctx, pool=pool):
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/synthesis/enumeration.py", line 623, in enumerate_with_info
    yield from self._enumerate_with_info(context, size, pool)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/synthesis/enumeration.py", line 682, in _enumerate_with_info
    to_keep = retention_policy(e, context, prev_exp, context, pool, cost_model)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/synthesis/enumeration.py", line 239, in retention_policy
    ordering = cost_model.compare(new_exp, old_exp, context, pool)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/cost_model.py", line 197, in compare
    lambda: order_objects(e1.size(), e2.size()))
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/cost_model.py", line 67, in prioritized_order
    o = f()
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/cost_model.py", line 196, in <lambda>
    lambda: self._compare(storage_size(e1, self.freebies), storage_size(e2, self.freebies), context),
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/cost_model.py", line 155, in _compare
    e1v = eval(e1, {})
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/evaluation.py", line 30, in eval
    return eval_bulk(e, (env,), *args, **kwargs)[0]
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/evaluation.py", line 70, in eval_bulk
    _compile(e, vmap, ops)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/evaluation.py", line 540, in _compile
    _compile(e.e1, env, out)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/evaluation.py", line 506, in _compile
    _compile(e.e, env, out)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/evaluation.py", line 626, in _compile
    _compile(e.e, env, out)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/evaluation.py", line 741, in _compile
    _compile(h.encode(e), env, out)
  File "/homes/iws/zgzhen/cozy/venv/lib/python3.6/site-packages/cozy/structures/treemultiset.py", line 120, in encode
    raise NotImplementedError(e)
NotImplementedError: ETreeMultisetElems(ELet(EBool(True).with_type(TBool()), ELambda(EVar('_var1186096').with_type(TBool()), EMakeMaxTreeMultiset(EEmptyList().with_type(TBag(TInt()))).with_type(TMaxTreeMultiset(TInt())))).with_type(TMaxTreeMultiset(TInt()))).with_type(TList(TInt()))
failed job: ImproveQueryJob[get_max]

get_max.log:

STARTING IMPROVEMENT JOB get_max

  query get_max():
    assume (exists l);
    max EStateVar(l)

call to improve:
improve(
        target=EArgMax(EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt()),
        context=RootCtx(state_vars=OrderedSet([EVar('l').with_type(TBag(TInt()))]), args=OrderedSet(), funcs=OrderedDict()),
        assumptions=EBinOp(EUnaryOp('unique', EVar('l').with_type(TBag(TInt()))).with_type(TBool()), 'and', EUnaryOp('exists', EVar('l').with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()),
        stop_callback=<function ImproveQueryJob.run.<locals>.<lambda> at 0x7f5dcddc98c8>,
        hints=[EStateVar(EVar('l').with_type(TBag(TInt()))).with_type(TBag(TInt()))],
        examples=(),
        cost_model=CostModel(assumptions=EBinOp(EUnaryOp('unique', EVar('l').with_type(TBag(TInt()))).with_type(TBool()), 'and', EUnaryOp('exists', EVar('l').with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool()), examples=(), funcs=OrderedDict(), freebies=[], ops=[Op('add', [('x', TInt())], [EUnaryOp('not', EBinOp(EVar('x').with_type(TInt()), 'in', EVar('l').with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool())], SCall(EVar('l').with_type(TBag(TInt())), 'add', (EVar('x').with_type(TInt()),)), ''), Op('remove', [('x', TInt())], [], SCall(EVar('l').with_type(TBag(TInt())), 'remove', (EVar('x').with_type(TInt()),)), '')]),
        ops=[Op('add', [('x', TInt())], [EUnaryOp('not', EBinOp(EVar('x').with_type(TInt()), 'in', EVar('l').with_type(TBag(TInt()))).with_type(TBool())).with_type(TBool())], SCall(EVar('l').with_type(TBag(TInt())), 'add', (EVar('x').with_type(TInt()),)), ''), Op('remove', [('x', TInt())], [], SCall(EVar('l').with_type(TBag(TInt())), 'remove', (EVar('x').with_type(TInt()),)), '')])

improving: max EStateVar(l)
subject to: ((unique l) and (exists l))

4 hints
 - EStateVar(l)
 - (unique EStateVar(l))
 - (exists EStateVar(l))
 - max EStateVar(l)
starting minor iteration 0 with |cache|=0
  |cache|=0
FOUND A GUESS
 * in max EStateVar(l)
 * replacing max EStateVar(l)
 * with 0
Found candidate improvement: 0
new example: {'l': Bag((1,))}
wrong; restarting with 1 examples
starting minor iteration 0 with |cache|=0
  |cache|=0
FOUND A GUESS
 * in max EStateVar(l)
 * replacing max EStateVar(l)
 * with 1
Found candidate improvement: 1
new example: {'l': Bag((2, 1, 0, -1))}
wrong; restarting with 2 examples
starting minor iteration 0 with |cache|=0
  |cache|=0
FOUND A GUESS
 * in max EStateVar(l)
 * replacing max EStateVar(l)
 * with EStateVar(max l)
Found candidate improvement: EStateVar(max l)
The candidate is valid!
EStateVar(EArgMax(EVar('l').with_type(TBag(TInt())), ELambda(EVar('x').with_type(TInt()), EVar('x').with_type(TInt()))).with_type(TInt())).with_type(TInt())
Determining whether to yield it...
Yep, it's an improvement!
Now watching 1 targets
starting minor iteration 0 with |cache|=0
  |cache|=0
Guessing at substitutions...
starting minor iteration 1 with |cache|=22
  |cache|=86
  |cache|=105
FOUND A GUESS
 * in EStateVar(max l)
 * replacing max l
 * with (sum l)
Found candidate improvement: EStateVar((sum l))
new example: {'l': Bag((2, 1)), 'x': 0, '_var1317': False, '_var1838': False, '_var3088': 0, '_var4729': 0, '_var5510': 0, '_var5883': Bag(()), '_var6800': 0, '_var7754': Bag(()), '_var17507': 0}
wrong; restarting with 3 examples
starting minor iteration 0 with |cache|=0
  |cache|=0
Guessing at substitutions...
starting minor iteration 1 with |cache|=22
  |cache|=75
  |cache|=106
FOUND A GUESS
 * in EStateVar(max l)
 * replacing max l
 * with (the l)
Found candidate improvement: EStateVar((the l))
new example: {'l': Bag((-1, 0)), 'x': 0, '_var1317': False, '_var1838': False, '_var3088': 0, '_var4729': 0, '_var5510': 0, '_var5883': Bag(()), '_var6800': 0, '_var7754': Bag(()), '_var17507': 0, '_var27752': False, '_var28863': False, '_var31745': 0, '_var35600': 0, '_var37102': 0, '_var37874': Bag(()), '_var39456': 0, '_var41027': Bag(()), '_var51890': 0}
wrong; restarting with 4 examples
starting minor iteration 0 with |cache|=0
  |cache|=0
Guessing at substitutions...
starting minor iteration 1 with |cache|=22
  |cache|=84
  |cache|=112
  |cache|=160
adapting request: _var104909 in l, (root) ---> x in l, (root)
  |cache|=195
adapting request: _var125543 in [], (root) ---> _var102489 in [], (root)
adapting request: _var125576 in l, (root) ---> x in l, (root)
  |cache|=248
  |cache|=317
  |cache|=344
  |cache|=352
adapting request: _var180675 in [], x in l, (root) ---> _var137597 in [], x in l, (root)
adapting request: _var180728 in l, x in l, (root) ---> _var140554 in l, x in l, (root)
Guessing at substitutions...
starting minor iteration 2 with |cache|=366
  |cache|=411
adapting request: _var211435 in [true], (root) ---> _var61244 in [true], (root)
  |cache|=431
  |cache|=472
  |cache|=498
  |cache|=505
adapting request: _var274745 in [false], (root) ---> _var62307 in [false], (root)
  |cache|=542
  |cache|=589
  |cache|=596
  |cache|=596
adapting request: _var347442 in [0], (root) ---> _var64956 in [0], (root)
  |cache|=632
  |cache|=680
  |cache|=687
  |cache|=700
adapting request: _var416739 in [1], (root) ---> _var68080 in [1], (root)
  |cache|=737
  |cache|=784
  |cache|=791
adapting request: _var468671 in [], (root) ---> _var69773 in [], (root)
adapting request: _var473590 in [[]], (root) ---> _var70664 in [[]], (root)
  |cache|=821
  |cache|=862
  |cache|=888
  |cache|=906
adapting request: _var532733 in EStateVar(l), (root) ---> _var72197 in EStateVar(l), (root)
  |cache|=980
  |cache|=1034
  |cache|=1088
  |cache|=1093
adapting request: _var615302 in [EStateVar(l)], (root) ---> _var74023 in [EStateVar(l)], (root)
  |cache|=1114
  |cache|=1136
  |cache|=1179
  |cache|=1182
  |cache|=1189
  |cache|=1201
  |cache|=1201
adapting request: _var743454 in [EStateVar(max l)], (root) ---> _var85786 in [EStateVar(max l)], (root)
  |cache|=1207
  |cache|=1263
adapting request: _var780252 in [true], (root) ---> _var61244 in [true], (root)
adapting request: _var783505 in [false], (root) ---> _var62307 in [false], (root)
  |cache|=1303
adapting request: _var787424 in [0], (root) ---> _var64956 in [0], (root)
adapting request: _var791527 in [1], (root) ---> _var68080 in [1], (root)
  |cache|=1342
  |cache|=1369
adapting request: _var821641 in [EStateVar(max l)], (root) ---> _var85786 in [EStateVar(max l)], (root)
  |cache|=1377
  |cache|=1392
  |cache|=1409
  |cache|=1417
  |cache|=1433
  |cache|=1449
  |cache|=1503
  |cache|=1563
  |cache|=1593
  |cache|=1605
  |cache|=1613
  |cache|=1621
  |cache|=1621
  |cache|=1621
  |cache|=1621
  |cache|=1621
  |cache|=1623
  |cache|=1627
  |cache|=1628
  |cache|=1651
  |cache|=1665
adapting request: _var1186096 in [true], (root) ---> _var94038 in [true], (root)
  |cache|=1703
  |cache|=1744
  |cache|=1755
adapting request: _var1246943 in [], _var94038 in [true], (root) ---> _var1205117 in [], _var94038 in [true], (root)
adapting request: _var1247050 in l, _var94038 in [true], (root) ---> _var1208545 in l, _var94038 in [true], (root)

Indeed

izgzhen commented 5 years ago

This expression is just 'ETreeMultisetElems(let _var1186096 = true in EMakeMaxTreeMultiset([]))'