(* ----------------------------------------------------------------------------
* $Id: PQBASE.mi,v 1.2 1996/05/19 07:53:50 dolzmann Exp $
* ----------------------------------------------------------------------------
* Copyright (c) 1993 Universitaet Passau
* ----------------------------------------------------------------------------
* This file is part of MAS.
* ----------------------------------------------------------------------------
* $Log: PQBASE.mi,v $
* Revision 1.2 1996/05/19 07:53:50 dolzmann
* Bug fixed in pqsimplifyaf.
*
* Revision 1.1 1994/11/28 21:10:04 dolzmann
* New modules PQBASE.md and PQBASE.mi:
* Procedures for the manipulating first oder formulas over the language of
* ordered rings.
* New modules RQEPRRC.md and RQEPRRC.mi:
* Procedures for the real quantifier elimination.
* New modules TFORM.md and TFORM.mi:
* Procedures for the computation of type formulas.
* Makefile adapted.
*
* ----------------------------------------------------------------------------
*)
IMPLEMENTATION MODULE PQBASE;
(* Polynomial Equation Base Definition Module. *)
(******************************************************************************
* P Q B A S E *
*-----------------------------------------------------------------------------*
* Author: Andreas Dolzmann *
* Language: Modula II *
* System: This program is written for the computer algebra system MAS by *
* Heinz Kredel. *
* Abstract: Implementation of the language of ordered fields. The *
* implementation use distributive polynomials over an arbitrary *
* domain for the representation of terms. *
******************************************************************************)
FROM DIPADOM IMPORT DILWR, DIPNEG, DIPROD, DIPSUM, DIREAD, DIWRIT;
FROM DIPC IMPORT DILBSO, DIPBSO, DIPERM, DIPFMO, DIPINV, DIPLPM,
DIPMAD, DIPMCP, DIPNOV, EVORD, EVSIGN, GRLEX,
IGRLEX, INVLEX, LEX, REVILEX, REVITDG, REVLEX,
REVTDEG, VALIS, DIPLBC;
FROM DIPTOOLS IMPORT DIPCNST, DIPIMO, DIPMVV;
FROM DOMRN IMPORT DOMRND;
FROM LISTTOOLS IMPORT LSRCHQ;
FROM MASADOM IMPORT ADDDREAD, ADDDWRIT, ADFI, ADGCD, ADNEG, ADONE,
ADQUOT, ADSIGN, ADWRIT,ADPCPP;
FROM MASBIOS IMPORT BKSP, BLINES, CREAD, CREADB, CWRITE, DIBUFF, DIGIT,
LETTER, LISTS, MASORD, SWRITE;
FROM MASELEM IMPORT GAMMAINT;
FROM MASERR IMPORT ERROR, confusion, fatal, harmless, severe, spotless;
FROM MASLISPU IMPORT Declare, PROCF1, PROCF2;
FROM MASLOG IMPORT FORAPPLYAT, FORELIMXOPS, FORMKCNF, FORMKDNF,
FORMKPOS, FORMKPRENEX, FORMKPRENEX1, FORMKVD,
FORREPAFS, FORSIMPLIFY, FORSIMPLIFYP, FORSMPL;
FROM MASSET IMPORT SetUnion;
FROM MASSTOR IMPORT ADV, COMP, FIRST, INV, LENGTH, LIST, LIST1, LISTVAR,
RED, SFIRST, SIL, SRED;
FROM MASSYM IMPORT ATOM, MEMQ;
FROM MASSYM2 IMPORT ASSOC, ASSOCQ, EXPLOD, SREAD1, SYMBOL, UREAD, UWRIT1,
UWRITE;
FROM MLOGBASE IMPORT ANY, EQUIV, ET, EXIST, FALSUM, FORALL, FORGARGS,
FORGLVAR, FORGOP, FORMKBINOP, FORMKFOR, FORMKLVAR,
FORMKUNOP, FORMKVAR, FORPARGS, FORPBINOP, FORPFOR,
FORPQUANT, FORPUNOP, FORPUNOPA, FORPVAR, FORVTENTER,
FORVTGET, IMP, NON, REP, TVAR, VEL, VERUM, XOR;
FROM MLOGIO IMPORT FORIREAD, FORPPRT, FORPREAD, FORTEXW, KEYREAD;
FROM SACLIST IMPORT ADV2, ADV3, ADV4, AWRITE, CCONC, CINV, CLOUT, COMP2,
CONC, EQUAL, FIRST2, LIST10, LIST2, LIST3, LIST4,
LIST5, MEMBER, SECOND, SLELT, SUFFIX, THIRD;
FROM SACPOL IMPORT VLREAD, VLWRIT;
FROM SACSET IMPORT LBIBMS;
CONST rcsidi = "$Id: PQBASE.mi,v 1.2 1996/05/19 07:53:50 dolzmann Exp $";
CONST copyrighti = "Copyright (c) 1993 Universitaet Passau";
(******************************************************************************
* G L O B A L V A R I A B L E S *
******************************************************************************)
VAR BbfParserSyms: LIST;(* The symbol table for the symbols of atomic
formulas. *)
VAR NewVariables: INTEGER;
(******************************************************************************
* A T O M I C F O R M U L A S *
******************************************************************************)
PROCEDURE pqmkaf(rel:LIST;pol:LIST):LIST;
(* polynomial equation make atomic formula.
rel is a relation, pol is a
polynomial, the atomic formula (rel,id) is returned. *)
BEGIN
RETURN LIST2(rel,pol);
END pqmkaf;
PROCEDURE pqpaf(af:LIST; VAR rel,pol:LIST);
(* polynomial equation parse atomic formula. af is an atomic
formula; the relation symbol of af is in rel returned; the polynomial of af
is in id returned. *)
BEGIN
FIRST2(af,rel,pol);
END pqpaf;
PROCEDURE pqgrel(af:LIST):LIST;
(* polynomial equation get relation symbol. af is an atomic formula. The
relation symbol of af is returned. *)
BEGIN
RETURN FIRST(af);
END pqgrel;
PROCEDURE pqgpol(af:LIST):LIST;
(* polynomial equation get relation symbol. af is an atomic formula. The
polynomial of af is returned. *)
BEGIN
RETURN SECOND(af);
END pqgpol;
PROCEDURE pqatom(phi:LIST):BOOLEAN;
(* polynomial equation atomic formula. pqatom returns true
iff phi has the structure of an atomic formula, i.e. phi is a list
with two elements, and the first element of the list is an valid
relation symbol. *)
VAR rel,id: LIST;
BEGIN
IF (phi=SIL) OR ATOM(phi) OR SYMBOL(phi) THEN RETURN FALSE; END;
ADV(phi,rel,phi);
IF (phi=SIL) OR (RED(phi)<>SIL) THEN RETURN FALSE; END;
RETURN (rel=EQU) OR (rel=NEQ) OR (rel=LES) OR (rel=GRE) OR
(rel=GRQ) OR (rel=LSQ);
END pqatom;
PROCEDURE pqprtaf(af: LIST);
(* polynomial equation print atomic formula. The atomic formula
af is printed.
*)
VAR rel,pol:LIST;
BEGIN
ADV2(af,rel,pol,af);
SWRITE("[");
DIWRIT(pol,VALIS);
IF rel=EQU THEN SWRITE(" = 0]");
ELSIF rel=NEQ THEN SWRITE(" <> 0]");
ELSIF rel=LES THEN SWRITE(" < 0]");
ELSIF rel=GRE THEN SWRITE(" > 0]");
ELSIF rel=LSQ THEN SWRITE(" <= 0]");
ELSIF rel=GRQ THEN SWRITE(" >= 0]");
ELSE ERROR(severe,"pqprtaf: unknown relation symbol");
END;
END pqprtaf ;
PROCEDURE pqtexwaf(af: LIST);
(* polynomia equation tex write atomic formula. The atomic formula af
is written to the output stream. *)
VAR rel,pol:LIST;
BEGIN
ADV2(af,rel,pol,af);
BLINES(0);
DITEX(pol,VALIS);
IF rel=EQU THEN SWRITE("=0");
ELSIF rel=NEQ THEN SWRITE("\neq 0");
ELSIF rel=LES THEN SWRITE("<0");
ELSIF rel=GRE THEN SWRITE(">0");
ELSIF rel=LSQ THEN SWRITE("\leq 0");
ELSIF rel=GRQ THEN SWRITE("\geq 0");
ELSE ERROR(severe,"pqtexwaf: unknown relation symbol");
END;
END pqtexwaf ;
PROCEDURE DITEX(A,V: LIST);
(*Distributive polynomial write. A is a distributive
polynomial in r variables, r ge 0. V is a variable list
for A. A is written in the output stream. *)
VAR AL, AS, E, EL, FL, ES, LL, RL, SL, TL, VL, VS: LIST;
BEGIN
(*1*) (*rl=0 or a=0.*)
IF A = 0 THEN AWRITE(A); RETURN; END;
RL:=DIPNOV(A);
IF RL = 0 THEN ADWRIT(DIPLBC(A)); RETURN; END;
(*2*) (*general case.*) AS:=A; FL:=0; (* LL:=DIPNBC(A);
IF LL > 1 THEN SWRITE("("); END; *)
REPEAT DIPMAD(AS, AL,E,AS); SWRITE(" "); SL:=ADSIGN(AL);
IF FL <> 0 THEN
IF SL > 0 THEN SWRITE("+"); END;
IF SL < 0 THEN SWRITE("-"); AL:=ADNEG(AL); END;
END;
FL:=1; TL:=EVSIGN(E);
IF TL = 0 THEN ADWRIT(AL);
ELSE SL:=ADONE(AL);
IF SL <> 1 THEN ADWRIT(AL); END;
ES:=CINV(E); VS:=V;
REPEAT ADV(ES, EL,ES); ADV(VS, VL,VS);
IF EL > 0 THEN SWRITE(" "); CLOUT(VL);
IF EL > 1 THEN SWRITE("^{");
AWRITE(EL); SWRITE("}"); END;
END;
UNTIL ES = SIL;
END;
UNTIL AS = SIL;
SWRITE(" ");
(* IF LL > 1 THEN SWRITE(")"); END; *)
(*5*) RETURN; END DITEX;
PROCEDURE pqnegaf(af: LIST):LIST;
(* negate atomic formula. af is a atomic formula. The negation of af is
returned. *)
VAR rel, pol: LIST;
BEGIN
pqpaf(af,rel,pol);
IF rel=EQU THEN RETURN pqmkaf(NEQ,pol);
ELSIF rel=NEQ THEN RETURN pqmkaf(EQU,pol);
ELSIF rel=GRE THEN RETURN pqmkaf(LSQ,pol);
ELSIF rel=LES THEN RETURN pqmkaf(GRQ,pol);
ELSIF rel=GRQ THEN RETURN pqmkaf(LES,pol);
ELSIF rel=LSQ THEN RETURN pqmkaf(GRE,pol);
ELSE ERROR(severe,"pqneqaf: unknown relation symbol in atomic formula.");
END;
END pqnegaf;
PROCEDURE pqsimplifyaf(af:LIST):LIST;
(* polynomial equation simplify atomic formula. af is an atomic formula.
af is simplified and af the result is returned. Only the relations between
a constant polynomial (and zero) are evaluated. Be careful: Use only
polynomials over an domain with a proper ADSIGN function.
(For example: RN, but not RF.) *)
VAR rel, lhs, cnst,z,sgn,dummy: LIST;
BEGIN
pqpaf(af,rel,lhs);
IF (lhs=0) AND ( (rel=EQU) OR (rel=LSQ) OR (rel=GRQ) ) THEN
RETURN VERUM;
ELSIF (lhs=0) AND ( (rel=NEQ) OR (rel=LES) OR (rel=GRE) ) THEN
RETURN FALSUM;
ELSIF DIPCNST(lhs) THEN
DIPMAD(lhs,cnst,z,dummy);
sgn:=ADSIGN(cnst);
IF sgn=-1 THEN
IF (rel=LES) OR (rel=LSQ) OR (rel=NEQ) THEN
RETURN VERUM;
ELSE
RETURN FALSUM;
END;
ELSIF sgn=0 THEN
IF (rel=EQU) OR (rel=LSQ) OR (rel=GRQ) THEN
RETURN VERUM;
ELSE
RETURN FALSUM;
END;
ELSIF sgn=1 THEN
IF (rel=GRE) OR (rel=GRQ) OR (rel=NEQ) THEN
RETURN VERUM;
ELSE
RETURN FALSUM;
END;
ELSE
ERROR(severe,"pqsimplifyaf: unknown ADSIGN value");
END;
ELSE
lhs:=DIPINORM(lhs,rel);
RETURN pqmkaf(rel,lhs);
END;
END pqsimplifyaf;
PROCEDURE DIPINORM(p: LIST; VAR rel:LIST):LIST;
(* distributive polynomial over integers normalize.
p is a distributive polynomial over domain DOMI.
The coefficients of the polynomial
are divided by the content of the polyomial p. The highest coefficient
is normalized to an positive number. The relation rel is adapted.*)
VAR content,ppt: LIST;
BEGIN
ADPCPP(p,content,ppt);
IF ADSIGN(content)=-1 THEN rel:=negrel(rel); END;
RETURN ppt;
END DIPINORM;
PROCEDURE negrel(rel: LIST):LIST;
BEGIN
IF rel=EQU THEN RETURN EQU;
ELSIF rel=NEQ THEN RETURN NEQ;
ELSIF rel=GRE THEN RETURN LES;
ELSIF rel=LES THEN RETURN GRE;
ELSIF rel=GRQ THEN RETURN LSQ;
ELSIF rel=LSQ THEN RETURN GRQ;
ELSE ERROR(severe,"negrel: unknown relation symbol in atomic formula.");
END;
END negrel;
PROCEDURE pqreadaf():LIST;
(* polynomial equation read atomic formula. An atomic formula is read from
the input stream. The global variable DOMAIN must be set.
Atomic fomulas have the following syntax: "<dip> <rel> <dip>",
where dip are distributive polynomials over an arbitrary domain
with the variable list VALIS and rel is one of the sympols
<,=,>,>=,<>,<=,#,LES,EQU,GRE,LSQ,NEQ,GRQ,LEQ,GEQ. *)
VAR c: GAMMAINT;
VAR lhs,rhs,rel,sym:LIST;
BEGIN
lhs:=DIREAD(VALIS,DOMAIN);
rel:=KEYREAD();
sym:=ASSOCQ(rel,BbfParserSyms);
IF sym=SIL THEN
DIBUFF();
ERROR(severe,"pqreadaf: unknown relation symbol.");
RETURN pqmkaf(EQU,lhs); (* dummy *)
ELSE
rel:=FIRST(sym);
END;
c:=CREADB();
IF c=MASORD("]") THEN (* for abbreviation only; not clean, but it is
correct. *)
BKSP();
rhs:=0;
ELSE
BKSP();
rhs:=DIREAD(VALIS,DOMAIN);
lhs:=DIPSUM(lhs,DIPNEG(rhs));
END;
RETURN pqmkaf(rel,lhs);
END pqreadaf;
PROCEDURE InitBbfParser();
(* Initialize black-box formula parser. *)
BEGIN
BbfParserSyms:=SIL;
LISTVAR(BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("<>"),NEQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("#"),NEQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("NEQ"),NEQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("="),EQU,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("!="),EQU,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("EQU"),EQU,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS(">"),GRE,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("GRE"),GRE,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("<"),LES,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("LES"),LES,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("<="),LSQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("LSQ"),LSQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("LEQ"),LSQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS(">="),GRQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("GRQ"),GRQ,BbfParserSyms);
BbfParserSyms:=COMP2(LISTS("GEQ"),GRQ,BbfParserSyms);
RETURN;
END InitBbfParser;
PROCEDURE pqsmart(phi:LIST):LIST;
(* polynomial equation atomic formula smart simplification.
phi is a conjunction or a disjunction over atomic formulas.
All atomic formulas with identical left hand sides are contracted to
one atomic formula. A conjunction or a disjunction over these contracted
formulas is returned. *)
VAR op,L,result: LIST;
BEGIN
FORPFOR(phi,op,L);
IF op=ET THEN
result:=ContractEt(L);
ELSIF op=VEL THEN
result:=ContractVel(L);
ELSE
BLINES(0);
UWRIT1(op);
ERROR(spotless,"pqsmart: operator symbol not valid.");
RETURN phi;
END;
IF (result=VERUM) OR (result=FALSUM) THEN
RETURN result;
ELSE
RETURN FORMKFOR(op,result);
END;
END pqsmart;
PROCEDURE ContractVel(l:LIST):LIST;
(* contract vel. l is a list of atomic formulas. These atomic formulas are
interpreted as arguments of a disjunction. The relations of atomic formulas
with equal left hand sides are contracted. A new list of atomic formulas
is returned. Every two atomic formulas in the returned list have differenet
left hand sides. For the returned list r the following
equivalent holds VEL(l) <=> VEL(r) *)
VAR mem, atom, rel, term, rels, fpoint, result: LIST;
BEGIN
mem:=SIL;
WHILE l<>SIL DO
ADV(l,atom,l);
pqpaf(atom,rel,term);
fpoint:=ASSOCQ(term,mem);
IF fpoint=SIL THEN
mem:=COMP2(term,rel,mem);
ELSE
rels:=FIRST(fpoint);
rels:=PQCRELOR(rels,rel);
SFIRST(fpoint,rels);
IF rels=VERUM THEN RETURN VERUM; END;
END;
END;
result:=SIL;
WHILE mem<>SIL DO
ADV2(mem,term,rel,mem);
result:=COMP(pqmkaf(rel,term),result)
END;
RETURN result;
END ContractVel;
PROCEDURE PQCRELOR(left,right:LIST):LIST;
(* contract relations or. left and right are relations or the
constants VERUM, FALSUM, the contraction of
left an right are returned. (this procedure works correct, even if left=SIL.)
*)
BEGIN
IF left=SIL THEN RETURN right;
ELSIF right=SIL THEN RETURN left;
ELSIF left=FALSUM THEN RETURN right;
ELSIF right=FALSUM THEN RETURN left;
ELSIF (left=VERUM) OR (right=VERUM) THEN RETURN VERUM;
ELSIF left=right THEN RETURN right;
END;
IF left=LES THEN
IF right=LSQ THEN RETURN LSQ;
ELSIF right=EQU THEN RETURN LSQ;
ELSIF right=NEQ THEN RETURN NEQ;
ELSIF right=GRQ THEN RETURN VERUM;
ELSIF right=GRE THEN RETURN NEQ;
ELSE ERROR(severe,"PQCRELOR: unknown relation symbol.");
END;
ELSIF left=LSQ THEN
IF right=LES THEN RETURN LSQ;
ELSIF right=EQU THEN RETURN LSQ;
ELSIF right=NEQ THEN RETURN VERUM;
ELSIF right=GRQ THEN RETURN VERUM;
ELSIF right=GRE THEN RETURN VERUM;
ELSE ERROR(severe,"PQCRELOR: unknown relation symbol.");
END;
ELSIF left=EQU THEN
IF right=LES THEN RETURN LSQ;
ELSIF right=LSQ THEN RETURN LSQ;
ELSIF right=NEQ THEN RETURN VERUM;
ELSIF right=GRQ THEN RETURN GRQ;
ELSIF right=GRE THEN RETURN GRQ;
ELSE ERROR(severe,"PQCRELOR: unknown relation symbol.");
END;
ELSIF left=NEQ THEN
IF right=LES THEN RETURN NEQ;
ELSIF right=LSQ THEN RETURN VERUM;
ELSIF right=EQU THEN RETURN VERUM;
ELSIF right=GRQ THEN RETURN VERUM;
ELSIF right=GRE THEN RETURN NEQ;
ELSE ERROR(severe,"PQCRELOR: unknown relation symbol.");
END;
ELSIF left=GRQ THEN
IF right=LES THEN RETURN VERUM;
ELSIF right=LSQ THEN RETURN VERUM;
ELSIF right=EQU THEN RETURN GRQ;
ELSIF right=NEQ THEN RETURN VERUM;
ELSIF right=GRE THEN RETURN GRQ;
ELSE ERROR(severe,"PQCRELOR: unknown relation symbol.");
END;
ELSIF left=GRE THEN
IF right=LES THEN RETURN NEQ;
ELSIF right=LSQ THEN RETURN VERUM;
ELSIF right=EQU THEN RETURN GRQ;
ELSIF right=NEQ THEN RETURN NEQ;
ELSIF right=GRQ THEN RETURN GRQ;
ELSE ERROR(severe,"PQCRELOR: unknown relation symbol.");
END;
ELSE
ERROR(severe,"PQCRELOR: unknown relation symbol.");
END;
END PQCRELOR;
PROCEDURE ContractEt(l:LIST):LIST;
(* contract vel. l is a list of atomic formulas. These atomic formulas are
interpreted
as arguments of a disjunction. The relations of atomic formulas with equal
identifiers are contracted. *)
VAR mem,atom,rel,term,rels,fpoint,result: LIST;
BEGIN
mem:=SIL;
WHILE l<>SIL DO
ADV(l,atom,l);
pqpaf(atom,rel,term);
fpoint:=ASSOCQ(term,mem);
IF fpoint=SIL THEN
mem:=COMP2(term,rel,mem);
ELSE
rels:=FIRST(fpoint);
rels:=PQCRELAND(rels,rel);
SFIRST(fpoint,rels);
IF rels=FALSUM THEN RETURN FALSUM; END;
END;
END;
result:=SIL;
WHILE mem<>SIL DO
ADV2(mem,term,rel,mem);
result:=COMP(pqmkaf(rel,term),result)
END;
RETURN result;
END ContractEt;
PROCEDURE PQCRELAND(left,right:LIST):LIST;
(* contract relations or. left and right are relations, the contraction of
left an right are returned. (this procedure works correct, even if left=SIL.)
*)
BEGIN
IF left=SIL THEN RETURN right; END;
IF left=right THEN RETURN right; END;
IF left=FALSUM THEN RETURN right; END;
IF left=LES THEN
IF right=LSQ THEN RETURN LES;
ELSIF right=EQU THEN RETURN FALSUM;
ELSIF right=NEQ THEN RETURN LES;
ELSIF right=GRQ THEN RETURN FALSUM;
ELSE (* right=GRE *) RETURN FALSUM;
END;
ELSIF left=LSQ THEN
IF right=LES THEN RETURN LES;
ELSIF right=EQU THEN RETURN EQU;
ELSIF right=NEQ THEN RETURN LES;
ELSIF right=GRQ THEN RETURN EQU;
ELSE (* right=GRE *) RETURN FALSUM;
END;
ELSIF left=EQU THEN
IF right=LES THEN RETURN FALSUM;
ELSIF right=LSQ THEN RETURN EQU;
ELSIF right=NEQ THEN RETURN FALSUM;
ELSIF right=GRQ THEN RETURN EQU;
ELSE (* right=GRE *) RETURN FALSUM;
END;
ELSIF left=NEQ THEN
IF right=LES THEN RETURN LES;
ELSIF right=LSQ THEN RETURN LES;
ELSIF right=EQU THEN RETURN FALSUM;
ELSIF right=GRQ THEN RETURN GRE;
ELSE (* right=GRE *) RETURN GRE;
END;
ELSIF left=GRQ THEN
IF right=LES THEN RETURN FALSUM;
ELSIF right=LSQ THEN RETURN EQU;
ELSIF right=EQU THEN RETURN EQU;
ELSIF right=NEQ THEN RETURN GRE;
ELSE (* right=GRE *) RETURN GRE;
END;
ELSE (* left=GRE *)
IF right=LES THEN RETURN FALSUM;
ELSIF right=LSQ THEN RETURN FALSUM;
ELSIF right=EQU THEN RETURN FALSUM;
ELSIF right=NEQ THEN RETURN GRE;
ELSE (* right=GRQ *) RETURN GRE;
END;
END;
END PQCRELAND;
(******************************************************************************
* U N I Q U E V A R I A B L E N A M E S *
******************************************************************************)
(******************************************************************************
In the following section we implement a procedure to generate unique names
of variables. This procedure is necessary to transform arbitrary
formulas in prenex normal form. The basic procedure is implemented
in the MASLOG module. But there is a serious problem to apply this
procedure for the PQ-system. We use distributive polynomials of the
DIP polynomiall system to represent
terms. But duriong the generation of unique names, we must introduce
new variables. The DIP sytsem uses exponent vectors with a positional
correspondence to the variables. Each exponent vector in each polynomial
of the formula must have the same length. So you cannot introduce trivially
a new variable. For a solving of this problem we introduce temporary a new
representation of atomic formulas. These representation has the following
form:
(PQSAF Substitutions AtomicFormula)
PQSAF is a MAS symbol to mark the special form of atomic formulas.
Substitutions is a list of lists with two atoms.
Atomic formula is a normal atomic formula of the PQ-system.
Each pair (o,n) of the list Substitutions has the meaning
move a exponent form position l-o+1 to position l-n+1, where l=LENGTH(VALIS).
The list of substitution must be applied in inverse order of their
occurence in the list Substitutions.
As variable names, we uses the names from VALIS.
The procedure works as follows:
1. Declare all variables from VALIS as maslog variables.
2. Call FORMKVD
3. Transform the special representation of the returned formula in standard
representation.
We use a global variable NewVariables to count the number of new introduced
variables.
******************************************************************************)
PROCEDURE EnterVariableNames(valis: LIST);
(* enter variable names. valis is a variable list. All names from valis
are entered in the MASLOG symbol table. *)
VAR var,dummy: LIST;
BEGIN
WHILE valis<>SIL DO
ADV(valis, var,valis);
dummy:=FORVTENTER(var);
END;
END EnterVariableNames;
PROCEDURE pqlsvars(af: LIST):LIST;
(* polynomial equation list variables. af is a atomic formula.
All variables used in af is returned as a list of MASLOG variables. *)
VAR rel, pol, var, result, valis, vv, v: LIST;
BEGIN
pol:=pqgpol(af);
IF pol=0 THEN RETURN SIL; END;
result:=SIL;
vv:=INV(DIPMVV(pol)); (* valis has the inverted order of ev *)
valis:=VALIS;
WHILE vv<>SIL DO
ADV(vv, v,vv);
ADV(valis, var,valis);
IF v=1 THEN
result:=COMP(FORMKVAR(FORVTENTER(var),ANY),result);
END;
END;
RETURN result;
END pqlsvars;
PROCEDURE PqsafSubstvar(af,old,new:LIST):LIST;
(* polynomial equation special atomic formula substitute variable.
phi is an atomic formula.
old and new are variables. The variable old is substituted with new in af.
VALIS is modified!!!! *)
VAR oIndex, nIndex,name,type,n: LIST;
BEGIN
FORPVAR(old, name,type);
oIndex:=LSRCHQ(FORVTGET(name),VALIS);
FORPVAR(new, name,type);
nIndex:=LSRCHQ(FORVTGET(name),VALIS);
IF nIndex=0 THEN
NewVariables:=NewVariables+1;
VALIS:=SUFFIX(VALIS,FORVTGET(name));
nIndex:=LENGTH(VALIS);
END;
IF FORGOP(af)<>PQSAF THEN
RETURN LIST3(PQSAF,LIST1(LIST2(oIndex,nIndex)),af);
ELSE
RETURN LIST3(PQSAF,COMP(LIST2(oIndex,nIndex),SECOND(af)),
THIRD(af));
END;
END PqsafSubstvar;
PROCEDURE PqsafNormalizeAf(af:LIST):LIST;
(* polynomial equation special atomic formula normalize atomic formula.
af is atomic formula is special representation. The normalized representation
is returned. *)
VAR op, pol, rel, subst,s, o,n,i,length,perm :LIST;
BEGIN
(* *) (* Initialization *)
op:=FORGOP(af);
IF (op=VERUM) OR (op=FALSUM) THEN RETURN af; END;
IF (op<>PQSAF) AND (NewVariables=0) THEN RETURN af; END;
IF op=PQSAF THEN
pqpaf(THIRD(af), rel,pol);
subst:=SECOND(af);
ELSE
pqpaf(af, rel,pol);
subst:=SIL;
END;
(* *) (* introduce new variables *)
length:=LENGTH(VALIS);
IF NewVariables>0 THEN
pol:=DIPINV(pol,length-NewVariables+1,NewVariables);
END;
(* *) (* generate permutation vector from substitution list *)
perm:=SIL;
FOR i:=length TO 1 BY -1 DO
perm:=COMP(i,perm);
END;
WHILE subst<>SIL DO
ADV(subst, s,subst);
FIRST2(s, o,n);
SLELT(perm,n,o);
SLELT(perm,o,n);
END;
(* *) (* permute polynomial *)
pol:=DIPERM(pol,perm);
RETURN pqmkaf(rel,pol);
END PqsafNormalizeAf;
PROCEDURE PQMKVD(phi:LIST): LIST;
(* polynomial equation make variable names disjoint. *)
VAR psi: LIST;
BEGIN
NewVariables:=0;
EnterVariableNames(VALIS);
psi:=FORMKVD(phi,PqsafSubstvar,pqlsvars);
psi:=FORAPPLYAT(psi,PqsafNormalizeAf);
RETURN psi;
END PQMKVD;
PROCEDURE vlistflvar(lvar:LIST):LIST;
(* variable list from lvar. lvar is a LVAR object. A variable list in the
format of the module DIPC representing the same list of
variables is returned. *)
VAR result, var, name,sort: LIST;
BEGIN
lvar:=FORGLVAR(lvar);
result:=SIL;
WHILE lvar<>SIL DO
ADV(lvar, var,lvar);
FORPVAR(var,name,sort);
result:=COMP(FORVTGET(name),result);
END;
RETURN INV(result);
END vlistflvar;
PROCEDURE lvarfvlist(vlist:LIST):LIST;
(* lvar from variable list. vlist is a variable list in the format of the
DIPC-module. A LVAR object representing the same variable list is returned. *)
VAR result,v: LIST;
BEGIN
result:=SIL;
WHILE vlist<>SIL DO
ADV(vlist, v,vlist);
result:=COMP(FORMKVAR(FORVTENTER(v),ANY),result);
END;
RETURN FORMKLVAR(INV(result));
END lvarfvlist;
(******************************************************************************
* M A S L O G I N T E R F A C E *
******************************************************************************)
PROCEDURE PQMKDNF(phi:LIST):LIST;
(* polynomial equation make disjunctive normal form. phi is a formula;
MLMKDNF returns a formula in strict disjunctive normal form which is
equivalent to phi. *)
BEGIN
RETURN FORMKDNF(phi,pqnegaf);
END PQMKDNF;
PROCEDURE PQMKCNF(phi:LIST):LIST;
(* polynomial equation make disjunctive normal form. phi is a formula;
a formula in strict conjunctive normal form which is
equivalent to phi is returned. *)
BEGIN
RETURN FORMKCNF(phi,pqnegaf);
END PQMKCNF;
PROCEDURE PQSMPL(phi:LIST):LIST;
(* polynomial equation simplify. phi is a formula; a simplification on
phi is returned. *)
BEGIN
RETURN FORSMPL(phi,pqsimplifyaf,pqnegaf);
END PQSMPL;
PROCEDURE PQSIMPLIFY(phi:LIST):LIST;
(* polynomial equation simplify. phi is a formula. A simplification of
phi is returned. Following simplification steps are done:
1. VERUM and FALSUM are eliminated
2. assoziative simplification
3. idempotenz
*)
BEGIN
RETURN FORSIMPLIFY(phi,pqsmart,pqsimplifyaf,pqnegaf);
END PQSIMPLIFY;
PROCEDURE PQSIMPLIFYP(phi,maxlevel:LIST):LIST;
(* polynomial equation simplify. phi is a formula. A simplification of
phi is returned. Following simplification steps are done:
1. VERUM and FALSUM are eliminated
2. assoziative simplification
3. idempotenz
maxlevel is the number of levels that are simplified.
*)
BEGIN
RETURN FORSIMPLIFYP(phi,maxlevel,pqsmart,pqsimplifyaf,pqnegaf);
END PQSIMPLIFYP;
PROCEDURE PQMKPOS(phi: LIST): LIST;
(* polynomial equation make positive. phi is a formula; a equivalent positive
formula is returned. *)
BEGIN
RETURN FORMKPOS(phi,ET,pqnegaf);
END PQMKPOS;
PROCEDURE PQPPRT(phi:LIST);
(* polynomial equation pretty print. phi is a formula; this procedure writes
the formula phi formatted in the output stream. *)
BEGIN
FORPPRT(phi,pqprtaf);
END PQPPRT;
PROCEDURE PQTEXW(phi: LIST);
(* polynomial equation tex write. The formula phi is printed in tex format in
the output stream. *)
BEGIN
FORTEXW(phi,pqtexwaf);
END PQTEXW;
PROCEDURE PQPREAD():LIST;
(* polynomial equation read. *)
BEGIN
RETURN FORPREAD(pqreadaf);
END PQPREAD;
PROCEDURE PQIREAD():LIST;
(* polynomial equation infix read. *)
VAR c: GAMMAINT;
VAR keyword, value: LIST;
BEGIN
c:=CREADB();
IF c <> MASORD("{") THEN
BKSP();
ELSE
REPEAT
keyword:=SREAD1();
c:=CREADB();
IF c<>MASORD("=") THEN
DIBUFF();
ERROR(severe,"PQIREAD: = expected");
END;
IF EQUAL(keyword,LISTS("DOMAIN"))=1 THEN
DOMAIN:=ADDDREAD();
ELSIF EQUAL(keyword,LISTS("VALIS"))=1 THEN
VALIS:=VLREAD();
ELSIF EQUAL(keyword,LISTS("EVORD"))=1 THEN
EVORD:=UREAD();
END;
c:=CREADB();
IF (c<>MASORD(",")) AND (c<>MASORD("}")) THEN
DIBUFF();
ERROR(severe,"PQIREAD: , or = expected");
END;
UNTIL c=MASORD("}");
BLINES(1);
SWRITE("DOMAIN: ");ADDDWRIT(DOMAIN);BLINES(0);
SWRITE("VALIS: ");VLWRIT(VALIS);BLINES(0);
SWRITE("EVORD: ");UWRITE(EVORD);BLINES(1);
END;
RETURN FORIREAD(pqreadaf);
END PQIREAD;
PROCEDURE PQELIMXOPS(phi: LIST):LIST;
(* polynomial equation eliminate extended operation symbols. phi is
formula, pref is a
symbol of the set \{VEL, ET, NON\}; FORELIMXOPS returns a formula phi1
equivalent to phi. If pref is NON then this function does nothing. Otherwise
this function replaces all subterms of phi with the operators IMP, REP, EQUIV
or XOR with terms with the operators VEL, ET and NON. There are two different
substitutions for EQUIV and XOR. If pref=ET (pref=VEL) then the outermost
operator of the replacement terms for EQUIV, XOR is ET (VEL). *)
BEGIN
RETURN FORELIMXOPS(phi,ET); (* -- to do -- set preference *)
END PQELIMXOPS;
PROCEDURE PQELIMXOPS1(phi,pref: LIST):LIST;
(* polynomial equation eliminate extended operation symbols. phi is
formula, pref is a
symbol of the set \{VEL, ET, NON\}; FORELIMXOPS returns a formula phi1
equivalent to phi. If pref is NON then this function does nothing. Otherwise
this function replaces all subterms of phi with the operators IMP, REP, EQUIV
or XOR with terms with the operators VEL, ET and NON. There are two different
substitutions for EQUIV and XOR. If pref=ET (pref=VEL) then the outermost
operator of the replacement terms for EQUIV, XOR is ET (VEL). *)
BEGIN
RETURN FORELIMXOPS(phi,pref); (* -- to do -- set preference *)
END PQELIMXOPS1;
PROCEDURE PQMKPRENEX(phi,pref:LIST): LIST;
(* polynomial equation make prenex.
phi is a formula; pref is an element of \{EXIST,
FORALL\}; a formula psi in prenex normal form is returned. phi must be a
relative positive formula without additional operation symbols like IMP, REP,
etc. All bound variables in phi must have different specifications (i.e.
different names or different types). The only transformation which is used to
calculate psi is the interchange of a junctor with a quantifier. The formula
psi has the minimal number of blocks of quantifiers under all prenex formulas
which are built using only the interchange of a junctor with a quantifier.
The argument pref is only respected, if there are two equivalent formulas with
the same optimal number of blocks of quantifiers. In this case the formula is
returned which has a "pref"-quantifier as the outermost operation symbol.*)
BEGIN
RETURN FORMKPRENEX(phi,pref);
END PQMKPRENEX;
(******************************************************************************
* P R I N G *
******************************************************************************)
PROCEDURE PQPRING(R: LIST): LIST;
(* polynomial equation polynomial ring. The global variables that describe the
polynomial ring are set. The list R is of the following format: The first entry
is the domain descriptor of the field, the second entry is the list of the
variables, and the third entry is the term order. You can omit an entry of R
by writing a -1 on the place of the entry. Not all entries must specified.
The old parameters are returned. *)
VAR old: LIST;
BEGIN
old:=LIST3(DOMAIN,VALIS,EVORD);
IF R<>SIL THEN
IF FIRST(R)<>-1 THEN ADV(R,DOMAIN,R); ELSE R:=RED(R); END;
END;
IF R<>SIL THEN
IF FIRST(R)<>-1 THEN ADV(R,VALIS,R); ELSE R:=RED(R); END;
END;
IF R<>SIL THEN
IF FIRST(R)<>-1 THEN ADV(R,EVORD,R); ELSE R:=RED(R); END;
END;
RETURN old;
END PQPRING;
PROCEDURE PQPRINGWR();
(* polynomial equation polynomial ring write. The description of the polynomial
ring is written in the output stream. *)
VAR variable,varlist: LIST;
BEGIN
BLINES(1);
SWRITE("Specification of the polynomial ring:");
BLINES(0);
SWRITE(" The domain: "); ADDDWRIT(DOMAIN);BLINES(0);
IF VALIS=SIL THEN
SWRITE("No list of variables specified!");
ELSE
SWRITE(" The list of variables: ");
VLWRIT(VALIS);
END;
BLINES(0);
SWRITE(" The term order of the polynomial ring: ");
IF EVORD>SIL THEN
SWRITE("user defined term order:");
UWRIT1(EVORD);
ELSE
CASE INTEGER(EVORD) OF
LEX: SWRITE("LEX"); |
INVLEX: SWRITE("INVLEX"); |
GRLEX: SWRITE("GRLEX"); |
IGRLEX: SWRITE("IGRLEX"); |
REVLEX: SWRITE("REVLEX"); |
REVILEX: SWRITE("REVILEX"); |
REVTDEG: SWRITE("REVTDEG"); |
REVITDG: SWRITE("REVITDG");
ELSE SWRITE("WARNING: unknown term order indicator.");
END;
END;
BLINES(1);
END PQPRINGWR;
(******************************************************************************
* M A I N *
******************************************************************************)
BEGIN
(* *** symbols for bb-formulas *** *)
Declare(EQU,"EQU");
Declare(NEQ,"NEQ");
Declare(LES,"LES");
Declare(LSQ,"LSQ");
Declare(GRQ,"GRQ");
Declare(GRE,"GRE");
Declare(PQSAF,"PQSAF");
(* *** listvar declarations for global variables. *** *)
LISTVAR(DOMAIN);
(* *** initialize the bb-formula parser. *** *)
InitBbfParser();
(* *** initialize the global variables. *** *)
(* DOMAIN:=LIST3(DOMRND,0,-1); (* RN -1 *) *)
(* last line does not work. It is executed before domain RN loaded *)
DOMAIN:=LIST3(8,0,-1); (* RN -1 *)
END PQBASE.
(* -EOF- *)