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.Term;
14:
15: /**
16: * Two kind of matching algorithm are coded in two nested classes BaseMatching
17: * TwosideMatching
18: */
19: class Matching {
20:
21: private Matching() {
22: }
23:
24: /**
25: * matching <code>trigger</code> to <code>targetTerm</code> recursively
26: * @param trigger a uni-trigger
27: * @param targetTerm a gound term
28: * @return all substitution found from this matching
29: */
30: public static SetOfSubstitution basicMatching(Trigger trigger,
31: Term targetTerm) {
32: return BasicMatching.getSubstitutions(trigger.getTriggerTerm(),
33: targetTerm);
34: }
35:
36: public static SetOfSubstitution twoSidedMatching(
37: UniTrigger trigger, Term targetTerm) {
38: TwoSidedMatching tsm = new TwoSidedMatching(trigger, targetTerm);
39: return tsm.getSubstitutions();
40: }
41:
42: }
|