search

sagemath / sage

Main repository of SageMath. Now open for Issues and Pull Requests.
https://www.sagemath.org
Other
1.21k stars 421 forks source link

Interface cryptominisat 5 #22818

Closed edd8e884-f507-429a-b577-5d554626c0fe closed 7 years ago

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

This ticket is a compagnon of #22817 which updates cryptominisat package to 5.0.1. Since our current cython interface does not work with cryptominisat 5, we have to rewrite the interface to use the python bindings that are now provided by cryptominisat.

The tarball is at https://github.com/msoos/cryptominisat/archive/5.0.1.tar.gz

(might have to renamed---or downloaded using a browser)

Depends on #22817

CC: @kiwifb

Component: packages: experimental

Keywords: days86, thursdaysbdx, sdl

Author: Thierry Monteil

Branch: c22de1d

Reviewer: Sébastien Labbé

Issue created by migration from https://trac.sagemath.org/ticket/22818

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Changed keywords from none to days86

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Description changed:

--- 
+++ 
@@ -1,2 +1,4 @@
 This ticket is a compagnon of #22817 which updates cryptominisat package to 5.0.1. Since our current cython interface does not work with cryptominisat 5, we have to rewrite the interface to use the python bindings that are now provided by cryptominisat.

+#22818 and #22817 depend on each other.
+
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Branch: u/tmonteil/interface_cryptominisat_5

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Commit: afffd2a

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

New commits:

67f23e7#22817 : package cryptominisat 5.0.1
756251fMerge branch 'u/tmonteil/package_cryptominisat_5' of trac.sagemath.org:sage into HEAD
f66caff#22818 : remove old cryptominisat directory.
dc9b158#22818 : update module_list.py.
afffd2a#22818 : new cryptominisat interface.
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Author: Thierry Monteil

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Changed commit from afffd2a to 2807be3

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

2807be3#22818 : let nvars() behave consistently with DIMACS convention.
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Changed commit from 2807be3 to 262cd46

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

1a480b2#22818 : rhs option is the opposite of the former isfalse option.
1eda2df#22818 : change in verbose output.
1c45dae#22818 : cryptominisat does not have a maxrestarts option anymore.
262cd46#22818 : some solvers (including recent cryptominisat) do not implement a learnt_clauses method.
dimpase commented 7 years ago

Description changed:

--- 
+++ 
@@ -2,3 +2,7 @@

 #22818 and #22817 depend on each other.

+the tarball is at https://github.com/msoos/cryptominisat/archive/5.0.1.tar.gz
+
+(might have to renamed---or downloaded using a browser)
+
dimpase commented 7 years ago
comment:8

works on freebsd/clang, which is a good approx of OSX.

seblabbe commented 7 years ago

22818 and #22817 depend on each other.

Why two tickets then?

Can you add any/all of the following to the new module cryptominisat.py ?

# Support of Python 3
from __future__ import division, absolute_import, print_function, unicode_literals

My mac OSX is still compiling the newest version of Sage...

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:10

Replying to @seblabbe:

22818 and #22817 depend on each other.

Why two tickets then?

Well, they do not really depend on each other, #22818 depends on #22817, but since the current interface was not working anymore, i wanted to make clear to the release manager that #22817 should not be considered until #22818 get a positive review.

Moreover, while i was pretty confident to be able to package cryptominisat 5 (and let it work with cmake), it was not clear to me whether i will be the author of the current ticket, i was first planning to contact Martin Albrecht top help there, but change after change, i could do something acceptable.

Can you add any/all of the following to the new module cryptominisat.py ?

# Support of Python 3
from __future__ import division, absolute_import, print_function, unicode_literals

I will do this.

My mac OSX is still compiling the newest version of Sage...

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago

Description changed:

--- 
+++ 
@@ -1,8 +1,6 @@
 This ticket is a compagnon of #22817 which updates cryptominisat package to 5.0.1. Since our current cython interface does not work with cryptominisat 5, we have to rewrite the interface to use the python bindings that are now provided by cryptominisat.

-#22818 and #22817 depend on each other.
-
-the tarball is at https://github.com/msoos/cryptominisat/archive/5.0.1.tar.gz
+The tarball is at https://github.com/msoos/cryptominisat/archive/5.0.1.tar.gz

 (might have to renamed---or downloaded using a browser)
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

5f02977#22818 : implement comment 9 for Python 3 compatibility.
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Changed commit from 262cd46 to 5f02977

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:12

Replying to @sagetrac-tmonteil:

Replying to @seblabbe:

Can you add any/all of the following to the new module cryptominisat.py ?

# Support of Python 3
from __future__ import division, absolute_import, print_function, unicode_literals

I will do this.

Done.

seblabbe commented 7 years ago
comment:13

On top of #22999, with OSX 10.10, sage -i cryptominisat works and I get on relevant files:

sage -t --long src/sage/sat/solvers/cryptominisat.py
    [9 tests, 1.04 s]
sage -t --long src/sage/sat/boolean_polynomials.py
    [2 tests, 1.53 s]
sage -t --long src/sage/sat/converters/polybori.py
    [121 tests, 1.13 s]
sage -t --long src/sage/sat/solvers/satsolver.pyx
    [41 tests, 1.07 s]
----------------------------------------------------------------------
All tests passed!
----------------------------------------------------------------------
seblabbe commented 7 years ago

Changed keywords from days86 to days86, thursdaysbdx

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:14

Be careful that since cryptominisat is tagged as experimental, sage -t --long seems not to consider it as installed. For this, you have to change the file /build/pkgs/cryptominisat/type to optional (the number of tests should increase). Note also that the file rings/polynomial/multi_polynomial_sequence.py should be tested as well.

seblabbe commented 7 years ago
comment:15

I would suggest to move

        from sage.misc.package import PackageNotFoundError

inside the except ImportError clause.

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Changed commit from 5f02977 to afe37c5

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

afe37c5#22818 : move PackageNotFoundError import as suggested in comment 15.
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Changed commit from afe37c5 to 3ff0423

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

5f02977#22818 : implement comment 9 for Python 3 compatibility.
3ff0423#22818 : move PackageNotFoundError import as suggested in comment 15.
seblabbe commented 7 years ago
comment:18

Ok, so I can install it:

$ sage -installed
...
cryptominisat...........................5.0.1
...

but I can not run it properly:

sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat
sage: CryptoMiniSat()
---------------------------------------------------------------------------
PackageNotFoundError                      Traceback (most recent call last)
<ipython-input-2-8287720c4b48> in <module>()
----> 1 CryptoMiniSat()

/Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.pyc in __init__(self, verbosity, confl_limit, threads)
     58             from pycryptosat import Solver
     59         except ImportError:
---> 60             raise PackageNotFoundError("cryptominisat")
     61         self._solver = Solver(verbose=int(verbosity), confl_limit=int(confl_limit), threads=int(threads))
     62         self._nvars = 0

PackageNotFoundError: the package u'cryptominisat' was not found.
You can install it by running 'sage -i cryptominisat' in a shell

The real error is:

sage: from pycryptosat import Solver
---------------------------------------------------------------------------
ImportError                               Traceback (most recent call last)
<ipython-input-3-280927e3230f> in <module>()
----> 1 from pycryptosat import Solver

ImportError: dlopen(/Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib
  Referenced from: /Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/pycryptosat.so
  Reason: image not found
seblabbe commented 7 years ago
comment:19

...this shows that message PackageNotFoundError: the package u'cryptominisat' was not found. You can install it by running 'sage -i cryptominisat' in a shell is misleading because for me it is installed.

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:20

Could you go to your SAGE_LOCAL directory and type:

find | grep cryptominisat
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:21

as well as:

 find | grep cryptosat
seblabbe commented 7 years ago
comment:22

find with no argument?

$ find | grep cryptominisat
usage: find [-H | -L | -P] [-EXdsx] [-f path] path ... [expression]
       find [-H | -L | -P] [-EXdsx] -f path [path ...] [expression]
seblabbe commented 7 years ago
comment:23

Maybe this what you mean:

$ cd local/lib
$ ls | grep cryp
libcryptominisat5.5.0.dylib
libcryptominisat5.dylib
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:24

Replying to @seblabbe:

find with no argument?

$ find | grep cryptominisat
usage: find [-H | -L | -P] [-EXdsx] [-f path] path ... [expression]
       find [-H | -L | -P] [-EXdsx] -f path [path ...] [expression]

Who said OSX was user-friendly ?

You can try:

find -name '*cryptominisat*'

and

find -name '*cryptosat*'
seblabbe commented 7 years ago
comment:25

I needed to add . :

$ find . -name '*cryptominisat*'
./bin/cryptominisat5_simple
./include/cryptominisat5
./include/cryptominisat5/cryptominisat.h
./include/cryptominisat5/cryptominisat_c.h
./lib/cmake/cryptominisat5
./lib/cmake/cryptominisat5/cryptominisat5Config.cmake
./lib/cmake/cryptominisat5/cryptominisat5Targets-relwithdebinfo.cmake
./lib/cmake/cryptominisat5/cryptominisat5Targets.cmake
./lib/libcryptominisat5.5.0.dylib
./lib/libcryptominisat5.dylib
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.py
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.pyc
./var/lib/sage/installed/cryptominisat-5.0.1
 $ find . -name '*cryptosat*'
./lib/python2.7/site-packages/pycryptosat-5.0.1-py2.7.egg-info
./lib/python2.7/site-packages/pycryptosat.so
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:26

I do not see much difference, except that my .so files become .dylib, which seems an OSX specificity. Not sure how this impacts things.

Does the following work: put the block

p cnf 2 3
1 0
-2 0
-1 2 3 0

in the file /tmp/cnf, and run:

./bin/cryptominisat5 --verb 0 /tmp/cnf
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:27

Apparently, you do not have a ./bin/cryptominisat5 file, so try instead:

./bin/cryptominisat5_simple /tmp/cnf
seblabbe commented 7 years ago
comment:28

I get:

$ ./bin/cryptominisat5_simple --verb 0 /tmp/cnf
dyld: Library not loaded: libcryptominisat5.5.0.dylib
  Referenced from: /Users/slabbe/Applications/sage-git/local/./bin/cryptominisat5_simple
  Reason: image not found
Trace/BPT trap: 5

Same output without --verb 0.

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:29

What if you do the same from a sage -sh shell ? What is the output of echo $LDFLAGS ?

kiwifb commented 7 years ago
comment:30

OK, I can start debug your stuff. I suspect some stuff is not set as we want it in cryptominisat build system on OS X. Given the reports I am seeing, I'll want the output of 

otool -L lib/libcryptominisat5.5.0.dylib
otool -L bin/cryptominisat5_simple
otool -L lib/python2.7/site-packages/pycryptosat.so

please.

seblabbe commented 7 years ago
comment:31

Replying to @sagetrac-tmonteil:

What if you do the same from a sage -sh shell ?

same result

What is the output of echo $LDFLAGS ?

$ sage -sh
$ echo $LDFLAGS
-L/Users/slabbe/Applications/sage-git/local/lib -Wl,-rpath,/Users/slabbe/Applications/sage-git/local/lib
seblabbe commented 7 years ago
comment:32
$ otool -L lib/libcryptominisat5.5.0.dylib
lib/libcryptominisat5.5.0.dylib:
    libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
    /Users/slabbe/Applications/sage-git/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
    /Users/slabbe/Applications/sage-git/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1197.1.1)
    /Users/slabbe/Applications/sage-git/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)

$ otool -L bin/cryptominisat5_simple
bin/cryptominisat5_simple:
    libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
    /usr/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.5)
    /Users/slabbe/Applications/sage-git/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
    /Users/slabbe/Applications/sage-git/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1197.1.1)
    /Users/slabbe/Applications/sage-git/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)

$ otool -L lib/python2.7/site-packages/pycryptosat.so
lib/python2.7/site-packages/pycryptosat.so:
    build/lib.macosx-10.9-x86_64-2.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0)
    libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
    /Users/slabbe/Applications/sage-git/local/lib/libpython2.7.dylib (compatibility version 2.7.0, current version 2.7.0)
    /System/Library/Frameworks/CoreFoundation.framework/Versions/A/CoreFoundation (compatibility version 150.0.0, current version 1152.0.0)
    /Users/slabbe/Applications/sage-git/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1213.0.0)
    /Users/slabbe/Applications/sage-git/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)
kiwifb commented 7 years ago
comment:33
Mirage:sage-build fbissey$ otool -L /Users/fbissey/build/sage-build/local/bin/cryptominisat5_simple
/Users/fbissey/build/sage-build/local/bin/cryptominisat5_simple:
    libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
    /usr/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.8)
    /Users/fbissey/build/sage-build/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
    /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.5.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.50.2)
Mirage:sage-build fbissey$ otool -L /Users/fbissey/build/sage-build/local/lib/libcryptominisat5.5.0.dylib
/Users/fbissey/build/sage-build/local/lib/libcryptominisat5.5.0.dylib:
    libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
    /Users/fbissey/build/sage-build/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
    /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.5.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.50.2)

install_name is not set. This will not work properly on OS X but the fix will belong to #22817 as it is for building cryptominisat itself. Looking into it.

seblabbe commented 7 years ago
comment:34

Documentation of INPUTS of __init__ should go into the class, because it should appear first in:

CryptoMiniSat??

You may write See documentation class for inputs inside __init__. There are many example like this in Sage code.

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

be9db62#22818 : move documentation of INPUT from `__init__` to the class, as suggested in [comment:34](#comment%3A34).
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Changed commit from 3ff0423 to be9db62

edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:36

Replying to @seblabbe:

Documentation of INPUTS of __init__ should go into the class, because it should appear first in:

CryptoMiniSat??

You may write See documentation class for inputs inside __init__. There are many example like this in Sage code.

Done. Note that actually, we should put most of the doc in the documentation od the SAT function which is the only one imported in the namespace. Looking at it, it seems that the arguments can not be passed to the different class constructors.

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Changed commit from be9db62 to 0566102

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

0566102#22818 : pass options from SAT to CruptoMiniSat.
edd8e884-f507-429a-b577-5d554626c0fe commented 7 years ago
comment:38

Replying to @sagetrac-tmonteil:

Looking at it, it seems that the arguments can not be passed to the different class constructors.

Done for cryptominisat.

It is less easy for LP solver, since SAT will need a solver option to decide between cryptominisat and LP, and then another solver option to decide which MILP backend to use. Moreover, the SatLP input tells about a solver option, but then it does not pass it to MixedIntegerLinearProgram(). In any case, this will be for another ticket since it does not concerns cryptominisat.

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 7 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

e382251#22818 : remove useless import.