Ctrl+C doesn't work in pycryptosat

[cipherboy]

When a program uses pycryptosat, it'll fail to respond to the Ctrl+C shortcut because the native component of pycryptosat, SATSolver from CryptoMiniSat, doesn't invoke Python's signal handler.

Demonstration:

from pycryptosat import Solver
import time

class TestSolveTimeLimit:
    def get_clauses(self):
        cls = []
        with open("tests/des16.cnf", "r") as f:
            for line in f:
                line = line.strip()
                if len(line) == 0:
                    continue
                if line[0] == "p":
                    continue
                if line[0] == "c":
                    continue
                line = line.split()
                line = [int(l.strip()) for l in line]
                assert line[-1] == 0
                cls.append(line[:-1])

        return cls

    def test_time(self):
        SAT_TIME_LIMIT = 1
        clauses = self.get_clauses() #returns a few hundred short clauses
        t0 = time.time()
        solver = Solver()
        solver.add_clauses(clauses)
        print("Solving...")
        sat, sol = solver.solve()
        took_time = time.time() - t0

        print(took_time)

test_case = TestSolveTimeLimit()
test_case.test_time()

Using des16.cnf from Massacci's des2fml-0.9 archive for instance.

Expected Output:

$ time python3 script.py
^C
$ # script.py exits in a reasonable amount of time after Ctrl+C is hit.

Actual Output:

$ time python3 script.py
^C
....
$ # script.py exits only after Solver.solve(...) returns with an answer!

Note that CMS has to solve the entire instance before it'll return from pycryptosat.Solver.solve(...)!

Obligatory output:

cmake.txt make.txt

[msoos]

Thanks! That's a great find! Please use the Pull Request function of GitHub so you can submit a fix. Here is how you can submit a PR:

https://help.github.com/en/github/collaborating-with-issues-and-pull-requests/about-pull-requests

Looking forward to merging your PR! Cheers,

Mate

[GregoryMorse]

This is likely a Windows issue (not a pycryptosat issue) as I dont experience it with pycryptosat or cryptominisat in Linux. However it is also possibly fixed. Not sure if the signal SIGINT stuff would work on Windows as it currently is.

[msoos]

OK, I think I just fixed it. Please wait a bit of time for the new, 5.11.13 pycryptominisat version to be built and sent to pypi. Once it's there, can you please check if it fixes the issue? I completely removed the Ctrl+C thing from pycryptominisat, it no longer tries to hook on to Ctrl+C.

I hope I fixed it. Thanks again for reminding me :) Please close the issue in case I did fix it, or please report back in case I haven't.

Thanks again, and sorry for the delay,

Mate

[msoos]

Ooops, 5.11.14... I messed up 5.11.13.

[msoos]

@GregoryMorse Can I close this issue? Has it fixed the problem for you?

Thanks again for opening the issue!

Mate

[GregoryMorse]

The Windows build seems to have become broken so I cannot test it:

src/picosat/picosat.c(8148): fatal error C1083: Cannot open include file: 'sys/time.h': No such file or directory

[msoos]

Ah, I see. Yeah, I think it never built on Windows due to picosat not building on Windows. I think I have fixed the underlying issue, though, so I'm closing this. I'd need a Windows install and someone very dedicated to use it on Windows for me to fix the Python Windows build... Not sure that's a priority given that Windows subsystem for Linux works so incredibly well!

[GregoryMorse]

Just to note however that the Windows wheel was building fine previously which was an unexpected surprise. So it is only very recent changes that broke it.

Update: I have on Windows: pycryptosat 0.6.1 working correctly but Ctrl+C is broken in it. But I guess this version is quite old. So I suppose at least as far as subsystem for Linux and Linux are concerned this issue is fixed. And quite a bit of reworking and testing is needed as you said to make the current source portable.

[msoos]

OK, I see. Yeah, probably the inclusion of picosat likely broke it. Let me try to fix.

[msoos]

OK, I had a go at it. Honestly, I am not prepared to support Windows -- it's a wonky OS with weird behaviour that few, if any, use. Hence, I am closing. If I fixed it, I'm glad. If I didn't, it was a good try :)

[GregoryMorse]

Yup looks good. I will check the next version on Windows and perhaps potentially fix the issues if they are only small header level issues. Its not particularly important indeed.