F=QFFRD(V)
[Quantifier-free formula read. V is a variable list of length
r>=1. A q.f.f. whose variables all occur in V is read from the
input stream and assigned to F.]
const ANDOP=10, OROP=11, EQOP=1.
safe C.
(1) [Read first term.] C=CREADB(); if BEGAF(C)==1
then { BKSP; F#=QFFRDA(V) } else if C=='(' then
{ F#=QFFRD(V); if CREADB()~=')' then
{ print "right parenthesis expected"; go to 5 } }
else { print "unexpected character"; go to 5 };
F=LIST1(F#); C=CREADB().
(2) [Next disjunct.] if C==')'|C=='$' then go to 4;
if C=='&' then { ADV(F;G#,F); G=LIST1(G#); go to 3 };
if C=='|' then { C=CREADB(); if BEGAF(C)==1 then
{ BKSP; F#=QFFRDA(V) } else if C=='(' then
{ F#=QFFRD(V); if CREADB()~=')' then
{ print "right parenthesis expected"; go to 5 } }
else { print "unexpected character"; go to 5 };
F=COMP(F#,F); C=CREADB(); go to 2 };
print "unexpected character"; go to 5.
(3) [Next conjunct.] if C=='|'|C=')'|C='$' then
{ G=INV(G); G=COMP(ANDOP,G); F=COMP(G,F);
go to 2 }; if C=='&' then { C=CREADB();
if BEGAF(C)==1 then { BKSP; G#=QFFRDA(V) } else
if C=='(' then { G#=QFFRD(V);
if CREADB()~=')' then
{ print "right parenthesis expected"; go to 5 } }
else { print "unexpected character"; go to 5 };
G=COMP(G#,G); C=CREADB();
go to 3 }; print "unexpected character"; go to 5.
(4) [Exit.] if C==')' then BKSP; if LENGTH(F)==1 then
F=FIRST(F) else { F=INV(F); F=COMP(OROP,F) };
return.
(5) [Error exit.] DIBUFF; print "reading through next $";
while C~='$' do C=CREADB();
print "the q.f.f. 0=0 returned"; F=LIST2(EQOP,0);
return..