Artifact f1eaeb7fe45d1d09460974422fb2939009fcdc61f8dd5545f33150ec34da9be0:
- Executable file
r38/packages/redlog/pasfmisc.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: 24305) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: pasfmisc.red,v 1.43 2003/12/11 10:51:19 lasaruk Exp $ % ---------------------------------------------------------------------- % Copyright (c) 2002 A. Dolzmann, A. Seidl, and T. Sturm % ---------------------------------------------------------------------- % $Log: pasfmisc.red,v $ % Revision 1.43 2003/12/11 10:51:19 lasaruk % Smart simplification improoved. % % Revision 1.42 2003/12/03 13:39:17 dolzmann % Fixed wrong calling of pasf_qff2ivl in pasf_bsatp. % % Revision 1.41 2003/12/02 07:43:08 lasaruk % Additive smart simplification added. % % Revision 1.40 2003/11/28 06:30:11 lasaruk % spaces removed. bsatp function added. % % Revision 1.39 2003/11/12 08:00:30 dolzmann % Changed a rl_mkn into rl_smkn correting a wrong construction of a or % containing only one argument. % % Revision 1.38 2003/11/11 15:05:59 sturm % (Temporarily?) removed special treatment for 'and in pasf_b2atl. % % Revision 1.37 2003/11/11 14:56:50 sturm % Fixed a bug in iv_merge. % % Revision 1.36 2003/10/28 09:55:42 dolzmann % Removed trailing spaces. % % Revision 1.35 2003/10/16 16:17:38 lasaruk % Compiler error messages partially removed. All others are due % to the noncompleteness of packet. % % Revision 1.34 2003/08/12 19:51:17 lasaruk % Bug in pasf_atf2ivl corrected % % Revision 1.33 2003/08/05 08:57:17 seidl % Intermediate check-in. % % Revision 1.32 2003/07/22 10:06:33 lasaruk % Serious bug in atf2ivl and pasf_ceil and pasf_floor removed. % % Revision 1.31 2003/07/21 21:57:41 seidl % Intermediate check-in. Part of advanced smart simplification works % already. % % Revision 1.30 2003/07/16 13:50:47 lasaruk % Debug messages removed. Bug in printing congurences removed. % Testfile adjusted to changes (working cases). % % Revision 1.29 2003/07/16 12:43:44 lasaruk % conflicts resolved. pasf_simpl removed. implementation of % pasf_simplb and pasf_b2terml added and tested. % temporary method for pasf_b2terml in algebraic mode added. % empty list bug in pasf_ivl2qff removed. % expansion method uses now pasf_b2terml. some comments done % better. % % Revision 1.28 2003/07/15 12:40:41 seidl % Renamed pasf_iv2qff to pasf_ivl2qff and pasf_qff2iv to pasf_qff2ivl. % Provided algebraic mode access to simplb, ivl2qff, qdd2ivl. Changed % pasf_mkrng so intervals with same upper and lower bound result in an % equation. Fixed serious bug in pasf_prepat. Added cvs header to % pasf.tst. Todo Lasaruk: pasf_ivl2qff crashes with empty interval as % argument, see testfile. % % Revision 1.27 2003/07/14 12:37:58 lasaruk % Common utilities attached and tested (see the testfile). % % Revision 1.26 2003/06/12 20:54:51 lasaruk % Testcases added. Small bug in merging fixed. true and false cases added. % % Revision 1.25 2003/06/04 12:33:40 lasaruk % Some smaller modifications. % % Revision 1.24 2003/05/31 14:41:50 lasaruk % PNF corrected. examples added. % % Revision 1.23 2003/05/28 20:37:51 lasaruk % Expansion done better. % % Revision 1.22 2003/05/26 20:50:57 lasaruk % Range expansion with congruences % % Revision 1.21 2003/05/22 22:00:58 lasaruk % DNF added. % % Revision 1.20 2003/05/17 17:04:16 lasaruk % bugs removed % % Revision 1.19 2003/05/17 16:27:56 lasaruk % Pasf simplification added. Some errors corrected. % % Revision 1.18 2003/05/15 23:34:47 lasaruk % Interval expansion added % % Revision 1.17 2003/04/20 12:04:04 lasaruk % Completely removed any reference to range predicates (in input % also). PNF made shorter. % % Revision 1.16 2003/04/14 10:11:39 lasaruk % Changes to work with bounded quantifieres added . Simplification bug % (content) removed. Range predicates removed. % % Revision 1.15 2003/03/16 22:31:45 lasaruk % PNF-bug removed. % % Revision 1.14 2003/03/04 09:33:23 lasaruk % Advanced simplification. PNF code attached but not used yet. Some code % migration. Documentation debugged. % % Revision 1.13 2003/02/24 12:50:37 lasaruk % Bug caused congruence error fixed. % % Revision 1.12 2003/02/17 10:55:40 lasaruk % Stable full featured version % % Revision 1.11 2003/02/03 13:41:04 lasaruk % Experimental version with full functionality. A bit buggy. % % Revision 1.10 2002/12/23 07:05:59 lasaruk % Operator pasf_op replaced by pasf_opn % % Revision 1.9 2002/12/02 12:53:37 lasaruk % Elimination of one variable in front of an ex quantifier. Not really % worth looking at. % % Revision 1.8 2002/10/10 09:09:20 lasaruk % Range predicate implemented. Todo: logical negation of range predicate % % Revision 1.7 2002/10/02 14:31:19 lasaruk % Initial check in. Only dummy methods for advanced simplification first. % % Revision 1.6 2002/09/26 14:54:55 lasaruk % Errors corrected. Negation form implemented. % % Revision 1.5 2002/09/26 10:47:31 lasaruk % Prenex normal form functionality added. Tests follow. % % Revision 1.4 2002/09/19 08:49:42 lasaruk % All operators are binary. Before printing modulus of cong and ncong is % put directly after the operator. Ordering corrected. % % Revision 1.3 2002/08/26 11:57:14 lasaruk % Added implementation of black box rl_ordatp % % Revision 1.2 2002/08/23 12:32:53 dolzmann % Added neccessary end; at the end of the file. % % Revision 1.1 2002/08/23 08:07:19 seidl % Added service rl_atl with trival black box rl_ordatp. % Created module pasfmisc for this. % % ---------------------------------------------------------------------- lisp << fluid '(pasf_misc_rcsid!* pasf_misc_copyright!*); pasf_misc_rcsid!* := "$Id: pasfmisc.red,v 1.43 2003/12/11 10:51:19 lasaruk Exp $"; pasf_misc_copyright!* := "Copyright (c) 1995-2002 by A. Dolzmann, A. Seidl, and T. Sturm" >>; module pasfmisc; procedure iv_new(lb,rb); % Interval datastructure constructor. [lb] is the lower bound and % [rb] is the upper bound. Returns a new interval $[lb,rb]$ % (including the bounds). {((if lb then lb else 0) . (if rb then rb else 0))}; procedure iv_newcong(op,class); % Interval datastructure congruence constructor. [op] is the % congruence operator (cong . modulo) or (ncong . modulo) and class % is a representant of the congruence class. Returns the (non % trivial) datastructure representation for $var op class$. {(op . if class then class else 0)}; procedure iv_congp(ivl); % Interval datastructure new interval congruence predicate. [ivl] % is an interval list. Returns t if and only if [ivl] contains a % congruence. if ivl then pairp caar ivl or iv_congp cdr ivl; procedure iv_empty(ivl); % Interval datastructure empty attribut. [ivl] is a an interval % list. Returns t if the list is empty. not ivl; procedure iv_congsplitl(ivl); % Interval datastructure congruence split of a interval list. [ivl] % is an interval list. Returns a pair (iv1 . iv2) where ivl1 is a % list of intervals without congruences and iv2 are all the % congruences. begin scalar split,rest; % Termination of the recursion if ivl then return (nil . nil); % Splitting the first list split := iv_congsplit car ivl; rest := iv_congsplitl cdr ivl; return ((car split . car rest) . (cdr split . cdr rest)); end; procedure iv_congsplit(iv); % Interval datastructure congruence split. [iv] is an interval. % Returns a pair (iv1 . iv2) where iv1 all intervals without % congruences and iv2 are all the congruences. if iv then if iv_congp({car iv}) then (car iv_congsplit cdr iv . (car iv . cdr iv_congsplit cdr iv)) else ((car iv . car iv_congsplit cdr iv) . cdr iv_congsplit cdr iv) else (nil . nil); procedure iv_cutn(ivl); % Interval datastructure multiple interval cut. [ivl] is a list of % intervals. Returns interval $\cap ivl$. if cdr ivl then iv_cut(car ivl,iv_cutn cdr ivl) else car ivl; procedure iv_cut(iv1,iv2); % Interval datastructure cut. [iv1] and [iv2] are congruence free % intervals. Returns interval $iv_1 \cap iv_2$. begin scalar curr,lower,res; % If one of the intervals is empty returning nil if iv_empty iv1 or iv_empty iv2 then return nil; % Until all lists are empty while not(iv_empty iv1 and iv_empty iv2) do << % Choosing the interval with the smallest lower bound. If % one of those is empty then we take the lower bound from the % over one. if iv_empty iv2 or (not iv_empty iv1 and pasf_leqp(caar iv1,caar iv2)) then << lower := car iv1; iv1 := cdr iv1 >> else << lower := car iv2; iv2 := cdr iv2 >>; % Initialization of a new result interval if null curr then curr := lower else if pasf_leq(cdr curr,car lower) then % The limit of the next smallest interval is bigger % than the end of the current curr := lower else if pasf_leqp(cdr curr,cdr lower) then << res := (car lower . cdr curr) . res; curr := lower >> else res := lower . res; >>; return reverse res end; procedure iv_cutcongs(ivl,congs); % Interval datastructure congruence processing. [ivl] is % a congruence free interval list; [congs] is a list of % congruences. Returns $congs \cup ivl$. begin scalar curr,res; if not congs then return ivl; while not iv_empty ivl do << for i := caar ivl : cdar ivl do << iv_cutcongs1(i,congs); if iv_cutcongs1(i,congs) then if curr then curr := (car curr . i) else curr := (i . i) else if curr then << res := curr . res; curr := nil >> >>; % Joining the last interval limit if null cdr ivl and curr then res := (car curr . cdar ivl) . res; ivl := cdr ivl >>; return reverse res end; procedure iv_cutcongs1(val,congs); % Interval datastructure congruence processing. [val] is % a value; [congs] is a list of congruences. Returns % t if and only if [val] satisfies all congruences. if congs then iv_cutcongs2(val,car congs) and iv_cutcongs1(val,cdr congs) else 't; procedure iv_cutcongs2(val,cong); % Interval datastructure congruence processing. [val] is a value; % [congs] is a congruence. Returns t if and only if [val] satisfies % [cong]. if caar cong eq 'cong then remainder(cdr cong - val,cdar cong) = 0 else remainder(cdr cong - val,cdar cong) <> 0; procedure iv_mergen(ivl); % Interval datastructure multiple intervals merge. [ivl] is an % interval list. Returns interval $\cup ivl$. if cdr ivl then iv_merge(car ivl,iv_mergen cdr ivl) else car ivl; procedure iv_merge(iv1,iv2); % Interval datastructure merge. [iv1] and [iv2] are intervals. % Returns interval $iv_1 \cup iv_2$. begin scalar curr,lower,res; % Test for congruences in the intervals if iv_congp iv1 or iv_congp iv2 then rederr{"iv_merge : merging a congruence not possible }"}; % Test for empty input lists if iv_empty iv1 and iv_empty iv2 then return nil; % Until all lists are empty while not(iv_empty iv1 and iv_empty iv2) do << % Choosing the interval with the smallest lower bound. If % one of those is empty then we take the lower bound from the % over one. if iv_empty iv2 or (not iv_empty iv1 and pasf_leqp(caar iv1,caar iv2)) then << lower := car iv1; iv1 := cdr iv1 >> else << lower := car iv2; iv2 := cdr iv2 >>; % Initialization of a new result interval if not curr then curr := lower else if pasf_leq(cdr curr,car lower) then << % The limit of the next smallest interval is bigger % than the end of the current res := curr . res; curr := lower >> else if pasf_leqp(cdr curr,cdr lower) then % A new limit must be set for the current % interval curr := (car curr . cdr lower); >>; return reverse (curr . res) end; procedure pasf_atf2iv(atf); % Presburger arithmetic standard form atomic formula to interval. % [atf] is an atomic formula. Returns an interval. begin scalar elimnf,nom,den,floor,ceil; elimnf := pasf_elimnf(pasf_simplat1 atf,car rl_fvarl atf); nom := pasf_arg2r elimnf; den := pasf_leadc elimnf; floor := pasf_floor(nom,den); ceil := pasf_ceil(nom,den); if pasf_op elimnf eq 'equal then % Check if the equality solution is integer if den eq 1 then % Floor and ceil are the same return iv_new(floor,floor) else return {}; if pasf_op elimnf eq 'leq then return iv_new('ninf,floor); if pasf_op elimnf eq 'lessp then return iv_new('ninf,addf(ceil,negf 1)); if pasf_op elimnf eq 'geq then return iv_new(ceil,'pinf); if pasf_op elimnf eq 'greaterp then return iv_new(addf(floor,1),'pinf); if pasf_op elimnf eq 'neq then return iv_merge(iv_new('ninf,addf(ceil,negf 1)), iv_new(addf(floor,1),'pinf)); if pasf_opn elimnf memq '(cong ncong) then % Check if the equality solution is integer if den eq 1 then % Floor and ceil are the same return iv_newcong(pasf_op elimnf,floor) else return {}; rederr{"pasf_atf2iv: illegal operator ",pasf_op atf} end; procedure pasf_qff2ivl(f); % Presburger arithmetic standard form positive quantifier free % formula to interval. [f] is a quantifier free formula. Returns an % interval. pasf_qff2ivl1 rl_dnf f; procedure pasf_qff2ivl1(f); % Presburger arithmetic standard form positive quantifier free % formula to interval subprocedure . [f] is a quantifier free % formula. Returns an interval. begin scalar fs,cng; if rl_tvalp f then % True or false if f eq 'true then rederr{"pasf_qff2ivl1 : true as a bound is invalid"} else return nil; if rl_op f eq 'and then << % Using the fact the formula is in DNF. Than an AND is the end % node of the formula's evaluation tree. for each pf in rl_argn f do % Only atomic formulas if pasf_cong pf then cng := append(pasf_atf2iv pf,cng) else fs := (pasf_atf2iv pf) . fs; return iv_cutcongs(iv_cutn fs,cng) >> else if rl_op f eq 'or then return iv_mergen for each pf in rl_argn f collect pasf_qff2ivl1 pf; % This case can only occur if one of the DNF conjunctions % contains only one atomic formula ( e.g. x = 0 or x = 10). This % leads to a correct expansion only if this atomic formula is an % equality and represent so a finit set. In other cases the % original input formula has already represented an infinit set % and was illegal for expansion. if pasf_opn f eq 'equal then return pasf_atf2iv f; % Something is wrong (mainly an error in DNF computation or % a formula with infinit satisfiability set in input) rederr{"pasf_qff2ivl1 : infinit bound in input",f} end; procedure pasf_ivl2qff(ivl,var); % Presburger arithmetic standard form interval list to quantifier % free formula. [ivl] is an interval list; [var] is a free % variable. Returns a quantifier free formula with [var] as single % free valiable with [ivl] as satisfaction interval. if not iv_empty ivl then rl_smkn('or,for each iv in ivl collect pasf_mkrng(var,numr simp car iv,numr simp cdr iv)) else 'false; procedure pasf_bsatp(f,var); % Presburger arithmetic standard form bound satisfiability. [f] is % a bound; [var] is the bound variable. Returns nil iff the bound % is not satifiable. pasf_qff2ivl f; % begin scalar atl; % atl := rl_atl f; % return pasf_qff2ivl(f,var); % end; procedure pasf_bsatp1(f,var,atf); % Presburger arithmetic standard form bound satisfiability % subroutine. [f] is a bount; [var] is the bound variable; [atf] is % an atomic formula contained in f. Returns 't iff the limits of % the interval defined by the formula satisfies f. nil; procedure pasf_ivl2atl(ivl,k); % Bound to list of atoms. [ivl] is a list of ascending intervals, % [k] is an ID. Returns a list of atoms such the conjunction % thereof is equivalent to the bound. begin scalar atl,r1; if null ivl then return nil; if null cdr ivl and caar ivl = cdar ivl then return {pasf_0mk2('equal,addf(numr simp k,negf numr simp caar ivl))}; atl := pasf_0mk2('geq,addf(numr simp k,negf numr simp caar ivl)) . atl; r1 := cdar ivl; ivl := cdr ivl; while ivl do << for i := r1+1 : (caar ivl)-1 do atl := pasf_0mk2('neq,addf(numr simp k,negf numr simp i)) . atl; r1 := cdar ivl; ivl := cdr ivl >>; atl := pasf_0mk2('leq,addf(numr simp k,negf numr simp r1)) . atl; return atl end; procedure pasf_b2atl(b,k); % could become cl function with bb qff2atl % Bound to list of atoms. if cl_atfp b then {b} % else if rl_op b eq 'and then % rl_argn b else if rl_tvalp b then (if b eq 'false then {} else rederr "pasf_b2atl: infinite bound") else pasf_ivl2atl(pasf_qff2ivl b,k); procedure pasf_simplb(f,var); % Presburger arithmetic standard form simplify formulas' bound. % [f] is a bound of some bounded formula (a quantifier free formula % in one variable having a finite satisfiability set); [var] is the % bounded variable. Returns an f-equivalent simplified formula % (flat simlified DNF of f). pasf_ivl2qff(pasf_qff2ivl f,var); procedure pasf_b2terml(b,var); % Presburger arithmetic standard form bound to termist. % [b] is a bound of some bounded formula (a quantifier free formula % in one variable having a finite satisfiability set); [var] is the % bounded variable. Returns the satisfiability set as a list % of satisfying terms (e.g. {1,2,3,10}). begin scalar ivl; ivl := pasf_qff2ivl b; return for each iv in ivl join if (numberp car iv) and (numberp cdr iv) then for i := car iv : cdr iv collect i else rederr{"pasf_b2terml : trying to expand infinit bound"} end; procedure pasf_ordatp(a1,a2); % Presburger arithmetic standard form atomic formula % predicate. [a1] and [a2] are atomic formulas. Returns [t] iff % [a1] is less than [a2]. begin scalar lhs1,lhs2; lhs1 := pasf_arg2l a1; lhs2 := pasf_arg2l a2; if lhs1 neq lhs2 then return ordp(lhs1,lhs2); return pasf_ordrelp(pasf_opn a1,pasf_opn a2) end; procedure pasf_ordrelp(r1,r2); % Presburger arithmetic standard form relation order predicate. % [r1] and [r2] are pasf-relations. Returns a [T] iff $[r1] < % [r2]$. not not (r2 memq (r1 memq '(equal neq leq lessp geq greaterp cong ncong))); procedure pasf_leqp(c1,c2); % Presburger arithmetic less or equal predicate on constant % expressions $\mathbb{Z} \cup \{ \infty,-\infty \}$. [c1] and [c2] % are two constant expressions. Returns [T] if [c1] is less or % equal than [c2]. if (c1 eq 'ninf) or (c2 eq 'pinf) or (c1 neq 'pinf and c2 neq 'pinf and c2 neq 'ninf and c1 <= c2) then t; procedure pasf_leq(c1,c2); % Presburger arithmetic less predicate on constant expressions % $\mathbb{Z} \cup \{ \infty,-\infty \}$. [c1] and [c2] are two % constant expressions. Returns [T] if [c1] is less than [c2]. if (c1 eq 'ninf) or (c2 eq 'pinf) or (c1 neq 'pinf and c2 neq 'pinf and c2 neq 'ninf and c1 < c2) then t; procedure pasf_varlat(atform); % Presburger arithmetic standard form atomic formula list of % variables. [atform] is an atomic formula. Returns the variables % contained in [atform] as a list. kernels pasf_arg2l atform; procedure pasf_varsubstat(atf,new,old); % Presburger arithmetic standard form substitute variable for % variable in atomic formula. [atf] is an atomic formula; [new] and % [old] are variables. Returns an atomic formula equivalent to % [atf] where [old] is substituted with [new]. pasf_0mk2(pasf_op atf,numr subf(pasf_arg2l atf,{old . new})); procedure pasf_negateat(atf); % Presburger arithmetic standard form negate atomic formula. [atf] % is an atomic formula. Returns an atomic formula equivalent to % $\lnot [atf]$. if (pasf_opn atf) memq '(cong ncong) then pasf_mkn(pasf_mkop(pasf_lnegrel pasf_opn atf,pasf_m atf), pasf_argn atf) else pasf_mkn(pasf_lnegrel pasf_opn atf,pasf_argn atf); procedure pasf_lnegrel(r); % Presburger arithmetic standard form logically negate % relation. [r] is a relation. Returns a relation $R$ such that for % terms $t_1$, $t_2$ we have $R(t_1,t_2)$ equivalent to $\lnot % [r](t_1,t_2)$. if r eq 'equal then 'neq else if r eq 'neq then 'equal else if r eq 'leq then 'greaterp else if r eq 'lessp then 'geq else if r eq 'geq then 'lessp else if r eq 'greaterp then 'leq else if r eq 'cong then 'ncong else if r eq 'ncong then 'cong else rederr {"pasf_lnegrel: unknown operator",r}; procedure pasf_anegateat(atf); % Presburger arithmetic standard form negate atomic formula % algebraically. [atf] is an atomic formula. Returns an atomic % formula equivalent to $-[atf]$. if (pasf_opn atf) memq '(cong ncong) then pasf_mk2(pasf_mkop(pasf_anegrel pasf_opn atf,pasf_m atf), negf pasf_arg2l atf,negf pasf_arg2r atf) else pasf_mk2(pasf_anegrel pasf_opn atf, negf pasf_arg2l atf,negf pasf_arg2r atf); procedure pasf_anegrel(r); % Presburger arithmetic standard form algebraically negate % relation. [r] is a relation. Returns a relation $R$ such that % $R(-t,0)$ is equivalent to $[r](t,0)$ for a term $t$. cdr atsoc(r,'((equal . equal) (neq . neq) (leq . geq) (geq . leq) (lessp . greaterp) (greaterp . lessp) (cong . cong) (ncong . ncong))) or rederr {"pasf_anegrel: unknown operator ",r}; procedure pasf_subat(al,f); begin scalar nlhs; nlhs := subf(pasf_arg2l f,al); if not domainp denr nlhs then rederr "pasf_subat: parametric denominator after substitution"; return pasf_0mk2(pasf_op f,numr nlhs) end; procedure pasf_subalchk(al); for each x in al do if not domainp denr simp cdr x then rederr "pasf_subalchk: parametric denominator in substituted term"; procedure pasf_eqnrhskernels(x); nconc(kernels numr w,kernels denr w) where w=simp cdr x; procedure pasf_floor(nom,den); % Presburer arithmetic standard form floor of two domain valued % standard forms. [nom] is the nominator SF, [den] is the % denominator SF. Returns the floor of [nom]/[den]. if domainp nom and domainp den then if null nom then nil else if remainder(nom,den) = 0 then if nom / den = 0 then nil else nom / den else % The value is not negative if nom*den > 0 then nom / den else nom / den - 1 else rederr{"pasf_floor: not a domain valued sf as input"}; procedure pasf_ceil(nom,den); % Presburer arithmetic standard form ceil of two domain valued % standard forms. [nom] is the nominator SF, [den] is the % denominator SF. Returns the ceil of [nom]/[den]. if domainp nom and domainp den then if null nom then nil else if remainder(nom,den) = 0 then if nom / den = 0 then nil else nom / den else % The value is not negative if nom*den > 0 then nom / den + 1 else nom / den else rederr{"pasf_floor: not a domain valued sf as input"}; procedure pasf_content(ex); % Presburger arithmetic standard form content. [ex] is a linear % expression. Returns the common divisor of all coefficients. if domainp ex then abs ex else !:gcd(abs lc ex,pasf_content red ex); procedure pasf_const(ex); % Presburger arithmetic standard form constant part of an expresion % computation. [expr] is an expression. Returns the constant part % of [expr]. if domainp ex then ex else pasf_const red ex; procedure pasf_termmlat(at); % Presburger arithmetic standard form term multiplicity list of % atomic formula. [at] is an atomic formula. Returns the % multiplicity list off all non-zero terms in [at]. if pasf_arg2l pasf_rednf at then {(pasf_arg2l pasf_rednf at . 1)}; endmodule; % pasfmisc end; % of file