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.. Ê#˜JšÏf¹ ˜¹ —…—<e