Artifact 7313b6a66da83a5f3fd38c8805539c54e96b030731102c3c8a058c95fdc4255c:
- Executable file
r38/packages/redlog/pasfnf.red
— part of check-in
[f2fda60abd]
at
2011-09-02 18:13:33
on branch master
— Some historical releases purely for archival purposes
git-svn-id: https://svn.code.sf.net/p/reduce-algebra/code/trunk/historical@1375 2bfe0521-f11c-4a00-b80e-6202646ff360 (user: arthurcnorman@users.sourceforge.net, size: 8012) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: pasfnf.red,v 1.15 2003/11/05 13:27:14 lasaruk Exp $ % ---------------------------------------------------------------------- % Copyright (c) 2001 A. Dolzmann, A. Lasaruk, A. Seidl, and T. Sturm % ---------------------------------------------------------------------- % $Log: pasfnf.red,v $ % Revision 1.15 2003/11/05 13:27:14 lasaruk % Some major redlog programming rules applied to the code. % Formulas are made positive acc. to the current kernel order. % % Revision 1.14 2003/07/16 13:50:47 lasaruk % Debug messages removed. Bug in printing congurences removed. % Testfile adjusted to changes (working cases). % % Revision 1.13 2003/07/14 12:37:58 lasaruk % Common utilities attached and tested (see the testfile). % % Revision 1.12 2003/05/31 14:41:50 lasaruk % PNF corrected. examples added. % % Revision 1.11 2003/04/20 12:04:04 lasaruk % Completely removed any reference to range predicates (in input % also). PNF made shorter. % % Revision 1.10 2003/04/14 10:11:39 lasaruk % Changes to work with bounded quantifieres added . Simplification bug % (content) removed. Range predicates removed. % % Revision 1.9 2003/03/26 11:19:23 lasaruk % Formula runthrough rewritten as cl_atnum. True/false in rlexpabnd bug % removed. Some services added. % % Revision 1.8 2003/03/16 22:31:45 lasaruk % PNF-bug removed. % % Revision 1.7 2003/03/11 12:30:36 lasaruk % Bug in normal form computation fixed. % % Revision 1.6 2003/03/11 00:41:29 lasaruk % Prenex normal form with correct range predicate handling added. Documentation % extended. Todo section added. % % Revision 1.5 2003/03/04 09:33:23 lasaruk % Advanced simplification. PNF code attached but not used yet. Some code % migration. Documentation debugged. % % Revision 1.4 2003/02/28 11:55:40 lasaruk % Simplifier congruence bug removed. Switch siatadv now actively used. % % Revision 1.3 2003/02/18 16:02:12 seidl % Header for CVS added. % % ---------------------------------------------------------------------- lisp << fluid '(pasf_nf_rcsid!* pasf_nf_copyright!*); pasf_misc_rcsid!* := "$Id: pasfnf.red,v 1.15 2003/11/05 13:27:14 lasaruk Exp $"; pasf_nf_copyright!* := "Copyright (c) 1995-2002 by A. Dolzmann, A. Lasaruk, A. Seidl, and T. Sturm" >>; % Pasf normal forms. Submodule of pasf. module pasfnf; procedure pasf_rednf(f); % Presburger arithmetic standard form compute the redlog normal % form $a rel b \equiv a - b rel 0$ for each atomic formula in % [f]. [f] is a formula. Returns an [f] equivalent formula in % redlog normal form. cl_apply2ats1(f,'pasf_rednf1, nil); procedure pasf_rednf1(atf); % Presburger arithmetic standard form compute the redlog normal % form $a rel b \equiv a - b rel 0$ for an atomic formula. [atf] is % a formula. Returns an [atf] equivalent atomic formula in redlog % normal form. pasf_mk2(pasf_op atf, addf(pasf_arg2l atf, negf pasf_arg2r atf), nil); procedure pasf_elimnf(psi, x); % Presburger arithmetic standard form elimination normal % form. [psi] is a matrix of the original formula, [x] is a % quantified variable. Returns [psi] in elimination normal form for % the quantified variable. cl_apply2ats1(psi,'pasf_elimnf1, {x}); procedure pasf_elimnf1(atf, x); % Presburger arithmetic standard form elimination normal form % subprocedure. [atf] is an atomic formula. Returns [atf] in % elimination normal form according to the quantified variable. begin scalar op,ex,oldkorder,leadc,reduct,exr; op := pasf_op atf; ex := addf(pasf_arg2l(atf),negf pasf_arg2r(atf)); if x memq kernels ex then << oldkorder := setkorder {x}; exr := reorder ex; leadc := lc exr; reduct := red exr; setkorder oldkorder; reorder ex; if minusf leadc then return pasf_anegateat pasf_mk2(op,multf(leadc,numr simp x), negf reduct) else return pasf_mk2(op,multf(leadc,numr simp x),negf reduct); >> else return pasf_mk2(op,nil,negf ex); end; procedure pasf_pnf(phi); % Presburger arithmetic standard form prenex normal form. [phi] is % a formula. Returns a prenex formula equivalent to [phi]. The % number of quantifier changes in the result is minimal among all % formulas that can be obtained from [phi] by moving quantifiers to % the outside. pasf_pnf1 rl_nnf phi; procedure pasf_pnf1(phi); % Presburger arithmetic standard form prenex normal form % subroutine. [phi] is a positive formula that does not contain any % extended boolean operator. Returns a prenex formula equivalent % to [phi]. The number of quantifier changes in the result is % minimal among all formulas that can be obtained from [phi] by % moving quantifiers to the outside. << if null cdr erg or pasf_qb car erg < pasf_qb cadr erg then car erg else cadr erg >> where erg=pasf_pnf2(cl_rename!-vars phi); procedure pasf_pnf2(phi); begin scalar op; op := rl_op phi; if rl_quap op then return pasf_pnf2!-quantifier(phi); if rl_junctp op or rl_bquap op then return pasf_pnf2!-junctor(phi); if rl_tvalp op then return {phi}; if rl_cxp op then rederr{"pasf_pnf2():",op,"invalid as operator"}; return {phi} end; procedure pasf_pnf2!-quantifier(phi); << if (null cdr e) or (rl_op phi eq rl_op car e) then {rl_mkq(rl_op phi,rl_var phi,car e)} else {rl_mkq(rl_op phi,rl_var phi,cadr e)} >> where e=pasf_pnf2 rl_mat phi; procedure pasf_pnf2!-junctor(phi); begin scalar args,bv,bound,junctor,e,l1,l2,onlyex,onlyall,phi1,phi2; integer m,qb; junctor := rl_op phi; if rl_bquap junctor then << bv := rl_var phi; bound := rl_b phi; args := {rl_mat phi}; >> else args := rl_argn phi; e := for each f in args collect pasf_pnf2(f); onlyex := T; onlyall := T; for each ej in e do << qb := pasf_qb car ej; if qb > m then << m := qb; onlyex := T; onlyall := T >>; if cdr ej then << l1 := (car ej) . l1; l2 := (cadr ej) . l2 >> else << l1 := (car ej) . l1; l2 := (car ej) . l2 >>; if eqn(m,qb) then << if rl_op car l1 eq 'all then onlyex := nil; if rl_op car l2 eq 'ex then onlyall := nil >>; >>; l1 := reversip l1; l2 := reversip l2; if eqn(m,0) then return {phi}; if onlyex neq onlyall then if onlyex then return {pasf_interchange(l1,junctor,'ex,bv,bound)} else % [onlyall] return {pasf_interchange(l2,junctor,'all,bv,bound)}; phi1 := pasf_interchange(l1,junctor,'ex,bv,bound); phi2 := pasf_interchange(l2,junctor,'all,bv,bound); if car phi1 eq car phi2 then return {phi1} else return {phi1,phi2} end; procedure pasf_qb(phi); begin scalar q,scan!-q; integer qb; while rl_quap(scan!-q := rl_op phi) do << if scan!-q neq q then << qb := qb + 1; q := scan!-q >>; phi := rl_mat phi >>; return qb end; procedure pasf_interchange(l,junctor,a,bv,bound); begin scalar ql,b,result; while pasf_contains!-quantifier(l) do << l := for each f in l collect << while rl_op f eq a do << b := (rl_var f) . b; f := rl_mat f >>; f >>; ql := b . ql; b := nil; a := cl_flip a >>; a := cl_flip a; result := if rl_bquap junctor then % In case of a bounded quantifier the list of % arguments of a matrix is of length 1 rl_mkbq(junctor,bv,bound,car l) else rl_mkn(junctor,l); for each b in ql do << for each v in b do result := rl_mkq(a,v,result); a := cl_flip a >>; return result end; procedure pasf_contains!-quantifier(l); l and (rl_quap rl_op car l or pasf_contains!-quantifier cdr l); endmodule; % pasfnf end;