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.strategy.feature;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Constraint;
15: import de.uka.ilkd.key.rule.IteratorOfIfFormulaInstantiation;
16: import de.uka.ilkd.key.rule.ListOfIfFormulaInstantiation;
17: import de.uka.ilkd.key.rule.TacletApp;
18:
19: /**
20: * Abstract superclass for the features treating constraints; contains some
21: * generally useful methods
22: */
23: public abstract class AbstractConstraintStrengthenFeature extends
24: BinaryTacletAppFeature {
25:
26: protected AbstractConstraintStrengthenFeature() {
27: super (false);
28: }
29:
30: /**
31: * @preconditions app.ifInstsComplete ()
32: * @param services TODO
33: * @return the conjunction of the constraints that are attached to formulas
34: * matched by the if-clauses of the taclet
35: */
36: protected static Constraint getIfConstraint(TacletApp app,
37: Services services) {
38: Constraint c = Constraint.BOTTOM;
39:
40: final ListOfIfFormulaInstantiation insts = app
41: .ifFormulaInstantiations();
42: if (insts == null)
43: return c;
44:
45: final IteratorOfIfFormulaInstantiation it = insts.iterator();
46: // TODO: c will be unsatifiable if intersection sorts are required
47: // (is this intended)? or rather new Namespace()
48: while (it.hasNext())
49: c = c.join(it.next().getConstrainedFormula().constraint(),
50: services);
51: return c;
52: }
53:
54: }
|