reduce-historical/r37/packages/redlog/dvfsfsiat.red

% ----------------------------------------------------------------------
% $Id: dvfsfsiat.red,v 1.9 1999/03/26 08:22:36 dolzmann Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: dvfsfsiat.red,v $
% Revision 1.9  1999/03/26 08:22:36  dolzmann
% Added code for possibly exploding equations and inequalities:
% Introduced new argument sop to the procedures dvfsf_safield and
% dvfsf_saval. Adapted all calls of these procedures to the new
% parameter list. Added procedure dvfsf_compose to compose the result of
% dvfsf_saval1. Added procedure dvfsf_sapfacf for the factorization of
% an equation or an inequality.
%
% Revision 1.8  1999/03/24 12:33:33  dolzmann
% Added and reformatted comments.
% Removed debugging code.
% Replaced gcdf!* by sfto_gcdf!*.
%
% Revision 1.7  1999/03/23 08:45:43  dolzmann
% Changed copyright information.
%
% Revision 1.6  1999/03/19 12:13:04  dolzmann
% Added simplification for atomic formulas of the form a*p+b=0 and a*p+b<>0,
% where a,b in Z and for atomic formulas of the form f || p*g, and p*f | g.
%
% Revision 1.5  1999/01/17 16:25:29  dolzmann
% Changed copyright notice.
% Added simplification procedures described in "P-adic constraint
% solving" by A. Dolzmann and T. Sturm.
%
% Revision 1.4  1999/01/10 12:11:51  dolzmann
% Added simplification of atomic formulas involving powers of p and integers.
% This simplification is only for p-adic valuations correct.
%
% Revision 1.3  1996/10/07 11:32:09  sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.2  1996/07/15 13:32:41  sturm
% Fixed a bug in dvfsf_saval1.
%
% Revision 1.1  1996/07/08 12:15:25  sturm
% Initial check-in.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(dvfsf_siat_rcsid!* dvfsf_siat_copyright!*);
   dvfsf_siat_rcsid!* :=
      "$Id: dvfsfsiat.red,v 1.9 1999/03/26 08:22:36 dolzmann Exp $";
   dvfsf_siat_copyright!* :=
      "Copyright (c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;

module dvfsfsiat;
% Discretely valued field standard simplifier for atomic formulas.
% Submodule of [dvfsf].

procedure dvfsf_simplat1(atf,sop);
   % Discretely valued field simplify atomic formula. [atf] is an
   % atomic formula; [sop] is a boolean operator. Returns a
   % quantifier-free formula that is a simplified equivalent of [atf].
   begin scalar op;
      op := dvfsf_op atf;
      if op eq 'equal or op eq 'neq then
 	 return dvfsf_safield(op,dvfsf_arg2l atf,sop);
      return dvfsf_saval(op,dvfsf_arg2l atf,dvfsf_arg2r atf,sop)
   end;

procedure dvfsf_saval(op,lhs,rhs,sop);
   % Discretely valued field simplify atomic formula built with
   % valuation relation. [op] is one of ['assoc], ['nasso], ['div], or
   % ['sdiv]; [lhs] and [rhs] are SF's; [sop] is a boolean operator.
   % Returns a formula equivalent to $[op]([lhs],[rhs])$.
   begin
      if minusf lhs then lhs := negf lhs;
      if minusf rhs then rhs := negf rhs;
      if lhs = rhs then
 	 return if op eq 'sdiv or op eq 'nassoc then 'false else 'true;
      % At most one of [lhs], [rhs] is zero. The following third reatment
      % of zero sides is probably redundant.
      if null lhs then <<
    	 if op eq 'sdiv then return 'false;
	 if op eq 'nassoc then return dvfsf_safield('neq,rhs,sop);
    	 % We know [op] is one of ['div], ['assoc].
    	 return dvfsf_safield('equal,rhs,sop)
      >>;
      if null rhs then <<
    	 if op eq 'sdiv or op eq 'nassoc then
 	    return dvfsf_safield('neq,lhs,sop);
    	 if op eq 'assoc then
 	    return dvfsf_safield('equal,lhs,sop);
    	 % We know [op eq 'div] now.
    	 return 'true
      >>;
      return dvfsf_saval1(op,lhs,rhs)
   end;

procedure dvfsf_saval1(op,lhs,rhs);
   % Discretely valued field simplify atomic formula built with
   % valuation relation subroutine. [op] is one of [div], [sdiv],
   % [assoc], [nassoc]; [lhs] and [rhs] are nonzero SF's. Returns a
   % formula equivalent to $[op]([lhs],[rhs])$.
   begin scalar gcd,natf1,sff,junct;
      junct := if op eq 'sdiv or op eq 'nassoc then 'and else 'or;
      lhs := dvfsf_vsimpf lhs;
      rhs := dvfsf_vsimpf rhs;
      gcd := sfto_gcdf!*(lhs,rhs);
      lhs := quotf(lhs,gcd);
      rhs := quotf(rhs,gcd);
      natf1 := dvfsf_saval2(op,lhs,rhs);
      if junct eq 'and then <<
	 if natf1 eq 'false then return 'false;
    	 sff := dvfsf_safield('neq,gcd,'and);
      	 return dvfsf_compose('and,natf1,sff)
      >>;
      % We know [junct eq 'or].
      if natf1 eq 'true then return natf1;
      sff := dvfsf_safield('equal,gcd,'or);
      return dvfsf_compose('or,natf1,sff)
   end;

procedure dvfsf_compose(op,at,f);
   % Discretely valued field compose. [op] is either ['or] or ['and];
   % [at] is an atomic formula; [f] is a formula. Returns a formula
   % equivalent to $[op](at,f)$.
   if op eq 'or and (at eq 'true or f eq 'true) then
      'true
   else if op eq 'and and (at eq 'false or f eq 'false) then
      'false
   else if (at eq 'true) or (at eq 'false) then
      f
   else if (f eq 'true) or (f eq 'false) then
      at
   else if (op neq rl_op f) or not(cl_cxfp f) then
      rl_mk2(op,at,f)
   else
      rl_mkn(op,at . rl_argn f);

procedure dvfsf_saval2(op,lhs,rhs);
   % Discretely valued field simplify atomic formula built with
   % valuation relation subroutine. [op] is one of [div], [sdiv],
   % [assoc], [nassoc]; [lhs] and [rhs] are nonzero SF's such that
   % [lhs] and [rhs] are relatively prime. Returns a formula
   % equivalent to $[op]([lhs],[rhs])$.
   begin scalar natf1,w;
      if dvfsf_p!* > 0 then  % Concrete valuation given.
	 natf1 := dvfsf_sacval(op,lhs,rhs)
      else <<
	 w := dvfsf_saaval(op,lhs,rhs);
	 if rl_tvalp w then
	    natf1 := w
	 else if w neq 'failed then <<
	    natf1 := w;   % TODO: Repeat the trivial simplifications for [w].
	    op := dvfsf_op natf1;
	    lhs := dvfsf_arg2l natf1;
	    rhs := dvfsf_arg2r natf1
      	 >> else
	    natf1 := dvfsf_mk2(op,lhs,rhs)
      >>;
      if (op eq 'assor or op eq 'nassoc) and ordp(rhs,lhs) then
	 natf1 := dvfsf_mk2(op,rhs,lhs);
      return natf1
   end;

procedure dvfsf_sacval(op,lhs,rhs);
   % Discretely valued field simplify atomic formula built with
   % valuation relation for concrete given valuation. [op] is one of
   % [div], [sdiv], [assoc], [nassoc]; [lhs] and [rhs] are nonzero
   % SF's. Returns a formula equivalent to $[op]([lhs],[rhs])$.
   % Evaluate variable free atomic formulas and move the domain
   % content to one side.
   begin scalar lcont,rcont,lv,rv;
      if domainp lhs and domainp rhs then <<
	 if op eq 'assoc then
	    return if dvfsf_v lhs = dvfsf_v rhs then 'true else 'false;
	 if op eq 'nassoc then
	    return if dvfsf_v lhs neq dvfsf_v rhs then 'true else 'false;
	 if op eq 'sdiv then
	    return if dvfsf_v lhs < dvfsf_v rhs then 'true else 'false;
	 % We know [op eq 'div] now.
	 return if dvfsf_v lhs <= dvfsf_v rhs then 'true else 'false
      >>;
      % The content is non-zero.
      lcont := sfto_dcontentf lhs;
      lhs := quotf(lhs,lcont);
      rcont := sfto_dcontentf rhs;
      rhs := quotf(rhs,rcont);
      lv := dvfsf_v lcont;
      rv := dvfsf_v rcont;
      if lv >= rv then
 	 lhs := multf(numr simp ((dvfsf_p!*)**(lv-rv)),lhs)
      else
 	 rhs := multf(numr simp ((dvfsf_p!*)**(rv-lv)),rhs);
      return dvfsf_mk2(op,lhs,rhs)
   end;

procedure dvfsf_safield(op,lhs,sop);
   % Discretely valued field simplify atomic formula with field
   % relation. [op] is either ['equal] or ['neq]; [lhs] is an SF;
   % [sop] is a boolean operator.
   % Returns a quantifier-free formula equivalent to $[op]([lhs],0)$.
   begin
      lhs := dvfsf_vsimpf lhs;
      if domainp lhs then
	 if op eq 'equal then
 	    return if null lhs then 'true else 'false
	 else  % [op eq 'neq]
	    return if null lhs then 'false else 'true;
      lhs := sfto_dprpartf lhs;
      if dvfsf_p!*>0 then
 	 return dvfsf_sapfacf(op,lhs,sop);
      lhs := dvfsf_dppower lhs;
      if domainp lhs then
	 return if op eq 'equal then 'false else 'true;
      return dvfsf_sapfacf(op,lhs,sop)
   end;

procedure dvfsf_sapfacf(op,lhs,sop);
   % Discretely valued field standard form polynomial factorization
   % atomic formula with field relation. [op] is either ['equal] or
   % [neq]. [lhs] is an SF. Returns a formula equivalent to
   % $[op](lhs,0)$; [sop] is a boolean operator. This procedure
   % possibly factorize [lhs] to explode the respective atomic
   % formula.
   begin scalar w,junct;
      junct := if op eq 'equal then 'or else 'and;
      if !*rlsifac and (!*rlsiexpla or !*rlsiexpl and sop = junct) then
      	 return rl_smkn(junct,
	    for each x in cdr fctrf lhs collect dvfsf_sapeq(op,car x));
      return dvfsf_sapeq(op,lhs)
   end;

procedure dvfsf_dppower(f);
   % Discretely valued field drop p power. [f] is an SF of the form
   % $(p^n f')$. Returns $f'$ as an SF.
   begin scalar qr,p;
      p := numr simp 'p;
      qr := qremf(f,p);
      while null(cdr qr) do <<
	 f := car qr;
 	 qr := qremf(car qr,p);
      >>;
      return f
   end;

procedure dvfsf_saaval(op,lhs,rhs);
   % Discretely valued field simplify atomic formula for abstract
   % valuation. [op] is one of [div], [sdiv], [assoc], [nassoc]; [lhs]
   % and [rhs] are SF's. Returns ['failed] or an atomic formula
   % equivalent $[op]([lhs],[rhs])$.
   begin scalar w;
      w := dvfsf_sappow(op,lhs,rhs);
      if w neq 'failed then
	 return w;
      w := dvfsf_savpc(op,lhs,rhs);
      if w neq 'failed then
	 return w;
      w := dvfsf_sapureintc(op,lhs,rhs);
      if w neq 'failed then
	 return w;
      w := dvfsf_sapfactor(op,lhs,rhs);
      if w neq 'failed then
	 return w;
      return 'failed
   end;

procedure dvfsf_sappow(op,lhs,rhs);
   % Discretely valued field simplify powers of p in atomic formula.
   % [op] is one of ['div], ['sdiv], ['nassoc], ['assoc]; [lhs] and
   % [rhs] are SF's. Returns ['failed] or a truth value. Simplifies
   % atomic formulas which relates 1 to $z p^n$, for an integer [z]
   % and a positive integer $n$ to a truth value. Otherwise ['failed]
   % is returned.
   begin scalar lp,rp;
      lp := dvfsf_ppowerp lhs;
      rp := dvfsf_ppowerp rhs;
      if rp and lhs = numr simp 1 then
    	 return if op = 'assoc then 'false else 'true;
      if lp and rhs = numr simp 1 then
    	 return if op = 'nassoc then 'true else 'false;
      return 'failed
   end;

procedure dvfsf_savpc(op,lhs,rhs);
   % Discretely valued field simplify atomic formulas build with
   % valuation relation, p, and a constant. [op] is one of [div],
   % [sdiv], [assoc], [nassoc]; [lhs] and [rhs] are SF's, such that
   % [lhs] and [rhs] are relatively prime. Returns ['failed] or an
   % atomic formula equivalent to $[op]([lhs],[rhs])$. The atomic
   % formula is simplified, if it relates $z p^n$ to a constant;
   % otherwise ['failed] is returned.
   %
   % WARNING: This simplifier is correct only for p-adic valued fields.
   %
   begin scalar w,op;
      if not !*rlsifac then
	 return 'failed;
      w := dvfsf_savpc1(op,lhs,rhs);
      if w eq 'failed then
	 return 'failed;
      op := dvfsf_op w;
      if dvfsf_arg2l w = dvfsf_arg2r w then
 	 return if op eq 'nassoc then 'false else 'true;
      return w
   end;

procedure dvfsf_savpc1(op,lhs,rhs);
   % Discretely valued field simplify atomic formulas build with
   % valuation relation, p, and a constant subroutine. [op] is one of
   % [div], [sdiv], [assoc], [nassoc]; [lhs] and [rhs] are SF's, such
   % that [lhs] and [rhs] are relatively prime. Returns ['failed] or
   % an atomic formula equivalent to $[op]([lhs],[rhs])$. The atomic
   % formula is simplified, if it relates $z p^n$ to a constant;
   % otherwise ['failed] is returned.
   begin scalar n;
      return if (domainp rhs) and (n := dvfsf_ppowerp lhs) then <<
      	 if op eq 'assoc then
      	    dvfsf_mk2('nassoc,sfto_zdeqn(rhs,n),numr simp 1)
      	 else if op eq 'nassoc then
      	    dvfsf_mk2('assoc,sfto_zdeqn(rhs,n),numr simp 1)
      	 else if op eq 'div then
      	    dvfsf_mk2('nassoc,sfto_zdgen(rhs,n),numr simp 1)
      	 else if op eq 'sdiv then
      	    dvfsf_mk2('nassoc,sfto_zdgtn(rhs,n),numr simp 1)
      	 else
	    rederr "Bug in dvfsf_savpc"
      >> else if (domainp lhs) and (n := dvfsf_ppowerp rhs) then <<
      	 if op eq 'assoc then
      	    dvfsf_mk2('nassoc,sfto_zdeqn(lhs,n),numr simp 1)
      	 else if op eq 'nassoc then
      	    dvfsf_mk2('assoc,sfto_zdeqn(lhs,n),numr simp 1)
      	 else if op eq 'div then
      	    dvfsf_mk2('assoc,sfto_zdgtn(lhs,n),numr simp 1)
      	 else if op eq 'sdiv then
      	    dvfsf_mk2('assoc,sfto_zdgen(lhs,n),numr simp 1)
      	 else
	    rederr "Bug in dvfsf_savpc"
      >> else
      	 'failed
   end;

procedure dvfsf_ppowerp(u);
   % Discretely valued field power of p predicate. [u] is an SF.
   % Returns [nil] or a positive integer $n$. Tests [u] on
   % representing a polynomial $z p^n$ for an integer $z$ and a
   % natural number $n$.
   begin scalar rou,w;
      rou := sfto_reorder(u,'p);
      w := (not domainp rou and mvar rou = 'p and
     	 domainp lc rou and null red rou);
      if w then
	 return ldeg u
   end;

procedure dvfsf_ppolyp(f);
   % Discretely valued field p polynomial predicate. [f] is an SF.
   % Returns [T] if [f] is a domian element or is a polynomial
   % containing only the variable ['p] otherwise [nil] is returned.
   begin scalar w;
      if domainp f then
	 return T;
      w := kernels f;
      return null cdr w and car w eq 'p
   end;

procedure dvfsf_ppolydec(f);
   % Discretely valued field p polynomial decomposition. [f] is an SF.
   % Returns a list $(...,(a_i,n_i),...)$ such that $[f]=\sum_i
   % a_ip^n_i$ and $n_i>n_{i+1}$.
   if null f then
      nil
   else if domainp f then
      {(f . 0)}
   else
      (lc f . ldeg f) . dvfsf_ppolydec red f;

procedure dvfsf_vsimpf(f);
   % Discretely valued field valuation simplification standard form.
   % [f] is an SF. Returns an SF $f'$, such that for all terms $g$ we
   % have $[f] \mathrel{\varrho} g$ if and only if $f'
   % \mathrel{\varrho} g$.
   begin scalar w,fdc,cep,c,n,cdc;
      if domainp f then
	 return f;
      if not dvfsf_ppolyp f then
	 return f;
      fdc := reversip dvfsf_ppolydec(f);
      w := car fdc;
      fdc := cdr fdc;
      if null fdc then
	 return f;
      n := cdr w;
      c := car w;
      if (c = 1) or (c = -1) then
	 return numr simp {'expt,'p,n};
      cdc := sort(zfactor c,function(lambda(x,y); (cdr x > cdr y)));
      if n + cdr car cdc < cdr car fdc then
	 return numr simp {'times,c,{'expt,'p,n}};
      while cdc do <<
	 cep := car cdc;
	 w := dvfsf_vsimpf1(car cep,cdr cep,n,fdc);
	 if w eq 'failed then
	    cdc := nil
	 else
	    cdc := cdr cdc;
      >>;
      if w eq 'failed then
	 return f;
      return numr simp {'times,c,{'expt,'p,n}};
   end;

procedure dvfsf_vsimpf1(q,m,n,fdc);
   % Discretely valued field valuation simplification standard form
   % subroutine. [f] is an SF. Returns an SF $f'$, such that for all
   % terms $g$ we have $[f] \mathrel{\varrho} g$ if and only if $f'
   % \mathrel{\varrho} g$.
   begin scalar w,k,qp;
      while fdc do <<
	 w := car fdc;  % a pair $(a . n)$ with $a*p^n$ is monomial of [f]
	 k := cdr w - n;
	 if m<k then <<
	    w := nil;
	    fdc := nil
	 >> else <<
	    qp := abs(q)^(m-k+1);
	    if gcdf!*(qp,car w) = qp then
	       fdc := cdr fdc
	    else <<
	       w := 'failed;
	       fdc := nil;
	    >>
      	 >>
      >>;
      if w eq 'failed then
	 return 'failed
   end;

procedure dvfsf_sapureintc(op,lhs,rhs);
   % Discretely valued field simplifiy atomic formulas pure integer
   % constraints. [op] is one of ['assoc], ['nassoc], ['div] or
   % ['sdiv]; [lhs] and [rhs] are SF's. Returns ['failed] or an atomic
   % formula. This procedure simplifies atomic formulas which relates
   % integers.
   if not !*rlsifac then
      'failed
   else if not(domainp lhs and domainp rhs) then
      'failed
   else if op eq 'assoc or op eq 'nassoc then
      dvfsf_mk2(op,sfto_sqfpartz(lhs*rhs),numr simp 1)
   else if op eq 'div then
      dvfsf_mk2('assoc,sfto_sqfpartz lhs,numr simp 1)
   else if op eq 'sdiv then
      dvfsf_mk2('nassoc,sfto_sqfpartz rhs,numr simp 1)
   else
      rederr "bug dvfsf_sapureintc";

procedure dvfsf_sapeq(op,lhs);
   % Discretely valued field simplify atomic formula p equation. [op]
   % is either ['equal] or ['neq]. [lhs] is an SF. Returns an atomic
   % formula equivalent to $[op]([lhs],0)$. This procedures
   % simplifies atomic formulas of the form $[op](z1 p + z2,0)$, with
   % $z1$ and $z2$ relatively prime.
   if not(not(domainp lhs) and mvar lhs eq 'p and ldeg lhs = 1
      and domainp lc lhs and domainp red lhs)
   then
      dvfsf_mk2(op,lhs,nil)
   else if (lc lhs neq 1) or not(minusf red lhs) or not(primep red lhs) then
      if op eq 'equal then 'false else 'true
   else
      dvfsf_mk2(if op eq 'equal then 'nassoc else 'assoc,
	 negf red lhs,numr simp 1);

procedure dvfsf_sapfactor(op,lhs,rhs);
   % Discretely valued field simplify atomic formula p factor. [op] is
   % one of ['assoc], ['nassoc], ['div], or ['sdiv]. [lhs] and [rhs]
   % are SF's. Returns ['failed] or atomic formula equivalent to
   % $[op]([lhs],[rhs])$. This procedures simplifies atomic formulas
   % of the form $f || p*g$, $p*f | g$.
   begin scalar w;
      if op eq 'sdiv then <<
      	 w := qremf(rhs,numr simp 'p);
      	 if null cdr w then
	    return dvfsf_mk2('div,lhs,car w);
	 return 'failed
      >>;
      if op eq 'div then <<
      	 w := qremf(lhs,numr simp 'p);
      	 if null cdr w then
	    return dvfsf_mk2('sdiv,car w,rhs);
	 return 'failed
      >>;
      return 'failed
   end;

endmodule;  % [dvfsfsiat]

end;  % of file