There are four procedures (they are in /user/csl/arnon/bin,
so to use them you should put that directory into your search path):

QEINF (user interface; for entering the data for the computation you
want to do)

QEGEN (the cruncher; this constructs the cad and does the qe if
appropriate)

QEDL3 (user interface; for creating a standard cad file)

QETRI (user interface; for creating a covering sets file)

=========

The rest of this document is old.

Here's a sample session with qeinf, entering the data for computation of
a cad of 3-space with the clustering algorithm. qeinf uses the first
argument of the command line ("Mig2" below) as the base of a filename in
which to store the data entered (this file will be "Mig2.infcl" for the
example below). Note that you indicate the choice of clustering vs.
original algorithm in two places, once with the second argument on the
command line ("cl" vs. "or"), and once in the first question that qeinf
asks you ("ENTER 1(ORIGINAL ALG) 3(CLUSTERING)"). This example also
illustrates the syntax that qeinf expects for polynomials, i.e.
multiplication is denoted by blank, exponentiation by "**", and the
polynomial is terminated with a dollar sign "$" . Also, each polynomial
is echoed as it is read.
------------------------------------------------

[d167] qeinf Mig2 cl
ENTER 1(ORIGINAL ALG) 3(CLUSTERING)
3
ENTER VARIABLE LIST
(p,q,r)
ENTER 0(CAD ONLY) OR 1(QE)
0
ENTER NUMBER OF INPUT POLYNOMIALS
5
ENTER POLYNOMIALS
32 r + 3 p q**2 - 8 p**2$

2 2
32 R + 3 P Q - 8 P


256 r**2 - 27 q**4 r + 144 p q**2 r - 128 p**2 r - 4 p**3 q**2 + 16
p**4$

2 4 2 2 3 2 4
256 R - 27 Q R + 144 P Q R - 128 P R - 4 P Q + 16 P


r$

R


9 q**2 - 32 p$


2
9 Q - 32 P


q$

Q

ENTER DIMENSION UP TO WHICH DEFINING FORMULAS TO BE CONSTRUCTED
0

------------------------------------------------
To actually construct the cad, we use qegen, as illustrated below. You
will note that all the user does is type the command line ("qegen Mig2
cl"); everything else is produced by the program.
------------------------------------------------
[d168]qegen Mig2 cl
Thu Nov 21 14:26:36 EST 1985
ENTER 1(ORIGINAL ALG) 3(CLUSTERING)
ENTER VARIABLE LIST
ENTER 0(CAD ONLY) OR 1(QE)
ENTER NUMBER OF INPUT POLYNOMIALS
ENTER POLYNOMIALS
ENTER DIMENSION UP TO WHICH DEFINING FORMULAS TO BE CONSTRUCTED
VALUE OF MU IS 6000

PRIME LIST GENERATION
PRIME LIST HAS LENGTH 521
FIRST PRIME IS 536860913
LAST PRIME IS 536870909

Thu Nov 21 14:37:44 EST 1985
272.5u 35.8s 11:08 46% 567+4642k 19+29io 466pf+0w
[d171]
------------------------------------------------
Finally, to look at the results of this computation, use qedsp, an
interactive, menu-driven display program. Here's the beginning of a
session with qedsp for this example.
------------------------------------------------

[d174] qedsp Mig2 cl
SELECT ITEM (M FOR MENU)
m
T - COMMAND OUTPUT TO TERMINAL (DEFAULT)
W - COMMAND OUTPUT TO OUTPUT FILE
U - CHANGE DEFAULT VARIABLE LIST
H - IDENTIFY ALGORITHM USED TO GENERATE SAVE FILE
F - INPUT FORMULA FOR QUANTIFIER ELIMINATION
K - DEFINING FORMULA CONSTRUCTION FLAG
S L - STATISTICS FOR (RELATIVIZED) CAD OF L-SPACE
R L - L-VARIATE RELATIVIZATION FORMULA (IF ANY)
A L - L-VARIATE CAD INPUT POLYNOMIALS
B L - BASIS FOR L-VARIATE CAD INPUT POLYNOMIALS
N L - CONTENTS OF L-VARIATE CAD INPUT POLYNOMIALS
P L - PROJECTION OF L-VARIATE CAD INPUT POLYNOMIALS
C L - CLUSTERS FOR (RELATIVIZED) CAD OF L-SPACE
I L - ADJACENCIES FOR (RELATIVIZED) CAD OF L-SPACE
D L - SPS AND DFS FOR (RELATIVIZED) CAD OF L-SPACE
G - EQUIVALENT QUANTIFIER-FREE FORMULA (IF ANY)
E - FIND CELLS SATISFYING QUANTIFIER-FREE FORMULA
X - TIME FOR QUANTIFIER ELIMINATION FROM CAD
Z - SET NEW RIGHT MARGIN
Q - EXIT
SELECT ITEM (M FOR MENU)
u
ENTER VARIABLE LIST OF LENGTH 3
(p,q,r)
SELECT ITEM (M FOR MENU)
a3

2 2
32 R + 3 P Q - 8 P


2 4 2 2 3 2 4
256 R - 27 Q R + 144 P Q R - 128 P R - 4 P Q + 16 P



R


2
9 Q - 32 P



Q

SELECT ITEM (M FOR MENU)
s3
(257201,8850) MILLISECONDS (COMPUTE,GC) 127 CELLS, 79 CLUSTERS, 256
ADJACEN
CIES,
(3451,0) MILLISECONDS (SP COMPUTE,GC)
NU = 600000 MU = 6000 LENGTH(PRIME) = 521 GCC = 1 GCCC =
294717 AVER
AGE NO. OF CELLS PER GC = 294717.00
SELECT ITEM (M FOR MENU)
------------------------------------------------
Finally, here's another example of qeinf, illustrating entry of a prenex
formula. The formula begins with a list of quantifiers. "(ap)" below
means 'for all p'; if we wanted existential, we would say "(ep)". The
example below is a decision problem; in general, it is assumed that the
lowest variables in the variable list are free and the highest bound.
Note that vertical bar ("|") is the symbol for OR, and "~=" is the
symbol for NOTEQUAL.
------------------------------------------------
[d186] qeinf Cp14Mig2 or
ENTER 1(ORIGINAL ALG) 3(CLUSTERING)
1
ENTER VARIABLE LIST
(p,q,r,x)
ENTER 0(CAD ONLY) OR 1(QE)
1
ENTER KL = NO. OF FREE VARIABLES
0
ENTER PRENEX FORMULA
(ap)(aq)(ar)(ax)
(
(
(q ~= 0 | r ~= 0 | p < 0) &
( r <= 0 |
( 9 q**2 - 32 p r >= 0 &
( 64 r**2 + 6 p q**2 - 16 p**2 r < 0 |
256R**3 - 128 P**2 R**2 + 144 P Q**2 R
+ 16 P**4 R - 27 Q**4 - 4 P**3 Q**2 < 0
)
)
)
)
|
x **4 + p x**2 + q x + r >= 0
)
&
(
x **4 + p x**2 + q x + r < 0
|
(
(q = 0 & r = 0 & p >= 0) |
( r > 0 &
( 9 q**2 - 32 p r < 0 |
( 64 r**2 + 6 p q**2 - 16 p**2 r >= 0 &
256R**3 - 128 P**2 R**2 + 144 P Q**2 R
+ 16 P**4 R - 27 Q**4 - 4 P**3 Q**2 >= 0
)
)
)
)
)
$


(AP)(AQ)(AR)(AX)( ( ( ( ( Q ~= 0 ) | ( R ~= 0 ) | ( P < 0 ) ) & ( (
R <= 0

2 2 2 2
) | ( ( 32 P R - 9 Q <= 0 ) & ( ( 32 R - 8 P R + 3 P Q < 0 ) | (

3 2 2 2 4 4 3 2
256 R - 128 P R + 144 P Q R + 16 P R - 27 Q - 4 P Q < 0 ) ) ) )
) | (

4 2 4 2
X + P X + Q X + R >= 0 ) ) & ( ( X + P X + Q X + R < 0 ) | ( ( (
Q = 0 )

2
& ( R = 0 ) & ( P >= 0 ) ) | ( ( R > 0 ) & ( ( 32 P R - 9 Q > 0 )
| ( (

2 2 2 3 2 2 2
4
32 R - 8 P R + 3 P Q >= 0 ) & ( 256 R - 128 P R + 144 P Q R +
16 P R

4 3 2
- 27 Q - 4 P Q >= 0 ) ) ) ) ) ) )

[d187]
------------------------------------------------




&