01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.strategy.feature;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.proof.Goal;
16: import de.uka.ilkd.key.rule.TacletApp;
17: import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
18: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
19:
20: /**
21: * Return zero of the least common reducible of two monomials is so trivial that
22: * it is not necessary to do the critical pair completion
23: *
24: * "A critical-pair/completion algorithm for finitely generated ideals in rings"
25: */
26: public class TrivialMonomialLCRFeature extends BinaryTacletAppFeature {
27: private final ProjectionToTerm a, b;
28:
29: private TrivialMonomialLCRFeature(ProjectionToTerm a,
30: ProjectionToTerm b) {
31: this .a = a;
32: this .b = b;
33: }
34:
35: public static Feature create(ProjectionToTerm a, ProjectionToTerm b) {
36: return new TrivialMonomialLCRFeature(a, b);
37: }
38:
39: protected boolean filter(TacletApp app, PosInOccurrence pos,
40: Goal goal) {
41: final Services services = goal.proof().getServices();
42: final Monomial aMon = Monomial.create(a.toTerm(app, pos, goal),
43: services);
44: final Monomial bMon = Monomial.create(b.toTerm(app, pos, goal),
45: services);
46:
47: /* final BigInteger ac = aMon.getCoefficient ();
48: final BigInteger bc = bMon.getCoefficient ();
49:
50: if ( ac.mod ( bc ).signum () != 0 && bc.mod ( ac ).signum () != 0 )
51: return false; */
52:
53: return aMon.variablesAreCoprime(bMon);
54: }
55: }
|