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: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: //
17:
18: package de.uka.ilkd.key.speclang;
19:
20: import java.util.HashMap;
21: import java.util.Map;
22:
23: import de.uka.ilkd.key.logic.Term;
24: import de.uka.ilkd.key.logic.sort.Sort;
25:
26: public class FormulaWithAxioms {
27: private final Term formula;
28: private final Map /*Operator -> Term*/axioms;
29:
30: public FormulaWithAxioms(Term formula,
31: Map /*Operator -> Term*/axioms) {
32: assert formula.sort() == Sort.FORMULA;
33: this .formula = formula;
34: this .axioms = new HashMap();
35: this .axioms.putAll(axioms);
36: }
37:
38: public FormulaWithAxioms(Term formula) {
39: this (formula, new HashMap());
40: }
41:
42: public Term getFormula() {
43: return formula;
44: }
45:
46: public Map /*Operator -> Term*/getAxioms() {
47: HashMap result = new HashMap();
48: result.putAll(axioms);
49: return result;
50: }
51: }
|