Skip to content
This repository has been archived by the owner on Jan 30, 2023. It is now read-only.

Commit

Permalink
retag the tests: cryptominisat->pycryptosat
Browse files Browse the repository at this point in the history
  • Loading branch information
@dimpase
dimpase committed Jan 22, 2022
1 parent be0b019 commit f834119
Show file tree
Hide file tree
Showing 7 changed files with 90 additions and 90 deletions.
2 changes: 1 addition & 1 deletion build/pkgs/curl/spkg-install.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 3 additions & 3 deletions src/doc/en/reference/sat/index.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/sage/combinat/matrices/dancing_links.pyx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
"""
Expand Down
4 changes: 2 additions & 2 deletions src/sage/rings/polynomial/multi_polynomial_sequence.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
76 changes: 38 additions & 38 deletions src/sage/sat/boolean_polynomials.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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,
Expand Down Expand Up @@ -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:
Expand Down
Loading

0 comments on commit f834119

Please sign in to comment.