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.Op;
17:
18: /**
19: *
20: */
21: public class GuardSatisfiabilityFormulaBuilder extends GuardSimplifier {
22:
23: public GuardSatisfiabilityFormulaBuilder(Term condition,
24: ArrayOfQuantifiableVariable arMinimizedVars) {
25: super (condition, arMinimizedVars);
26:
27: simplify();
28: }
29:
30: public Term createFormula() {
31: if (isValidGuard() || isUnsatisfiableGuard()
32: || !bindsVariables())
33: return getCondition();
34:
35: final UpdateSimplifierTermFactory utf = UpdateSimplifierTermFactory.DEFAULT;
36: final TermFactory tf = utf.getBasicTermFactory();
37:
38: return tf.createQuantifierTerm(Op.EX, getMinimizedVars()
39: .toArray(), getCondition());
40: }
41: }
|