Skip to content

Commit 417429f

Browse files
author
Matthias Koeppe
committed
src/sage/sat: sage -fixdoctests --only-tags
1 parent e43e09a commit 417429f

File tree

5 files changed

+73
-66
lines changed

5 files changed

+73
-66
lines changed

‎src/sage/sat/boolean_polynomials.py

Lines changed: 35 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -72,8 +72,8 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
7272
7373
We construct a very small-scale AES system of equations::
7474
75-
sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # optional - sage.modules sage.rings.finite_rings
76-
sage: while True: # workaround (see :trac:`31891`) # optional - sage.modules sage.rings.finite_rings
75+
sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # needs sage.modules sage.rings.finite_rings
76+
sage: while True: # workaround (see :trac:`31891`) # needs sage.modules sage.rings.finite_rings
7777
....: try:
7878
....: F, s = sr.polynomial_system()
7979
....: break
@@ -83,68 +83,70 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
8383
and pass it to a SAT solver::
8484
8585
sage: from sage.sat.boolean_polynomials import solve as solve_sat
86-
sage: s = solve_sat(F) # optional - pycryptosat sage.modules sage.rings.finite_rings
87-
sage: F.subs(s[0]) # optional - pycryptosat sage.modules sage.rings.finite_rings
86+
sage: s = solve_sat(F) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings
87+
sage: F.subs(s[0]) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings
8888
Polynomial Sequence with 36 Polynomials in 0 Variables
8989
9090
This time we pass a few options through to the converter and the solver::
9191
92-
sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat sage.modules sage.rings.finite_rings
93-
sage: F.subs(s[0]) # optional - pycryptosat sage.modules sage.rings.finite_rings
92+
sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat, needs sage.modules sage.rings.finite_rings
93+
sage: F.subs(s[0]) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings
9494
Polynomial Sequence with 36 Polynomials in 0 Variables
9595
9696
We construct a very simple system with three solutions
9797
and ask for a specific number of solutions::
9898
99-
sage: B.<a,b> = BooleanPolynomialRing() # optional - pycryptosat sage.modules
100-
sage: f = a*b # optional - pycryptosat sage.modules
101-
sage: l = solve_sat([f],n=1) # optional - pycryptosat sage.modules
102-
sage: len(l) == 1, f.subs(l[0]) # optional - pycryptosat sage.modules
99+
sage: # optional - pycryptosat, needs sage.modules
100+
sage: B.<a,b> = BooleanPolynomialRing()
101+
sage: f = a*b
102+
sage: l = solve_sat([f],n=1)
103+
sage: len(l) == 1, f.subs(l[0])
103104
(True, 0)
104105
105-
sage: l = solve_sat([a*b],n=2) # optional - pycryptosat sage.modules
106-
sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat sage.modules
106+
sage: l = solve_sat([a*b],n=2) # optional - pycryptosat # needs sage.modules
107+
sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat # needs sage.modules
107108
(True, 0, 0)
108109
109-
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) # optional - pycryptosat sage.modules
110+
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) # optional - pycryptosat, needs sage.modules
110111
[(0, 0), (0, 1), (1, 0)]
111-
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) # optional - pycryptosat sage.modules
112+
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) # optional - pycryptosat, needs sage.modules
112113
[(0, 0), (0, 1), (1, 0)]
113-
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) # optional - pycryptosat sage.modules
114+
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) # optional - pycryptosat, needs sage.modules
114115
[(0, 0), (0, 1), (1, 0)]
115116
116117
In the next example we see how the ``target_variables`` parameter works::
117118
118119
sage: from sage.sat.boolean_polynomials import solve as solve_sat
119-
sage: R.<a,b,c,d> = BooleanPolynomialRing() # optional - pycryptosat sage.modules
120-
sage: F = [a + b, a + c + d] # optional - pycryptosat sage.modules
120+
sage: R.<a,b,c,d> = BooleanPolynomialRing() # optional - pycryptosat # needs sage.modules
121+
sage: F = [a + b, a + c + d] # optional - pycryptosat # needs sage.modules
121122
122123
First the normal use case::
123124
124-
sage: sorted((D[a], D[b], D[c], D[d]) # optional - pycryptosat sage.modules
125+
sage: sorted((D[a], D[b], D[c], D[d]) # optional - pycryptosat # needs sage.modules
125126
....: for D in solve_sat(F, n=infinity))
126127
[(0, 0, 0, 0), (0, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0)]
127128
128129
Now we are only interested in the solutions of the variables a and b::
129130
130-
sage: solve_sat(F, n=infinity, target_variables=[a,b]) # optional - pycryptosat sage.modules
131+
sage: solve_sat(F, n=infinity, target_variables=[a,b]) # optional - pycryptosat, needs sage.modules
131132
[{b: 0, a: 0}, {b: 1, a: 1}]
132133
133134
Here, we generate and solve the cubic equations of the AES SBox (see :trac:`26676`)::
134135
136+
sage: # long time, optional - pycryptosat, needs sage.modules
135137
sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence
136138
sage: from sage.sat.boolean_polynomials import solve as solve_sat
137-
sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, # long time, optional - pycryptosat sage.modules
139+
sage: sr = sage.crypto.mq.SR(1, 4, 4, 8,
138140
....: allow_zero_inversions=True)
139-
sage: sb = sr.sbox() # long time, optional - pycryptosat sage.modules
140-
sage: eqs = sb.polynomials(degree=3) # long time, optional - pycryptosat sage.modules
141-
sage: eqs = PolynomialSequence(eqs) # long time, optional - pycryptosat sage.modules
142-
sage: variables = map(str, eqs.variables()) # long time, optional - pycryptosat sage.modules
143-
sage: variables = ",".join(variables) # long time, optional - pycryptosat sage.modules
144-
sage: R = BooleanPolynomialRing(16, variables) # long time, optional - pycryptosat sage.modules
145-
sage: eqs = [R(eq) for eq in eqs] # long time, optional - pycryptosat sage.modules
146-
sage: sls_aes = solve_sat(eqs, n = infinity) # long time, optional - pycryptosat sage.modules
147-
sage: len(sls_aes) # long time, optional - pycryptosat sage.modules
141+
sage: sb = sr.sbox()
142+
sage: eqs = sb.polynomials(degree=3)
143+
sage: eqs = PolynomialSequence(eqs)
144+
sage: variables = map(str, eqs.variables())
145+
sage: variables = ",".join(variables)
146+
sage: R = BooleanPolynomialRing(16, variables)
147+
sage: eqs = [R(eq) for eq in eqs]
148+
sage: sls_aes = solve_sat(eqs, n = infinity)
149+
sage: len(sls_aes)
148150
256
149151
150152
TESTS:
@@ -345,10 +347,10 @@ def learn(F, converter=None, solver=None, max_learnt_length=3, interreduction=Fa
345347
We construct a simple system and solve it::
346348
347349
sage: set_random_seed(2300)
348-
sage: sr = mq.SR(1, 2, 2, 4, gf2=True, polybori=True) # optional - pycryptosat sage.modules sage.rings.finite_rings
349-
sage: F,s = sr.polynomial_system() # optional - pycryptosat sage.modules sage.rings.finite_rings
350-
sage: H = learn_sat(F) # optional - pycryptosat sage.modules sage.rings.finite_rings
351-
sage: H[-1] # optional - pycryptosat sage.modules sage.rings.finite_rings
350+
sage: sr = mq.SR(1, 2, 2, 4, gf2=True, polybori=True) # optional - pycryptosat, needs sage.modules sage.rings.finite_rings
351+
sage: F,s = sr.polynomial_system() # optional - pycryptosat # needs sage.modules sage.rings.finite_rings
352+
sage: H = learn_sat(F) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings
353+
sage: H[-1] # optional - pycryptosat # needs sage.modules sage.rings.finite_rings
352354
k033 + 1
353355
"""
354356
try:

‎src/sage/sat/solvers/cryptominisat.py

Lines changed: 18 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -182,12 +182,13 @@ def __call__(self, assumptions=None):
182182
183183
EXAMPLES::
184184
185+
sage: # optional - pycryptosat
185186
sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat
186-
sage: solver = CryptoMiniSat() # optional - pycryptosat
187-
sage: solver.add_clause((1,2)) # optional - pycryptosat
188-
sage: solver.add_clause((-1,2)) # optional - pycryptosat
189-
sage: solver.add_clause((-1,-2)) # optional - pycryptosat
190-
sage: solver() # optional - pycryptosat
187+
sage: solver = CryptoMiniSat()
188+
sage: solver.add_clause((1,2))
189+
sage: solver.add_clause((-1,2))
190+
sage: solver.add_clause((-1,-2))
191+
sage: solver()
191192
(None, False, True)
192193
193194
sage: solver.add_clause((1,-2)) # optional - pycryptosat
@@ -231,23 +232,25 @@ def clauses(self, filename=None):
231232
232233
EXAMPLES::
233234
235+
sage: # optional - pycryptosat
234236
sage: from sage.sat.solvers import CryptoMiniSat
235-
sage: solver = CryptoMiniSat() # optional - pycryptosat
236-
sage: solver.add_clause((1,2,3,4,5,6,7,8,-9)) # optional - pycryptosat
237-
sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True) # optional - pycryptosat
238-
sage: solver.clauses() # optional - pycryptosat
237+
sage: solver = CryptoMiniSat()
238+
sage: solver.add_clause((1,2,3,4,5,6,7,8,-9))
239+
sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True)
240+
sage: solver.clauses()
239241
[((1, 2, 3, 4, 5, 6, 7, 8, -9), False, None),
240242
((1, 2, 3, 4, 5, 6, 7, 8, 9), True, True)]
241243
242244
DIMACS format output::
243245
246+
sage: # optional - pycryptosat
244247
sage: from sage.sat.solvers import CryptoMiniSat
245-
sage: solver = CryptoMiniSat() # optional - pycryptosat
246-
sage: solver.add_clause((1, 2, 4)) # optional - pycryptosat
247-
sage: solver.add_clause((1, 2, -4)) # optional - pycryptosat
248-
sage: fn = tmp_filename() # optional - pycryptosat
249-
sage: solver.clauses(fn) # optional - pycryptosat
250-
sage: print(open(fn).read()) # optional - pycryptosat
248+
sage: solver = CryptoMiniSat()
249+
sage: solver.add_clause((1, 2, 4))
250+
sage: solver.add_clause((1, 2, -4))
251+
sage: fn = tmp_filename()
252+
sage: solver.clauses(fn)
253+
sage: print(open(fn).read())
251254
p cnf 4 2
252255
1 2 4 0
253256
1 2 -4 0

‎src/sage/sat/solvers/dimacs.py

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -490,14 +490,14 @@ def __call__(self, assumptions=None):
490490
TESTS::
491491
492492
sage: from sage.sat.boolean_polynomials import solve as solve_sat
493-
sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # optional - sage.rings.finite_rings sage.rings.polynomial.pbori
494-
sage: while True: # workaround (see :trac:`31891`) # optional - sage.rings.finite_rings sage.rings.polynomial.pbori
493+
sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # needs sage.rings.finite_rings sage.rings.polynomial.pbori
494+
sage: while True: # workaround (see :trac:`31891`) # needs sage.rings.finite_rings sage.rings.polynomial.pbori
495495
....: try:
496496
....: F, s = sr.polynomial_system()
497497
....: break
498498
....: except ZeroDivisionError:
499499
....: pass
500-
sage: solve_sat(F, solver=sage.sat.solvers.RSat) # optional - RSat # optional - sage.rings.finite_rings sage.rings.polynomial.pbori
500+
sage: solve_sat(F, solver=sage.sat.solvers.RSat) # optional - rsat, needs sage.rings.finite_rings sage.rings.polynomial.pbori
501501
502502
"""
503503
if assumptions is not None:

‎src/sage/sat/solvers/picosat.py

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -147,12 +147,13 @@ def __call__(self, assumptions=None):
147147
148148
EXAMPLES::
149149
150+
sage: # optional - pycosat
150151
sage: from sage.sat.solvers.picosat import PicoSAT
151-
sage: solver = PicoSAT() # optional - pycosat
152-
sage: solver.add_clause((1,2)) # optional - pycosat
153-
sage: solver.add_clause((-1,2)) # optional - pycosat
154-
sage: solver.add_clause((-1,-2)) # optional - pycosat
155-
sage: solver() # optional - pycosat
152+
sage: solver = PicoSAT()
153+
sage: solver.add_clause((1,2))
154+
sage: solver.add_clause((-1,2))
155+
sage: solver.add_clause((-1,-2))
156+
sage: solver()
156157
(None, False, True)
157158
158159
sage: solver.add_clause((1,-2)) # optional - pycosat
@@ -207,13 +208,14 @@ def clauses(self, filename=None):
207208
208209
DIMACS format output::
209210
211+
sage: # optional - pycosat
210212
sage: from sage.sat.solvers.picosat import PicoSAT
211-
sage: solver = PicoSAT() # optional - pycosat
212-
sage: solver.add_clause((1, 2, 4)) # optional - pycosat
213-
sage: solver.add_clause((1, 2, -4)) # optional - pycosat
214-
sage: fn = tmp_filename() # optional - pycosat
215-
sage: solver.clauses(fn) # optional - pycosat
216-
sage: print(open(fn).read()) # optional - pycosat
213+
sage: solver = PicoSAT()
214+
sage: solver.add_clause((1, 2, 4))
215+
sage: solver.add_clause((1, 2, -4))
216+
sage: fn = tmp_filename()
217+
sage: solver.clauses(fn)
218+
sage: print(open(fn).read())
217219
p cnf 4 2
218220
1 2 4 0
219221
1 2 -4 0

‎src/sage/sat/solvers/satsolver.pyx

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -139,9 +139,9 @@ cdef class SatSolver:
139139
140140
sage: from io import StringIO
141141
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")
142-
sage: from sage.sat.solvers.sat_lp import SatLP # optional - sage.numerical.mip
143-
sage: solver = SatLP() # optional - sage.numerical.mip
144-
sage: solver.read(file_object) # optional - sage.numerical.mip
142+
sage: from sage.sat.solvers.sat_lp import SatLP # needs sage.numerical.mip
143+
sage: solver = SatLP() # needs sage.numerical.mip
144+
sage: solver.read(file_object) # needs sage.numerical.mip
145145
Traceback (most recent call last):
146146
...
147147
NotImplementedError: the solver "an ILP-based SAT Solver" does not support xor clauses
@@ -339,7 +339,7 @@ def SAT(solver=None, *args, **kwds):
339339
340340
EXAMPLES::
341341
342-
sage: SAT(solver="LP") # optional - sage.numerical.mip
342+
sage: SAT(solver="LP") # needs sage.numerical.mip
343343
an ILP-based SAT Solver
344344
345345
TESTS::

0 commit comments

Comments
 (0)