F=QFFRDA(V)
[Quantifier-free formula read, atomic formula. V is a variable
list of length r>=1. A quantifier-free atomic formula whose
variables all occur in V is read from the input stream and
assigned to F.]
const EQOP=1,NEOP=2,LTOP=3.
const LEOP=4,GTOP=5,GEOP=6.
safe C,R,r,i,s.
(1) [Read first part of polynomial.]
L1=LIST4('<','>','=','~');
L2=LIST4('&','|',')','$'); P1=RPSRF(V,L1);
(2) [Read operator.] C=CREAD(); i=LSRCH(C,L1); if i==0
then { print "illegal operator"; go to 4 }; D=CREADB();
case C of { '<' do if D=='=' then R=LEOP
else { R=LTOP; BKSP }; '>' do if D=='=' then
R=GEOP else { R=GTOP; BKSP }; '=' do { R=EQOP; BKSP };
'~' do if D=='=' then R=NEOP else
{ print "~ must be followed by ="; go to 4 } }.
(3) $[Read second part of polynomial and finish]
P2=RPSRF(V,L2);
r=LENGTH(V); P=RPDIF(r,P1,P2); IPSRP(r,P;a,P);
s=RNSIGN(a); if s<0 then case R of
{ EQOP do R=R; NEOP do R=R;
LTOP do R=GTOP; LEOP do R=GEOP; GTOP do R=LTOP;
GEOP do R=LEOP }; F=LIST2(R,P); return.
(4) $[Error exit.] DIBUFF;
print "reading through next atomic formula terminator";
while LSRCH(C,L2)==0 do C=CREADB(); BKSP;
print "the formula 0=0 returned"; F=LIST2(EQOP,0);
return..