Open GregoryMorse opened 4 years ago
Hi,
Thanks, that sounds good! Can you please make a pull request out of these changes? Here is a quick guide to do it:
https://docs.github.com/en/enterprise/2.15/user/articles/creating-a-pull-request
Note that espresso is not really needed, I never use it and it's not that useful anyway. Instead, if you want to do some translation of ANF to CNF, I suggest using our tool, Bosphorus:
https://github.com/meelgroup/bosphorus
So maybe all we need is the headers/RNG stuff. Can you please make a pull request out of this?
Note that I am not the maintainer, so it's only Vegard who can tell you what's needed etc :) I have a slightly updated version of this tool here:
https://github.com/msoos/sha1-sat
Perhaps that works easier for you, but it's not the original so you may want to use Vegard's version anyway! Just my 2 cents, I'm sure Vegard will have his own view on this :)
Okay I will try to put this into a PR. The Windows process code is mostly just technically interesting for Linux devs who want to know how to deal with these stdin/stdout and child process type details.
I agree though espresso is probably not the best approach anymore. I see your version already looks portable. Thanks for the input.
Thanks for this nice project. I got it working on Windows and will give relevant code snippets though conditional compilation and integration based on that would be needed to add it to the repo.
Headers and RNG stuff (taken from boost):
espresso child process communication (fork -> Windows child process equivalent using as much C library and as little WinAPI as possible):
And the termination wait:
lrand48()
change torng48()
andsrand48(rand())
changes torng48.seed(rand())
.Not so much - certainly could be integrated.
As for building espresso on Windows, a valid getopt.c and getopt.h are necessary as well as changing cvrin.c to not
FREE(PLA->filename);
since strdup in Windows apparently is using a C-library managed buffer not a malloc'ed one. A crash on exit will cause the child pipe to become unreadable unfortunately.I tested many of the command line options and found that compact-adders seems to not work at all - leads to UNSAT. However, I am parsing the output myself in a Python script and using various Python SAT solver libraries like pysat, pycosat or pycryptosat and it works with both --cnf and --opb. (I'm not sure how to test the half adders or xor options currently).