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