Artifact 666e8aa1075fc8023979d1d50d174dfb85d36b6461845c70a3a7e9a8c143a1a9:
- Executable file
r38/packages/redlog/pasfqe.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: 25248) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: pasfqe.red,v 1.57 2004/02/22 21:08:15 lasaruk Exp $ % ---------------------------------------------------------------------- % Copyright (c) 2001 A. Dolzmann, A. Seidl, and T. Sturm % ---------------------------------------------------------------------- % $Log: pasfqe.red,v $ % Revision 1.57 2004/02/22 21:08:15 lasaruk % Added switch rlsusisubst for substitution of equalities. Substitution % results in smaller formulas or formulas with less free variables. % Up to 80% length reduction. Switch rlsusitr should not be used yet. % % Revision 1.56 2003/12/16 07:45:34 lasaruk % Redlog normal form in the simplifier. % % Revision 1.55 2003/12/11 10:51:19 lasaruk % Smart simplification improoved. % % Revision 1.54 2003/12/02 15:27:13 sturm % Introduced ioto_nterpri to avoid ugly linebreaks in verbosity output. % % Revision 1.53 2003/12/02 15:00:57 sturm % Removed a call to cl_simpl in pasf_qeex (superfluous checking for truth % values). % Do a more general check on variable not occurring. % % Revision 1.52 2003/12/02 14:37:07 sturm % Rewritten pasf_qeexblock and added canonical verbose output. % % Revision 1.51 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.50 2003/10/28 10:02:03 dolzmann % Added correct content of fluids pasf_siat_rcsid!* and % pasf_siat_copyright!*. % % Revision 1.49 2003/10/16 16:17:38 lasaruk % Compiler error messages partially removed. All others are due % to the noncompleteness of packet. % % Revision 1.48 2003/10/12 15:18:11 sturm % pasf_qe requires second (theo, dummy for now) argument. This became visible % under CSL. % % Revision 1.47 2003/08/28 15:30:40 lasaruk % Simplification verbose output done better. QE-Bug with truth values % corrected (will be done more effitient). Some fancy examples added. % % Revision 1.46 2003/07/16 12:58:50 lasaruk % Error in QE removed. % % Revision 1.45 2003/07/16 12:51:35 lasaruk % Tipp error. % % Revision 1.44 2003/07/16 12:48:33 lasaruk % See message below. % % Revision 1.43 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.42 2003/06/04 12:33:40 lasaruk % Some smaller modifications. % % Revision 1.41 2003/05/28 20:37:51 lasaruk % Expansion done better. % % Revision 1.40 2003/05/26 20:50:57 lasaruk % Range expansion with congruences % % Revision 1.39 2003/05/22 22:00:58 lasaruk % DNF added. % % Revision 1.38 2003/05/17 17:04:16 lasaruk % bugs removed % % Revision 1.37 2003/05/17 16:27:56 lasaruk % Pasf simplification added. Some errors corrected. % % Revision 1.36 2003/05/15 23:34:47 lasaruk % Interval expansion added % % Revision 1.35 2003/04/20 12:04:04 lasaruk % Completely removed any reference to range predicates (in input % also). PNF made shorter. % % Revision 1.34 2003/04/14 10:11:39 lasaruk % Changes to work with bounded quantifieres added . Simplification bug % (content) removed. Range predicates removed. % % Revision 1.33 2003/03/26 11:19:23 lasaruk % Formula runthrough rewritten as cl_atnum. True/false in rlexpabnd bug % removed. Some services added. % % Revision 1.32 2003/03/04 09:33:23 lasaruk % Advanced simplification. PNF code attached but not used yet. Some code % migration. Documentation debugged. % % Revision 1.31 2003/02/24 19:50:19 lasaruk % Congruences without x removed. % % Revision 1.30 2003/02/18 12:45:03 lasaruk % Better code for some methods. % % Revision 1.29 2003/02/17 14:44:55 lasaruk % Debug messages removed. % % Revision 1.28 2003/02/17 10:55:40 lasaruk % Stable full featured version % % Revision 1.27 2003/02/03 13:41:04 lasaruk % Experimental version with full functionality. A bit buggy. % % Revision 1.26 2003/02/02 17:33:44 lasaruk % Internal representation of data is converted completely into SF's % except the representation of moduli. % % Revision 1.25 2003/02/01 08:42:50 lasaruk % Stack container implemented. % % Revision 1.24 2003/02/01 07:38:33 lasaruk % Recursive range expansion. % % Revision 1.23 2003/01/31 14:25:06 lasaruk % Bug fixed. % % Revision 1.22 2003/01/31 14:18:48 lasaruk % Found better method for impoding. % % Revision 1.21 2003/01/31 14:09:58 lasaruk % New variable method added. K is no loger fixed, but a new variable. % % Revision 1.20 2003/01/29 16:07:46 lasaruk % Better limits. % % Revision 1.19 2003/01/29 15:24:47 sturm % Added service rlexpand for context pasf. Had to split pasf_exprng for this. % % Revision 1.18 2003/01/27 17:40:02 lasaruk % Switches renamed. Bugs in docu fixed. % % Revision 1.17 2003/01/26 18:31:49 lasaruk % Simplification position altered. % % Revision 1.16 2003/01/26 17:49:37 lasaruk % Null congruence error added. Terms without quant. varl. stay % untouched. Bugs fixed. % % Revision 1.15 2003/01/21 17:39:14 lasaruk % Switch rlsiatadv turned off. Bugs fixed. % % Revision 1.14 2003/01/21 10:44:14 lasaruk % Congruence substitution added. Bugs fixed. % % Revision 1.13 2003/01/20 10:36:51 lasaruk % First trial to work with congruences. Bugs fixed. % % Revision 1.12 2003/01/06 18:20:32 lasaruk % Bugs fixed % % Revision 1.11 2003/01/06 17:33:27 lasaruk % Some simplifier bugs fixed. Alternating quantifier elimination attached. % % Revision 1.10 2003/01/05 15:55:05 lasaruk % Simplification improoved. Expansion of range predicates added. % % Revision 1.9 2002/12/31 13:57:49 lasaruk % Simplifier bugs fixed. % % Revision 1.8 2002/12/31 13:33:34 lasaruk % Standard simplifier attached. Standard simplification of expressions % attached. % % Revision 1.7 2002/12/23 07:41:19 lasaruk % Simplifier turned off temporary % % Revision 1.6 2002/12/23 07:07:05 lasaruk % Elimination code completely rewritten % % Revision 1.5 2002/12/10 08:49:41 lasaruk % Correct elimination of an exist. quantifier call added. % Procedures debugged. % % Revision 1.3 2002/12/02 12:53:37 lasaruk % Elimination of one variable in front of an ex quantifier. Not really % worth looking at. % % Revision 1.2 2002/11/15 12:00:48 seidl % Head added. % % ---------------------------------------------------------------------- lisp << fluid '(pasf_qe_rcsid!* pasf_qe_copyright!*); pasf_qe_rcsid!* := "$Id"; pasf_qe_copyright!* := "Copyright (c) 2003 A. Dolzmann, A. Seidl, and T. Sturm" >>; module pasfqe; % Presburger arithmetic standard form quantifier % elimination. Submodule of [pasf]. procedure elimdata_new(repr,n,m,min_si,max_si,ats); % Elimination data constructor. [repr] is a list of canonical % representants, [n] is the lcm of all leading coeficients of the % left hand side of the elimination normal form, [m] is the lcm of % all moduli, [min_si] and [max_si] are the minimal constant values % among all atomic formulas and [ats] is the list of (atf_j,min_sj, % max_sj) where [atf] is an atomic formula containing the % quantified variable and [min_si] and [max_si] are the minimal and % maximal constant value of atf's right hand side. Returns the % elimination data in the elimdata datastructure format. {repr,n,m,min_si,max_si,ats}; procedure elimdata_repr(elimdata); % Elimination data canonical representants accessor. [elimdata] is % the elimination data. Returns the canonical representants. car elimdata; procedure elimdata_n(elimdata); % Elimination data n accessor. [elimdata] is the elimination % data. Returns n. cadr elimdata; procedure elimdata_m(elimdata); % Elimination data m accessor. [elimdata] is the elimination % data. Returns m. caddr elimdata; procedure elimdata_min_si(elimdata); % Elimination data min_si accessor. [elimdata] is the elimination % data. Returns min_si. cadddr elimdata; procedure elimdata_max_si(elimdata); % Elimination data max_si accessor. [elimdata] is the elimination % data. Returns max_si. car cddddr elimdata; procedure elimdata_ats(elimdata); % Elimination data atomic formula list accessor. [elimdata] is the % elimination data. Returns the atomic formula list. cadr cddddr elimdata; procedure elimdata_join(elimdatalst); % Elimination data join a list of elimination data information. % [elimdatalst] is a list of elimdata. Returns the common % elimination information of all list elements. begin scalar rep,n,m,min_si,max_si; rep :={}; n := 1; m := 1; min_si := nil; max_si := nil; if elimdatalst then << max_si := elimdata_max_si car elimdatalst; min_si := elimdata_min_si car elimdatalst; for each elimdata in elimdatalst do << % Just joning the list of canonic representants rep := append(rep,elimdata_repr elimdata); % LCM of all n,m n := *lcm(n,elimdata_n elimdata); m := *lcm(m,elimdata_m elimdata); % max_si and min_si computation if minusf addf(max_si,negf elimdata_max_si elimdata) then max_si := elimdata_min_si elimdata; if minusf addf(min_si,negf elimdata_min_si elimdata) then min_si := elimdata_max_si elimdata >> >>; return elimdata_new(rep,n,m,min_si,max_si,nil) end; procedure pasf_qe(phi,theo); % Presburger arithmetic standard form compute a quantifier free % formula equivalent to psi. [psi] is a formula. Returns a % quantifier free formula equivalent to $\psi()$. begin scalar split,rslt,phi_prime; if !*rlverbose then ioto_tprin2 "++++ Entering pasf_qe"; phi_prime := rl_pnf phi; split := cl_splt phi_prime; % Performing DNF on the matrix rslt := rl_dnf cadr split; for each block in car split do rslt := pasf_qeblock(car block,cdr block,rslt); return if !*rlpasfsimplify then cl_simpl(rslt,nil,-1) else rslt; end; procedure pasf_qeblock(omega,varl,psi); % Presburger erithmetic standrd form eliminate a block of % quantifiers. [omega] if the quantifier type, varl is a list of % the block bounded variables and [psi] is the matrix of the % formula. begin integer dpth,vlv; if !*rlverbose then << ioto_tprin2 {"---- ",omega . reverse varl}; dpth := length varl; if !*rlqedfs then << % should not happen by now vlv := dpth / 4; ioto_prin2t {" [DFS: depth ",dpth,", watching ",dpth - vlv,"]"} >> else ioto_prin2t {" [BFS: depth ",dpth,"]"} >>; if omega eq 'ex then return pasf_qeexblock(varl,psi,dpth,vlv); % [op eq 'all] return cl_nnfnot pasf_qeexblock(varl,cl_nnfnot psi,dpth,vlv) end; procedure pasf_qeexblock(varl,psi,dpth,vlv); % Presburger erithmetic standrd form eliminate a block of % existential quantifiers. [varl] are the bounded variables, [psi] % is the matrix of the formula. Returns a quantifier free formula % equivalent to $\exists varl \psi()$. begin scalar co,cvl,w,coe,f,newj,v; integer c,delc,oldcol,count; cvl := varl; if rl_op psi eq 'or then for each x in rl_argn psi do co := cl_save(co,{cl_mkcoel(cvl,x,nil,nil)}) else co := cl_save(co,{cl_mkcoel(cvl,psi,nil,nil)}); while co do << w := cl_get co; co := cdr w; coe := car w; cvl := cl_covl coe; f := cl_cof coe; count := count + 1; if !*rlverbose then if !*rlqedfs then << if vlv = length cvl then ioto_tprin2t {"-- crossing: ",dpth - vlv}; ioto_prin2 {"[",dpth - length cvl} >> else << if c=0 then << ioto_tprin2t {"-- left: ",length cvl}; c := cl_colength co + 1 >>; ioto_nterpri(length explode c + 4); ioto_prin2 {"[",c}; c := c - 1 >>; v := car cvl; cvl := cdr cvl; f := pasf_qeex(f,v); if !*rlpasfsimplify then f := cl_simpl(f,nil,-1); if f eq 'true then << co := nil; newj := '(true) >> else if null cvl then newj := adjoin(f,newj) else if rl_op f eq 'or then << if !*rlverbose then oldcol := cl_colength co; for each x in rl_argn f do co := cl_save(co,{cl_mkcoel(cvl,x,nil,nil)}); if !*rlverbose then delc := delc + oldcol + length rl_argn f - cl_colength co >> else << if !*rlverbose then oldcol := cl_colength(co); co := cl_save(co,{cl_mkcoel(cvl,f,nil,nil)}); if !*rlverbose then delc := delc + oldcol + 1 - cl_colength(co) >>; if !*rlverbose then << ioto_prin2 "] "; if !*rlqedfs and null cvl then ioto_prin2 ". " >> >>; if !*rlverbose then ioto_prin2{"[DEL:",delc,"/",count,"]"}; return rl_smkn('or,newj) end; procedure pasf_qeex(psi,x); % Presburger arithmetic standard form eliminate an existential % quantifier in front of a quantifier free formula. [psi] is a % formula, [x] is the quantified variable. Returns a quantifier % free formula equivalent to $\exists x \psi()$. begin scalar simpl,normpsi,elimdata; % Debug output if pasf_verbosep() then << prin2 "Eliminating subformula: "; print psi; prin2 "Elimination variable: "; print x >>; % Trivial case check % % /TODO bad solution if not (x memq cl_fvarl1 psi) then << if !*rlverbose then ioto_prin2 "*"; return psi >>; if !*rlverbose then ioto_prin2 "e"; % Computing the elimination normal form normpsi := pasf_elimnf(psi,x); % Getting the elimination data of psi elimdata := pasf_canrep normpsi; % Computing the quantifier free equivalent simpl := pasf_rednf if null elimdata_repr elimdata then pasf_substfc(normpsi,elimdata) else pasf_substf(normpsi,elimdata); return simpl end; procedure pasf_canrep(f); % Presburger arithmetic standard form search for canonical % representants. [f] a formula in elimination normal form with only % range predicates. Returns the elimindation data structure % elimdata. elimdata_join pasf_canrep1(f,nil); procedure pasf_canrep1(f,bvar); % Presburger arithmetic standard form search for canonical % representants subroutine. [f] a formula in elimination normal % form with only range predicates, [bvar] is the list of bounded % variables. Returns the elimindation data structure elimdata. if rl_quap rl_op f then % Formula should be pnf'ed first rederr{"pasf_canrep : Quantifier inside a formula matrix"} else if rl_bquap rl_op f then % Removing bounded quantifiers and adding new bounded % variable to the variable list. pasf_canrep1(rl_mat f,(rl_var f) . bvar) else if rl_boolp rl_op f then for each subf in rl_argn f join pasf_canrep1(subf,bvar) else % We are now sure to have no nested range predicates {pasf_compeld(f,bvar)}; procedure pasf_compeld(atf,bvar); % Presburger arithmetic standard form compute elimination % data. [atf] is an atomic formula, [bvar] is the list of bounded % variables by range predicates. Returns the elimination data. begin scalar op,n,m,max_s,min_s,repr,a_i; % Avoiding formulas with no quantified variable inside if null pasf_leadc atf then return elimdata_new(nil,1,1,nil,nil,nil); % Getting the operator op := pasf_opn atf; n := 1; m := 1; max_s := nil; min_s := nil; repr := nil; if op memq '(cong ncong) then m := lcm(m,pasf_m atf) else if op memq '(equal neq leq geq lessp greaterp) then << n := lcm(n,pasf_leadc atf); a_i := pasf_arg2r atf; % Substituting k's into a_i for each var in bvar do a_i := numr subf(a_i,{(var . nil)}); % Debug output if pasf_verbosep() then << prin2 "s_i = "; print pasf_const a_i >>; max_s := pasf_const a_i; min_s := pasf_const a_i; repr := {pasf_mk2(pasf_op atf,pasf_arg2l atf,a_i)} >>; % Debug output if pasf_verbosep() then << prin2 "lcm(n_i) = "; print n; prin2 "lcm(m_i) = "; print m; prin2 "max_s = "; print max_s; prin2 "min_s = "; print min_s >>; return elimdata_new(repr,n,m,max_s,min_s,nil) end; procedure pasf_consteln(atf); % Presburger arithmetic standard form constant part of an atomic % formula in elimination normal form. [atf] is an atomic formula in % elimination normal form. Returns the constant part of [atf]. pasf_const pasf_arg2r atf; procedure pasf_substfc(psi,elimdata); % Presburger arithmetic standard form subsitute formula with only % congruences. [psi] is the formula in elimination normal form, % [elimdata] is the elimiation data. Returns a quantifier free % formula equivalent to $ex(x,psi)$. begin scalar m; m := addf(elimdata_m elimdata,negf 1); % Debug output if pasf_verbosep() then << prin2 "m = "; print m >>; return pasf_exprng pasf_substfc1(m,psi) end; procedure pasf_substfc1(m,psi); % Presburger arithmetic standard form subsitute formula with only % congruences subprocedure. [m] is the upper range for the range % predicate (SF), [psi] is the formula in elimination normal % form. Returns a range predicate bounded formula. begin scalar subs,rng,k; k := pasf_newvar psi; % Debug output if pasf_verbosep() then << prin2 "Creating new variable "; print k; prin2 "m = "; print m >>; subs := cl_apply2ats1(psi,'pasf_substf2,{k,1,nil}); rng := pasf_mkrng(k,0,if m then m else 0); if m then return rl_mkbq('bex,k,rng,rl_mkn('and,{subs})) else return subs end; procedure pasf_substf(psi,elimdata); % Presburger arithmetic standard form subsitute formula. [psi] is % the formula in elimination normal form and [elimdata] is the % elimination data. Returns a quantifier free formula equivalent to % $ex(x,psi)$. begin scalar n_prime,s,m; s := pasf_ceil(addf(elimdata_min_si elimdata, negf elimdata_min_si elimdata),2); % Debug output if pasf_verbosep() then << prin2 "s = "; print s >>; n_prime := elimdata_n elimdata; % Debug output if pasf_verbosep() then << prin2 "n' = "; print n_prime >>; m := elimdata_m elimdata; % Debug output if pasf_verbosep() then << prin2 "m = "; print m >>; % For each canonical representant in psi return pasf_rednf rl_mkn('or, for each atf in elimdata_repr elimdata collect pasf_exprng if null pasf_arg2l atf then pasf_substf1(0,psi,atf) else pasf_substf1(multf(pasf_leadc atf, addf(s,*lcm(n_prime,m))),psi,atf)); end; procedure pasf_substf1(t_j,psi,atf); % Presburger arithmetic standard form subsitute formula % subprocedure. [t_j] is the range for the range predicate, [psi] % is the formula in elimination normal form and [atf] is of one of % the canonical representants of [psi]. Returns a bounded formula. begin scalar cong,subs,rng,leadc,k; k := pasf_newvar psi; % Debug output if pasf_verbosep() then << prin2 "Creating new variable "; print k >>; % Debug output if pasf_verbosep() then << prin2 "t_j = "; print t_j >>; leadc := pasf_leadc atf; cong := pasf_mk2(pasf_mkop('cong,leadc), addf(pasf_arg2r atf,numr simp k),nil); subs := cl_apply2ats1(psi,'pasf_substf2, {k,leadc,pasf_arg2r atf}); if null t_j then rederr{"pasf_substf1 : t_j is 0"} else rng := pasf_mkrng(k,-t_j,t_j); return rl_mkbq('bex,k,rng,rl_mkn('and,subs . {cong})) end; procedure pasf_substf2(atf,k,n_j,a_j); % Presburger arithmetic standard form subsitute formula % subprocedure. [psi] is an atomic formula in elimination normal % form, [k] is the range variable, [n_j] and [a_j] are the % substitution parameters. Returns the substituted atomic formula. begin scalar n_i,a_i; n_i := pasf_leadc atf; % Returning unchanged formula if no quantified variable in the % formula. if null n_i then return atf; a_i := pasf_arg2r atf; return if pasf_opn(atf) memq '(cong ncong) then pasf_mk2(pasf_mkop(pasf_opn atf,multf(pasf_m atf,n_j)), addf(multf(n_i,a_j),multf(n_i,numr simp k)), multf(n_j,a_i)) else pasf_mk2(pasf_mkop(pasf_opn atf,0), addf(multf(n_i,a_j),multf(n_i,numr simp k)), multf(n_j,a_i)); end; procedure pasf_leadc(atf); % Presburger arithmetic standard form leading coeficient of a % elimination normal form. [atf] is an atomic formula in % elimination normal form. Returns the leading coeficient. if domainp pasf_arg2l atf then % /FIXME Warning, could be a trap, because only nil possible pasf_arg2l atf else lc pasf_arg2l atf; procedure pasf_expand(f); % Presburger arithmetic standard form expand a formula with range % predicates. [f] is a formula with range predicates. Returns an % equivalent formula without range predicates. cl_simpl(pasf_exprng1 f,nil,-1); procedure pasf_exprng(f); % Presburger arithmetic standard form expand range predicate. [f] % is a formula bounded by a range quantifier. Returns an equivalent % quantifier free formula. if !*rlpasfrangeexpand then % Redlog normal form needed here because this function is called % inside the QE process, where the formulas are not neccesary in % redlog normal form. pasf_expand pasf_rednf f else f; procedure pasf_exprng1(f); % Presburger arithmetic standard form expand bounded % quantifier. [f] is a formula bounded only by bounded % quantifiers. Returns an equivalent quantifier free formula. if rl_bquap rl_op f then pasf_exprng2 rl_mkbq(rl_op f,rl_var f,rl_b f, cl_simpl(pasf_exprng1 rl_mat f,nil,-1)) else if rl_boolp rl_op f then rl_mkn(rl_op f,for each subf in rl_argn f collect cl_simpl(pasf_exprng1 subf,nil,-1)) else f; procedure pasf_exprng2(f); % Presburger arithmetic standard form expand bounded % quantifier. [f] is a formula bounded only by one bounded % quantifier. Returns an equivalent quantifier free formula. begin scalar evaltype,terml; % Long or or long and check if rl_op f eq 'bex then evaltype := 'or else if rl_op f eq 'ball then evaltype := 'and else % Unknown operator rederr{"pasf_expand : unknown or illegal quantifier",rl_op f}; % Building the interval to substitute into terml := pasf_b2terml(rl_b f,rl_var f); return rl_mkn(evaltype, for each j in terml collect pasf_subfof(rl_var f,j,rl_mat f)); end; procedure pasf_subfof(var,ex,f); % Presburger arithmetic standard form substitute into a formula. % [var] is the variable to substitute, [ex] is the expression to % substitute and [f] is the formula. Returns the formula where % every occurence of [var] is substituted by [ex]. cl_apply2ats1(f,'pasf_subfof1,{var,ex}); procedure pasf_subfof1(atf,var,ex); % Presburger arithmetic standard form substitute into a formula % subroutinue. [atf] is an atomic formula, [var] is the variable to % substitute and [ex] is the expression to substitute. Returns an % atomic formula where every occurence of [var] is substituted by % [ex]. pasf_mk2(pasf_op atf, numr subf(pasf_arg2l atf,{(var . ex)}), numr subf(pasf_arg2r atf,{(var . ex)})); procedure pasf_newvar(f); % Presburger arithmetic standard form new variable generation. [f] % is a formula. Returns a new variable which is not present in [f]. intern gensym(); procedure pasf_newvar1(f); % Presburger arithmetic standard form new variable generation. [f] % is a formula. Returns a new variable which is not present in [f]. begin scalar varl,varv,expld,l; varl := cl_varl pasf_rednf f; varv := 0; % Checking only the whole varlist for each var in append(car varl,cdr varl) do << expld := explode var; % Looking for k variables if car expld eq 'k then << l := implode cdr expld; if l >= varv then varv := l+1 >> >>; return implode('k . explode(varv)) end; endmodule; end;