Assertion error trying to instantiate two "SmtEnumerator"s

[rodamber]

The following program attempts to create two objects of the class SmtEnumerator:

#!/usr/bin/env python

import tyrell.spec as S
from tyrell.enumerator import SmtEnumerator
from tyrell.logger import get_logger

logger = get_logger('tyrell')
logger.setLevel('DEBUG')

spec_str = '''
enum SmallInt {
  "-1", "-2", "0", "1", "2"
}
value Int {
    is_positive: bool;
}
value Empty;

program Toy(Int, Int) -> Int;
func const: Int -> SmallInt;

func empty: Empty -> Empty;
'''

logger.info('Parsing Spec...')
spec = S.parse(spec_str)
logger.info('Parsing succeeded')

logger.info('Building synthesizer 1...')
SmtEnumerator(spec, depth=3, loc=2)

logger.info('Building synthesizer 2...')
SmtEnumerator(spec, depth=3, loc=2)

But fails with an assertion error:

(venv) bash-3.2$ python smt_bug_minimal.py
[info] Parsing Spec...
[debug] Building Tyrell spec from parse tree...
[debug] Processing type definitions...
[debug] Processing input/output definitions...
[debug] Processing function definitions...
[debug] Processing global predicates...
[info] Parsing succeeded
[info] Building synthesizer 1...
[info] Building synthesizer 2...
Traceback (most recent call last):
File "smt_bug_minimal.py", line 33, in
SmtEnumerator(spec, depth=3, loc=2)
File "/Users/rodamber/Projects/msc/code/current/tyrell/tyrell/enumerator/smt.py", line 240, in init
self.createFunctionConstraints(self.z3_solver)
File "/Users/rodamber/Projects/msc/code/current/tyrell/tyrell/enumerator/smt.py", line 94, in createFunctionConstraints
assert len(self.nodes) == len(self.variables_fun)
AssertionError

[danieltrt]

In Tyrell class variables/attributes are assigned outside of the init method. Therefore these attributes are shared among its instances.

I don't know if it's an intended feature or if it was simply a mistake due to python's diverging syntax.

Anyway, this "problem" is not exclusive to this class. A quick fix is to avoid using different enumerators in the same process.