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.strategy.quantifierHeuristics;
12:
13: import de.uka.ilkd.key.logic.IteratorOfTerm;
14: import de.uka.ilkd.key.logic.SetAsListOfTerm;
15: import de.uka.ilkd.key.logic.SetOfTerm;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
18: import de.uka.ilkd.key.logic.op.Op;
19: import de.uka.ilkd.key.logic.op.Operator;
20: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
21: import de.uka.ilkd.key.logic.op.Quantifier;
22: import de.uka.ilkd.key.logic.op.SetAsListOfQuantifiableVariable;
23: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
24:
25: class TriggerUtils {
26:
27: /**
28: * remove all the quantifiable variable bounded in the top level
29: * of a given formula.
30: */
31: public static Term discardQuantifiers(Term qterm) {
32: Term t = qterm;
33: while (t.op() instanceof Quantifier)
34: t = t.sub(0);
35: return t;
36: }
37:
38: /**
39: * @return set of terms that are that the term splite d through the operator
40: * <code>op</code>
41: */
42: public static IteratorOfTerm iteratorByOperator(Term term,
43: Operator op) {
44: return setByOperator(term, op).iterator();
45: }
46:
47: public static SetOfTerm setByOperator(Term term, Operator op) {
48: if (term.op() == op)
49: return setByOperator(term.sub(0), op).union(
50: setByOperator(term.sub(1), op));
51: return SetAsListOfTerm.EMPTY_SET.add(term);
52: }
53:
54: /**
55: *
56: * @param set0
57: * @param set1
58: * @return a set of quantifiableVariable which are belonged to
59: * both set0 and set1 have
60: */
61: public static SetOfQuantifiableVariable intersect(
62: SetOfQuantifiableVariable set0,
63: SetOfQuantifiableVariable set1) {
64: SetOfQuantifiableVariable res = SetAsListOfQuantifiableVariable.EMPTY_SET;
65: final IteratorOfQuantifiableVariable it = set0.iterator();
66: while (it.hasNext()) {
67: final QuantifiableVariable el = it.next();
68: if (set1.contains(el))
69: res = res.add(el);
70: }
71: return res;
72: }
73:
74: public static boolean isTrueOrFalse(Term res) {
75: final Operator op = res.op();
76: return op == Op.TRUE || op == Op.FALSE;
77: }
78: }
|