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.metaconstruct;
12:
13: import de.uka.ilkd.key.java.ProgramElement;
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.logic.Name;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.TermFactory;
18: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
19: import de.uka.ilkd.key.logic.op.ArrayOfLocation;
20: import de.uka.ilkd.key.logic.op.NRFunctionWithExplicitDependencies;
21: import de.uka.ilkd.key.logic.op.Op;
22: import de.uka.ilkd.key.logic.sort.Sort;
23: import de.uka.ilkd.key.rule.encapsulation.UniverseAnalyser;
24: import de.uka.ilkd.key.rule.inst.SVInstantiations;
25: import de.uka.ilkd.key.util.Debug;
26:
27: public class Universes extends AbstractMetaOperator {
28: public Sort sort(Term[] term) {
29: return Sort.FORMULA;
30: }
31:
32: public Universes() {
33: super (new Name("#Universes"), 1);
34: }
35:
36: public Term calculate(Term term, SVInstantiations svInst,
37: Services services) {
38: Term programTerm = term.sub(0);
39: ProgramElement pi = programTerm.javaBlock().program();
40: Term phiTerm = programTerm.sub(0);
41:
42: //get field sets
43: NRFunctionWithExplicitDependencies phiOp = (NRFunctionWithExplicitDependencies) phiTerm
44: .op();
45: Debug.assertTrue(phiOp.getNumPartitions() == 3);
46: ArrayOfLocation R = phiOp.getDependencies(0);
47: ArrayOfLocation P = phiOp.getDependencies(1);
48: ArrayOfLocation F = phiOp.getDependencies(2);
49: Debug.assertTrue(R != null && P != null && F != null);
50:
51: //perform analysis
52: UniverseAnalyser ua = new UniverseAnalyser();
53: if (ua.analyse(R, P, F, pi, svInst, services)) {
54: return TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
55: } else {
56: return programTerm;
57: }
58: }
59: }
|