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.updatesimplifier;
12:
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
15: import de.uka.ilkd.key.logic.op.Op;
16: import de.uka.ilkd.key.logic.op.QuanUpdateOperator;
17: import de.uka.ilkd.key.util.Debug;
18:
19: /**
20: *
21: */
22: public class QuanAssignmentPairLazy extends AbstractAssignmentPairLazy {
23:
24: public QuanAssignmentPairLazy(Term update, int locationPos) {
25: super (update, locationPos);
26: Debug.assertTrue(getUpdateOp() instanceof QuanUpdateOperator);
27: }
28:
29: /* (non-Javadoc)
30: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#boundVars()
31: */
32: public ArrayOfQuantifiableVariable boundVars() {
33: return getQuanUpdateOp().boundVars(getUpdateTerm(),
34: getLocationPos());
35: }
36:
37: /* (non-Javadoc)
38: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#guard()
39: */
40: public Term guard() {
41: return getQuanUpdateOp().guard(getUpdateTerm(),
42: getLocationPos());
43: }
44:
45: /* (non-Javadoc)
46: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#nontrivialGuard()
47: */
48: public boolean nontrivialGuard() {
49: return guard().op() != Op.TRUE;
50: }
51:
52: private QuanUpdateOperator getQuanUpdateOp() {
53: return (QuanUpdateOperator) getUpdateOp();
54: }
55:
56: }
|