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.encapsulation;
12:
13: class TypeSchemeConstraintSolver {
14: private TypeSchemeConstraint constraint;
15: private TypeSchemeVariable vars[];
16:
17: private boolean run(int varPos) {
18: if (varPos >= vars.length) {
19: return true;
20: }
21:
22: IteratorOfTypeScheme it = vars[varPos].getValueRange()
23: .iterator();
24: while (it.hasNext()) {
25: vars[varPos].assignValue(it.next());
26: if (constraint.evaluate()) {
27: if (run(varPos + 1)) {
28: return true;
29: }
30: }
31: }
32:
33: vars[varPos].assignDefaultValue();
34: return false;
35: }
36:
37: /**
38: * Tries to solve a type scheme constraint.
39: * @param constraint the constraint; after a successful execution of this
40: * method, the values assigned to its type scheme variables describe the
41: * solution
42: * @return true if successful, false otherwise
43: */
44: public boolean solve(TypeSchemeConstraint constraint) {
45: this .constraint = constraint;
46: this .vars = constraint.getFreeVars().toArray();
47:
48: for (int i = 0; i < vars.length; i++) {
49: vars[i].assignDefaultValue();
50: }
51:
52: return run(0) && constraint.evaluate();
53: }
54: }
|