Opened 3 years ago

Closed 3 years ago

Last modified 4 months ago

#22818 closed enhancement (fixed)

Interface cryptominisat 5

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

Description (last modified by tmonteil)

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 3 years ago by tmonteil

  • Description modified (diff)
  • Keywords days86 added

comment:2 Changed 3 years ago by tmonteil

  • Branch set to u/tmonteil/interface_cryptominisat_5

comment:3 Changed 3 years ago by tmonteil

  • Authors set to Thierry Monteil
  • Commit set to 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 3 years ago by git

  • Commit changed from afffd2a0b590c332a34788336ea6b4fcc36bc500 to 2807be33c315b8ed1bc230f82f4c9284bc218818

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

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

comment:5 Changed 3 years ago by git

  • Commit changed from 2807be33c315b8ed1bc230f82f4c9284bc218818 to 262cd467374d41040e280bab399792163459b211

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 3 years ago by tmonteil

  • Status changed from new to needs_review

comment:7 Changed 3 years ago by dimpase

  • Description modified (diff)

comment:8 Changed 3 years ago by dimpase

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

comment:9 in reply to: ↑ description ; follow-up: Changed 3 years ago by slabbe

#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 ; follow-up: Changed 3 years ago by tmonteil

  • 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 3 years ago by git

  • Commit changed from 262cd467374d41040e280bab399792163459b211 to 5f02977b312c5179f10b3aeec48d7f5adead45f6

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 3 years ago by tmonteil

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 3 years ago by slabbe

  • 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 3 years ago by slabbe (previous) (diff)

comment:14 Changed 3 years ago by tmonteil

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 3 years ago by slabbe

I would suggest to move

        from sage.misc.package import PackageNotFoundError

inside the except ImportError clause.

comment:16 Changed 3 years ago by git

  • Commit changed from 5f02977b312c5179f10b3aeec48d7f5adead45f6 to afe37c5c8d90707b3d3daab9af1e066177fa627f

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 3 years ago by git

  • Commit changed from afe37c5c8d90707b3d3daab9af1e066177fa627f to 3ff0423b70bdffb5121a67f9033e072bedc30382

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 3 years ago by slabbe

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 3 years ago by slabbe (previous) (diff)

comment:19 Changed 3 years ago by slabbe

...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 3 years ago by tmonteil

Could you go to your SAGE_LOCAL directory and type:

find | grep cryptominisat

comment:21 Changed 3 years ago by tmonteil

as well as:

 find | grep cryptosat

comment:22 follow-up: Changed 3 years ago by 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]

comment:23 Changed 3 years ago by slabbe

Maybe this what you mean:

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

comment:24 in reply to: ↑ 22 Changed 3 years ago by tmonteil

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 3 years ago by slabbe

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 3 years ago by tmonteil

  • Cc fbissey 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 3 years ago by tmonteil

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

./bin/cryptominisat5_simple /tmp/cnf

comment:28 Changed 3 years ago by slabbe

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 3 years ago by slabbe (previous) (diff)

comment:29 follow-up: Changed 3 years ago by tmonteil

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

comment:30 Changed 3 years ago by fbissey

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 3 years ago by slabbe

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 3 years ago by slabbe

$ 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 3 years ago by slabbe (previous) (diff)

comment:33 Changed 3 years ago by fbissey

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 follow-up: Changed 3 years ago by 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.

comment:35 Changed 3 years ago by git

  • Commit changed from 3ff0423b70bdffb5121a67f9033e072bedc30382 to be9db62c3fb4d993f64a6678167c83038ae6c078

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 ; follow-up: Changed 3 years ago by tmonteil

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 3 years ago by git

  • Commit changed from be9db62c3fb4d993f64a6678167c83038ae6c078 to 056610267dbabf730fde0469e76a13f8015559e4

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 3 years ago by tmonteil

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 3 years ago by git

  • Commit changed from 056610267dbabf730fde0469e76a13f8015559e4 to e382251bcd94a8aade51a688bf942a4ecd7ce616

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

e382251#22818 : remove useless import.

comment:40 Changed 3 years ago by slabbe

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

comment:41 Changed 3 years ago by git

  • Commit changed from e382251bcd94a8aade51a688bf942a4ecd7ce616 to 5236281cb06a89832b57d1a63bc78bedd0156153

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

5236281#22818 : comment 40.

comment:42 follow-up: Changed 3 years ago by fbissey

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

comment:43 in reply to: ↑ 42 Changed 3 years ago by tmonteil

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 3 years ago by git

  • Commit changed from 5236281cb06a89832b57d1a63bc78bedd0156153 to 6ed1c73144024dd2af9f8ca88c503e2aebaaec5b

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 3 years ago by tmonteil

Done.

comment:46 Changed 3 years ago by slabbe

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 3 years ago by slabbe (previous) (diff)

comment:47 follow-up: Changed 3 years ago by fbissey

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 ; follow-up: Changed 3 years ago by slabbe

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 3 years ago by slabbe (previous) (diff)

comment:49 in reply to: ↑ 48 ; follow-up: Changed 3 years ago by fbissey

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 3 years ago by slabbe

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 3 years ago by tmonteil

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 3 years ago by tmonteil

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 3 years ago by slabbe

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 3 years ago by slabbe

  • Reviewers set to 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 3 years ago by slabbe (previous) (diff)

comment:55 Changed 3 years ago by slabbe

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 3 years ago by slabbe

  • Status changed from needs_review to needs_work

comment:57 Changed 3 years ago by git

  • Commit changed from 6ed1c73144024dd2af9f8ca88c503e2aebaaec5b to c9dd3554d82e640ff88eb435d51a823ad6608ac4

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

9593ce6Merge
c9dd355 #22818 : comment 55.

comment:58 Changed 3 years ago by tmonteil

  • Status changed from needs_work to needs_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 3 years ago by slabbe

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 3 years ago by slabbe

  • Status changed from needs_review to needs_work

comment:61 Changed 3 years ago by git

  • Commit changed from c9dd3554d82e640ff88eb435d51a823ad6608ac4 to c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4

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

c22de1d#22818 : comment 59.

comment:62 Changed 3 years ago by tmonteil

  • Status changed from needs_work to needs_review

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

comment:63 Changed 3 years ago by slabbe

  • Status changed from needs_review to positive_review

comment:64 Changed 3 years ago by tmonteil

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 follow-up: Changed 3 years ago by slabbe

I think yes. Maybe in another ticket.

comment:66 in reply to: ↑ 65 Changed 3 years ago by tmonteil

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 3 years ago by tmonteil

This is now #23219.

comment:68 Changed 3 years ago by vbraun

  • Branch changed from u/tmonteil/interface_cryptominisat_5 to c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4
  • Resolution set to fixed
  • Status changed from positive_review to closed

comment:69 Changed 2 years ago by slabbe

  • Commit c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4 deleted

See #23351 for a follow up ticket.

comment:70 Changed 4 months ago by tmonteil

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