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.rule.updatesimplifier;
12:
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.TermFactory;
15: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
16: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
17:
18: class IfExCascadeEntryBuilder extends GuardSimplifier {
19:
20: private Term thenBranch;
21:
22: public IfExCascadeEntryBuilder(final Term condition,
23: final ArrayOfQuantifiableVariable minimizedVars,
24: final Term thenBranch) {
25: super (condition, minimizedVars);
26: this .thenBranch = thenBranch;
27:
28: simplify();
29: }
30:
31: protected boolean isNeededVar(QuantifiableVariable var) {
32: return thenBranch.freeVars().contains(var);
33: }
34:
35: protected void substitute(QuantifiableVariable var, Term substTerm) {
36: thenBranch = subst(var, substTerm, thenBranch);
37: }
38:
39: public Term createTerm(Term elseBranch) {
40: if (isValidGuard() && !bindsVariables()
41: || thenBranch.equalsModRenaming(elseBranch)) {
42: return thenBranch;
43: } else if (isUnsatisfiableGuard()) {
44: return elseBranch;
45: } else if (bindsVariables()) {
46: final ArrayOfQuantifiableVariable vars = new ArrayOfQuantifiableVariable(
47: getMinimizedVars().toArray());
48: return TermFactory.DEFAULT.createIfExThenElseTerm(vars,
49: getCondition(), thenBranch, elseBranch);
50: } else {
51: return TermFactory.DEFAULT.createIfThenElseTerm(
52: getCondition(), thenBranch, elseBranch);
53: }
54: }
55:
56: public boolean isAlwaysElse() {
57: return isUnsatisfiableGuard();
58: }
59:
60: public boolean isEndOfCascade() {
61: return isValidGuard() && !bindsVariables();
62: }
63: }
|