crillab / d4

d4 Model Counter
GNU Lesser General Public License v3.0
14 stars 4 forks source link

Independent counting giving inconsistent results #9

Open haz opened 2 years ago

haz commented 2 years ago

This may not be a bug with the current repo version, but has there been any major bugs in the generated original output that have since been squashed? I have an independent parser for the traditional (ala c2d) .nnf format, and while the d4 solver is reporting the right model count, the computed model count on the parsed .nnf file is all over the place. Parser seems to consistently work with dsharp, so I suspect it may just be something wonky with the d4 output.

For reference, I'm using the d4 binary available for direct download here.

As an alternative, is there any option to run the latest and generate the old .nnf format? Or perhaps a utility that converts from the new to the old?

Thanks!