#22818 closed enhancement (fixed)
Interface cryptominisat 5
Reported by:  tmonteil  Owned by:  

Priority:  major  Milestone:  sage8.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 )
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 renamedor downloaded using a browser)
Change History (70)
comment:1 Changed 3 years ago by
 Description modified (diff)
 Keywords days86 added
comment:2 Changed 3 years ago by
 Branch set to u/tmonteil/interface_cryptominisat_5
comment:3 Changed 3 years ago by
 Commit set to afffd2a0b590c332a34788336ea6b4fcc36bc500
comment:4 Changed 3 years ago by
 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
 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
 Status changed from new to needs_review
comment:7 Changed 3 years ago by
 Description modified (diff)
comment:8 Changed 3 years ago by
works on freebsd/clang, which is a good approx of OSX.
comment:9 in reply to: ↑ description ; followup: ↓ 10 Changed 3 years ago by
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 ; followup: ↓ 12 Changed 3 years ago by
 Description modified (diff)
Replying to slabbe:
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
 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
comment:13 Changed 3 years ago by
 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! 
comment:14 Changed 3 years ago by
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
I would suggest to move
from sage.misc.package import PackageNotFoundError
inside the except ImportError
clause.
comment:16 Changed 3 years ago by
 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
 Commit changed from afe37c5c8d90707b3d3daab9af1e066177fa627f to 3ff0423b70bdffb5121a67f9033e072bedc30382
comment:18 Changed 3 years ago by
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) <ipythoninput28287720c4b48> in <module>() > 1 CryptoMiniSat() /Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/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) <ipythoninput3280927e3230f> in <module>() > 1 from pycryptosat import Solver ImportError: dlopen(/Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib Referenced from: /Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/pycryptosat.so Reason: image not found
comment:19 Changed 3 years ago by
...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
Could you go to your SAGE_LOCAL
directory and type:
find  grep cryptominisat
comment:21 Changed 3 years ago by
as well as:
find  grep cryptosat
comment:22 followup: ↓ 24 Changed 3 years ago by
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
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
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 userfriendly ?
You can try:
find name '*cryptominisat*'
and
find name '*cryptosat*'
comment:25 Changed 3 years ago by
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/cryptominisat5Targetsrelwithdebinfo.cmake ./lib/cmake/cryptominisat5/cryptominisat5Targets.cmake ./lib/libcryptominisat5.5.0.dylib ./lib/libcryptominisat5.dylib ./lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat ./lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.py ./lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.pyc ./var/lib/sage/installed/cryptominisat5.0.1
$ find . name '*cryptosat*' ./lib/python2.7/sitepackages/pycryptosat5.0.1py2.7.egginfo ./lib/python2.7/sitepackages/pycryptosat.so
comment:26 Changed 3 years ago by
 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
Apparently, you do not have a ./bin/cryptominisat5
file, so try instead:
./bin/cryptominisat5_simple /tmp/cnf
comment:28 Changed 3 years ago by
I get:
$ ./bin/cryptominisat5_simple verb 0 /tmp/cnf dyld: Library not loaded: libcryptominisat5.5.0.dylib Referenced from: /Users/slabbe/Applications/sagegit/local/./bin/cryptominisat5_simple Reason: image not found Trace/BPT trap: 5
Same output without verb 0
.
comment:29 followup: ↓ 31 Changed 3 years ago by
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
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/sitepackages/pycryptosat.so
please.
comment:31 in reply to: ↑ 29 Changed 3 years ago by
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/sagegit/local/lib Wl,rpath,/Users/slabbe/Applications/sagegit/local/lib
comment:32 Changed 3 years ago by
$ 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/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/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/sagegit/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/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/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/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0) $ otool L lib/python2.7/sitepackages/pycryptosat.so lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.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/sagegit/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/sagegit/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/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)
comment:33 Changed 3 years ago by
Mirage:sagebuild fbissey$ otool L /Users/fbissey/build/sagebuild/local/bin/cryptominisat5_simple /Users/fbissey/build/sagebuild/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/sagebuild/local/lib/libm4ri0.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:sagebuild fbissey$ otool L /Users/fbissey/build/sagebuild/local/lib/libcryptominisat5.5.0.dylib /Users/fbissey/build/sagebuild/local/lib/libcryptominisat5.5.0.dylib: libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/fbissey/build/sagebuild/local/lib/libm4ri0.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 followup: ↓ 36 Changed 3 years ago by
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
 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 ; followup: ↓ 38 Changed 3 years ago by
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
 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
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
 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
Still, there should be at least one EXAMPLES::
in __init__
for 100% coverage reason.
comment:41 Changed 3 years ago by
 Commit changed from e382251bcd94a8aade51a688bf942a4ecd7ce616 to 5236281cb06a89832b57d1a63bc78bedd0156153
Branch pushed to git repo; I updated commit sha1. New commits:
5236281  #22818 : comment 40.

comment:42 followup: ↓ 43 Changed 3 years ago by
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
comment:44 Changed 3 years ago by
 Commit changed from 5236281cb06a89832b57d1a63bc78bedd0156153 to 6ed1c73144024dd2af9f8ca88c503e2aebaaec5b
Branch pushed to git repo; I updated commit sha1. New commits:
6e93c20  Merge branch 'develop' into package_cryptominisat_5

a8db509  patch to get install_name to be properly installed on OS X. Subtle QA for install by using GNUInstallDirs  may need more love.

fd86b98  Make sure we find sage's zlib rather the system one.

6ed1c73  Merge branch 't/22818/interface_cryptominisat_5' into t/22817/package_cryptominisat_5

comment:45 Changed 3 years ago by
Done.
comment:46 Changed 3 years ago by
On OSX 10.10, on top of #22999 and with #22818, I get:
$ sage f cryptominisat ... [cryptominisat5.0.1] Successfully installed cryptominisat5.0.1
Then, I still get:
sage: import pycryptosat Traceback (most recent call last) <ipythoninput11cca6683c235> in <module>() > 1 import pycryptosat ImportError: dlopen(/Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib Referenced from: /Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/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/cryptominisat5Targetsrelwithdebinfo.cmake local/lib/cmake/cryptominisat5/cryptominisat5Targets.cmake local/lib/libcryptominisat5.5.0.dylib local/lib/libcryptominisat5.dylib local/lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat local/lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.py local/lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.pyc local/var/lib/sage/installed/cryptominisat5.0.1 $ find local name '*cryptosat*' local/lib/python2.7/sitepackages/pycryptosat5.0.1py2.7.egginfo local/lib/python2.7/sitepackages/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/sagegit/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/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/sagegit/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/sagegit/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.8) /Users/slabbe/Applications/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/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/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0) $ otool L lib/python2.7/sitepackages/pycryptosat.so lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.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/sagegit/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/sagegit/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/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)
comment:47 followup: ↓ 48 Changed 3 years ago by
lib/python2.7/sitepackages/pycryptosat.so
is not normal. My install shows
Mirage:sagebuild fbissey$ otool L local/lib/python2.7/sitepackages/pycryptosat.so local/lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0) /Users/fbissey/build/sagebuild/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/fbissey/build/sagebuild/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 reinstalling may be something to try.
comment:48 in reply to: ↑ 47 ; followup: ↓ 49 Changed 3 years ago by
I did:
rm local/lib/python2.7/sitepackages/pycryptosat.so sage f cryptominisat
I get:
$ otool L local/lib/python2.7/sitepackages/pycryptosat.so local/lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/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/sagegit/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/sagegit/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?
comment:49 in reply to: ↑ 48 ; followup: ↓ 50 Changed 3 years ago by
Replying to slabbe:
I did:
rm local/lib/python2.7/sitepackages/pycryptosat.so sage f cryptominisatand 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
comment:51 Changed 3 years ago by
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 selftests 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
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
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 experimental1 optional
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
 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).
comment:55 Changed 3 years ago by
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 DIMACSbased 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
 Status changed from needs_review to needs_work
comment:57 Changed 3 years ago by
 Commit changed from 6ed1c73144024dd2af9f8ca88c503e2aebaaec5b to c9dd3554d82e640ff88eb435d51a823ad6608ac4
comment:58 Changed 3 years ago by
 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
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
 Status changed from needs_review to needs_work
comment:61 Changed 3 years ago by
 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
 Status changed from needs_work to needs_review
Sorry, it was an editing noise, the right sentences ends brefore, see https://www.msoos.org/xorclauses/
comment:63 Changed 3 years ago by
 Status changed from needs_review to positive_review
comment:64 Changed 3 years ago by
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 followup: ↓ 66 Changed 3 years ago by
I think yes. Maybe in another ticket.
comment:66 in reply to: ↑ 65 Changed 3 years ago by
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
This is now #23219.
comment:68 Changed 3 years ago by
 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
 Commit c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4 deleted
See #23351 for a follow up ticket.
comment:70 Changed 4 months ago by
 Keywords sdl added
New commits:
#22817 : package cryptominisat 5.0.1
Merge branch 'u/tmonteil/package_cryptominisat_5' of trac.sagemath.org:sage into HEAD
#22818 : remove old cryptominisat directory.
#22818 : update module_list.py.
#22818 : new cryptominisat interface.