Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
sagemath
GitHub Repository: sagemath/sagelib
Path: blob/master/sage/interfaces/qepcad.py
4076 views
1
r"""
2
Interface to QEPCAD
3
4
The basic function of QEPCAD is to construct cylindrical algebraic
5
decompositions (CADs) of $\RR^k$, given a list of polynomials. Using
6
this CAD, it is possible to perform quantifier elimination and formula
7
simplification.
8
9
A CAD for a set $A$ of $k$-variate polynomials decomposes $\RR^j$ into
10
disjoint cells, for each $j$ in $0 \leq j \leq k$. The sign of each
11
polynomial in $A$ is constant in each cell of $\RR^k$, and for each
12
cell in $\RR^j$ ($j > 1$), the projection of that cell into
13
$\RR^{j-1}$ is a cell of $\RR^{j-1}$. (This property makes the
14
decomposition ``cylindrical''.)
15
16
Given a formula $\exists x. P(a,b,x) = 0$ (for a polynomial $P$), and
17
a cylindrical algebraic decomposition for $P$, we can eliminate the
18
quantifier (find an equivalent formula in the two variables $a$, $b$
19
without the quantifier $\exists$) as follows. For each cell $C$ in
20
$\RR^2$, find the cells of $\RR^3$ which project to $C$. (This
21
collection is called the \emph{stack} over $C$.) Mark $C$ as true if
22
some member of the stack has sign $= 0$; otherwise, mark $C$ as false.
23
Then, construct a polynomial formula in $a$, $b$ which specifies
24
exactly the true cells (this is always possible). The same technique
25
works if the body of the quantifier is any boolean combination of
26
polynomial equalities and inequalities.
27
28
Formula simplification is a similar technique. Given a formula which
29
describes a simple set of $\RR^k$ in a complicated way as a boolean
30
combination of polynomial equalities and inequalities, QEPCAD can
31
construct a CAD for the polynomials and recover a simple equivalent
32
formula.
33
34
Note that while the following documentation is tutorial in nature, and
35
is written for people who may not be familiar with QEPCAD, it is
36
documentation for the \sage interface rather than for QEPCAD. As
37
such, it does not cover several issues that are very important to use
38
QEPCAD efficiently, such as variable ordering, the efficient use of
39
the alternate quantifiers and \code{_root_} expressions, the
40
\code{measure-zero-error} command, etc. For more information on
41
QEPCAD, see the online documentation at
42
\url{http://www.cs.usna.edu/~qepcad/B/QEPCAD.html} and Chris Brown's
43
tutorial handout and slides from
44
\url{http://www.cs.usna.edu/~wcbrown/research/ISSAC04/Tutorial.html}.
45
(Several of the examples in this documentation came from these
46
sources.)
47
48
The examples below require that the optional qepcad package is installed.
49
50
QEPCAD can be run in a fully automatic fashion, or interactively.
51
We first demonstrate the automatic use of QEPCAD.
52
53
Since \sage has no built-in support for quantifiers, this interface
54
provides \code{qepcad_formula} which helps construct quantified
55
formulas in the syntax QEPCAD requires. ::
56
57
sage: var('a,b,c,d,x,y,z')
58
(a, b, c, d, x, y, z)
59
sage: qf = qepcad_formula
60
61
We start with a simple example. Consider an arbitrarily-selected
62
ellipse::
63
64
sage: ellipse = 3*x^2 + 2*x*y + y^2 - x + y - 7
65
66
What is the projection onto the $x$ axis of this ellipse? First we
67
construct a formula asking this question. ::
68
69
sage: F = qf.exists(y, ellipse == 0); F
70
(E y)[3 x^2 + 2 x y + y^2 - x + y - 7 = 0]
71
72
Then we run qepcad to get the answer::
73
74
sage: qepcad(F) # optional - qepcad
75
8 x^2 - 8 x - 29 <= 0
76
77
How about the projection onto the $y$ axis? ::
78
79
sage: qepcad(qf.exists(x, ellipse == 0)) # optional - qepcad
80
8 y^2 + 16 y - 85 <= 0
81
82
QEPCAD deals with more quantifiers than just ``exists'', of course.
83
Besides the standard ``forall'', there are also ``for infinitely
84
many'', ``for all but finitely many'', ``for a connected subset'', and
85
``for exactly $k$''. The \function{qepcad} documentation has examples
86
of all of these; here we'll just give one example.
87
88
First we construct a circle::
89
90
sage: circle = x^2 + y^2 - 3
91
92
For what values $k$ does a vertical line $x=k$ intersect the combined
93
figure of the circle and ellipse exactly three times? ::
94
95
sage: F = qf.exactly_k(3, y, circle * ellipse == 0); F # optional - qepcad
96
(X3 y)[(x^2 + y^2 - 3) (3 x^2 + 2 x y + y^2 - x + y - 7) = 0]
97
sage: qepcad(F) # optional - qepcad
98
8 x^2 - 8 x - 29 <= 0 /\ x^2 - 3 <= 0 /\ 8 x^4 - 26 x^2 - 4 x + 13 >= 0 /\ [ 8 x^4 - 26 x^2 - 4 x + 13 = 0 \/ x^2 - 3 = 0 \/ 8 x^2 - 8 x - 29 = 0 ]
99
100
Here we see that the solutions are among the eight ($4 + 2 + 2$) roots
101
of the three polynomials inside the brackets, but not all of these
102
roots are solutions; the polynomial inequalities outside the brackets
103
are needed to select those roots that are solutions.
104
105
QEPCAD also supports an extended formula language, where
106
$\mbox{_root_}k \quad P(\bar x, y)$ refers to a particular zero of
107
$P(\bar x, y)$ (viewed as a polynomial in $y$). If there are $n$ roots,
108
then _root_$1$ refers to the least root and _root_$n$ refers to the greatest;
109
also, _root_$-n$ refers to the least root and _root_$-1$ refers to the
110
greatest.
111
112
This extended language is available both on input and output; see the
113
QEPCAD documentation for more information on how to use this syntax on
114
input. We can request output that's intended to be easy to interpret
115
geometrically; then QEPCAD will use the extended language to produce
116
a solution formula without the selection polynomials. ::
117
118
sage: qepcad(F, solution='geometric') # optional - qepcad
119
x = _root_1 8 x^2 - 8 x - 29
120
\/
121
8 x^4 - 26 x^2 - 4 x + 13 = 0
122
\/
123
x = _root_-1 x^2 - 3
124
125
We then see that the 6 solutions correspond to the vertical tangent on
126
the left side of the ellipse, the four intersections between the
127
ellipse and the circle, and the vertical tangent on the right side of
128
the circle.
129
130
Let's do some basic formula simplification and visualization.
131
We'll look at the region which is inside both the ellipse and the circle::
132
133
sage: F = qf.and_(ellipse < 0, circle < 0); F # optional - qepcad
134
[3 x^2 + 2 x y + y^2 - x + y - 7 < 0 /\ x^2 + y^2 - 3 < 0]
135
sage: qepcad(F) # optional - qepcad
136
y^2 + 2 x y + y + 3 x^2 - x - 7 < 0 /\ y^2 + x^2 - 3 < 0
137
138
We get back the same formula we put in. This is not surprising (we
139
started with a pretty simple formula, after all), but it's not very
140
enlightening either. Again, if we ask for a 'geometric' output, then we see
141
an output that lets us understand something about the shape of the solution
142
set. ::
143
144
sage: qepcad(F, solution='geometric') # optional - qepcad
145
[
146
[
147
x = _root_-2 8 x^4 - 26 x^2 - 4 x + 13
148
\/
149
x = _root_2 8 x^4 - 26 x^2 - 4 x + 13
150
\/
151
8 x^4 - 26 x^2 - 4 x + 13 < 0
152
]
153
/\
154
y^2 + 2 x y + y + 3 x^2 - x - 7 < 0
155
/\
156
y^2 + x^2 - 3 < 0
157
]
158
\/
159
[
160
x > _root_2 8 x^4 - 26 x^2 - 4 x + 13
161
/\
162
x < _root_-2 8 x^4 - 26 x^2 - 4 x + 13
163
/\
164
y^2 + x^2 - 3 < 0
165
]
166
167
There's another reason to prefer output using _root_ expressions; not
168
only does it sometimes give added insight into the geometric
169
structure, it also can be more efficient to construct. Consider this
170
formula for the projection of a particular semicircle onto the $x$
171
axis::
172
173
sage: F = qf.exists(y, qf.and_(circle == 0, x + y > 0)); F # optional - qepcad
174
(E y)[x^2 + y^2 - 3 = 0 /\ x + y > 0]
175
sage: qepcad(F) # optional - qepcad
176
x^2 - 3 <= 0 /\ [ x > 0 \/ 2 x^2 - 3 < 0 ]
177
178
Here, the formula $x > 0$ had to be introduced in order to get a
179
solution formula; the original CAD of F did not include the
180
polynomial $x$. To avoid having QEPCAD do the extra work to come up
181
with a solution formula, we can tell it to use the extended language;
182
it's always possible to construct a solution formula in the extended
183
language without introducing new polynomials. ::
184
185
sage: qepcad(F, solution='extended') # optional - qepcad
186
x^2 - 3 <= 0 /\ x > _root_1 2 x^2 - 3
187
188
Up to this point, all the output we've seen has basically been in the
189
form of strings; there is no support (yet) for parsing these outputs
190
back into \sage polynomials (partly because \sage does not yet have
191
support for symbolic conjunctions and disjunctions). The function
192
\function{qepcad} supports three more output types that give numbers which
193
can be manipulated in \sage: any-point, all-points, and cell-points.
194
195
These output types give dictionaries mapping variable names to values.
196
With any-point, \function{qepcad} either produces a single dictionary
197
specifying a point where the formula is true, or raises an exception
198
if the formula is false everywhere. With all-points,
199
\function{qepcad} either produces a list of dictionaries for all
200
points where the formula is true, or raises an exception if the
201
formula is true on infinitely many points. With cell-points,
202
\function{qepcad} produces a list of dictionaries with one point for
203
each cell where the formula is true. (This means you will have at least
204
one point in each connected component of the solution, although you will
205
often have many more points than that.)
206
207
Let's revisit some of the above examples and get some points to play
208
with. We'll start by finding a point on our ellipse. ::
209
210
sage: p = qepcad(ellipse == 0, solution='any-point'); p # optional - qepcad
211
{'y': 0.9685019685029527?, 'x': -1.468501968502953?}
212
213
(Note that despite the decimal printing and the question marks, these
214
are really exact numbers.)
215
216
We can verify that this point is a solution. To do so, we create
217
a copy of ellipse as a polynomial over QQ (instead of a symbolic
218
expression). ::
219
220
sage: pellipse = QQ['x,y'](ellipse) # optional - qepcad
221
sage: pellipse(**p) == 0 # optional - qepcad
222
True
223
224
For cell-points, let's look at points \emph{not} on the ellipse. ::
225
226
sage: pts = qepcad(ellipse != 0, solution='cell-points'); pts # optional - qepcad
227
[{'y': 0, 'x': 4}, {'y': 1, 'x': 2.468501968502953?}, {'y': -9, 'x': 2.468501968502953?}, {'y': 9, 'x': 1/2}, {'y': -1, 'x': 1/2}, {'y': -5, 'x': 1/2}, {'y': 3, 'x': -1.468501968502953?}, {'y': -1, 'x': -1.468501968502953?}, {'y': 0, 'x': -3}]
228
229
For the points here which are in full-dimensional cells, QEPCAD has the
230
freedom to choose rational sample points, and it does so.
231
232
And, of course, all these points really are not on the ellipse. ::
233
234
sage: [pellipse(**p) != 0 for p in pts] # optional - qepcad
235
[True, True, True, True, True, True, True, True, True]
236
237
Finally, for all-points, let's look again at finding vertical lines that
238
intersect the union of the circle and the ellipse exactly three times. ::
239
240
sage: F = qf.exactly_k(3, y, circle * ellipse == 0); F # optional - qepcad
241
(X3 y)[(x^2 + y^2 - 3) (3 x^2 + 2 x y + y^2 - x + y - 7) = 0]
242
sage: pts = qepcad(F, solution='all-points'); pts # optional - qepcad
243
[{'x': 1.732050807568878?}, {'x': 1.731054913462534?}, {'x': 0.678911384208004?}, {'x': -0.9417727377417167?}, {'x': -1.468193559928821?}, {'x': -1.468501968502953?}]
244
245
Since $y$ is bound by the quantifier, the solutions only refer to $x$.
246
247
We can substitute one of these solutions into the original equation::
248
249
sage: pt = pts[0] # optional - qepcad
250
sage: pcombo = QQ['x,y'](circle * ellipse) # optional - qepcad
251
sage: intersections = pcombo(y=polygen(AA, 'y'), **pt); intersections # optional - qepcad
252
y^4 + 4.464101615137755?*y^3 + 0.2679491924311227?*y^2
253
254
and verify that it does have three roots::
255
256
sage: intersections.roots() # optional - qepcad
257
[(-4.403249005600958?, 1), (-0.06085260953679653?, 1), (0, 2)]
258
259
Let's check all six solutions. ::
260
261
sage: [len(pcombo(y=polygen(AA, 'y'), **p).roots()) for p in pts] # optional - qepcad
262
[3, 3, 3, 3, 3, 3]
263
264
We said earlier that we can run QEPCAD either automatically or
265
interactively. Now that we've discussed the automatic modes, let's turn
266
to interactive uses.
267
268
If the \function{qepcad} function is passed \code{interact=True}, then
269
instead of returning a result, it returns an object of class
270
\class{Qepcad} representing a running instance of QEPCAD that you can
271
interact with. For example::
272
273
sage: qe = qepcad(qf.forall(x, x^2 + b*x + c > 0), interact=True); qe # optional - qepcad
274
QEPCAD object in phase 'Before Normalization'
275
276
This object is a fairly thin wrapper over QEPCAD; most QEPCAD commands
277
are available as methods on the \class{Qepcad} object. Given a
278
\class{Qepcad} object \var{qe}, you can type \code{qe.[tab]} to see
279
the available QEPCAD commands; to see the documentation for an
280
individual QEPCAD command, for example \code{d_setting}, you can type
281
\code{qe.d_setting?}. (In QEPCAD, this command is called
282
\code{d-setting}; we systematically replace hyphens with underscores
283
for this interface.)
284
285
The execution of QEPCAD is divided into four phases; most commands are
286
not available during all phases. We saw above that QEPCAD starts out
287
in phase `Before Normalization'; we see that the \code{d_cell} command
288
is not available in this phase::
289
290
sage: qe.d_cell() # optional - qepcad
291
Error GETCID: This command is not active here.
292
293
We will focus here on the fourth (and last) phase, `Before Solution',
294
because this interface has special support for some operations in this
295
phase. Consult the QEPCAD documentation for information on the other
296
phases.
297
298
We can tell QEPCAD to finish off the current phase and move to the
299
next with its \code{go} command. (There is also the \code{step}
300
command, which partially completes a phase for phases that have
301
multiple steps, and the \code{finish} command, which runs QEPCAD to
302
completion.) ::
303
304
sage: qe.go() # optional - qepcad
305
QEPCAD object has moved to phase 'Before Projection (x)'
306
sage: qe.go() # optional - qepcad
307
QEPCAD object has moved to phase 'Before Choice'
308
sage: qe.go() # optional - qepcad
309
QEPCAD object has moved to phase 'Before Solution'
310
311
Note that the \class{Qepcad} object returns the new phase whenever the
312
phase changes, as a convenience for interactive use; except that when
313
the new phase is `EXITED', the solution formula printed by QEPCAD is
314
returned instead. ::
315
316
sage: qe.go() # optional - qepcad
317
4 c - b^2 > 0
318
sage: qe # optional - qepcad
319
QEPCAD object in phase 'EXITED'
320
321
Let's pick a nice, simple example, return to phase 4, and explore the
322
resulting \var{qe} object. ::
323
324
sage: qe = qepcad(circle == 0, interact=True); qe # optional - qepcad
325
QEPCAD object in phase 'Before Normalization'
326
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
327
QEPCAD object has moved to phase 'Before Projection (y)'
328
QEPCAD object has moved to phase 'Before Choice'
329
QEPCAD object has moved to phase 'Before Solution'
330
331
We said before that QEPCAD creates ``cylindrical algebraic
332
decompositions''; since we have a bivariate polynomial, we get
333
decompositions of $\RR^0$, $\RR^1$, and $\RR^2$. In this case, where
334
our example is a circle of radius $\sqrt{3}$ centered on the origin,
335
these decompositions are as follows:
336
337
The decomposition of $\RR^0$ is trivial (of course). The
338
decomposition of $\RR^1$ has five cells: $x < -\sqrt{3}$, $x =
339
-\sqrt{3}$, $-\sqrt{3} < x < \sqrt{3}$, $x = \sqrt{3}$, and $x >
340
\sqrt{3}$. These five cells comprise the \emph{stack} over the single
341
cell in the trivial decomposition of $\RR^0$.
342
343
These five cells give rise to five stacks in $\RR^2$. The first and
344
fifth stack have just one cell apiece. The second and fourth stacks
345
have three cells: $y < 0$, $y = 0$, and $y > 0$. The third stack has
346
five cells: below the circle, the lower semicircle, the interior of
347
the circle, the upper semicircle, and above the circle.
348
349
QEPCAD (and this QEPCAD interface) number the cells in a stack
350
starting with 1. Each cell has an \emph{index}, which is a tuple of
351
integers describing the path to the cell in the tree of all cells.
352
For example, the cell ``below the circle'' has index (3,1) (the first
353
cell in the stack over the third cell of $\RR^1$) and the interior of
354
the circle has index (3,3).
355
356
We can view these cells with the QEPCAD command \code{d_cell}. For
357
instance, let's look at the cell for the upper semicircle::
358
359
sage: qe.d_cell(3, 4) # optional - qepcad
360
---------- Information about the cell (3,4) ----------
361
Level : 2
362
Dimension : 1
363
Number of children : 0
364
Truth value : T by trial evaluation.
365
Degrees after substitution : Not known yet or No polynomial.
366
Multiplicities : ((1,1))
367
Signs of Projection Factors
368
Level 1 : (-)
369
Level 2 : (0)
370
---------- Sample point ----------
371
The sample point is in a PRIMITIVE representation.
372
<BLANKLINE>
373
alpha = the unique root of x^2 - 3 between 0 and 4
374
= 1.7320508076-
375
<BLANKLINE>
376
Coordinate 1 = 0
377
= 0.0000000000
378
Coordinate 2 = alpha
379
= 1.7320508076-
380
----------------------------------------------------
381
382
We see that, the level of this cell is 2, meaning that it is part of
383
the decomposition of $\RR^2$. The dimension is 1, meaning that the
384
cell is homeomorphic to a line (rather than a plane or a point). The
385
sample point gives the coordinates of one point in the cell, both
386
symbolically and numerically.
387
388
For programmatic access to cells, we've defined a \sage wrapper class
389
\class{QepcadCell}. These cells can be created with the \method{cell}
390
method; for example::
391
392
sage: c = qe.cell(3, 4); c # optional - qepcad
393
QEPCAD cell (3, 4)
394
395
A \class{QepcadCell} has accessor methods for the important state held
396
within a cell. For instance::
397
398
sage: c.level() # optional - qepcad
399
2
400
sage: c.index() # optional - qepcad
401
(3, 4)
402
sage: qe.cell(3).number_of_children() # optional - qepcad
403
5
404
sage: len(qe.cell(3)) # optional - qepcad
405
5
406
407
One particularly useful thing we can get from a cell is its sample point,
408
as \sage algebraic real numbers. ::
409
410
sage: c.sample_point() # optional - qepcad
411
(0, 1.732050807568878?)
412
sage: c.sample_point_dict() # optional - qepcad
413
{'y': 1.732050807568878?, 'x': 0}
414
415
We've seen that we can get cells using the \method{cell} method.
416
There are several QEPCAD commands that print lists of cells; we can
417
also get cells using the \method{make_cells} method, passing it the
418
output of one of these commands. ::
419
420
sage: qe.make_cells(qe.d_true_cells()) # optional - qepcad
421
[QEPCAD cell (4, 2), QEPCAD cell (3, 4), QEPCAD cell (3, 2), QEPCAD cell (2, 2)]
422
423
Also, the cells in the stack over a given cell can be accessed using
424
array subscripting or iteration. (Remember that cells in a stack are
425
numbered starting with one; we preserve this convention in the
426
array-subscripting syntax.) ::
427
428
sage: c = qe.cell(3) # optional - qepcad
429
sage: c[1] # optional - qepcad
430
QEPCAD cell (3, 1)
431
sage: [c2 for c2 in c] # optional - qepcad
432
[QEPCAD cell (3, 1), QEPCAD cell (3, 2), QEPCAD cell (3, 3), QEPCAD cell (3, 4), QEPCAD cell (3, 5)]
433
434
We can do one more thing with a cell: we can set its truth value.
435
Once the truth values of the cells have been set, we can get QEPCAD to
436
produce a formula which is true in exactly the cells we have selected.
437
This is useful if QEPCAD's quantifier language is insufficient to
438
express your problem.
439
440
For example, consider again our combined figure of the circle and the
441
ellipse. Suppose you want to find all vertical lines that intersect
442
the circle twice, and also intersect the ellipse twice. The vertical
443
lines that intersect the circle twice can be found by simplifying::
444
445
sage: F = qf.exactly_k(2, y, circle == 0); F # optional - qepcad
446
(X2 y)[x^2 + y^2 - 3 = 0]
447
448
and the vertical lines that intersect the ellipse twice are expressed by::
449
450
sage: G = qf.exactly_k(2, y, ellipse == 0); G # optional - qepcad
451
(X2 y)[3 x^2 + 2 x y + y^2 - x + y - 7 = 0]
452
453
and the lines that intersect both figures would be::
454
455
sage: qf.and_(F, G) # optional - qepcad
456
Traceback (most recent call last):
457
...
458
ValueError: QEPCAD formulas must be in prenex (quantifiers outermost) form
459
460
...except that QEPCAD does not support formulas like this; in QEPCAD
461
input, all logical connectives must be inside all quantifiers.
462
463
Instead, we can get QEPCAD to construct a CAD for our combined figure
464
and set the truth values ourselves. (The exact formula we use doesn't
465
matter, since we're going to replace the truth values in the cells; we
466
just need to use a formula that uses both polynomials.) ::
467
468
sage: qe = qepcad(qf.and_(ellipse == 0, circle == 0), interact=True) # optional - qepcad
469
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
470
QEPCAD object has moved to phase 'Before Projection (y)'
471
QEPCAD object has moved to phase 'Before Choice'
472
QEPCAD object has moved to phase 'Before Solution'
473
474
Now we want to find all cells $c$ in the decomposition of $\RR^1$ such
475
that the stack over $c$ contains exactly two cells on the ellipse, and
476
also contains exactly two cells on the circle.
477
478
Our input polynomials are ``level-2 projection factors'', we see::
479
480
sage: qe.d_proj_factors() # optional - qepcad
481
P_1,1 = fac(J_1,1) = fac(dis(A_2,1))
482
= 8 x^2 - 8 x - 29
483
P_1,2 = fac(J_1,2) = fac(dis(A_2,2))
484
= x^2 - 3
485
P_1,3 = fac(J_1,3) = fac(res(A_2,1|A_2,2))
486
= 8 x^4 - 26 x^2 - 4 x + 13
487
A_2,1 = input
488
= y^2 + 2 x y + y + 3 x^2 - x - 7
489
A_2,2 = input
490
= y^2 + x^2 - 3
491
492
so we can test whether a cell is on the ellipse by checking that the
493
sign of the corresponding projection factor is 0 in our cell.
494
For instance, the cell (12,2) is on the ellipse::
495
496
sage: qe.cell(12,2).signs()[1][0] # optional - qepcad
497
0
498
499
So we can update the truth values as desired like this::
500
501
sage: for c in qe.cell(): # optional - qepcad
502
... count_ellipse = 0 # optional - qepcad
503
... count_circle = 0 # optional - qepcad
504
... for c2 in c: # optional - qepcad
505
... count_ellipse += (c2.signs()[1][0] == 0) # optional - qepcad
506
... count_circle += (c2.signs()[1][1] == 0) # optional - qepcad
507
... c.set_truth(count_ellipse == 2 and count_circle == 2) # optional - qepcad
508
509
and then we can get our desired solution formula. (The 'G' stands for
510
'geometric', and gives solutions using the same rules as
511
\code{solution='geometric'} described above.) ::
512
513
sage: qe.solution_extension('G') # optional - qepcad
514
8 x^2 - 8 x - 29 < 0
515
/\
516
x^2 - 3 < 0
517
518
AUTHORS:
519
520
- Carl Witty (2008-03): initial version
521
"""
522
523
#*****************************************************************************
524
# Copyright (C) 2008 Carl Witty <[email protected]>
525
#
526
# Distributed under the terms of the GNU General Public License (GPL)
527
# as published by the Free Software Foundation; either version 2 of
528
# the License, or (at your option) any later version.
529
# http://www.gnu.org/licenses/
530
#*****************************************************************************
531
532
from __future__ import with_statement
533
534
import sage.misc.misc
535
import pexpect
536
import re
537
import sys
538
539
from sage.misc.flatten import flatten
540
from sage.misc.sage_eval import sage_eval
541
from sage.misc.preparser import implicit_mul
542
543
from expect import Expect, ExpectFunction, AsciiArtString
544
545
def _qepcad_cmd(memcells=None):
546
r"""
547
Construct a QEPCAD command line. Optionally set the
548
number of memory cells to use.
549
550
EXAMPLES::
551
552
sage: from sage.interfaces.qepcad import _qepcad_cmd
553
sage: _qepcad_cmd()
554
'env qe=.../local/ qepcad '
555
sage: _qepcad_cmd(memcells=8000000)
556
'env qe=.../local/ qepcad +N8000000'
557
"""
558
if memcells is not None:
559
memcells_arg = '+N%s' % memcells
560
else:
561
memcells_arg = ''
562
return "env qe=%s qepcad %s"%(sage.misc.misc.SAGE_LOCAL, memcells_arg)
563
564
_command_info_cache = None
565
566
def _update_command_info():
567
r"""
568
Read the file \file{qepcad.help} to find the list of commands
569
supported by QEPCAD. Used for tab-completion and documentation.
570
571
EXAMPLES::
572
573
sage: from sage.interfaces.qepcad import _update_command_info, _command_info_cache
574
sage: _update_command_info() # optional - qepcad
575
sage: _command_info_cache['approx_precision'] # optional - qepcad
576
('46', 'abcde', 'm', 'approx-precision N\n\nApproximate algeraic numbers to N decimal places.\n', None)
577
"""
578
global _command_info_cache
579
if _command_info_cache is not None:
580
return
581
582
cache = {}
583
584
with open('%s/bin/qepcad.help'%sage.misc.misc.SAGE_LOCAL) as help:
585
assert(help.readline().strip() == '@')
586
587
while True:
588
cmd_line = help.readline()
589
while len(cmd_line.strip()) == 0:
590
cmd_line = help.readline()
591
cmd_line = cmd_line.strip()
592
if cmd_line == '@@@':
593
break
594
595
(cmd, id, phases, kind) = cmd_line.split()
596
assert(help.readline().strip() == '@')
597
598
help_text = ''
599
help_line = help.readline()
600
while help_line.strip() != '@':
601
help_text += help_line
602
help_line = help.readline()
603
604
# I went through qepcad.help and picked out commands that
605
# I thought might be worth a little extra tweaking...
606
special = None
607
608
# These commands have been tweaked.
609
if cmd in ['d-all-cells-in-subtree', 'd-cell', 'd-pcad',
610
'd-pscad', 'd-stack', 'manual-choose-cell']:
611
special = 'cell'
612
if cmd in ['ipfzt', 'rational-sample', 'triv-convert', 'use-db',
613
'use-selected-cells-cond', 'verbose']:
614
special = 'yn'
615
616
# The tweaking for these commands has not been implemented yet.
617
if cmd in ['selected-cells-cond']:
618
special = 'formula'
619
if cmd in ['ch-pivot', 'rem-pf', 'rem-pj']:
620
special = 'i,j'
621
if cmd in ['d-2d-cad', 'set-truth-value', 'solution-extension']:
622
special = 'interactive'
623
if cmd in ['p-2d-cad', 'trace-alg', 'trace-data']:
624
special = 'optional'
625
626
cmd = cmd.replace('-', '_')
627
628
cache[cmd] = (id, phases, kind, help_text, special)
629
630
_command_info_cache = cache
631
632
_rewrote_qepcadrc = False
633
def _rewrite_qepcadrc():
634
r"""
635
Write the file \file{default.qepcadrc} to specify a path to Singular
636
(which QEPCAD uses for Gr\"obner basis computations).
637
638
EXAMPLES:
639
sage: from sage.interfaces.qepcad import _rewrite_qepcadrc
640
sage: _rewrite_qepcadrc()
641
sage: from sage.misc.misc import SAGE_LOCAL
642
sage: open('%s/default.qepcadrc'%SAGE_LOCAL).readlines()[-1]
643
'SINGULAR .../local//bin'
644
"""
645
global _rewrote_qepcadrc
646
if _rewrote_qepcadrc: return
647
648
SL = sage.misc.misc.SAGE_LOCAL
649
fn = '%s/default.qepcadrc'%SL
650
text = \
651
"""# THIS FILE IS AUTOMATICALLY GENERATED -- DO NOT EDIT
652
653
#####################################################
654
# QEPCAD rc file.
655
# This file allows for some customization of QEPCADB.
656
# Right now, the ability to give a path to Singular,
657
# so that it gets used for some computer algebra
658
# computations is the only feature.
659
#####################################################
660
SINGULAR %s/bin""" % SL
661
662
open(fn, 'w').write(text)
663
664
# QEPCAD does not have a typical "computer algebra system" interaction
665
# model. Instead, you run QEPCAD once for each problem you wish to solve,
666
# then interact with it while you solve that problem.
667
668
# For this reason, most of the methods on the Expect class are
669
# inapplicable. To avoid confusing the user with useless commands
670
# in tab completion, we split the control into two classes:
671
# Qepcad_expect is a subclass of Expect, and is never seen by the user;
672
# Qepcad is a wrapper for Qepcad_expect, and is what the user interacts with.
673
674
class Qepcad_expect(Expect):
675
r"""
676
The low-level wrapper for QEPCAD.
677
"""
678
def __init__(self, memcells=None,
679
maxread=100000,
680
logfile=None,
681
server=None):
682
r"""
683
Initialize a low-level wrapper for QEPCAD. You can specify
684
the number of memory cells that QEPCAD allocates on startup
685
(which controls the maximum problem size QEPCAD can handle),
686
and specify a logfile. You can also specify a server, and the
687
interface will run QEPCAD on that server, using ssh. (UNTESTED)
688
689
EXAMPLES::
690
691
sage: from sage.interfaces.qepcad import Qepcad_expect
692
sage: Qepcad_expect(memcells=100000, logfile=sys.stdout)
693
Qepcad
694
"""
695
_rewrite_qepcadrc()
696
Expect.__init__(self,
697
name="QEPCAD",
698
# yuck: when QEPCAD first starts,
699
# it doesn't give prompts
700
prompt="\nEnter an .*:\r",
701
command=_qepcad_cmd(memcells),
702
maxread=maxread,
703
server=server,
704
restart_on_ctrlc=False,
705
verbose_start=False,
706
logfile=logfile)
707
708
class Qepcad:
709
r"""
710
The wrapper for QEPCAD.
711
"""
712
713
def __init__(self, formula,
714
vars=None, logfile=None, verbose=False,
715
memcells=None, server=None):
716
r"""
717
Construct a QEPCAD wrapper object. Requires a formula, which
718
may be a \class{qformula} as returned by the methods of
719
\code{qepcad_formula}, a symbolic equality or inequality, a
720
polynomial $p$ (meaning $p = 0$), or a string, which is passed
721
straight to QEPCAD.
722
723
\var{vars} specifies the variables to use; this gives the variable
724
ordering, which may be very important. If \var{formula} is
725
given as a string, then \var{vars} is required; otherwise,
726
if \var{vars} is omitted, then a default ordering is used
727
(alphabetical ordering for the free variables).
728
729
A logfile can be specified with \var{logfile}.
730
If \code{verbose=True} is given, then the logfile is automatically
731
set to \code{sys.stdout}, so all QEPCAD interaction is echoed to
732
the terminal.
733
734
You can set the amount of memory that QEPCAD allocates with
735
\var{memcells}, and you can use \var{server} to run QEPCAD on
736
another machine using ssh. (UNTESTED)
737
738
Usually you will not call this directly, but use \function{qepcad}
739
to do so. Check the \function{qepcad} documentation for more
740
information.
741
742
EXAMPLES::
743
744
sage: from sage.interfaces.qepcad import Qepcad
745
sage: Qepcad(x^2 - 1 == 0) # optional - qepcad
746
QEPCAD object in phase 'Before Normalization'
747
"""
748
self._cell_cache = {}
749
750
if verbose:
751
logfile=sys.stdout
752
753
varlist = None
754
if vars is not None:
755
if isinstance(vars, str):
756
varlist = vars.strip('()').split(',')
757
else:
758
varlist = [str(v) for v in vars]
759
760
if isinstance(formula, str):
761
if varlist is None:
762
raise ValueError, "vars must be specified if formula is a string"
763
764
free_vars = len(varlist) - formula.count('(')
765
else:
766
formula = qepcad_formula.formula(formula)
767
fvars = formula.vars
768
fqvars = formula.qvars
769
if varlist is None:
770
varlist = sorted(fvars) + fqvars
771
else:
772
# Do some error-checking here. Parse the given vars
773
# and ensure they match up with the variables in the formula.
774
if frozenset(varlist) != (fvars | frozenset(fqvars)):
775
raise ValueError, "specified vars don't match vars in formula"
776
if len(fqvars) and varlist[-len(fqvars):] != fqvars:
777
raise ValueError, "specified vars don't match quantified vars"
778
free_vars = len(fvars)
779
formula = repr(formula)
780
781
self._varlist = varlist
782
self._free_vars = free_vars
783
784
varlist = [v.replace('_', '') for v in varlist]
785
if len(frozenset(varlist)) != len(varlist):
786
raise ValueError, "variables collide after stripping underscores"
787
formula = formula.replace('_', '')
788
789
qex = Qepcad_expect(logfile=logfile)
790
qex._send('[ input from Sage ]')
791
qex._send('(' + ','.join(varlist) + ')')
792
qex._send(str(free_vars))
793
# I hope this prompt is distinctive enough...
794
# if not, we could list all the cases separately
795
qex._change_prompt(['\r\n([^\r\n]*) >\r\n', pexpect.EOF])
796
qex.eval(formula + '.')
797
self._qex = qex
798
799
def __repr__(self):
800
r"""
801
Return a string representation of this \class{Qepcad} object.
802
803
EXAMPLES::
804
805
sage: qepcad(x - 1 == 0, interact=True) # optional - qepcad
806
QEPCAD object in phase 'Before Normalization'
807
"""
808
return "QEPCAD object in phase '%s'"%self.phase()
809
810
def assume(self, assume):
811
r"""
812
The following documentation is from \file{qepcad.help}:
813
814
Add an assumption to the problem. These will not be
815
included in the solution formula.
816
817
For example, with input (E x)[ a x^2 + b x + c = 0],
818
if we issue the command
819
820
assume [ a /= 0 ]
821
822
we'll get the solution formula b^2 - 4 a c >= 0. Without
823
the assumption we'd get something like [a = 0 /\ b /= 0] \/
824
[a /= 0 /\ 4 a c - b^2 <= 0] \/ [a = 0 /\ b = 0 /\ c = 0].
825
826
EXAMPLES::
827
828
sage: var('a,b,c,x')
829
(a, b, c, x)
830
sage: qf = qepcad_formula
831
sage: qe = qepcad(qf.exists(x, a*x^2 + b*x + c == 0), interact=True) # optional - qepcad
832
sage: qe.assume(a != 0) # optional - qepcad
833
sage: qe.finish() # optional - qepcad
834
4 a c - b^2 <= 0
835
"""
836
if not isinstance(assume, str):
837
assume = qepcad_formula.formula(assume)
838
if len(assume.qvars):
839
raise ValueError, "assumptions cannot be quantified"
840
if not assume.vars.issubset(frozenset(self._varlist[:self._free_vars])):
841
raise ValueError, "assumption contains variables not present in formula"
842
assume = repr(assume)
843
assume = assume.replace('_', '')
844
result = self._eval_line("assume [%s]" % assume)
845
if len(result):
846
return AsciiArtString(result)
847
848
def solution_extension(self, kind):
849
r"""
850
The following documentation is modified from \file{qepcad.help}:
851
852
solution-extension x
853
854
Use an alternative solution formula construction method. The
855
parameter x is allowed to be T,E, or G. If x is T, then a
856
formula in the usual language of Tarski formulas is produced.
857
If x is E, a formula in the language of Extended Tarski formulas
858
is produced. If x is G, then a geometry-based formula is
859
produced.
860
861
EXAMPLES::
862
863
sage: var('x,y')
864
(x, y)
865
sage: qf = qepcad_formula
866
sage: qe = qepcad(qf.and_(x^2 + y^2 - 3 == 0, x + y > 0), interact=True) # optional
867
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
868
QEPCAD object has moved to phase 'Before Projection (y)'
869
QEPCAD object has moved to phase 'Before Choice'
870
QEPCAD object has moved to phase 'Before Solution'
871
sage: qe.solution_extension('E') # optional - qepcad
872
x > _root_1 2 x^2 - 3 /\ y^2 + x^2 - 3 = 0 /\ [ 2 x^2 - 3 > 0 \/ y = _root_-1 y^2 + x^2 - 3 ]
873
sage: qe.solution_extension('G') # optional - qepcad
874
[
875
[
876
2 x^2 - 3 < 0
877
\/
878
x = _root_-1 2 x^2 - 3
879
]
880
/\
881
y = _root_-1 y^2 + x^2 - 3
882
]
883
\/
884
[
885
x^2 - 3 <= 0
886
/\
887
x > _root_-1 2 x^2 - 3
888
/\
889
y^2 + x^2 - 3 = 0
890
]
891
sage: qe.solution_extension('T') # optional - qepcad
892
y + x > 0 /\ y^2 + x^2 - 3 = 0
893
"""
894
if kind == 'I':
895
raise ValueError, "Interactive solution construction not handled by Sage interface"
896
result = self._eval_line('solution-extension %s'%kind)
897
tagline = 'An equivalent quantifier-free formula:'
898
loc = result.find(tagline)
899
if loc >= 0:
900
result = result[loc + len(tagline):]
901
result = result.strip()
902
if len(result):
903
return AsciiArtString(result)
904
905
def set_truth_value(self, index, nv):
906
r"""
907
Given a cell index (or a cell) and an integer, set the truth value
908
of the cell to that integer. Valid integers are 0 (false),
909
1 (true), and 2 (undetermined).
910
911
EXAMPLES::
912
913
sage: qe = qepcad(x == 1, interact=True) # optional - qepcad
914
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
915
QEPCAD object has moved to phase 'At the end of projection phase'
916
QEPCAD object has moved to phase 'Before Choice'
917
QEPCAD object has moved to phase 'Before Solution'
918
sage: qe.set_truth_value(1, 1) # optional - qepcad
919
"""
920
index_str = _format_cell_index([index])
921
self._eval_line('set-truth-value\n%s\n%s' % (index_str, nv))
922
923
def phase(self):
924
r"""
925
Return the current phase of the QEPCAD program.
926
927
EXAMPLES::
928
929
sage: qe = qepcad(x > 2/3, interact=True) # optional - qepcad
930
sage: qe.phase() # optional - qepcad
931
'Before Normalization'
932
sage: qe.go() # optional
933
QEPCAD object has moved to phase 'At the end of projection phase'
934
sage: qe.phase() # optional - qepcad
935
'At the end of projection phase'
936
sage: qe.go() # optional
937
QEPCAD object has moved to phase 'Before Choice'
938
sage: qe.phase() # optional - qepcad
939
'Before Choice'
940
sage: qe.go() # optional
941
QEPCAD object has moved to phase 'Before Solution'
942
sage: qe.phase() # optional - qepcad
943
'Before Solution'
944
sage: qe.go() # optional - qepcad
945
3 x - 2 > 0
946
sage: qe.phase() # optional - qepcad
947
'EXITED'
948
"""
949
match = self._qex.expect().match
950
if match == pexpect.EOF:
951
return 'EXITED'
952
else:
953
return match.group(1)
954
955
def _parse_answer_stats(self):
956
r"""
957
Parse the final string printed by QEPCAD, which should be
958
the simplified quantifier-free formula followed by some
959
statistics. Return a pair of the formula and the statistics
960
(both as strings).
961
962
EXAMPLES::
963
964
sage: qe = qepcad(x^2 > 2, interact=True) # optional - qepcad
965
sage: qe.finish() # optional - qepcad
966
x^2 - 2 > 0
967
sage: (ans, stats) = qe._parse_answer_stats() # optional - qepcad
968
sage: ans # optional - qepcad
969
'x^2 - 2 > 0'
970
sage: stats # random, optional - qepcad
971
'-----------------------------------------------------------------------------\r\n0 Garbage collections, 0 Cells and 0 Arrays reclaimed, in 0 milliseconds.\r\n492514 Cells in AVAIL, 500000 Cells in SPACE.\r\n\r\nSystem time: 16 milliseconds.\r\nSystem time after the initialization: 4 milliseconds.\r\n-----------------------------------------------------------------------------\r\n'
972
"""
973
if self.phase() != 'EXITED':
974
raise ValueError, "QEPCAD is not finished yet"
975
final = self._qex.expect().before
976
match = re.search('\nAn equivalent quantifier-free formula:(.*)\n=+ The End =+\r\n\r\n(.*)$', final, re.DOTALL)
977
978
if match:
979
return (match.group(1).strip(), match.group(2))
980
else:
981
return (final, '')
982
983
def answer(self):
984
r"""
985
For a QEPCAD instance which is finished, return the
986
simplified quantifier-free formula that it printed just before
987
exiting.
988
989
EXAMPLES::
990
991
sage: qe = qepcad(x^3 - x == 0, interact=True) # optional - qepcad
992
sage: qe.finish() # optional - qepcad
993
x - 1 <= 0 /\ x + 1 >= 0 /\ [ x = 0 \/ x - 1 = 0 \/ x + 1 = 0 ]
994
sage: qe.answer() # optional - qepcad
995
x - 1 <= 0 /\ x + 1 >= 0 /\ [ x = 0 \/ x - 1 = 0 \/ x + 1 = 0 ]
996
"""
997
return AsciiArtString(self._parse_answer_stats()[0])
998
999
def final_stats(self):
1000
r"""
1001
For a QEPCAD instance which is finished, return the
1002
statistics that it printed just before exiting.
1003
1004
EXAMPLES::
1005
1006
sage: qe = qepcad(x == 0, interact=True) # optional
1007
sage: qe.finish() # optional
1008
x = 0
1009
sage: qe.final_stats() # random, optional
1010
-----------------------------------------------------------------------------
1011
0 Garbage collections, 0 Cells and 0 Arrays reclaimed, in 0 milliseconds.
1012
492840 Cells in AVAIL, 500000 Cells in SPACE.
1013
System time: 8 milliseconds.
1014
System time after the initialization: 4 milliseconds.
1015
-----------------------------------------------------------------------------
1016
"""
1017
return AsciiArtString(self._parse_answer_stats()[1])
1018
1019
def trait_names(self):
1020
r"""
1021
Returns a list of the QEPCAD commands which are available as
1022
extra methods on a \class{Qepcad} object.
1023
1024
EXAMPLES::
1025
1026
sage: qe = qepcad(x^2 < 0, interact=True) # optional - qepcad
1027
sage: len(qe.trait_names()) # random, optional - qepcad
1028
97
1029
sage: 'd_cell' in qe.trait_names() # optional - qepcad
1030
True
1031
"""
1032
_update_command_info()
1033
return _command_info_cache.keys()
1034
1035
def cell(self, *index):
1036
r"""
1037
Given a cell index, returns a \class{QepcadCell} wrapper for that
1038
cell. Uses a cache for efficiency.
1039
1040
EXAMPLES::
1041
1042
sage: qe = qepcad(x + 3 == 42, interact=True) # optional - qepcad
1043
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
1044
QEPCAD object has moved to phase 'At the end of projection phase'
1045
QEPCAD object has moved to phase 'Before Choice'
1046
QEPCAD object has moved to phase 'Before Solution'
1047
sage: qe.cell(2) # optional - qepcad
1048
QEPCAD cell (2)
1049
sage: qe.cell(2) is qe.cell(2) # optional - qepcad
1050
True
1051
"""
1052
index_str = _format_cell_index(index)
1053
if self._cell_cache.has_key(index_str):
1054
return self._cell_cache[index_str]
1055
else:
1056
c = self.make_cells(self.d_cell(index))[0]
1057
self._cell_cache[index_str] = c
1058
return c
1059
1060
def make_cells(self, text):
1061
r"""
1062
Given the result of some QEPCAD command that returns cells
1063
(such as \method{d_cell}, \method{d_witness_list}, etc.),
1064
return a list of cell objects.
1065
1066
EXAMPLES::
1067
1068
sage: var('x,y')
1069
(x, y)
1070
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
1071
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
1072
QEPCAD object has moved to phase 'Before Projection (y)'
1073
QEPCAD object has moved to phase 'Before Choice'
1074
QEPCAD object has moved to phase 'Before Solution'
1075
sage: qe.make_cells(qe.d_false_cells()) # optional - qepcad
1076
[QEPCAD cell (5, 1), QEPCAD cell (4, 3), QEPCAD cell (4, 1), QEPCAD cell (3, 5), QEPCAD cell (3, 3), QEPCAD cell (3, 1), QEPCAD cell (2, 3), QEPCAD cell (2, 1), QEPCAD cell (1, 1)]
1077
"""
1078
# get rid of AsciiArtString
1079
text = str(text)
1080
1081
lines = text.strip().splitlines()
1082
1083
cells = []
1084
cell_lines = []
1085
in_cell = False
1086
1087
for line in lines:
1088
if 'Information about the cell' in line:
1089
in_cell = True
1090
if in_cell: cell_lines.append(line)
1091
if line == '----------------------------------------------------':
1092
cells.append(QepcadCell(self, cell_lines))
1093
cell_lines = []
1094
in_cell = False
1095
1096
return cells
1097
1098
1099
def __getattr__(self, attrname):
1100
r"""
1101
Returns a \class{QepcadFunction} object for any QEPCAD command.
1102
1103
EXAMPLES::
1104
1105
sage: qe = qepcad(x^3 == 8, interact=True) # optional - qepcad
1106
sage: qe.d_cell # optional - qepcad
1107
d_cell
1108
"""
1109
if attrname[:1] == "_":
1110
raise AttributeError
1111
if not attrname in self.trait_names():
1112
raise AttributeError
1113
return QepcadFunction(self, attrname)
1114
1115
def _eval_line(self, cmd, restart_if_needed=False):
1116
r"""
1117
Send a command to QEPCAD, wait for a prompt, and return the
1118
text printed by QEPCAD before the prompt. Not intended for
1119
direct use.
1120
1121
EXAMPLES::
1122
1123
sage: qe = qepcad(x^2 == x^3, interact=True) # optional - qepcad
1124
sage: qe._eval_line('d-formula') # optional - qepcad
1125
'-x^3 + x^2 = 0'
1126
"""
1127
# Evidently when the QEPCAD command parser reads a command, it
1128
# parses from the beginning of a line until it has found a command,
1129
# ignoring newlines. It then throws away the rest of the line
1130
# after the end of the command. There is no command terminator;
1131
# each command does its own argument parsing and executes
1132
# as soon as it sees all the arguments.
1133
1134
# Thus, if the user gives a function call with a missing argument,
1135
# QEPCAD will wait forever for the missing argument to show up
1136
# (with no further prompting), and Sage will wait forever for
1137
# a prompt. Not good.
1138
1139
# To avoid this, we add a trailing "&" to each command.
1140
# If there is a missing argument, then the QEPCAD argument parsing
1141
# will give a syntax error on the "&", instead of waiting forever;
1142
# if there is no missing argument then QEPCAD will silently
1143
# ignore the "&". (Hopefully all QEPCAD commands will treat "&"
1144
# as a syntax error; as far as I know that's the case.)
1145
1146
# This trailing "&" also helps with another problem; sometimes
1147
# we get a copy of the command we send to QEPCAD echoed back as
1148
# the first line of the result. I'm guessing this is because
1149
# readline turns raw mode on when it's reading and off when it isn't;
1150
# if we manage to send a command with raw mode off, then it's
1151
# echoed twice (once by the normal UNIX tty handling and once by
1152
# readline). To work around this problem, we check for an "&"
1153
# in the first line of the input, and remove the text up to the "&"
1154
# if it is present. (Hopefully QEPCAD doesn't print "&" as part
1155
# of its normal operation.)
1156
1157
result = self._qex._eval_line(cmd + ' &')
1158
1159
nl = result.find('\n')
1160
if nl < 0: nl = len(result)
1161
1162
amp = result.find('&', 0, nl)
1163
if amp > 0: result = result[amp+1:]
1164
1165
result = result.strip()
1166
1167
return result
1168
1169
def _function_call(self, name, args):
1170
r"""
1171
Given a command name and a list of arguments, send the command
1172
to QEPCAD and return the result. Not intended for direct use.
1173
1174
EXAMPLES::
1175
1176
sage: qe = qepcad(x^2 - 1 == 0, interact=True) # optional - qepcad
1177
sage: qe.go(); qe.go() # optional - qepcad
1178
QEPCAD object has moved to phase 'At the end of projection phase'
1179
QEPCAD object has moved to phase 'Before Choice'
1180
sage: qe._function_call('d_level_factors', (1,)) # optional - qepcad
1181
A_1,1 = input
1182
= x + 1
1183
A_1,2 = input
1184
= x - 1
1185
"""
1186
name = name.replace('_', '-')
1187
args = map(str, args)
1188
pre_phase = self.phase()
1189
result = self._eval_line('%s %s'%(name, ' '.join(args)))
1190
post_phase = self.phase()
1191
if len(result) and post_phase != 'EXITED':
1192
return AsciiArtString(result)
1193
if pre_phase != post_phase:
1194
if post_phase == 'EXITED' and name != 'quit':
1195
return self.answer()
1196
return AsciiArtString("QEPCAD object has moved to phase '%s'"%post_phase)
1197
1198
def _format_cell_index(a):
1199
"""
1200
Given a tuple (or list, etc.) containing a QEPCAD cell index, return a
1201
string with a properly-formatted index. The input is flattened, so
1202
extra levels of brackets are ignored. Also, if the first item
1203
in the flattened list is a \class{QepcadCell} object, then its index
1204
is used in place of the object.
1205
1206
EXAMPLES::
1207
1208
sage: from sage.interfaces.qepcad import _format_cell_index
1209
1210
sage: qe = qepcad(x == 0, interact=True); qe.go(); qe.go(); qe.go() # optional - qepcad
1211
QEPCAD object has moved to phase 'At the end of projection phase'
1212
QEPCAD object has moved to phase 'Before Choice'
1213
QEPCAD object has moved to phase 'Before Solution'
1214
sage: _format_cell_index(qe.cell(1)) # optional - qepcad
1215
'(1)'
1216
sage: _format_cell_index((qe.cell(1), 2, 3)) # optional - qepcad
1217
'(1, 2, 3)'
1218
sage: _format_cell_index(())
1219
'()'
1220
sage: _format_cell_index(5)
1221
'(5)'
1222
"""
1223
a = flatten([a])
1224
if len(a) and isinstance(a[0], QepcadCell):
1225
a[0:1] = a[0].index()
1226
if len(a) == 1:
1227
return '(%s)' % a[0]
1228
else:
1229
return str(tuple(a))
1230
1231
class QepcadFunction(ExpectFunction):
1232
r"""
1233
A wrapper for a QEPCAD command.
1234
"""
1235
def _sage_doc_(self):
1236
r"""
1237
Returns the documentation for a QEPCAD command, from
1238
\file{qepcad.help}.
1239
1240
EXAMPLES::
1241
1242
sage: qe = qepcad(x == 17, interact=True) # optional - qepcad
1243
sage: cmd = qe.approx_precision # optional - qepcad
1244
sage: cmd._sage_doc_() # optional - qepcad
1245
'approx-precision N\n\nApproximate algeraic numbers to N decimal places.\n'
1246
"""
1247
_update_command_info()
1248
return _command_info_cache[self._name][3]
1249
1250
def __call__(self, *args):
1251
r"""
1252
Calls QEPCAD with the command this is a wrapper for.
1253
1254
For commands which take cell indexes, \function{_format_cell_index}
1255
is automatically called. For commands which take 'y' or 'n',
1256
booleans are also allowed. (These special commands were hand-selected
1257
after reading \file{qepcad.help}.)
1258
1259
EXAMPLES::
1260
1261
sage: qe = qepcad(x^2 < 1, interact=True) # optional - qepcad
1262
sage: cmd = qe.d_formula # optional - qepcad
1263
sage: cmd.__call__() # optional - qepcad
1264
x^2 - 1 < 0
1265
"""
1266
_update_command_info()
1267
info = _command_info_cache[self._name]
1268
special = info[4]
1269
# Tweak the argument processing for a few commands.
1270
args = list(args)
1271
1272
if special == 'cell':
1273
args = [_format_cell_index(args)]
1274
1275
if special == 'yn':
1276
if isinstance(args[0], bool):
1277
args[0] = 'y' if args[0] else 'n'
1278
1279
if special == 'interactive':
1280
raise ValueError, "Cannot call %s through Sage interface... interactive commands not handled"
1281
1282
return self._parent._function_call(self._name, args)
1283
1284
def qepcad(formula, assume=None, interact=False, solution=None, vars=None, **kwargs):
1285
r"""
1286
Quantifier elimination and formula simplification using QEPCAD B.
1287
1288
If \var{assume} is specified, then the given formula is ``assumed'',
1289
which is taken into account during final solution formula construction.
1290
1291
If \code{interact=True} is given, then a \class{Qepcad} object is
1292
returned which can be interacted with either at the command line
1293
or programmatically.
1294
1295
The type of solution returned can be adjusted with \var{solution}.
1296
The options are \code{'geometric'}, which tries to construct a
1297
solution formula with geometric meaning; \code{'extended'}, which
1298
gives a solution formula in an extended language that may be more
1299
efficient to construct; \code{'any-point'}, which returns any
1300
point where the formula is true; \code{'all-points'}, which
1301
returns a list of all points where the formula is true (or raises
1302
an exception if there are infinitely many); and \code{'cell-points'},
1303
which returns one point in each cell where the formula is true.
1304
1305
All other keyword arguments are passed through to the \class{Qepcad}
1306
constructor.
1307
1308
For much more documentation and many more examples, see the module
1309
docstring for this module (type \code{sage.interfaces.qepcad?} to
1310
read this docstring from the \sage command line).
1311
1312
The examples below require that the optional qepcad package is installed.
1313
1314
EXAMPLES::
1315
1316
sage: qf = qepcad_formula
1317
1318
sage: var('a,b,c,d,x,y,z,long_with_underscore_314159')
1319
(a, b, c, d, x, y, z, long_with_underscore_314159)
1320
sage: K.<q,r> = QQ[]
1321
1322
sage: qepcad('(E x)[a x + b > 0]', vars='(a,b,x)') # optional - qepcad
1323
a /= 0 \/ b > 0
1324
1325
sage: qepcad(a > b) # optional - qepcad
1326
b - a < 0
1327
1328
sage: qepcad(qf.exists(x, a*x^2 + b*x + c == 0)) # optional - qepcad
1329
4 a c - b^2 <= 0 /\ [ c = 0 \/ a /= 0 \/ 4 a c - b^2 < 0 ]
1330
1331
sage: qepcad(qf.exists(x, a*x^2 + b*x + c == 0), assume=(a != 0)) # optional - qepcad
1332
4 a c - b^2 <= 0
1333
1334
For which values of $a$, $b$, $c$ does $a x^2 + b x + c$ have
1335
2 real zeroes? ::
1336
1337
sage: exact2 = qepcad(qf.exactly_k(2, x, a*x^2 + b*x + c == 0)); exact2 # optional - qepcad
1338
a /= 0 /\ 4 a c - b^2 < 0
1339
1340
one real zero? ::
1341
1342
sage: exact1 = qepcad(qf.exactly_k(1, x, a*x^2 + b*x + c == 0)); exact1 # optional - qepcad
1343
[ a > 0 /\ 4 a c - b^2 = 0 ] \/ [ a < 0 /\ 4 a c - b^2 = 0 ] \/ [ a = 0 /\ 4 a c - b^2 < 0 ]
1344
1345
No real zeroes? ::
1346
1347
sage: exact0 = qepcad(qf.forall(x, a*x^2 + b*x + c != 0)); exact0 # optional - qepcad
1348
4 a c - b^2 >= 0 /\ c /= 0 /\ [ b = 0 \/ 4 a c - b^2 > 0 ]
1349
1350
$3^{75}$ real zeroes? ::
1351
1352
sage: qepcad(qf.exactly_k(3^75, x, a*x^2 + b*x + c == 0)) # optional - qepcad
1353
FALSE
1354
1355
We can check that the results don't overlap::
1356
1357
sage: qepcad(r'[[%s] /\ [%s]]' % (exact0, exact1), vars='a,b,c') # optional - qepcad
1358
FALSE
1359
sage: qepcad(r'[[%s] /\ [%s]]' % (exact0, exact2), vars='a,b,c') # optional - qepcad
1360
FALSE
1361
sage: qepcad(r'[[%s] /\ [%s]]' % (exact1, exact2), vars='a,b,c') # optional - qepcad
1362
FALSE
1363
1364
and that the union of the results is as expected::
1365
1366
sage: qepcad(r'[[%s] \/ [%s] \/ [%s]]' % (exact0, exact1, exact2), vars=(a,b,c)) # optional - qepcad
1367
b /= 0 \/ a /= 0 \/ c /= 0
1368
1369
So we have finitely many zeroes if $a$, $b$, or $c$ is nonzero;
1370
which means we should have infinitely many zeroes if they are all
1371
zero. ::
1372
1373
sage: qepcad(qf.infinitely_many(x, a*x^2 + b*x + c == 0)) # optional - qepcad
1374
a = 0 /\ b = 0 /\ c = 0
1375
1376
The polynomial is nonzero almost everywhere iff it is not
1377
identically zero. ::
1378
1379
sage: qepcad(qf.all_but_finitely_many(x, a*x^2 + b*x + c != 0)) # optional - qepcad
1380
b /= 0 \/ a /= 0 \/ c /= 0
1381
1382
The non-zeroes are continuous iff there are no zeroes or if
1383
the polynomial is zero. ::
1384
1385
sage: qepcad(qf.connected_subset(x, a*x^2 + b*x + c != 0)) # optional - qepcad
1386
4 a c - b^2 >= 0 /\ [ a = 0 \/ 4 a c - b^2 > 0 ]
1387
1388
The zeroes are continuous iff there are no or one zeroes, or if the
1389
polynomial is zero::
1390
1391
sage: qepcad(qf.connected_subset(x, a*x^2 + b*x + c == 0)) # optional - qepcad
1392
a = 0 \/ 4 a c - b^2 >= 0
1393
sage: qepcad(r'[[%s] \/ [%s] \/ [a = 0 /\ b = 0 /\ c = 0]]' % (exact0, exact1), vars='a,b,c') # optional - qepcad
1394
a = 0 \/ 4 a c - b^2 >= 0
1395
1396
Since polynomials are continuous and $y > 0$ is an open set,
1397
they are positive infinitely often iff they are positive at
1398
least once. ::
1399
1400
sage: qepcad(qf.infinitely_many(x, a*x^2 + b*x + c > 0)) # optional - qepcad
1401
c > 0 \/ a > 0 \/ 4 a c - b^2 < 0
1402
sage: qepcad(qf.exists(x, a*x^2 + b*x + c > 0)) # optional - qepcad
1403
c > 0 \/ a > 0 \/ 4 a c - b^2 < 0
1404
1405
However, since $y >= 0$ is not open, the equivalence does not
1406
hold if you replace ``positive'' with ``nonnegative''.
1407
(We assume $a \neq 0$ to get simpler formulas.) ::
1408
1409
sage: qepcad(qf.infinitely_many(x, a*x^2 + b*x + c >= 0), assume=(a != 0)) # optional - qepcad
1410
a > 0 \/ 4 a c - b^2 < 0
1411
sage: qepcad(qf.exists(x, a*x^2 + b*x + c >= 0), assume=(a != 0)) # optional - qepcad
1412
a > 0 \/ 4 a c - b^2 <= 0
1413
1414
TESTS:
1415
1416
We verify that long variable names work. (Note that QEPCAD
1417
does not support underscores, so they are stripped from the formula.) ::
1418
1419
sage: qepcad(qf.exists(a, a*long_with_underscore_314159 == 1)) # optional - qepcad
1420
longwithunderscore314159 /= 0
1421
"""
1422
use_witness = False
1423
if solution == 'any-point':
1424
formula = qepcad_formula.formula(formula)
1425
if len(formula.qvars) == 0:
1426
if vars is None:
1427
vars = sorted(list(formula.vars))
1428
formula = qepcad_formula.exists(vars, formula)
1429
vars = None
1430
use_witness = True
1431
1432
qe = Qepcad(formula, vars=vars, **kwargs)
1433
if assume is not None:
1434
qe.assume(assume)
1435
if interact:
1436
if solution is not None:
1437
print "WARNING: 'solution=' is ignored for interactive use"
1438
return qe
1439
else:
1440
qe.go()
1441
qe.go()
1442
qe.go()
1443
if solution is None:
1444
qe.finish()
1445
return qe.answer()
1446
elif solution == 'geometric':
1447
s = qe.solution_extension('G')
1448
qe.quit()
1449
return s
1450
elif solution == 'extended':
1451
s = qe.solution_extension('E')
1452
qe.quit()
1453
return s
1454
elif solution == 'any-point':
1455
if use_witness:
1456
cells = qe.make_cells(qe.d_witness_list())
1457
else:
1458
cells = qe.make_cells(qe.d_true_cells())
1459
qe.quit()
1460
if len(cells) == 0:
1461
raise ValueError, "input formula is false everywhere"
1462
return cells[0].sample_point_dict()
1463
elif solution == 'cell-points':
1464
cells = qe.make_cells(qe.d_true_cells())
1465
qe.quit()
1466
return [c.sample_point_dict() for c in cells]
1467
elif solution == 'all-points':
1468
cells = qe.make_cells(qe.d_true_cells())
1469
qe.quit()
1470
for c in cells:
1471
if c._dimension > 0:
1472
raise ValueError, "input formula is true for infinitely many points"
1473
return [c.sample_point_dict() for c in cells]
1474
else:
1475
raise ValueError, "Unknown solution type (%s)" % solution
1476
1477
1478
import os
1479
def qepcad_console(memcells=None):
1480
r"""
1481
Run QEPCAD directly. To exit early, press Control-C.
1482
1483
EXAMPLES::
1484
1485
sage: qepcad_console() # not tested
1486
...
1487
Enter an informal description between '[' and ']':
1488
"""
1489
_rewrite_qepcadrc()
1490
# This will only spawn local processes
1491
os.system(_qepcad_cmd(memcells))
1492
1493
1494
def qepcad_banner():
1495
"""
1496
Return the QEPCAD startup banner.
1497
1498
EXAMPLES::
1499
1500
sage: from sage.interfaces.qepcad import qepcad_banner
1501
sage: qepcad_banner() # optional - qepcad
1502
=======================================================
1503
Quantifier Elimination
1504
in
1505
Elementary Algebra and Geometry
1506
by
1507
Partial Cylindrical Algebraic Decomposition
1508
...
1509
by
1510
Hoon Hong
1511
([email protected])
1512
With contributions by: Christopher W. Brown, George E.
1513
Collins, Mark J. Encarnacion, Jeremy R. Johnson
1514
Werner Krandick, Richard Liska, Scott McCallum,
1515
Nicolas Robidoux, and Stanly Steinberg
1516
=======================================================
1517
"""
1518
qex = Qepcad_expect()
1519
qex._start()
1520
banner = qex.expect().before
1521
qex.quit(timeout=0)
1522
return AsciiArtString(banner)
1523
1524
def qepcad_version():
1525
"""
1526
Return a string containing the current QEPCAD version number.
1527
1528
EXAMPLES::
1529
1530
sage: qepcad_version() # random, optional - qepcad
1531
'Version B 1.48, 25 Oct 2007'
1532
1533
TESTS::
1534
1535
sage: qepcad_version() # optional - qepcad
1536
'Version B ..., ...'
1537
"""
1538
banner = str(qepcad_banner())
1539
lines = banner.split('\n')
1540
for line in lines:
1541
if 'Version' in line:
1542
return line.strip()
1543
1544
class qformula:
1545
"""
1546
A qformula holds a string describing a formula in QEPCAD's syntax,
1547
and a set of variables used.
1548
"""
1549
def __init__(self, formula, vars, qvars=[]):
1550
r"""
1551
Construct a qformula from a string, a frozenset of variable names,
1552
and (optionally) a list of ordered quantified names.
1553
1554
EXAMPLES::
1555
1556
sage: from sage.interfaces.qepcad import qformula
1557
sage: f = qformula('x + y = 0', frozenset(['x','y']))
1558
sage: f
1559
x + y = 0
1560
sage: f.formula
1561
'x + y = 0'
1562
sage: f.vars
1563
frozenset(['y', 'x'])
1564
sage: f.qvars
1565
[]
1566
"""
1567
self.formula = formula
1568
self.vars = vars
1569
self.qvars = qvars
1570
1571
def __repr__(self):
1572
r"""
1573
Returns a string representation of a qformula (this is just
1574
the formula it holds).
1575
1576
EXAMPLES::
1577
1578
sage: from sage.interfaces.qepcad import qformula
1579
sage: f = qformula('x + y = 0', frozenset(['x','y']))
1580
sage: f.__repr__()
1581
'x + y = 0'
1582
"""
1583
return self.formula
1584
1585
class qepcad_formula_factory:
1586
r"""
1587
Contains routines to help construct formulas in QEPCAD syntax.
1588
"""
1589
1590
def _normalize_op(self, op):
1591
r"""
1592
Given a relational operator (either a string, or a function from
1593
the \module{operator} module) return the corresponding QEPCAD
1594
operator.
1595
1596
EXAMPLES::
1597
1598
sage: qf = qepcad_formula
1599
sage: qf._normalize_op(operator.ne)
1600
'/='
1601
sage: qf._normalize_op('==')
1602
'='
1603
"""
1604
import operator
1605
if op == operator.eq: return '='
1606
if op == operator.ne: return '/='
1607
if op == operator.lt: return '<'
1608
if op == operator.gt: return '>'
1609
if op == operator.le: return '<='
1610
if op == operator.ge: return '>='
1611
1612
if op == '==': return '='
1613
if op == '!=': return '/='
1614
1615
return op
1616
1617
def _varset(self, p):
1618
r"""
1619
Given a polynomial or a symbolic expression, return a frozenset
1620
of the variables involved.
1621
1622
EXAMPLES::
1623
1624
sage: qf = qepcad_formula
1625
sage: var('x,y')
1626
(x, y)
1627
sage: K.<p,q> = QQ[]
1628
sage: qf._varset(x)
1629
frozenset(['x'])
1630
sage: qf._varset(x*y)
1631
frozenset(['y', 'x'])
1632
sage: qf._varset(q)
1633
frozenset(['q'])
1634
sage: qf._varset(p*q)
1635
frozenset(['q', 'p'])
1636
"""
1637
try:
1638
vars = p.variables()
1639
except AttributeError:
1640
vars = []
1641
return frozenset([str(v) for v in vars])
1642
1643
def _combine_formulas(self, formulas):
1644
r"""
1645
Given a list of formulas, convert them to strings and return
1646
the free variables found in the formulas.
1647
1648
Since this is used to build boolean expressions for QEPCAD,
1649
and QEPCAD boolean expressions cannot be built from quantified
1650
formulas, an exception is raised if an input formula is quantified.
1651
1652
INPUT:
1653
1654
- ``formulas`` -- a list of unquantified formulas
1655
1656
OUTPUT:
1657
1658
form_strs -- a list of formulas as strings
1659
vars -- a frozenset of all variables in the formulas
1660
1661
EXAMPLES::
1662
1663
sage: var('x,y')
1664
(x, y)
1665
sage: qf = qepcad_formula
1666
sage: qf._combine_formulas([x^2 == 0, y < 17])
1667
(['x^2 = 0', 'y < 17'], frozenset(['y', 'x']))
1668
"""
1669
formulas = map(self.atomic, formulas)
1670
formulas = map(self.atomic, formulas)
1671
formula_strs = map(repr, formulas)
1672
vars = frozenset()
1673
for f in formulas:
1674
vars = vars | f.vars
1675
if len(f.qvars):
1676
raise ValueError, "QEPCAD formulas must be in prenex (quantifiers outermost) form"
1677
return formula_strs, vars
1678
1679
def atomic(self, lhs, op='=', rhs=0):
1680
r"""
1681
Constructs a QEPCAD formula from the given inputs.
1682
1683
INPUT:
1684
1685
- ``lhs`` -- a polynomial, or a symbolic equality or inequality
1686
- ``op`` -- a relational operator, default '='
1687
- ``rhs`` -- a polynomial, default 0
1688
1689
If \var{lhs} is a symbolic equality or inequality, then \var{op}
1690
and \var{rhs} are ignored.
1691
1692
This method works by printing the given polynomials, so we don't
1693
care what ring they are in (as long as they print with integral
1694
or rational coefficients).
1695
1696
EXAMPLES::
1697
1698
sage: qf = qepcad_formula
1699
sage: var('a,b,c')
1700
(a, b, c)
1701
sage: K.<x,y> = QQ[]
1702
sage: def test_qf(qf):
1703
... return qf, qf.vars
1704
sage: test_qf(qf.atomic(a^2 + 17))
1705
(a^2 + 17 = 0, frozenset(['a']))
1706
sage: test_qf(qf.atomic(a*b*c <= c^3))
1707
(a b c <= c^3, frozenset(['a', 'c', 'b']))
1708
sage: test_qf(qf.atomic(x+y^2, '!=', a+b))
1709
(y^2 + x /= a + b, frozenset(['y', 'x', 'b', 'a']))
1710
sage: test_qf(qf.atomic(x, operator.lt))
1711
(x < 0, frozenset(['x']))
1712
"""
1713
if isinstance(lhs, qformula):
1714
return lhs
1715
1716
from sage.symbolic.expression import is_SymbolicEquation
1717
if is_SymbolicEquation(lhs):
1718
rhs = lhs.rhs()
1719
op = lhs.operator()
1720
lhs = lhs.lhs()
1721
1722
op = self._normalize_op(op)
1723
1724
formula = ('%r %s %r' % (lhs, op, rhs))
1725
formula = formula.replace('*', ' ')
1726
vars = self._varset(lhs) | self._varset(rhs)
1727
1728
return qformula(formula, vars)
1729
1730
def formula(self, formula):
1731
r"""
1732
Constructs a QEPCAD formula from the given input.
1733
1734
INPUTS:
1735
1736
- ``formula`` -- a polynomial, a symbolic equality or inequality,
1737
or a list of polynomials, equalities, or inequalities
1738
1739
A polynomial $p$ is interpreted as the equation $p = 0$.
1740
A list is interpreted as the conjunction (``and'') of the elements.
1741
1742
EXAMPLES::
1743
1744
sage: var('a,b,c,x')
1745
(a, b, c, x)
1746
sage: qf = qepcad_formula
1747
sage: qf.formula(a*x + b)
1748
a x + b = 0
1749
sage: qf.formula((a*x^2 + b*x + c, a != 0))
1750
[a x^2 + b x + c = 0 /\ a /= 0]
1751
"""
1752
if isinstance(formula, (list, tuple)):
1753
return self.and_(formula)
1754
else:
1755
return self.atomic(formula)
1756
1757
def and_(self, *formulas):
1758
r"""
1759
Returns the conjunction of its input formulas. (This method would
1760
be named ``and'' if that weren't a Python keyword.)
1761
1762
Each input formula may be a \class{qformula} as returned by the
1763
methods of \code{qepcad_formula}, a symbolic equality or
1764
inequality, or a polynomial $p$ (meaning $p = 0$).
1765
1766
EXAMPLES::
1767
1768
sage: var('a,b,c,x')
1769
(a, b, c, x)
1770
sage: qf = qepcad_formula
1771
sage: qf.and_(a*b, a*c, b*c != 0)
1772
[a b = 0 /\ a c = 0 /\ b c /= 0]
1773
sage: qf.and_(a*x^2 == 3, qf.or_(a > b, b > c))
1774
[a x^2 = 3 /\ [a > b \/ b > c]]
1775
"""
1776
formulas = flatten(formulas)
1777
formula_strs, vars = self._combine_formulas(formulas)
1778
formula = '[' + r' /\ '.join(formula_strs) + ']'
1779
return qformula(formula, vars)
1780
1781
def or_(self, *formulas):
1782
r"""
1783
Returns the disjunction of its input formulas. (This method would
1784
be named ``or'' if that weren't a Python keyword.)
1785
1786
Each input formula may be a \class{qformula} as returned by the
1787
methods of \code{qepcad_formula}, a symbolic equality or
1788
inequality, or a polynomial $p$ (meaning $p = 0$).
1789
1790
EXAMPLES::
1791
1792
sage: var('a,b,c,x')
1793
(a, b, c, x)
1794
sage: qf = qepcad_formula
1795
sage: qf.or_(a*b, a*c, b*c != 0)
1796
[a b = 0 \/ a c = 0 \/ b c /= 0]
1797
sage: qf.or_(a*x^2 == 3, qf.and_(a > b, b > c))
1798
[a x^2 = 3 \/ [a > b /\ b > c]]
1799
"""
1800
formulas = flatten(formulas)
1801
formula_strs, vars = self._combine_formulas(formulas)
1802
formula = '[' + r' \/ '.join(formula_strs) + ']'
1803
return qformula(formula, vars)
1804
1805
def not_(self, formula):
1806
r"""
1807
Returns the negation of its input formula. (This method would be
1808
named ``not'' if that weren't a Python keyword.)
1809
1810
The input formula may be a \class{qformula} as returned by the
1811
methods of \code{qepcad_formula}, a symbolic equality or
1812
inequality, or a polynomial $p$ (meaning $p = 0$).
1813
1814
EXAMPLES::
1815
1816
sage: var('a,b')
1817
(a, b)
1818
sage: qf = qepcad_formula
1819
sage: qf.not_(a > b)
1820
[~a > b]
1821
sage: qf.not_(a^2 + b^2)
1822
[~a^2 + b^2 = 0]
1823
sage: qf.not_(qf.and_(a > 0, b < 0))
1824
[~[a > 0 /\ b < 0]]
1825
"""
1826
(formula_str,), vars = self._combine_formulas([formula])
1827
f = '[~' + formula_str + ']'
1828
return qformula(f, vars)
1829
1830
def implies(self, f1, f2):
1831
r"""
1832
Returns the implication of its input formulas (that is, given
1833
formulas $P$ and $Q$, returns ``$P$ implies $Q$'').
1834
1835
The input formulas may be a \class{qformula} as returned by the
1836
methods of \code{qepcad_formula}, a symbolic equality or
1837
inequality, or a polynomial $p$ (meaning $p = 0$).
1838
1839
EXAMPLES::
1840
1841
sage: var('a,b')
1842
(a, b)
1843
sage: qf = qepcad_formula
1844
sage: qf.implies(a, b)
1845
[a = 0 ==> b = 0]
1846
sage: qf.implies(a^2 < b, b^2 < a)
1847
[a^2 < b ==> b^2 < a]
1848
"""
1849
(f1s, f2s), vars = self._combine_formulas([f1, f2])
1850
f = '[' + f1s + ' ==> ' + f2s + ']'
1851
return qformula(f, vars)
1852
1853
# QEPCAD also has a "reverse implication" symbol "<==", which
1854
# I'm not bothering to support.
1855
1856
def iff(self, f1, f2):
1857
r"""
1858
Returns the equivalence of its input formulas (that is, given
1859
formulas $P$ and $Q$, returns ``$P$ iff $Q$'').
1860
1861
The input formulas may be a \class{qformula} as returned by the
1862
methods of \code{qepcad_formula}, a symbolic equality or
1863
inequality, or a polynomial $p$ (meaning $p = 0$).
1864
1865
EXAMPLES::
1866
1867
sage: var('a,b')
1868
(a, b)
1869
sage: qf = qepcad_formula
1870
sage: qf.iff(a, b)
1871
[a = 0 <==> b = 0]
1872
sage: qf.iff(a^2 < b, b^2 < a)
1873
[a^2 < b <==> b^2 < a]
1874
"""
1875
(f1s, f2s), vars = self._combine_formulas([f1, f2])
1876
f = '[' + f1s + ' <==> ' + f2s + ']'
1877
return qformula(f, vars)
1878
1879
def exists(self, v, formula):
1880
r"""
1881
Given a variable (or list of variables) and a formula, returns
1882
the existential quantification of the formula over the variables.
1883
1884
This method is available both as \method{exists} and \method{E}
1885
(the QEPCAD name for this quantifier).
1886
1887
The input formula may be a \class{qformula} as returned by the
1888
methods of \code{qepcad_formula}, a symbolic equality or
1889
inequality, or a polynomial $p$ (meaning $p = 0$).
1890
1891
EXAMPLE::
1892
1893
sage: var('a,b')
1894
(a, b)
1895
sage: qf = qepcad_formula
1896
sage: qf.exists(a, a^2 + b > b^2 + a)
1897
(E a)[a^2 + b > b^2 + a]
1898
sage: qf.exists((a, b), a^2 + b^2 < 0)
1899
(E a)(E b)[a^2 + b^2 < 0]
1900
sage: qf.E(b, b^2 == a)
1901
(E b)[b^2 = a]
1902
"""
1903
return self.quantifier('E', v, formula)
1904
E = exists
1905
1906
def forall(self, v, formula):
1907
r"""
1908
Given a variable (or list of variables) and a formula, returns
1909
the universal quantification of the formula over the variables.
1910
1911
This method is available both as \method{forall} and \method{A}
1912
(the QEPCAD name for this quantifier).
1913
1914
The input formula may be a \class{qformula} as returned by the
1915
methods of \code{qepcad_formula}, a symbolic equality or
1916
inequality, or a polynomial $p$ (meaning $p = 0$).
1917
1918
EXAMPLE::
1919
1920
sage: var('a,b')
1921
(a, b)
1922
sage: qf = qepcad_formula
1923
sage: qf.forall(a, a^2 + b > b^2 + a)
1924
(A a)[a^2 + b > b^2 + a]
1925
sage: qf.forall((a, b), a^2 + b^2 > 0)
1926
(A a)(A b)[a^2 + b^2 > 0]
1927
sage: qf.A(b, b^2 != a)
1928
(A b)[b^2 /= a]
1929
"""
1930
return self.quantifier('A', v, formula)
1931
A = forall
1932
1933
def infinitely_many(self, v, formula):
1934
r"""
1935
Given a variable and a formula, returns a new formula which is
1936
true iff the original formula was true for infinitely many
1937
values of the variable.
1938
1939
This method is available both as \method{infinitely_many}
1940
and \method{F} (the QEPCAD name for this quantifier).
1941
1942
The input formula may be a \class{qformula} as returned by the
1943
methods of \code{qepcad_formula}, a symbolic equality or
1944
inequality, or a polynomial $p$ (meaning $p = 0$).
1945
1946
EXAMPLE::
1947
1948
sage: var('a,b')
1949
(a, b)
1950
sage: qf = qepcad_formula
1951
sage: qf.infinitely_many(a, a^2 + b > b^2 + a)
1952
(F a)[a^2 + b > b^2 + a]
1953
sage: qf.F(b, b^2 != a)
1954
(F b)[b^2 /= a]
1955
"""
1956
return self.quantifier('F', v, formula, allow_multi=False)
1957
F = infinitely_many
1958
1959
def all_but_finitely_many(self, v, formula):
1960
r"""
1961
Given a variable and a formula, returns a new formula which is
1962
true iff the original formula was true for all but finitely many
1963
values of the variable.
1964
1965
This method is available both as \method{all_but_finitely_many}
1966
and \method{G} (the QEPCAD name for this quantifier).
1967
1968
The input formula may be a \class{qformula} as returned by the
1969
methods of \code{qepcad_formula}, a symbolic equality or
1970
inequality, or a polynomial $p$ (meaning $p = 0$).
1971
1972
EXAMPLE::
1973
1974
sage: var('a,b')
1975
(a, b)
1976
sage: qf = qepcad_formula
1977
sage: qf.all_but_finitely_many(a, a^2 + b > b^2 + a)
1978
(G a)[a^2 + b > b^2 + a]
1979
sage: qf.G(b, b^2 != a)
1980
(G b)[b^2 /= a]
1981
"""
1982
return self.quantifier('G', v, formula, allow_multi=False)
1983
G = all_but_finitely_many
1984
1985
def connected_subset(self, v, formula, allow_multi=False):
1986
r"""
1987
Given a variable and a formula, returns a new formula which is
1988
true iff the set of values for the variable at which the
1989
original formula was true is connected (including cases where
1990
this set is empty or is a single point).
1991
1992
This method is available both as \method{connected_subset}
1993
and \method{C} (the QEPCAD name for this quantifier).
1994
1995
The input formula may be a \class{qformula} as returned by the
1996
methods of \code{qepcad_formula}, a symbolic equality or
1997
inequality, or a polynomial $p$ (meaning $p = 0$).
1998
1999
EXAMPLE::
2000
2001
sage: var('a,b')
2002
(a, b)
2003
sage: qf = qepcad_formula
2004
sage: qf.connected_subset(a, a^2 + b > b^2 + a)
2005
(C a)[a^2 + b > b^2 + a]
2006
sage: qf.C(b, b^2 != a)
2007
(C b)[b^2 /= a]
2008
"""
2009
return self.quantifier('C', v, formula)
2010
C = connected_subset
2011
2012
def exactly_k(self, k, v, formula, allow_multi=False):
2013
r"""
2014
Given a nonnegative integer $k$, a variable, and a formula,
2015
returns a new formula which is true iff the original formula
2016
is true for exactly $k$ values of the variable.
2017
2018
This method is available both as \method{exactly_k}
2019
and \method{X} (the QEPCAD name for this quantifier).
2020
2021
(Note that QEPCAD does not support $k=0$ with this syntax, so if
2022
$k=0$ is requested we implement it with \method{forall} and
2023
\method{not_}.)
2024
2025
The input formula may be a \class{qformula} as returned by the
2026
methods of \code{qepcad_formula}, a symbolic equality or
2027
inequality, or a polynomial $p$ (meaning $p = 0$).
2028
2029
EXAMPLE::
2030
2031
sage: var('a,b')
2032
(a, b)
2033
sage: qf = qepcad_formula
2034
sage: qf.exactly_k(1, x, x^2 + a*x + b == 0)
2035
(X1 x)[a x + x^2 + b = 0]
2036
sage: qf.exactly_k(0, b, a*b == 1)
2037
(A b)[~a b = 1]
2038
"""
2039
from sage.all import ZZ
2040
k = ZZ(k)
2041
if k < 0:
2042
raise ValueError, "negative k in exactly_k quantifier"
2043
2044
if k == 0:
2045
return self.forall(v, self.not_(formula))
2046
2047
return self.quantifier('X%s' % k, v, formula)
2048
X = exactly_k
2049
2050
def quantifier(self, kind, v, formula, allow_multi=True):
2051
r"""
2052
A helper method for building quantified QEPCAD formulas; not
2053
expected to be called directly.
2054
2055
Takes the quantifier kind (the string label of this quantifier),
2056
a variable or list of variables, and a formula, and returns
2057
the quantified formula.
2058
2059
EXAMPLES::
2060
2061
sage: var('a,b')
2062
(a, b)
2063
sage: qf = qepcad_formula
2064
sage: qf.quantifier('NOT_A_REAL_QEPCAD_QUANTIFIER', a, a*b==0)
2065
(NOT_A_REAL_QEPCAD_QUANTIFIER a)[a b = 0]
2066
sage: qf.quantifier('FOO', (a, b), a*b)
2067
(FOO a)(FOO b)[a b = 0]
2068
"""
2069
2070
formula = self.formula(formula)
2071
2072
if allow_multi and isinstance(v, (list, tuple)):
2073
if len(v) == 0:
2074
return formula
2075
else:
2076
return self.quantifier(kind, v[0],
2077
self.quantifier(kind, v[1:], formula))
2078
2079
form_str = str(formula)
2080
if form_str[-1] != ']':
2081
form_str = '[' + form_str + ']'
2082
v = str(v)
2083
if not (v in formula.vars):
2084
raise ValueError, "Attempting to quantify variable which does not occur in formula"
2085
form_str = "(%s %s)%s" % (kind, v, form_str)
2086
return qformula(form_str, formula.vars - frozenset([v]), [v] + formula.qvars)
2087
2088
2089
qepcad_formula = qepcad_formula_factory()
2090
2091
_qepcad_algebraic_re = \
2092
re.compile(' ?the unique root of (.*) between (.*) and (.*)$')
2093
2094
def _eval_qepcad_algebraic(text):
2095
r"""
2096
Given a string of the form:
2097
'the unique root of 8 x^2 - 8 x - 29 between -47/32 and -1503/1024'
2098
(as produced by QEPCAD) this returns the corresponding \sage
2099
algebraic real number.
2100
2101
Requires that the given rational bounds are exactly representable as
2102
arbitrary-precision floating-point numbers (that is, that the
2103
denominators are powers of two); this is true of the expressions
2104
given by QEPCAD.
2105
2106
EXAMPLES::
2107
2108
sage: from sage.interfaces.qepcad import _eval_qepcad_algebraic
2109
sage: x = _eval_qepcad_algebraic('the unique root of 8 x^2 - 8 x - 29 between -47/32 and -1503/1024'); x
2110
-1.468501968502953?
2111
sage: 8*x^2 - 8*x - 29 == 0
2112
True
2113
"""
2114
from sage.rings.rational_field import QQ
2115
from sage.rings.polynomial.polynomial_ring import polygen
2116
from sage.rings.real_mpfi import RealIntervalField
2117
from sage.rings.qqbar import AA
2118
2119
match = _qepcad_algebraic_re.match(text)
2120
2121
p_text = match.group(1)
2122
lbound = QQ(match.group(2))
2123
ubound = QQ(match.group(3))
2124
2125
p = sage_eval(implicit_mul(p_text), {'x': polygen(QQ)})
2126
2127
for prec_scale in range(15):
2128
fld = RealIntervalField(53 << prec_scale)
2129
intv = fld(lbound, ubound)
2130
if intv.lower().exact_rational() == lbound and intv.upper().exact_rational() == ubound:
2131
return AA.polynomial_root(p, intv)
2132
2133
raise ValueError, "%s or %s not an exact floating-point number"%(lbound, ubound)
2134
2135
class QepcadCell:
2136
r"""
2137
A wrapper for a QEPCAD cell.
2138
"""
2139
def __init__(self, parent, lines):
2140
r"""
2141
Constructs a \class{QepcadCell} wrapper for a QEPCAD cell, given
2142
a \class{Qepcad} object and a list of lines holding QEPCAD's
2143
cell output. This is typically called by the \method{make_cells}
2144
method of \class{Qepcad}.
2145
2146
EXAMPLES::
2147
2148
sage: from sage.interfaces.qepcad import QepcadCell
2149
sage: var('a,b')
2150
(a, b)
2151
sage: qe = qepcad(a^2 + b^2 == 5, interact=True) # optional - qepcad
2152
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2153
QEPCAD object has moved to phase 'Before Projection (b)'
2154
QEPCAD object has moved to phase 'Before Choice'
2155
QEPCAD object has moved to phase 'Before Solution'
2156
sage: qe.d_cell(4, 3) # optional - qepcad
2157
---------- Information about the cell (4,3) ----------
2158
Level : 2
2159
Dimension : 1
2160
Number of children : 0
2161
Truth value : F by trial evaluation.
2162
Degrees after substitution : Not known yet or No polynomial.
2163
Multiplicities : ()
2164
Signs of Projection Factors
2165
Level 1 : (0)
2166
Level 2 : (+)
2167
---------- Sample point ----------
2168
The sample point is in a PRIMITIVE representation.
2169
<BLANKLINE>
2170
alpha = the unique root of x^2 - 5 between 2289/1024 and 1145/512
2171
= 2.2360679775-
2172
<BLANKLINE>
2173
Coordinate 1 = alpha
2174
= 2.2360679775-
2175
Coordinate 2 = 1
2176
= 1.0000000000
2177
----------------------------------------------------
2178
2179
sage: QepcadCell(qe, str(qe.d_cell(4, 3)).splitlines()) # optional - qepcad
2180
QEPCAD cell (4, 3)
2181
"""
2182
self._parent = parent
2183
self._lines = lines
2184
2185
max_level = len(parent._varlist)
2186
2187
all_signs = []
2188
saw_signs = False
2189
2190
saw_primitive = False
2191
saw_extended = False
2192
2193
grab_extended = False
2194
2195
all_coordinates = []
2196
2197
for line in lines:
2198
if 'Information about the cell' in line:
2199
tail = line.split('(')[1]
2200
index = tail.split(')')[0]
2201
if index == '':
2202
index = ()
2203
else:
2204
index = sage_eval(index)
2205
if not isinstance(index, tuple):
2206
index = (index,)
2207
self._index = index
2208
2209
self._dimension = sum([r&1 for r in index])
2210
if 'Level ' in line:
2211
self._level = int(line.split(':')[1].strip())
2212
if 'Number of children' in line:
2213
nkids = int(line.split(':')[1].strip())
2214
if nkids > 0 or self._level == max_level:
2215
self._number_of_children = nkids
2216
else:
2217
self._number_of_children = None
2218
if 'Truth value' in line:
2219
pass # might change
2220
if 'Degrees after substitution' in line:
2221
if self._level == max_level or self._level == 0:
2222
self._degrees = None
2223
else:
2224
self._degrees = sage_eval(line.split(':')[1].strip())
2225
if 'Multiplicities' in line:
2226
self._multiplicities = sage_eval(line.split(':')[1].strip())
2227
if 'Signs of Projection Factors' in line:
2228
saw_signs = True
2229
if saw_signs and 'Level' in line:
2230
(lev, n, colon, signs) = line.split()
2231
assert(lev == 'Level' and colon == ':')
2232
assert(int(n) == len(all_signs) + 1)
2233
signs = signs.replace('+','1').replace('-','-1').replace(')',',)')
2234
all_signs.append(sage_eval(signs))
2235
if 'PRIMITIVE' in line:
2236
saw_primitive = True
2237
if 'EXTENDED' in line:
2238
saw_extended = True
2239
2240
if 'alpha = ' in line:
2241
alpha_text = line[8:]
2242
if 'Coordinate ' in line:
2243
(coord_n, val) = line.split('=')
2244
n = int(coord_n.split()[1])
2245
assert(n == len(all_coordinates) + 1)
2246
if n == self._level and saw_extended:
2247
grab_extended = True
2248
else:
2249
all_coordinates.append(val)
2250
elif grab_extended:
2251
assert('=' in line)
2252
grab_extended = False
2253
all_coordinates.append(line.split('=')[1])
2254
2255
if saw_signs:
2256
self._signs = all_signs
2257
2258
if saw_primitive or saw_extended:
2259
self._raw_sample_point = (saw_extended, alpha_text, all_coordinates)
2260
2261
def __iter__(self):
2262
r"""
2263
Iterate through the stack over a QEPCAD cell.
2264
2265
EXAMPLES::
2266
2267
sage: var('x,y')
2268
(x, y)
2269
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2270
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2271
QEPCAD object has moved to phase 'Before Projection (y)'
2272
QEPCAD object has moved to phase 'Before Choice'
2273
QEPCAD object has moved to phase 'Before Solution'
2274
sage: [c.sample_point() for c in qe.cell(3)] # optional - qepcad
2275
[(0, -3), (0, -1), (0, -1/2), (0, 1), (0, 3)]
2276
"""
2277
for i in range(1, self._number_of_children + 1):
2278
yield self[i]
2279
2280
def __getitem__(self, i):
2281
r"""
2282
Select an element from the stack over a QEPCAD cell.
2283
2284
Note that cells are numbered starting with 1.
2285
2286
EXAMPLES::
2287
2288
sage: var('x,y')
2289
(x, y)
2290
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional
2291
sage: qe.go(); qe.go(); qe.go() # optional
2292
QEPCAD object has moved to phase 'Before Projection (y)'
2293
QEPCAD object has moved to phase 'Before Choice'
2294
QEPCAD object has moved to phase 'Before Solution'
2295
sage: qe.cell(2).__getitem__(3) # optional
2296
QEPCAD cell (2, 3)
2297
"""
2298
return self._parent.cell(self.index() + (i,))
2299
2300
def __len__(self):
2301
r"""
2302
Return the number of elements in the stack over a QEPCAD cell.
2303
(This is always an odd number, if the stack has been constructed.)
2304
2305
EXAMPLES::
2306
2307
sage: var('x,y')
2308
(x, y)
2309
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2310
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2311
QEPCAD object has moved to phase 'Before Projection (y)'
2312
QEPCAD object has moved to phase 'Before Choice'
2313
QEPCAD object has moved to phase 'Before Solution'
2314
sage: len(qe.cell()) # optional - qepcad
2315
5
2316
sage: [len(c) for c in qe.cell()] # optional - qepcad
2317
[1, 3, 5, 3, 1]
2318
"""
2319
return self._number_of_children
2320
2321
def __repr__(self):
2322
r"""
2323
Return a string representation of a QEPCAD cell. Just gives the
2324
cell index.
2325
2326
EXAMPLES::
2327
2328
sage: var('x,y')
2329
(x, y)
2330
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2331
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2332
QEPCAD object has moved to phase 'Before Projection (y)'
2333
QEPCAD object has moved to phase 'Before Choice'
2334
QEPCAD object has moved to phase 'Before Solution'
2335
sage: qe.cell() # optional - qepcad
2336
QEPCAD cell ()
2337
sage: qe.cell(1) # optional - qepcad
2338
QEPCAD cell (1)
2339
sage: qe.cell(2, 2) # optional - qepcad
2340
QEPCAD cell (2, 2)
2341
"""
2342
ind = self.index()
2343
if len(ind) == 1:
2344
ind = '(%s)' % ind[0]
2345
else:
2346
ind = str(ind)
2347
return ('QEPCAD cell %s' % ind)
2348
2349
def index(self):
2350
r"""
2351
Gives the index of a QEPCAD cell.
2352
2353
EXAMPLES::
2354
2355
sage: var('x,y')
2356
(x, y)
2357
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2358
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2359
QEPCAD object has moved to phase 'Before Projection (y)'
2360
QEPCAD object has moved to phase 'Before Choice'
2361
QEPCAD object has moved to phase 'Before Solution'
2362
sage: qe.cell().index() # optional - qepcad
2363
()
2364
sage: qe.cell(1).index() # optional - qepcad
2365
(1,)
2366
sage: qe.cell(2, 2).index() # optional - qepcad
2367
(2, 2)
2368
"""
2369
return self._index
2370
2371
def level(self):
2372
r"""
2373
Returns the level of a QEPCAD cell.
2374
2375
EXAMPLES::
2376
2377
sage: var('x,y')
2378
(x, y)
2379
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2380
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2381
QEPCAD object has moved to phase 'Before Projection (y)'
2382
QEPCAD object has moved to phase 'Before Choice'
2383
QEPCAD object has moved to phase 'Before Solution'
2384
sage: qe.cell().level() # optional - qepcad
2385
0
2386
sage: qe.cell(1).level() # optional - qepcad
2387
1
2388
sage: qe.cell(2, 2).level() # optional - qepcad
2389
2
2390
"""
2391
return self._level
2392
2393
def signs(self):
2394
r"""
2395
Returns the sign vector of a QEPCAD cell. This is a list of lists.
2396
The outer list contains one element for each level of the cell;
2397
the inner list contains one element for each projection factor at
2398
that level. These elements are either -1, 0, or 1.
2399
2400
EXAMPLES::
2401
2402
sage: var('x,y')
2403
(x, y)
2404
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2405
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2406
QEPCAD object has moved to phase 'Before Projection (y)'
2407
QEPCAD object has moved to phase 'Before Choice'
2408
QEPCAD object has moved to phase 'Before Solution'
2409
sage: from sage.interfaces.qepcad import QepcadCell
2410
sage: all_cells = flatten(qe.cell(), ltypes=QepcadCell, max_level=1) # optional - qepcad
2411
sage: [(c, c.signs()[1][0]) for c in all_cells] # optional - qepcad
2412
[(QEPCAD cell (1, 1), 1), (QEPCAD cell (2, 1), 1), (QEPCAD cell (2, 2), 0), (QEPCAD cell (2, 3), 1), (QEPCAD cell (3, 1), 1), (QEPCAD cell (3, 2), 0), (QEPCAD cell (3, 3), -1), (QEPCAD cell (3, 4), 0), (QEPCAD cell (3, 5), 1), (QEPCAD cell (4, 1), 1), (QEPCAD cell (4, 2), 0), (QEPCAD cell (4, 3), 1), (QEPCAD cell (5, 1), 1)]
2413
"""
2414
return self._signs
2415
2416
def number_of_children(self):
2417
r"""
2418
Return the number of elements in the stack over a QEPCAD cell.
2419
(This is always an odd number, if the stack has been constructed.)
2420
2421
EXAMPLES::
2422
2423
sage: var('x,y')
2424
(x, y)
2425
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2426
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2427
QEPCAD object has moved to phase 'Before Projection (y)'
2428
QEPCAD object has moved to phase 'Before Choice'
2429
QEPCAD object has moved to phase 'Before Solution'
2430
sage: qe.cell().number_of_children() # optional - qepcad
2431
5
2432
sage: [c.number_of_children() for c in qe.cell()] # optional - qepcad
2433
[1, 3, 5, 3, 1]
2434
"""
2435
return self._number_of_children
2436
2437
def set_truth(self, v):
2438
r"""
2439
Sets the truth value of this cell, as used by QEPCAD for solution
2440
formula construction.
2441
2442
The argument \var{v} should be either a boolean or \code{None}
2443
(which will set the truth value to ``undetermined'').
2444
2445
EXAMPLES::
2446
2447
sage: var('x,y')
2448
(x, y)
2449
sage: qe = qepcad(x^2 + y^2 == 1, interact=True) # optional - qepcad
2450
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2451
QEPCAD object has moved to phase 'Before Projection (y)'
2452
QEPCAD object has moved to phase 'Before Choice'
2453
QEPCAD object has moved to phase 'Before Solution'
2454
sage: qe.solution_extension('T') # optional - qepcad
2455
y^2 + x^2 - 1 = 0
2456
sage: qe.cell(3, 3).set_truth(True) # optional - qepcad
2457
sage: qe.solution_extension('T') # optional - qepcad
2458
y^2 + x^2 - 1 <= 0
2459
"""
2460
if v is None:
2461
nv = 2
2462
else:
2463
nv = 1 if v else 0
2464
self._parent.set_truth_value(self, nv)
2465
2466
def sample_point(self):
2467
r"""
2468
Returns the coordinates of a point in the cell, as a tuple of
2469
\sage algebraic reals.
2470
2471
EXAMPLES::
2472
2473
sage: qe = qepcad(x^2 - x - 1 == 0, interact=True) # optional - qepcad
2474
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2475
QEPCAD object has moved to phase 'At the end of projection phase'
2476
QEPCAD object has moved to phase 'Before Choice'
2477
QEPCAD object has moved to phase 'Before Solution'
2478
sage: v1 = qe.cell(2).sample_point()[0]; v1 # optional - qepcad
2479
-0.618033988749895?
2480
sage: v2 = qe.cell(4).sample_point()[0]; v2 # optional - qepcad
2481
1.618033988749895?
2482
sage: v1 + v2 == 1 # optional - qepcad
2483
True
2484
"""
2485
try:
2486
return self._sample_point
2487
except AttributeError:
2488
(extended, alpha, coordinates) = self._raw_sample_point
2489
2490
need_alpha = False
2491
for c in coordinates:
2492
if 'alpha' in c:
2493
need_alpha = True
2494
break
2495
2496
if need_alpha:
2497
locals = {'alpha': _eval_qepcad_algebraic(alpha)}
2498
else:
2499
locals = {}
2500
2501
points = []
2502
2503
for c in coordinates:
2504
if 'unique' in c:
2505
points.append(_eval_qepcad_algebraic(c))
2506
else:
2507
points.append(sage_eval(implicit_mul(c), locals))
2508
2509
return tuple(points)
2510
2511
def sample_point_dict(self):
2512
r"""
2513
Returns the coordinates of a point in the cell, as a dictionary
2514
mapping variable names (as strings) to \sage algebraic reals.
2515
2516
EXAMPLES::
2517
2518
sage: qe = qepcad(x^2 - x - 1 == 0, interact=True) # optional - qepcad
2519
sage: qe.go(); qe.go(); qe.go() # optional - qepcad
2520
QEPCAD object has moved to phase 'At the end of projection phase'
2521
QEPCAD object has moved to phase 'Before Choice'
2522
QEPCAD object has moved to phase 'Before Solution'
2523
sage: qe.cell(4).sample_point_dict() # optional - qepcad
2524
{'x': 1.618033988749895?}
2525
"""
2526
points = self.sample_point()
2527
vars = self._parent._varlist
2528
2529
return dict([(vars[i], points[i]) for i in range(len(points))])
2530
2531