(* ---------------------------------------------------------------------------- * $Id: PQBASE.md,v 1.1 1994/11/28 21:10:01 dolzmann Exp $ * ---------------------------------------------------------------------------- * Copyright (c) 1994 Universitaet Passau * ---------------------------------------------------------------------------- * This file is part of MAS. * ---------------------------------------------------------------------------- * $Log: PQBASE.md,v $ * Revision 1.1 1994/11/28 21:10:01 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. * * ---------------------------------------------------------------------------- *) DEFINITION 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 MASSTOR IMPORT LIST;CONSTrcsid = "$Id: PQBASE.md,v 1.1 1994/11/28 21:10:01 dolzmann Exp $";CONSTcopyright = "Copyright (c) 1994 Universitaet Passau"; (****************************************************************************** * G L O B A L V A R I A B L E S * ******************************************************************************)VAREQU, NEQ, GRE, LES, GRQ, LSQ: LIST; (* Relations =, #, >, <, >=, <= *)VARPQSAF: LIST ; (* symbol to mark a polynomial equation special atomic formula *)VARDOMAIN: LIST;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. *)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. *)PROCEDURE pqmkaf(rel:LIST;pol:LIST):LIST; (* polynomial equation simplification make atomic formula. rel is a relation, pol is a polynomial, the atomic formula (rel,id) is returned. *)PROCEDURE pqpaf(af:LIST;VARrel,pol:LIST); (* polynomial equation simplification 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. *)PROCEDURE pqgrel(af:LIST):LIST; (* polynomial equation get relation symbol. af is an atomic formula. The relation symbol of af is returned. *)PROCEDURE pqgpol(af:LIST):LIST; (* polynomial equation get polynomial. af is an atomic formula. The polynomial of af is returned. *)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. *)PROCEDURE pqprtaf(af: LIST); (* polynomial equation simplification print atomic formula. The atomic formula af is printed. *)PROCEDURE pqtexwaf(af: LIST); (* polynomia equation tex write atomic formula. The atomic formula af is written to the output stream. *)PROCEDURE pqnegaf(af: LIST):LIST; (* negate atomic formula. af is a atomic formula. The negation of af is returned. *)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.) *)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: "<dilp> <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. *)PROCEDURE InitBbfParser(); (* Initialize black-box formula parser. *)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 contraced formulas is returned. *)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. *)PROCEDURE PQCRELOR(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.) *)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. *)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.) *) (****************************************************************************** * 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. *)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. *)PROCEDURE PQSMPL(phi:LIST):LIST; (* polynomial equation simplify. phi is a formula; a simplification on phi is returned. *)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 *)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. *)PROCEDURE PQMKPOS(phi: LIST): LIST; (* polynomial equation make positive. phi is a formula; a equivalent positive formula is returned. *)PROCEDURE PQPPRT(phi:LIST); (* polynomial equation pretty print. phi is a formula; this procedure writes the formula phi formatted in the output stream. *)PROCEDURE PQTEXW(phi: LIST); (* polynomial equation tex write. The formula phi is printed in tex format in the output stream. *)PROCEDURE PQPREAD():LIST; (* polynomial equation read. *)PROCEDURE PQIREAD():LIST; (* polynomial equation infix read. *)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). *)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). *)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.*) (****************************************************************************** * 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. *)PROCEDURE PQPRINGWR(); (* polynomial equation polynomial ring write. The description of the polynomial ring is written in the output stream. *)PROCEDURE PQMKVD(phi:LIST): LIST; (* polynomial equation make variable names disjoint. *)ENDPQBASE. (* -EOF- *)