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.