From 7fd74f53db81394d45535bec6cedc749222955eb Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 5 Jul 2017 14:01:15 +0200 Subject: 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. --- .../model/builder/LogicStructureBuilder.xtend | 144 ++++++++++++++------- 1 file changed, 95 insertions(+), 49 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu') 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 import java.util.LinkedList import java.util.List import java.util.Map +import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import org.eclipse.xtend.lib.annotations.Data +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf @Data class InterpretationValidationResult { val List problems; @@ -81,7 +82,7 @@ class LogicStructureBuilder{ * @param term An expression which results in a logic element. * @return The logic element value of the expression. Returns the element directly, not a symbolic reference! */ - def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.resolve(interpretation,emptyMap) as DefinedElement} + def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.toTerm.resolve(interpretation,emptyMap) as DefinedElement} /** * Checks if the interpretation is a valid solution of the problem by checking the satisfactions of each assertion. * Returns the collection of failed assertions. @@ -266,6 +267,19 @@ class LogicStructureBuilder{ else return left.asInteger % right.asInteger } + def protected dispatch Object resolve(InstanceOf instanceOf, LogicModelInterpretation interpretation, Map variableBinding) { + val typeReference = instanceOf.range + if(typeReference instanceof ComplexTypeReference) { + val elements = this.getElements(interpretation,typeReference.referred) + val element = instanceOf.value.resolve(interpretation,variableBinding) + if(element instanceof DefinedElement) { + return elements.contains(element) + } else throw new AssertionError('''InstanceOf with «element.class.simpleName» object''') + } else { + throw new AssertionError('''InstanceOf with «typeReference.class.simpleName» reference''') + } + } + def protected dispatch Object resolve(Exists exists, LogicModelInterpretation interpretation, Map variableBinding) { executeExists(exists.expression,interpretation,variableBinding,exists.quantifiedVariables) } def protected dispatch Object resolve(Forall forall, LogicModelInterpretation interpretation, Map variableBinding) { @@ -273,58 +287,90 @@ class LogicStructureBuilder{ def protected dispatch Object resolve(SymbolicValue symbolicValue, LogicModelInterpretation interpretation, Map variableBinding) { val referenced = symbolicValue.symbolicReference - if(referenced instanceof DefinedElement) { - return referenced - } else if(referenced instanceof Variable) { - return variableBinding.get(referenced) - } else if(referenced instanceof FunctionDeclaration) { - val parameterSubstitution = new ArrayList - if(! symbolicValue.parameterSubstitutions.empty) { - for(place : 0..symbolicValue.parameterSubstitutions.size-1) { - val variable = symbolicValue.parameterSubstitutions.get(place) - parameterSubstitution += variable.resolve(interpretation,variableBinding) - } - } - return interpretation.getInterpretation(referenced,parameterSubstitution) - } else if(referenced instanceof FunctionDefinition) { - val parameterSubstitution = new HashMap() - for(place: 0.. parameterSubstitution, Map variableBinding) { + return element + } + protected dispatch def Object resolveSymbolicValue(Variable variable, LogicModelInterpretation interpretation, List parameterSubstitution, Map variableBinding) { + return variable.lookup(variableBinding) + } + protected dispatch def Object resolveSymbolicValue(FunctionDeclaration declaration, LogicModelInterpretation interpretation, List parameterSubstitution, Map variableBinding) { + val internalDefinition = hasDefined(declaration) + if(internalDefinition === null) { + interpretation.getInterpretation(declaration,createBinding2(parameterSubstitution, interpretation, variableBinding)) + } else { + internalDefinition.resolveSymbolicValue(interpretation,parameterSubstitution,variableBinding) + } + } + protected dispatch def Object resolveSymbolicValue(FunctionDefinition definition, LogicModelInterpretation interpretation, List parameterSubstitution, Map variableBinding) { + return definition.value.resolve(interpretation,createBinding(interpretation,variableBinding,definition.variable,parameterSubstitution)) + } + protected dispatch def Object resolveSymbolicValue(ConstantDeclaration declaration, LogicModelInterpretation interpretation, List parameterSubstitution, Map variableBinding) { + val internalDefinition = hasDefined(declaration) + if(internalDefinition === null) { + return interpretation.getInterpretation(declaration) + } else { + return internalDefinition.resolveSymbolicValue(interpretation,parameterSubstitution,variableBinding) + } + } + protected dispatch def Object resolveSymbolicValue(ConstantDefinition definition, LogicModelInterpretation interpretation, List parameterSubstitution, Map variableBinding) { + return definition.value.resolve(interpretation,emptyMap) + } + protected dispatch def Object resolveSymbolicValue(RelationDeclaration declaration, LogicModelInterpretation interpretation, List parameterSubstitution, Map variableBinding) { + val internalDefinition = hasDefined(declaration) + if(internalDefinition === null) { + interpretation.getInterpretation(declaration,createBinding2(parameterSubstitution, interpretation, variableBinding)) + } else { + internalDefinition.resolveSymbolicValue(interpretation,parameterSubstitution,variableBinding) + } + } + protected dispatch def Object resolveSymbolicValue(RelationDefinition definition, LogicModelInterpretation interpretation, List parameterSubstitution, Map variableBinding) { + return definition.value.resolve(interpretation,createBinding(interpretation,variableBinding,definition.variables,parameterSubstitution)) + } + + private def hasDefined(RelationDeclaration declaration) { + val container = declaration.eContainer + if(container instanceof LogicProblem) { + val internalDefinitions = container.relations.filter(RelationDefinition).filter[it.defines === declaration] + if(!internalDefinitions.empty) { + return internalDefinitions.head } - return referenced.value.resolve(interpretation,parameterSubstitution) - } else if(referenced instanceof RelationDeclaration) { - val parameterSubstitunion = new ArrayList - if(! symbolicValue.parameterSubstitutions.empty) { - for(place : 0..symbolicValue.parameterSubstitutions.size-1) { - val variable = symbolicValue.parameterSubstitutions.get(place) - parameterSubstitunion += variable.resolve(interpretation,variableBinding) - } + } + return null + } + private def hasDefined(FunctionDeclaration declaration) { + val container = declaration.eContainer + if(container instanceof LogicProblem) { + val internalDefinitions = container.relations.filter(FunctionDefinition).filter[it.defines === declaration] + if(!internalDefinitions.empty) { + return internalDefinitions.head } - return (interpretation.getInterpretation(referenced,parameterSubstitunion) as Boolean) - } else if(referenced instanceof RelationDefinition) { - val parameterSubstitution = new HashMap() - for(place: 0.. variableBinding) { - return variableBinding.get(variable) + private def createBinding(LogicModelInterpretation interpretation, Map previousVariableBinding, List definitionVariables, List parameterSubstitution){ + val binding = new HashMap(previousVariableBinding) + for(place: 0.. variableBinding) { - return definedElement + private def List createBinding2(List parameterSubstitution, LogicModelInterpretation interpretation, Map variableBinding) { + parameterSubstitution.map[it.resolve(interpretation,variableBinding)] } def private compare(Object left, Object right) { -- cgit v1.2.3-54-g00ecf