1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
2 | * |
3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
4 | * |
5 | * "Hilbert II" is free software; you can redistribute |
6 | * it and/or modify it under the terms of the GNU General Public |
7 | * License as published by the Free Software Foundation; either |
8 | * version 2 of the License, or (at your option) any later version. |
9 | * |
10 | * This program is distributed in the hope that it will be useful, |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
13 | * GNU General Public License for more details. |
14 | */ |
15 | |
16 | package org.qedeq.kernel.bo.logic.model; |
17 | |
18 | import java.util.ArrayList; |
19 | import java.util.List; |
20 | |
21 | import org.qedeq.kernel.bo.logic.common.SubjectVariable; |
22 | |
23 | /** |
24 | * This class interpretation. |
25 | * |
26 | * @author Michael Meyling |
27 | */ |
28 | public final class SubjectVariableInterpreter { |
29 | |
30 | /** List of subject variables allocations. */ |
31 | private List subjectVariableAllocations; |
32 | |
33 | /** Model contains entities. */ |
34 | private Model model; |
35 | |
36 | /** |
37 | * Constructor. |
38 | * |
39 | * @param model Model we work on. |
40 | */ |
41 | public SubjectVariableInterpreter(final Model model) { |
42 | this.model = model; |
43 | subjectVariableAllocations = new ArrayList(); |
44 | } |
45 | |
46 | /** |
47 | * Change to next valuation. |
48 | * |
49 | * @return Is there a next new valuation? |
50 | */ |
51 | public synchronized boolean next() { |
52 | boolean next = true; |
53 | for (int i = subjectVariableAllocations.size() - 1; i >= -1; i--) { |
54 | if (i < 0) { |
55 | next = false; |
56 | break; |
57 | } |
58 | final SubjectVariableAllocation allocation |
59 | = (SubjectVariableAllocation) subjectVariableAllocations.get(i); |
60 | if (allocation.getValue() + 1 < model.getEntitiesSize()) { |
61 | allocation.increaseNumber(); |
62 | break; |
63 | } |
64 | allocation.resetNumber(); |
65 | } |
66 | return next; |
67 | } |
68 | |
69 | /** |
70 | * Add subject variable. This is usually done for interpreting a quantifier. |
71 | * |
72 | * @param var Subject variable to add to our interpretation. |
73 | */ |
74 | public synchronized void addSubjectVariable(final SubjectVariable var) { |
75 | // if we forbid quantifing with same variable twice, we must activate the following |
76 | // if (subjectVariables.contains(var)) { |
77 | // throw new RuntimeException("variable already exists: " + var); |
78 | // } |
79 | // System.out.println("added subject variable " + var); |
80 | subjectVariableAllocations.add(new SubjectVariableAllocation(var)); |
81 | } |
82 | |
83 | /** |
84 | * Add subject variable even if already existing. |
85 | * |
86 | * @param var Remove this subject variable. |
87 | * @param value Set interpretation to this entity number. |
88 | */ |
89 | public synchronized void forceAddSubjectVariable(final SubjectVariable var, final int value) { |
90 | subjectVariableAllocations.add(new SubjectVariableAllocation(var, value)); |
91 | } |
92 | |
93 | /** |
94 | * Remove existing subject variable interpretation. |
95 | * |
96 | * @param var Remove this subject variable. |
97 | */ |
98 | public synchronized void forceRemoveSubjectVariable(final SubjectVariable var) { |
99 | int index = getIndex(var); |
100 | if (index < 0) { |
101 | throw new RuntimeException("variable does not exist: " + var); |
102 | } |
103 | final SubjectVariableAllocation current |
104 | = (SubjectVariableAllocation) subjectVariableAllocations.get(index); |
105 | if (!current.isFixed()) { |
106 | throw new RuntimeException("trying to remove not fixed allocation: " + current); |
107 | } |
108 | subjectVariableAllocations.remove(index); |
109 | // System.out.println("removed subject variable " + var); |
110 | } |
111 | /** |
112 | * Remove existing subject variable interpretation. |
113 | * |
114 | * @param var Remove this subject variable. |
115 | */ |
116 | public synchronized void removeSubjectVariable(final SubjectVariable var) { |
117 | int index = getIndex(var); |
118 | if (index < 0) { |
119 | throw new RuntimeException("variable does not exist: " + var); |
120 | } |
121 | final SubjectVariableAllocation current |
122 | = (SubjectVariableAllocation) subjectVariableAllocations.get(index); |
123 | if (current.isFixed()) { |
124 | throw new RuntimeException("trying to remove fixed allocation: " + current); |
125 | } |
126 | subjectVariableAllocations.remove(index); |
127 | // System.out.println("removed subject variable " + var); |
128 | } |
129 | |
130 | private synchronized int getSubjectVariableSelection(final SubjectVariable var) { |
131 | int selection = 0; |
132 | int index = getIndex(var); |
133 | if (index >= 0) { |
134 | selection = ((SubjectVariableAllocation) subjectVariableAllocations.get(index)) |
135 | .getValue(); |
136 | } else { |
137 | addSubjectVariable(var); |
138 | } |
139 | return selection; |
140 | } |
141 | |
142 | /** |
143 | * Get current interpretation of subject variable. |
144 | * |
145 | * @param var Subject variable we are interested in. |
146 | * @return Current entity for subject variable. |
147 | */ |
148 | public synchronized Entity getEntity(final SubjectVariable var) { |
149 | return model.getEntity(getSubjectVariableSelection(var)); |
150 | } |
151 | |
152 | private int getIndex(final SubjectVariable var) { |
153 | int index = -1; |
154 | for (index = subjectVariableAllocations.size() - 1; index >= 0; index--) { |
155 | final SubjectVariableAllocation current |
156 | = (SubjectVariableAllocation) subjectVariableAllocations.get(index); |
157 | if (var.equals(current.getVariable())) { |
158 | break; |
159 | } |
160 | } |
161 | return index; |
162 | } |
163 | |
164 | /** |
165 | * Set interpretation of subject variable to next entity. |
166 | * |
167 | * @param var Switch to next entity for this subject variable. |
168 | */ |
169 | public synchronized void increaseSubjectVariableSelection(final SubjectVariable var) { |
170 | ((SubjectVariableAllocation) subjectVariableAllocations.get(getIndex(var))).increaseNumber(); |
171 | } |
172 | |
173 | public synchronized String toString() { |
174 | final StringBuffer buffer = new StringBuffer(); |
175 | buffer.append("subject variables {"); |
176 | for (int i = 0; i < subjectVariableAllocations.size(); i++) { |
177 | if (i > 0) { |
178 | buffer.append(", "); |
179 | } |
180 | SubjectVariableAllocation var = (SubjectVariableAllocation) subjectVariableAllocations.get(i); |
181 | buffer.append(var.getVariable()); |
182 | buffer.append("="); |
183 | buffer.append(model.getEntity(var.getValue())); |
184 | } |
185 | buffer.append("}"); |
186 | return buffer.toString(); |
187 | } |
188 | |
189 | /** |
190 | * Clear variable interpretation. |
191 | */ |
192 | public synchronized void clear() { |
193 | subjectVariableAllocations.clear(); |
194 | } |
195 | |
196 | } |