Windows translation

[GregoryMorse]

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):

#include <algorithm>
#include <io.h>
#include <process.h>
#include <fcntl.h>
#include <Windows.h>
#include <intrin.h>
#define __builtin_popcount __popcnt

#include <boost/random/linear_congruential.hpp>
...
//#include <sys/wait.h>
//#include <unistd.h>
…
static boost::rand48 rng48;

espresso child process communication (fork -> Windows child process equivalent using as much C library and as little WinAPI as possible):

			if (_pipe(wfd, 4096, _O_BINARY | _O_NOINHERIT) == -1)
				throw std::runtime_error("pipe() failed");

			if (_pipe(rfd, 4096, _O_BINARY | _O_NOINHERIT) == -1)
				throw std::runtime_error("pipe() failed");
			int fdStdIn = _dup(wfd[0]);
			int fdStdOut = _dup(rfd[1]);
			_close(rfd[1]);
			_close(wfd[0]);
			TCHAR szCmdline[] = TEXT("espresso");
			PROCESS_INFORMATION pi{};
			STARTUPINFO si{};
			si.cb = sizeof(STARTUPINFO);
			si.hStdInput = (HANDLE)_get_osfhandle(fdStdIn);
			si.hStdOutput = (HANDLE)_get_osfhandle(fdStdOut);
			si.hStdError = si.hStdOutput;
			si.dwFlags |= STARTF_USESTDHANDLES;
			if (!CreateProcess(NULL, szCmdline, NULL, NULL, TRUE, 0, NULL, NULL, &si, &pi))
				std::runtime_error("CreateProcess failed");
			CloseHandle(pi.hThread);
			_close(fdStdIn);
			_close(fdStdOut);

And the termination wait:

			while (true) {
				DWORD status;
				status = WaitForSingleObject(pi.hProcess, INFINITE);
				if (status == WAIT_OBJECT_0) break;
				throw std::runtime_error("wait() failed");
			}
			CloseHandle(pi.hProcess);

lrand48() change to rng48() and srand48(rand()) changes to rng48.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).

[msoos]

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?

[msoos]

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 :)

[GregoryMorse]

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.