% ----------------------------------------------------------------------
% $Id: acfsfsism.red,v 1.3 1999/04/12 09:26:00 sturm Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: acfsfsism.red,v $
% Revision 1.3 1999/04/12 09:26:00 sturm
% Updated comments for exported procedures.
%
% Revision 1.2 1999/03/23 08:05:19 dolzmann
% Changed copyright information.
% Added fluids for the rcsid of the file and for the copyright information.
%
% Revision 1.1 1997/08/22 17:30:42 sturm
% Created an acfsf context based on ofsf.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(acfsf_sism_rcsid!* acfsf_sism_copyright!*);
acfsf_sism_rcsid!* :=
"$Id: acfsfsism.red,v 1.3 1999/04/12 09:26:00 sturm Exp $";
acfsf_sism_copyright!* := "Copyright (c) 1995-1999 A. Dolzmann and T. Sturm"
>>;
module acfsfsism;
% Algebraically closed field standard form smart simplification.
% Submodule of [acfsf].
%DS
% <IRL> ::= (<IR>,...)
% <IR> ::= <PARA> . <DB>
% <DB> ::= (<LE>,...)
% <LE> ::= <LABEL> . <ENTRY>
% <LABEL> ::= <INTEGER>
% <ENTRY> ::= <ACFSF RELATION> . <STANDARD QUOTIENT>
procedure acfsf_smrmknowl(knowl,v);
% Algebraically closed 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].
if null knowl then
nil
else if v member kernels caar knowl then
acfsf_smrmknowl(cdr knowl,v)
else <<
cdr knowl := acfsf_smrmknowl(cdr knowl,v);
knowl
>>;
procedure acfsf_smcpknowl(knowl);
% Algebraically closed field smart simplification copy knowledge.
% [knowl] is an IRL. Returns an IRL. Copies [knowl] and the
% contained IR's and DB's.
for each ir in knowl collect
car ir . append(cdr ir,nil);
procedure acfsf_smupdknowl(op,atl,knowl,n);
% Algebraically closed 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.
begin scalar w,ir,a;
while atl do <<
a := if op eq 'and then car atl else acfsf_negateat car atl;
atl := cdr atl;
ir := acfsf_at2ir(a,n);
if w := assoc(car ir,knowl) then <<
cdr w := acfsf_sminsert(cadr ir,cdr w);
if cdr w eq 'false then <<
atl := nil;
knowl := 'false
>> % else [acfsf_sminsert] has updated [cdr w] destructively.
>> else
knowl := ir . knowl
>>;
return knowl
end;
procedure acfsf_smmkatl(op,oldknowl,newknowl,n);
% Algebraically closed 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.
acfsf_irl2atl(op,newknowl,n);
procedure acfsf_smdbgetrel(abssq,db);
if abssq = cddar db then
cadar db
else if cdr db then
acfsf_smdbgetrel(abssq,cdr db);
procedure acfsf_at2ir(atf,n);
% Algebraically closed field standard form atomic formula to IR.
% [atf] is an atomic formula; [n] is an integer. Returns the IR
% representing [atf] on level [n].
begin scalar op,par,abs,c;
op := acfsf_op atf;
abs := par := acfsf_arg2l atf;
while not domainp abs do abs := red abs;
par := addf(par,negf abs);
c := sfto_dcontentf(par);
par := quotf(par,c);
abs := quotsq(!*f2q abs,!*f2q c);
return par . {n . (op . abs)}
end;
procedure acfsf_irl2atl(op,irl,n);
% Algebraically closed field standard form IRL to atomic formula
% list. [irl] is an IRL; [n] is an integer. Returns a list of
% atomic formulas containing the level-[n] atforms encoded in IRL.
for each ir in irl join acfsf_ir2atl(op,ir,n);
procedure acfsf_ir2atl(op,ir,n);
(for each le in cdr ir join
if car le = n then {acfsf_entry2at(op,cdr le,a)}) where a=!*f2q car ir;
procedure acfsf_entry2at(op,entry,parasq);
if !*rlidentify then
cl_identifyat acfsf_entry2at1(op,entry,parasq)
else
acfsf_entry2at1(op,entry,parasq);
procedure acfsf_entry2at1(op,entry,parasq);
acfsf_0mk2(acfsf_clnegrel(car entry,op eq 'and),
numr addsq(parasq,cdr entry));
procedure acfsf_sminsert(le,db);
% Algebraically closed field standard form smart simplify insert.
% [le] is a marked entry; [db] is a database. Returns a database.
% Destructively inserts [le] into [db].
begin scalar a,w,scdb,oscdb;
repeat <<
w := acfsf_sminsert1(cadr car db,cddr car db,cadr le,cddr le,car le);
if w and not idp w then << % identifiers [false] and [true] possible.
db := cdr db;
le := w
>>
>> until null w or idp w or null db;
if w eq 'false then return 'false;
if w eq 'true then return db;
if null db then return {le};
oscdb := db;
scdb := cdr db;
while scdb do <<
a := car scdb;
scdb := cdr scdb;
w := acfsf_sminsert1(cadr a,cddr a,cadr le,cddr le,car le);
if w eq 'true then <<
scdb := nil;
a := 'true
>> else if w eq 'false then <<
scdb := nil;
a := 'false
>> else if w then <<
cdr oscdb := scdb;
le := w
>> else
oscdb := cdr oscdb
>>;
if a eq 'false then return 'false;
if a eq 'true then return db;
return le . db
end;
procedure acfsf_sminsert1(r1,a,r2,b,n);
% Algebraically closed field standard form smart simplify insert.
% [r1], [r2] are relations, [a], [b] are absolute summands in SQ
% representation; [n] is the current level. Returns [nil], [false],
% [true], or a marked entry. Simplification of $\alpha=[r2](f+b,0)$
% under the condition $\gamma=[r1](f+a,0)$ is considered: [nil]
% means there is no simplification posssible; [true] means that
% $\gamma$ implies $\alpha$; [false] means that $\alpha$
% contradicts $\gamma$; the atomic formula encoded by a resulting
% marked entry wrt. $f$ is equivalent to $\alpha$ under $\gamma$.
begin scalar w,diff,n;
diff := numr subtrsq(a,b);
if null diff then <<
w := acfsf_smeqtable(r1,r2);
if w eq 'false then return 'false;
% [w eq r1]
return 'true
>>;
if minusf diff then <<
w := acfsf_smordtable(r1,r2);
if atom w then return w;
if eqcar(w,r1) and cdr w then return 'true;
return n . (car w . if cdr w then a else b)
>>;
w := acfsf_smordtable(r2,r1);
if atom w then return w;
if eqcar(w,r1) and null cdr w then return 'true;
return n . (car w . if cdr w then b else a)
end;
procedure acfsf_smeqtable(r1,r2);
% Algebraically closed field standard form smart simplify equal
% absolute summands table. [r1], [r2] are relations. Returns
% [false] or a relation $R$ such that $R(f+a,0)$ is equivalent to
% $[r1](f+a,0) \land [r2](f+a,0)$.
if r1 eq r2 then r1 else 'false;
procedure acfsf_smordtable(r1,r2);
% Algebraically closed field standard form smart simplify ordered
% absolute summands table. [r1], [r2] are relations. Returns [nil],
% which means that no simplification is possible, [false] or a pair
% $R . s$ where $R$ is a relation and $s$ is one of [T], [nil]. For
% absolute summands $a<b$ we have $[r1](f+a,0) \land [r2](f+b,0)$
% equivalent to $R(f+a,0)$ in case $[s]=[T]$ or to $R(f+b,0)$ in
% case $[s]=[nil]$.
if r1 eq 'equal and r2 eq 'equal then
'false
else if r1 neq r2 then
'equal . (r1 eq 'equal);
endmodule; % [acfsfsism]
end; % of file