@@ -14,10 +14,10 @@ def __init__(self, r, random_seed=16):
14
14
15
15
def zero_blocks (self , f ):
16
16
"""divides the zero set of f into blocks
17
- >>> from sage.rings.polynomial.pbori.brial import *
18
- >>> r = declare_ring(["x", "y", "z"], dict())
19
- >>> e = CNFEncoder(r)
20
- >>> e.zero_blocks(r.variable(0)*r.variable(1)*r.variable(2))
17
+ sage: from sage.rings.polynomial.pbori.brial import *
18
+ sage: r = declare_ring(["x", "y", "z"], dict())
19
+ sage: e = CNFEncoder(r)
20
+ sage: e.zero_blocks(r.variable(0)*r.variable(1)*r.variable(2))
21
21
[{y: 0}, {z: 0}, {x: 0}]
22
22
"""
23
23
f = Polynomial (f )
@@ -78,17 +78,17 @@ def get_val(var):
78
78
79
79
def clauses (self , f ):
80
80
"""
81
- >>> from sage.rings.polynomial.pbori.brial import *
82
- >>> r = declare_ring(["x", "y", "z"], dict())
83
- >>> e = CNFEncoder(r)
84
- >>> e.clauses(r.variable(0)*r.variable(1)*r.variable(2)) # doctest:+ELLIPSIS
81
+ sage: from sage.rings.polynomial.pbori.brial import *
82
+ sage: r = declare_ring(["x", "y", "z"], dict())
83
+ sage: e = CNFEncoder(r)
84
+ sage: e.clauses(r.variable(0)*r.variable(1)*r.variable(2)) # doctest:+ELLIPSIS
85
85
[{...x: 0...}]
86
- >>> e.clauses(r.variable(1)+r.variable(0)) # doctest:+ELLIPSIS
86
+ sage: e.clauses(r.variable(1)+r.variable(0)) # doctest:+ELLIPSIS
87
87
[{...x: 1...}, {...y: 1...}]
88
88
89
- >>> [sorted(c.iteritems()) for c in e.clauses(r.variable(0)*r.variable(1)*r.variable(2))]
89
+ sage: [sorted(c.iteritems()) for c in e.clauses(r.variable(0)*r.variable(1)*r.variable(2))]
90
90
[[(z, 0), (y, 0), (x, 0)]]
91
- >>> [sorted(c.iteritems()) for c in e.clauses(r.variable(1)+r.variable(0))]
91
+ sage: [sorted(c.iteritems()) for c in e.clauses(r.variable(1)+r.variable(0))]
92
92
[[(y, 1), (x, 0)], [(y, 0), (x, 1)]]
93
93
"""
94
94
f_plus_one = f + 1
@@ -102,14 +102,14 @@ def clauses(self, f):
102
102
103
103
def polynomial_clauses (self , f ):
104
104
"""
105
- >>> from sage.rings.polynomial.pbori.brial import *
106
- >>> r = declare_ring(["x", "y", "z"], dict())
107
- >>> e = CNFEncoder(r)
108
- >>> e.polynomial_clauses(r.variable(0)*r.variable(1)*r.variable(2))
105
+ sage: from sage.rings.polynomial.pbori.brial import *
106
+ sage: r = declare_ring(["x", "y", "z"], dict())
107
+ sage: e = CNFEncoder(r)
108
+ sage: e.polynomial_clauses(r.variable(0)*r.variable(1)*r.variable(2))
109
109
[x*y*z]
110
- >>> v = r.variable
111
- >>> p = v(1)*v(2)+v(2)*v(0)+1
112
- >>> groebner_basis([p], heuristic = False)==groebner_basis(e.polynomial_clauses(p), heuristic = False)
110
+ sage: v = r.variable
111
+ sage: p = v(1)*v(2)+v(2)*v(0)+1
112
+ sage: groebner_basis([p], heuristic = False)==groebner_basis(e.polynomial_clauses(p), heuristic = False)
113
113
True
114
114
"""
115
115
@@ -141,11 +141,11 @@ def get_sign(val):
141
141
142
142
def dimacs_encode_polynomial (self , p ):
143
143
"""
144
- >>> from sage.rings.polynomial.pbori.brial import *
145
- >>> d=dict()
146
- >>> r = declare_ring(["x", "y", "z"], d)
147
- >>> e = CNFEncoder(r)
148
- >>> e.dimacs_encode_polynomial(d["x"]+d["y"]+d["z"])
144
+ sage: from sage.rings.polynomial.pbori.brial import *
145
+ sage: d=dict()
146
+ sage: r = declare_ring(["x", "y", "z"], d)
147
+ sage: e = CNFEncoder(r)
148
+ sage: e.dimacs_encode_polynomial(d["x"]+d["y"]+d["z"])
149
149
['1 2 -3 0', '1 -2 3 0', '-1 -2 -3 0', '-1 2 3 0']
150
150
"""
151
151
clauses = self .clauses (p )
@@ -156,14 +156,14 @@ def dimacs_encode_polynomial(self, p):
156
156
157
157
def dimacs_cnf (self , polynomial_system ):
158
158
r"""
159
- >>> from sage.rings.polynomial.pbori.brial import *
160
- >>> r = declare_ring(["x", "y", "z"], dict())
161
- >>> e = CNFEncoder(r)
162
- >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
159
+ sage: from sage.rings.polynomial.pbori.brial import *
160
+ sage: r = declare_ring(["x", "y", "z"], dict())
161
+ sage: e = CNFEncoder(r)
162
+ sage: e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
163
163
'c cnf generated by PolyBoRi\np cnf 3 1\n-1 -2 -3 0'
164
- >>> e.dimacs_cnf([r.variable(1)+r.variable(0)])
164
+ sage: e.dimacs_cnf([r.variable(1)+r.variable(0)])
165
165
'c cnf generated by PolyBoRi\np cnf 3 2\n1 -2 0\n-1 2 0'
166
- >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
166
+ sage: e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
167
167
'c cnf generated by PolyBoRi\np cnf 3 3\n-1 -2 -3 0\n-1 2 0\n1 -2 0'
168
168
"""
169
169
clauses_list = [c for p in polynomial_system for c in self .
@@ -182,18 +182,18 @@ class CryptoMiniSatEncoder(CNFEncoder):
182
182
183
183
def dimacs_encode_polynomial (self , p ):
184
184
r"""
185
- >>> from sage.rings.polynomial.pbori.brial import *
186
- >>> d=dict()
187
- >>> r = declare_ring(["x", "y", "z"], d)
188
- >>> e = CryptoMiniSatEncoder(r)
189
- >>> p = d["x"]+d["y"]+d["z"]
190
- >>> p.deg()
185
+ sage: from sage.rings.polynomial.pbori.brial import *
186
+ sage: d=dict()
187
+ sage: r = declare_ring(["x", "y", "z"], d)
188
+ sage: e = CryptoMiniSatEncoder(r)
189
+ sage: p = d["x"]+d["y"]+d["z"]
190
+ sage: p.deg()
191
191
1
192
- >>> len(p)
192
+ sage: len(p)
193
193
3
194
- >>> e.dimacs_encode_polynomial(p)
194
+ sage: e.dimacs_encode_polynomial(p)
195
195
['x1 2 3 0\nc g 1 x + y + z']
196
- >>> e.dimacs_encode_polynomial(p+1)
196
+ sage: e.dimacs_encode_polynomial(p+1)
197
197
['x1 2 -3 0\nc g 2 x + y + z + 1']
198
198
"""
199
199
if p .deg () != 1 or len (p ) <= 1 :
@@ -216,14 +216,14 @@ def dimacs_encode_polynomial(self, p):
216
216
217
217
def dimacs_cnf (self , polynomial_system ):
218
218
r"""
219
- >>> from sage.rings.polynomial.pbori.brial import *
220
- >>> r = declare_ring(["x", "y", "z"], dict())
221
- >>> e = CryptoMiniSatEncoder(r)
222
- >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
219
+ sage: from sage.rings.polynomial.pbori.brial import *
220
+ sage: r = declare_ring(["x", "y", "z"], dict())
221
+ sage: e = CryptoMiniSatEncoder(r)
222
+ sage: e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
223
223
'c cnf generated by PolyBoRi\np cnf 3 1\n-1 -2 -3 0\nc g 1 x*y*z\nc v 1 x\nc v 2 y\nc v 3 z'
224
- >>> e.dimacs_cnf([r.variable(1)+r.variable(0)])
224
+ sage: e.dimacs_cnf([r.variable(1)+r.variable(0)])
225
225
'c cnf generated by PolyBoRi\np cnf 3 1\nx1 2 0\nc g 2 x + y\nc v 1 x\nc v 2 y'
226
- >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
226
+ sage: e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
227
227
'c cnf generated by PolyBoRi\np cnf 3 2\n-1 -2 -3 0\nc g 3 x*y*z\nx1 2 0\nc g 4 x + y\nc v 1 x\nc v 2 y\nc v 3 z'
228
228
"""
229
229
uv = list (used_vars_set (polynomial_system ).variables ())
0 commit comments