diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend | 407 |
1 files changed, 407 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend new file mode 100644 index 00000000..b3e44b46 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend | |||
@@ -0,0 +1,407 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
46 | import java.math.BigDecimal | ||
47 | import java.util.ArrayList | ||
48 | import java.util.Collection | ||
49 | import java.util.Collections | ||
50 | import java.util.HashMap | ||
51 | import java.util.LinkedList | ||
52 | import java.util.List | ||
53 | import java.util.Map | ||
54 | |||
55 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
56 | import org.eclipse.xtend.lib.annotations.Data | ||
57 | |||
58 | @Data class InterpretationValidationResult { | ||
59 | val List<String> problems; | ||
60 | val List<Assertion> invalidAssertions; | ||
61 | def isValid() { return problems.empty && invalidAssertions.empty} | ||
62 | } | ||
63 | |||
64 | class LogicStructureBuilder{ | ||
65 | val protected extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
66 | |||
67 | def public dispatch Collection<DefinedElement> getElements(LogicModelInterpretation interpretation, TypeDeclaration type) { | ||
68 | return interpretation.getElements(type) | ||
69 | } | ||
70 | def public dispatch Collection<DefinedElement> getElements(LogicModelInterpretation interpretation, TypeDefinition type) { | ||
71 | return type.elements | ||
72 | } | ||
73 | |||
74 | def public Term evalAsTerm(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap).toTerm } | ||
75 | def public boolean evalAsBool(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Boolean} | ||
76 | def public int evalAsInt(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Integer } | ||
77 | def public BigDecimal evalAsReal(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as BigDecimal } | ||
78 | /** | ||
79 | * Evaluate the expression on a solution to an logic element. | ||
80 | * @param interpretation The interpretation which the expression is evaluated on. | ||
81 | * @param term An expression which results in a logic element. | ||
82 | * @return The logic element value of the expression. Returns the element directly, not a symbolic reference! | ||
83 | */ | ||
84 | def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.resolve(interpretation,emptyMap) as DefinedElement} | ||
85 | /** | ||
86 | * Checks if the interpretation is a valid solution of the problem by checking the satisfactions of each assertion. | ||
87 | * Returns the collection of failed assertions. | ||
88 | * @param interpretation The checked interpretation. | ||
89 | * @param problem The interpretation is checked on this problem. | ||
90 | * @return The collection of failed assertions. | ||
91 | */ | ||
92 | def public validateInterpretationOnProblem(LogicModelInterpretation interpretation, LogicProblem problem) { | ||
93 | val List<String> problems = new LinkedList | ||
94 | |||
95 | // Checking types | ||
96 | val type2ElementsMap = problem.types.toInvertedMap[interpretation.getElements(it)] | ||
97 | |||
98 | // Checking definition does not changed | ||
99 | for(type : problem.types.filter(TypeDefinition)) { | ||
100 | val elements = type2ElementsMap.get(type) | ||
101 | if(!type.elements.containsAll(elements)) | ||
102 | problems+='''The interpretation of «type.name» does not contains each elements of the problem''' | ||
103 | if(!elements.containsAll(type.elements)) | ||
104 | problems+='''The interpretation of «type.name» does not contains additional elements not specified in the problem''' | ||
105 | } | ||
106 | // Checking the type table | ||
107 | val allElements = type2ElementsMap.values.flatten.toSet | ||
108 | for (element : allElements) { | ||
109 | if(! checkElement(problem, type2ElementsMap, element)) { | ||
110 | problems += '''«element.name» does not follows the type hierarchy''' | ||
111 | } | ||
112 | } | ||
113 | |||
114 | // Checking assertions | ||
115 | val List<Assertion> invalidAssertions = new LinkedList | ||
116 | for(assertion : problem.assertions) { | ||
117 | if(! interpretation.evalAsBool(assertion.value)) { | ||
118 | invalidAssertions+= assertion | ||
119 | problems += '''«assertion.name» is violated!''' | ||
120 | } | ||
121 | } | ||
122 | return new InterpretationValidationResult(problems,invalidAssertions) | ||
123 | //problem.assertions.filter[x | ! interpretation.evalAsBool(x.value)] | ||
124 | } | ||
125 | |||
126 | private def checkElement(LogicProblem problem, Map<Type, List<DefinedElement>> type2ElementsMap, DefinedElement element) { | ||
127 | val compatibleDynamicTypes = new LinkedList | ||
128 | for(possibleDynamicType: problem.types.filter[!it.isIsAbstract]) { | ||
129 | //println(possibleDynamicType.name) | ||
130 | val compatibleTypes = possibleDynamicType.transitiveClosureStar[it.supertypes] | ||
131 | //compatibleTypes.forEach[print(''' + «it.name»''')] | ||
132 | val incompatibleTypes = problem.types.filter[!compatibleTypes.contains(it)] | ||
133 | //incompatibleTypes.forEach[print(''' - «it.name»''')] | ||
134 | if(compatibleTypes.forall[ type2ElementsMap.get(it).contains(element)] && incompatibleTypes.forall[!type2ElementsMap.get(it).contains(element)]) { | ||
135 | //println("Ok") | ||
136 | compatibleDynamicTypes += possibleDynamicType | ||
137 | } | ||
138 | } | ||
139 | return compatibleDynamicTypes.size == 1 | ||
140 | } | ||
141 | |||
142 | def protected dispatch Term toTerm(Integer o) { createIntLiteral=>[value = o] } | ||
143 | def protected dispatch Term toTerm(BigDecimal o) { createRealLiteral=>[value = o]} | ||
144 | def protected dispatch Term toTerm(Boolean o) { createBoolLiteral=>[value = o]} | ||
145 | def protected dispatch Term toTerm(SymbolicDeclaration o) { createSymbolicValue=>[symbolicReference = o]} | ||
146 | def public Term termDescriptiontoTerm(TermDescription term) { | ||
147 | if(term instanceof Term) return term | ||
148 | else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] | ||
149 | else if (term instanceof Constant) return createSymbolicValue=>[symbolicReference = term] | ||
150 | else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term] | ||
151 | else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) | ||
152 | } | ||
153 | /** | ||
154 | * Returns if the operation with the numbers in the parameter requires the use of <code>BigDecimal</code>. | ||
155 | */ | ||
156 | def private isBigDecimalRequired(Object... numbers) { return numbers.exists[it instanceof BigDecimal || it instanceof RealLiteral] } | ||
157 | def private dispatch BigDecimal asBigDecimal(IntLiteral i) { i.value.asBigDecimal } | ||
158 | def private dispatch BigDecimal asBigDecimal(RealLiteral i) { i.value.asBigDecimal } | ||
159 | def private dispatch BigDecimal asBigDecimal(Integer i) { BigDecimal.valueOf(i) } | ||
160 | def private dispatch BigDecimal asBigDecimal(BigDecimal i) { i } | ||
161 | def private dispatch Integer asInteger(Integer i) { i } | ||
162 | def private dispatch Integer asInteger(BigDecimal i) { i.intValue } | ||
163 | def private dispatch Integer asInteger(IntLiteral i) { i.value.asInteger } | ||
164 | |||
165 | // Atomic resoulutions | ||
166 | def protected dispatch Object resolve(IntLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value as Integer } | ||
167 | def protected dispatch Object resolve(BoolLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value } | ||
168 | def protected dispatch Object resolve(RealLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value as BigDecimal } | ||
169 | |||
170 | def protected dispatch Object resolve(Not not, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
171 | return ! (not.operand.resolve(interpretation,variableBinding) as Boolean) } | ||
172 | def protected dispatch Object resolve(And and, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
173 | //for(operand : and.operands) { | ||
174 | //val r = operand.resolve(interpretation,variableBinding) as Boolean | ||
175 | //println(r) | ||
176 | //} | ||
177 | return and.operands.forall[resolve(interpretation,variableBinding) as Boolean] as Boolean } | ||
178 | def protected dispatch Object resolve(Or or, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
179 | //val resolved = or.operands.map[resolve(interpretation,variableBinding) as Boolean] | ||
180 | //println(resolved) | ||
181 | return or.operands.exists[resolve(interpretation,variableBinding) as Boolean] } | ||
182 | def protected dispatch Object resolve(Impl impl, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
183 | val left = impl.leftOperand. resolve(interpretation,variableBinding) as Boolean | ||
184 | val right = impl.rightOperand.resolve(interpretation,variableBinding) as Boolean | ||
185 | return (! left) || (right) } | ||
186 | def protected dispatch Object resolve(Iff iff, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
187 | return (iff.leftOperand.resolve(interpretation,variableBinding) as Boolean) == | ||
188 | (iff.rightOperand.resolve(interpretation,variableBinding) as Boolean) } | ||
189 | def protected dispatch Object resolve(IfThenElse ite, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
190 | val condition = ite.condition.resolve(interpretation,variableBinding) as Boolean | ||
191 | if(condition) return ite.ifTrue.resolve(interpretation,variableBinding) | ||
192 | else return ite.ifFalse.resolve(interpretation,variableBinding) | ||
193 | } | ||
194 | def protected dispatch Object resolve(MoreThan moreThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
195 | val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
196 | val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
197 | if(isBigDecimalRequired(left,right)) { | ||
198 | return left.asBigDecimal.compareTo(right.asBigDecimal) > 0 } | ||
199 | else { return left.asInteger > right.asInteger } } | ||
200 | def protected dispatch Object resolve(LessThan lessThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
201 | val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
202 | val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
203 | if(isBigDecimalRequired(left,right)) { | ||
204 | return left.asBigDecimal.compareTo(right.asBigDecimal) < 0 } | ||
205 | else { return left.asInteger < right.asInteger } } | ||
206 | def protected dispatch Object resolve(MoreOrEqualThan moreThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
207 | val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
208 | val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
209 | if(isBigDecimalRequired(left,right)) { | ||
210 | return left.asBigDecimal.compareTo(right.asBigDecimal) >= 0 } | ||
211 | else { return left.asInteger >= right.asInteger } } | ||
212 | def protected dispatch Object resolve(LessOrEqualThan lessThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
213 | val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
214 | val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
215 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.compareTo(right.asBigDecimal) <= 0 | ||
216 | else { return left.asInteger <= right.asInteger } } | ||
217 | |||
218 | |||
219 | def protected dispatch Object resolve(Equals equals, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
220 | val left = equals.leftOperand.resolve(interpretation,variableBinding) | ||
221 | val right = equals.rightOperand.resolve(interpretation,variableBinding) | ||
222 | return compare(left,right) | ||
223 | } | ||
224 | def protected dispatch Object resolve(Distinct distinct, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
225 | val elements = distinct.operands.map[it.resolve(interpretation,variableBinding)] | ||
226 | if(elements.size== 0) return true | ||
227 | else { | ||
228 | val res = (0..<elements.size).forall[i | | ||
229 | (0..<i).forall[j| | ||
230 | ! this.compare(elements.get(i),elements.get(j))]] | ||
231 | //println('''«elements» = «res»''') | ||
232 | return res | ||
233 | } | ||
234 | |||
235 | //return elements.forall[x| elements.filter[it!=x].forall[y | x != y ]] | ||
236 | } | ||
237 | |||
238 | def protected dispatch Object resolve(Plus plus, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
239 | val left = plus.leftOperand.resolve(interpretation,variableBinding) as Number | ||
240 | val right = plus.rightOperand.resolve(interpretation,variableBinding) as Number | ||
241 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.add(right.asBigDecimal) | ||
242 | else return left.asInteger + right.asInteger | ||
243 | } | ||
244 | def protected dispatch Object resolve(Minus minus, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
245 | val left = minus.leftOperand.resolve(interpretation,variableBinding) as Number | ||
246 | val right = minus.rightOperand.resolve(interpretation,variableBinding) as Number | ||
247 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.subtract(right.asBigDecimal) | ||
248 | else return left.asInteger - right.asInteger | ||
249 | } | ||
250 | def protected dispatch Object resolve(Multiply multiply, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
251 | val left = multiply.leftOperand.resolve(interpretation,variableBinding) | ||
252 | val right = multiply.rightOperand.resolve(interpretation,variableBinding) | ||
253 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.multiply(right.asBigDecimal) | ||
254 | else return left.asInteger * right.asInteger | ||
255 | } | ||
256 | def protected dispatch Object resolve(Divison divide, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
257 | val left = divide.leftOperand.resolve(interpretation,variableBinding) as Number | ||
258 | val right = divide.rightOperand.resolve(interpretation,variableBinding) as Number | ||
259 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.divide(right.asBigDecimal) | ||
260 | return left.asInteger / right.asInteger | ||
261 | } | ||
262 | def protected dispatch Object resolve(Mod modulo, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
263 | val left = modulo.leftOperand.resolve(interpretation,variableBinding) as Number | ||
264 | val right = modulo.rightOperand.resolve(interpretation,variableBinding) as Number | ||
265 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.remainder(right.asBigDecimal) | ||
266 | else return left.asInteger % right.asInteger | ||
267 | } | ||
268 | |||
269 | def protected dispatch Object resolve(Exists exists, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
270 | executeExists(exists.expression,interpretation,variableBinding,exists.quantifiedVariables) } | ||
271 | def protected dispatch Object resolve(Forall forall, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
272 | executeForall(forall.expression,interpretation,variableBinding,forall.quantifiedVariables) } | ||
273 | |||
274 | def protected dispatch Object resolve(SymbolicValue symbolicValue, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
275 | val referenced = symbolicValue.symbolicReference | ||
276 | if(referenced instanceof DefinedElement) { | ||
277 | return referenced | ||
278 | } else if(referenced instanceof Variable) { | ||
279 | return variableBinding.get(referenced) | ||
280 | } else if(referenced instanceof FunctionDeclaration) { | ||
281 | val parameterSubstitution = new ArrayList<Object> | ||
282 | if(! symbolicValue.parameterSubstitutions.empty) { | ||
283 | for(place : 0..symbolicValue.parameterSubstitutions.size-1) { | ||
284 | val variable = symbolicValue.parameterSubstitutions.get(place) | ||
285 | parameterSubstitution += variable.resolve(interpretation,variableBinding) | ||
286 | } | ||
287 | } | ||
288 | return interpretation.getInterpretation(referenced,parameterSubstitution) | ||
289 | } else if(referenced instanceof FunctionDefinition) { | ||
290 | val parameterSubstitution = new HashMap<Variable,Object>() | ||
291 | for(place: 0..<referenced.variable.size) { | ||
292 | parameterSubstitution.put( | ||
293 | referenced.variable.get(place), | ||
294 | symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding)) | ||
295 | } | ||
296 | return referenced.value.resolve(interpretation,parameterSubstitution) | ||
297 | } else if(referenced instanceof RelationDeclaration) { | ||
298 | val parameterSubstitunion = new ArrayList<Object> | ||
299 | if(! symbolicValue.parameterSubstitutions.empty) { | ||
300 | for(place : 0..symbolicValue.parameterSubstitutions.size-1) { | ||
301 | val variable = symbolicValue.parameterSubstitutions.get(place) | ||
302 | parameterSubstitunion += variable.resolve(interpretation,variableBinding) | ||
303 | } | ||
304 | } | ||
305 | return (interpretation.getInterpretation(referenced,parameterSubstitunion) as Boolean) | ||
306 | } else if(referenced instanceof RelationDefinition) { | ||
307 | val parameterSubstitution = new HashMap<Variable,Object>() | ||
308 | for(place: 0..<referenced.variables.size) { | ||
309 | parameterSubstitution.put( | ||
310 | referenced.variables.get(place), | ||
311 | symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding)) | ||
312 | } | ||
313 | return referenced.value.resolve(interpretation,parameterSubstitution) | ||
314 | } else if(referenced instanceof ConstantDeclaration) { | ||
315 | return interpretation.getInterpretation(referenced) | ||
316 | } else if(referenced instanceof ConstantDefinition) { | ||
317 | return referenced.value.resolve(interpretation,Collections.emptyMap); | ||
318 | } else throw new IllegalArgumentException('''Unknown referred symbol: «referenced»''') | ||
319 | } | ||
320 | |||
321 | // TermDescriptions are reduced to terms | ||
322 | def protected dispatch resolve(Variable variable, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
323 | return variableBinding.get(variable) | ||
324 | } | ||
325 | |||
326 | def protected dispatch resolve(DefinedElement definedElement, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
327 | return definedElement | ||
328 | } | ||
329 | |||
330 | def private compare(Object left, Object right) { | ||
331 | if(left instanceof Number && right instanceof Number) { | ||
332 | if(isBigDecimalRequired(left as Number,right as Number)) { | ||
333 | return (left as Number).asBigDecimal.compareTo((right as Number).asBigDecimal) == 0 | ||
334 | } else { | ||
335 | return (left as Number).asInteger == (right as Number).asInteger | ||
336 | } | ||
337 | } else return left.equals(right) | ||
338 | } | ||
339 | |||
340 | def allIntegers(LogicModelInterpretation interpretation) { | ||
341 | if(interpretation.minimalInteger <= interpretation.maximalInteger) { | ||
342 | (interpretation.minimalInteger .. interpretation.maximalInteger).map[asInteger] | ||
343 | } else return emptySet | ||
344 | } | ||
345 | |||
346 | def private boolean executeExists( | ||
347 | Term expression, | ||
348 | LogicModelInterpretation interpretation, | ||
349 | Map<Variable,Object> variableBinding, | ||
350 | List<Variable> variablesToBind) | ||
351 | { | ||
352 | if(variablesToBind.empty) { | ||
353 | val res = expression.resolve(interpretation,variableBinding) as Boolean | ||
354 | return res | ||
355 | } | ||
356 | else { | ||
357 | val unfoldedVariable = variablesToBind.head | ||
358 | val possibleValuesType = unfoldedVariable.range | ||
359 | if(possibleValuesType instanceof ComplexTypeReference) { | ||
360 | return this.getElements(interpretation,possibleValuesType.referred).exists[newBinding | | ||
361 | executeExists( | ||
362 | expression, | ||
363 | interpretation, | ||
364 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
365 | variablesToBind.subList(1,variablesToBind.size))] | ||
366 | } else if(possibleValuesType instanceof IntTypeReference) { | ||
367 | return interpretation.allIntegers.exists[newBinding | | ||
368 | executeExists( | ||
369 | expression, | ||
370 | interpretation, | ||
371 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
372 | variablesToBind.subList(1,variablesToBind.size))] | ||
373 | } | ||
374 | else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''') | ||
375 | } | ||
376 | } | ||
377 | |||
378 | def private boolean executeForall( | ||
379 | Term expression, | ||
380 | LogicModelInterpretation interpretation, | ||
381 | Map<Variable,Object> variableBinding, | ||
382 | List<Variable> variablesToBind) | ||
383 | { | ||
384 | if(variablesToBind.empty) { | ||
385 | return expression.resolve(interpretation,variableBinding) as Boolean | ||
386 | } | ||
387 | else { | ||
388 | val unfoldedVariable = variablesToBind.head | ||
389 | val possibleValuesType = unfoldedVariable.range | ||
390 | if(possibleValuesType instanceof ComplexTypeReference) { | ||
391 | return this.getElements(interpretation,possibleValuesType.referred).forall[newBinding | | ||
392 | executeForall( | ||
393 | expression, | ||
394 | interpretation, | ||
395 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
396 | variablesToBind.subList(1,variablesToBind.size))] | ||
397 | } else if(possibleValuesType instanceof IntTypeReference) { | ||
398 | return interpretation.allIntegers.forall[newBinding | | ||
399 | executeForall( | ||
400 | expression, | ||
401 | interpretation, | ||
402 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
403 | variablesToBind.subList(1,variablesToBind.size))] | ||
404 | } else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''') | ||
405 | } | ||
406 | } | ||
407 | } \ No newline at end of file | ||