diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 14:01:15 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-07-05 14:01:15 +0200 |
commit | 7fd74f53db81394d45535bec6cedc749222955eb (patch) | |
tree | 6ffb6b07d6c63125a42e72587ad7d26bd333123c /Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf | |
parent | SMT solver implementation of multiple model generation (diff) | |
download | VIATRA-Generator-7fd74f53db81394d45535bec6cedc749222955eb.tar.gz VIATRA-Generator-7fd74f53db81394d45535bec6cedc749222955eb.tar.zst VIATRA-Generator-7fd74f53db81394d45535bec6cedc749222955eb.zip |
When there is a definition to a declaration in the logic problem, the
logic structure builder calls the definition when the interpretation of
the declaration is requested.
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend | 144 |
1 files changed, 95 insertions, 49 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 index b3e44b46..760aa8b8 100644 --- 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 | |||
@@ -51,9 +51,10 @@ import java.util.HashMap | |||
51 | import java.util.LinkedList | 51 | import java.util.LinkedList |
52 | import java.util.List | 52 | import java.util.List |
53 | import java.util.Map | 53 | import java.util.Map |
54 | import org.eclipse.xtend.lib.annotations.Data | ||
54 | 55 | ||
55 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 56 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
56 | import org.eclipse.xtend.lib.annotations.Data | 57 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf |
57 | 58 | ||
58 | @Data class InterpretationValidationResult { | 59 | @Data class InterpretationValidationResult { |
59 | val List<String> problems; | 60 | val List<String> problems; |
@@ -81,7 +82,7 @@ class LogicStructureBuilder{ | |||
81 | * @param term An expression which results in a logic element. | 82 | * @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 | * @return The logic element value of the expression. Returns the element directly, not a symbolic reference! |
83 | */ | 84 | */ |
84 | def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.resolve(interpretation,emptyMap) as DefinedElement} | 85 | def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.toTerm.resolve(interpretation,emptyMap) as DefinedElement} |
85 | /** | 86 | /** |
86 | * Checks if the interpretation is a valid solution of the problem by checking the satisfactions of each assertion. | 87 | * 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 | * Returns the collection of failed assertions. |
@@ -266,6 +267,19 @@ class LogicStructureBuilder{ | |||
266 | else return left.asInteger % right.asInteger | 267 | else return left.asInteger % right.asInteger |
267 | } | 268 | } |
268 | 269 | ||
270 | def protected dispatch Object resolve(InstanceOf instanceOf, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
271 | val typeReference = instanceOf.range | ||
272 | if(typeReference instanceof ComplexTypeReference) { | ||
273 | val elements = this.getElements(interpretation,typeReference.referred) | ||
274 | val element = instanceOf.value.resolve(interpretation,variableBinding) | ||
275 | if(element instanceof DefinedElement) { | ||
276 | return elements.contains(element) | ||
277 | } else throw new AssertionError('''InstanceOf with «element.class.simpleName» object''') | ||
278 | } else { | ||
279 | throw new AssertionError('''InstanceOf with «typeReference.class.simpleName» reference''') | ||
280 | } | ||
281 | } | ||
282 | |||
269 | def protected dispatch Object resolve(Exists exists, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | 283 | def protected dispatch Object resolve(Exists exists, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { |
270 | executeExists(exists.expression,interpretation,variableBinding,exists.quantifiedVariables) } | 284 | executeExists(exists.expression,interpretation,variableBinding,exists.quantifiedVariables) } |
271 | def protected dispatch Object resolve(Forall forall, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | 285 | def protected dispatch Object resolve(Forall forall, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { |
@@ -273,58 +287,90 @@ class LogicStructureBuilder{ | |||
273 | 287 | ||
274 | def protected dispatch Object resolve(SymbolicValue symbolicValue, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | 288 | def protected dispatch Object resolve(SymbolicValue symbolicValue, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { |
275 | val referenced = symbolicValue.symbolicReference | 289 | val referenced = symbolicValue.symbolicReference |
276 | if(referenced instanceof DefinedElement) { | 290 | return referenced.resolveSymbolicValue(interpretation,symbolicValue.parameterSubstitutions,variableBinding) |
277 | return referenced | 291 | } |
278 | } else if(referenced instanceof Variable) { | 292 | |
279 | return variableBinding.get(referenced) | 293 | protected dispatch def Object resolveSymbolicValue(DefinedElement element, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { |
280 | } else if(referenced instanceof FunctionDeclaration) { | 294 | return element |
281 | val parameterSubstitution = new ArrayList<Object> | 295 | } |
282 | if(! symbolicValue.parameterSubstitutions.empty) { | 296 | protected dispatch def Object resolveSymbolicValue(Variable variable, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { |
283 | for(place : 0..symbolicValue.parameterSubstitutions.size-1) { | 297 | return variable.lookup(variableBinding) |
284 | val variable = symbolicValue.parameterSubstitutions.get(place) | 298 | } |
285 | parameterSubstitution += variable.resolve(interpretation,variableBinding) | 299 | protected dispatch def Object resolveSymbolicValue(FunctionDeclaration declaration, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { |
286 | } | 300 | val internalDefinition = hasDefined(declaration) |
287 | } | 301 | if(internalDefinition === null) { |
288 | return interpretation.getInterpretation(referenced,parameterSubstitution) | 302 | interpretation.getInterpretation(declaration,createBinding2(parameterSubstitution, interpretation, variableBinding)) |
289 | } else if(referenced instanceof FunctionDefinition) { | 303 | } else { |
290 | val parameterSubstitution = new HashMap<Variable,Object>() | 304 | internalDefinition.resolveSymbolicValue(interpretation,parameterSubstitution,variableBinding) |
291 | for(place: 0..<referenced.variable.size) { | 305 | } |
292 | parameterSubstitution.put( | 306 | } |
293 | referenced.variable.get(place), | 307 | protected dispatch def Object resolveSymbolicValue(FunctionDefinition definition, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { |
294 | symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding)) | 308 | return definition.value.resolve(interpretation,createBinding(interpretation,variableBinding,definition.variable,parameterSubstitution)) |
309 | } | ||
310 | protected dispatch def Object resolveSymbolicValue(ConstantDeclaration declaration, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { | ||
311 | val internalDefinition = hasDefined(declaration) | ||
312 | if(internalDefinition === null) { | ||
313 | return interpretation.getInterpretation(declaration) | ||
314 | } else { | ||
315 | return internalDefinition.resolveSymbolicValue(interpretation,parameterSubstitution,variableBinding) | ||
316 | } | ||
317 | } | ||
318 | protected dispatch def Object resolveSymbolicValue(ConstantDefinition definition, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { | ||
319 | return definition.value.resolve(interpretation,emptyMap) | ||
320 | } | ||
321 | protected dispatch def Object resolveSymbolicValue(RelationDeclaration declaration, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { | ||
322 | val internalDefinition = hasDefined(declaration) | ||
323 | if(internalDefinition === null) { | ||
324 | interpretation.getInterpretation(declaration,createBinding2(parameterSubstitution, interpretation, variableBinding)) | ||
325 | } else { | ||
326 | internalDefinition.resolveSymbolicValue(interpretation,parameterSubstitution,variableBinding) | ||
327 | } | ||
328 | } | ||
329 | protected dispatch def Object resolveSymbolicValue(RelationDefinition definition, LogicModelInterpretation interpretation, List<? extends Term> parameterSubstitution, Map<Variable,Object> variableBinding) { | ||
330 | return definition.value.resolve(interpretation,createBinding(interpretation,variableBinding,definition.variables,parameterSubstitution)) | ||
331 | } | ||
332 | |||
333 | private def hasDefined(RelationDeclaration declaration) { | ||
334 | val container = declaration.eContainer | ||
335 | if(container instanceof LogicProblem) { | ||
336 | val internalDefinitions = container.relations.filter(RelationDefinition).filter[it.defines === declaration] | ||
337 | if(!internalDefinitions.empty) { | ||
338 | return internalDefinitions.head | ||
295 | } | 339 | } |
296 | return referenced.value.resolve(interpretation,parameterSubstitution) | 340 | } |
297 | } else if(referenced instanceof RelationDeclaration) { | 341 | return null |
298 | val parameterSubstitunion = new ArrayList<Object> | 342 | } |
299 | if(! symbolicValue.parameterSubstitutions.empty) { | 343 | private def hasDefined(FunctionDeclaration declaration) { |
300 | for(place : 0..symbolicValue.parameterSubstitutions.size-1) { | 344 | val container = declaration.eContainer |
301 | val variable = symbolicValue.parameterSubstitutions.get(place) | 345 | if(container instanceof LogicProblem) { |
302 | parameterSubstitunion += variable.resolve(interpretation,variableBinding) | 346 | val internalDefinitions = container.relations.filter(FunctionDefinition).filter[it.defines === declaration] |
303 | } | 347 | if(!internalDefinitions.empty) { |
348 | return internalDefinitions.head | ||
304 | } | 349 | } |
305 | return (interpretation.getInterpretation(referenced,parameterSubstitunion) as Boolean) | 350 | } |
306 | } else if(referenced instanceof RelationDefinition) { | 351 | return null |
307 | val parameterSubstitution = new HashMap<Variable,Object>() | 352 | } |
308 | for(place: 0..<referenced.variables.size) { | 353 | private def hasDefined(ConstantDeclaration declaration) { |
309 | parameterSubstitution.put( | 354 | val container = declaration.eContainer |
310 | referenced.variables.get(place), | 355 | if(container instanceof LogicProblem) { |
311 | symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding)) | 356 | val internalDefinitions = container.relations.filter(ConstantDefinition).filter[it.defines === declaration] |
357 | if(!internalDefinitions.empty) { | ||
358 | return internalDefinitions.head | ||
312 | } | 359 | } |
313 | return referenced.value.resolve(interpretation,parameterSubstitution) | 360 | } |
314 | } else if(referenced instanceof ConstantDeclaration) { | 361 | return null |
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 | } | 362 | } |
320 | 363 | private def createBinding(LogicModelInterpretation interpretation, Map<Variable,Object> previousVariableBinding, List<Variable> definitionVariables, List<? extends Term> parameterSubstitution){ | |
321 | // TermDescriptions are reduced to terms | 364 | val binding = new HashMap<Variable,Object>(previousVariableBinding) |
322 | def protected dispatch resolve(Variable variable, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | 365 | for(place: 0..<definitionVariables.size) { |
323 | return variableBinding.get(variable) | 366 | binding.put( |
367 | definitionVariables.get(place), | ||
368 | parameterSubstitution.get(place).resolve(interpretation,previousVariableBinding)) | ||
369 | } | ||
370 | return binding | ||
324 | } | 371 | } |
325 | 372 | private def List<Object> createBinding2(List<? extends Term> parameterSubstitution, LogicModelInterpretation interpretation, Map<Variable, Object> variableBinding) { | |
326 | def protected dispatch resolve(DefinedElement definedElement, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | 373 | parameterSubstitution.map[it.resolve(interpretation,variableBinding)] |
327 | return definedElement | ||
328 | } | 374 | } |
329 | 375 | ||
330 | def private compare(Object left, Object right) { | 376 | def private compare(Object left, Object right) { |