QFFWRS(F,V,n)
[Quantifier-free formula write subroutine. F is a quantifier-free
formula whose polynomials are either rational or integral polynomials.
V is a variable list for F. n==1 if the polynomials of F are
rational polynomials and n==0 if the polynomials of F are integral.
F is written in the output stream. The global array G is
used for storage of auxiliary information. At entry the global
variable g is the current largest active element of G.
At exit g is the new largest active element of G.]
const PSIZE=57.
const ANDOP=10, OROP=11, EQOP=1, NEOP=2.
const LTOP=3, LEOP=4, GTOP=5, GEOP=6.
safe G,g.
global G[80].
global g.
safe W[10].
safe r,i,s,j,x,y,m1,m2,b,z.
(1) [Determine operator.] F'=F;
ADV(F';R,F').
(2) [Begin atomic formula.] if R~=ANDOP&R~=OROP then
{ A=FIRST(F'); if OPOS>=RMARG-2 then
POLWR(PSIZE-3); CWRIT2('(',' '); if A==0 then
{ if OPOS>=RMARG-2 then POLWR(PSIZE-3);
CWRIT2('0',' '); go to 6 }; if V==() then
{ if n==1 then { FIRST2(A;c1,c2); m1=3 }
else { c1=A; m1=2 }; IFCL2(c1;x,y);
if y==0 then m1=m1+1 else m1=m1+(y+2)/3;
if n==1 then { IFCL2(c2;x,y); m1=m1+(y+2)/3 };
if OPOS>=RMARG-m1 then POLWR(PSIZE-3);
if n==1 then RNWRIT(A) else IWRITE(A); CWRITE(' ');
go to 6 } } else go to 7.
(3) [Initialize for nonconstant polynomial.] r=LENGTH(V);
V'=V; for i=1,...,r do ADV(V';W[i],V');
A'=SDIPFP(r,A); b=1; U=RNINT(1).
(4) [Determine whether next term will fit on current
output line.] if A'==() then go to 6;
FIRST2(A';c,d); if n==1 then { FIRST2(c;c1,c2); m1=4 }
else { c1=c; m1=3 }; IFCL2(c1;x,y);
if y==0 then m1=m1+1 else m1=m1+(y+2)/3;
if n==1 then { IFCL2(c2;x,y);
m1=m1+(y+2)/3 }; m2=0;
while d~=() do { ADV2(d;j,e,d); m2=m2+LENGTH(W[j]);
IFCL2(e;x,y); m2=m2+((y+2)/3)+1 };
if (RMARG-OPOS)<=(m1+m2)&OPOS>LMARG
then POLWR(PSIZE-3);
if (RMARG-OPOS)<=(m1+m2) then
{ CLOUT("term skipped -- requires ");
AWRITE(m1+m2); CLOUT(" columns. LMARG is ");
AWRITE(LMARG); CLOUT(", RMARG is ");
AWRITE(RMARG); emptob; A'=RED2(A'); go to 4 }.
(5) [Write next term.] ADV2(A';c,d,A');
if n==1 then { s=RNSIGN(c); c=RNABS(c) }
else { s=ISIGNF(c); c=IABSF(c) };
if s<0 then CWRITE('-') else if b==0
then CWRITE('+'); CWRITE(' '); b=0;
if n==1&RNCOMP(c,U)~=0 then
{ RNWRIT(c); CWRITE(' ') }
else if n==0&c~=1 then { IWRITE(c); CWRITE(' ') };
z=1; d=CINV(d);
while d~=() do { z=0; ADV2(d;e,j,d); CLOUT(W[j]);
if e>1 then { G[g+1]=OPOS+1; AWRITE(e); G[g+2]=OPOS;
g=g+2 }; CWRITE(' ') };
if z==1&((n==1&RNCOMP(c,U)==0)
|(n==0&c==1)) then
{ AWRITE(1); CWRITE(' ') }; go to 4.
(6) [Finish atomic formula.] if OPOS>=(RMARG-4) then
POLWR(PSIZE-3); case R of { EQOP do CWRITE('=');
NEOP do CWRIT2('~','='); LTOP do CWRITE('<');
LEOP do CWRIT2('<','='); GTOP do CWRITE('>');
GEOP do CWRIT2('>','=') }; CWRIT2(' ','0'); go to 8.
(7) [Disjunction or conjunction.] if OPOS>=RMARG-2 then
POLWR(PSIZE-3); CWRIT2('(',' '); repeat
{ ADV(F';F#,F'); if n==1 then QFFWRS(F#,V,1)
else QFFWRS(F#,V,0); if F'~=() then
{ if OPOS>=RMARG-3 then POLWR(PSIZE-3);
if R==OROP then CWRIT3(' ','|',' ') else
CWRIT3(' ','&',' ') } } until F'==().
(8) [Finish.] if OPOS>=RMARG-2 then POLWR(PSIZE-3);
CWRIT2(' ',')'); return..