de.uka.ilkd.key.strategy.termgenerator

Class MultiplesModEquationsGenerator.CofactorPolynomial

java.lang.Object

de.uka.ilkd.key.strategy.termgenerator.MultiplesModEquationsGenerator.CofactorItem

de.uka.ilkd.key.strategy.termgenerator.MultiplesModEquationsGenerator.CofactorPolynomial

Enclosing class:

MultiplesModEquationsGenerator

private static class MultiplesModEquationsGenerator.CofactorPolynomial
extends MultiplesModEquationsGenerator.CofactorItem

Field Summary

Fields

Modifier and Type	Field and Description
Polynomial	poly

Fields inherited from class de.uka.ilkd.key.strategy.termgenerator.MultiplesModEquationsGenerator.CofactorItem

cofactor

Constructor Summary

Constructors

Constructor and Description
CofactorPolynomial(Polynomial poly, Polynomial cofactor)

Method Summary

Modifier and Type	Method and Description
MultiplesModEquationsGenerator.CofactorPolynomial	add(MultiplesModEquationsGenerator.CofactorMonomial mono, Monomial coeff) Add coeff times mono to this polynomial, adjusting the cofactor accordingly
MultiplesModEquationsGenerator.CofactorItem	reduce(MultiplesModEquationsGenerator.CofactorMonomial mono) Reduce the polynomial by adding a multiple of the monomial mono.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

poly

public final Polynomial poly

Constructor Detail

CofactorPolynomial

public CofactorPolynomial(Polynomial poly,
                          Polynomial cofactor)

Method Detail

add

public MultiplesModEquationsGenerator.CofactorPolynomial add(MultiplesModEquationsGenerator.CofactorMonomial mono,
                                                             Monomial coeff)

Add coeff times mono to this polynomial, adjusting the cofactor accordingly

reduce

public MultiplesModEquationsGenerator.CofactorItem reduce(MultiplesModEquationsGenerator.CofactorMonomial mono)

Reduce the polynomial by adding a multiple of the monomial mono. The result is either CofactorPolynomial or CofactorMonomial, depending on whether the resulting polynomial has one or multiple monomials