Artifact 348ba515c3776c7ddf77170fff078745b64fc986d6e22d115127a6c6803bc1af:
- Executable file
r38/packages/redlog/dvfsfsism.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: 8257) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: dvfsfsism.red,v 1.3 1999/05/06 12:18:41 sturm Exp $ % ---------------------------------------------------------------------- % Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm % ---------------------------------------------------------------------- % $Log: dvfsfsism.red,v $ % Revision 1.3 1999/05/06 12:18:41 sturm % Updated comments for exported procedures. % % Revision 1.2 1999/03/23 08:47:12 dolzmann % Changed copyright information. % Corrected comments for extracting with exc. % % Revision 1.1 1999/03/21 13:36:50 dolzmann % Initial check-in. % Smart simplification for discretely valued fields based on susi. % % ---------------------------------------------------------------------- lisp << fluid '(dvfsf_sism_rcsid!* dvfsf_sism_copyright!*); dvfsf_sism_rcsid!* := "$Id: dvfsfsism.red,v 1.3 1999/05/06 12:18:41 sturm Exp $"; dvfsf_sism_copyright!* := "Copyright (c) 1995-1999 A. Dolzman and T. Sturm" >>; module dvfsfsism; % Discretely valued field standard form simplify smart. Submodule of % [dvfsf]. This module provides the black boxes [rl_smupdknowl], % [rl_smrmknowl], [rl_smcpknowl], [rl_smmkatl], and [rl_susirmknowl] % to [cl_simpl]. They are used with switch [rlsism] on. procedure dvfsf_smupdknowl(op,atl,knowl,n); % Discretely valued field smart simplification update knowledge. % [op] is one of [and], [or]; [atl] is a list of (simplified) % atomic formulas; [knowl] is a conjunctive IRL; [n] is the current % level. Returns an IRL. Destructively updates [knowl] wrt. the % [atl] information. Accesses the switch [rlsusi]. if !*rlsusi then cl_susiupdknowl(op,atl,knowl,n) else cl_smupdknowl(op,atl,knowl,n); procedure dvfsf_smrmknowl(knowl,v); % Discretely valued field smart simplification remove from % knowledge. [knowl] is an IRL; [v] is a variable. Returns an IRL. % Destructively removes all information about [v] from [knowl]. % Accesses the switch [rlsusi]. if !*rlsusi then dvfsf_susirmknowl(knowl,v) else cl_smrmknowl(knowl,v); procedure dvfsf_smcpknowl(knowl); % Discretely valued field smart simplification copy knowledge. % [knowl] is an IRL. Returns an IRL. Copies [knowl]. Accesses the % switch [rlsusi]. if !*rlsusi then cl_susicpknowl(knowl) else cl_smcpknowl(knowl); procedure dvfsf_smmkatl(op,knowl,newknowl,n); % Discretely valued field smart simplification make atomic formula % list. [op] is one of [and], [or]; [oldknowl] and [newknowl] are % IRL's; [n] is an integer. Returns a list of atomic formulas. % Accesses the switch [rlsusi]. if !*rlsusi then cl_susimkatl(op,knowl,newknowl,n) else cl_smmkatl(op,knowl,newknowl,n); procedure dvfsf_susirmknowl(knowl,v); % Discretely valued field susi remove knowledge. [knowl] is a % KNOWL; [v] is a variable. Returns a KNOWL. Remove all information % about [v] from [knowl]. for each p in knowl join if v memq dvfsf_varlat car p then nil else {p}; procedure dvfsf_susibin(old,new); % Discretely valued field standard form susi binary smart simplification. % [old] and [new] are LAT's. Returns ['false] or a SUSIPRG. We % assume that [old] is a part of a already existence KNOWL and new % has to be added to this KNOWL. begin scalar oop,olhs,orhs,olev,nop,nlhs,nrhs,nlev,!*rlsiexpl; olev := cdr old; old := car old; oop := dvfsf_op old; olhs := dvfsf_arg2l old; orhs := dvfsf_arg2r old; nlev := cdr new; new := car new; nop := dvfsf_op new; nlhs := dvfsf_arg2l new; nrhs := dvfsf_arg2r new; if olhs = nlhs and orhs = nrhs then return dvfsf_susibin1(oop,nop,nlhs,nrhs,nlev); if (olhs = nrhs and orhs = nlhs) then % [oop], [noop] cannot be [equal], [neq] return dvfsf_susibin2(oop,nop,nlhs,nrhs,nlev); if (oop eq 'equal or oop eq 'neq) and nop neq 'equal and nop neq 'neq and dvfsf_susibin!-eqlhsmatch(nlhs,nrhs,olhs) then return dvfsf_susibin1(oop,nop,nlhs,nrhs,nlev); if (nop eq 'equal or nop eq 'neq) and oop neq 'equal and oop neq 'neq and dvfsf_susibin!-eqlhsmatch(olhs,orhs,nlhs) then return dvfsf_susibin1(oop,nop,olhs,orhs,nlev); return nil end; procedure dvfsf_susibin!-eqlhsmatch(lhs,rhs,eqlhs); % Discretely valued field standard form super simplifier binary % smart simplification equal left hand side match. Check if % $[lhs]-[rhs]=[eqlhs]$. begin scalar w; w := dvfsf_simplat1(dvfsf_0mk2('equal,addf(lhs,negf rhs)),nil); if not rl_tvalp w then return dvfsf_arg2l w = eqlhs; return nil end; procedure dvfsf_susibin1(rold,rnew,lhs,rhs,nlev); if rold eq rnew then '((delete . t)) else if rold eq 'neq then if rnew eq 'equal then 'false else if rnew eq 'sdiv or rnew eq 'nassoc then '((delete . nil)) else nil else if rold eq 'sdiv then if rnew eq 'neq or rnew eq 'div or rnew eq 'nassoc then '((delete . t)) else % [rnew memq '(assoc equal)] 'false else if rold eq 'div then if rnew eq 'sdiv or rnew eq 'assoc or rnew eq 'equal then '((delete . nil)) else if rnew eq 'nassoc then {'(delete . nil),'(delete . t), 'add . (dvfsf_mk2('sdiv,lhs,rhs) . nlev)} else nil else if rold eq 'assoc then if rnew eq 'sdiv or rnew eq 'nassoc then 'false else if rnew eq 'div then '((delete . t)) else if rnew eq 'equal then '((delete . nil)) else % [rnew eq 'neq] nil else if rold eq 'equal then if rnew eq 'neq or rnew eq 'sdiv or rnew eq 'nassoc then 'false else % [rnew memq '(div, assoc)] '((delete . t)) else if rold eq 'nassoc then if rnew eq 'sdiv then '((delete . nil)) else if rnew eq 'assoc or rnew eq 'equal then 'false else if rnew eq 'div then {'(delete . nil),'(delete . t), 'add . (dvfsf_mk2('sdiv,lhs,rhs) . nlev)} else % [rnew eq 'neq] '((delete . t)) else rederr {"BUG IN dvfsf_susibin1(",rold,",",rnew,")"}; procedure dvfsf_susibin2(rold,rnew,nlhs,nrhs,nlev); % Smart simplification with crossed sides. Assumed to be called % with valuation relations only, and also not with two of the % symmetric relations [assoc], [nassoc]. if rold eq 'div then if rnew eq 'sdiv then 'false else if rnew eq 'div then {'(delete . nil),'(delete . t), 'add . (dvfsf_simplat1(dvfsf_mk2('assoc,nlhs,nrhs),nil) . nlev)} else if rnew eq 'assoc then '((delete . nil)) else if rnew eq 'nassoc then {'(delete . nil),'(delete . t), 'add . (dvfsf_mk2('sdiv,nrhs,nlhs) . nlev)} else nil else if rold eq 'sdiv then if rnew eq 'div or rnew eq 'sdiv or rnew eq 'assoc then 'false else if rnew eq 'nassoc then '((delete . t)) else nil else if rold eq 'nassoc then if rnew eq 'sdiv then '((delete . nil)) else if rnew eq 'div then {'(delete . nil),'(delete . t), 'add . (dvfsf_mk2('sdiv,nlhs,nrhs) . nlev)} else nil else if rold eq 'assoc then if rnew eq 'sdiv then 'false else if rnew eq 'div then '((delete . t)) else nil else nil; procedure dvfsf_susipost(atl,knowl); % Discretely valued field standad form susi post simplification. [atl] is a % list of atomic formulas. [knowl] is a KNOWL. Returns a list % $\lambda$ of atomic formulas, such that % $\bigwedge[knowl]\land\bigwedge\lambda$ is equivalent to % $\bigwedge[knowl]\land\bigwedge[atl]$ atl; procedure dvfsf_susitf(at,knowl); % Discretely valued field standard form susi transform. [at] is an % atomic formula, [knowl] is a knowledge. Returns an atomic formula % $\alpha$ such that $\alpha\land\bigwedge[knowl]$ is equivalent to % $[at]\land\bigwedge[knowl]$. $\alpha$ has possibly a more % convenient relation than [at]. at; endmodule; % [dvfsfsism] end; % of file