~trn/reduce-algebra

5fddd1e249f727a15e274f3b5c8a4f3b0030c061 — Jeffrey H. Johnson 6 days ago edb436a + 5715d3f
Merge branch 'svn/trunk'
M packages/redlog/cl/clsimpl.red => packages/redlog/cl/clsimpl.red +2 -4
@@ 32,10 32,8 @@ copyright('clsimpl, "(c) 1995-2021 A. Dolzmann, T. Sturm");
% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
%

rl_provideService rl_simpl = cl_simpl
   using rl_negateat, rl_simplat1, rl_smupdknowl, rl_smrmknowl, rl_smcpknowl,
   rl_smmkatl, rl_ordatp, rl_susipost, rl_susitf, rl_susibin, rl_b2terml,
   rl_simplb, rl_b2atl, rl_bsatp;
rl_provideService rl_simpl = cl_simpl using rl_negateat, rl_simplat1,
   rl_smupdknowl, rl_smrmknowl, rl_smcpknowl, rl_smmkatl, rl_ordatp;

asserted procedure cl_simpl(f: Formula, atl: List, n: Integer): Formula;
   % Common logic simplify. [f] is a formula; [atl] is a list of atomic

M packages/redlog/mri/mri.red => packages/redlog/mri/mri.red +4 -1
@@ 59,7 59,6 @@ put('mri,'rl_params,'(
   (rl_smmkatl!* . cl_smmkatl)
   (rl_negateat!* . mri_negateat)
   (rl_tordp!* . ordp)
   (rl_bsatp!* . mri_bsatp)
   (rl_ordatp!* . mri_ordatp)
   (rl_subat!* . mri_subat)
   (rl_subalchk!* . null)


@@ 80,6 79,10 @@ put('mri,'rl_services,'(
   (rl_fvarl!* . cl_fvarl)
   (rl_qe!* . mri_qe)));

put('mri,'rl_simpb,'pasf_simpb);
put('mri,'rl_resimpb,'pasf_resimpb);
put('mri,'rl_prepb,'pasf_prepb);

put('mri,'simpfnname,'mri_simpfn);
put('mri,'rl_prepat,'mri_prepat);
put('mri,'rl_resimpat,'mri_resimpat);

M packages/redlog/mri/mri_ofsf.red => packages/redlog/mri/mri_ofsf.red +0 -1
@@ 36,7 36,6 @@ rl_copyc('mri_ofsf,'ofsf);

rl_bbiadd('mri_ofsf,'rl_simplat1!*,'mri_simplat1);
rl_bbiadd('mri_ofsf,'rl_negateat!*,'mri_negateat);
rl_bbiadd('mri_ofsf,'rl_bsatp!*,'mri_bsatp);    % for now

endmodule;


M packages/redlog/mri/mri_pasf.red => packages/redlog/mri/mri_pasf.red +0 -1
@@ 36,7 36,6 @@ rl_copyc('mri_pasf,'pasf);

rl_bbiadd('mri_pasf,'rl_simplat1!*,'mri_simplat1);
rl_bbiadd('mri_pasf,'rl_negateat!*,'mri_negateat);
%rl_bbiadd('mri_pasf,'rl_bsatp!*,'mri_bsatp);    % for now

endmodule;


M packages/redlog/ofsf/ofsf.rlg => packages/redlog/ofsf/ofsf.rlg +1 -1
@@ 2172,7 2172,7 @@ false
sub(first second sol,for each atf in dong mkand atf);


true and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0
0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0

rlsimpl ws;


M packages/redlog/ofsf/ofsfsmtqe.red => packages/redlog/ofsf/ofsfsmtqe.red +4 -0
@@ 1,4 1,8 @@
module ofsfsmtqe;
% This is the start of a clean alternative implementation of the infeasible
% core computation in ofsfic. It has been written by T. Sturm and M. Kosta in
% Nancy in May 2017 (rev. 4020). It is not used, probably because it turned
% out that fallback CAD was more relevant than expected.

revision('ofsfsmtqe, "$Id$");


M packages/redlog/pasf/pasf.red => packages/redlog/pasf/pasf.red +33 -2
@@ 142,7 142,6 @@ put('pasf,'rl_params,'(
   (rl_susibin!* . pasf_susibin)
   (rl_susipost!* . pasf_susipost)
   (rl_susitf!* . pasf_susitf)
   (rl_bsatp!* . pasf_bsatp)
   (rl_structat!* . pasf_structat)
   (rl_rxffn!* . pasf_rxffn)
   (rl_smt2ReadAt!* . pasf_smt2ReadAt)));


@@ 187,11 186,43 @@ put('pasf,'rl_services,'(
   (rl_smt2Print!* . pasf_smt2Print)
   (rl_struct!* . cl_struct)));

% Administration definitions
put('pasf,'rl_simpb,'pasf_simpb);

asserted procedure pasf_simpb(u, x: Id, m: Formula): Formula;
   % Simp bound. Do not confuse with "simp bounded quantifer". redlog/rlami
   % knows about bounded quantifiers but the bounds are context-specific,
   % like atomic formulas. u is the unsimped bound. We also receive the
   % already simped variable x and matrix formula m. x is required for a
   % syntax check. f has beed added for symmetry, although pasf is currently
   % the only context supporting bounded quantifiers. Note that the return
   % value is only the simped u.
   begin scalar w;
      w := rl_simp1 u;
      pasf_bsatp(w, x);  % Test for finite solution set
      return w
   end;

put('pasf,'rl_resimpb,'pasf_resimpb);

asserted procedure pasf_resimpb(u: Formula): Formula;
   % Resimp bound. Do not confuse with "resimp bounded quantifer".
   % redlog/rlami knows about bounded quantifiers but the bounds are
   % context-specific, like atomic formulas.
   rl_resimp u;

put('pasf,'rl_prepb,'pasf_prepb);

asserted procedure pasf_prepb(u: Formula): LispPrefixForm;
   % Prep bound. Do not confuse with "prep bounded quantifer". redlog/rlami
   % knows about bounded quantifiers but the bounds are context-specific,
   % like atomic formulas.
   rl_prepfof u;

put('pasf,'simpfnname,'pasf_simpfn);
put('pasf,'rl_prepat,'pasf_prepat);
put('pasf,'rl_resimpat,'pasf_resimpat);
put('pasf,'rl_lengthat,'pasf_lengthat);

put('pasf,'rl_prepterm,'prepf);
put('pasf,'rl_simpterm,'pasf_simpterm);


M packages/redlog/pasf/pasfsibq.red => packages/redlog/pasf/pasfsibq.red +2 -2
@@ 64,8 64,8 @@ asserted procedure pasf_simpltb(op: Id, var: Id, b: Formula, mtx: Formula): Form
      if mtx eq 'false and op eq 'bex or mtx eq 'true and op eq 'ball then
         return mtx;
      % Matrix does not contain the bound variable. Note: nil as a result of
      % rl_bsatp means, that satisfability test has failed.
      if not(var memq rl_fvarl mtx) and rl_bsatp(b, var) then
      % pasf_bsatp means, that satisfability test has failed.
      if not(var memq rl_fvarl mtx) and pasf_bsatp(b, var) then
         return mtx;
      % Bound is an equation. Note: Should be only relevant if rlsism is off
      bfvl := cl_fvarl b;

M packages/redlog/rl/redlog.rlg => packages/redlog/rl/redlog.rlg +8 -10
@@ 32,25 32,23 @@ g := for i:=1:6 mkor
      mkid(a,i) <= mkid(a,j);


g := false or (true and 0 <= 0 and a1 - a2 <= 0 and a1 - a3 <= 0
g := (0 <= 0 and a1 - a2 <= 0 and a1 - a3 <= 0 and a1 - a4 <= 0 and a1 - a5 <= 0

 and a1 - a4 <= 0 and a1 - a5 <= 0 and a1 - a6 <= 0) or (true
 and a1 - a6 <= 0) or ( - a1 + a2 <= 0 and 0 <= 0 and a2 - a3 <= 0

 and  - a1 + a2 <= 0 and 0 <= 0 and a2 - a3 <= 0 and a2 - a4 <= 0

 and a2 - a5 <= 0 and a2 - a6 <= 0) or (true and  - a1 + a3 <= 0
 and a2 - a4 <= 0 and a2 - a5 <= 0 and a2 - a6 <= 0) or ( - a1 + a3 <= 0

 and  - a2 + a3 <= 0 and 0 <= 0 and a3 - a4 <= 0 and a3 - a5 <= 0

 and a3 - a6 <= 0) or (true and  - a1 + a4 <= 0 and  - a2 + a4 <= 0
 and a3 - a6 <= 0) or ( - a1 + a4 <= 0 and  - a2 + a4 <= 0 and  - a3 + a4 <= 0

 and  - a3 + a4 <= 0 and 0 <= 0 and a4 - a5 <= 0 and a4 - a6 <= 0) or (true
 and 0 <= 0 and a4 - a5 <= 0 and a4 - a6 <= 0) or ( - a1 + a5 <= 0

 and  - a1 + a5 <= 0 and  - a2 + a5 <= 0 and  - a3 + a5 <= 0 and  - a4 + a5 <= 0
 and  - a2 + a5 <= 0 and  - a3 + a5 <= 0 and  - a4 + a5 <= 0 and 0 <= 0

 and 0 <= 0 and a5 - a6 <= 0) or (true and  - a1 + a6 <= 0 and  - a2 + a6 <= 0
 and a5 - a6 <= 0) or ( - a1 + a6 <= 0 and  - a2 + a6 <= 0 and  - a3 + a6 <= 0

 and  - a3 + a6 <= 0 and  - a4 + a6 <= 0 and  - a5 + a6 <= 0 and 0 <= 0)
 and  - a4 + a6 <= 0 and  - a5 + a6 <= 0 and 0 <= 0)


% Quantifier elimination and variants

M packages/redlog/rl/rlami.red => packages/redlog/rl/rlami.red +61 -46
@@ 75,14 75,17 @@ asserted procedure rl_prepfof(f: Formula): LispPrefixForm;

asserted procedure rl_prepfof1(f: Formula): LispPrefixForm;
   % prep f (in the sense of prepf, prepsq).
   begin scalar op;
   begin scalar op, w;
      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};
      if rl_bquap op then
         return {op, rl_var f, rl_prepfof1 rl_b f, rl_prepfof1 rl_mat f};
      if rl_bquap op then <<
         if null (w := get(car rl_cid!*, 'rl_prepb)) then
            rederr {"current context", rl_usedcname!*, "does not support bounded quantifiers"};
         return {op, rl_var f, apply(w, {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 an atomic formula


@@ 173,19 176,15 @@ asserted procedure rl_simpq(f: MixedPrefixForm): Formula;

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";
   begin scalar simpb, x, m;
      if null (simpb := get(car rl_cid!*, 'rl_simpb)) then
         rederr {"current context", rl_usedcname!*, "does not support bounded quantifiers"};
      x := reval cadr f;
      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);
      if not idp x then
         typerr(x, "bounded quantified variable");
      flag({x}, 'used!*);
      return rl_mkbq(car f, x, wb, wf)
      m := rl_simp1 cadddr f;
      return rl_mkbq(car f, x, apply(simpb, {caddr f, x, m}), m)
   end;

asserted procedure rl_qvarchk(v: Any): Void;


@@ 210,8 209,8 @@ asserted procedure rl_simp!*fof(u: List): Formula;
      return rl_resimp f
   end;

procedure rl_resimp(u);
   % Reduce logic resimp. [u] is a formula.
asserted procedure rl_resimp(u: Formula): Formula;
   % Reduce logic resimp.
   begin scalar op, w;
      op := rl_op u;
      if rl_tvalp op then


@@ 225,24 224,26 @@ procedure rl_resimp(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)
         rl_qvarchk rl_var u;
         if null (w := get(car rl_cid!*, 'rl_resimpb)) then
            rederr {"current context", rl_usedcname!*, "does not support bounded quantifiers"};
         return rl_mkbq(rl_op u, rl_var u, apply(w, {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})
   end;

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

procedure rl_lengthlogical(u);
asserted procedure rl_lengthlogical(u: MixedPrefixForm): Integer;
   rl_lengthfof rl_simp u;

procedure rl_lengthfof(f);
   % First order formula length. [u] is a formula. Returns the number
   % of top-level constituents of [u].
procedure rl_lengthfof(f: Formula): Integer;
   % First order formula length. Returns the number of top-level constituents
   % of f.
   begin scalar op;
      op := rl_op f;
      if rl_tvalp op then


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

procedure rl_sub!*fof(al, f);
asserted procedure rl_sub!*fof(al: Alist, f: MixedPrefixForm): MixedPrefixForm;
   rl_mk!*fof rl_subfof(al, rl_simp f);




@@ 272,6 273,27 @@ rl_builtin {
   }
};

foractions!* := lto_insertq('mkor, foractions!*);

put('mkor, 'initval, '(quote false));

put('mkor, 'bin, 'rl_mkor);

flag('(rl_mkor), 'opfn);

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

rl_builtin {
   name = mkand, 
   doc = {


@@ 283,34 305,27 @@ rl_builtin {
   }
};

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

symbolic operator rlmkor, rlmkand;
put('mkand, 'initval, '(quote true));

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)
   >>;
put('mkand, 'bin, 'rl_mkand);

flag('(rl_mkand), 'opfn);

procedure rlmkand(a, b);
asserted procedure rl_mkand(a: LispPrefixForm, b: LispPrefixForm): LispPrefixForm;
   if !*mode eq 'symbolic then
      rederr "`mkand' invalid in symbolic mode"
      rederr "`for ... mkand' invalid in symbolic mode"
   else if null a then
      rederr "empty body in `for ... mkand'"
   else if b eq 'true then
      a
   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)
   >>;

endmodule;  % [rlami]
endmodule;

end;  % of file
end;

M packages/support/revision.red => packages/support/revision.red +1 -1
@@ 31,6 31,6 @@

fluid '(revision!*);

revision!* := 6012;
revision!* := 6016;

end;

M psl/dist/comp/aarch64/aarch64-cmac.sl => psl/dist/comp/aarch64/aarch64-cmac.sl +34 -24
@@ 754,10 754,10 @@
           ((anyp zerop))
           ((anyp negp) (*WDifference ArgOne (minus ArgTwo)))
           ((regp regp) (ADD ArgOne ArgOne ArgTwo))
           ((regp imm8-rotatedp) (ADD ArgOne ArgOne ArgTwo))
           ((regp imm12-shiftedp) (ADD ArgOne ArgOne ArgTwo))
           ((regp anyp) (*Move ArgTwo (reg t3))
                        (ADD ArgOne ArgOne (reg t3)))
           ((anyp imm8-rotatedp) (*Move ArgOne (reg t2))
           ((anyp imm12-shiftedp) (*Move ArgOne (reg t2))
                        (ADD (reg t2) (reg t2) ArgTwo)
                        (*Move (reg t2) ArgOne))
           (            (*Move ArgOne (reg t2))


@@ 785,14 785,14 @@
           ((anyp anyp zerop) (*Move ArgTwo ArgOne))
           ((anyp anyp negp) (*WDifference3 Argone ArgTwo (minus Argthree)))
           ((regp regp regp) (ADD ArgOne ArgTwo ArgThree))
           ((regp imm8-rotatedp regp)
           ((regp imm12-shiftedp regp)
                                (ADD ArgOne Argthree ArgTwo))
           ((regp regp imm8-rotatedp)
           ((regp regp imm12-shiftedp)
                                (ADD ArgOne ArgTwo ArgThree))
           ((regp imm8-rotatedp anyp)
           ((regp imm12-shiftedp anyp)
                               (*Move ArgThree (reg t3))
                               (ADD ArgOne (reg t3) ArgTwo))
           ((regp anyp imm8-rotatedp)
           ((regp anyp imm12-shiftedp)
                               (*Move ArgTwo (reg t3))
                               (ADD ArgOne (reg t3) ArgThree))
           ((regp regp anyp)  (*Move ArgThree (reg t3))


@@ 802,12 802,12 @@
           ((regp anyp anyp)  (*Move ArgTwo (reg t2)) % *Move may clobber t3
                               (*Move ArgThree (reg t3))
                               (ADD ArgOne (reg t2) (reg t3)))
           ((anyp regp imm8-rotatedp) (ADD (reg t1) ArgTwo ArgThree)
           ((anyp regp imm12-shiftedp) (ADD (reg t1) ArgTwo ArgThree)
                               (*Move (reg t1) ArgOne))
           ((anyp regp anyp)  (*Move ArgThree (reg t3))
                               (ADD (Reg t2) ArgTwo (reg t3))
                               (*Move (reg t2) ArgOne))
           ((anyp anyp imm8-rotatedp) (*Move ArgTwo (reg t2))
           ((anyp anyp imm12-shiftedp) (*Move ArgTwo (reg t2))
                               (ADD (reg t2) (reg t2) ArgThree)
                               (*Move (reg t2) ArgOne))
           (                   (*Move ArgTwo (reg t2))


@@ 828,16 828,16 @@
           ((regp regp zerop) (*Move ArgOne ArgTwo))
           ((regp regp negp) (*WPlus3 ArgOne ArgTwo (minus ArgThree)))
           ((regp regp regp) (SUB ArgOne ArgTwo ArgThree))
           ((regp imm8-rotatedp regp)
           ((regp imm12-shiftedp regp)
	   	                (*Move ArgTwo (reg t3))
                                (SUB ArgOne (reg t3) Argthree))
           ((regp regp imm8-rotatedp)
           ((regp regp imm12-shiftedp)
                                (SUB ArgOne ArgTwo ArgThree))
           ((regp imm8-rotatedp anyp)
           ((regp imm12-shiftedp anyp)
	   	   		(*Move ArgTwo (reg t2))
                                (*Move ArgThree (reg t3))
                                (SUB ArgOne (reg t2) (reg t3)))
           ((regp anyp imm8-rotatedp)
           ((regp anyp imm12-shiftedp)
                               (*Move ArgTwo (reg t3))
                               (SUB ArgOne (reg t3) ArgThree))
           ((regp regp anyp)  (*Move ArgThree (reg t3))


@@ 847,12 847,12 @@
           ((regp anyp anyp)  (*Move ArgTwo (reg t2))
                               (*Move ArgThree (reg t3))
                               (SUB ArgOne (reg t2) (reg t3)))
           ((anyp regp imm8-rotatedp) (SUB (Reg t1) ArgTwo ArgThree)
           ((anyp regp imm12-shiftedp) (SUB (Reg t1) ArgTwo ArgThree)
                               (*Move (reg t1) ArgOne))
           ((anyp regp anyp)  (*Move ArgThree (reg t3))
                               (SUB (Reg t2) ArgTwo (reg t3))
                               (*Move (reg t2) ArgOne))
           ((anyp anyp imm8-rotatedp) (*Move ArgTwo (reg t2))
           ((anyp anyp imm12-shiftedp) (*Move ArgTwo (reg t2))
                               (SUB (reg t2) (reg t2) ArgThree)
                               (*Move (reg t2) ArgOne))
           (                   (*Move ArgTwo (reg t2))


@@ 916,12 916,12 @@
			  (*Move (reg t1) (reg x0))))
(put 'wdivide 'destroys '((reg 1) (reg 2)))

(de *Wcmp(arg1 arg2)
(de *Wcmp (arg1 arg2)
  (Expand2OperandCMacro arg1 arg2 '*Wcmp))

(DefCmacro *Wcmp
       ((regp regp) (CMP ArgOne ArgTwo))
       ((regp imm8-rotatedp) (CMP ArgOne ArgTwo))
       ((regp imm12-shiftedp) (CMP ArgOne ArgTwo))
       ((Anyp Regp) (*Move ArgOne (reg t1))
                    (CMP (reg t1) ArgTwo))
       ((Regp Anyp) (*Move ArgTwo (reg t2))


@@ 1111,22 1111,32 @@
(DefCMacro *JumpIF
     ((regp regp)       (CMP ArgOne ArgTwo)
                         (ArgFour ArgThree))
     ((regp imm8-rotatedp) (CMP ArgOne ArgTwo)
     ((regp imm12-shiftedp) (CMP ArgOne ArgTwo)
                         (ArgFour ArgThree))
%% ((imm8-rotatedp regp (CMP ArgTwo ArgOne)
%%                       (ArgFive ArgThree))
     ((regp imm12-neg-shiftedp) (CMN ArgOne (wminus ArgTwo))
                         (ArgFour ArgThree))
     ((imm12-shiftedp regp) (CMP ArgTwo ArgOne)
                         (ArgFive ArgThree))
     ((imm12-neg-shiftedp regp) (CMN ArgTwo (wminus ArgOne))
                         (ArgFive ArgThree))
     ((regp anyp)       (*Move ArgTwo (reg t3))
                         (CMP ArgOne (reg t3))
                         (ArgFour ArgThree))
     ((anyp regp)       (*Move ArgOne (reg t3))
                         (CMP (reg t3) ArgTwo )
                         (ArgFour ArgThree))
     ((anyp imm8-rotatedp) (*Move ArgOne (reg t3))
     ((anyp imm12-shiftedp) (*Move ArgOne (reg t3))
                         (CMP (reg t3) ArgTwo)
                         (ArgFour ArgThree))
%% ((imm8-rotatedp anyp) (*Move ArgTwo (reg t2))
%%                       (CMP (reg t2) ArgOne)
%%                       (ArgFive ArgThree))
     ((anyp imm12-neg-shiftedp) (*Move ArgOne (reg t3))
                         (CMN (reg t3) (wminus ArgTwo))
                         (ArgFour ArgThree))
     ((imm12-shiftedp anyp) (*Move ArgTwo (reg t3))
                         (CMP (reg t3) ArgOne)
                         (ArgFive ArgThree))
     ((imm12-neg-shiftedp anyp) (*Move ArgTwo (reg t3))
                         (CMN (reg t3) (wminus ArgOne))
                         (ArgFive ArgThree))
     (                   (*Move ArgOne (reg t1))
                         (*Move ArgTwo (reg t2))
                         (CMP (reg t1) (reg t2))


@@ 1151,7 1161,7 @@
(DefCMacro *JumpNotEQ)

(de *JumpNotEQ(Lbl ArgOne ArgTwo)
        (*JumpIF ArgOne ArgTwo Lbl '(b!.ne . 'b!.ne)))
        (*JumpIF ArgOne ArgTwo Lbl '(b!.ne . b!.ne)))

(DefCMacro *JumpWlessp)


M psl/dist/comp/armv6/armv6-cmac.sl => psl/dist/comp/armv6/armv6-cmac.sl +1 -1
@@ 513,7 513,7 @@
%%%  (idloc id)   and    (quote (idloc id)),
%%% since the quote in the latter form is stripped before passing it on.
%%% Therefore, a special form (saveidloc id) is used.  This will be handled in
%%% ExpandItem (see the redefintion in armv6-spec.sl.
%%% ExpandItem (see the redefinition in armv6-spec.sl.

(de *LoadIDLoc (dest src)
  (let ((idnumber (WConstEvaluable src))

M psl/dist/kernel/aarch64/bpsl => psl/dist/kernel/aarch64/bpsl +0 -0
M psl/dist/kernel/aarch64/main.s => psl/dist/kernel/aarch64/main.s +11 -19
@@ 1057,9 1057,8 @@ l0155:
 ldr X0, [X24, X11, lsl #3]
 ldr W0, [X0, X1, lsl #2]
 cbnz X0, l0156
 ldr X9, [sp, #40]
 movn X10, #0
 cmp X9, X10
 ldr X11, [sp, #40]
 cmn X11, #1
 b.eq l0157
 ldr X0, [sp, #40]
 b l0158


@@ 1076,9 1075,8 @@ l0156:
 ldr X11, l0147
 cmp X0, X11
 b.ne l0160
 ldr X9, [sp, #40]
 movn X10, #0
 cmp X9, X10
 ldr X11, [sp, #40]
 cmn X11, #1
 b.ne l0161
 ldr X9, [sp, #32]
 str X9, [sp, #40]


@@ 1283,8 1281,7 @@ faslin:
 str X0, [sp, #40]
 mov X1, #65535
 and X1, X1, X0
 mov X11, #399
 cmp X1, X11
 cmp X1, #399
 b.eq l0190
 ldr X0, [sp, #32]
// (idloc binaryclose)


@@ 1428,7 1425,6 @@ l0191:
 mov X0, X28
 ldp X29, X30, [sp], #112
 ret
 nop
l0189:
 .quad 369
l0188:


@@ 1809,14 1805,14 @@ l0222:
l0234:
 stp X29, X30, [sp, #-16]!
 mov X29, sp
 mov X11, #2047
 sub X0, X0, X11
 sub X0, X0, #2047
 lsl X0, X0, #3
 ubfx X2, X1, #0, #56
 add X0, X0, X2
 ldr X0, [X0]
 ldp X29, X30, [sp], #16
 ret
 nop
 .quad 1
// (*entry read-id-table expr 1)
 .globl l0240


@@ 2173,22 2169,18 @@ l0283:
gtid:
 stp X29, X30, [sp, #-16]!
 mov X29, sp
 mov X9, #0
// ($global nextsymbol)
 ldr X11, l0278
 ldr X10, [X24, X11, lsl #3]
 cmp X9, X10
 b.ne l0284
 ldr X11, [X24, X11, lsl #3]
 cbnz X11, l0284
// (idloc reclaim)
 ldr X11, l0279
 ldr X10, [X23, X11, lsl #3]
 blr X10
 mov X9, #0
// ($global nextsymbol)
 ldr X11, l0278
 ldr X10, [X24, X11, lsl #3]
 cmp X9, X10
 b.ne l0284
 ldr X11, [X24, X11, lsl #3]
 cbnz X11, l0284
 ldr X0, l0280
// (idloc kernel-fatal-error)
 ldr X11, l0281

M psl/dist/lap/aarch64/aarch64-cmac.b => psl/dist/lap/aarch64/aarch64-cmac.b +0 -0
M web/htdocs/include/begin-head.php => web/htdocs/include/begin-head.php +14 -11
@@ 1,15 1,18 @@
<!DOCTYPE html>
<html lang="en" xmlns="http://www.w3.org/1999/xhtml">
    <head>
        <meta charset="utf-8" />
        <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no" />
        <meta name="description" content="The REDUCE Computer Algebra System" />
        <meta name="keywords" content="Open Source, Software, Development, Developers, Projects, Downloads, SF.net, SourceForge,

<head>
    <meta charset="utf-8" />
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no" />
    <meta name="description" content="The REDUCE Computer Algebra System" />
    <meta name="keywords" content="Open Source, Software, Development, Developers, Projects, Downloads, SF.net, SourceForge,
                    BSD License, Science/Research, OS Portable (Source code to work with many OS platforms),
                    Mathematics, Lisp, REDUCE, reduce-algebra, computer algebra system, CAS" />
        <title><?= isset($page_title) ? $page_title : "REDUCE $header_title" ?></title>
        <link rel="canonical" href="https://reduce-algebra.sourceforge.io<?=$_SERVER['SCRIPT_NAME']?>" />
        <link rel="icon" type="image/png" href="/images/icon.png" />
        <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/bootstrap@5.0.2/dist/css/bootstrap.min.css"
              integrity="sha384-EVSTQN3/azprG1Anm3QDgpJLIm9Nao0Yz1ztcQTwFspd3yD65VohhpuuCOmLASjC" crossorigin="anonymous" />
        <link rel="stylesheet" href="/StyleSheet.css" />
    <title>
        <?= isset($page_title) ? $page_title : "REDUCE $header_title" ?>
    </title>
    <link rel="canonical" href="https://reduce-algebra.sourceforge.io<?=$_SERVER['SCRIPT_NAME']?>" />
    <link rel="icon" type="image/png" href="/images/icon.png" />
    <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/bootstrap@5.1.0/dist/css/bootstrap.min.css"
        integrity="sha384-KyZXEAg3QhqLMpG8r+8fhAXLRk2vvoC2f3B09zVXn8CA5QIVfZOJ3BCsw2P0p/We" crossorigin="anonymous" />
    <link rel="stylesheet" href="/StyleSheet.css" />

M web/htdocs/include/footer.php => web/htdocs/include/footer.php +10 -8
@@ 9,10 9,11 @@
            All information available through this web site is
            Copyright &copy; Anthony C. Hearn and the
            <a href="https://sourceforge.net/p/reduce-algebra/_members/">REDUCE
                developers</a> 2009&ndash;<?= date('Y') ?>.  All Rights
            Reserved.
                developers</a> 2009&ndash;<?= date('Y') ?>. All Rights Reserved.
        </p>
        <p>
            This web site is built using <a href="https://www.php.net/">PHP</a>
            and <a href="https://getbootstrap.com/">Bootstrap</a>.
            Microsoft Internet Explorer does not display this web site
            correctly; please use a current web browser.
        </p>


@@ 24,16 25,17 @@
        <p>This web page should be
            <a href="javascript:void(location.href =
                     'https://html5.validator.nu/?doc='+encodeURIComponent(location.href))"
               style="color:black;text-decoration:none;">valid</a>
                style="color:black;text-decoration:none;">valid</a>
            <!-- target="_blank" or holding down ctrl causes this to fail! -->
            <a href="https://en.wikipedia.org/wiki/XHTML#XHTML5">XHTML5</a>.
        </p>
    </div>
</footer>

    </div>
    </div>
</div>
</div>

    <!-- Bootstrap JavaScript bundle with Popper -->
    <script src="https://cdn.jsdelivr.net/npm/bootstrap@5.0.2/dist/js/bootstrap.bundle.min.js"
            integrity="sha384-MrcW6ZMFYlzcLA8Nl+NtUVF0sA7MsXsP1UyJoMp4YLEuNSfAP+JcXn/tWtIaxVXM" crossorigin="anonymous"></script>
<!-- Bootstrap JavaScript bundle with Popper -->
<script src="https://cdn.jsdelivr.net/npm/bootstrap@5.1.0/dist/js/bootstrap.bundle.min.js"
    integrity="sha384-U1DAWAznBHeqEIlVSCgzq+c9gqGAJn5c/t99JyeKa9xxaYpSvHU5awsuZVVFIhvj"
    crossorigin="anonymous"></script>