Trac #33183: Better fix installation of cryptominisat and pycryptosat

Release Manager · Release Manager · commit 4fc017fc6fb6 · 2022-01-29T18:35:22.000+01:00
a followup to #33162 URL: https://trac.sagemath.org/33183 Reported by: dimpase Ticket author(s): Dima Pasechnik Reviewer(s): Matthias Koeppe
diff --git a/build/pkgs/cryptominisat/SPKG.rst b/build/pkgs/cryptominisat/SPKG.rst
@@ -35,3 +35,4 @@ Special Update/Build Instructions
 
 CryptoMiniSat's tarball downloaded from github is called VERSION.tar.gz
 and should be renamed to cryptominisat-VERSION.tar.gz
+Its Python module is installed by the pycryptosat spkg.
diff --git a/build/pkgs/cryptominisat/spkg-install.in b/build/pkgs/cryptominisat/spkg-install.in
@@ -3,7 +3,3 @@ cd src
 sdh_cmake -DUSE_GAUSS='ON' $EXTRA_OPTS
 sdh_make VERBOSE=ON
 sdh_make_install VERBOSE=ON
-
-cd pycryptosat
-
-sdh_pip_install .
diff --git a/build/pkgs/pycryptosat/SPKG.rst b/build/pkgs/pycryptosat/SPKG.rst
@@ -0,0 +1,22 @@
+pycryptosat: Python module of cryptominisat
+===========================================
+
+Description
+-----------
+
+   Build and install pycryptosat into appropriate venv.
+   See cryptominisat for more details.
+
+License
+-------
+
+MIT License
+
+
+Upstream Contact
+----------------
+
+-  Authors: Mate Soos
+-  Email: soos.mate@gmail.com
+-  Website: http://www.msoos.org/
+-  Releases: https://github.com/msoos/cryptominisat/releases
diff --git a/build/pkgs/pycryptosat/checksums.ini b/build/pkgs/pycryptosat/checksums.ini
@@ -0,0 +1 @@
+../cryptominisat/checksums.ini
diff --git a/build/pkgs/pycryptosat/dependencies b/build/pkgs/pycryptosat/dependencies
@@ -0,0 +1,5 @@
+$(PYTHON) m4ri zlib libpng cryptominisat | cmake boost_cropped $(PYTHON_TOOLCHAIN)
+
+----------
+All lines of this file are ignored except the first.
+It is copied by SAGE_ROOT/build/make/install into SAGE_ROOT/build/make/Makefile.
diff --git a/build/pkgs/pycryptosat/distros/conda.txt b/build/pkgs/pycryptosat/distros/conda.txt
@@ -0,0 +1 @@
+cryptominisat
diff --git a/build/pkgs/pycryptosat/distros/homebrew.txt b/build/pkgs/pycryptosat/distros/homebrew.txt
@@ -0,0 +1 @@
+cryptominisat
diff --git a/build/pkgs/pycryptosat/distros/repology.txt b/build/pkgs/pycryptosat/distros/repology.txt
@@ -0,0 +1 @@
+cryptominisat
diff --git a/build/pkgs/pycryptosat/install-requires.txt b/build/pkgs/pycryptosat/install-requires.txt
@@ -0,0 +1 @@
+pycryptosat
diff --git a/build/pkgs/pycryptosat/package-version.txt b/build/pkgs/pycryptosat/package-version.txt
@@ -0,0 +1 @@
+5.6.8
diff --git a/build/pkgs/pycryptosat/spkg-install.in b/build/pkgs/pycryptosat/spkg-install.in
@@ -0,0 +1,7 @@
+cd src
+
+sdh_cmake -DUSE_GAUSS='ON' $EXTRA_OPTS
+
+cd pycryptosat
+
+sdh_pip_install .
diff --git a/build/pkgs/pycryptosat/type b/build/pkgs/pycryptosat/type
@@ -0,0 +1 @@
+optional
diff --git a/src/doc/en/reference/sat/index.rst b/src/doc/en/reference/sat/index.rst
@@ -130,9 +130,9 @@ construct a very small-scale AES system of equations and pass it to a SAT solver
     ....:         break
     ....:     except ZeroDivisionError:
     ....:         pass
-    sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - cryptominisat
-    sage: s = solve_sat(F)                                            # optional - cryptominisat
-    sage: F.subs(s[0])                                                # optional - cryptominisat
+    sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat
+    sage: s = solve_sat(F)                                            # optional - pycryptosat
+    sage: F.subs(s[0])                                                # optional - pycryptosat
     Polynomial Sequence with 36 Polynomials in 0 Variables
 
 Details on Specific Highlevel Interfaces
diff --git a/src/sage/combinat/matrices/dancing_links.pyx b/src/sage/combinat/matrices/dancing_links.pyx
@@ -922,7 +922,7 @@ cdef class dancing_linksWrapper:
 
         Using some optional SAT solvers::
 
-            sage: x.to_sat_solver('cryptominisat')          # optional - cryptominisat
+            sage: x.to_sat_solver('cryptominisat')          # optional - pycryptosat
             CryptoMiniSat solver: 4 variables, 7 clauses.
 
         """
diff --git a/src/sage/rings/polynomial/multi_polynomial_sequence.py b/src/sage/rings/polynomial/multi_polynomial_sequence.py
@@ -1422,8 +1422,8 @@ def solve(self, algorithm='polybori', n=1,  eliminate_linear_variables=True, ver
 
         And we may use SAT-solvers if they are available::
 
-            sage: sol = S.solve(algorithm='sat') # optional - cryptominisat
-            sage: print(reproducible_repr(sol))  # optional - cryptominisat
+            sage: sol = S.solve(algorithm='sat') # optional - pycryptosat
+            sage: print(reproducible_repr(sol))  # optional - pycryptosat
             [{x: 0, y: 1, z: 0}]
             sage: S.subs( sol[0] )
             [0, 0, 0]
diff --git a/src/sage/sat/boolean_polynomials.py b/src/sage/sat/boolean_polynomials.py
@@ -81,68 +81,68 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
 
     and pass it to a SAT solver::
 
-        sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - cryptominisat
-        sage: s = solve_sat(F)                                            # optional - cryptominisat
-        sage: F.subs(s[0])                                                # optional - cryptominisat
+        sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat
+        sage: s = solve_sat(F)                                            # optional - pycryptosat
+        sage: F.subs(s[0])                                                # optional - pycryptosat
         Polynomial Sequence with 36 Polynomials in 0 Variables
 
     This time we pass a few options through to the converter and the solver::
 
-        sage: s = solve_sat(F, s_verbosity=1, c_max_vars_sparse=4, c_cutting_number=8) # optional - cryptominisat
+        sage: s = solve_sat(F, s_verbosity=1, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat
         c ...
         ...
-        sage: F.subs(s[0])                                                             # optional - cryptominisat
+        sage: F.subs(s[0])                                                             # optional - pycryptosat
         Polynomial Sequence with 36 Polynomials in 0 Variables
 
     We construct a very simple system with three solutions and ask for a specific number of solutions::
 
-        sage: B.<a,b> = BooleanPolynomialRing() # optional - cryptominisat
-        sage: f = a*b                           # optional - cryptominisat
-        sage: l = solve_sat([f],n=1)            # optional - cryptominisat
-        sage: len(l) == 1, f.subs(l[0])         # optional - cryptominisat
+        sage: B.<a,b> = BooleanPolynomialRing() # optional - pycryptosat
+        sage: f = a*b                           # optional - pycryptosat
+        sage: l = solve_sat([f],n=1)            # optional - pycryptosat
+        sage: len(l) == 1, f.subs(l[0])         # optional - pycryptosat
         (True, 0)
 
-        sage: l = solve_sat([a*b],n=2)        # optional - cryptominisat
-        sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - cryptominisat
+        sage: l = solve_sat([a*b],n=2)        # optional - pycryptosat
+        sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat
         (True, 0, 0)
 
-        sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=3))  # optional - cryptominisat
+        sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=3))  # optional - pycryptosat
         [(0, 0), (0, 1), (1, 0)]
-        sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=4))   # optional - cryptominisat
+        sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=4))   # optional - pycryptosat
         [(0, 0), (0, 1), (1, 0)]
-        sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=infinity))  # optional - cryptominisat
+        sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=infinity))  # optional - pycryptosat
         [(0, 0), (0, 1), (1, 0)]
 
     In the next example we see how the ``target_variables`` parameter works::
 
-        sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - cryptominisat
-        sage: R.<a,b,c,d> = BooleanPolynomialRing()                       # optional - cryptominisat
-        sage: F = [a+b,a+c+d]                                             # optional - cryptominisat
+        sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat
+        sage: R.<a,b,c,d> = BooleanPolynomialRing()                       # optional - pycryptosat
+        sage: F = [a+b,a+c+d]                                             # optional - pycryptosat
 
     First the normal use case::
 
-        sage: sorted((D[a], D[b], D[c], D[d]) for D in solve_sat(F,n=infinity))      # optional - cryptominisat
+        sage: sorted((D[a], D[b], D[c], D[d]) for D in solve_sat(F,n=infinity))      # optional - pycryptosat
         [(0, 0, 0, 0), (0, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0)]
 
     Now we are only interested in the solutions of the variables a and b::
 
-        sage: solve_sat(F,n=infinity,target_variables=[a,b])              # optional - cryptominisat
+        sage: solve_sat(F,n=infinity,target_variables=[a,b])              # optional - pycryptosat
         [{b: 0, a: 0}, {b: 1, a: 1}]
 
     Here, we generate and solve the cubic equations of the AES SBox (see :trac:`26676`)::
 
-        sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence    # optional - cryptominisat, long time
-        sage: from sage.sat.boolean_polynomials import solve as solve_sat                       # optional - cryptominisat, long time
-        sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, allow_zero_inversions = True)                  # optional - cryptominisat, long time
-        sage: sb = sr.sbox()                                                                    # optional - cryptominisat, long time
-        sage: eqs = sb.polynomials(degree = 3)                                                  # optional - cryptominisat, long time
-        sage: eqs = PolynomialSequence(eqs)                                                     # optional - cryptominisat, long time
-        sage: variables = map(str, eqs.variables())                                             # optional - cryptominisat, long time
-        sage: variables = ",".join(variables)                                                   # optional - cryptominisat, long time
-        sage: R = BooleanPolynomialRing(16, variables)                                          # optional - cryptominisat, long time
-        sage: eqs = [R(eq) for eq in eqs]                                                                 # optional - cryptominisat, long time
-        sage: sls_aes = solve_sat(eqs, n = infinity)                                            # optional - cryptominisat, long time
-        sage: len(sls_aes)                                                                      # optional - cryptominisat, long time
+        sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence    # optional - pycryptosat, long time
+        sage: from sage.sat.boolean_polynomials import solve as solve_sat                       # optional - pycryptosat, long time
+        sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, allow_zero_inversions = True)                  # optional - pycryptosat, long time
+        sage: sb = sr.sbox()                                                                    # optional - pycryptosat, long time
+        sage: eqs = sb.polynomials(degree = 3)                                                  # optional - pycryptosat, long time
+        sage: eqs = PolynomialSequence(eqs)                                                     # optional - pycryptosat, long time
+        sage: variables = map(str, eqs.variables())                                             # optional - pycryptosat, long time
+        sage: variables = ",".join(variables)                                                   # optional - pycryptosat, long time
+        sage: R = BooleanPolynomialRing(16, variables)                                          # optional - pycryptosat, long time
+        sage: eqs = [R(eq) for eq in eqs]                                                                 # optional - pycryptosat, long time
+        sage: sls_aes = solve_sat(eqs, n = infinity)                                            # optional - pycryptosat, long time
+        sage: len(sls_aes)                                                                      # optional - pycryptosat, long time
         256
 
     TESTS:
@@ -164,7 +164,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
         ....:     k9 + k28,
         ....:     k11 + k20]
         sage: from sage.sat.boolean_polynomials import solve as solve_sat
-        sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat'))     # optional - cryptominisat
+        sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat'))     # optional - pycryptosat
         [{k28: 0,
           k26: 1,
           k24: 0,
@@ -338,15 +338,15 @@ def learn(F, converter=None, solver=None, max_learnt_length=3, interreduction=Fa
 
     EXAMPLES::
 
-       sage: from sage.sat.boolean_polynomials import learn as learn_sat # optional - cryptominisat
+       sage: from sage.sat.boolean_polynomials import learn as learn_sat # optional - pycryptosat
 
     We construct a simple system and solve it::
 
-       sage: set_random_seed(2300)                      # optional - cryptominisat
-       sage: sr = mq.SR(1,2,2,4,gf2=True,polybori=True) # optional - cryptominisat
-       sage: F,s = sr.polynomial_system()               # optional - cryptominisat
-       sage: H = learn_sat(F)                           # optional - cryptominisat
-       sage: H[-1]                                      # optional - cryptominisat
+       sage: set_random_seed(2300)                      # optional - pycryptosat
+       sage: sr = mq.SR(1,2,2,4,gf2=True,polybori=True) # optional - pycryptosat
+       sage: F,s = sr.polynomial_system()               # optional - pycryptosat
+       sage: H = learn_sat(F)                           # optional - pycryptosat
+       sage: H[-1]                                      # optional - pycryptosat
        k033 + 1
     """
     try:
diff --git a/src/sage/sat/solvers/cryptominisat.py b/src/sage/sat/solvers/cryptominisat.py
diff --git a/src/sage/sat/solvers/satsolver.pyx b/src/sage/sat/solvers/satsolver.pyx

Original file line number	Diff line number	Diff line change
`@@ -35,3 +35,4 @@ Special Update/Build Instructions`
`35`	`35`
`36`	`36`	`CryptoMiniSat's tarball downloaded from github is called VERSION.tar.gz`
`37`	`37`	`and should be renamed to cryptominisat-VERSION.tar.gz`
	`38`	`+Its Python module is installed by the pycryptosat spkg.`