Artifact 42e47366c54a179d8a49da7508e0db0b9605ec10d29f3095cb084fd9c1c61aa2:
- Executable file
r38/packages/redlog/ofsfhqe.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: 64637) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: ofsfhqe.red,v 1.7 2003/11/07 12:39:55 dolzmann Exp $ % ---------------------------------------------------------------------- % Copyright (c) 2003 Andreas Dolzmann and Lorenz Gilch % ---------------------------------------------------------------------- % $Log: ofsfhqe.red,v $ % Revision 1.7 2003/11/07 12:39:55 dolzmann % Changed comments. Removed lines that were commented out. % % Revision 1.6 2003/10/24 11:55:45 gilch % Renamed !*rlrqtfcsplit to !*rlhqetfcsplit. % Renamed !*rlrqvb to !*rlhqevb. % Renamed !*rlrqvarsel to !*rlhqevarsel. % Renamed !*rlrqvarselx to !*rlhqevarselx. % Renamed !*rlrqdim0 to !*rlhqedim0. % Renamed !*rlrqtheory to !*rlhqetheory. % Renamed !*rlrqgbred to !*rlhqegbred. % Renamed !*rlrqconnect to !*rlhqeconnect. % Renamed !*rlrqstrconst to !*rlhqestrconst. % Renamed !*rlrqgbdimmin to !*rlhqegbdimmin. % Renamed !*rlrqgen to !*rlhqegen. % Renamed ofsf_rqtheo!* to ofsf_hqetheo!*. % Renamed ofsf_rqxvars!* to ofsf_hqexvars!*. % % Revision 1.5 2003/10/24 07:17:17 dolzmann % Added lost spaces after numbers. % % Revision 1.4 2003/10/23 15:33:43 gilch % Overworked verbose messages. % % Revision 1.3 2003/10/23 15:04:17 dolzmann % Overworked verbose messages. % % Revision 1.2 2003/10/21 15:47:54 gilch % Corrected wrong prefix ofsf_ to gbsc. % % Revision 1.1 2003/10/21 15:20:06 gilch % Moved rlprojects/{gbdim.red,d0.red,qenf.red,rrcqe.red} into this module. % Changed prefix. % Renamed switch rlrqselectxn to rlrqvarsel. % Renamed switch rlrqselectxn2 to rlrqvarselx. % Renamed switch rlrqverbose to rlrqvb. % Renamed switch rlrqtoplevelonly to rlrqdim0. % Renamed switch rlrqinitialcd to rlrqtheory. % Moved switch declarations to redlog.red. % Moved inital switch setting to redlog.red. % Moved fluid declarations for switches to ofsf.red. % Renamed fluid rlrqgeneric!* to ofsf_rqtheo and rlrqgenvar to ofsf_rqxvars. % Renamed rrcqe_rrcqe to ofsf_hqe. % Renamed rrcqe_rrcqegen to ofsf_ghqe. % Renamed rrcqegenres to rl_s2a!-ghqe and moved to rlami. % Renamed ofsf_mkf to ofsf_rqrequantify and ofsf_mkf(!) to ofsf_sfl2f. % Renamed procedure ofsf_simp to ofsf_rqsimpl. % Renamed procedure ofsf_htl to ofsf_mvp. % Renamed procedure ofsf_main to ofsf_d0main and ofsf_main to ofsf_d0main1. % % Revision 1.9 2003/08/19 15:02:26 gilch % Fixed a bug in rrcqe_genvar. % % Revision 1.8 2003/07/21 11:27:58 gilch % Added switches rlrqgen, rlrqgeneric, rlrqgenvar. Added procedures % rrcqe_rrcqegenres, rrcqe_rrcqegen, rrcqe_genvar. Updated rrcqe_rrcqe for % generic QE. % % Revision 1.7 2003/06/26 11:45:13 gilch % Fixed bugs in rrcqe_rrcnfblockqe and rrcqe_connect. % % Revision 1.6 2003/06/25 13:16:37 gilch % Added verbose outputs. % % Revision 1.5 2003/05/27 15:22:28 gilch % Added procedures rrcqe_connect, rrcqe_samephi, rrcqe_samephip, % rrcqe_connectrrcnf, rrcqe_smkn, rrcqe_conjp. Added switch rlrqconnect. % Updated procedures rrcqe_rrcnfeliminate and rrcqe_rrcnfblockqe for use with % rlrqconnect. % % Revision 1.4 2003/05/07 11:36:33 gilch % Added switch rlrqtoplevelonly and updated rrcqe_rrcqe for use with it. Added % procedured rrcqe_mkf,rrcqe_mkf2 and rrcqe_mkf3. % % Revision 1.3 2003/05/02 08:58:27 gilch % Added switch rlrqverbose. % % Revision 1.2 2003/04/29 14:34:02 gilch % Added procedure rrcqe_simp, added verbose outputs. % % Revision 1.1 2003/04/25 13:00:58 gilch % Initial check-in. % % ---------------------------------------------------------------------- lisp << fluid '(ofsf_hqe_rcsid!* ofsf_hqe_copyright!*); ofsf_hqe_rcsid!* := "$Id: ofsfhqe.red,v 1.7 2003/11/07 12:39:55 dolzmann Exp $"; ofsf_hqe_copyright!* := "Copyright (c) 2003 by A. Dolzmann and L. Gilch" >>; module ofsfhqe; % Ordered fields standard form Hermitian quantifier elimination. % Real Root Counting Quantifier Elimination. % Input: A First-order formula % Output: A quantifier-free formula, which is equivalent to the input formula. procedure ofsf_ghqe(f); % Generic Real Root Counting Quantifier Elimination. [f] is a first-order % formula. Returns an equivalent quantifier-free formula. begin scalar res,ofsf_hqetheo!*,ofsf_hqexvars!*,!*rlhqegen; ofsf_hqetheo!* := nil; ofsf_hqexvars!* := nil; !*rlhqegen := T; res := ofsf_hqe f; !*rlhqegen := nil; ofsf_hqexvars!* := nil; return {rl_smkn('and,rl_thsimpl ofsf_hqetheo!*),res} end; procedure ofsf_hqe(phi); % Real Root Counting Quantifier Elimination. [phi] is a first-order % formula. Returns a quantifier-free formula. Wrapper for % [ofsf_hqe0] managing [rlqgvb]. begin scalar w,svrlhqevb,svcgbverbose; svrlhqevb := !*rlhqevb; svcgbverbose := !*cgbverbose; if not !*rlverbose then off1 'rlhqevb; if not(!*cgbverbose and !*rlverbose and !*rlhqevb) then off1 'cgbverbose; w := ofsf_hqe0 phi; onoff('rlhqevb,svrlhqevb); onoff('cgbverbose,svcgbverbose); return w end; procedure ofsf_hqe0(phi); % Real Root Counting Quantifier Elimination. [phi] is a first-order formula. % Returns a quantifier-free formula. begin scalar phi1,ql,firstblock;integer n; if !*rlhqevb then ioto_tprin2 {"+++++ simplifying input formula of RRCQE with ", cl_atnum phi," atomic formulas... "}; phi1 := cl_simpl(phi,nil,-1); if !*rlhqevb then ioto_prin2 {"done. Number of atomic formulas now: ",cl_atnum phi1}; if phi1 member {'true,'false} then return phi1; if !*rlhqevb then ioto_tprin2 "+++++ building prenex normal form... "; phi1 := cl_pnf phi1; if !*rlhqevb then ioto_prin2 "done."; ql := cl_splt phi1; phi1 := cadr ql; ql := car ql; if !*rlhqegen and null ofsf_hqexvars!* then ofsf_hqexvars!* := ofsf_genvar ql; while not null ql and not firstblock do << if !*rlverbose then << n:=n+1; ioto_tprin2 {"+++++ Eliminating ",car ql," (",length ql -n+1, ioto_cplu(" block",length ql -n+1)," left)"} >>; phi1 := ofsf_rrcnfblockqe(car ql, phi1); if phi1 member {'true,'false} then ql := nil else << if !*rlhqedim0 then firstblock := t; ql := cdr ql >> >>; if !*rlhqevb then ioto_tprin2 {"+++++ leaving RRCQE: ", cl_atnum phi1," atomic formulas"}; return ofsf_rqrequantify(ql,phi1) end; procedure ofsf_rqrequantify(ql,phi); % Construction of a quantified formula. [ql] is a list of the form % $ (Q v_{1} ... v_{k})$, where $Q$ is either $ex$ or $all$ and % $v_{1}, ... v_{k}$ are identifiers, [phi] is a formula. Returns a % formula. if not !*rlhqedim0 or null ql then phi else ofsf_rqrequantify2(ql,phi); procedure ofsf_rqrequantify2(ql,phi); % Subroutine of ofsf_rqrequantify. [ql] is a list of the form % $ (Q v_{1} ... v_{k})$, where $Q$ is either $ex$ or $all$ and % $v_{1}, ... v_{k}$ are identifiers, [phi] is a formula. Returns a % formula. begin; while not null ql do << phi := ofsf_rqrequantify3(caar ql,cdar ql,phi); ql := cdr ql >>; return phi end; procedure ofsf_rqrequantify3(q,varl,phi); % Subroutine of ofsf_rqrequantify2. [q] is one of $ex$ or $all$, % [varl] is a list of identifiers, [phi] is a formula. Returns a % formula. if null varl then phi else ofsf_rqrequantify3(q,cdr varl,rl_mkq(q,car varl,phi)); procedure ofsf_rrcnfblockqe(ql,phi); % Elimination of one quantifier block. [ql] is a list of the form % $ (Q v_{1} ... v_{k})$, where $Q$ is either $ex$ or $all$ and $v_{1}, ... % v_{k}$ are identifiers, [phi] is a quantifier-free formula. Returns a % quantifier-free formula. begin scalar psi,gamma; integer i; if !*rlhqevb then ioto_tprin2 "+++++ building positive normal form ... "; if car ql eq 'all then psi := cl_nnfnot phi else psi := cl_nnf phi; if !*rlhqevb then << ioto_prin2 {"done, now ",cl_atnum psi," atomic formulas"}; ioto_tprin2 "+++++ building RRC normal forms ..." >>; gamma := ofsf_connect ofsf_rrcnf(psi,cdr ql); if gamma member {'true,'false} then psi := gamma else << if !*rlhqevb then ioto_prin2 {"done."}; % if !*rlverbose then % ioto_tprin2 {"+++++ ",length gamma," conjunctions to eliminate."}; psi := 'false; for each elem in gamma do << if !*rlverbose then << i := i+1; ioto_tprin2 {"++++ ",length gamma -i +1, ioto_cplu(" conjunction", length gamma -i +1 neq 1)," left"} >>; psi := ofsf_rqsimpl(rl_smkn('or, {psi,ofsf_rrcnfeliminate(elem,cdr ql)})); % if !*rlverbose then % ioto_tprin2 {"+++++ Eliminated conjunction ",i} >> >>; if car ql eq 'all then psi := cl_nnfnot psi; return psi end; procedure ofsf_rrcnfeliminate(rrcnf,varl); % Elimination of a conjunction. [rrcnf] is a RRCNF, [varl] is a list % of identifiers. Returns a quantifier-free formula. if null car rrcnf and null cadr rrcnf and null caddr rrcnf then ofsf_rqsimpl ofsf_smkn('and,cadddr rrcnf) else if !*rlhqeconnect then if ofsf_conjp cadddr rrcnf then ofsf_rqsimpl rl_smkn('and,{cadddr rrcnf,ofsf_qenf(cadddr rrcnf, car rrcnf,cadr rrcnf,caddr rrcnf,varl)}) else ofsf_rqsimpl rl_smkn('and,{cadddr rrcnf,ofsf_qenf('true,car rrcnf, cadr rrcnf,caddr rrcnf,varl)}) else ofsf_rqsimpl rl_smkn('and,{rl_smkn('and,cadddr rrcnf),ofsf_qenf( rl_smkn('and,cadddr rrcnf),car rrcnf,cadr rrcnf, caddr rrcnf,varl)}); procedure ofsf_connect(rrcnfl); % Connects RRCNF's with same EPL, GPL, NPL. [rrcnfl] is a list of RRCNF's. % Returns a list of RRCNF's. begin scalar samephi,newlist,l; if rrcnfl member {'true,'false} or not !*rlhqeconnect then return rrcnfl; l := for each elem in rrcnfl collect {sort(car elem,'ordp), sort(cadr elem,'ordp),sort(caddr elem,'ordp), rl_smkn('and,cadddr elem)}; while not null l do << samephi := ofsf_samephi(car l,cdr l); newlist := (car samephi) . newlist; l := cadr samephi >>; return newlist end; procedure ofsf_samephi(rrcnf,rrcnfl); % Connects RRCNF's with same EPL, GPL, NPL as in first argument. [rrcnf] is % a RRCNF, [rrcnfl] is a list of RRCNF's. Returns a list of the form: % $(rrcnf1 rrcnfl1)$, where $rrcnf1$ is a RRCNF and $rrcnfl1$ is a % list of RRCNF's. begin scalar rrcnf1,rrcnfl1; rrcnf1 := rrcnf; while not null rrcnfl do << if ofsf_samephip(rrcnf,car rrcnfl) then rrcnf1 := ofsf_connectrrcnf(rrcnf, car rrcnfl) else rrcnfl1 := (car rrcnfl) . rrcnfl1; rrcnfl := cdr rrcnfl >>; return {rrcnf1, rrcnfl1} end; procedure ofsf_samephip(r1,r2); % Predicate, if two RRCNF's have same EPL, GPL, NPL. [r1] and [r2] are % RRCNF's. Returns T or NIL. (car r1 = car r2) and (cadr r1 = cadr r2) and (caddr r1 = caddr r2); procedure ofsf_connectrrcnf(r1,r2); % Connects two RRCNF's with same EPL, GPL, NPL. [r1] and [r2] are % RRCNF's. Returns a RRCNF. if cadddr r1 = 'true or cadddr r2 = 'true then {car r1, cadr r1, caddr r1, 'true} else {car r1, cadr r1, caddr r1, rl_smkn('or,{cadddr r1,cadddr r2})}; procedure ofsf_smkn(op,phi); % Formula construction. [op] is either OR or AND, [phi] is either a THEORY % or a formula. Returns the formula $(op phi)$, only if rlhqeconnect is off, % else [phi] itself. if not !*rlhqeconnect then rl_smkn(op,phi) else phi; procedure ofsf_conjp(f); % Tests, if a a formula is a conjunction. [f] is a formula. Returns T or % NIL. if listp f and rl_op f eq 'or then nil else t; procedure ofsf_genvar(l); % Get variables from quantifier blocks. [l] is a list of the form % $(... (q v_{1} ... v_{k}) ...)$, where $q$ is a quantifier and $v_{1}$, % ..., $v_{k}$ are identifiers. Returns a list of identifiers, the list of % all identifiers. if null l then nil else append(cdar l, ofsf_genvar cdr l); % Procedures for RRCNF computations: procedure ofsf_rrcnf(m,vl); % Ordered field standard form real root counting normal form. [m] % is a quantifier-free formula; [vl] is a list of variables. % Returns a truth value or a list of triplets % $(\eta,\gamma,\nu,\theta)$, where $\eta$, $\gamma$, and $\nu$ are % lists of polynomials coming from equations, $>$-constraints, and % $\neq$-constraints, respectively; $\theta$ is a theory. begin scalar w; if !*rlhqevb then {"++++ computing DNF of formula with ",cl_atnum m," atomic formulas"}; w := cl_dnf m; if !*rlhqevb then {"++++ finished DNF Computation: ",cl_atnum w," atomic formulas"}; if rl_tvalp w then return w; w := if rl_op w eq 'or then cdr w else {w}; return for each br in w join if rl_op br eq 'and then ofsf_rrcnf1(cdr br,vl) else ofsf_rrcnf1({br},vl) end; %DS % <RRCNF> ::= (...,(<EPL>,<GPL>,<NPL>,<THEORY>),...) % <EPL> ::= (...,SF,...) left hand sides of equations % <GPL> ::= (...,SF,...) left hand sides of $>$-ATF's % <NPL> ::= (...,SF,...) left hand sides of $\neq$-ATF's % <THEORY> ::= (...,ATF,...) ATF's containing only parameters procedure ofsf_new(); {{nil,nil,nil,nil}}; procedure ofsf_addequal(rrcnf,lhs); << for each v in rrcnf do car v := lhs . car v; rrcnf >>; procedure ofsf_addgreaterp(rrcnf,lhs); << for each v in rrcnf do cadr v := lhs . cadr v; rrcnf >>; procedure ofsf_addlessp(rrcnf,lhs); begin scalar neglhs; neglhs := negf lhs; for each v in rrcnf do cadr v := neglhs . cadr v; return rrcnf end; procedure ofsf_addneq(rrcnf,lhs); << for each v in rrcnf do caddr v := lhs . caddr v; rrcnf >>; procedure ofsf_addgeq(rrcnf,lhs); for each v in rrcnf join {{lhs . car v,cadr v,caddr v,cadddr v}, {car v,lhs . cadr v,caddr v,cadddr v}}; procedure ofsf_addleq(rrcnf,lhs); begin scalar neglhs; neglhs := negf lhs; return for each v in rrcnf join {{lhs . car v,cadr v,caddr v,cadddr v}, {car v,neglhs . cadr v,caddr v,cadddr v}} end; procedure ofsf_addtheo(rrcnf,at); << for each v in rrcnf do cadddr v := at . cadddr v; rrcnf >>; procedure ofsf_rrcnf1(atl,vl); % Ordered field standard form real root counting normal form % subroutine. [atl] is a list of atomic formulas; [vl] is a list of % variables. Returns a list of lists $(\eta,\gamma,\nu,\theta)$, % where $\eta$, $\gamma$, and $\nu$ are lists of polynomials coming % from equations, $>$-constraints, and $\neq$-constraints, % respectively; $\theta$ is a theory. begin scalar resl,op,lhs; resl := ofsf_new(); for each at in atl do << op := rl_op at; lhs := ofsf_arg2l at; resl := if null intersection(kernels lhs,vl) then ofsf_addtheo(resl,at) else if op eq 'equal then ofsf_addequal(resl,lhs) else if op eq 'greaterp then ofsf_addgreaterp(resl,lhs) else if op eq 'lessp then ofsf_addlessp(resl,lhs) else if op eq 'neq then ofsf_addneq(resl,lhs) else if op eq 'geq then ofsf_addgeq(resl,lhs) else if op eq 'leq then ofsf_addleq(resl,lhs) >>; return resl end; % ----------------------------------------------------------------------------- % Quantifier Elimination of a first-order formula in elimination normal form % ----------------------------------------------------------------------------- % Quantifier elimination of formulas in normal form. % Input: A first-order formula $ phi $ and a formula $ xi $, which is a % conjunction of atomic formulas, whose identifiers are independent of the % bounded identifiers in $ phi $. The atomic formulas of $ phi $ contains only % relations with $ > $, $ = $ or $ neq $. Every relation of $ phi$ % contains at least one bounded variable. The polynomials of $ xi $ are square- % primitiv, and the polynomials of equalities and inequalities are squarefree. % Output: a quantifier-free formula $ psi $, so that % $ psi AND xi $ is equivalent to $ phi AND xi $. procedure ofsf_qenf(xi,flist,glist,hlist,varl); % Quantifier elimination of formulas in elimination normal form. % [xi] is a conjunction of atomic formulas, [flist], [glist] and [hlist] % are lists of SF's, [varl] is a list of identifiers. Returns % a quantifier-free formula. begin; if !*rlverbose then ioto_tprin2 {"+++ entering QENF: theo:", length xi," r:",length flist," s:", length glist," t:",length hlist}; if xi = 'false then << if !*rlverbose then ioto_tprin2 {"+++ leaving QENF (0)"}; return 'false >> else if null flist and null glist and null hlist then << if !*rlverbose then ioto_tprin2 {"+++ leaving QENF (0)"}; return 'true >> else if null flist then return ofsf_caser0(xi,varl,glist,hlist) else return ofsf_eliminategsys(xi,flist,glist,hlist,varl) end; procedure ofsf_eliminategsys(xi,flist,glist,hlist,varl); % Elimination of all branches of corresponding Green Groebner System. [xi] % is a conjunctionof atomic formulas. [flist], [glist] and [hlist] % are lists of SF's, [varl] is a list of identifiers. Returns a % quantifier-free formula. begin scalar s,ita,gb,dim,psi;integer i; if !*rlverbose then ioto_tprin2 {"++ computing green Groebner system ... "}; s := ofsf_ggsys(flist,varl,xi); if !*rlverbose then ioto_prin2 {"done"}; psi := 'false; for each branch in s do << if !*rlverbose then << i := i+1; ioto_tprin2 {"++ ",length s - i + 1, " branch(es) left"} >>; ita := ofsf_mkconj car branch; gb := cadr branch; if !*rlhqevb then ioto_tprin2 {"++ computing dimension of branch ... "}; dim := ofsf_dim(gb,varl); if !*rlhqevb then ioto_tprin2 "done"; psi := ofsf_or(psi,ofsf_eliminatedim(gb,glist,hlist,varl,dim,ita,xi)) >>; if !*rlverbose then ioto_tprin2 {"+++ leaving QENF (",cl_atnum psi, ")"}; return psi end; procedure ofsf_eliminatedim(gb,glist,hlist,varl,dim,ita,xi); % Case disjunction depending of dimension of $Id(gb)$. [gb],[glist],and % [hlist] are lists of SF's, [varl] is a list of identifiers, [dim] is a % list of the form $(d ivarl)$, where $d$ indicates the dimension of the % ideal and $ivarl$ a maximally independent set of identifiers, [ita] is % a list of atomic formulas, [xi] is a conjunction of atomic formulas. % Returns a quantifier-free formula. if car dim = -1 then 'false else if car dim = 0 then ofsf_and(ita,ofsf_d0main(gb,varl,glist,hlist)) else if car dim = length varl then ofsf_and(ita,ofsf_casedimn(ita,xi,varl,glist,hlist)) else ofsf_and(ita,ofsf_casedim(ita,xi,ofsf_remvarl(varl,cadr dim), cadr dim,gb,glist,hlist)); procedure ofsf_caser0(xi,varl,glist,hlist); % Case, that there are no equations in phi. % [xi] is a conjunction of atomic formulas, [varl] is a list of identifiers, % [glist] and [hlist] are lists of SF's. Returns a % quantifier-free formula. begin scalar xn,remvarl,psi,phi12,phi3,phi4,neqlist; % if !*rlverbose then % ioto_prin2 "[case #f = 0]"; if !*rlhqevarsel then << xn := ofsf_selectxn(varl,glist); remvarl := setdiff(varl,{xn}) >> else << xn := car varl; remvarl := cdr varl >>; if !*rlhqevb then ioto_tprin2 "++ transforming Matrix in case #f = 0 ..."; psi := ofsf_transformmatrix(xn,glist,hlist); if !*rlhqevb then ioto_tprin2 " done"; neqlist := car psi; phi12 := cadr psi; phi3 := caddr psi; phi4 := cadddr psi; psi := ofsf_and(neqlist,phi12); if psi = 'true then << if !*rlverbose then ioto_tprin2 {"+++ leaving QENF [r=0] (0)"}; return psi >>; if !*rlhqevb then ioto_tprin2 {"++ Eliminating phi3: ",length phi3," subformulas"}; psi := ofsf_or(psi,ofsf_eliminatephi34(xi,phi3,xn,glist,neqlist)); if !*rlhqevb then << ioto_tprin2 {"++ phi3 eliminated."}; ioto_tprin2 {"++ eliminating phi4: ",length phi4," subformulas"} >>; psi := ofsf_or(psi,ofsf_eliminatephi34(xi,phi4,xn,glist,neqlist)); if !*rlhqevb then ioto_tprin2 {"++ phi4 eliminated."}; if !*rlverbose then ioto_tprin2 {"+++ leaving QENF [r=0] (",cl_atnum psi, ")"}; if psi = 'true or psi = 'false then return psi else if not null remvarl then if !*rlhqedim0 then return ofsf_mknewf2(remvarl,psi) else return ofsf_hqe0 ofsf_and(xi,ofsf_mknewf2(remvarl,psi)) else return psi end; procedure ofsf_eliminatephi34(xi,phi34,xn,glist,neqlist); % Eliminate conjunctions of $phi3$ and $phi4$. [xi] is a conjunction of % atomic formulas, [phi34] is a list of the form % $(... (condl f) ...)$, where $condl$ is a list of lists of atomic % formulas and $f$ a SF, [xn] is an identifier, [glist] is a list of SF's, % [neqlist] is a quantifier-free formula. Returns a quantifier-free formula. begin scalar foundtrue,condl,c,phi; phi := 'false; while not null phi34 and not foundtrue do << condl := caar phi34; if !*rlhqevb then ioto_tprin2 {"+ Eliminating subformula of phi3/phi4, ", length condl," cases..."}; while not null condl and not foundtrue do << if !*rlhqevb then ioto_tprin2 "checking consistence ... "; c := ofsf_consistent(xi,car condl); if !*rlhqevb then ioto_prin2 "done."; if car c then phi := ofsf_or(phi,ofsf_and(neqlist,ofsf_and(cadr c, ofsf_qenfcase0(car condl,xn,glist,cadar phi34)))); if phi = 'true then foundtrue := t; condl := cdr condl >>; phi34 := cdr phi34 >>; return phi end; procedure ofsf_selectxn(varl,glist); % Selects variable, depending on switch rlhqevarselx;. % [varl] is a list of identifiers, [glist] is a list of SF's. Returns an % identifier. begin scalar res; if !*rlhqevb then ioto_prin2 "selecting Xn in case r=0 ..."; if !*rlhqevarselx then res := ofsf_selectxn2(varl, glist) else res := ofsf_selectxn1(varl,glist); if !*rlhqevb then ioto_prin2 " done."; return res end; procedure ofsf_selectxn1(varl,glist); % Select variable, so that the residue class rings have minimal dimension. % [varl] is a list of identifiers, [glist] is a list of SF's. Returns an % identifier. begin scalar vl2,d,oldorder,d2,du,elem1;integer d1; if null glist or null cdr varl then return car varl; vl2 := varl; while not null vl2 do << oldorder := setkorder {car vl2}; d1 := 0; du := nil; for each elem in glist do << elem1 := reorder elem; if domainp elem1 or mvar elem1 neq car vl2 then d2 := 0 else d2 := ldeg elem1; if d2 > d1 then d1 := d2; if null du or d2 < du then du := d2; >>; if null d or d1 <= car d then << d := {du,d1,car vl2}; vl2 := cdr vl2 >> else << vl2 := nil; d := nil >>; setkorder oldorder >>; if not null d then return caddr d else return car varl end; procedure ofsf_selectxn2(varl,glist); % Alternative version of ofsf_selectxn. [varl] is a list of identifiers, % [glist] is a list of SF's. Returns an identifier. begin scalar vl2,l,xl,oldorder,elem1,dl; if null glist or null cdr varl then return car varl; vl2 := varl; dl := ofsf_difference glist; while not null vl2 do << oldorder := setkorder {car vl2}; xl := ofsf_gethexponent(car vl2,glist); for each elem in dl do << elem1 := reorder elem; if domainp elem1 or mvar elem1 neq car vl2 then xl := 0 . xl else xl := (ldeg elem1) . xl >>; l := ((car vl2) . sort(xl,'geq)) . l; setkorder oldorder; vl2 := cdr vl2 >>; return ofsf_getminvar l end; procedure ofsf_difference(l); % Computes all differences from elements of a list. [l] is a list of SF's. % Returns a list. begin scalar res; while not null cdr l do << for each elem in cdr l do res := lto_insert(addf(car l, negf elem),res); l := cdr l >>; return res end; procedure ofsf_gethexponent(x,l); % Gets highest exponent of a variable of each elemnt of a list. [x] is an % identifier, [l] is a list of SF's. Returns a list of integers. begin scalar xl,elem1; for each elem in l do << elem1 := reorder elem; if domainp elem1 or mvar elem1 neq x then xl := 0 . xl else xl := (ldeg elem1 - 1) . xl >>; return xl end; procedure ofsf_getminvar(l); % Subroutine of ofsf_selectxn. [l] is a list of the form $(v i1 ... is)$, % where $v$ is an identifier and $i1$,...,$in$ are integers. Returns an % identifier. begin scalar res,m; if null cdar l then return caar l; for each elem in l do << if null res or cadr elem < m then << res := {(car elem) . cddr elem}; m := cadr elem >> else if cadr elem = m then res := ((car elem) . cddr elem) . res >>; if length res = 1 then return caar res else return ofsf_getminvar res end; procedure ofsf_consistent(xi,cond); % Tests, if both arguments are consistent. [xi] and [cond] are formulas. % Returns a list with first element T or NIL and second element the % difference of [cond] and [xi]. begin scalar xi2,cond2; if xi eq 'true then return {t, cond} else if cond eq 'true then return {t,'true}; xi2 := if rl_op xi neq 'and then {xi} else cdr xi; cond2 := if rl_op cond neq 'and then {cond} else cdr cond; return ofsf_consistent1(list2set xi2,cond2) end; procedure ofsf_consistent1(xi,cond); % Subroutine of ofsf_consistent. [xi] and [cond] are lists of atomic % formulas. Returns a list with first element T or NIL and second element % the difference of [cond] and [xi]. begin scalar found,xi1,cond1; xi1 := xi; cond1 := cond; while not found and not null xi1 do << while not null cond1 do << if rl_op car xi1 eq 'equal and rl_op car cond1 eq 'neq and quotf(ofsf_arg2l car cond1, ofsf_arg2l car xi1) then << cond1 := nil; found := t >> else if rl_op car cond1 eq 'equal and rl_op car xi1 member {'neq,'greaterp,'lessp} and quotf(ofsf_arg2l car xi1, ofsf_arg2l car cond1) then << cond1 := nil; found := t >> else cond1 := cdr cond1 >>; cond1 := cond; xi1 := cdr xi1 >>; if found then return {not found} else return {not found, rl_smkn('and,setdiff(cond,xi))} end; procedure ofsf_transformmatrix(xn,gl,hl); % Matrix transformation w.r.t inner bounded variable. [xn] is an % identifier, [gl] and [hl] are lists of SF's. % Returns a list: $ ( (and (neq hk 0) ... ) (or phi1 phi2) phi3 phi4) $. begin scalar xn,neqlist,glist,phi1,phi2,phi3,phi4, phi3phi4,phi1orphi2; neqlist := hl; glist := gl; if not null glist then << phi3phi4 := ofsf_getphi3phi4(xn,glist); phi3 := car phi3phi4; phi4 := cadr phi3phi4; phi1 := ofsf_buildphi1(xn,glist); phi2 := ofsf_buildphi2(xn,glist) >>; neqlist := ofsf_buildhkneq0(xn,neqlist); if null phi1 then phi1orphi2 := 'true else phi1orphi2 := ofsf_or(phi1, phi2); return {neqlist, phi1orphi2, phi3,phi4} end; procedure ofsf_getphi3phi4(xn,phi); % Construction of conditions for formulas $ phi3 $ and $ phi4 $. % [xn] is an identifier,[phi] is a list of SF's. Result has % the form: $ (..(condl equation)..) $, where $condl$ is a list of atomic % formulas and $equation$ is a SF. begin scalar conj,phi3,phi4; for each formulal on phi do << conj := ofsf_getconj3(xn,car formulal); if conj neq 'false then phi3 := conj . phi3; for each formula in cdr formulal do << conj := ofsf_getconj4(xn,car formulal,formula); if conj neq 'false then phi4 := conj . phi4 >> >>; phi3 := list2set phi3; phi4 := list2set phi4; return {phi3, phi4} end; procedure ofsf_getconj3(xn,f); % Subroutine of ofsf_getphi3phi4. [xn] is an identifier, [f] is a SF. % Result is FALSE or a list of the form $ (cond f)$, % where $cond$ is list of formulas and $f$ is a SF. % If one formula of $cond$ is true, then f isn't a % constant function. $cond$ may also be {TRUE}, if f definitly isn't a % constant function wrt. [xn]. begin scalar d,notconst; d := numr difff(f,xn); notconst := ofsf_getnotconst(xn,d); if notconst = 'true then return {{'true}, d} else if notconst = 'false then return 'false else return {notconst,d} end; procedure ofsf_getneq0f(xn,f); % Conditions for not zero-function.[xn] is an identifier, [f] is a SF. % Result is the formula, that f isn't the constant function 0 without OR. begin scalar res,df,oldorder; oldorder := setkorder(xn . kord!*); df := reorder f; setkorder oldorder; if null df then return 'false; while not null df do if domainp df then << df := nil; res := nil >> else if mvar df neq xn then << res := ofsf_0mk2('neq, df) . res; df := nil >> else if domainp lc df then << df := nil; res := nil >> else << res := ofsf_0mk2('neq, lc df) . res; df := red df >>; if null res then return 'true else return list2set res end; procedure ofsf_getneq0fgen(xn,f); % Conditions for not zero-function in generic case.[xn] is an % identifier, [f] is a SF. Result is the formula, that f isn't the % constant function 0 without OR. begin scalar res,df,oldorder; oldorder := setkorder(xn . kord!*); df := reorder f; setkorder oldorder; if null df then return 'false; while not null df do if domainp df then << df := nil; res := nil >> else if mvar df neq xn then << res := ofsf_0mk2('neq, df) . res; df := nil >> else if domainp lc df then << df := nil; res := nil >> else if not intersection(kernels lc df, ofsf_hqexvars!*) then << ofsf_hqetheo!* := ofsf_0mk2('neq, lc df) . ofsf_hqetheo!*; df := nil; res := nil >> else << res := ofsf_0mk2('neq, lc df) . res; df := red df >>; if null res then return 'true else return list2set res end; procedure ofsf_getconj4(xn,f1,f2); % Subroutine of ofsf_getphi3phi4. [xn] is an identifier, [f1], [f2] are % SF's. Result is FALSE or a list of the form $ (cond d)$, % where $cond$ is list of formulas and $d$ is a SF. % If one formula of $cond$ is true, % then $d := f1 - f2$ isn't a constant function. $cond$ may also be {TRUE}, % if $f1 - f2$ definitly isn't a constant function wrt to [xn]. begin scalar s,notconst; s := addf(f1,negf f2); notconst := ofsf_getnotconst(xn,s); if notconst = 'true then return {{'true}, s} else if notconst = 'false then return 'false else return {notconst,s} end; procedure ofsf_getnotconst(xn,f); % Conditions for "not constant function" wrt to [xn]. [xn] is an identifier, % [f] is a SF. Result is the formula, that f isn't a % constant function wrt. [xn] without OR. begin scalar res,df,oldorder; oldorder := setkorder(xn . kord!*); df := reorder f; if !*rlhqegen then res := ofsf_getnotconstfgen(xn,df,nil) else res := ofsf_getnotconstf(xn,df,nil); setkorder oldorder; return res end; procedure ofsf_getnotconstf(xn,f,l); % Conditions for "not constant function" wrt to [xn]. [xn] is an identifier, % [f] is a SF, [l] is a list. Result is the formula, that f isn't a % constant function wrt. [xn] without OR. if domainp f or mvar f neq xn then if null l then 'false else cdr l else if domainp lc f then if null l then 'true else l else if null l then ofsf_getnotconstf(xn,red f, {ofsf_0mk2('equal, ofsf_normcond lc f), ofsf_0mk2('neq, ofsf_normcond lc f)}) else if car l eq 'false then cdr l else if car l eq 'true then l else if ofsf_quottest(sfto_sqfpartf lc f,car l) then ofsf_getnotconstf(xn,red f,l) else ofsf_getnotconstf(xn,red f, ofsf_and1(ofsf_0mk2('equal, ofsf_normcond lc f),car l) . ofsf_and1(ofsf_0mk2('neq, ofsf_normcond lc f), car l) . cdr l); procedure ofsf_normcond(f); % Normalize Condition. [f] is a SF. Returns a SF, % its squarefree part without primitive part. sfto_sqfpartf sfto_dprpartf f; procedure ofsf_getnotconstfgen(xn,f,l); % Conditions for "not constant function" wrt to [xn] in generic % case. [xn] is an identifier, [f] is a SF. Result is the formula, % that f isn't a constant function wrt. [xn] without OR. if domainp f or mvar f neq xn then if null l then 'false else cdr l else if domainp lc f then if null l then 'true else l else if not intersection(kernels lc f, ofsf_hqexvars!*) then << ofsf_hqetheo!* := ofsf_0mk2('neq, lc f) . ofsf_hqetheo!*; if null l then 'true else l >> else if null l then ofsf_getnotconstf(xn,red f, {ofsf_0mk2('equal, ofsf_normcond lc f), ofsf_0mk2('neq, ofsf_normcond lc f)}) else if car l eq 'false then cdr l else if car l eq 'true then l else if ofsf_quottest(sfto_sqfpartf lc f,car l) then ofsf_getnotconstf(xn,red f,l) else ofsf_getnotconstf(xn,red f, ofsf_and1(ofsf_0mk2('equal, ofsf_normcond lc f),car l) . ofsf_and1(ofsf_0mk2('neq, ofsf_normcond lc f), car l) . cdr l); procedure ofsf_quottest(f1,f2); % Tests, if an element of [f2] divides [f1]. [f1] is a SF, [f2] is a % conjunction of equalities. Returns T or NIL. if rl_op f2 eq 'equal then ofsf_quottest1(f1,{ofsf_arg2l f2}) else ofsf_quottest1(f1,for each elem in cdr f2 collect ofsf_arg2l elem); procedure ofsf_quottest1(f1,f2); % Tests, if an element of [f2] divides [f1]. [f1] is a SF, [f2] is a % list of SF's. Returns T or NIL. if null f2 then nil else if quotf(f1,car f2) then t else ofsf_quottest1(f1,cdr f2); procedure ofsf_inf(xn,f); % Formula, so that f is positive for x->oo. [xn] is an identifier, % [f] is SF. Result is a formula. begin scalar res, oldorder; oldorder := setkorder(xn . kord!*); res := ofsf_inf1(xn,reorder f); setkorder oldorder; return res end; procedure ofsf_inf1(xn,f); % Formula, so that f is positive for x->oo. [xn] is an identifier, % [f] is a SF. Result is a formula. if null f then 'false else if domainp f then if f > 0 then 'true else 'false else if mvar f neq xn then ofsf_0mk2('greaterp, f) else if domainp lc f then if (lc f) > 0 then 'true else 'false else ofsf_or(ofsf_0mk2('greaterp, lc f), ofsf_and(ofsf_0mk2('equal, lc f), ofsf_inf1(xn,red f))); procedure ofsf_minf(xn,f); % Formula, so that f is positive for x->-oo. [xn] is ans identifier, % [f] is a SF. Result is a formula. begin scalar res, oldorder; oldorder := setkorder(xn . kord!*); res := ofsf_minf1(xn,reorder f); setkorder oldorder; return res end; procedure ofsf_minf1(xn,f); % Formula, so that f is positive for x->-oo. [xn] is an identifier, % [f] is a SF. Result is a formula. if null f then 'false else if domainp f then if f > 0 then 'true else 'false else if mvar f neq xn then ofsf_0mk2('greaterp, f) else if domainp lc f then if multf(lc f,exptf(numr simp '(minus 1),ldeg f)) > 0 then 'true else 'false else ofsf_or(ofsf_0mk2('greaterp, multf(lc f,exptf(numr simp '(minus 1),ldeg f))), ofsf_and(ofsf_0mk2('equal, lc f),ofsf_minf1(xn,red f))); procedure ofsf_buildphi1(xn,glist); % Construction of $ phi1 $. [xn] is an identifier, [glist] is a list of % SF's. Result is a formula. begin scalar glist2,conj1,phi1; glist2 := glist; phi1 := 'true; while not null glist2 do << conj1 := ofsf_inf(xn,car glist2); if conj1 = 'false then << glist2 := nil; phi1 := 'false >> else << glist2 := cdr glist2; phi1 := ofsf_and(phi1,conj1) >> >>; return phi1 end; procedure ofsf_buildphi2(xn,glist); % Construction of $ phi2 $. [xn] is an identifier, [glist] is a list of % SF's. Result is a formula. begin scalar phi2,conj1,glist2; glist2 := glist; phi2 := 'true; while not null glist2 do << conj1 := ofsf_minf(xn,car glist2); if conj1 = 'false then << glist2 := nil; phi2 := 'false >> else << glist2 := cdr glist2; phi2 := ofsf_and(phi2,conj1) >> >>; return phi2 end; procedure ofsf_buildhkneq0(xn,neqlist); % Construction of conjunction, that each $ h_{k} $ isn't the zero-function. % [xn] is an identifier, [neqlist] is a list of SF's. Result is a % formula. begin scalar res,n2,conj1; n2 := neqlist; while not null n2 do << if !*rlhqegen then conj1 := ofsf_getneq0fgen(xn,car n2) else conj1 := ofsf_getneq0f(xn,car n2); if conj1 = 'true then n2 := cdr n2 else if conj1 = 'false then << res := 'false; n2 := nil >> else << res := rl_smkn('or,conj1) . res; n2 := cdr n2 >> >>; if res member {'true,'false} then return res else return ofsf_rqsimpl rl_smkn('and,res) end; procedure ofsf_and(f1,f2); % Conjunction. [f1] and [f2] are formulas. Returns the conjunction % $ f1 and f2 $. begin scalar phi; if !*rlhqevb then ioto_tprin2 {"simplifying a conjunction ... "}; phi := cl_simpl(rl_smkn('and,{f1,f2}),nil,-1); if !*rlhqevb then ioto_prin2 "done"; return phi end; procedure ofsf_or(f1,f2); % Conjunction. [f1] and [f2] are formulas. Returns the disjunction % $ f1 and f2 $. begin scalar !*rlsiexpla,!*rlsipw,phi; if !*rlhqevb then ioto_tprin2 {"simplifying a disjunction ... "}; phi := cl_simpl(rl_smkn('or,{f1,f2}),nil,-1); if !*rlhqevb then ioto_prin2 "done"; return phi end; procedure ofsf_and1(f1,f2); % Conjunction. [f1] and [f2] are formulas. Returns the disjunction % $ f1 and f2 $ without changing atomic formula relations. begin scalar !*rlsiexpla,!*rlsipw,phi; if !*rlhqevb then ioto_tprin2 {"simplifying a disjunction ... "}; phi := cl_simpl(rl_smkn('and,{f1,f2}),nil,-1); if !*rlhqevb then ioto_prin2 "done."; return phi end; procedure ofsf_mknewf2(varl,f); % Construction of new formula. [varl] is a list of identifiers, [f] is % a quantifier-free formula. Returns a formula, $ ex(x1,...,ex(xn,f))$. % [varl] has the form $ (xn ... x1) $. if null varl then f else ofsf_mknewf2(cdr varl,rl_mkq('ex, car varl, f)); procedure ofsf_qenfcase0(condl,xn,gl,f); % Quantifier Elimination in the case of r=0. [condl] is a conj. of % conditions, [xn] is an identifier, [gl] is a list of SF's, [f] is a SF. % Returns a formula. begin scalar oldorder,psi,sf_condl,sf_f; % if !*rlverbose then % ioto_tprin2 {"++++ Eliminating case #f = 0 with #g:",length gl}; oldorder := setkorder(xn . kord!*); sf_f := reorder f; if condl = 'true then sf_condl := nil else if rl_op condl neq 'and then sf_condl := {condl} else sf_condl := cdr condl; sf_f := ofsf_deletemon(xn,sf_f,sf_condl,sf_condl); setkorder oldorder; sf_f := reorder sf_f; psi := ofsf_d0main({sf_f},{xn},gl,nil); % if !*rlverbose then % ioto_tprin2 {"+++++ Case #f = 0 eliminated."}; return psi end; procedure ofsf_deletemon(xn,f,l1,l2); % Delete leading monomials, which are Zero in [l]. [xn] is an identifier, % [f] is a SF, [l1] and [l2] are lists of atomic formulas. Returns a SF. % [f] has at least degree 1 wrt. [xn]. if null l2 or domainp f then f else if rl_op car l2 eq 'equal then if mvar f neq xn then if quotf(f,ofsf_arg2l car l2) then nil else ofsf_deletemon(xn,f,l1,cdr l2) else if quotf(lc f,ofsf_arg2l car l2) then ofsf_deletemon(xn,red f,l1,l1) else ofsf_deletemon(xn,f,l1,cdr l2) else ofsf_deletemon(xn,f,l1,cdr l2); procedure ofsf_ggsys(l,varl,xi); % Green Groebner system computation. [l] is a list of SF's, [varl] is a % list of identifiers, [xi] is a conjunction of atomic formulas. Returns a % list of the form: $ (.. (cond gb) ...)$, where $cond$ is a list of % conditions and $gb$ a groebner basis with SF's. [xi] should be the % initial condition. begin scalar !*cgbreal,cdl,gsys;%!*cgbgs; !*cgbreal := t; % !*cgbgs := t; if !*rlhqetheory then cdl := ofsf_mkcondlist xi; if !*rlhqegen then << !*cgbgen := T; gsys := cgb_ggsysf(l,cdl,ofsf_hqexvars!*,varl,'revgradlex,nil); !*cgbgen := nil; ofsf_hqetheo!* := append(ofsf_buildtheory(gsys,cdl),ofsf_hqetheo!*); gsys := ofsf_buildgenggsys gsys >> else gsys := cgb_ggsysf(l,cdl,nil,varl,'revgradlex,nil); if !*rlhqegbred then return ofsf_gbred(gsys,varl) else return gsys end; procedure ofsf_gbred(gsys,varl); % Computation of a reduced Groebner system. [gsys] is a Groebner system, % [varl] is a list of identifiers. Returns a Groebner system. for each elem in gsys collect {car elem, ofsf_gbred1(cadr elem,varl)}; procedure ofsf_gbred1(gb,varl); % Computation of a reduced Groebner basis. [gb] is a list of SF's. % [varl] is a list of identifiers. Returns a list of SF's. begin scalar old,gb1; old := vdp_init(varl,'revgradlex,nil); gb1 := for each elem in gb collect vdp_f2vdp elem; gb1 := gb_traverso!-final gb1; gb1 := for each elem in gb1 collect vdp_2f elem; vdp_cleanup old; return gb1 end; procedure ofsf_mkconj(condlist); % Make conjunction. [condlist] is a list of conditions. Returns a formula. if null condlist or condlist eq 'true then 'true else if null cdr condlist then car condlist else rl_smkn('and,condlist); procedure ofsf_casedimn(ita,xi,varl,glist,hlist); % Construction of the formula in the case, that ideal has dimension n. % [ita], [xi] are conjunctions of atomic formulas, [varl] is a list of % identifiers, [glist] and [hlist] are lists of SF's. Returns a formula. if !*rlhqedim0 then ofsf_mknewf2(varl,ofsf_sfl2f(nil,glist,hlist)) else ofsf_qenf(ofsf_and1(ita,xi),nil,glist,hlist,varl); procedure ofsf_sfl2f(fl,gl,hl); % Build conjunction of $>$-relations and inequalities. [fl], [gl] and [hl] % are lists of SF's. Returns a formula. begin scalar fl1,gl1,hl1; fl1 := for each elem in fl collect ofsf_0mk2('equal,elem); gl1 := for each elem in gl collect ofsf_0mk2('greaterp,elem); hl1 := for each elem in hl collect ofsf_0mk2('neq,elem); return rl_smkn('and,append(fl1,append(gl1,hl1))) end; procedure ofsf_remvarl(varl,ivarl); % Gets remainder variables of maximal set of independent variables. % [varl] and [ivarl] are lists of identifiers. Returns a list of % identifiers. setdiff(varl,ivarl); procedure ofsf_casedim(ita,xi,bvarl,ivarl,gb,glist,hlist); % Construction of the formula in the case, that ideal has dimension 1,..n-1. % [ita], [xi] are conjunctions of atomic formulas, [bvarl] and [ivarl] are % lists of identifiers, [gb], [glist] and [hlist] are lists of SF's. Returns % a formula. begin scalar newpsi,newgb,newglist,newhlist,theo; if !*rlhqedim0 then return ofsf_mknewf2(append(bvarl,ivarl),ofsf_sfl2f(gb,glist,hlist)); newgb := ofsf_sort(gb,bvarl); newglist := ofsf_sort(glist,bvarl); newhlist := ofsf_sort(hlist,bvarl); theo := ofsf_mktheo(car newgb,car newglist,car newhlist); newpsi := ofsf_rqsimpl(rl_smkn('and,{theo,ofsf_qenf(ofsf_and1(theo, ofsf_and1(ita,xi)),cadr newgb,cadr newglist,cadr newhlist,bvarl)})); return ofsf_hqe0 ofsf_mknewf2(ivarl,newpsi) end; procedure ofsf_rqsimpl(phi); % Formula Simplifier. [phi] is a formula. Returns a formula. begin scalar phi1; if !*rlhqevb then ioto_tprin2 {"simplifying formula with ",cl_atnum phi, " atomic formulas ... "}; phi1 := cl_simpl(phi,nil,-1); if !*rlhqevb then ioto_prin2 {"done (", cl_atnum phi1, ")"}; return phi1 end; procedure ofsf_sort(l,varl); % Sorts list depending, if elements have variables of [varl]. [l] is a list % of SF's and [varl] is a list of identifiers. Returns a list of the form % $ (il dl) $, where $il$ are all elements of [l], which haven't variables % of [varl], $dl$ are the remaining elements. begin scalar l1,il,dl; l1 := l; while not null l1 do << if intersection(kernels car l1,varl) then dl := car l1 . dl else il := car l1 . il; l1 := cdr l1 >>; return {il,dl} end; procedure ofsf_mktheo(fl,gl,hl); % Make conjunction. [fl], [gl] and [hl] are lists of SF's. Returns a % formula. begin scalar res; res := for each elem in fl collect ofsf_0mk2('equal,elem); res := append(for each elem in gl collect ofsf_0mk2('greaterp,elem),res); res := append(for each elem in hl collect ofsf_0mk2('neq,elem),res); return rl_smkn('and,res) end; procedure ofsf_mkcondlist(conj); % Build condition list for call of cgb_ggsys. [c] is a conjunction of % atomic formulas. Returns a list of atomic formulas. All $<$- and % $>$-relations become inequations. begin scalar l,cdl,cd; if conj eq 'true then return nil; l := if rl_op conj neq 'and then {conj} else cdr conj; while not null l do << cd := ofsf_getcdform car l; if not null cd then cdl := cd . cdl; l := cdr l >>; return cdl end; procedure ofsf_getcdform(af); % Subroutine of ofsf_mkcdlist. [af] is an atomic formula. Returns an % atomic formula. if rl_op af member {'equal,'neq} then af else if rl_op af member {'greaterp,'lessp} then ofsf_0mk2('neq, ofsf_arg2l af); procedure ofsf_buildtheory(gsys,icd); % Construction of a Theory. [gsys] Is a Groebner System, [cd] is a % initial condition. Returns a Theory, a list of inequations. begin scalar cdl,res; cdl := for each elem in gsys join car elem; cdl := setminus(cdl,rl_thsimpl icd); for each elem in cdl do << if rl_op elem eq 'neq and not intersection(kernels ofsf_arg2l elem,ofsf_hqexvars!*) then res := elem . res >>; return rl_thsimpl res end; procedure ofsf_buildgenggsys(gsys); % Removes Conditions from branches, which are in a theory. [gsys] is a % Groebner System. Returns a Groebner System. for each branch in gsys collect {setminus(car branch,ofsf_hqetheo!*),cadr branch}; % ----------------------------------------------------------------------------- % Case of zero-dimensional ideal % ----------------------------------------------------------------------------- % Computes a formula, so that the ideal has a zero and the conditions hold. % % Input: A Groebner Basis $ gb $ of the ideal, a list $ varl $ of main % variables, a list $ greaterlist $ of polynomials, which should have positive % values, and a list $ neqlist $ of polynomials, which shouldn't bee zero. % % Output: A quantifier-free formula procedure ofsf_d0main(gb,varl,greaterlist,neqlist); % [gb],[greaterlist] and [neqlist] are lists of SF's, [varl] is a list of % identifiers. Returns a list of SQ's, the coefficients of the % characteristic polynomial in the order $ c_{0},...,c_{n} $. begin scalar beta,chi,helist,y,coeffl,qf,vdp_gb,vsbasis,old,oldorder; integer i; if !*rlverbose then ioto_tprin2 {"+ begin d0: r:",length gb," n:", length varl," s:",length greaterlist," t:",length neqlist}; helist := ofsf_buildhelist(greaterlist,neqlist); old := vdp_init(varl,'revgradlex,nil); vdp_gb := ofsf_redgroebner for each elem in gb collect vdp_f2vdp elem; if !*rlhqevb then ioto_tprin2 "+ computing residue class ring vector space basis ... "; vsbasis := ofsf_gvsbasis(ofsf_gb2gltb vdp_gb,varl); if !*rlhqevb then ioto_prin2 {"done. Dimension: ",length vsbasis}; if !*rlhqestrconst then << vsbasis := for each elem in vsbasis collect vdp_f2vdp elem; beta := gbsc_strconst(vsbasis,vdp_gb,4) >>; y := intern gensym(); oldorder := setkorder(y . kord!*); chi := if not !*rlhqetfcsplit then simp 1; if !*rlverbose then ioto_tprin2 {"computing characteristic ", ioto_cplu("polynomial",length helist neq 1),":"}; for each elem in helist do << if !*rlverbose then << i := i+1; ioto_prin2 {" ",length helist-i+1}; >>; if !*rlhqetfcsplit then chi := ofsf_d0main1(vdp_gb,vsbasis,beta,elem,y) . chi else chi := multsq(chi,ofsf_d0main1(vdp_gb,vsbasis,beta,elem,y)) >>; if !*rlverbose then ioto_prin2 " done."; if not !*rlhqetfcsplit then << coeffl := reversip ofsf_coefflist(chi,y); if !*rlhqevb then ioto_prin2 "Done."; if !*rlverbose then ioto_tprin2 {"computing type formula of length ", length coeffl," ... "}; qf := ofsf_tfc coeffl >> else << if !*rlverbose then << ioto_prin2 "constructing disjunction of type formulas ... "; >>; qf := ofsf_tfcmain(chi,y); >>; setkorder oldorder; if !*rlverbose then % ioto_tprin2 {"+++++ Type Formula Computation finished: ",cl_atnum qf}; ioto_prin2t {"done (",cl_atnum qf,")"}; qf := cl_simpl(rl_mk1('not,qf),nil,-1); if !*rlverbose then ioto_tprin2 {"+ end of d0 (",cl_atnum qf,")"}; vdp_cleanup old; return qf end; procedure ofsf_d0main1(vdpgb,vsbasis,beta,he,charX); % Main procedure for zero-dimensional case. % [vdpgb] is a list of VDP's, [vsbasis] is a list of SF's or VDP's, [beta] % is a BETA, [he] is a SF, [charX] is an identifier. Returns a SF, the % characteristic polynomial wrt. arguments. ofsf_charpoly('mat . ofsf_buildq(vdpgb,he,vsbasis,beta),charX); procedure ofsf_gb2gltb(vdpgb); % Head terms from Groebner basis. [vdpgb] is a list of VDP's, Returns a % list of SF's. begin scalar basis2; basis2 := for each elem in vdpgb collect vdp_fmon(bc_a2bc 1, vdp_evlmon elem); basis2 := for each elem in basis2 collect vdp_2f elem; return basis2 end; procedure ofsf_gvsbasis(ltb,varl); % Groebner vector space basis. [ltb] is a list of SF's, [varl] is a list of % identifiers. Returns a list of SF's. Computes a vector space basis of % $ K[X]/I $: the reduced terms basis. begin scalar htl,basis,basis2,v,d,tt; htl := ofsf_mvp(ltb, varl); if length htl neq length varl then rederr "ideal not zero dimensional"; basis := {numr simp 1}; for each term in htl do << v := car term; d := cdr term; basis2 := basis; for each elem in basis do for i:=1:(d-1) do << tt := multf(elem,exptf(numr simp v,i)); if not ofsf_redp(tt,ltb) then basis := tt . basis >> >>; return basis end; procedure ofsf_mvp(ltb,varl); % Minimum variable powers. [ltb] is a list of SF's, [varl] is a list of % identifiers. Returns an Alist $ (...(v . d)...)$ such % that $v^d$ is in [ltb] and vice versa. begin scalar htlist,var,v,d,w; for each term in ltb do << var := kernels term; if (length var = 1) and member(car var,varl) then << v := car var; d := ldeg term; w := assoc(v,htlist); if w then cdr w := min(cdr w, d) else htlist := (v . d) . htlist >> >>; return htlist end; procedure ofsf_redp(tt,ltb); % Reduction predicate. [tt] is a SF, [ltb] is a list of SF's. Returns t % iff [tt] is reducible w.r.t. [ltb] else NIL. begin scalar c; c := t; while c and ltb do << if null cdr qremf(tt,car ltb) then c := nil else ltb := cdr ltb >>; return not c end; procedure ofsf_trace(vdpgb,he,vi,vj,vsbasis); % Trace of $ m_{he,vi,vj} $. [vdpgb] is a list of VDP's, [he], [vi], [vj] % are SF's, [vsbasis] is a list of SF's. Returns a SQ. begin scalar res; res := simp 0; for each elem in vsbasis do res := addsq(res,ofsf_trace1(vdpgb,he,vi,vj,elem)); return res end; procedure ofsf_trace1(vdpgb,he,vi,vj,elem); % Trace computation subroutine without use of structure constants. [he], % [vi], [vj], [elem] are SF's, [vdpgb] is a list of VDP's. Returns a SQ. ofsf_getcoeff(ofsf_prod(he,vi,vj,elem,vdpgb),vdp_f2vdp elem); procedure ofsf_prod(he,vi,vj,elem,vdpgb); % Reduction step of ofsf_trace2. [he], [vi], [vj], [elem] are SF's, [vdpgb] % is a list of VDP's. Returns a VDP. gb_reduce(vdp_f2vdp multf(he,multf(vi,multf(vj,elem))),vdpgb); procedure ofsf_getcoeff(f,vi); % Coefficient of [v_i] in [f]. [f], [vi] are VDP's. Returns a SQ. if vdp_zero!? f then simp 0 else if vdp_evlmon f = vdp_evlmon vi then vdp_lbc f else ofsf_getcoeff(vdp_mred f,vi); procedure ofsf_charpoly(q,x); % Characteristic polynomial. [q] is a matrix, a list of lists of Lisp Prefix % form with 'mat-Tag, [x] is an identifier. Returns a SQ. simp aeval {'char_poly,q,x}; procedure ofsf_coefflist(p,x); % Extract coefficients of polynomial. [p] is a SQ, [x] is an identifier. % Returns a list of SQ's. % Result has form: $ (c_0 c_1 ... c_d) $. begin scalar res,q1,q2,d; q1 := reorder numr p; q2 := denr p; d := ldeg q1; res := ofsf_coefflist1(q1,x,d); res := for each elem in res collect quotsq(simp prepf elem,simp prepf q2); return res end; procedure ofsf_coefflist1(p,x,d); % Subroutine of ofsf_coefflist. [p] is a SF, [x] is an identifier, [d] is % an integer. Returns a list of SQ's. if (domainp p or mvar p neq x) and d=0 then {p} else if not domainp p and ldeg p = d then (lc p) . ofsf_coefflist1(red p,x,d-1) else nil . ofsf_coefflist1(p,x,d-1); procedure ofsf_buildq(vdpgb,he,vsbasis,beta); % Computation of matrix Q. [vsbasis] is a list of SF's or VDP's, [vdpgb] % is a list of VDP's, [he] is a SF, [beta] is a BETA. % Returns a list of lists of Lisp Prefix forms. if !*rlhqestrconst then ofsf_buildqsc(vdpgb,he,vsbasis,beta) else ofsf_buildq1(vdpgb,he,vsbasis); procedure ofsf_buildq1(vdpgb,he,vsbasis); % Computation of matrix Q without using structure constants. % [vsbasis] is a list of SF's, [vdpgb] is a list of VDP's, [he] is a SF. % Returns a list of lists of Lisp Prefix forms. begin scalar redhe,q,dim;integer i; if !*rlhqevb then ioto_tprin2 {"computing matrix Q of dimension ",length vsbasis}; redhe := he; q := for each vlist on vsbasis collect for each vj in vlist collect prepsq ofsf_trace(vdpgb,redhe,car vlist,vj,vsbasis); q := for each line in q collect << i := i+1; nconc(for j := 1:i-1 collect nil,line) >>; dim := length vsbasis; for y := 2:dim do for x := 1:y-1 do nth(nth(q,y),x) := nth(nth(q,x),y); if !*rlhqevb then ioto_tprin2 " done"; return q end; procedure ofsf_buildhelist(greaterlist,neqlist); % Computation of all necessary products of polynomials in nequations and % >-relations. [greaterlist] and [neqlist] are lists of SF's. Returns a % list of SF's. begin scalar helist,chi1,glist; if null greaterlist and null neqlist then return {1}; chi1 := 1; for each elem in neqlist do chi1 := multf(chi1,exptf(elem,2)); glist := ofsf_buildglist greaterlist; helist := for each elem in glist collect multf(elem,chi1); return helist end; procedure ofsf_buildglist(greaterlist); % Computation of all necessary products of polynomials in >-relations. % [greaterlist] is a list of SF's. Returns a list of SF's. begin scalar recres; if null greaterlist then return {1} else if length greaterlist = 1 then return {exptf(car greaterlist,2),car greaterlist}; recres := ofsf_buildglist cdr greaterlist; return append(ofsf_buildglist1(exptf(car greaterlist,2),recres), ofsf_buildglist1(car greaterlist,recres)) end; procedure ofsf_buildglist1(pol,pollist); % Subroutine of ofsf_buildglist. [pol] is a SF, [pollist] is a list of SF's. % Returns a list of SF's. for each poly in pollist collect multf(pol,poly); % Following procedures are used for building matrix Q with use of structure % constants: procedure ofsf_redgroebner(vdpgb); % Reduction of a Groebner Basis. [vdpgb] is a list of VDP's. Returns a list % of VDP's. Throws all elements of [vdpgb] out, if their head term is % divided by another one. begin scalar h,f,f0,evf0; f := vdpgb; while not null f do << f0 := car f; evf0 := vdp_evlmon f0; f := cdr f; if (not gb_searchinlist(evf0,f)) and (not gb_searchinlist(evf0,h)) then h := f0 . h >>; return h end; procedure ofsf_buildqsc(vdpgb,he,vsbasis,beta); % Computation of matrix Q using structure constants. % [vsbasis] is a list of SF's, [vdpgb] is a list of VDP's, % [he] is a SF, [beta] is a BETA. Returns a list of lists of Lisp % Prefix forms. begin scalar redhe,q,dim;integer i; if !*rlhqevb then ioto_tprin2 {"computing matrix Q of dimension ",length vsbasis}; redhe := gb_reduce(vdp_f2vdp he,vdpgb); q := for each vlist on vsbasis collect for each vj in vlist collect mk!*sq ofsf_tracesc(redhe,car vlist,vj,vsbasis,beta); q := for each line in q collect << i := i+1; nconc(for j := 1:i-1 collect nil,line) >>; dim := length vsbasis; for y := 2:dim do for x := 1:y-1 do nth(nth(q,y),x) := nth(nth(q,x),y); if !*rlhqevb then ioto_tprin2 " done"; return q end; procedure ofsf_tracesc(redhe,vi,vj,vdpvsbasis,beta); % Trace Computation. [vdpvsbasis] is a list of VDP's, [redhe], % [vi] and [vj] are VDP's, [beta] is a BETA. Returns a SQ. begin scalar res; res := simp 0; for each bk in vdpvsbasis do res := addsq(res,ofsf_tracesc1(redhe,vi,vj,bk,vdpvsbasis,beta)); return res end; procedure ofsf_tracesc1(redhe,vi,vj,bk,vdpvsbasis,beta); % Trace Computation subroutine. [vdpvsbasis] is a list of VDP's, % [redhe],[vi], [vj] and [bk] are VDP's, [beta] is a BETA. Returns a SQ. begin scalar traceelem,vivjbk; traceelem := simp 0; vivjbk := vdp_prod(vi,vdp_prod(vj,bk)); for each bl in vdpvsbasis do traceelem := addsq(traceelem,ofsf_tracesc2(redhe,bk,bl,vivjbk,beta)); return traceelem end; procedure ofsf_tracesc2(redhe,bk,bl,vivjbk,beta); % Trace Computation subroutine.[redhe],[bk], [bk] and [vivjbk]are VDP's, % [beta] is a BETA. Returns a SQ. multsq(gbsc_getlincombc(bl,redhe), gbsc_betaget(beta,vdp_prod(bl,vivjbk),bk)); % ----------------------------------------------------------------------------- % Computation of the dimension and a maximally independent set of variables % of the ideal. % ----------------------------------------------------------------------------- % Input: A lust of SF's, representing a Groebner Basis wrt. the $ revgradlex $ % term order, and a list of main variables. % Output: Dimension $ d $ and a set of maximally independent variables. procedure ofsf_dim(gb,varl); % Dimension and maximal set of independent variables of an ideal. % [gb] is a list of SF's, [varl] is a list of identifiers. Returns % a list of the form $ (d U) $, where $ d $ is the dimension of the % ideal and $ U $ is a set of maximally independent variables. if null gb then {length varl,varl} else if ofsf_proper(gb,varl) then ofsf_dimmain(gb,varl) else {-1,nil}; procedure ofsf_proper(gb,varl); % Tests, if the ideal constructed by [gb] is proper, e.g. not the % whole ring. [gb] is a list of SF's, [varl] is a list of identifiers. % Returns T or NIL. if null gb then t else if intersection(kernels car gb,varl) then ofsf_proper(cdr gb,varl) else nil; procedure ofsf_dimmain(gb,varl); % Dimension and maximal set of independent variables of an ideal. % [gb] is a list of SF's, [varl] is a list of identifiers. % Returns a list of the form $ (d U) $, where $ d $ is the dimension % of the ideal and $ U $ is a set of maximally independent variables. begin scalar htl, m; htl := ofsf_htl(gb,varl); m := ofsf_dimrec(htl,varl,1,nil,nil); if !*rlhqegbdimmin then return ofsf_getmin m else return ofsf_getmax m end; procedure ofsf_htl(gb,varl); % Head Terms of a Groebner Basis. [gb] is a list of SF's, [varl] is a % list of identifiers. Returns a list of SF's. begin scalar old, vdpgb, res; old := vdp_init(varl,'revgradlex,nil); vdpgb := for each elem in gb collect vdp_f2vdp elem; res := for each elem in vdpgb collect vdp_fmon(bc_a2bc 1, vdp_evlmon elem); res := for each elem in res collect vdp_2f elem; vdp_cleanup old; return res end; procedure ofsf_dimrec(s,varl,k,u,m); % Subroutine of Algorithm DIMENSION. [s] is a list of SF's, [varl] is % a list of identifiers, [k] is a % positive integer, [u] is a list of identifiers, [m] is a list of % lists of identifiers. Returns a list of lists of identifiers. begin scalar m2; m2 := m; for i:=k:length varl do if not ofsf_intersectionp( list2set(ofsf_getxi(varl,i) . u),s) then << m2 := ofsf_dimrec(s,varl,i+1, list2set(ofsf_getxi(varl,i) . u),m2)>>; if not ofsf_subsetp(u,m2) then m2 := u . m2; return m2 end; procedure ofsf_getxi(varl,i); % Get i-th variable X_{i}. [varl] is a list of identifiers, [i] is a % positive integer. Returns an identifier. nth(varl,i); procedure ofsf_getmax(m); % Get maximal length of an element from a list of lists. [m] is a list % of lists of identifiers. Returns a list of the form $ (d u) $, where % $ d $ is an integer, the dimension of the ideal, and $ u $ is a % maximally independent set of variables of maximal cardinality. begin scalar u; integer d,lengthU; while not null m do << lengthU := length car m; if lengthU > d then << d := lengthU; u := car m >>; m := cdr m >>; return {d, u} end; procedure ofsf_getmin(m); % Get minimal length of an element from a list of lists. [m] is a list % of lists of identifiers. Returns a list of the form $ (d u) $, where % $ d $ is an integer, the dimension of the ideal, and $ u $ is a % maximally independent set of variables of minimal cardinality. begin scalar u; integer d,du,lengthU; if not null m then << d := length car m; du := d; u := car m; m := cdr m >>; while not null m do << lengthU := length car m; if lengthU > d then d := lengthU else if lengthU < du then << du := lengthU; u := car m >>; m := cdr m >>; return {d, u} end; procedure ofsf_intersectionp(vl,s); % Test, if intersection of terms wrt. variables in [vl] and s isn't % empty. [vl] is a list of identifiers, [s] is a list of SF's. Returns % T or NIL. begin scalar news,found; news := s; while not null news do << if subsetp(kernels car news,vl) then << news := nil; found := t >> else news := cdr news >>; return found end; procedure ofsf_subsetp(u,m2); % Tests, if [u] is contained in any element of [m2]. [u] is a list % of identifiers, [m2] is a list of lists of identifiers. Returns T % or NIL. begin scalar newm2,found; newm2 := m2; while not null newm2 do << if subsetp(u,car newm2) then << newm2 := nil; found := t >> else newm2 := cdr newm2 >>; return found end; endmodule; % [ofsfhqe] end; % of file