Confusing default path in `kclause_to_dimacs.py`

[6b6279]

kclause_to_dimacs.py tries to load off Kclause expressions off .kmax/kclause/x86_64/kclause. I have transformed a Kconfig file into the Kclause format using kextract --extract Kconfig | kclause > Kclause. Am I supposed to redirect kclause's output specifically to the path that kclause_to_dimacs.py looks for? Wouldn’t it be more practical for kclause_to_dimacs.py to recieve a command-line parameter that corresponds to the Kclause file to process?

[paulgazz]

Hi @6b6279. Thanks for the suggestion. This is being addressed in #229. Originally, the klocalizer tool used the path in kclause_to_dimacs.py to store the file, which is why that path was used. Right now, it is just an example script, rather than a stand-alone tool; it's not installed when using pip, for instance. Once the issues with #226 are resolved, I can add this as a tool. For now, please edit the script to take in an argument (#229 for an example of this) or just hardcode the path you'd like.

[6b6279]

Hi, thanks a lot for the patch. I initially tried using the version from your comment in #226 but there was a mismatch regarding types (probably due to pickle?). I am going to try again with the version from your pull request #229.

[paulgazz]

Hi @6b6279 I just remembered that we support dimacs output using the klocalizer tool, which uses kclause under the hood (#54). It uses solver.dimacs(). You can run this from a Linux source directory like this:

klocalizer -a x86_64 --save-dimacs dimacs

This will create a dimacs file for the x86_64 Kconfig files. I haven't extensively tested this (or seen whether it's related to #226 since it uses a different way to generate). Please let me know if this works for you.

[6b6279]

That works. I guess there is no need to use the script when klocalizer has an built-in option for it. Thanks a lot.