(* ----------------------------------------------------------------------------
* $Id: PQSMPL.mi,v 1.3 1995/11/04 18:00:28 pesch Exp $
* ----------------------------------------------------------------------------
* Copyright (c) 1993 Universitaet Passau
* ----------------------------------------------------------------------------
* This file is part of MAS.
* ----------------------------------------------------------------------------
* $Log: PQSMPL.mi,v $
* Revision 1.3 1995/11/04 18:00:28 pesch
* Changed comments violating documentation rules. Should be rewritten.
*
* Revision 1.2 1994/11/28 21:12:09 dolzmann
* Moved procedures from PQSMPL into PQBASE.
*
* Revision 1.1 1993/12/18 20:12:20 dolzmann
* System for the simplification of boolean combinations of polynomial
* equations.
*
* ----------------------------------------------------------------------------
*)
IMPLEMENTATION MODULE PQSMPL;
(* Polynomial Equation Simplification Implementation Module. *)
(******************************************************************************
* P O L Y N O M I A L E Q U A T I O N S I M P L I F I C A T I O N *
*-----------------------------------------------------------------------------*
* Author: Andreas Dolzmann *
* Language: Modula II *
* System: This program is written for the computer algebra system MAS by *
* Heinz Kredel. *
* Remark: Libraries maskern, maslisp and maslog, masdom, maspoly, ... *
* are used. *
* Abstract: A program for simplification of polynomial equations and *
* inequations in the field of the complex numbers. *
******************************************************************************)
FROM MASELEM IMPORT GAMMAINT;
FROM MASSTOR IMPORT ADV, COMP, FIRST, INV, LENGTH, LIST, LIST1, LISTVAR,
RED, SFIRST, SIL, SRED;
FROM MASBIOS IMPORT BKSP, BLINES, CREAD, CREADB, CWRITE, DIBUFF, DIGIT,
LETTER, LISTS, MASORD, SWRITE;
FROM SACLIST IMPORT ADV2, ADV3, ADV4, AWRITE, CCONC, CINV, CLOUT, COMP2,
CONC, EQUAL, LIST10, LIST2, LIST3, LIST4, LIST5,
MEMBER, SECOND, THIRD;
FROM MASERR IMPORT ERROR, confusion, fatal, harmless, severe, spotless;
FROM MASSYM IMPORT ATOM, MEMQ;
FROM MASSYM2 IMPORT ASSOC, ASSOCQ, EXPLOD, SREAD1, SYMBOL, UREAD, UWRIT1,
UWRITE;
FROM MASLISPU IMPORT Declare;
FROM MLOGBASE IMPORT ET, FALSUM, FORGARGS, FORGOP, FORMKBINOP, FORMKFOR,
FORMKUNOP, FORPARGS, FORPBINOP, FORPFOR, FORPUNOP,
FORPUNOPA, IMP, NON, TVAR, VEL, VERUM;
FROM MASLOG IMPORT FORAPPLYAT, FORELIMXOPS, FORMKCNF, FORMKDNF,
FORMKPOS, FORSMPL, FORMKPRENEX, FORMKPRENEX1;
FROM MLOGIO IMPORT FORIREAD, FORPPRT, FORPREAD, FORTEXW, KEYREAD;
FROM DIPADOM IMPORT DILWR, DIPNEG, DIPROD, DIPSUM, DIREAD, DIWRIT;
FROM DIPC IMPORT DILBSO, DIPBSO, DIPFMO, DIPINV, DIPLPM, DIPMAD,
DIPNOV, EVORD, EVSIGN, GRLEX, IGRLEX, INVLEX, LEX,
REVILEX, REVITDG, REVLEX, REVTDEG, VALIS;
FROM DIPGB IMPORT DIIFGB, DIIFNF, DILIS, DIPGB, DIPNOR;
FROM MASADOM IMPORT ADDDWRIT, ADFI, ADDDREAD;
FROM SACSET IMPORT LBIBMS;
FROM SACPOL IMPORT VLREAD, VLWRIT;
FROM PQBASE IMPORT DOMAIN, PQMKCNF, PQMKDNF, PQSMPL, PQMKPRENEX,
PQELIMXOPS, pqmkaf, pqpaf, PQIREAD, PQPPRT, EQU, NEQ;
FROM DIPTOOLS IMPORT ADDDFDIP, DILINV, DILPROD, DIPONE, DIPPOWER,
EvordPop, EvordPush, ValisPop, ValisPush;
TYPE SetRel=(subset,superset,setequal,setnorel);
CONST rcsidi = "$Id: PQSMPL.mi,v 1.3 1995/11/04 18:00:28 pesch Exp $";
CONST copyrighti = "Copyright (c) 1993 Universitaet Passau";
(******************************************************************************
* G L O B A L V A R I A B L E S *
******************************************************************************)
VAR PQTRACE: LIST; (* This variable determines, how many tracing
output is printed. *)
VAR PQRMSTest: LIST; (* This variable determines the method for the radical
mebership test. (Radical Membership Test)*)
VAR PQPOWERS: LIST; (* A list of powers for a pseudo radical membership
test. *)
VAR PQIBREP: LIST; (* This variable determines whether a ideal basis is
replaced by another or not. (Ideal Basis REPlace) *)
VAR PQREDCON: LIST; (* This variable determines wheter the conclusions
are reduced. *)
(******************************************************************************
* S I M P L I F I C A T I O N *
******************************************************************************)
PROCEDURE PQSCNF(phi: LIST):LIST;
(* polynomial equation simplification normal form. phi is an arbitrary
quantifier-free formula. A equivalent formula in SCNF is returned. *)
VAR nf: LIST;
BEGIN
nf:=SimplifyNf(PQMKCNF(PQSMPL(phi)));
IF (nf=VERUM) OR (nf=FALSUM) THEN
RETURN nf;
END;
RETURN PQscnf(PQGetDataCnf(nf));
END PQSCNF;
PROCEDURE PQSDNF(phi: LIST):LIST;
(* polynomial equation simplification normal form. phi is an arbitrary
quantifier-free formula. A equivalent formula in SDNF is returned. *)
VAR nf: LIST;
BEGIN
nf:=SimplifyNf(PQMKCNF(PQSMPL(phi)));
IF (nf=VERUM) OR (nf=FALSUM) THEN
RETURN nf;
END;
RETURN PQsdnf(PQGetDataDnf(nf));
END PQSDNF;
PROCEDURE PQCnfSimplify(nu:LIST):LIST;
(* polynomial equation cnf based simplification. nu is an quantifier free
formula. The formula nu is simplified. Consult the documentation for a
description of the rules which are applied *)
BEGIN
DLSWRITE("starting cnf based simplification",1);
(* DLPQPRT("Input formula",nu,2); *)
RETURN PQSimplify1(SimplifyNf(PQMKCNF(PQSMPL(nu))),1);
END PQCnfSimplify;
PROCEDURE PQDnfSimplify(nu:LIST):LIST;
(* polynomial equation dnf based simplification. nu is an quantifier free
formula. The formula nu is simplified. Consult the documentation for a
description of the rules which are applied *)
BEGIN
DLSWRITE("starting cnf based simplification",1);
(* DLPQPRT("Input formula",nu,2); *)
RETURN PQSimplify1(SimplifyNf(PQMKDNF(PQSMPL(nu))),2);
END PQDnfSimplify;
PROCEDURE PQSimplify1(nf,type: LIST):LIST;
(* polynomial equation simplification. nf is a quantifier free formula
in cnf (type=1) or dnf (type=2). Consult the documentation for a description
of the rules which are applied. The formula is divided in two parts:
Implications of the form "(AND PHI=0) => gamma=0" and a conjunction of
the form "AND PSI=0". PHI=0 denotes a set of polynomial equations phi=0 and
PSI=0 denotes a set of polynomial equations psi=0. *)
VAR POLS, PSI, GB1, GBi2, PHI, GAMMA, gamma, phi: LIST;
VAR gamma1: LIST;
VAR GAMMA1, PHI1, phi1, B: LIST;
VAR domain: LIST;
BEGIN
IF (nf=VERUM) OR (nf=FALSUM) THEN
DLPQPRT("Input formula in SNF",nf,2);
RETURN nf;
END;
IF type=1 THEN
POLS:=PQGetData1(nf,1);
DLPQPRT("Input formula in SCNF",PQscnf(POLS),2);
ELSE
POLS:=PQGetData1(nf,2);
DLPQPRT("Input formula in SDNF",PQsdnf(POLS),2);
END;
PSI:=THIRD(POLS);
DLSWRITE("1.) consistency test over psi",1);
GB1:=SIL;
IF PSI<>SIL THEN
domain:=ADDDFDIP(FIRST(PSI));
GB1:=DIPADGB(PSI); (* This computation is not necceary
in the case of PQRMSTest<=3 *)
IF IdealMember(GB1,DIPONE(domain)) THEN
IF type=1 THEN
RETURN FALSUM;
ELSE
RETURN VERUM;
END
END;
CASE INTEGER(PQIBREP) OF
0: |
1: PSI:=DIPADIRSET(PSI); |
2: PSI:=DIPADIRSET(GB1);
ELSE ERROR(severe,"PQIBREP unknown code!");
END;
END;
PHI:=FIRST(POLS);
GAMMA:=SECOND(POLS);
GAMMA1:=SIL;
PHI1:=SIL;
DLSWRITE("2.) simplification of the implications",1);
WHILE PHI<>SIL DO
ADV(GAMMA,gamma,GAMMA);
ADV(PHI,phi,PHI);
IF NOT TestRMember(phi,GB1,gamma,B,gamma1) THEN
GAMMA1:=COMP(gamma1,GAMMA1);
PHI1:=COMP(B,PHI1);
END;
END;
IF type=1 THEN
RETURN PQSMPL(PQscnf(LIST3(INV(PHI1),INV(GAMMA1),PSI)));
ELSE
RETURN PQSMPL(PQsdnf(LIST3(INV(PHI1),INV(GAMMA1),PSI)));
END
END PQSimplify1;
PROCEDURE SimplifyNf(nf: LIST):LIST;
(* simplify normal form. nf is a formula in disjunctive normal form or
conjunctive normal form. A simplification of nf is returned.
Following rules are applied: Equal literals in clauses are contracted,
atomic formulas with identical polynomials are contracted to TRUE or FALSE. *)
(* Note: identical clauses are not contracted. This happens in the
GetDataXXX Procedures. In this procedure equal implications are contracted. *)
VAR literal, clause, lhs, rel, op1, op2, Literals, Clauses: LIST;
VAR PolRel, ResLits, ResClaus, assoc, s: LIST;
VAR exit: BOOLEAN;
BEGIN
s:=PQSMPL(nf); (* To strong ! *)
IF (s=VERUM) OR (s=FALSUM) THEN RETURN s; END;
FORPFOR(nf,op1,Clauses);
ResClaus:=SIL;
WHILE Clauses<>SIL DO
ResLits:=SIL;
PolRel:=SIL;
FORPARGS(Clauses, clause, Clauses);
FORPFOR(clause,op2,Literals);
exit:=FALSE;
WHILE (Literals<>SIL) AND NOT exit DO
FORPFOR(Literals,literal,Literals);
pqpaf(literal,rel,lhs);
assoc:=ASSOCQ(lhs,PolRel);
IF assoc=SIL THEN
PolRel:=COMP2(lhs,rel,PolRel);
ResLits:=COMP(literal,ResLits);
ELSIF FIRST(assoc)<>rel THEN
DLSWRITE("smart simplify successful",3);
ResLits:=SIL;
exit:=TRUE;
ELSE
DLSWRITE("identical atomic formulas deleted",
3);
END;
END;
IF ResLits<>SIL THEN
ResClaus:=COMP(FORMKFOR(op2,INV(ResLits)),ResClaus);
END;
END;
IF (ResClaus=SIL) AND (op1=ET) THEN
RETURN VERUM;
ELSIF (ResClaus=SIL) AND (op1=VEL) THEN
RETURN FALSUM;
ELSE (* ResClaus<>SIL *)
RETURN FORMKFOR(op1,INV(ResClaus));
END;
END SimplifyNf;
(******************************************************************************
* P R E P R O Z E S S I N G *
******************************************************************************)
(******************************************************************************
* data structure SNFC ("Simplification Normal Form Content") *
* *
* This datastructure represents the important datas from a formula in SCNF *
* or SDNF. A variable of the type SNFC is a list with three elements. *
* The first and second elemts represents the first part of the S?NF and the *
* third element the second part of the S?NF. *
* The first and the second element are lists with one element for each *
* implikation in the S?NF. Each element in the first list is a list of all *
* polynomials in the premise of the implication. Each element in the second *
* list is the polynomial in the conclusion. The third element is a list of *
* all polynomials in the second part of the S?NF. *
******************************************************************************)
PROCEDURE PQGetDataCnf(cnf: LIST): LIST;
(* polynomial equation get data from cnf. *)
BEGIN
RETURN PQGetData1(cnf,1);
END PQGetDataCnf;
PROCEDURE PQGetDataDnf(dnf: LIST): LIST;
(* polynomial equation get data from dnf. *)
BEGIN
RETURN PQGetData1(dnf,2);
END PQGetDataDnf;
PROCEDURE PQGetData1(nf,type: LIST):LIST;
(* polynomial equation get data. nf is a cnf (type=1) or a dnf (type=2).
The polynomials which occurs in the formula nf are extracted.
The formula is transformed in a formula with a structure
similar to (OP (AND PHI_j=0) => gamma_i=0) OP (AND PSI=0).
PHI_j=0 denotes a set of polynomial equations phi_ij=0 and PSI=0
denotes a set of polynomial equations psi=0. A list with the following
format is returned. (PHI,GAMMA,PSI), where PHI is a list of a list of
the polynomials in PHI_j, GAMMA is a list of the polynomials gamma_j, and
PSI is a list of the polynomials on PSI=0. *)
VAR clause,atomic:LIST;
VAR POS,NEG:LIST;
VAR PHI,GAMMA,PSI: LIST;
VAR dummy,HLP: LIST;
VAR rel,pol,domain,af: LIST;
BEGIN
PHI:=SIL; PSI:=SIL; GAMMA:=SIL;
FORPFOR(nf,dummy,nf);
(* extract the domain descriptor *)
af:=FIRST(FORGARGS(FIRST(nf))); (* The first atomic formula of the
first clause. *)
pqpaf(af,dummy,pol);
domain:=ADDDFDIP(pol);
(* *** *)
WHILE nf<>SIL DO
FORPARGS(nf,clause,nf);
FORPFOR(clause,dummy,clause);
POS:=SIL; NEG:=SIL;
WHILE clause<>SIL DO
FORPARGS(clause,atomic,clause);
pqpaf(atomic,rel,pol);
IF rel=NEQ THEN
NEG:=COMP(pol,NEG);
ELSIF rel=EQU THEN
POS:=COMP(pol,POS);
ELSE
ERROR(severe,"unknown relation symbol");
END;
END;
IF type<>1 THEN (* a logical negation is necessary *)
HLP:=NEG;
NEG:=POS;
POS:=HLP;
END;
IF NEG=SIL THEN
PSI:=SETADD(DILPROD(POS,domain),PSI);
ELSE
NEG:=INV(NEG);
POS:=DILPROD(POS,domain);
IF NOT SeqPair(NEG,PHI,POS,GAMMA) THEN
PHI:=COMP(NEG,PHI);
GAMMA:=COMP(POS,GAMMA);
ELSE
DLSWRITE("identical implications deleted", 3);
END;
END;
END;
RETURN LIST3(INV(PHI),INV(GAMMA),INV(PSI));
END PQGetData1;
(******************************************************************************
* P O S T P R O C E S S I N G *
******************************************************************************)
PROCEDURE PQscnf(POLS: LIST):LIST;
(* polynomial equation simplification conjunctive normal form.
POLS is a list in the format, that PQGetDataCnf returns.
The SCNF associated with the list POLS is returned. *)
VAR fst,snd: LIST;
BEGIN
PQsnf1(POLS,1,fst,snd);
IF (fst=SIL) AND (snd=SIL) THEN
RETURN VERUM;
ELSIF fst=SIL THEN
RETURN FORMKFOR(ET,INV(snd));
ELSIF snd=SIL THEN
RETURN FORMKFOR(ET,INV(fst));
ELSE
RETURN FORMKBINOP(ET,FORMKFOR(ET,INV(fst)),
FORMKFOR(ET,INV(snd)));
END;
END PQscnf;
PROCEDURE PQsdnf(POLS: LIST):LIST;
(* polynomial equation simplification disjunctive normal form.
POLS is a list in the format, that PQGetDataCnf returns.
The SDNF associated with the list POLS is returned. *)
VAR fst, snd: LIST;
BEGIN
PQsnf1(POLS,2,fst,snd);
IF (fst=SIL) AND (snd=SIL) THEN
RETURN FALSUM;
ELSIF fst=SIL THEN
RETURN FORMKUNOP(NON,FORMKFOR(ET,INV(snd)));
ELSIF snd=SIL THEN
RETURN FORMKFOR(VEL,INV(fst));
ELSE
RETURN FORMKBINOP(VEL,FORMKFOR(VEL,INV(fst)),
FORMKUNOP(NON,FORMKFOR(ET,INV(snd))));
END;
END PQsdnf;
PROCEDURE PQsnf1(POLS,type:LIST;VAR fst,snd: LIST);
(* polynomial equation simplification normal form.
POLS is a list in the format, that PQGetDataCnf returns.
The first and the second part of the SCNF (type=1) or SDNF (type=2)
is returned. fst=SIL or snd=sil indicates, that this part can be omitted. *)
VAR PHIij, PHIj, phi, GAMMAi, gamma, PHIj1, PSIi, psi: LIST;
BEGIN
ADV3(POLS,PHIij,GAMMAi,PSIi,POLS);
fst:=SIL;
WHILE PHIij<>SIL DO
ADV(PHIij,PHIj,PHIij);
ADV(GAMMAi,gamma,GAMMAi);
PHIj1:=SIL;
WHILE PHIj<>SIL DO
ADV(PHIj,phi,PHIj);
PHIj1:=COMP(pqmkaf(EQU,phi),PHIj1)
END;
IF type=1 THEN
fst:=COMP(FORMKBINOP(IMP,FORMKFOR(ET,INV(PHIj1)),
pqmkaf(EQU,gamma)),fst);
ELSE
fst:=COMP(FORMKUNOP(NON,FORMKBINOP(IMP,FORMKFOR(ET,
INV(PHIj1)),pqmkaf(EQU,gamma))),fst);
END;
END;
snd:=SIL;
WHILE PSIi<>SIL DO
ADV(PSIi,psi,PSIi);
snd:=COMP(pqmkaf(EQU,psi),snd);
END;
RETURN;
END PQsnf1;
(******************************************************************************
* I D E A L P R O C E D U R E S *
******************************************************************************)
PROCEDURE TestRMember(F,G,p:LIST; VAR B,p1: LIST):BOOLEAN;
(* test radical membership. F is a final radical basis,
G is a Groebner basis. p is a polynomial. If true is
returned then p in RAD(F join G). Note: If p is in the radical
then true is not necessary returned!
A new ideal basis of Id(F) is assigned to B. *)
VAR result:BOOLEAN;
BEGIN
CASE INTEGER(PQIBREP) OF
0: result:=TestRMember1(F,G,p,p1);
B:=F; |
1: B:=DIPADIRSET(F);
result:=TestRMember1(F,G,p,p1); |
2: B:=DIPADGB(F);
result:=TestRMember1(SIL,DIPADGBunion(B,G),p,p1);
ELSE ERROR(severe,"PQIBREP unknown code!");
END;
RETURN result;
END TestRMember;
PROCEDURE TestRMember1(F,G,p:LIST;VAR p1: LIST):BOOLEAN;
(* test radical membership 1. F is a final radical basis,
G is a Groebner basis. p is a polynomial. If true is
returned then p in RAD(F join G). Note: If p is in the radical
then true is not necessary returned! *)
VAR GB, F1, F0, RGB, power, POWERS: LIST;
VAR result: BOOLEAN;
VAR domain:LIST;
BEGIN
IF p=0 THEN RETURN TRUE; END;
domain:=ADDDFDIP(p);
result:=FALSE;
CASE INTEGER(PQRMSTest) OF
1: result:=MEMBER(p,CCONC(G,F))=1; |
2: F1:=CCONC(G,F);
result:=(MEMBER(p,F1)=1) OR (DIPADNF(F1,p)=0); |
3: F0:=CCONC(G,F);
F1:=DIPADIRSET(F0);
result:=(MEMBER(p,F0)=1) OR (MEMBER(p,F1)=1)
OR (DIPADNF(F1,p)=0); |
4: GB:=DIPADGBext(G,F);
result:=IdealMember(GB,p) |
5: POWERS:=PQPOWERS;
IF EQUAL(DIPONE(domain),p)=1 THEN
POWERS:=LIST1(1);
END;
GB:=DIPADGBext(G,F);
WHILE (POWERS<>SIL) AND NOT result DO
ADV(POWERS,power,POWERS);
IF IdealMember(GB,DIPPOWER(p,power)) THEN
result:=TRUE;
END;
END; |
6: GB:=DIPADGBext(G,F);
result:= (IdealMember(GB,p) OR
RadicalMember(GB,p)) |
7: (* GB:=DIPADGBext(G,F);
result:=RadicalMember(GB,p); *)
result:=RadicalMember(CCONC(G,F),p);
ELSE
ERROR(severe,"TestRMember: unknown code");
RETURN FALSE;
END;
IF (PQRMSTest>3) AND (PQREDCON=1) THEN
DLSWRITE("computing the normal form of the conclusion",2);
p1:=DIPADNF(GB,p);
DLSWRITE("... finished.",2);
ELSE
p1:=p;
END;
IF PQTRACE>=1 THEN
IF result THEN
SWRITE("Radical membership test ");
AWRITE(PQRMSTest);
SWRITE(" succeed.");
BLINES(0);
ELSE
SWRITE("Radical membership test ");
AWRITE(PQRMSTest);
SWRITE(" failed.");
BLINES(0);
END;
END;
RETURN result;
END TestRMember1;
PROCEDURE IdealMember(G,p:LIST):BOOLEAN;
(* ideal membership test. G is groebner basis. Iff p in ID(g) then 1
is returned otherwise 0. *)
BEGIN
RETURN DIPADNF(G,p)=0;
END IdealMember;
PROCEDURE RadicalMember(G,p:LIST):BOOLEAN;
(* radical membership test. G is an ideal basis. Iff p in RAD(G) then 1 is
returned otherwise 0. The new variable Rw is introduced. *)
VAR G1, G2: LIST;
VAR result: BOOLEAN;
VAR p1: LIST;
VAR domain: LIST;
BEGIN
IF p=0 THEN RETURN TRUE; END;
domain:=ADDDFDIP(p);
G1:=DILINV(G,0,1);
p1:=DIPINV(p,0,1);
ValisPush(COMP(LIST2(45,54),VALIS));
(* G2:=DIPADGBext(G1,LIST1(rabinowitsch(p1)));*)
G2:=DIPADGB(COMP(rabinowitsch(p1),G1));
result:=DIPADNF(G2,DIPONE(domain))=0;
ValisPop();
RETURN result;
END RadicalMember;
PROCEDURE rabinowitsch(p:LIST):LIST;
(* rabinowitsch. p is a non zero polynomial.
The polynomial 1-Zp is returned. Z denotes the variable with the exponent
vector (0,...,0,1). *)
VAR z,zexp,nov,dipone: LIST;
VAR domain: LIST;
BEGIN
domain:=ADDDFDIP(p);
nov:=DIPNOV(p);
dipone:=DIPFMO(ADFI(domain,1),GenEV(0,nov));
zexp:=GenEV(0,nov-1);
zexp:=INV(COMP(1,zexp));
z:=DIPFMO(ADFI(domain,1),zexp);
RETURN DIPSUM(dipone,DIPNEG(DIPROD(z,p)));
END rabinowitsch;
(******************************************************************************
* D I P A D - P R O C E D U R E S *
******************************************************************************)
PROCEDURE DIPADGB(P:LIST):LIST;
(* distributive polynomial arbitrary domain groebner basis. P is a list of
polynomials (over the ring of integers). A groebner basis of P is returned.
This procedure is at moment only a dummy procedure. It should
calculate a groebner basis in respect to the coefficient ring of the
polynomials. *)
VAR g:LIST;
BEGIN
DLSWRITE("Computing a Groebner Base ...",2);
g:=DIPGB(P,0);
DLSWRITE("... finished!",2);
RETURN g;
END DIPADGB;
PROCEDURE DIPADNF(P,S:LIST):LIST;
(* distributive polynomial arbitrary domain normal form. P is a list of
polynomials. The normal form of the polynomial
S w.r.t. P is returned. This procedure is at moment only a dummy. Is should
work on Polynomials over arbitrary fields and rings. *)
BEGIN
RETURN DIPNOR(P,S);
END DIPADNF;
PROCEDURE DILADNF(P,S:LIST):LIST;
(* distributive polynomial list arbitrary domain normal form. P is a list of
polynomials. S is a list of polynomials.
The list of normal forms of the polynomials of
S w.r.t. P is returned. This procedure is at moment only a dummy. Is should
work on Polynomials over arbitrary fields and rings. *)
VAR s,result: LIST;
BEGIN
result:=SIL;
WHILE S<>SIL DO
ADV(S,s,S);
result:=COMP(DIPADNF(P,s),result);
END;
RETURN INV(result);
END DILADNF;
PROCEDURE DIPADGBext(gb,pols:LIST):LIST;
(* distributive polynomial arbitrary domain groebner basis extension.
gb is a groebner basis, pols is a list of polynomials.
A groebner basis of the ideal basis gb join pols is calculated and
returned. This procedure is at moment only a dummy. *)
BEGIN
IF pols=SIL THEN RETURN gb; END;
RETURN DIPADGB(CCONC(gb,pols));
END DIPADGBext;
PROCEDURE DIPADGBunion(gb1,gb2:LIST):LIST;
(* distributive polynomial arbitrary domain groebner basis union. gb1 and
gb2 are groebner basis. A groebner basis of the ideal basis gb1 join gb2
is calculated and returned. This procedure is at moment only a dummy. *)
BEGIN
IF gb2=SIL THEN RETURN gb1; END;
IF gb1=SIL THEN RETURN gb2; END;
RETURN DIPADGB(CCONC(gb1,gb2));
END DIPADGBunion;
PROCEDURE DIPADIRSET(P:LIST):LIST;
(* distributive polynomial arbitrary domain irreducible set. P is a list
of polynomials. A set PP of polynomials is returned. PP is the result of
reducing each element p modulo P - {p} until no further reductions are
possible. *)
BEGIN
RETURN DILIS(P);
END DIPADIRSET;
PROCEDURE DIPADGBRED(gb: LIST):LIST;
(* distributive polynomial groebner basis reduction. gb is a groebner basis
of distributive polynomials over an arbitrary domain.
The unique reduced and ordered groebner basis to gp is returned. *)
BEGIN
IF (gb=SIL) OR (RED(gb)=SIL) THEN RETURN gb; END;
RETURN DIPLPM(DILIS(gb));
END DIPADGBRED;
(******************************************************************************
* A U X I L I A R Y P R O C E D U R E S *
******************************************************************************)
PROCEDURE SETADD(elem,set: LIST):LIST;
(* set add element. If the element elem is not in the set set, then
{elem} join set is returned else set is returned. *)
BEGIN
IF MEMBER(elem,set)=1 THEN
DLSWRITE("SETADD: element already in the set!",3);
RETURN set;
ELSE
RETURN COMP(elem,set);
END;
END SETADD;
PROCEDURE GenEV(value,length:LIST):LIST;
(* generate exponent vector. A exponent vector of the length length with
entries value is generated. *)
VAR i: INTEGER;
VAR result:LIST;
BEGIN
result:=SIL;
FOR i:=1 TO length DO
result:=COMP(value,result);
END;
RETURN result;
END GenEV;
PROCEDURE SeqPair(elem1,SEQ1,elem2,SEQ2:LIST): BOOLEAN;
(* sequence pair. elem1 and elem2 are elements, SEQ1, SEQ2 are final sequences
with the same length.
1 is returned iff there is a n in Nat such that elem1=SEQ1_n and elem2=SEQ2_n.
*)
VAR seq1,seq2: LIST;
BEGIN
WHILE SEQ1<>SIL DO
ADV(SEQ1,seq1,SEQ1);
ADV(SEQ2,seq2,SEQ2);
IF (EQUAL(seq1,elem1)=1) AND (EQUAL(seq2,elem2)=1) THEN
RETURN TRUE;
END;
END;
RETURN FALSE;
END SeqPair;
(******************************************************************************
* O P T I O N S *
******************************************************************************)
PROCEDURE PQOPT(O:LIST):LIST;
(* polynomial equation options. The options of the PQ-System are set.
The list O is of the following format: The first entry
is the trace level of the system, the second entry determines the method for
the radical membership test, the third entry is a list of powers for the
pseudo radical membership test, the fourth entry controls the replacement
of the premises of the implications, and the fifth entry controls the
You can omit an entry of O
by writing a -1 on the place of the entry. You need not specify all entries.
The old parameters are returned. *)
VAR old: LIST;
BEGIN
old:=LIST5(PQTRACE,PQRMSTest,PQPOWERS,PQIBREP,PQREDCON);
IF O<>SIL THEN
IF FIRST(O)<>-1 THEN ADV(O,PQTRACE,O); ELSE O:=RED(O); END;
END;
IF O<>SIL THEN
IF FIRST(O)<>-1 THEN ADV(O,PQRMSTest,O);ELSE O:=RED(O); END;
END;
IF O<>SIL THEN
IF FIRST(O)<>-1 THEN ADV(O,PQPOWERS,O); ELSE O:=RED(O); END;
END;
IF O<>SIL THEN
IF FIRST(O)<>-1 THEN ADV(O,PQIBREP,O); ELSE O:=RED(O); END;
END;
IF O<>SIL THEN
IF FIRST(O)<>-1 THEN ADV(O,PQREDCON,O); ELSE O:=RED(O); END;
END;
RETURN old;
END PQOPT;
PROCEDURE PQOPTWR();
(* polynomial options write. The options of the PQ-System are printed in the
output stream. *)
BEGIN
SWRITE("The setting of the options of the PQ-System:");
BLINES(0);
SWRITE(" The trace level is "); AWRITE(PQTRACE);
SWRITE(".");BLINES(0);
SWRITE(" Radical memebership test using ");
BLINES(0);
CASE INTEGER(PQRMSTest) OF
1: SWRITE(" element test."); |
2: SWRITE(" reduction with the ideal basis."); |
3: SWRITE(" reduction with the interreduced ideal basis.");|
4: SWRITE(" ideal membership test."); |
5: SWRITE(" ideal membership test with the ");
IF RED(PQPOWERS)=SIL THEN
SWRITE("power "); AWRITE(FIRST(PQPOWERS));
ELSE
SWRITE("powers "); UWRIT1(PQPOWERS);
END;
SWRITE("."); |
6: SWRITE(" radical membership test after ideal membership test."); |
7: SWRITE(" radical membership test."); |
ELSE SWRITE(" unknown test method specified!");
END;
BLINES(0);
CASE INTEGER(PQIBREP) OF
0: SWRITE(" Conjunctions over polynomial equations are not replaced."); |
1: SWRITE(" Reducing conjunctions over polynomial equations with the");
BLINES(0);
SWRITE(" interreduction-method."); |
2: SWRITE(" Reducing conjunctions over polynomial equations with the");
BLINES(0);
SWRITE(" Groebner-Basis-method.");
ELSE SWRITE("WARNING: unknown code for PQIBREP");
END;
BLINES(0);
IF PQREDCON=0 THEN
SWRITE(" The conclusions in the implications are not reduced.");
ELSE
SWRITE(" The conclusions in the implications are reduced.");
END;
BLINES(0);
END PQOPTWR;
(******************************************************************************
* D E B U G L E V E L *
******************************************************************************)
PROCEDURE PQSetTrace(level:LIST):LIST;
(* polynomial equation set debug level. The debug level is set to level.
The old value is returned. *)
VAR old:LIST;
BEGIN
old:=PQTRACE;
PQTRACE:=level;
RETURN old;
END PQSetTrace;
PROCEDURE PQGetTrace():LIST;
(* polynomial equation get debug level. The actual debug level is returned. *)
BEGIN
RETURN PQTRACE;
END PQGetTrace;
PROCEDURE DLSWRITE(S: ARRAY OF CHAR;level:LIST);
(* debug level SWRITE. The string S is in dependency of the debug level
written to the output stream. In contrast to MAS a blank line is added.
(analogous to UWRITE and UWRIT1) *)
BEGIN
IF PQTRACE >= level THEN
SWRITE(S);
BLINES(0);
END;
END DLSWRITE;
PROCEDURE DLSWRIT1(S: ARRAY OF CHAR;level:LIST);
(* debug level SWRITE. The string S is in dependency of the debug level
written to the output stream. *)
BEGIN
IF PQTRACE >= level THEN
SWRITE(S);
END;
END DLSWRIT1;
PROCEDURE DLUWRITE(L,level:LIST);
(* debug level UWRITE. The list L is in dependency of the debug level
written to the output stream. *)
BEGIN
IF PQTRACE >= level THEN
UWRITE(L);
END;
END DLUWRITE;
PROCEDURE DLUWRIT1(L,level:LIST);
(* debug level UWRIT1. The list L is in dependency of the debug level
written to the output stream. *)
BEGIN
IF PQTRACE >= level THEN
UWRIT1(L);
END;
END DLUWRIT1;
PROCEDURE DLBLINES(n:LIST;level:LIST);
(* debug level BLINES. n blank lines are in dependency of the debug level
written to the output stream. *)
BEGIN
IF PQTRACE >= level THEN
BLINES(n);
END;
END DLBLINES;
PROCEDURE DLPQPRT(S:ARRAY OF CHAR; phi: LIST; level:LIST);
(* debug level polynomial equation print. The string S is written to the
output stream, the the formula phi is written to the output stream. As the
final step a blank lines is written to the output stream. *)
BEGIN
IF PQTRACE>= level THEN
SWRITE(S);
BLINES(0);
PQPPRT(phi);
BLINES(0);
END;
END DLPQPRT;
PROCEDURE PQDEMO();
(* Demonstration for this package. *)
VAR V, phi: LIST;
BEGIN
SWRITE(" ");
SWRITE("D E M O N S T R A T I O N O F T H E P Q - S Y S T E M");
BLINES(2);
SWRITE("Enter the list of variables, please!");
BLINES(1);
V:=UREAD();
VALIS:=V;
BLINES(0);
SWRITE("Enter the formula, please!");
BLINES(1);
phi:=PQIREAD();
phi:=PQCnfSimplify(phi);
BLINES(1);
SWRITE("The result is:");
PQPPRT(phi);
BLINES(2);
END PQDEMO;
(******************************************************************************
* M A I N *
******************************************************************************)
BEGIN
(* *** listvar declarations for global variables. *** *)
LISTVAR(PQRMSTest);
LISTVAR(PQPOWERS);
LISTVAR(PQTRACE);
LISTVAR(PQIBREP);
LISTVAR(PQREDCON);
(* *** initialize the global variables. *** *)
PQTRACE:=0;
PQPOWERS:=LIST1(1);;
PQRMSTest:=6;
PQIBREP:=1;
PQREDCON:=0;
END PQSMPL.
(* -EOF- *)