001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.strategy.quantifierHeuristics;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
017: import de.uka.ilkd.key.logic.op.Op;
018: import de.uka.ilkd.key.logic.op.Operator;
019: import de.uka.ilkd.key.proof.Goal;
020: import de.uka.ilkd.key.rule.TacletApp;
021: import de.uka.ilkd.key.strategy.feature.Feature;
022: import de.uka.ilkd.key.strategy.feature.SmallerThanFeature;
023: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
024:
025: /**
026: * Ordering used to sort the clauses in a quantified formula. This ordering
027: * should only be applied if at least one of the two clauses contains more than
028: * one literal (otherwise, use <code>LiteralsSmallerThanFeature</code>).
029: */
030: public class ClausesSmallerThanFeature extends SmallerThanFeature {
031:
032: private final ProjectionToTerm left, right;
033:
034: private final QuanEliminationAnalyser quanAnalyser = new QuanEliminationAnalyser();
035:
036: // ugly
037: private PosInOccurrence focus = null;
038: private Services services = null;
039:
040: private final LiteralsSmallerThanFeature litComparator;
041:
042: private ClausesSmallerThanFeature(ProjectionToTerm left,
043: ProjectionToTerm right, IntegerLDT numbers) {
044: this .left = left;
045: this .right = right;
046: this .litComparator = (LiteralsSmallerThanFeature) LiteralsSmallerThanFeature
047: .create(left, right, numbers);
048: }
049:
050: public static Feature create(ProjectionToTerm left,
051: ProjectionToTerm right, IntegerLDT numbers) {
052: return new ClausesSmallerThanFeature(left, right, numbers);
053: }
054:
055: protected boolean filter(TacletApp app, PosInOccurrence pos,
056: Goal goal) {
057: final Term leftTerm = left.toTerm(app, pos, goal);
058: final Term rightTerm = right.toTerm(app, pos, goal);
059:
060: focus = pos;
061: services = goal.proof().getServices();
062:
063: final ClauseCollector m1 = new ClauseCollector();
064: m1.collect(leftTerm);
065: final ClauseCollector m2 = new ClauseCollector();
066: m2.collect(rightTerm);
067:
068: final boolean res = lessThan(m1.getResult(), m2.getResult());
069:
070: focus = null;
071: services = null;
072:
073: return res;
074: }
075:
076: /**
077: * this overwrites the method of <code>SmallerThanFeature</code>
078: */
079: protected boolean lessThan(Term t1, Term t2) {
080:
081: final int t1Def = quanAnalyser.eliminableDefinition(t1, focus);
082: final int t2Def = quanAnalyser.eliminableDefinition(t2, focus);
083:
084: if (t1Def > t2Def)
085: return true;
086: if (t1Def < t2Def)
087: return false;
088:
089: if (t1.op() == Op.OR) {
090: if (t2.op() == Op.OR) {
091: return super .lessThan(t1, t2);
092: } else {
093: return false;
094: }
095: } else {
096: if (t2.op() == Op.OR) {
097: return true;
098: } else {
099: return litComparator.compareTerms(t1, t2, focus,
100: services);
101: }
102: }
103: }
104:
105: private class ClauseCollector extends Collector {
106: protected void collect(Term te) {
107: final Operator op = te.op();
108: if (op == Op.AND) {
109: collect(te.sub(0));
110: collect(te.sub(1));
111: } else {
112: addTerm(te);
113: }
114: }
115: }
116:
117: }
|