retag the tests: cryptominisat->pycryptosat

dimpase · dimpase · commit f834119e76e2 · 2022-01-22T20:07:39.000Z
diff --git a/build/pkgs/curl/spkg-install.in b/build/pkgs/curl/spkg-install.in
@@ -15,6 +15,6 @@ if [ "$UNAME" = "Darwin" ]; then
     fi
 fi
 
-sdh_configure $CURL_CONFIGURE
+sdh_configure $CURL_CONFIGURE --with-openssl
 sdh_make
 sdh_make_install
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
