public class MultiplesModEquationsGenerator extends java.lang.Object implements TermGenerator
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.Modifier and Type | Class and Description |
---|---|
private static class |
MultiplesModEquationsGenerator.CofactorItem |
private static class |
MultiplesModEquationsGenerator.CofactorMonomial |
private static class |
MultiplesModEquationsGenerator.CofactorPolynomial |
Modifier and Type | Field and Description |
---|---|
private ProjectionToTerm |
source |
private ProjectionToTerm |
target |
Modifier | Constructor and Description |
---|---|
private |
MultiplesModEquationsGenerator(ProjectionToTerm source,
ProjectionToTerm target) |
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
Polynomial s. |
java.util.Iterator<Term> |
generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
private java.util.Iterator<Term> |
toIterator(Term quotient) |
private final ProjectionToTerm source
private final ProjectionToTerm target
private MultiplesModEquationsGenerator(ProjectionToTerm source, ProjectionToTerm target)
public static TermGenerator create(ProjectionToTerm source, ProjectionToTerm target)
public java.util.Iterator<Term> generate(RuleApp app, PosInOccurrence pos, Goal goal)
generate
in interface TermGenerator
private ImmutableList<Term> computeMultiples(Monomial sourceM, Monomial targetM, java.util.List<MultiplesModEquationsGenerator.CofactorPolynomial> cofactorPolys, Services services)
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
.private ImmutableList<Term> addRes(MultiplesModEquationsGenerator.CofactorMonomial newMono, Monomial sourceM, ImmutableList<Term> res, Services services)
private java.util.List<MultiplesModEquationsGenerator.CofactorPolynomial> extractPolys(Goal goal, Services services)
Polynomial
s.