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.pp;
012:
013: import de.uka.ilkd.key.logic.ConstrainedFormula;
014: import de.uka.ilkd.key.logic.Constraint;
015: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
016: import de.uka.ilkd.key.logic.Sequent;
017:
018: /**
019: * Select the formulas of the sequent that should be printed, using
020: * the user constraint
021: */
022:
023: public class ConstraintSequentPrintFilter implements SequentPrintFilter {
024:
025: protected Sequent originalSequent;
026:
027: protected Constraint userConstraint;
028:
029: protected ListOfSequentPrintFilterEntry antec = null;
030: protected ListOfSequentPrintFilterEntry succ = null;
031:
032: public ConstraintSequentPrintFilter(Sequent p_s,
033: Constraint p_userConstraint) {
034: originalSequent = p_s;
035: userConstraint = p_userConstraint;
036: }
037:
038: protected void filterSequent() {
039: if (antec != null)
040: return;
041:
042: IteratorOfConstrainedFormula it;
043:
044: antec = SLListOfSequentPrintFilterEntry.EMPTY_LIST;
045: it = originalSequent.antecedent().iterator();
046: while (it.hasNext())
047: antec = antec.append(filterFormula(it.next()));
048:
049: succ = SLListOfSequentPrintFilterEntry.EMPTY_LIST;
050: it = originalSequent.succedent().iterator();
051: while (it.hasNext())
052: succ = succ.append(filterFormula(it.next()));
053: }
054:
055: protected SequentPrintFilterEntry filterFormula(
056: ConstrainedFormula p_cfma) {
057: /*
058: return new Entry ( new ConstrainedFormula ( p_cfma.formula (),
059: Constraint.BOTTOM ),
060: p_cfma,
061: Constraint.BOTTOM );
062: */
063:
064: if (p_cfma.constraint().isAsWeakAs(userConstraint))
065: return new Entry(new ConstrainedFormula(p_cfma.formula(),
066: Constraint.BOTTOM), p_cfma, userConstraint);
067: else {
068: return new Entry(p_cfma, p_cfma,
069: determineDisplayConstraint(p_cfma, userConstraint));
070: }
071: }
072:
073: public static Constraint determineDisplayConstraint(
074: ConstrainedFormula p_cfma, Constraint p_userConstraint) {
075: Constraint c = p_userConstraint.join(p_cfma.constraint(), null);
076: if (c.isSatisfiable())
077: return c;
078: return p_cfma.constraint();
079: }
080:
081: /**
082: * @return the original sequent
083: */
084: public Sequent getSequent() {
085: return originalSequent;
086: }
087:
088: /**
089: * Get the formulas of the filtered sequent and the constraints to
090: * use for instantiating metavariables when printing
091: */
092: public ListOfSequentPrintFilterEntry getAntec() {
093: filterSequent();
094: return antec;
095: }
096:
097: public ListOfSequentPrintFilterEntry getSucc() {
098: filterSequent();
099: return succ;
100: }
101:
102: protected static class Entry implements SequentPrintFilterEntry {
103: final ConstrainedFormula filteredFormula;
104: final ConstrainedFormula originalFormula;
105:
106: final Constraint displayConstraint;
107:
108: public Entry(ConstrainedFormula p_filteredFormula,
109: ConstrainedFormula p_originalFormula,
110: Constraint p_displayConstraint) {
111: filteredFormula = p_filteredFormula;
112: originalFormula = p_originalFormula;
113: displayConstraint = p_displayConstraint;
114: }
115:
116: /**
117: * Formula to display
118: */
119: public ConstrainedFormula getFilteredFormula() {
120: return filteredFormula;
121: }
122:
123: /**
124: * Original formula from sequent
125: */
126: public ConstrainedFormula getOriginalFormula() {
127: return originalFormula;
128: }
129:
130: /**
131: * Constraint for metavariable instantiations
132: */
133: public Constraint getDisplayConstraint() {
134: return displayConstraint;
135: }
136: }
137:
138: }
|