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.logic;
12:
13: import java.util.Iterator;
14: import java.util.List;
15:
16: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
17: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
18:
19: /**
20: * A structure for storing the arguments to an Operator
21: * when creating a Term. Each argument, in form of a Term,
22: * can have bound variables, in form of an ArrayOfQuantifiableVariable.
23: * This class allows efficient extraction of the different parts.
24: */
25: public class PairOfTermArrayAndBoundVarsArray {
26: private Term[] term;
27: private ArrayOfQuantifiableVariable[] var;
28:
29: public PairOfTermArrayAndBoundVarsArray(List list) {
30: term = new Term[list.size()];
31: var = new ArrayOfQuantifiableVariable[list.size()];
32: boolean hasBoundVars = false;
33: Iterator iter = list.iterator();
34: for (int i = 0; iter.hasNext(); i++) {
35: TermWithBoundVars t = (TermWithBoundVars) iter.next();
36: term[i] = t.term;
37: if (t.boundVars == null) {
38: var[i] = new ArrayOfQuantifiableVariable(
39: new QuantifiableVariable[0]);
40: } else {
41: var[i] = t.boundVars;
42: hasBoundVars = true;
43: }
44: }
45: if (!hasBoundVars) {
46: var = null;
47: }
48: }
49:
50: public Term[] getTerms() {
51: return term;
52: }
53:
54: public ArrayOfQuantifiableVariable[] getBoundVars() {
55: return var;
56: }
57:
58: public int size() {
59: return term.length;
60: }
61:
62: }
|