search

CozySynthesizer / cozy

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

clausedb example produces assertion error #100

Open anhnamtran opened 5 years ago

anhnamtran commented 5 years ago

Right now, Cozy produces an AsssertionError when run with any timeout on examples/clausedb.ds. The assertion is a warning that is "This target is already a bad idea".

To reproduce: 

git clone git@github.com:CozySynthesizer/cozy.git
cd cozy
pip3 install -r requirements.txt
python3 -m cozy examples/clausedb.ds

The output should produce numerous failed jobs and the stack trace should show the assertion error.

Calvin-L commented 5 years ago

Cozy does not currently support collections whose elements are also collections, such as the Set<Set<Bound>> type in clausedb.ds. This is not a necessary restriction, but right now it is very deep-seated in the Cozy implementation.

Background: Some of the inputs in the examples folder were "hopeful" inputs that I knew Cozy couldn't support but which I hoped it would someday. examples/clausedb.ds is one of these "hopeful" inputs.