| java.lang.Object
 de.uka.ilkd.key.strategy.termgenerator.MultiplesModEquationsGenerator
| MultiplesModEquationsGenerator | | public class MultiplesModEquationsGenerator implements TermGenerator(Code) | | 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.
|
|
|