de.uka.ilkd.key.rule.metaconstruct.arith

Class Monomial

java.lang.Object

de.uka.ilkd.key.rule.metaconstruct.arith.Monomial

public class Monomial
extends java.lang.Object

Class for analysing and modifying monomial expressions over the integers

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	Monomial.Analyser

Field Summary

Fields

Modifier and Type	Field and Description
private java.math.BigInteger	coefficient
static Monomial	ONE
private ImmutableList<Term>	parts

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Monomial(ImmutableList<Term> parts, java.math.BigInteger coefficient)

Method Summary

Modifier and Type	Method and Description
Monomial	addToCoefficient(java.math.BigInteger c)
private java.math.BigInteger	cofactor(java.math.BigInteger v0, java.math.BigInteger v1) Extended euclidian algorithm for computing cofactors.
static Monomial	create(Term monoTerm, Services services)
private static Monomial	createHelp(Term monomial, Services services)
private static ImmutableList<Term>	difference(ImmutableList<Term> a, ImmutableList<Term> b)
Monomial	divideLCR(Monomial m)
boolean	divides(Monomial m)
boolean	equals(java.lang.Object o)
java.math.BigInteger	getCoefficient()
ImmutableList<Term>	getParts()
int	hashCode()
Monomial	multiply(java.math.BigInteger c)
Monomial	multiply(Monomial m)
Monomial	reduce(Monomial m)
boolean	reducible(Monomial m)
Monomial	setCoefficient(java.math.BigInteger c)
java.lang.String	toString()
Term	toTerm(Services services)
boolean	variablesAreCoprime(Monomial m)
boolean	variablesDisjoint(Monomial m)
boolean	variablesEqual(Monomial m)
boolean	variablesSubsume(Monomial m)

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

parts

private final ImmutableList<Term> parts

coefficient

private final java.math.BigInteger coefficient

ONE

public static final Monomial ONE

Constructor Detail

Monomial

private Monomial(ImmutableList<Term> parts,
                 java.math.BigInteger coefficient)

Method Detail

create

public static Monomial create(Term monoTerm,
                              Services services)

createHelp

private static Monomial createHelp(Term monomial,
                                   Services services)

setCoefficient

public Monomial setCoefficient(java.math.BigInteger c)

multiply

public Monomial multiply(java.math.BigInteger c)

multiply

public Monomial multiply(Monomial m)

addToCoefficient

public Monomial addToCoefficient(java.math.BigInteger c)

divides

public boolean divides(Monomial m)

Returns:

true iff the monomial this divides the monomial m

variablesSubsume

public boolean variablesSubsume(Monomial m)

Returns:

true iff the variables/parts of this subsume the variables of m, i.e., if each variable that occurs in m occurs in the same or a higher power in this

variablesEqual

public boolean variablesEqual(Monomial m)

variablesDisjoint

public boolean variablesDisjoint(Monomial m)

reducible

public boolean reducible(Monomial m)

Returns:

true iff the coefficient of m can be made smaller (absolutely) by subtracting a multiple of this

reduce

public Monomial reduce(Monomial m)

Returns:

the result of dividing the monomial m by the monomial this

divideLCR

public Monomial divideLCR(Monomial m)

Returns:

the result of dividing the least common reducible (LCR) of monomial m and this by the monomial this

cofactor

private java.math.BigInteger cofactor(java.math.BigInteger v0,
                                      java.math.BigInteger v1)

Extended euclidian algorithm for computing cofactors. This satisfies the equation gcd(a,b)=a*cofactor(a,b)+b*cofactor(b,a)

toTerm

public Term toTerm(Services services)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

difference

private static ImmutableList<Term> difference(ImmutableList<Term> a,
                                              ImmutableList<Term> b)

Returns:

the list of all terms that occur in a but not in b. multiplicity is treated as well here, so this is really difference of multisets

getCoefficient

public java.math.BigInteger getCoefficient()

getParts

public ImmutableList<Term> getParts()

variablesAreCoprime

public boolean variablesAreCoprime(Monomial m)