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: package de.uka.ilkd.key.strategy.quantifierHeuristics;
18:
19: import de.uka.ilkd.key.logic.Name;
20: import de.uka.ilkd.key.logic.Term;
21: import de.uka.ilkd.key.logic.TermBuilder;
22: import de.uka.ilkd.key.logic.op.Function;
23: import de.uka.ilkd.key.logic.op.MapAsListFromQuantifiableVariableToTerm;
24: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToTerm;
25: import de.uka.ilkd.key.logic.op.Metavariable;
26: import de.uka.ilkd.key.logic.op.Op;
27: import de.uka.ilkd.key.logic.op.Operator;
28: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
29: import de.uka.ilkd.key.logic.op.Quantifier;
30: import de.uka.ilkd.key.logic.op.RigidFunction;
31: import de.uka.ilkd.key.logic.sort.Sort;
32:
33: /**
34: * This class is used to create metavariables for every universal variables in
35: * quantified formula <code>allTerm</code> and create constant functions for
36: * all existential variables. The variables with new created metavariables or
37: * constant functions are store to a map <code>mapQM</code>.
38: */
39: class ReplacerOfQuanVariablesWithMetavariables {
40:
41: final private static TermBuilder tb = TermBuilder.DF;
42:
43: private ReplacerOfQuanVariablesWithMetavariables() {
44: }
45:
46: public static Substitution createSubstitutionForVars(Term allTerm) {
47: MapFromQuantifiableVariableToTerm res = MapAsListFromQuantifiableVariableToTerm.EMPTY_MAP;
48: Term t = allTerm;
49: Operator op = t.op();
50: while (op instanceof Quantifier) {
51: QuantifiableVariable q = t.varsBoundHere(0)
52: .getQuantifiableVariable(0);
53: Term m;
54: if (op == Op.ALL) {
55: Metavariable mv = new Metavariable(ARBITRARY_NAME, q
56: .sort());
57: m = tb.func(mv);
58: } else {
59: Function f = new RigidFunction(ARBITRARY_NAME,
60: q.sort(), new Sort[0]);
61: m = tb.func(f);
62: }
63: res = res.put(q, m);
64: t = t.sub(0);
65: op = t.op();
66: }
67: return new Substitution(res);
68: }
69:
70: private final static Name ARBITRARY_NAME = new Name("unifier");
71:
72: }
|