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