QFFWLS(F,V,n) [Quantifier-free formula write, linear. 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 in a format readable by qffrd. There are no preceding or terminating emptobs, i.e. QFFWLS acts like standard SAC-2 write routines, simply inserting a stream of characters into the output buffer. In order for this to mesh well with diipsr and dirpsr, it is desirable that OSIZE = ISIZE; then e.g. very long coefficients will split across lines in such a way that they are readable.] const ANDOP=10, OROP=11, EQOP=1, NEOP=2. const LTOP=3, LEOP=4, GTOP=5, GEOP=6. (1) [Determine operator.] F'=F; ADV(F';R,F'). (2) [Atomic formula.] if R~=ANDOP&R~=OROP then { A=FIRST(F'); CWRIT2('(',' '); r=LENGTH(V); A'=SDIPFP(r,A); DIPSWL(A',V,n); 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 4 }. (3) [Disjunction or conjunction.] CWRIT2('(',' '); repeat { ADV(F';F#,F'); if n==1 then QFFWLS(F#,V,1) else QFFWLS(F#,V,0); if F'~=() then { if R==OROP then CWRIT3(' ','|',' ') else CWRIT3(' ','&',' ') } } until F'==(). (4) [Finish.] CWRIT2(' ',')'); return.. #Jf