Artifact 769b8252cef31d45f454e0ee3f74b06e47b3bb174b7a9e0a50aa153a4f7b47f4:
- Executable file
r38/packages/redlog/ofsfxopt.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: 26997) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: ofsfxopt.red,v 1.3 2003/01/31 17:07:09 sturm Exp $ % ---------------------------------------------------------------------- % Copyright (c) 1998-2003 Dr. Andreas Dolzmann % ---------------------------------------------------------------------- % $Log: ofsfxopt.red,v $ % Revision 1.3 2003/01/31 17:07:09 sturm % Procedure ofsf_xopt!-check makes cl_simpl(cl_pnf f,nil,-1) now. % This has to be changed later, because this simplification is performed % twice now. % % Revision 1.2 2003/01/14 16:08:50 dolzmann % Fixed a bug in ofsf_xopt!-xopt. ofsf_xopt!-xopt had returned a answer % instead of a formula for quantifier-free formulas. % % Revision 1.1 2003/01/13 09:59:24 dolzmann % Initial check-in. % Extended optimization, formerly called xopt. % %----------------------------------------------------------------------- % Revision 1.3 1999/11/13 16:34:34 dolzmann % Adapted to REDLOG 2.0. Changed copyright message. % % Revision 1.2 1999/11/13 16:07:53 dolzmann % Adapted to REDLOG 2.0. % % Revision 1.1 1998/05/25 06:51:00 dolzmann % Extended optimization: Initial check-in. % This code is the pure optimization coded extract from sopt.red. % Added and corrected comments. Sorted the procedures. % Modified xopt_s2a!-ansl. %----------------------------------------------------------------------- lisp << fluid '(ofsfxopt_rcsid!* ofsfxopt_copyright!*); ofsfxopt_rcsid!* := "$Id: ofsfxopt.red,v 1.3 2003/01/31 17:07:09 sturm Exp $"; ofsfxopt_copyright!* := "Copyright (c) 1998-2003 by Dr. A. Dolzmann" >>; module ofsfxopt; % Extended optimization. A very restricted form of the QE by virtual % substitution. Pnf of input must be an existential quantified weak % parametric linear formula containing only weak relations. % Global variables: used only for statistics % fluid '(ofsf_xopt!-nodes!* ofsf_xopt!-delnodes!* ofsf_xopt!-plnodes!* % ofsf_xopt!-fnodes!* ofsf_xopt!-thcof!* !*rlxoptqe); % % Switches used by xopt: % on1 'rlxopt; % ofsf uses xopt procedures % on1 'rlxoptsb; % select boundary type % on1 'rlxoptpl; % passive list % on1 'rlxoptri; % result inheritance % off1 'rlxoptric; % result inheritance to conatiner % off1 'rlxoptrir; % result inheritance to result % on1 'rlxoptses; % structural elimination sets. %DS % <ANSL> ::= (...,<ANS>,...) % <ANS> ::= (<GD> . <PT>) % <GD> ::= "quantifier free formula" % <PT> ::= (...,<CT>,...) % <CT> ::= (<VAR>,<VALUE>); % <VALUE> ::= Lisp-Prefix smacro procedure ofsf_xopt!-ansl!-mk(l); l; smacro procedure ofsf_xopt!-ansl!-ansl(ansl); ansl; smacro procedure ofsf_xopt!-ans!-mk(gd,pt); gd . pt; smacro procedure ofsf_xopt!-ans!-gd(ans); car ans; smacro procedure ofsf_xopt!-ans!-pt(ans); cdr ans; smacro procedure ofsf_xopt!-pt!-ctl(pt); pt; smacro procedure ofsf_xopt!-pt!-mk(ctl); ctl; smacro procedure ofsf_xopt!-ct!-mk(v,vl); v . vl; smacro procedure ofsf_xopt!-ct!-var(ct); car ct; smacro procedure ofsf_xopt!-ct!-value(ct); cdr ct; %DS % <CO> ::= (...,<CE>,...) % <CE> ::= (<VL>,<FORMULA>,<PT>,<PL>) % <VL> ::= "list of variables to be eliminated" % <FORMULA> ::= "RL-formula" % <PL> ::= (...,<ATOMIC_FORMULA>,...) smacro procedure ofsf_xopt!-co!-mk(cel); cel; smacro procedure ofsf_xopt!-co!-cel(co); co; smacro procedure ofsf_xopt!-ce!-mk(vl,f,pt,pl); {vl,f,pt,pl}; smacro procedure ofsf_xopt!-ce!-vl(ce); car ce; smacro procedure ofsf_xopt!-ce!-f(ce); cadr ce; smacro procedure ofsf_xopt!-ce!-pt(ce); caddr ce; smacro procedure ofsf_xopt!-ce!-pl(ce); cadddr ce; procedure ofsf_xopt!-co!-putl(co,cel); for each ce in cel collect ofsf_xopt!-co!-put(co,ce); smacro procedure ofsf_xopt!-co!-put(co,ce); ce . co; smacro procedure ofsf_xopt!-co!-get(co); co; smacro procedure ofsf_xopt!-co!-length(co); length co; %DS % <CS> ::= (<UBL>,<LBL>,<EQL>) % <UBL> ::= (...,<CP>,...) % "upper bounds" % <LBL> ::= (...,<CP>,...) % "lower bounds" % <EQL> ::= (...,<CP>,...) % "equations" % <CP> ::= "minimal polynomial" | minf | pinf smacro procedure ofsf_xopt!-cs!-mk(ubl,lbl,eql); {ubl,lbl,eql}; smacro procedure ofsf_xopt!-cs!-ubl(cs); car cs; smacro procedure ofsf_xopt!-cs!-lbl(cs); cadr cs; smacro procedure ofsf_xopt!-cs!-eql(cs); caddr cs; smacro procedure ofsf_xopt!-cp!-mk(p); p; smacro procedure ofsf_xopt!-cp!-p(cp); cp; procedure ofsf_xopt!-cs!-null(cs); null car cs and null cadr cs and null caddr cs; %DS % <ES> ::= (...,<CP>,...) smacro procedure ofsf_xopt!-es!-mk(cpl); cpl; smacro procedure ofsf_xopt!-es!-cpl(es); es; procedure ofsf_xopt!-check(f); % Ordered field standard form extended optimization check. [f] is a % formula. Returns non-[nil] if f can be eliminated by using xopt. ofsf_xopt!-check1(cl_simpl(cl_pnf f,nil,-1),nil,T); procedure ofsf_xopt!-check1(f,vl,p); begin scalar op,argl,r; if f eq 'true or f eq 'false then return nil; op := rl_op f; % if op eq 'ex or op eq 'all then if op eq 'ex then return p and ofsf_xopt!-check1(rl_mat f,rl_var f . vl,T); if op eq 'all then return nil; if rl_cxp op then << argl := rl_argn f; r := t; while argl and r do << r := ofsf_xopt!-check1(car argl,vl,nil); argl := cdr argl >>; return r >>; return ofsf_op f memq '('leq,geq,equal) and sfto_linwpp(ofsf_arg2l f,vl) end; procedure ofsf_xopt!-qea(f); % Ordered field standard form extended optimization quantifier % elimination with answer. [f] is an existentially quantified, weak % parametric, linear formula with only weak relations. Returns a % list of pairs $(..., (c_i, A_i), ...)$. The $c_i$ are % quantifier-free formulas, and the $A_i$ are lists of equations. % Entry point for ofsf_qea. begin scalar !*rlxoptqe; return ofsf_xopt!-trans!-ansl ofsf_xopt!-xopt f end; procedure ofsf_xopt!-trans!-ansl(u); % translate ansl. [u] is a ANSL. Returns a answer as required by % [cl_qea]. for each ans in ofsf_xopt!-ansl!-ansl u collect {ofsf_xopt!-ans!-gd ans, for each ct in ofsf_xopt!-pt!-ctl ofsf_xopt!-ans!-pt ans collect {'equal,ofsf_xopt!-ct!-var ct,ofsf_xopt!-ct!-value ct}}; procedure ofsf_xopt!-qe(f); % Ordered field standard form extended optimization quantifier % elimination with answer. [f] is an existentially quantified, weak % parametric, linear formula with only weak relations. Returns a % quantifier free formula equivalent to [f]. Entry point for % ofsf_qe. begin scalar !*rlxoptqe; !*rlxoptqe := T; return ofsf_xopt!-xopt f end; procedure ofsf_xopt!-xopt(f); % Extended optimization. [f] is an existentially quantified, weak % parametric, linear formula with only weak relations; Returns a % ANSL or a quantifier free formual. begin scalar exl,mtr,w,co; scalar !*rlsiatadv,!*rlsitsqspl,!*rlsifac,!*rldavgcd,!*rlsipd,!*rlsipw; integer ofsf_xopt!-delnodes!*,ofsf_xopt!-plnodes!*,ofsf_xopt!-fnodes!*, ofsf_xopt!-thcof!*,ofsf_xopt!-nodes!*; !*rlsipw := T; f := cl_simpl(cl_pnf f,nil,-1); w := cl_splt f; exl := car w; if null exl then if !*rlxoptqe then return f else return ofsf_xopt!-ansl!-mk {ofsf_xopt!-ans!-mk(f,ofsf_xopt!-pt!-mk nil)}; if cdr exl then rederr "ofsf_xopt!-xopt: more than one quantifier block"; exl := car exl; if car exl neq 'ex then rederr "ofsf_xopt!-xopt: not an existential formula"; exl := cdr exl; mtr := cadr w; co := ofsf_xopt!-co!-mk if rl_op mtr neq 'or then {ofsf_xopt!-ce!-mk(exl,mtr,nil,nil)} else for each x in rl_argn mtr collect ofsf_xopt!-ce!-mk(exl,x,nil,nil); if not !*rlxoptqe then return ofsf_xopt!-backsub ofsf_xopt!-elim co; w := ofsf_xopt!-backsub ofsf_xopt!-elim co; if !*rlverbose then ioto_prin2t "Constructing result formula..."; w := for each ans in ofsf_xopt!-ansl!-ansl w collect ofsf_xopt!-ans!-gd ans; w := cl_simpl(rl_smkn('or,w),nil,-1); if !*rlverbose then ioto_prin2t "...done."; return w end; procedure ofsf_xopt!-elim(co); % Quantifier elimination. [co] is a CO. Returns an ANSL. begin scalar w,ce,cel,resl,theo; integer n; if !*rlverbose then ofsf_xopt!-nodes!* := ofsf_xopt!-co!-length co; while co do << if !*rlverbose then n := n+1; % -- Get from container -- w := ofsf_xopt!-co!-get co; ce := car w; co := cdr w; if !*rlverbose then ioto_prin2 {"[",n,"/",ofsf_xopt!-nodes!*}; % -- Eliminate -- cel := ofsf_xopt!-qevar(ce,theo); % Update container ans resl w := ofsf_xopt!-updco(cel,co,resl,theo); co := car w; resl := cadr w; theo := caddr w; % -- Finish -- if !*rlverbose then ioto_prin2 "] "; >>; if !*rlverbose then << ioto_cterpri(); ioto_prin2t {"Number of computed nodes: ",ofsf_xopt!-nodes!*}; ioto_prin2t {"Number of PL hits: ",ofsf_xopt!-plnodes!*}; ioto_prin2t {"Number of identical CE's: ",ofsf_xopt!-delnodes!*}; ioto_prin2t {"Number of FALSE results: ",ofsf_xopt!-fnodes!*}; ioto_prin2t {"Number of CE's deleted by theo: ",ofsf_xopt!-thcof!*}; >>; return ofsf_xopt!-cel2ansl resl; end; procedure ofsf_xopt!-qevar(ce,theo); % Quantifier elimination eliminate variable. [ce] is a CE, [theo] % is a theory. Returns a list of CE's. begin scalar v,cs,es,cel; v := ofsf_xopt!-varsel ce; cs := ofsf_xopt!-cset(ofsf_xopt!-ce!-f ce,v); if ofsf_xopt!-cs!-null cs then return {ofsf_xopt!-ce!-mk(delq(v,ofsf_xopt!-ce!-vl ce), ofsf_xopt!-ce!-f ce, ofsf_xopt!-pt!-mk(ofsf_xopt!-ct!-mk(v,'arbitrary) . ofsf_xopt!-pt!-ctl ofsf_xopt!-ce!-pt ce), ofsf_xopt!-ce!-pl ce)}; if !*rlxoptpl then << cs := ofsf_xopt!-applypl(cs,ofsf_xopt!-ce!-pl ce); if ofsf_xopt!-cs!-null cs then return {ofsf_xopt!-ce!-mk(nil,'false,nil,nil)} >>; es := ofsf_xopt!-eset cs; cel := ofsf_xopt!-succs(ce,es,v,theo); return cel end; procedure ofsf_xopt!-varsel(ce); % Variable selection. [ce] is a CE. Returns a variable. car ofsf_xopt!-ce!-vl ce; procedure ofsf_xopt!-cset(f,v); % Candidate set. [f] is a formula, [v] is a variable. Returns a CS. if !*rlxoptses then ofsf_xopt!-scset(f,v) else ofsf_xopt!-csettrad(f,v); procedure ofsf_xopt!-scset(f,v); % Structural candidate set. [f] is a formula; [v] is a variable; % Returns a CS. begin scalar w; w := ofsf_xopt!-scset1(f,v); if !*rlverbose and (cdr w eq 'finite) then ioto_prin2 "g"; return car w end; procedure ofsf_xopt!-scset1(f,v); % Structural candidate set 1. [f] is a formula; [v] is a variable; % Returns a pair $(\Gamma,\tau)$, where $\gamma$ is a CS and $\tau$ % is either ['finite] or [nil]. if rl_junctp rl_op f then ofsf_xopt!-scsetjunct(f,v) else if cl_atfp(f) then ofsf_xopt!-scsetat(f,v) else rederr {"ofsf_xopt!-scset1: Unexpected operator",rl_op f}; procedure ofsf_xopt!-scsetjunct(f,v); % Structural candidate set junction. [f] is a junction; [v] is a % variable; Returns a pair $(\Gamma,\tau)$, where $\gamma$ is a CS % and $\tau$ is either ['finite] or [nil]. begin scalar w,fl,nl,r; r := ofsf_xopt!-cs!-mk(nil,nil,nil); for each x in rl_argn f do << w := ofsf_xopt!-scset1(x,v); if cdr w then fl := car w . fl else nl := car w . nl >>; if fl then if rl_op f eq 'and then << if !*rlverbose and nl then ioto_prin2 "s"; return ofsf_xopt!-scsetselect fl . 'finite >> else if rl_op f eq 'or and null nl then << for each cs in fl do r := ofsf_xopt!-scsetunion(cs,r); return r . 'finite >>; for each cs in fl do r := ofsf_xopt!-scsetunion(cs,r); for each cs in nl do r := ofsf_xopt!-scsetunion(cs,r); return r . nil end; procedure ofsf_xopt!-scsetselect(csl); % Structural candidate set select. [csl] is a list of CS's. Returns % a CS. car csl; procedure ofsf_xopt!-scsetunion(cs1,cs2); % Structural candidate set union. [cs1] and [cs2] are CS's. Returns a CS. ofsf_xopt!-cs!-mk( union(ofsf_xopt!-cs!-ubl cs1,ofsf_xopt!-cs!-ubl cs2), union(ofsf_xopt!-cs!-lbl cs1,ofsf_xopt!-cs!-lbl cs2), union(ofsf_xopt!-cs!-eql cs1,ofsf_xopt!-cs!-eql cs2)); procedure ofsf_xopt!-scsetat(at,v); % Structural candidate set atomic formula. [at] is an atomic % formula; [v] is a variable; Returns a pair $(\Gamma,\tau)$, where % $\gamma$ is a CS and $\tau$ is either ['finite] or [nil]. begin scalar bt,p; bt := ofsf_xopt!-boundarytype(at,v); p := ofsf_arg2l at; return if bt eq 'ub then ofsf_xopt!-cs!-mk({p},nil,nil) . nil else if bt eq 'lb then ofsf_xopt!-cs!-mk(nil,{p},nil) . nil else if bt eq 'equ then ofsf_xopt!-cs!-mk(nil,nil,{p}) . 'finite else ofsf_xopt!-cs!-mk(nil,nil,nil) . nil end; procedure ofsf_xopt!-boundarytype(at,v); % Boundary type. [at] is an atomic formula; [v] is a variable. % Returns ['ub], ['lb], or ['equ]. begin scalar rel,p,rp,w; rel := ofsf_op at; p := ofsf_arg2l at; if domainp p then return nil; rp := sfto_reorder(p,v); if mvar rp neq v then return nil; if rel eq 'equal then return 'equ; w := lc rp; if not domainp w then rederr "ofsf_xopt!-boundarytype: parametric coefficient"; if not(rel memq '(geq leq)) then rederr {"ofsf_xopt!-boundarytype: unknown relation",rel}; return if minusf w then if rel eq 'geq then 'ub else 'lb else if rel eq 'geq then 'lb else 'ub; end; procedure ofsf_xopt!-csettrad(f,v); % Candidate set traditional style. [f] is a formula, v is a % variable. Returns a CS. begin scalar atl,bt,ubl,lbl,eql,p; atl := cl_atl1(f); for each at in atl do << bt := ofsf_xopt!-boundarytype(at,v); p := ofsf_arg2l at; if bt eq 'ub then ubl := p . ubl else if bt eq 'lb then lbl := p . lbl else if bt eq 'equ then eql := p . eql >>; return ofsf_xopt!-cs!-mk(ubl,lbl,eql) end; procedure ofsf_xopt!-applypl(cs,pl); % TODO: Keine Spezialfaelle von ESET durch PL? % Apply passive list. [cs] is a CS; [pl] is a PL. Returns a CS. if not !*rlxoptpl then cs else if null pl then cs else ofsf_xopt!-cs!-mk(ofsf_xopt!-applypl1(ofsf_xopt!-cs!-ubl cs,pl), ofsf_xopt!-applypl1(ofsf_xopt!-cs!-lbl cs,pl), ofsf_xopt!-applypl1(ofsf_xopt!-cs!-eql cs,pl)); procedure ofsf_xopt!-applypl1(cpl,pl); % Apply passive list 1. [cpl] is a list of CP's; [pl] is a PL. % Returns a list of CP's. for each cp in cpl join if cl_simpl(ofsf_0mk2('equal,ofsf_xopt!-cp!-p cp),pl,-1) eq 'false then << ofsf_xopt!-plnodes!* := ofsf_xopt!-plnodes!*+1; >> else {cp}; procedure ofsf_xopt!-eset(cs); % Elimination set. [cs] is a CS. Retuns an ES. if !*rlxoptsb then ofsf_xopt!-esetos(cs) else ofsf_xopt!-esetbs(cs); procedure ofsf_xopt!-esetos(cs); % Elimination set one sides. [cs] is a CS. Retuns an ES. begin scalar ubl,lbl,eql; ubl := ofsf_xopt!-cs!-ubl cs; lbl := ofsf_xopt!-cs!-lbl cs; eql := ofsf_xopt!-cs!-eql cs; return ofsf_xopt!-es!-mk if null ubl and null lbl then ofsf_xopt!-es!-mk eql else if null ubl then 'pinf . eql else if null lbl then 'minf . eql else if length ubl <= length lbl then 'pinf . union(ubl,eql) else 'minf . union(lbl,eql) end; procedure ofsf_xopt!-esetbs(cs); % Elimination set both sides. [cs] is a CS. Retuns an ES. ofsf_xopt!-es!-mk union( union(ofsf_xopt!-cs!-ubl cs,ofsf_xopt!-cs!-lbl cs),ofsf_xopt!-cs!-eql cs); procedure ofsf_xopt!-succs(ce,es,v,theo); % Successors. [ce] is a CE; [es] is an ES; [v] is a variable; % [theo] is a list of atomic formulas. Returns a list of CE's. begin scalar cel,npl; npl := ofsf_xopt!-ce!-pl ce; for each cp in ofsf_xopt!-es!-cpl es do << % TODO: Abbruch bei TRUE cel := ofsf_xopt!-succs1(ce,cp,v,npl,theo) . cel; npl := ofsf_xopt!-updpl(cp,npl); % TODO: Am Ende ueberfluessig. >>; return reversip cel end; procedure ofsf_xopt!-succs1(ce,cp,v,npl,theo); % Successors 1. [ce] is an CE; [cp] is a CP; [v] is a variable; % [npl] is a PL; [theo] is a theory. Returns a CE. begin scalar p,f,w; p := ofsf_xopt!-cp!-p cp; f := ofsf_xopt!-sub(ofsf_xopt!-ce!-f ce,v,p,theo); return if w then ofsf_xopt!-ce!-mk(nil,'false,nil,nil) else ofsf_xopt!-ce!-mk(delq(v,ofsf_xopt!-ce!-vl ce), f, ofsf_xopt!-pt!-mk(ofsf_xopt!-ct!-mk( v,ofsf_xopt!-solv(p,v)) . ofsf_xopt!-pt!-ctl ofsf_xopt!-ce!-pt ce), ofsf_xopt!-plsub(npl,v,p)) end; procedure ofsf_xopt!-sub(f,v,sol,theo); % TODO: Ist das teuer! % Substitution. [f] is a formula; [v] is a variable; [sol] is a SF; % [theo] is a theory. Returns a formula. begin scalar w; w := ofsf_xopt!-sub1(f,v,sol); if not(!*rlxoptrir) or not(!*rlxoptri) then return cl_simpl(w,theo,-1); w := cl_simpl(w,nil,-1); return if cl_simpl(w,theo,-1) eq 'false then 'false else w end; procedure ofsf_xopt!-sub1(f,v,sol); % Substitution 1. [f] is a formula; [v] is a variable; [sol] is a % SF. Returns a formula. if sol memq '(minf pinf) then cl_apply2ats1(f,'ofsf_xopt!-subiat,{v,sol}) else % cl_apply2ats1(f,'ofsf_xopt!-subat,{v,sfto_reorder(sol,v)}); cl_apply2ats1(f,'ofsf_xopt!-subat,{v,sol}); procedure ofsf_xopt!-subiat(atf,v,it); % Substitution infinity. [atf] is an atomic formula; [v] is a % variable; [it] is either ['pinf] or ['minf]. Returns a formula. begin scalar rel,p,rp,pos; rel := ofsf_op atf; if rel eq 'equal then return if v memq ofsf_varlat atf then 'false else atf; if rel eq 'neq then return if v memq ofsf_varlat atf then 'true else atf; p := ofsf_arg2l atf; if domainp p then return atf; rp := sfto_reorder(p,v); if mvar rp neq v then return atf; pos := if it eq 'pinf then not minusf lc rp else minusf lc rp; return if (pos and rel memq '(geq greaterp)) or (not pos and rel memq '(leq lessp)) then 'true else 'false end; procedure ofsf_xopt!-subat(atf,v,sol); % Substution in atomic formula. [atf] is an atomic formula; [v] is % a variable; [sol] is a SF. Returns an atomic formula. ofsf_0mk2(ofsf_op atf,ofsf_xopt!-sublf(ofsf_arg2l atf,v,sol)); procedure ofsf_xopt!-sublf(p,v,mp); % Substitution linear forms. [p] is a SF, [v] is a kernel, [mp] is % a SF. Returns a SF. begin scalar oldorder,rmp,rp,r; if not(v memq kernels p) then return p; oldorder := setkorder {v}; rmp := reorder mp; % rmp := mp; rp := reorder p; r := if minusf lc rmp then addf(multf(lc rp,red rmp),negf multf(lc rmp,red rp)) else addf(negf multf(lc rp,red rmp),multf(lc rmp,red rp)); setkorder oldorder; return reorder r end; procedure ofsf_xopt!-solv(p,v); % Solve. [p] is either a SF, ['pinf], or ['minf]; [v] is a % variable. Returns Lisp-prefix. begin scalar rp; if p memq '(minf pinf) then return p; rp := sfto_reorder(p,v); return prepsq quotsq(!*f2q reorder negf red rp,!*f2q reorder lc rp) end; procedure ofsf_xopt!-plsub(pl,v,sol); % Passive list substitution. [pl] is a [PL]; [v] is a variable; % [sol] is a SF. Returns a PL. begin scalar w; if not !*rlxoptpl then return nil; if null pl then return nil; w := rl_smkn('and,pl); w := cl_simpl(ofsf_xopt!-sub(w,v,sol,nil),nil,-1); if w eq 'true then return nil; if w eq 'false then rederr {"ofsf_xopt!-plsub: Result",w}; if cl_atfp w then w := {w} else if rl_op w neq 'and then rederr {"ofsf_xopt!-plsub: unexpected operator",rl_op w} else w := rl_argn w; return for each f in w join if cl_atfp f then {f} else << if !*rlverbose then ioto_prin2 "C"; nil >> end; procedure ofsf_xopt!-updpl(cp,pl); % Update passive list. [cp] is a CP; [pl] is a PL. Returns a [PL]. begin scalar w; if not !*rlxoptpl then return nil; w := ofsf_xopt!-cp!-p cp; if w memq '(pinf minf) then return pl; return ofsf_0mk2('neq,w) . pl end; procedure ofsf_xopt!-updco(cel,co,resl,theo); % Update container. [cel] is a list of CE's; [co] is a container; % [resl] is a list of CE's; [theo] is a theory. Returns ['false] or % a list $(C,R,\Theta,m)$, where $C$ is the updated [co], $R$ is % the updated [resl], $\Theta$ is the updated [theo], and $m$ is % the number of conatiner elementes added. begin scalar ce,f,w; while cel do << ce := car cel; cel := cdr cel; f := ofsf_xopt!-ce!-f ce; if f eq 'false then << ofsf_xopt!-fnodes!* := ofsf_xopt!-fnodes!*+1; nil >> else if f eq 'true then << resl := {ce}; co := nil; cel := nil >> else if null ofsf_xopt!-ce!-vl ce then << w := ofsf_xopt!-resinherit(ce,resl,co,theo); resl := car w; co := cadr w; theo := caddr w >> else if rl_op f eq 'or then for each ff in rl_argn f do << co := ofsf_xopt!-ccoput(co, ofsf_xopt!-ce!-mk(ofsf_xopt!-ce!-vl ce, ff, ofsf_xopt!-ce!-pt ce, ofsf_xopt!-ce!-pl ce)); >> else co := ofsf_xopt!-ccoput(co,ce); >>; return {co,resl,theo} end; procedure ofsf_xopt!-resinherit(ce,resl,co,theo); % TODO: Splitting OR's??? % Result inheritance. [ce] is a CE, [resl] is a list of CE's, [co] % is a CO, and [theo] is a theory. Returns a list $(R,C,\Theta)$, % where $R$ is the updated [resl], $C$ is the updated [co] and % $\Theta$ is the updated [theo]. begin scalar f; if ofsf_xopt!-celmember(ce,resl) then return {resl,co,theo}; if not !*rlxoptri then << if !*rlverbose then ioto_prin2 "."; return {ce . resl,co,theo} >>; f := ofsf_xopt!-ce!-f ce; if rl_op f eq 'and then << if !*rlverbose then ioto_prin2 "."; return {ce . resl,co,theo} >>; theo := cl_simpl(rl_smkn('and,cl_nnfnot f . theo),nil,-1); if cl_atfp theo then theo := {theo} else if rl_op theo neq 'and then rederr {"ofsf_xopt!-resinherit: Unexpected operator",rl_op theo} else theo := for each atf in rl_argn theo join if cl_atfp atf then {atf}; if !*rlxoptrir then resl := ofsf_xopt!-thapplycel(resl,theo); if !*rlxoptric then co := ofsf_xopt!-thapplyco(co,theo); % mathprint rl_prepfof rl_smkn('and,theo); if !*rlverbose then ioto_prin2 "."; return {ce . resl,co,theo} end; procedure ofsf_xopt!-celmember(ce,cel); % Container element list member. [ce] is a CE; [cel] is a list of % CE's. Returns [nil] or non-[nil]. begin scalar f,a,scel,flg; f := ofsf_xopt!-ce!-f ce; scel := cel; while scel do << a := car scel; scel := cdr scel; if f = ofsf_xopt!-ce!-f a then << scel := nil; flg := T >> >>; return flg end; procedure ofsf_xopt!-thapplycel(cel,theo); % Apply theory to contaioner element list. [cel] is a list of CE's; % [theo] is a theory. Returns a list of CE's. for each ce in cel join if cl_simpl(ofsf_xopt!-ce!-f ce,theo,-1) neq 'false then {ce}; procedure ofsf_xopt!-thapplyco(co,theo); % Apply theory to container. [co] is an CO. [th] is a theory. % Returns a [CO]. begin scalar co,ce,w,r,f; while co do << w := ofsf_xopt!-co!-get co; ce := car w; co := cdr w; f := cl_simpl(ofsf_xopt!-ce!-f ce,theo,-1); if f eq 'false then ofsf_xopt!-thcof!* := ofsf_xopt!-thcof!* +1 else r := ofsf_xopt!-co!-put(r,ofsf_xopt!-ce!-mk(ofsf_xopt!-ce!-vl ce, f, ofsf_xopt!-ce!-pt ce, ofsf_xopt!-ce!-pl ce)) >>; return r end; procedure ofsf_xopt!-ccoput(co,ce); % Conditionally container put. [ce] is a CE; [co] is a CO. Returns a CO. begin scalar sco,w,f,flg,pl; f := ofsf_xopt!-ce!-f ce; sco := co; while sco do << w := ofsf_xopt!-co!-get(sco); sco := cdr w; w := car w; if ofsf_xopt!-ce!-f w = f then << sco := nil; flg := T >> >>; if flg then << co := delq(w,co); pl := intersection(ofsf_xopt!-ce!-pl ce,ofsf_xopt!-ce!-pl w); ce := ofsf_xopt!-ce!-mk( ofsf_xopt!-ce!-vl ce,f,ofsf_xopt!-ce!-pt ce,pl); ofsf_xopt!-delnodes!* := ofsf_xopt!-delnodes!*+1 >> else ofsf_xopt!-nodes!* := ofsf_xopt!-nodes!*+1; return ofsf_xopt!-co!-put(co,ce) end; procedure ofsf_xopt!-cel2ansl(cel); % Container element list to answer list. [cel] is a list of CE's. % Returns an ANSL. ofsf_xopt!-ansl!-mk for each ce in cel collect ofsf_xopt!-ans!-mk(ofsf_xopt!-ce!-f ce,ofsf_xopt!-ce!-pt ce); procedure ofsf_xopt!-backsub(ansl); % Back substitution answer list. [ansl] is an ANSL. Returns an % ANSL. The returned answer list is in a more convenient form. ofsf_xopt!-ansl!-mk for each ans in ofsf_xopt!-ansl!-ansl ansl collect ofsf_xopt!-backsubans ans; procedure ofsf_xopt!-backsubans(ans); % Back substitution answer. [ans] is an ANS. Returns an ANS. The % returned answer is in a more convenient form. ofsf_xopt!-ans!-mk( ofsf_xopt!-ans!-gd ans,ofsf_xopt!-backsubpt ofsf_xopt!-ans!-pt ans); procedure ofsf_xopt!-backsubpt(pt); % Back substitution point. [pt] is a PT. Returns a PT. The returned % point is in a more convenient form. begin scalar subl,w; return ofsf_xopt!-pt!-mk for each ct in ofsf_xopt!-pt!-ctl pt collect << w := prepsq subsq(simp ofsf_xopt!-ct!-value ct,subl); subl := (ofsf_xopt!-ct!-var ct . w) . subl; ofsf_xopt!-ct!-mk(ofsf_xopt!-ct!-var ct,w) >> end; endmodule; % ofsfxopt end; % of file