Artifact 1461c249e958e10bbf9c61cfd9aacd09274b881fc1bb89dadc4734324dcbc35b:
- Executable file
r37/packages/redlog/acfsfgs.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: 23323) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: acfsfgs.red,v 1.6 1999/04/13 13:05:33 sturm Exp $ % ---------------------------------------------------------------------- % Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm % ---------------------------------------------------------------------- % $Log: acfsfgs.red,v $ % Revision 1.6 1999/04/13 13:05:33 sturm % Minor corrections in comments. % % Revision 1.5 1999/04/12 09:25:58 sturm % Updated comments for exported procedures. % % Revision 1.4 1999/03/23 08:14:18 dolzmann % Changed copyright information. % Added fluids for the rcsid of the file and for the copyright information. % % Revision 1.3 1997/10/02 13:49:49 dolzmann % In procedure acfsf_qe1: Remove atomic formulas containing bound variables % from the theory. % % Revision 1.2 1997/08/24 16:17:41 sturm % Call cl_sitheo instead of acfsf_gssimpltheo. % Added service rl_surep with black box rl_multsurep. % Added service rl_siaddatl. % % Revision 1.1 1997/08/22 17:30:39 sturm % Created an acfsf context based on ofsf. % % ---------------------------------------------------------------------- lisp << fluid '(acfsf_gs_rcsid!* acfsf_gs_copyright!*); acfsf_gs_rcsid!* := "$Id: acfsfgs.red,v 1.6 1999/04/13 13:05:33 sturm Exp $"; acfsf_gs_copyright!* := "Copyright (c) 1995-1999 A. Dolzmann and T. Sturm" >>; module acfsfgs; % Algebraically closed field standard form Groebner simplifier. % Submodule of [acfsf]. %DS % <CIMPL> ::= (<GP>, <PROD1>, <PROD2>, <OTHER>) % <GP> ::= ((<GB> . <PROD>) . <OTHER>) % <GB> ::= (<SF>,...) % <PROD> ::= <SF> % <PROD1> ::= <SF> % <PROD2> ::= <SF> % <OTHER> ::= (<ATOMIC_FORMULA>,...) procedure acfsf_gsc(f,atl); % Algebraically closed field Groebner simplification via % conjunctive normal form. [f] is a formula; [atl] is a theory. % Returns [inconsistent] or a formula equivalent to [f]. The % returned formula is somehow simpler than [f]. This procedure % temporarily turns off the switches [groebopt] and [rlsiexpla]. % Temporarily changes the [torder] to [{{},revgradlex}] unless % [rlgsutord] is on. Accesses the switches [rlverbose], [rlgsvb], % [rlgsbnf], [rlgsrad], [rlgssub], [rlgsred], [rlgsprod], % [rlgserf], [rlgsutord], and the fluid [rlradmemv!*]. begin scalar w,svrlgsvb; svrlgsvb := !*rlgsvb; if !*rlverbose and !*rlgsvb then on1 'rlgsvb else off1 'rlgsvb; w := acfsf_gsc1(f,atl); onoff('rlgsvb,svrlgsvb); return w end; procedure acfsf_gsc1(f,atl); % Algebraically closed field Groebner simplification via % conjunctive normal form subroutine. [f] is a formula; [atl] is a % theory. Returns [inconsistent] or a formula equivalent to [f]. % The returned formula is somehow simpler than [f]. This procedure % temporarily turns off the switches [groebopt] and [rlsiexpla]. % Temporarily changes the [torder] to [{{},revgradlex}] unless % [rlgsutord] is on. Accesses the switches [rlgsvb], [rlgsbnf], % [rlgsrad], [rlgssub], [rlgsred], [rlgsprod], [rlgserf], % [rlgsutord], and the fluid [rlradmemv!*]. begin scalar phi,!*rlsiexpla; % Hack, but otherwise phi is not a bnf! if !*rlgsbnf then << if !*rlgsvb then ioto_prin2 "[CNF"; phi := cl_simpl(cl_cnf cl_nnf f,atl,-1); if !*rlgsvb then ioto_prin2 "] " >> else phi := cl_simpl(f,atl,-1); if phi eq 'inctheo then return 'inctheo; if rl_tvalp phi then return phi; phi := acfsf_gssimplify0(phi,atl); if phi eq 'inctheo then return 'inctheo; return cl_simpl(phi,atl,-1) end; procedure acfsf_gsd(f,atl); % Algebraically closed field Groebner simplification via % disjunctive normal form. [f] is a formula; [atl] is a theory. % Returns [inconsistent] or a formula equivalent to [f]. The % returned formula is somehow simpler than [f]. This procedure % temporarily turns off the switches [groebopt] and [rlsiexpla]. % Temporarily changes the [torder] to [{{},revgradlex}] unless % [rlgsutord] is on. Accesses the switches [rlverbose], [rlgsvb], % [rlgsbnf], [rlgsrad], [rlgssub], [rlgsred], [rlgsprod], % [rlgserf], [rlgsutord], and the fluid [rlradmemv!*]. begin scalar w,svrlgsvb; svrlgsvb := !*rlgsvb; if !*rlverbose and !*rlgsvb then on1 'rlgsvb else off1 'rlgsvb; w := acfsf_gsd1(f,atl); onoff('rlgsvb,svrlgsvb); return w end; procedure acfsf_gsd1(f,atl); % Algebraically closed field Groebner simplification via % disjunctive normal form subroutine. [f] is a formula; [atl] is a % theory. Returns [inconsistent] or a formula equivalent to [f]. % The returned formula is somehow simpler than [f]. This procedure % temporarily turns off the switches [groebopt] and [rlsiexpla]. % Temporarily changes the [torder] to [{{},revgradlex}] unless % [rlgsutord] is on. Accesses the switches [rlgsvb], [rlgsbnf], % [rlgsrad], [rlgssub], [rlgsred], [rlgsprod], [rlgserf], % [rlgsutord], and the fluid [rlradmemv!*]. begin scalar phi,!*rlsiexpla; % Hack, but otherwise phi is not a bnf! if !*rlgsbnf then << if !*rlgsvb then ioto_prin2 "[DNF"; phi := cl_simpl(cl_nnfnot cl_dnf f,atl,-1); if !*rlgsvb then ioto_prin2 "] "; >> else phi := cl_simpl(cl_nnfnot f,atl,-1); if phi eq 'inctheo then return 'inctheo; if rl_tvalp phi then return cl_nnfnot phi; phi := acfsf_gssimplify0(phi,atl); if phi eq 'inctheo then return 'inctheo; return cl_simpl(cl_nnfnot phi,atl,-1) end; procedure acfsf_gsn(f,atl); % Algebraically closed field Groebner simplification via normal % form. [f] is a formula; [atl] is a theory. Returns [inconsistent] % or a formula equivalent to [f]. The returned formula is somehow % simpler than [f]. The normal form used depends on the toplevel % operator of [f]. This procedure temporarily turns off the % switches [groebopt] and [rlsiexpla]. Temporarily changes the % [torder] to [{{},revgradlex}] unless [rlgsutord] is on. Accesses % the switches [rlverbose], [rlgsvb], [rlgsbnf], [rlgsrad], % [rlgssub], [rlgsred], [rlgsprod], [rlgserf], [rlgsutord], and the % fluid [rlradmemv!*]. if rl_tvalp f then f else if cl_atflp(rl_argn f) then if rl_op(f) eq 'and then acfsf_gsd(f,atl) else acfsf_gsc(f,atl) else if rl_op(f) eq 'and then acfsf_gsc(f,atl) else acfsf_gsd(f,atl); procedure acfsf_gssimplify0(f,atl); % Algebraically closed field Groebner simplify. [f] is a % conjunction of disjunctions of atomic formulas, a disjunction of % atomic formulas, or an atomic formula; [atl] is a theory. Returns % [inctheo] or a formula. This procedure temporarily turns off the % switch [groebopt]. Temporarily changes the [torder] to % [{{},revgradlex}] unless [rlgsutord] is on. Accesses the switches % [rlgsvb], [rlgsrad], [rlgssub], [rlgsred], [rlgsprod], [rlgserf], % [rlgsutord], and the fluid [rlradmemv!*]. begin scalar res,oldtorder,!*groebopt,svkord; svkord := kord!*; oldtorder := cdr torder('((list) revgradlex)); if !*rlgsutord then torder(oldtorder); res := acfsf_gssimplify(f,atl); torder oldtorder; kord!* := svkord; return res; end; procedure acfsf_gssimplify(f,atl); % Algebraically closed field Groebner simplify. [f] is a % conjunction of disjunctions of atomic formulas, a disjunction of % atomic formulas, or an atomic formula; [atl] is a theory. Returns % [inctheo] or a formula. Accesses the switches [rlgsvb], % [rlgsrad], [rlgssub], [rlgsred], [rlgsprod], [rlgserf], and the % fluid [rlradmemv!*]. begin scalar al,gp,ipart,npart,w,gprem,gprodal,gatl; atl := cl_sitheo atl; if atl eq 'inctheo or acfsf_gsinctheop(atl) then return 'inctheo; if (cl_atfp f) or (rl_op f eq 'or) then % degenerated cnf al := acfsf_gssplit!-cnf {f} else al := acfsf_gssplit!-cnf rl_argn f; if w := lto_catsoc('gprem,al) then << gp := acfsf_gsextract!-gp atl; gprem := acfsf_gsgprem(w,gp); if gprem eq 'false then return 'false; >>; gatl := append(atl,lto_catsoc('gprem,al)); gp := acfsf_gsextract!-gp(gatl); caar gp := sfto_groebnerf(caar gp); ipart := lto_catsoc('impl,al); npart := lto_catsoc('noneq,al); if ipart then ipart := acfsf_gspart(ipart,gp); if npart and gatl then npart := acfsf_gspart(npart,gp); if gprem then << if null !*rlgsprod then << gprodal := lto_catsoc('gprodal,al); gprem := acfsf_gssimulateprod(gprem,gprodal) >>; return rl_smkn('and,gprem . nconc(ipart,npart)) >>; return rl_smkn('and,nconc(ipart,npart)) end; procedure acfsf_gsinctheop(atl); % Algebraically closed field standard form Groebner simplifier % inconsistent theory predicate. [atl] is a list of atomic % formulas. [T] or [nil] is returned. begin scalar w; if null atl then return nil; if !*rlgsvb then ioto_prin2 "Inctheop... "; w := cl_nnfnot acfsf_gsimplication( cl_nnfnot rl_smkn('and,atl),'((nil . 1) . nil)); if !*rlgsvb then ioto_prin2t "done."; return w eq 'false end; procedure acfsf_gssplit!-cnf(f); % Algebraically closed field standard form Groebner simplifier % split conjunctive normal form. [f] is an list of disjunctions of % atomic formulas. An assoc list is returned. The returned assoc % list have the following items. [('impl . imp)] where [imp] is the % list off all disjunctions containing at least one inequation, % [('gprem . gprem)] where [gprem] is the list of all atomic % formulas occuring in [f] and atomic formulas equivalent to % disjunctions of inequalities occuring in [f], [('noneq . noneq)] % where [noneq] is a list of disjunctions of atomic formulas % containing no inequations, and [('gprodal . gprodal)]. The value % [gprodal] is a assoc list containing to each equation the product % representation, if the equation was extracted from a disjunction. begin scalar noneq,imp,prod,gprodal,gprem,w,x; for each phi in f do if rl_op phi memq '(and or) then % [phi] is not an atomic formula if (w := acfsf_gsdis!-type rl_argn phi) eq 'impl then imp := phi . imp else if w eq 'noneq then noneq := phi . noneq else << % [if w eq 'equal then] prod := 1; for each atf in rl_argn phi do prod := multf(prod,acfsf_arg2l atf); x := acfsf_0mk2('equal,prod); gprem := x . gprem; gprodal := (x . phi) . gprodal >> else gprem := phi . gprem; if !*rlgsvb then << ioto_tprin2t {"global: ",length gprem,"; impl: ",length imp, "; no neq: ",length noneq, "; glob-prod-al: ",length gprodal,"."} >>; return { 'impl . imp, 'noneq . noneq, 'gprem . gprem, 'gprodal . gprodal} end; procedure acfsf_gsdis!-type(atl); % Algebraically closed field standard form Groebner simplifier % disjunction type. [atl] is a non null list of atomic formulas. % ['equal], ['impl], or ['noneq] is returned. ['equal] is returned % if and only if all atomic formulas have the relation [equal]; % [impl] is returned, if and only if one of the atomic formula is % an equality, otherwise [noneq] is returned. begin scalar op,w; if null atl then return 'equal; op := acfsf_op car atl; if op eq 'neq then return 'impl; w := acfsf_gsdis!-type cdr atl; if w eq 'impl then return 'impl; if op eq 'equal and w eq 'equal then return 'equal; return 'noneq end; procedure acfsf_gsextract!-gp(atl); % Algebraically closed field standard form extract global premise. % [atl] is a list of atomic formulas. A GP is returned. begin scalar w; w := acfsf_gsdis2impl(for each at in atl collect acfsf_negateat(at)); return ( (car w . multf(cadr w, caddr w)) . cadddr w) end; procedure acfsf_gsgprem(atl,gp); % Algebraically closed field standard form Groebner simplifier % simplify global premise. [atl] is a list of atomic formulas; [gp] % is a GP. A formula is returned. begin scalar w; if !*rlgsvb then ioto_prin2 "[GP"; w := cl_nnfnot acfsf_gsimplication(cl_nnfnot rl_smkn('and,atl),gp); if !*rlgsvb then ioto_prin2 "] "; return w end; procedure acfsf_gspart(part,gp); % Algebraically closed field standard form Groebner simplify % simplify part. [part] is a list of disjunctions of atomic % formulas and atomic formulas. [gp] is a GP. A list [l] of % disjunctions of atomic formulas and atomic formulas is returned. % The formula on position $i$ in [l] is somehow simpler than the % formula on the position $i$ in part. Supposed that the formula % $\bigwedge(g_i=0)$ is true where $g_i$ are the terms in [gp] then % the positional corresponding fomulas in the two lists [part] and % [l] are equivalent. begin scalar w,curlen,res; if !*rlgsvb then curlen := length part; res := for each phi in part collect << if !*rlgsvb then ioto_prin2 {"[",curlen}; w := acfsf_gsimplication(phi,gp); if !*rlgsvb then << curlen := curlen - 1; ioto_prin2 {"] "} >>; w >>; if !*rlgsvb then ioto_cterpri(); return res end; procedure acfsf_gsimplication(f,gp); % Algebraically closed field standard form Groebner simplification % implication. [f] is a disjunction of atomic formulas or an atomic % formula. [gp] is a GP. Returns a formula. It is a truth value, an % atomic formula or a disjunction of atomic formulas, unless the % simplification of an atomic formula yields a complex formula. begin scalar prem,prod1,prod2,gprod,rprod,iprem,w,z,atl,natl; if cl_cxfp f then atl := rl_argn f else atl := {f}; w := acfsf_gsdis2impl atl; iprem := car w; prod1 := cadr w; prod2 := caddr w; gprod := cdar gp; prem := append(iprem,caar gp); if null prem then return f; prem := sfto_groebnerf prem; z := numr simp acfsf_gsmkradvar(); rprod := acfsf_gseqprod(prod1,prod2,gprod,prem,z); if rprod eq 'true then << if !*rlgsvb then ioto_prin2 "!"; return 'true >>; w := acfsf_gsusepremise(cdr gp,prem,z); if w eq 'true then << if !*rlgsvb then ioto_prin2 "!"; return 'true >>; natl := acfsf_gsredatl(atl,prem,z,rprod); if natl eq 'true then << if !*rlgsvb then ioto_prin2 "!"; return 'true >>; if rprod and rprod neq 'false then natl := rprod . natl; natl := nconc(natl,acfsf_gspremise(iprem,caar gp)); return rl_smkn('or,natl) end; procedure acfsf_gsredatl(atl,prem,z,rprod); % Algebraically closed field standard form reduce atomic formula % list. [atl] is a list of SF's; [prem] is a Groebner basis; [z] is % a kernel; [rprod] is a flag. Returns ['true] or a list of atomic % formulas. begin scalar a,w,natl; while atl do << a := car atl; atl := cdr atl; w := acfsf_gsredat(a,prem,z,rprod); if w eq 'true then atl := nil else if w and w neq 'false then natl := w . natl >>; if w eq 'true then return 'true; return natl end; procedure acfsf_gsusepremise(atl,prem,z); % Algebraically closed field standard form use premise. [atl] is a % list of atomic formulas; [prem] is a Groebner basis; [z] is a % kernel. returns [nil] or ['true]. begin scalar w; while atl do << w := acfsf_gsredat(car atl,prem,z,nil); if w eq 'true then atl := nil else atl := cdr atl; >>; if w eq 'true then return 'true; end; procedure acfsf_gseqprod(iprod1,iprod2,gprod,prem,z); % Algebraically closed field standard form equation product. % [iprod1], [iprod2], and [prem] are SF's; [prem] is a list of % SF's; [z] is a kernel. Returns [nil] or a formula. begin scalar p,w; p := multf(iprod1,multf(iprod2,gprod)); % Comment the test on [!*rlgsrad] out if the radical membership % test should always be performed for the equation product. if !*rlgsrad and (null sfto_greducef(1,addf(1,negf multf(p,z)) . prem)) then return 'true; w := acfsf_gstryeval('equal,sfto_preducef(p,prem)); if rl_tvalp w then return w; if null !*rlgsprod then return nil; if !*rlgsred then return acfsf_0mk2('equal,sfto_preducef(iprod1,prem)); return acfsf_0mk2('equal,iprod1); end; procedure acfsf_gsmkradvar(); % Algebraically closed field standard form Groebner simplifier make % radical memebership test variable. Returns an identifier that is % not used as an algebraic mode variable. begin scalar w; integer n; w := 'rlgsradmemv!*; while get(w,'avalue) do w := mkid(w,n := n+1); if !*rlgsutord then acfsf_gsupdtorder w; return w; end; procedure acfsf_gsupdtorder(v); % Algebraically closed field standard form Groebner simplifier % update term order. [v] is a kernel. Inserts the main variable [v] % into the variable list of the global fixed term order of the % [groebner] package. Not all torders are supported, if a variable % list is present. To get over this problem one can insert the tag % variable [v] in the variable list before calling the Groebner % simplifier. begin scalar curtorder,vl,remain,mode; curtorder := cdr torder('((list) revgradlex)); vl := cdar curtorder; if null vl or (v memq vl) then << torder curtorder; return nil >>; mode := cadr curtorder; if not(mode memq '(lex gradlex revgradlex gradlexgradlex gradlexrevgradlex lexgradlex lexrevgradlex weighted)) then rederr {"term order", mode, "not supported"}; remain := cddr curtorder; vl := append(vl,{v}); torder (('list . vl) . mode . remain) end; procedure acfsf_gstryeval(rel,lhs); % Algebraically closed field standard form try evaluation. [rel] is % an acfsf-relation; [lhs] a SF. returns [nil], a truth value or an % atomic formula. In the first case the atomic formula $([lhs] % [rel] 0)$ cannot be evaluated or should be ignored. In the other % case the returned value is equivalent to the the atomic formula. begin scalar w,!*rlsiexpla; if !*rlgserf then << w := cl_simplat(acfsf_0mk2(rel,lhs),nil); return if rl_tvalp w then w >>; if domainp lhs then return cl_simplat(acfsf_0mk2(rel,lhs),nil) end; procedure acfsf_gsdis2impl(atl); % Algebraically closed field standard form Groebner simplifier % disjunction to implication. [atl] is a list of atomic formulas. A % CIMPL is returned. The classification of the atomic formulas in % [atl] is done by [acfsf_attype]. begin scalar prem,prod1,prod2,other,w,a; prod1 := prod2 := 1; for each at in atl do << w := acfsf_gsattype at; if w then << a := car w; if a eq 'equal then prod1 := multf(cdr w,prod1) else if a eq 'cequal then prod2 := multf(cdr w,prod2) else if a eq 'neq then prem := cdr w . prem else rederr {"BUG IN ACFSF_GSDIS2IMPL",car w} >>; if not (w memq '(equal neq)) then other := at . other >>; return {prem, prod1, prod2, other}; end; procedure acfsf_gsattype(at); % Algebraically closed field standard form Groebner simplifier % atomic formula type. [at] is an atomic formula. [nil] or a pair % $(\rho,p)$ is returned. $\rho$ is either ['equal], ['neq], or % ['cequal]; $p$ is a SF. (if w eq 'equal then ('equal . acfsf_arg2l at) else if w memq '(geq leq) then ('cequal . acfsf_arg2l at) else if w eq 'neq then ('neq . acfsf_arg2l at)) where w=acfsf_op at; procedure acfsf_gsredat(at,gb,z,flag); % Algebraically closed field standard form Groebner simplifier % reduce atomic formula. [at] is an atomic formula; [gb] is a % Groebner basis; [z] is a variable; [flag] is a flag. [nil], a % truth value or an atomic formula is returned. The behavior of % this procedure depends on the switches [rl_gsred] and [rl_gsrad]. % [nil] is returned if the atomic formula belongs to the premise or % [flag] is [T] and [at] is an equation. Is [flag] is non [nil] % then equations can be ignored. In the other cases the returned % value is equivalent to [at]. The intention of this procedure is % the reduction of [at] wrt. the radical generated by [gb]. begin scalar w,x,op,arg,nat; op := acfsf_op at; if (op eq 'neq) or (flag and op eq 'equal) then return nil; arg := acfsf_arg2l at; w := sfto_preducef(arg,gb); if !*rlgsred then nat := cl_simplat(acfsf_0mk2(op,w),nil) else if x := acfsf_gstryeval(op,w) then nat := x else nat := at; if (rl_tvalp nat) or (op eq 'equal) or (null !*rlgsrad) then return nat; if null sfto_greducef(1,addf(1,negf multf(w,z)) . gb) then return cl_simplat(acfsf_0mk2(op,nil),nil); return nat; end; procedure acfsf_gspremise(tl,gp); % Algebraically closed field standard form Groebner simplify % premise. [tl] and [gp] are lists of SF's. A list of atomic % formulas is returned. The behavior of this procedure depends on % the switches [rl_gsred] and [rl_gssub]. The conjunction over the % returned formulas is equivalent to the formula $\bigvee(t_i \neq % 0)$ supposed that $\bigwedge(g_j = 0)$, where $t_i$ are the terms % in [tl] and $g_j$ are the terms in [gp]. If the switch [rl_gsred] % is on then all terms $t_i$ are reduced modulo Id([gp]). If the % switch [!*rl_gssub] is on, the term list is substituted by the % reduced Groebner base of the term list. begin scalar gb,rtl,w; if !*rlgsred then << gb := sfto_groebnerf gp; for each sf in tl do if w := sfto_preducef(sf,gb) then rtl := lto_insert(w,rtl); >> else rtl := tl; if !*rlgssub then return for each sf in sfto_groebnerf rtl collect acfsf_0mk2('neq,sf); return for each sf in rtl collect acfsf_0mk2('neq,sf) end; procedure acfsf_gssimulateprod(prem,prodal); % Algebraically closed field standard form simulate rlprod switch. % [prem] is a quantifier free formula. [prodal] is an assoc list % containing to some equations its product representation. begin scalar w,res; if rl_tvalp prem then return prem; if cl_atfp prem and (w := lto_cassoc(prem,prodal)) then return w; res := for each f in rl_argn prem collect if cl_atfp f and (w := lto_cassoc(f,prodal)) then w else f; return rl_mkn(rl_op prem,res) end; endmodule; % [acfsfgs] end; % of file