aboutsummaryrefslogtreecommitdiffstats
path: root/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
Migrating Additional projects
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.xtend407
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 @@
1package hu.bme.mit.inf.dslreasoner.logic.model.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
24import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
31import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
32import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
33import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
34import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
35import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
36import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
37import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration
38import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
39import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
40import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription
41import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
42import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
43import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
44import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
45import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
46import java.math.BigDecimal
47import java.util.ArrayList
48import java.util.Collection
49import java.util.Collections
50import java.util.HashMap
51import java.util.LinkedList
52import java.util.List
53import java.util.Map
54
55import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
56import 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
64class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-02 20:32:06 +0000