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.rule.soundness;
012:
013: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
014: import de.uka.ilkd.key.logic.Sequent;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.TermFactory;
017: import de.uka.ilkd.key.logic.op.Equality;
018: import de.uka.ilkd.key.logic.op.Op;
019: import de.uka.ilkd.key.rule.*;
020:
021: /**
022: * Build the meaning formula for a given taclet
023: */
024: public class MeaningFormulaBuilder {
025:
026: private final TacletApp app;
027:
028: public MeaningFormulaBuilder(TacletApp p_app) {
029: app = p_app;
030: }
031:
032: public Term build() {
033: checkTaclet();
034: return createMF();
035: }
036:
037: /**
038: * Ensure that we are really able to cope with the
039: * given taclet (incomplete)
040: */
041: private void checkTaclet() {
042: if (isRewriteTacletWithRWorAdd()
043: && !(((RewriteTaclet) getTaclet())
044: .getStateRestriction() == RewriteTaclet.SAME_UPDATE_LEVEL))
045: throw new IllegalArgumentException(
046: "Can't handle rewrite taclets "
047: + "without the \"\\sameUpdateLevel\" flag\n"
048: + "and with if- or add-parts");
049:
050: if (getTaclet().varsNewDependingOn().hasNext())
051: throw new IllegalArgumentException("Can't handle taclets "
052: + "with a \"new depending on\" variable condition");
053:
054: if (getTaclet().getVariableConditions().hasNext())
055: throw new IllegalArgumentException("Can't handle taclets "
056: + "with a generic variable condition");
057: }
058:
059: /**
060: * @return true iff the treated taclet is a rewrite taclet that has an
061: * non-empty if-part or a non-empty add-part
062: */
063: private boolean isRewriteTacletWithRWorAdd() {
064: if (!isRewriteTaclet())
065: return false;
066:
067: if (((RewriteTaclet) getTaclet()).ifSequent() != Sequent.EMPTY_SEQUENT)
068: return true;
069:
070: final IteratorOfTacletGoalTemplate it = getTaclet()
071: .goalTemplates().iterator();
072:
073: while (it.hasNext()) {
074: if (it.next().sequent() != Sequent.EMPTY_SEQUENT)
075: return true;
076: }
077:
078: return false;
079: }
080:
081: private Term createMF() {
082: return Imp(createPremisses(), createConclusion());
083: }
084:
085: private Term createConclusion() {
086: final Term ifPart = createMF(getTaclet().ifSequent());
087:
088: if (isFindTaclet() && !isRewriteTaclet()) {
089: if (isAntecTaclet())
090: return Imp(getFind(), ifPart);
091: else
092: return Or(getFind(), ifPart);
093: }
094:
095: return ifPart;
096: }
097:
098: private Term createPremisses() {
099: Term res = True();
100: final IteratorOfTacletGoalTemplate it = getTaclet()
101: .goalTemplates().iterator();
102:
103: while (it.hasNext())
104: res = And(res, createMF(it.next()));
105:
106: return res;
107: }
108:
109: private Term createMF(TacletGoalTemplate p) {
110: final Term addPart = createMF(p.sequent());
111:
112: if (isFindTaclet()) {
113: if (isRewriteTaclet()) {
114: if (p instanceof RewriteTacletGoalTemplate) {
115: final Term rwPart = createRWPartRewrite((RewriteTacletGoalTemplate) p);
116: return Imp(rwPart, addPart);
117: }
118: } else {
119: if (p instanceof AntecSuccTacletGoalTemplate) {
120: final Term rwPart = createMF(((AntecSuccTacletGoalTemplate) p)
121: .replaceWith());
122: return Or(rwPart, addPart);
123: }
124: }
125: }
126:
127: return addPart;
128: }
129:
130: private Term createRWPartRewrite(RewriteTacletGoalTemplate p) {
131: final Equality eq = getFind().sort().getEqualitySymbol();
132: return getTF().createEqualityTerm(eq, getFind(),
133: p.replaceWith());
134: }
135:
136: private Term createMF(Sequent p) {
137: Term antec = True();
138: IteratorOfConstrainedFormula it = p.antecedent().iterator();
139:
140: while (it.hasNext())
141: antec = And(antec, it.next().formula());
142:
143: Term succ = False();
144: it = p.succedent().iterator();
145:
146: while (it.hasNext())
147: succ = Or(succ, it.next().formula());
148:
149: return Imp(antec, succ);
150: }
151:
152: private Term And(Term p0, Term p1) {
153: return getTF().createJunctorTermAndSimplify(Op.AND, p0, p1);
154: }
155:
156: private Term Or(Term p0, Term p1) {
157: return getTF().createJunctorTermAndSimplify(Op.OR, p0, p1);
158: }
159:
160: private Term Imp(Term p0, Term p1) {
161: return getTF().createJunctorTermAndSimplify(Op.IMP, p0, p1);
162: }
163:
164: private Term True() {
165: return getTF().createJunctorTerm(Op.TRUE);
166: }
167:
168: private Term False() {
169: return getTF().createJunctorTerm(Op.FALSE);
170: }
171:
172: private boolean isFindTaclet() {
173: return getTaclet() instanceof FindTaclet;
174: }
175:
176: private boolean isAntecTaclet() {
177: return getTaclet() instanceof AntecTaclet;
178: }
179:
180: private boolean isRewriteTaclet() {
181: return getTaclet() instanceof RewriteTaclet;
182: }
183:
184: private TacletApp getTacletApp() {
185: return app;
186: }
187:
188: private Taclet getTaclet() {
189: return getTacletApp().taclet();
190: }
191:
192: private Term getFind() {
193: if (isFindTaclet())
194: return ((FindTaclet) getTaclet()).find();
195: return null;
196: }
197:
198: private TermFactory getTF() {
199: return TermFactory.DEFAULT;
200: }
201:
202: }
|