From f834119e76e2fda7e9346c6755d91278e51e0d9a Mon Sep 17 00:00:00 2001 From: Dima Pasechnik Date: Sat, 15 Jan 2022 21:37:37 +0000 Subject: [PATCH] retag the tests: cryptominisat->pycryptosat --- build/pkgs/curl/spkg-install.in | 2 +- src/doc/en/reference/sat/index.rst | 6 +- src/sage/combinat/matrices/dancing_links.pyx | 2 +- .../polynomial/multi_polynomial_sequence.py | 4 +- src/sage/sat/boolean_polynomials.py | 76 +++++++++--------- src/sage/sat/solvers/cryptominisat.py | 78 +++++++++---------- src/sage/sat/solvers/satsolver.pyx | 12 +-- 7 files changed, 90 insertions(+), 90 deletions(-) diff --git a/build/pkgs/curl/spkg-install.in b/build/pkgs/curl/spkg-install.in index bc09f074780..99890b5b0f7 100644 --- 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 index c7a3ba619dd..c0cfb22f855 100644 --- 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 index ab43cef4260..d3b406751d7 100644 --- 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 index 7b493051d81..7893d5f95be 100644 --- 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 index 603f4aabcc5..eb708081346 100644 --- 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. = 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. = 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. = 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. = 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 index b7360ab3762..6a090604438 100644 --- a/src/sage/sat/solvers/cryptominisat.py +++ b/src/sage/sat/solvers/cryptominisat.py @@ -47,7 +47,7 @@ class CryptoMiniSat(SatSolver): EXAMPLES:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat """ def __init__(self, verbosity=0, confl_limit=None, threads=None): r""" @@ -58,7 +58,7 @@ def __init__(self, verbosity=0, confl_limit=None, threads=None): EXAMPLES:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat(threads=1) # optional - cryptominisat + sage: solver = CryptoMiniSat(threads=1) # optional - pycryptosat """ if threads is None: from sage.parallel.ncpus import ncpus @@ -81,12 +81,12 @@ def var(self, decision=None): EXAMPLES:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.var() # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.var() # optional - pycryptosat 1 - sage: solver.add_clause((-1,2,-4)) # optional - cryptominisat - sage: solver.var() # optional - cryptominisat + sage: solver.add_clause((-1,2,-4)) # optional - pycryptosat + sage: solver.var() # optional - pycryptosat 5 """ self._nvars += 1 @@ -101,15 +101,15 @@ def nvars(self): EXAMPLES:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.nvars() # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.nvars() # optional - pycryptosat 0 If a variable with intermediate index is not used, it is still considered as a variable:: - sage: solver.add_clause((1,-2,4)) # optional - cryptominisat - sage: solver.nvars() # optional - cryptominisat + sage: solver.add_clause((1,-2,4)) # optional - pycryptosat + sage: solver.nvars() # optional - pycryptosat 4 """ return self._nvars @@ -131,8 +131,8 @@ def add_clause(self, lits): EXAMPLES:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.add_clause((1, -2 , 3)) # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.add_clause((1, -2 , 3)) # optional - pycryptosat """ if 0 in lits: raise ValueError("0 should not appear in the clause: {}".format(lits)) @@ -156,8 +156,8 @@ def add_xor_clause(self, lits, rhs=True): EXAMPLES:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.add_xor_clause((1, 2 , 3), False) # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.add_xor_clause((1, 2 , 3), False) # optional - pycryptosat """ if 0 in lits: raise ValueError("0 should not appear in the clause: {}".format(lits)) @@ -182,15 +182,15 @@ def __call__(self, assumptions=None): EXAMPLES:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.add_clause((1,2)) # optional - cryptominisat - sage: solver.add_clause((-1,2)) # optional - cryptominisat - sage: solver.add_clause((-1,-2)) # optional - cryptominisat - sage: solver() # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.add_clause((1,2)) # optional - pycryptosat + sage: solver.add_clause((-1,2)) # optional - pycryptosat + sage: solver.add_clause((-1,-2)) # optional - pycryptosat + sage: solver() # optional - pycryptosat (None, False, True) - sage: solver.add_clause((1,-2)) # optional - cryptominisat - sage: solver() # optional - cryptominisat + sage: solver.add_clause((1,-2)) # optional - pycryptosat + sage: solver() # optional - pycryptosat False """ satisfiable, assignments = self._solver.solve() @@ -204,8 +204,8 @@ def __repr__(self): TESTS:: sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver # optional - pycryptosat CryptoMiniSat solver: 0 variables, 0 clauses. """ return "CryptoMiniSat solver: {} variables, {} clauses.".format(self.nvars(), len(self.clauses())) @@ -231,22 +231,22 @@ def clauses(self, filename=None): EXAMPLES:: sage: from sage.sat.solvers import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.add_clause((1,2,3,4,5,6,7,8,-9)) # optional - cryptominisat - sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True) # optional - cryptominisat - sage: solver.clauses() # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.add_clause((1,2,3,4,5,6,7,8,-9)) # optional - pycryptosat + sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True) # optional - pycryptosat + sage: solver.clauses() # optional - pycryptosat [((1, 2, 3, 4, 5, 6, 7, 8, -9), False, None), ((1, 2, 3, 4, 5, 6, 7, 8, 9), True, True)] DIMACS format output:: sage: from sage.sat.solvers import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.add_clause((1, 2, 4)) # optional - cryptominisat - sage: solver.add_clause((1, 2, -4)) # optional - cryptominisat - sage: fn = tmp_filename() # optional - cryptominisat - sage: solver.clauses(fn) # optional - cryptominisat - sage: print(open(fn).read()) # optional - cryptominisat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.add_clause((1, 2, 4)) # optional - pycryptosat + sage: solver.add_clause((1, 2, -4)) # optional - pycryptosat + sage: fn = tmp_filename() # optional - pycryptosat + sage: solver.clauses(fn) # optional - pycryptosat + sage: print(open(fn).read()) # optional - pycryptosat p cnf 4 2 1 2 4 0 1 2 -4 0 @@ -256,9 +256,9 @@ def clauses(self, filename=None): the following extension: having an ``x`` in front of a line makes that line an XOR clause:: - sage: solver.add_xor_clause((1,2,3), rhs=True) # optional - cryptominisat - sage: solver.clauses(fn) # optional - cryptominisat - sage: print(open(fn).read()) # optional - cryptominisat + sage: solver.add_xor_clause((1,2,3), rhs=True) # optional - pycryptosat + sage: solver.clauses(fn) # optional - pycryptosat + sage: print(open(fn).read()) # optional - pycryptosat p cnf 4 3 1 2 4 0 1 2 -4 0 @@ -268,9 +268,9 @@ def clauses(self, filename=None): Note that inverting an xor-clause is equivalent to inverting one of the variables:: - sage: solver.add_xor_clause((1,2,5),rhs=False) # optional - cryptominisat - sage: solver.clauses(fn) # optional - cryptominisat - sage: print(open(fn).read()) # optional - cryptominisat + sage: solver.add_xor_clause((1,2,5),rhs=False) # optional - pycryptosat + sage: solver.clauses(fn) # optional - pycryptosat + sage: print(open(fn).read()) # optional - pycryptosat p cnf 5 4 1 2 4 0 1 2 -4 0 diff --git a/src/sage/sat/solvers/satsolver.pyx b/src/sage/sat/solvers/satsolver.pyx index 326497aa3ef..9ce831636a6 100644 --- a/src/sage/sat/solvers/satsolver.pyx +++ b/src/sage/sat/solvers/satsolver.pyx @@ -127,12 +127,12 @@ cdef class SatSolver: sage: from io import StringIO sage: file_object = StringIO("c A sample .cnf file with xor clauses.\np cnf 3 3\n1 2 0\n3 0\nx1 2 3 0") - sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat # optional - cryptominisat - sage: solver = CryptoMiniSat() # optional - cryptominisat - sage: solver.read(file_object) # optional - cryptominisat - sage: solver.clauses() # optional - cryptominisat + sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat # optional - pycryptosat + sage: solver = CryptoMiniSat() # optional - pycryptosat + sage: solver.read(file_object) # optional - pycryptosat + sage: solver.clauses() # optional - pycryptosat [((1, 2), False, None), ((3,), False, None), ((1, 2, 3), True, True)] - sage: solver() # optional - cryptominisat + sage: solver() # optional - pycryptosat (None, True, True, True) TESTS:: @@ -350,7 +350,7 @@ def SAT(solver=None, *args, **kwds): Forcing CryptoMiniSat:: - sage: SAT(solver="cryptominisat") # optional - cryptominisat + sage: SAT(solver="cryptominisat") # optional - pycryptosat CryptoMiniSat solver: 0 variables, 0 clauses. Forcing PicoSat::