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: package de.uka.ilkd.key.parser.ocl;
09:
10: import java.util.HashMap;
11: import java.util.Map;
12:
13: import de.uka.ilkd.key.logic.Named;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.TermBuilder;
16:
17: /**
18: * Collects all axioms, which are created during the translation.
19: *
20: */
21: public class AxiomCollector {
22:
23: private static final TermBuilder tb = TermBuilder.DF;
24:
25: private Map /*Named -> Term */axioms = new HashMap();
26:
27: public void collectAxiom(Named n, Term a) {
28: if (axioms.containsKey(n)) {
29: axioms.put(n, (tb.and((Term) axioms.get(n), a)));
30: } else {
31: axioms.put(n, a);
32: }
33:
34: }
35:
36: /**
37: * Returns all collected axioms.
38: *
39: * @return Map from defined symbols to axioms
40: */
41: public Map /*Named -> Term*/getAxioms() {
42: return axioms;
43: }
44: }
|