% ----------------------------------------------------------------------
% $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