de.uka.ilkd.key.strategy.termgenerator

Class MultiplesModEquationsGenerator

java.lang.Object

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

All Implemented Interfaces:

TermGenerator

public class MultiplesModEquationsGenerator
extends java.lang.Object
implements TermGenerator

Try to rewrite a monomial (term) source so that it becomes a multiple of another monomial target, using the integer equations of the antecedent. The output of the term generator is a list of polynomials x such that x * target = source (modulo ...). This is done using the method introduced in "Automating elementary number-theoretic proofs using Groebner bases", 2007, John Harrison. Compared to the paper, we only perform a simplified Groebner basis computation, basically only consisting of reduction steps with polynomials that have a single monomial. This is already enough to handle many practical cases and to significantly improve polynomial division modulo equations. In the future, this class should also be used for instantiating explicit quantifiers over the integers.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	MultiplesModEquationsGenerator.CofactorItem
private static class	MultiplesModEquationsGenerator.CofactorMonomial
private static class	MultiplesModEquationsGenerator.CofactorPolynomial

Field Summary

Fields

Modifier and Type	Field and Description
private ProjectionToTerm	source
private ProjectionToTerm	target

Constructor Summary

Constructors

Modifier	Constructor and Description
private	MultiplesModEquationsGenerator(ProjectionToTerm source, ProjectionToTerm target)

Method Summary

Modifier and Type	Method and Description
private ImmutableList<Term>	addRes(MultiplesModEquationsGenerator.CofactorMonomial newMono, Monomial sourceM, ImmutableList<Term> res, Services services)
private ImmutableList<Term>	computeMultiples(Monomial sourceM, Monomial targetM, java.util.List<MultiplesModEquationsGenerator.CofactorPolynomial> cofactorPolys, Services services) Compute multiples of targetM that are congruent to sourceM modulo the polynomials in cofactorPolys.
static TermGenerator	create(ProjectionToTerm source, ProjectionToTerm target)
private java.util.List<MultiplesModEquationsGenerator.CofactorPolynomial>	extractPolys(Goal goal, Services services) Extract all integer equations of the antecedent and convert them into Polynomials.
java.util.Iterator<Term>	generate(RuleApp app, PosInOccurrence pos, Goal goal)
private java.util.Iterator<Term>	toIterator(Term quotient)

Methods inherited from class java.lang.Object

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

Field Detail

source

private final ProjectionToTerm source

target

private final ProjectionToTerm target

Constructor Detail

MultiplesModEquationsGenerator

private MultiplesModEquationsGenerator(ProjectionToTerm source,
                                       ProjectionToTerm target)

Method Detail

create

public static TermGenerator create(ProjectionToTerm source,
                                   ProjectionToTerm target)

generate

public java.util.Iterator<Term> generate(RuleApp app,
                                         PosInOccurrence pos,
                                         Goal goal)

Specified by:

generate in interface TermGenerator

toIterator

private java.util.Iterator<Term> toIterator(Term quotient)

computeMultiples

private ImmutableList<Term> computeMultiples(Monomial sourceM,
                                             Monomial targetM,
                                             java.util.List<MultiplesModEquationsGenerator.CofactorPolynomial> cofactorPolys,
                                             Services services)

Compute multiples of targetM that are congruent to sourceM modulo the polynomials in cofactorPolys. The result is a list of terms x with the property x * targetM = sourceM (modulo ...). This method will change the object cofactorPolys.

addRes

private ImmutableList<Term> addRes(MultiplesModEquationsGenerator.CofactorMonomial newMono,
                                   Monomial sourceM,
                                   ImmutableList<Term> res,
                                   Services services)

extractPolys

private java.util.List<MultiplesModEquationsGenerator.CofactorPolynomial> extractPolys(Goal goal,
                                                                                       Services services)

Extract all integer equations of the antecedent and convert them into Polynomials.