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.. #Jf