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: /** this class contains a Taclet together with its suggested
12: * instantiations. */package de.uka.ilkd.key.rule.inst;
13:
14: import de.uka.ilkd.key.logic.op.MapFromSchemaVariableToTerm;
15: import de.uka.ilkd.key.rule.Taclet;
16:
17: public class TacletInstantiations {
18:
19: /** the rule */
20: private Taclet rule;
21: /** the instantations */
22: private MapFromSchemaVariableToTerm instantiations;
23:
24: public TacletInstantiations(Taclet rule,
25: MapFromSchemaVariableToTerm instantiations) {
26: this .rule = rule;
27: this .instantiations = instantiations;
28: }
29:
30: public Taclet taclet() {
31: return rule;
32: }
33:
34: public MapFromSchemaVariableToTerm instantiations() {
35: return instantiations;
36: }
37:
38: public String toString() {
39: return "rule: " + taclet() + "; instantiation: "
40: + instantiations();
41: }
42:
43: }
|