Opened 6 years ago

Closed 5 years ago

Last modified 3 years ago

#22818 closed enhancement (fixed)

Interface cryptominisat 5

Reported by: Thierry Monteil Owned by:
Priority: major Milestone: sage-8.0
Component: packages: experimental Keywords: days86, thursdaysbdx, sdl
Cc: François Bissey Merged in:
Authors: Thierry Monteil Reviewers: Sébastien Labbé
Report Upstream: N/A Work issues:
Branch: c22de1d (Commits, GitHub, GitLab) Commit:
Dependencies: #22817 Stopgaps:

Status badges

Description (last modified by Thierry Monteil)

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)

Change History (70)

comment:1 Changed 6 years ago by Thierry Monteil

Description: modified (diff)
Keywords: days86 added

comment:2 Changed 6 years ago by Thierry Monteil

Branch: u/tmonteil/interface_cryptominisat_5

comment:3 Changed 6 years ago by Thierry Monteil

Authors: Thierry Monteil
Commit: afffd2a0b590c332a34788336ea6b4fcc36bc500

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.

comment:4 Changed 6 years ago by git

Commit: afffd2a0b590c332a34788336ea6b4fcc36bc5002807be33c315b8ed1bc230f82f4c9284bc218818

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

2807be3#22818 : let nvars() behave consistently with DIMACS convention.

comment:5 Changed 6 years ago by git

Commit: 2807be33c315b8ed1bc230f82f4c9284bc218818262cd467374d41040e280bab399792163459b211

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.

comment:6 Changed 6 years ago by Thierry Monteil

Status: newneeds_review

comment:7 Changed 6 years ago by Dima Pasechnik

Description: modified (diff)

comment:8 Changed 6 years ago by Dima Pasechnik

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

comment:9 in reply to:  description ; Changed 6 years ago by Sébastien Labbé

#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...

comment:10 in reply to:  9 ; Changed 6 years ago by Thierry Monteil

Description: modified (diff)

Replying to slabbe:

#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...

comment:11 Changed 6 years ago by git

Commit: 262cd467374d41040e280bab399792163459b2115f02977b312c5179f10b3aeec48d7f5adead45f6

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

5f02977#22818 : implement comment 9 for Python 3 compatibility.

comment:12 in reply to:  10 Changed 6 years ago by Thierry Monteil

Replying to tmonteil:

Replying to slabbe:

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.

comment:13 Changed 6 years ago by Sébastien Labbé

Keywords: thursdaysbdx added

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!
----------------------------------------------------------------------
Last edited 6 years ago by Sébastien Labbé (previous) (diff)

comment:14 Changed 6 years ago by Thierry Monteil

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.

comment:15 Changed 6 years ago by Sébastien Labbé

I would suggest to move

        from sage.misc.package import PackageNotFoundError

inside the except ImportError clause.

comment:16 Changed 6 years ago by git

Commit: 5f02977b312c5179f10b3aeec48d7f5adead45f6afe37c5c8d90707b3d3daab9af1e066177fa627f

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.

comment:17 Changed 6 years ago by git

Commit: afe37c5c8d90707b3d3daab9af1e066177fa627f3ff0423b70bdffb5121a67f9033e072bedc30382

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.

comment:18 Changed 6 years ago by Sébastien Labbé

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
Last edited 6 years ago by Sébastien Labbé (previous) (diff)

comment:19 Changed 6 years ago by Sébastien Labbé

...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.

comment:20 Changed 6 years ago by Thierry Monteil

Could you go to your SAGE_LOCAL directory and type:

find | grep cryptominisat

comment:21 Changed 6 years ago by Thierry Monteil

as well as:

 find | grep cryptosat

comment:22 Changed 6 years ago by Sébastien Labbé

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]

comment:23 Changed 6 years ago by Sébastien Labbé

Maybe this what you mean:

$ cd local/lib
$ ls | grep cryp
libcryptominisat5.5.0.dylib
libcryptominisat5.dylib

comment:24 in reply to:  22 Changed 6 years ago by Thierry Monteil

Replying to slabbe:

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*'

comment:25 Changed 6 years ago by Sébastien Labbé

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

comment:26 Changed 6 years ago by Thierry Monteil

Cc: François Bissey added

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

comment:27 Changed 6 years ago by Thierry Monteil

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

./bin/cryptominisat5_simple /tmp/cnf

comment:28 Changed 6 years ago by Sébastien Labbé

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.

Last edited 6 years ago by Sébastien Labbé (previous) (diff)

comment:29 Changed 6 years ago by Thierry Monteil

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

comment:30 Changed 6 years ago by François Bissey

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.

comment:31 in reply to:  29 Changed 6 years ago by Sébastien Labbé

Replying to 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

comment:32 Changed 6 years ago by Sébastien Labbé

$ 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)
Last edited 6 years ago by Sébastien Labbé (previous) (diff)

comment:33 Changed 6 years ago by François Bissey

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.

comment:34 Changed 6 years ago by Sébastien Labbé

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.

comment:35 Changed 6 years ago by git

Commit: 3ff0423b70bdffb5121a67f9033e072bedc30382be9db62c3fb4d993f64a6678167c83038ae6c078

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:36 in reply to:  34 ; Changed 6 years ago by Thierry Monteil

Replying to slabbe:

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.

comment:37 Changed 6 years ago by git

Commit: be9db62c3fb4d993f64a6678167c83038ae6c078056610267dbabf730fde0469e76a13f8015559e4

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

0566102#22818 : pass options from SAT to CruptoMiniSat.

comment:38 in reply to:  36 Changed 6 years ago by Thierry Monteil

Replying to 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.

comment:39 Changed 6 years ago by git

Commit: 056610267dbabf730fde0469e76a13f8015559e4e382251bcd94a8aade51a688bf942a4ecd7ce616

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

e382251#22818 : remove useless import.

comment:40 Changed 6 years ago by Sébastien Labbé

Still, there should be at least one EXAMPLES:: in __init__ for 100% coverage reason.

comment:41 Changed 6 years ago by git

Commit: e382251bcd94a8aade51a688bf942a4ecd7ce6165236281cb06a89832b57d1a63bc78bedd0156153

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

5236281#22818 : comment 40.

comment:42 Changed 6 years ago by François Bissey

You should rebase the branch of this ticket on the new branch of #22817.

comment:43 in reply to:  42 Changed 6 years ago by Thierry Monteil

Replying to fbissey:

You should rebase the branch of this ticket on the new branch of #22817.

Sure, i must first compile the changes made on #22817, and test it.

comment:44 Changed 6 years ago by git

Commit: 5236281cb06a89832b57d1a63bc78bedd01561536ed1c73144024dd2af9f8ca88c503e2aebaaec5b

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

6e93c20Merge branch 'develop' into package_cryptominisat_5
a8db509patch to get install_name to be properly installed on OS X. Subtle QA for install by using GNUInstallDirs - may need more love.
fd86b98Make sure we find sage's zlib rather the system one.
6ed1c73Merge branch 't/22818/interface_cryptominisat_5' into t/22817/package_cryptominisat_5

comment:45 Changed 6 years ago by Thierry Monteil

Done.

comment:46 Changed 6 years ago by Sébastien Labbé

On OSX 10.10, on top of #22999 and with #22818, I get:

$ sage -f cryptominisat
...
[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

Then, I still get:

sage: import pycryptosat
Traceback (most recent call last)
<ipython-input-1-1cca6683c235> in <module>()
----> 1 import pycryptosat

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

I do not know if there is something else I must do to install the new version of the branch? Do some rm in the lib folder to erase previous wrong cryptominisat lib from previous tries? Tell me if so.

Here is the output of previous commands you asked me:

$ find local -name '*cryptominisat*'
local/bin/cryptominisat5_simple
local/include/cryptominisat5
local/include/cryptominisat5/cryptominisat.h
local/include/cryptominisat5/cryptominisat_c.h
local/lib/cmake/cryptominisat5
local/lib/cmake/cryptominisat5/cryptominisat5Config.cmake
local/lib/cmake/cryptominisat5/cryptominisat5Targets-relwithdebinfo.cmake
local/lib/cmake/cryptominisat5/cryptominisat5Targets.cmake
local/lib/libcryptominisat5.5.0.dylib
local/lib/libcryptominisat5.dylib
local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat
local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.py
local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.pyc
local/var/lib/sage/installed/cryptominisat-5.0.1

$ find local -name '*cryptosat*'
local/lib/python2.7/site-packages/pycryptosat-5.0.1-py2.7.egg-info
local/lib/python2.7/site-packages/pycryptosat.so

Here is the output of otool as above if this may help:

$ otool -L lib/libcryptominisat5.5.0.dylib
lib/libcryptominisat5.5.0.dylib:
	/Users/slabbe/Applications/sage-git/local/lib/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:
	/Users/slabbe/Applications/sage-git/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
	/Users/slabbe/Applications/sage-git/local/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.8)
	/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)
Last edited 6 years ago by Sébastien Labbé (previous) (diff)

comment:47 Changed 6 years ago by François Bissey

lib/python2.7/site-packages/pycryptosat.so is not normal. My install shows

Mirage:sage-build fbissey$ otool -L local/lib/python2.7/site-packages/pycryptosat.so 
local/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)
	/Users/fbissey/build/sage-build/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
	/Users/fbissey/build/sage-build/local/lib/libpython2.7.dylib (compatibility version 2.7.0, current version 2.7.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.60.2)
	/System/Library/Frameworks/CoreFoundation.framework/Versions/A/CoreFoundation (compatibility version 150.0.0, current version 1349.8.0)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.5.0)

For some reason you appear to have an old install in the python folder. I didn't have to do any rm but removing that file before re-installing may be something to try.

comment:48 in reply to:  47 ; Changed 6 years ago by Sébastien Labbé

I did:

rm local/lib/python2.7/site-packages/pycryptosat.so
sage -f cryptominisat

I get:

$ otool -L local/lib/python2.7/site-packages/pycryptosat.so
local/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)
	/Users/slabbe/Applications/sage-git/local/lib/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)

and now:

sage: import pycryptosat
sage: from pycryptosat import Solver
sage: s = Solver()
sage: s.add_clause((1r,1r,1r,1r,-1r))
sage: s.solve()
(True, (None, False))

which is great! Should I sage -f -c cryptominisat now?

Last edited 6 years ago by Sébastien Labbé (previous) (diff)

comment:49 in reply to:  48 ; Changed 6 years ago by François Bissey

Replying to slabbe:

I did:

rm local/lib/python2.7/site-packages/pycryptosat.so
sage -f cryptominisat

and now:

sage: import pycryptosat
sage: from pycryptosat import Solver
sage: s = Solver()
sage: s.add_clause((1r,1r,1r,1r,-1r))
sage: s.solve()
(True, (None, False))

Looks good. I am not sure why the old one stuck around. It must have tricked cmake in being up to date.

Should I sage -f -c cryptominisat now?

????

comment:50 in reply to:  49 Changed 6 years ago by Sébastien Labbé

Should I sage -f -c cryptominisat now?

????

Indeed, I was confusing with #22999.

Should #22999 be a dependency of #22818, since it is now necessary for some versions of osx?

comment:51 Changed 6 years ago by Thierry Monteil

It could be a dependency of #218017, which is about building cryptominisat 5. Also, if everything builds fine on supported archs, we could move crymtominisat from experimental to optional (in particular this avoids the need to modify its type by hand when running doctests).

Regarding sage -f -c cryptominisat, there is no self-tests yet, so it will make no difference with sage -f cryptominisat (though it is always a good idea when reviewing a packaging ticket).

comment:52 Changed 6 years ago by Thierry Monteil

That said, i would really like to have cryptominisat 5 entering Sage 8.0, since i rely on sat solvers for some tutorials, where some people run the 32bit Sage Debian Live USB.

comment:53 Changed 6 years ago by Sébastien Labbé

On osx 10.10 with 8.0.beta7 + #22999 + #22818 + this change:

  • build/pkgs/cryptominisat/type

    diff --git a/build/pkgs/cryptominisat/type b/build/pkgs/cryptominisat/type
    index 9839eb2..134d9bc 100644
    a b  
    1 experimental
     1optional

the command:

sage -t --long src/sage/sat/solvers/cryptominisat.py src/sage/sat/boolean_polynomials.py src/sage/sat/converters/polybori.py src/sage/sat/solvers/satsolver.pyx src/sage/rings/polynomial/multi_polynomial_sequence.py

gives

Using --optional=4ti2,atlas,cbc,ccache,cryptominisat,latte_int,lidia,lrslib,mpir,pandoc_attributes,pandocfilters,python2,rst2ipynb,sage
Doctesting 5 files.
sage -t --long src/sage/sat/solvers/cryptominisat.py
    [49 tests, 1.16 s]
sage -t --long src/sage/sat/boolean_polynomials.py
    [27 tests, 1.98 s]
sage -t --long src/sage/sat/converters/polybori.py
    [121 tests, 1.21 s]
sage -t --long src/sage/sat/solvers/satsolver.pyx
    [42 tests, 1.20 s]
sage -t --long src/sage/rings/polynomial/multi_polynomial_sequence.py
    [237 tests, 11.70 s]
----------------------------------------------------------------------
All tests passed!
----------------------------------------------------------------------

comment:54 Changed 6 years ago by Sébastien Labbé

Reviewers: Sébastien Labbé

To me this is good to go and I am ok with changing type to optional.

I did not check that documentation builds fine though (overnight my computer will work on #22999 instead).

Last edited 6 years ago by Sébastien Labbé (previous) (diff)

comment:55 Changed 6 years ago by Sébastien Labbé

I builded the documentation but I can't find cryptominisat doc in the reference manual:

sage/sat/solvers/cryptominisat should be listed in src/doc/en/reference/sat/index.rst in the following section:

Details on Specific Solvers
^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. toctree::
   :maxdepth: 1

   sage/sat/solvers/satsolver
   sage/sat/solvers/dimacs
   sage/sat/solvers/sat_lp
.. optional - cryptominisat
.. sage/sat/solvers/cryptominisat/cryptominisat
.. sage/sat/solvers/cryptominisat/solverconf

In the same file, is the following paragraph still up to date?

Furthermore, Sage provides a C++ interface to the *CryptoMiniSat* [CMS]_
SAT solver which can be used interchangably with DIMACS-based solvers, but also
provides advanced features. For this last solver, the optional CryptoMiniSat
package must be installed, this can be accomplished by typing the following in the
shell::

    sage -i cryptominisat sagelib

In cryptominisat.py, it should be `` instead of ' :

    - 'confl_limit' -- an integer (default: ``None``). Abort after this many
      conflicts. If set to ``None``, never aborts.

Similar problem some lines below (I think this one should break the doc building) :

    - ``filename'' - ...

In input blocks, - should be changed to -- to adhere to the sage convention (several instances):

-        - ``decision`` - accepted for compatibility with other solvers, ignored.
+        - ``decision`` -- accepted for compatibility with other solvers, ignored.

Remove the empty line here:

+            sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat
+            sage: solver = CryptoMiniSat()                                  # optional - cryptominisat
+
+            sage: solver.nvars()                                            # optional - cryptominisat
+            0

Finaly, I would replace the top paragraph:

-This solver relies on Python bindings provided by upstream cryptominisat, and
-replaces the cython interface (written by Martin Albrecht in 2012) that does not
-work with recent versions of cryptominisat anymore.
-
-The ``cryptominisat`` package should be installed on your Sage installation.
-
-AUTHORS:
-
-- Thierry Monteil (2017): first version
+This solver relies on Python bindings provided by upstream cryptominisat.
+
+The ``cryptominisat`` package should be installed on your Sage installation.
+
+AUTHORS:
+
+- Thierry Monteil (2017): replaced the cython interface that does not work 
+   with version >=5.0 of cryptominisat anymore.
+- Martin Albrecht (2012): first version

Finally, no dot in the title:

-CryptoMiniSat Solver.
+CryptoMiniSat Solver

comment:56 Changed 6 years ago by Sébastien Labbé

Status: needs_reviewneeds_work

comment:57 Changed 6 years ago by git

Commit: 6ed1c73144024dd2af9f8ca88c503e2aebaaec5bc9dd3554d82e640ff88eb435d51a823ad6608ac4

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

9593ce6Merge
c9dd355 #22818 : comment 55.

comment:58 Changed 6 years ago by Thierry Monteil

Status: needs_workneeds_review

Thanks for the hints. I applied them quite blindly since i do not have enough RAM to build de doc anymore.

comment:59 Changed 5 years ago by Sébastien Labbé

Great. I managed to build the documentation without errors. I managed to see the Cryptominisat documentation in the reference manual. Every things is okay. Only one problem with the following paragraph which

  • misses a :: at the end,
  • misses a punctuation before Note that
  • misses the end of the last sentence?
        Note that in cryptominisat, the DIMACS standard format is augmented with
        the following extension: having an ``x`` in front of a line makes that
        line an XOR clause i Note that cryptominisat has its own 

comment:60 Changed 5 years ago by Sébastien Labbé

Status: needs_reviewneeds_work

comment:61 Changed 5 years ago by git

Commit: c9dd3554d82e640ff88eb435d51a823ad6608ac4c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4

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

c22de1d#22818 : comment 59.

comment:62 Changed 5 years ago by Thierry Monteil

Status: needs_workneeds_review

Sorry, it was an editing noise, the right sentences ends brefore, see https://www.msoos.org/xor-clauses/

comment:63 Changed 5 years ago by Sébastien Labbé

Status: needs_reviewpositive_review

comment:64 Changed 5 years ago by Thierry Monteil

Thanks for all the review, i am so happy that cryptominisat can now be installed on 32bit machines. BTW, shall we move the package from experimental to optional ?

comment:65 Changed 5 years ago by Sébastien Labbé

I think yes. Maybe in another ticket.

comment:66 in reply to:  65 Changed 5 years ago by Thierry Monteil

Replying to slabbe:

I think yes. Maybe in another ticket.

OK, let us not miss the 8.0 with a new round for that.

comment:67 Changed 5 years ago by Thierry Monteil

This is now #23219.

comment:68 Changed 5 years ago by Volker Braun

Branch: u/tmonteil/interface_cryptominisat_5c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4
Resolution: fixed
Status: positive_reviewclosed

comment:69 Changed 5 years ago by Sébastien Labbé

Commit: c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4

See #23351 for a follow up ticket.

comment:70 Changed 3 years ago by Thierry Monteil

Keywords: sdl added
Note: See TracTickets for help on using tickets.