~trn/reduce-algebra

06140e0ae2f53dfc77ca5ae5c0a265bd46d42dbd — Jeffrey H. Johnson 15 days ago 52bf8b3 + df188ac
Merge branch 'svn/trunk'
M packages/redlog/cl/clqe.red => packages/redlog/cl/clqe.red +2 -46
@@ 70,9 70,6 @@ procedure containerP(x);
% Point ::= (Coordinate, ...)
% Coordinate ::= Equation (* Kernel = Integer *)

struct Point asserted by listp;


%DS
% EliminationResult ::= (Theory . ExtendedQeResult)
% ExtendedQeResult ::= (..., (QfFormula, SamplePoint), ...)


@@ 335,38 332,6 @@ asserted procedure cl_gqea(f: Formula, theo: Theory, xbvl: KernelL): Elimination
      return cl_mkER(theo, eqr)
   end;

rl_provideService rl_lqe = cl_lqe using rl_negateat, rl_translat, rl_elimset,
   rl_elimset, rl_trygauss, rl_varsel, rl_betterp, rl_qemkans, rl_transform,
   rl_subat, rl_qefsolset, rl_bettergaussp, rl_esetunion, rl_bestgaussp,
   rl_specelim, rl_fbqe;

asserted procedure cl_lqe(f: Formula, theo: Theory, pt: Point): TheoryFormulaPair;
   % Local quantifier elimination. [pt] is the suggested value for the local
   % parameter $v$. Returns a pair $\Theta . \phi$. $\Theta$ extends [theo];
   % $\phi$ is a formula. We have $\Theta \models [f] \longleftrightarrow \phi$.
   % $\phi$ is obtained from [f] by eliminating as much quantifiers as possible.
   % Accesses the switch [rlqepnf]; if [rlqepnf] is on, then [f] has to be
   % prenex. Accesses the fluids [cl_pal!*], [cl_lps!*], and [cl_theo!*].
   % [cl_lps!*] is the list of local parameters; [cl_pal] is an Alist containing
   % the suggested values for the local parameters; and [cl_theo!*] is the
   % theory generated by the local quantifier elimination.
   begin scalar w, er, theo, !*rlqelocal, !*rlsipw, !*rlsipo, cl_pal!*, cl_lps!*, cl_theo!*;
      !*rlsipw := !*rlqelocal := t;
      cl_pal!* := pt;
      cl_lps!* := for each x in pt collect car x;
      cl_theo!* := nil;
      w := for each x in theo collect rl_subat(cl_pal!*, x);
      w := rl_simpl(rl_smkn('and, w), nil, -1);
      if w eq 'false then
         rederr "rllqe: inconsistent theory";
      er := cl_qe1(f, theo, nil);
      theo := nconc(cl_theo!*, theo);
      cl_pal!* := cl_lps!* := cl_theo!* := nil;
      if rl_exceptionp er then
         return er;
      return rl_lthsimpl(theo) . rl_simpl(caar cl_erEQR er, theo, -1)
   end;

rl_provideService rl_qe = cl_qe using rl_negateat, rl_translat, rl_elimset,
   rl_elimset, rl_trygauss, rl_varsel, rl_betterp, rl_qemkans, rl_transform,
   rl_qefsolset, rl_bettergaussp, rl_bestgaussp, rl_esetunion, rl_specelim,


@@ 714,8 679,6 @@ asserted procedure cl_qevar(f: QfFormula, vl: KernelL, an: Answer, theo: Theory,
         return (t . w) . theo;
      if status eq 'failed then
         return (nil . w) . theo;
      if status eq 'local then
         return (t . car w) . cl_theo!*;
      if status eq 'elim then
         return (t . car w) . cdr w;
      rederr {"cl_qevar: bad status", status}


@@ 741,10 704,7 @@ asserted procedure cl_gauss(f: QfFormula, vl: KernelL, an: Answer, theo: Theory,
            ioto_prin2 "g";
         vl := lto_delq(car w, vl);
         ww := cl_esetsubst(f, car w, cdr w, vl, an, theo, ans, bvl);
         if !*rlqelocal then
            return (t . car ww) . cl_theo!*
         else
            return (t . car ww) . cdr ww
         return (t . car ww) . cdr ww
      >>
   end;



@@ 779,11 739,7 @@ asserted procedure cl_process!-candvl(f: QfFormula, vl: KernelL, an: Answer, the
            if !*rlverbose and (not !*rlqedfs or !*rlqevbold) then
               ioto_prin2 "e";
            ww := cl_esetsubst(f, v, rl_elimset(v, alp), lto_delq(v, vl), an, theo, ans, bvl);
            if !*rlqelocal then <<
               candvl := nil;
               w := ww;
               status := 'local
            >> else if rl_betterp(ww, w) then <<
            if rl_betterp(ww, w) then <<
               w := ww;
               status := 'elim
            >>

M packages/redlog/ofsf/ofsf.red => packages/redlog/ofsf/ofsf.red +1 -1
@@ 218,7 218,7 @@ put('ofsf,'rl_services,'(
   (rl_cad!* . ofsf_cad)
   (rl_gcad!* . ofsf_gcad)
   (rl_cadswitches!* . ofsf_cadswitches)
   (rl_lqe!* . cl_lqe)
   (rl_lqe!* . ofsf_lqe)
   (rl_xqe!* . ofsf_xopt!-qe)
   (rl_xqea!* . ofsf_xopt!-qea)
   (rl_lthsimpl!* . ofsf_lthsimpl)

M packages/redlog/ofsf/ofsf.rlg => packages/redlog/ofsf/ofsf.rlg +86 -0
@@ 125,6 125,92 @@ rlghqe phi;
 not(2*a  - 2*a*c + b  = 0 or (a <> 0 and 4*a*c - b  > 0))}


% Local QE Examples from https://doi.org/10.1145/345542.345589
generic_quadratic_equation := ex(x, v2*x^2 + v1*x + v0 = 0)$


rllqe(generic_quadratic_equation, {}, {v2=1, v1=1, v0=1});


                      2
{{v2 <> 0,4*v0*v2 - v1  > 0},v0 = 0}


generic_polygon3 := ex({x, y},
   for i:=1:3 mkand mkid(a, i)*x + mkid(b, i)*y <= mkid(c, i))$


rllqe(generic_polygon3, {}, {a1=1, a2=-3, a3=5, b1=-7, b2=11, b3=-13});


{{b3 < 0,

  b2 > 0,

  b1 < 0,

  a3 > 0,

  a2 < 0,

  a2*b3 - a3*b2 < 0,

  a1 > 0,

  a1*b2 - a2*b1 < 0},

      2                                                                   2
 a1*b2 *c3 - a1*b2*b3*c2 - a2*b1*b2*c3 + a2*b2*b3*c1 + a3*b1*b2*c2 - a3*b2 *c1

  <= 0}


generic_polygon10 := ex({x, y},
   for i:=1:10 mkand mkid(a, i)*x + mkid(b, i)*y <= mkid(c, i))$


generic_polygon10_p := {
   a1=2,a2=-3,a3=5,a4=-7,a5=11,a6=-13,a7=17,a8=-19,a9=23,a10=-29,
   b1=31,b2=-37,b3=41,b4=-43,b5=47,b6=-53,b7=59,b8=-61,b9=67,b10=-71}$


generic_polygon10_sol := rllqe(generic_polygon10, {}, generic_polygon10_p)$


length first generic_polygon10_sol;


55

rlatnum second generic_polygon10_sol;


160


kahans_problem := all({x,y},
   b**2*(x-c)**2+a**2*(y-d)**2-a**2*b**2=0 impl x**2+y**2-1 <=0)$


rllqe(sub(d=0, kahans_problem), {}, {a=1/2, b=1/2, c=1/2});


   2
{{b  <> 0,

   2
  b *c > 0,

   2
  a  > 0,

   2    2
  a  - b  = 0},

  2            2               2            2
 a  - 2*a*c + c  - 1 <= 0 and a  + 2*a*c + c  - 1 <= 0}


% Examples from a talk on Isabel by T. Nipkow
wnip := rlall(a>=3/4 and a^2<=b*(c+1) and b<=4c impl (a-1)^2<b*c)$


M packages/redlog/ofsf/ofsf.tst => packages/redlog/ofsf/ofsf.tst +21 -0
@@ 17,6 17,27 @@ rlgcad phi;
rlhqe phi;
rlghqe phi;

% Local QE Examples from https://doi.org/10.1145/345542.345589
generic_quadratic_equation := ex(x, v2*x^2 + v1*x + v0 = 0)$
rllqe(generic_quadratic_equation, {}, {v2=1, v1=1, v0=1});

generic_polygon3 := ex({x, y},
   for i:=1:3 mkand mkid(a, i)*x + mkid(b, i)*y <= mkid(c, i))$
rllqe(generic_polygon3, {}, {a1=1, a2=-3, a3=5, b1=-7, b2=11, b3=-13});

generic_polygon10 := ex({x, y},
   for i:=1:10 mkand mkid(a, i)*x + mkid(b, i)*y <= mkid(c, i))$
generic_polygon10_p := {
   a1=2,a2=-3,a3=5,a4=-7,a5=11,a6=-13,a7=17,a8=-19,a9=23,a10=-29,
   b1=31,b2=-37,b3=41,b4=-43,b5=47,b6=-53,b7=59,b8=-61,b9=67,b10=-71}$
generic_polygon10_sol := rllqe(generic_polygon10, {}, generic_polygon10_p)$
length first generic_polygon10_sol;
rlatnum second generic_polygon10_sol;

kahans_problem := all({x,y},
   b**2*(x-c)**2+a**2*(y-d)**2-a**2*b**2=0 impl x**2+y**2-1 <=0)$
rllqe(sub(d=0, kahans_problem), {}, {a=1/2, b=1/2, c=1/2});

% Examples from a talk on Isabel by T. Nipkow
wnip := rlall(a>=3/4 and a^2<=b*(c+1) and b<=4c impl (a-1)^2<b*c)$
rlqe wnip;

M packages/redlog/ofsf/ofsfqe.red => packages/redlog/ofsf/ofsfqe.red +37 -0
@@ 85,6 85,43 @@ procedure ofsf_qea(f,theo);
      cl_qea(f,theo)
   >>;

%% rl_provideService rl_lqe = cl_lqe using rl_negateat, rl_translat, rl_elimset,
%%    rl_elimset, rl_trygauss, rl_varsel, rl_betterp, rl_qemkans, rl_transform,
%%    rl_subat, rl_qefsolset, rl_bettergaussp, rl_esetunion, rl_bestgaussp,
%%    rl_specelim, rl_fbqe;

asserted procedure ofsf_lqe(f: Formula, theo: Theory, pt: Alist): TheoryFormulaPair;
   % Local quantifier elimination. [pt] is the suggested value for the local
   % parameter $v$. Returns a pair $\Theta . \phi$. $\Theta$ extends [theo];
   % $\phi$ is a formula. We have $\Theta \models [f] \longleftrightarrow \phi$.
   % $\phi$ is obtained from [f] by eliminating as much quantifiers as possible.
   % Accesses the switch [rlqepnf]; if [rlqepnf] is on, then [f] has to be
   % prenex. Accesses the fluids [cl_pal!*], [cl_lps!*], and [cl_theo!*].
   % [cl_lps!*] is the list of local parameters; [cl_pal] is an Alist containing
   % the suggested values for the local parameters; and [cl_theo!*] is the
   % theory generated by the local quantifier elimination.
   begin scalar w, er, theo, !*rlqelocal, !*rlqevarseltry, !*rlsipw, !*rlsipo, cl_pal!*, cl_lps!*, cl_theo!*;
      !*rlqelocal := t;
      !*rlqevarseltry := nil;  % fluid cl_theo!* prohibits looping in cl_process!-candvl()
      !*rlsipw := t;
      !*rlsipo := nil;
      cl_pal!* := pt;
      cl_lps!* := for each x in pt collect car x;
      cl_theo!* := nil;
      w := for each x in theo collect rl_subat(cl_pal!*, x);
      w := rl_simpl(rl_smkn('and, w), nil, -1);
      if w eq 'false then
         rederr "rllqe: inconsistent theory";
      er := cl_qe1(f, theo, nil);
      % We ignore the theory returned as cdr er, and use cl_theo!* instead. It
      % does not contain the input theory yet.
      theo := nconc(cl_theo!*, theo);
      cl_pal!* := cl_lps!* := cl_theo!* := nil;
      if rl_exceptionp er then
         return er;
      return rl_lthsimpl(theo) . rl_simpl(caar cl_erEQR er, theo, -1)
   end;

procedure ofsf_varsel(f,vl,theo);
   % Ordered field standard form variable selection. [vl] is a list of
   % variables; [f] is a quantifier-free formula; [theo] is the

M packages/redlog/qqe_ofsf/qqe_ofsf.red => packages/redlog/qqe_ofsf/qqe_ofsf.red +0 -2
@@ 146,11 146,9 @@ put('qqe_ofsf,'rl_services,'(
%%   (rl_cad!* . ofsf_cad) % later
%%   (rl_gcad!* . ofsf_gcad) % later
%%   (rl_cadswitches!* . ofsf_cadswitches)
   (rl_lqe!* . cl_lqe)
   (rl_xqe!* . ofsf_xopt!-qe)
   (rl_xqea!* . ofsf_xopt!-qea)
   (rl_lthsimpl!* . ofsf_lthsimpl) %% belongs to qe
   (rl_lthsimpl!* . ofsf_lthsimpl)
   (rl_quine!* . cl_quine)
%%   (rl_cadporder!* . ofsf_cadporder)
%%   (rl_gcadporder!* . ofsf_gcadporder)

M packages/redlog/rl/rlami.red => packages/redlog/rl/rlami.red +118 -119
@@ 21,90 21,91 @@ copyright('rlami, "(c) 1995-2009 A. Dolzmann, T. Sturm, 2017 T. Sturm");
% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 
% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
%

procedure rl_mk!*fof(u);
   % Reduce logic make tagged form of first-order formula. [u] is a
   % first-order formula. Returns pseudo Lisp prefix of [u]. This is
   % analogous to [mk!*sq] in [alg.red].
% LispPrefixForm is specified in assert/assertchkfn.red. A PseudoPrefixForm
% has as its car a tag, which carries relevant information on processing such
% a form. A classical example is the !*sq tag for standard quotients. We use
% here !*fof for first-orderformulas. A MixedPrefixForm is a LispPrefixForm
% possibly containing PseudoPrefixForms as subexpressions.

struct MixedPrefixForm asserted by mixedPrefixFormP;
struct PseudoPrefixForm asserted by pairp;

procedure mixedPrefixFormP(x);
   atom x or pairp x;

asserted procedure rl_mk!*fof(u: Formula): PseudoPrefixForm;
   % Reduce logic make tagged form of first-order formula. Convert u to pseudo
   % Lisp prefix after optional simplification.
   rl_mk!*fof1 rl_csimpl u;

procedure rl_mk!*fof1(u);
   % Reduce logic make tagged form of first-order formula subroutine.
   % [u] is a first-order formula. Returns pseudo Lisp prefix of [u].
   % This is analogous to [mk!*sq] in [alg.red].
asserted procedure rl_mk!*fof1(u: Formula): PseudoPrefixForm;
   % Reduce logic make tagged form of first-order formula subroutine. Convert
   % u to pseudo Lisp prefix. This is analogous to mk!*sq in alg.red.
   if rl_tvalp u then
      u
   else if eqcar(u,'equal) then
   else if eqcar(u, 'equal) then
      rl_prepfof1 u
   else
      '!*fof . rl_cid!* . u . if !*resubs then !*sqvar!* else {nil};

procedure rl_reval(u,v);
   % Reduce logic [reval]. [u] is a formula in some mixed pseudo Lisp
   % prefix form where [car u] is either ['!*fof] or a first-order
   % operator; [v] is bool. Returns Lisp prefix of [u] in case [v] is
   % non-[nil], and pseudo Lisp prefix of [u] else.
asserted procedure rl_reval(u: MixedPrefixForm, v: ExtraBoolean);
   % Reduce logic reval. Convert u to Lisp prefix if v is non-nil, and to
   % pseudo prefix else.
   if v then rl_prepfof rl_simp1 u else rl_mk!*fof rl_simp1 u;

procedure rl_csimpl(u);
asserted procedure rl_csimpl(u: Formula): Formula;
   % Conditional simplify.
   if !*rlsimpl and getd 'rl_simpl then %???
      rl_simpl(u,{},-1)
   if !*rlsimpl and getd 'rl_simpl then
      rl_simpl(u, {}, -1)
   else
      u;

procedure rl_prepfof(f);
   % [prep] first-order with bounded quantifers formula.
asserted procedure rl_prepfof(f: Formula): LispPrefixForm;
   % prep f (in the sense of prepf, prepsq), after optional simplification.
   rl_prepfof1 rl_csimpl f;

procedure rl_prepfof1(f);
   % [prep] first-order formula with bounded quantifers subroutine.
   begin scalar op,w;
asserted procedure rl_prepfof1(f: Formula): LispPrefixForm;
   % prep f (in the sense of prepf, prepsq).
   begin scalar op;
      op := rl_op f;
      if rl_tvalp op then
         return op;
      if rl_quap op then
         return {op,rl_var f,rl_prepfof1 rl_mat f};
         return {op, rl_var f, rl_prepfof1 rl_mat f};
      if rl_bquap op then
         return {op,rl_var f,rl_prepfof1 rl_b f,rl_prepfof1 rl_mat f};
         return {op, rl_var f, rl_prepfof1 rl_b f, rl_prepfof1 rl_mat f};
      if rl_boolp op then
         return op . for each x in rl_argn f collect rl_prepfof1 x;
      % [f] is atomic.
      return apply(get(car rl_cid!*,'rl_prepat),{f})
      % f is an atomic formula
      return apply(get(car rl_cid!*, 'rl_prepat), {f})
   end;

asserted procedure rl_cleanup(u: Any, v: ExtraBoolean): Any;
   % This is bound to the property [cleanupfn] of the rl_service!$ functions
   % that are in turn the [psopfn] of the corresponding rlservice AM
   % entrypoints. The [cleanupfn] is used with the evaluation of [psopfn] in
   % [reval1] in [alg/reval.red], where it converts - in the right moment - the
   % result of of rl_service!$ to Lisp prefix so that [part(rlservice(...),
   % ...)] works properly. However, the final evaluation result is generally
   % Pseudo Lisp Prefix.
   reval1(u,v);

procedure rl_simpa(u);
   % simp an answer structure
   for each a in cdr reval u collect
      {rl_simp cadr a,
         for each b in cdaddr a collect
            rl_simp b, cdr cadddr a};

procedure rl_simp(u);
   % [simp] first-order formula.
asserted procedure rl_cleanup(u, v: ExtraBoolean);
   % This is bound to the property 'cleanupfn of the rl_service!$ functions
   % that are in turn the psopfn of the corresponding rlservice AM
   % entrypoints. The cleanupfn is used with the evaluation of psopfn in
   % reval1 in alg/reval.red, where it converts - in the right moment - the
   % result of of rl_service!$ to Lisp prefix so that part(rlservice(...), 
   % ...) works properly. However, the final evaluation result is generally
   % pseudo prefix.
   reval1(u, v);

asserted procedure rl_simp(u: MixedPrefixForm): Formula;
   % simp to formula (in the sense of simp to standard quotient), after
   % conditional simplification.
   rl_csimpl rl_simp1 u;

procedure rl_simp1(u);
   % Reduce logic [simp]. [u] is (pseudo) Lisp prefix of a formula.
   % Returns the formula encoded by [u].
asserted procedure rl_simp1(u: MixedPrefixForm): Formula;
   % simp to formula (in the sense of simp to standard quotient).
   begin scalar w, h;
      if null rl_cid!* then rederr {"select a context"};
      if atom u then


@@ 132,74 133,72 @@ procedure rl_simp1(u);
      return rl_simp1(u)
   end;

procedure rl_simpatom(u);
   % Reduce logic simp atom. [u] is an atom.
asserted procedure rl_simpatom(u: Atom): Formula;
   % simp atom to formula.
   begin scalar w;
      if null u then typerr("nil","logical");
      if numberp u then typerr({"number",u},"logical");
      if stringp u then typerr({"string",u},"logical");
      if null u then typerr("nil", "logical");
      if numberp u then typerr({"number", u}, "logical");
      if stringp u then typerr({"string", u}, "logical");
      if rl_tvalp u then return u;
      if (w := rl_gettype(u)) then <<
         if w memq '(logical equation scalar slprog) then
            return rl_simp1 cadr get(u,'avalue);
         typerr({w,u},"logical")
         if w eq 'logical or w eq 'equation or w eq 'scalar then
            return rl_simp1 cadr get(u, 'avalue);
         typerr({w, u}, "logical")
      >>;
      % [u] algebraically unbound.
      % u is algebraically unbound.
      if boundp u then return rl_simp1 eval u;
      typerr({"unbound id",u},"logical")
      typerr({"unbound id", u}, "logical")
   end;

procedure rl_simpbop(f);
   % Reduce logic simp boolean operator.
   rl_mkn(car f,for each x in cdr f collect rl_simp1 x);
asserted procedure rl_simpbop(f: MixedPrefixForm): Formula;
   % simp form that starts with a boolean operator.
   rl_mkn(car f, for each x in cdr f collect rl_simp1 x);

procedure rl_simpq(f);
   % Reduce logic simp quantifier.
   begin scalar vl,w;
asserted procedure rl_simpq(f: MixedPrefixForm): Formula;
   % simp form that starts with a quantifier.
   begin scalar vl, w;
      vl := reval cadr f;
      if eqcar(vl,'list) then
      if eqcar(vl, 'list) then
         vl := cdr vl
      else
         vl := {vl};
      w := rl_simp1 caddr f;
      for each x in reverse vl do <<
         rl_qvarchk x;
         w := rl_mkq(car f,x,w)
         w := rl_mkq(car f, x, w)
      >>;
      flag(vl,'used!*);
      flag(vl, 'used!*);
      return w
   end;

procedure rl_simpbq(f);
   % Reduce logic simp bounded quantifier. [f] is a list [(Q,x,b,f)]
   % where [Q] is a quantifier, [x] is an id, and [b] and [f] are
   % lisp-prefix. Returns a bounded quantifier headed formula.
   begin scalar x,wb,wf;
asserted procedure rl_simpbq(f: MixedPrefixForm): Formula;
   % simp form that starts with a bounded quantifier.
   begin scalar x, wb, wf;
      if car rl_cid!* neq 'pasf then
         rederr "boundend quantifiers only allowed within PASF context";
      x := reval cadr f;
      if not idp x then typerr("not identifer","bounded quantified variable");
      if not idp x then typerr("not identifer", "bounded quantified variable");
      wb := rl_simp1 caddr f;
      %%% test, wether x is the only free variable in [wb].
      wf := rl_simp1 cadddr f;
      % Test, wether the bounded quantifier has a finite solution set.
      % rl_bsatp fails per definition if that is not the case.
      rl_bsatp(wb,x);
      flag({x},'used!*);
      return rl_mkbq(car f,x,wb,wf)
      rl_bsatp(wb, x);
      flag({x}, 'used!*);
      return rl_mkbq(car f, x, wb, wf)
   end;

procedure rl_qvarchk(v);
asserted procedure rl_qvarchk(v: Any): Void;
   % Syntax-check quantified variable.
   if not sfto_kernelp v or (!*rlbrkcxk and pairp v) then
      typerr(v,"quantified variable");

procedure rl_simp!*fof(u);
   % Reduce logic simp [!*fof] operator. [u] is of the form
   % $([tag],f,[!*sqvar!*])$ where [tag] is a context tag and $f$ is a
   % formula.
   begin scalar tag,f,w;
      if caddr u then return cadr u;  % [!*sqvar!*=T]
      typerr(v, "quantified variable");

asserted procedure rl_simp!*fof(u: List): Formula;
   % simp form that starts with !*fof. The leading !*fof has already gone, and
   % u is its argument list of the form (tag, f, !*sqvar!*) where tag is a
   % context tag and f is an already simped formula.
   begin scalar tag, f, w;
      if caddr u then return cadr u;  % !*sqvar!* = T
      tag := car u;
      f := cadr u;
      if tag neq rl_cid!* then <<


@@ 213,30 212,30 @@ procedure rl_simp!*fof(u);

procedure rl_resimp(u);
   % Reduce logic resimp. [u] is a formula.
   begin scalar op,w;
   begin scalar op, w;
      op := rl_op u;
      if rl_tvalp op then
         return u;
      if rl_quap op then <<
         if (w := rl_gettype(rl_var u)) then
            typerr({w,rl_var u},"quantified variable");
            typerr({w, rl_var u}, "quantified variable");
         rl_qvarchk rl_var u;
         return rl_mkq(op,rl_var u,rl_resimp rl_mat u)
         return rl_mkq(op, rl_var u, rl_resimp rl_mat u)
      >>;
      if rl_bquap op then <<
         if (w := rl_gettype(rl_var u)) then
            typerr({w,rl_var u},"quantified variable");
         return rl_mkbq(op,rl_var u,rl_resimp rl_b u,rl_resimp rl_mat u)
            typerr({w, rl_var u}, "quantified variable");
         return rl_mkbq(op, rl_var u, rl_resimp rl_b u, rl_resimp rl_mat u)
      >>;
      if rl_boolp op then
         return rl_mkn(op,for each x in rl_argn u collect rl_resimp x);
      return apply(get(car rl_cid!*,'rl_resimpat),{u})
         return rl_mkn(op, for each x in rl_argn u collect rl_resimp x);
      return apply(get(car rl_cid!*, 'rl_resimpat), {u})
   end;

procedure rl_gettype(v);
   % Get type. Return type information if present. Handle scalars
   % properly.
   (if w then car w else get(v,'rtype)) where w = get(v,'avalue);
   (if w then car w else get(v, 'rtype)) where w = get(v, 'avalue);

procedure rl_lengthlogical(u);
   rl_lengthfof rl_simp u;


@@ 255,61 254,61 @@ procedure rl_lengthfof(f);
      if rl_cxp op then
         return length rl_argn f;
      % [f] is atomic.
      return apply(get(car rl_cid!*,'rl_lengthat),{f})
      return apply(get(car rl_cid!*, 'rl_lengthat), {f})
   end;

procedure rl_sub!*fof(al,f);
   rl_mk!*fof rl_subfof(al,rl_simp f);
procedure rl_sub!*fof(al, f);
   rl_mk!*fof rl_subfof(al, rl_simp f);


rl_builtin {
   name = mkor,
   name = mkor, 
   doc = {
      synopsis = {pos = 1, text = "for R mkor E"},
      description = "for-loop action for constructing disjunctions",
      returns = "Any",
      arg = {pos = 1, name = "R", text = "range specification as documented in Sect.5.4 of the REDUCE manual "},
      synopsis = {pos = 1, text = "for R mkor E"}, 
      description = "for-loop action for constructing disjunctions", 
      returns = "Any", 
      arg = {pos = 1, name = "R", text = "range specification as documented in Sect.5.4 of the REDUCE manual "}, 
      arg = {pos = 2, name = "E", text = "RLISP expression"}
   }
};

rl_builtin {
   name = mkand,
   name = mkand, 
   doc = {
      synopsis = {pos = 1, text = "for R mkand E"},
      description = "for-loop action for constructing conjunctions",
      returns = "Any",
      arg = {pos = 1, name = "R", text = "range specification as documented in Sect.5.4 of the REDUCE manual "},
      synopsis = {pos = 1, text = "for R mkand E"}, 
      description = "for-loop action for constructing conjunctions", 
      returns = "Any", 
      arg = {pos = 1, name = "R", text = "range specification as documented in Sect.5.4 of the REDUCE manual "}, 
      arg = {pos = 2, name = "E", text = "RLISP expression"}
   }
};

foractions!* := 'mkand . 'mkor . foractions!*;
deflist('((mkand rlmkand) (mkor rlmkor)),'bin);
deflist('((mkand (quote true)) (mkor (quote false))),'initval);
deflist('((mkand rlmkand) (mkor rlmkor)), 'bin);
deflist('((mkand (quote true)) (mkor (quote false))), 'initval);

symbolic operator rlmkor,rlmkand;
symbolic operator rlmkor, rlmkand;

procedure rlmkor(a,b);
procedure rlmkor(a, b);
   if !*mode eq 'symbolic then
      rederr "`mkor' invalid in symbolic mode"
   else <<
      if null a then a := 'false;
      if null b then b := 'false;
      a := if eqcar(a,'or) then cdr a else {a};
      b := if eqcar(b,'or) then cdr b else {b};
      'or . nconc(b,a)
      a := if eqcar(a, 'or) then cdr a else {a};
      b := if eqcar(b, 'or) then cdr b else {b};
      'or . nconc(b, a)
   >>;

procedure rlmkand(a,b);
procedure rlmkand(a, b);
   if !*mode eq 'symbolic then
      rederr "`mkand' invalid in symbolic mode"
   else <<
      if null a then a := 'true;
      if null b then b := 'true;
      a := if eqcar(a,'and) then cdr a else {a};
      b := if eqcar(b,'and) then cdr b else {b};
      'and . nconc(b,a)
      a := if eqcar(a, 'and) then cdr a else {a};
      b := if eqcar(b, 'and) then cdr b else {b};
      'and . nconc(b, a)
   >>;

endmodule;  % [rlami]