% ----------------------------------------------------------------------
% $Id: ofsfmisc.red,v 1.13 1999/04/01 11:25:56 dolzmann Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: ofsfmisc.red,v $
% Revision 1.13 1999/04/01 11:25:56 dolzmann
% Added and corrected comments.
%
% Revision 1.12 1999/03/23 07:41:38 dolzmann
% Changed copyright information.
%
% Revision 1.11 1997/08/24 16:18:51 sturm
% Added service rl_surep with black box rl_multsurep.
% Added service rl_siaddatl.
%
% Revision 1.10 1996/10/23 11:17:45 dolzmann
% Corrected comments.
%
% Revision 1.9 1996/10/07 12:03:26 sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.8 1996/10/03 16:06:09 sturm
% Fixed a bug in ofsf_structat.
%
% Revision 1.7 1996/10/01 10:25:08 reiske
% Introduced new service rltnf and related code.
%
% Revision 1.6 1996/09/30 16:55:59 sturm
% Cleaned up the use of several (conditional) negate-relation procedures.
%
% Revision 1.5 1996/09/05 11:15:19 dolzmann
% Added implementation for black boxes rl_structat, rl_ifstructat, and
% rl_termmlat.
%
% Revision 1.4 1996/08/01 11:45:48 reiske
% Added implementation for black boxes rl_a2cdl and rl_getineq.
%
% Revision 1.3 1996/07/07 14:39:50 sturm
% Added implementation for black box ofsf_eqnrhskernels.
%
% Revision 1.2 1996/05/21 17:14:19 sturm
% Added procedures ofsf_subat and ofsf_subalchk.
%
% Revision 1.1 1996/03/22 12:14:11 sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(ofsf_misc_rcsid!* ofsf_misc_copyright!*);
ofsf_misc_rcsid!* := "$Id: ofsfmisc.red,v 1.13 1999/04/01 11:25:56 dolzmann Exp $";
ofsf_misc_copyright!* :=
"Copyright (c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;
module ofsfmisc;
% Ordered field standard form miscellaneous. Submodule of [ofsf].
procedure ofsf_termprint(u);
% Ordered field standard form term print term. [u] is a SF. The
% return value is not specified. Prints [u] AM-like.
<<
sqprint !*f2q u where !*nat=nil;
ioto_prin2 nil
>>;
procedure ofsf_canegrel(r,flg);
% Ordered field standard form conditionally algberaically negate
% relation. [r] is a relation. Returns a relation $R$. If [flg] is
% non-[nil], then $[R]=[r]$. If [flg] is [nil], then [R] is a
% relation, such that $R(-t,0)$ is equivalent to $[r](t,0)$ for
% every term $t$.
if flg then r else ofsf_anegrel r;
procedure ofsf_anegrel(r);
% Ordered field 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)))
or rederr {"ofsf_anegrel: unknown operator ",r};
procedure ofsf_clnegrel(r,flg);
% Ordered field standard form conditionally logically negate
% relation. [r] is a relation; [flg] is bool. Return a relation
% $R$. If [flg] is non-[nil] [r] is returned. Othewise a relation
% $R$ is returned such that for terms $t_1$, $t_2$ we have
% $R(t_1,t_2)$ equivalent to $\lnot [r](t_1,t_2)$.
if flg then r else ofsf_lnegrel r;
procedure ofsf_lnegrel(r);
% Ordered field 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 rederr {"ofsf_lnegrel: unknown operator ",r};
procedure ofsf_fctrat(atf);
% Ordered field standard form factorize atomic formula. [atf] is an
% atomic formula $l \mathrel{\varrho} 0$. Returns a list $(...,(f_i
% . d_i),...)$, where $f$ is an irreducible SF and $d$ is a
% positive integer. We have $l=c \prod_i g_i^{d_i}$ for an integer
% $c$.
cdr fctrf ofsf_arg2l atf;
procedure ofsf_negateat(f);
% Ordered field standard form negate atomic formula. [f] is an
% atomic formula. Returns an atomic formula equivalent to $\lnot
% [f]$.
ofsf_mkn(ofsf_lnegrel ofsf_op f,ofsf_argn f);
procedure ofsf_varlat(atform);
% Ordered field standard form atomic formula list of variables.
% [atform] is an atomic formula. Returns the variables contained in
% [atform] as a list.
kernels ofsf_arg2l(atform);
procedure ofsf_varsubstat(atf,new,old);
% Ordered field 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].
ofsf_0mk2(ofsf_op atf,numr subf(ofsf_arg2l atf,{old . new}));
procedure ofsf_ordatp(a1,a2);
% Ordered field standard form atomic formula predicate. [a1] and
% [a2] are atomic formulas. Returns [t] iff [a1] is less than [a2].
begin scalar lhs1,lhs2;
lhs1 := ofsf_arg2l a1;
lhs2 := ofsf_arg2l a2;
if lhs1 neq lhs2 then return ordp(lhs1,lhs2);
return ofsf_ordrelp(ofsf_op a1,ofsf_op a2)
end;
procedure ofsf_ordrelp(r1,r2);
% Ordered field standard form relation order predicate.
% [r1] and [r2] are ofsf-relations. Returns a [T] iff $[r1] < [r2]$.
not not (r2 memq (r1 memq '(equal neq leq lessp geq greaterp)));
procedure ofsf_a2cdl(atml);
% Ordered field standard form atomic to case distinction list.
% [atml] is a list of atomic formulas with multiplicity, the right
% hand side of which is always zero. Returns a list, each
% containing a list of case distinction w.r.t. the term $t$, i.e.
% ${t<0,t=0,t>0}$ resp. ${t=0,t neq 0}$.
begin scalar atf,terml,flag;
while atml do <<
atf := caar atml;
atml := cdr atml;
terml := ofsf_arg2l atf . terml;
if not(ofsf_op atf memq '(equal neq)) then flag := T
>>;
return for each x in terml collect
if flag then
{ofsf_0mk2('lessp,x),ofsf_0mk2('equal,x),ofsf_0mk2('greaterp,x)}
else
{ofsf_0mk2('equal,x),ofsf_0mk2('neq,x)}
end;
procedure ofsf_t2cdl(term);
% Ordered field standard form term to case distinction list. [term]
% is a term. Returns a list of full case distinctions w.r.t. the
% term, i.e. ${[term]<0,[term]=0,[term]>0}$.
{ofsf_0mk2('lessp,term),ofsf_0mk2('equal,term),ofsf_0mk2('greaterp,term)};
procedure ofsf_subat(al,f);
begin scalar nlhs;
nlhs := subf(ofsf_arg2l f,al);
if not domainp denr nlhs then
rederr "parametric denominator after substitution";
return ofsf_0mk2(ofsf_op f,numr nlhs)
end;
procedure ofsf_subalchk(al);
for each x in al do
if not domainp denr simp cdr x then
rederr "parametric denominator in substituted term";
procedure ofsf_eqnrhskernels(x);
nconc(kernels numr w,kernels denr w) where w=simp cdr x;
procedure ofsf_getineq(f,bvl);
% Generate theory get inequalities. [f] is a formula, the right
% hand side is always zero; [bvl] is a list of variables. Returns
% the list of all inequalities occuring in [f] not containing any
% variables from [bvl].
begin scalar atml,atf,cdl;
atml := cl_atml f;
while atml do <<
atf := caar atml;
atml := cdr atml;
if ofsf_op atf memq '(neq) and
null intersection(bvl, kernels ofsf_arg2l atf) then
cdl := atf . cdl
>>;
return cdl
end;
procedure ofsf_structat(at,al);
% Orederd field standard form structure of an atomic formula. [at]
% is an atomic formula $([op],l,0)$; [al] is an ALIST. Returns an
% atomic formula. [al] is of the form $(...,(f_i . v_i),...)$ where
% $f_i$ is an SF and $v_i$ is a variable. The left hand side of
% [at] occurs as a key in [al]. Returns the atomic formula
% $[op](v_i,0)$, provided $l=f_i$.
begin scalar lhs;
lhs := ofsf_arg2l at;
if domainp lhs then
return at;
return ofsf_0mk2(ofsf_op at, numr simp cdr assoc(lhs,al))
end;
procedure ofsf_ifstructat(at,al);
begin scalar w,r;
w := fctrf ofsf_arg2l at;
r := car w;
for each x in cdr w do
r := multf(r,expf(numr simp cdr assoc(car x,al),cdr x));
return ofsf_0mk2(ofsf_op at,r)
end;
procedure ofsf_termmlat(at);
% Ordered field 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 ofsf_arg2l at then
{(ofsf_arg2l at . 1)};
procedure ofsf_multsurep(at,atl);
if ofsf_op at eq 'equal then
ofsf_multsurep!-equal(at,atl)
else
ofsf_multsurep!-neq(at,atl);
procedure ofsf_multsurep!-equal(at,atl);
begin scalar c,a;
c := ofsf_arg2l at;
while atl do <<
a := car atl;
atl := cdr atl;
if ofsf_op a eq 'equal and quotf(c,ofsf_arg2l a) then <<
a := 'found;
atl := nil
>>
>>;
return a eq 'found
end;
procedure ofsf_multsurep!-neq(at,atl);
begin scalar c,a;
c := ofsf_arg2l at;
while atl do <<
a := car atl;
atl := cdr atl;
if ofsf_op a eq 'neq and quotf(ofsf_arg2l a,c) then <<
a := 'found;
atl := nil
>>
>>;
return a eq 'found
end;
endmodule; % [ofsfmisc]
end; % of file