From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../model/builder/LogicModelInterpretation.xtend | 102 ++++ .../logic/model/builder/LogicProblemBuilder.xtend | 563 +++++++++++++++++++++ .../logic/model/builder/LogicSolver.xtend | 47 ++ .../model/builder/LogicStructureBuilder.xtend | 407 +++++++++++++++ .../logic/model/builder/TracedLogicProblem.xtend | 26 + .../logic/model/builder/TracedOutput.xtend | 6 + .../logic/model/builder/VariableContext.xtend | 33 ++ .../TypeConsistencyChecker.xtend | 75 +++ .../model/statistics/StatisticSections2CSV.xtend | 89 ++++ .../model/statistics/StatisticSections2Print.xtend | 23 + .../mit/inf/dslreasoner/util/CollectionsUtil.xtend | 82 +++ .../LogicProblemBuilder_AdvancedConstructs.xtend | 71 +++ .../util/SetWithCustomEquivalence.xtend | 103 ++++ .../util/visualisation/Interpretation2Gml.xtend | 5 + .../workspace/FileSystemWorkspace.xtend | 74 +++ .../dslreasoner/workspace/ProjectWorkspace.xtend | 105 ++++ .../dslreasoner/workspace/ReasonerWorkspace.xtend | 100 ++++ 17 files changed, 1911 insertions(+) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicStructureBuilder.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedLogicProblem.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedOutput.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/VariableContext.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/consistencychecker/TypeConsistencyChecker.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/CollectionsUtil.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/LogicProblemBuilder_AdvancedConstructs.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/SetWithCustomEquivalence.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/visualisation/Interpretation2Gml.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/FileSystemWorkspace.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ProjectWorkspace.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ReasonerWorkspace.xtend (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend new file mode 100644 index 00000000..a2d30b1b --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicModelInterpretation.xtend @@ -0,0 +1,102 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import java.util.List + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +interface LogicModelInterpretation{ + + /** + * Returns the elements of a type. + */ + def List getElements(Type type) + /** + * Returns the interpretation of a function. The parameters and the return values are encoded to primitive java objects defined by the following table: + *

+ * + * + * + * + * + *
Term typeJava object type
Element of a type DefinedElement
Boolean literal Boolean
Integer literal Integer
Real literal BigDecimal

+ * @param function The target function to be interpreted. + * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table. + * @return The result of the function call encoded as defined in the table. + */ + def Object getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) + /** + * Returns the interpretation of a relation. The parameters are encoded to primitive java objects defined by the following table: + *

+ * + * + * + * + * + *
Term typeJava object type
Element of a type DefinedElement
Boolean literal Boolean
Integer literal Integer
Real literal BigDecimal

+ * @param relation The target relation to be interpreted. + * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table. + * @return If the parameter tuple is in the relation. + */ + def boolean getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) + /** + * Returns the interpretation of a constant. The value is encoded to primitive java objects defined by the following table: + *

+ * + * + * + * + * + *
Term typeJava object type
Element of a type DefinedElement
Boolean literal Boolean
Integer literal Integer
Real literal BigDecimal

+ * @param constant The target constant to be interpreted. + * @return The value of the constant encoded as specified in the table. + */ + def Object getInterpretation(ConstantDeclaration constant) + def int getMinimalInteger() + def int getMaximalInteger() +} + +class Uninterpreted implements LogicModelInterpretation { + /*private val static unknownBecauseUninterpreted = LogiclanguageFactory.eINSTANCE.createUnknownBecauseUninterpreted + public def static getUnknownBecauseUninterpreted() {return Uninterpreted.unknownBecauseUninterpreted}*/ + + override getElements(Type type) { + throw new UnsupportedOperationException("The interpteration is unknown.") + } + + def getKnownElements(Type type) { + val allSubtypes = type.transitiveClosureStar[it.subtypes] + return allSubtypes.filter(TypeDefinition).map[elements].flatten.toList + } + + def allElementsAreInterpreted(Type type) { + val allSubtypes = type.transitiveClosureStar[it.subtypes] + return allSubtypes.exists[it instanceof TypeDeclaration] + } + + override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { + throw new UnsupportedOperationException("The interpteration is unknown.") + } + + override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { + throw new UnsupportedOperationException("The interpteration is unknown.") + } + + override getInterpretation(ConstantDeclaration constant) { + throw new UnsupportedOperationException("The interpteration is unknown.") + } + + override getMinimalInteger() { + throw new UnsupportedOperationException("The interpteration is unknown.") + } + + override getMaximalInteger() { + throw new UnsupportedOperationException("The interpteration is unknown.") + } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend new file mode 100644 index 00000000..ba1b9fd6 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend @@ -0,0 +1,563 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemFactory +import hu.bme.mit.inf.dslreasoner.util.LogicProblemBuilder_AdvancedConstructs +import java.math.BigDecimal +import java.util.ArrayList +import java.util.Collections +import java.util.LinkedList +import java.util.List +import java.util.Map +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.xtext.xbase.lib.Functions.Function1 + +@Data class FunctionDescription { + Iterable parameters + TypeReference range +} + +class LogicProblemBuilderException extends Exception { + new(String reason) { + super(reason) + } +} + +public class LogicProblemBuilder{ + val protected extension LogiclanguageFactory logicFactiory = LogiclanguageFactory.eINSTANCE + val protected extension LogicproblemFactory problemFactory = LogicproblemFactory.eINSTANCE + val protected advancedConstructs = new LogicProblemBuilder_AdvancedConstructs(this) + + def public createProblem(){ createLogicProblem } + + // Names + def protected String canonize(CharSequence name) { + if(name == null) return "" + val result = name.toString.split("\\s+"); + if(result.size == 1) { + val element = result.get(0); + if(element == "bool" || + element == "int" || + element == "real") throw new LogicProblemBuilderException('''Reserved keyword "«element»"!''') + else return result.join(' ') + } + else return result.join(' ') + } + def protected String generateUniqueName(Iterable previous, Function1 namer) { + var int i = 0 + var generateNew = false; + var String finalName; + do { + i = i+1; + val nameCandidate = namer.apply(i) + finalName = nameCandidate + generateNew = previous.exists[equals(nameCandidate)] + } + while(generateNew) + return finalName + } + + // Type builders + def public Element(CharSequence elementName) { return createDefinedElement => [x|x.name = elementName.canonize] } + def public Element() { return createDefinedElement } + def public TypeDeclaration(CharSequence name, boolean isAbstract) { TypeDeclaration => [x | x.name = name.canonize x.isAbstract = isAbstract] } + def public TypeDeclaration() { createTypeDeclaration } + def public TypeDefinition(CharSequence name, boolean isAbstract, DefinedElement... elements) { TypeDefinition(name, isAbstract, elements as Iterable) } + def public TypeDefinition(CharSequence name, boolean isAbstract, Iterable elements) { createTypeDefinition => [x | x.name = name.canonize x.isAbstract = isAbstract x.elements += elements ] } + + def public Supertype(Type subtype, Type supertype) { + subtype.supertypes+=supertype + } + def public SetSupertype(Type subtype, Type supertype, boolean value) { + if(value) subtype.supertypes+=supertype + else subtype.subtypes-=supertype + } + + // Type add + def public add(LogicProblem problem, Type type) { + problem.nameIfAnonymType(type) + problem.types+=type + if(type instanceof TypeDefinition) { + problem.elements+=type.elements + } + return type + } + def protected dispatch nameIfAnonymType(LogicProblem problem, Type typeDeclaration) { + if(typeDeclaration.name.nullOrEmpty) + typeDeclaration.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»'''] + } + def protected dispatch nameIfAnonymType(LogicProblem problem, TypeDefinition typeDefinition) { + if(typeDefinition.name.nullOrEmpty) + typeDefinition.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»'''] + for(element : typeDefinition.elements) + if(element.name.nullOrEmpty) + element.name = typeDefinition.elements.map[it.name].generateUniqueName[i | '''type «i.toString»'''] + } + + def public LogicBool() { createBoolTypeReference } + def public LogicInt() { createIntTypeReference } + def public LogicReal() { createRealTypeReference } + def toTypeReference(TypeDescriptor descriptor) { + if(descriptor instanceof TypeReference) { return EcoreUtil.copy(descriptor); } + else if(descriptor instanceof Type) { return createComplexTypeReference => [referred = descriptor]} + else throw new UnsupportedOperationException("Unsupported type descriptor: " + descriptor.class) + } + + // Variables + def public createVar(CharSequence name, TypeDescriptor range) { + return createVariable => [it.name = name.canonize it.range = range.toTypeReference] + } + + // Functions + def public FunctionDescription ->(TypeDescriptor parameter, TypeDescriptor range) { return #[parameter] -> range } + def public FunctionDescription ->(Iterable parameters, TypeDescriptor range) { return new FunctionDescription(parameters.map[toTypeReference], range.toTypeReference); } + def public FunctionDeclaration(CharSequence name, FunctionDescription functionDescription) { FunctionDeclaration(name,functionDescription.range, functionDescription.parameters) } + def public FunctionDeclaration(FunctionDescription functionDescription) { FunctionDeclaration(functionDescription.range, functionDescription.parameters) } + def public FunctionDeclaration(CharSequence name, TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(name, range, parameters as Iterable) } + def public FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable) } + def public FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] } + def public FunctionDeclaration(TypeDescriptor range, Iterable parameters) { + val function = createFunctionDeclaration + for(parameter : parameters) function.parameters+=parameter.toTypeReference + function.range = range.toTypeReference + return function + } + + def public FunctionDefinition(CharSequence name, TypeDescriptor range, Function1 expression) { + val context = new VariableContext(this,logicFactiory) + val definition = expression.apply(context) + return FunctionDefinition(name,range,context.variables,definition); + } + def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable variables, TermDescription definition) { + return createFunctionDefinition => [ + it.name = name.canonize + it.parameters += variables.map[it.range.toTypeReference] + it.variable += variables + it.range = range.toTypeReference + it.value = definition.toTerm + ] + } + def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable parameters, Map,Term> parametersToValue) { + return FunctionDefinition(name,range,parameters,parametersToValue,null) + } + def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable parameters, Map,Term> parametersToValue, Term defaultValue) { + val parameterList = parameters.toList; + val variableList = (1..parameterList.size).map[index | '''param «index»'''.createVar(parameterList.get(index-1))].toList + return FunctionDefinition(name,range,variableList,advancedConstructs.FunctionDefinitionBody(variableList,parametersToValue,defaultValue)) + } + + // Add function to a problem + def public add(LogicProblem input, Function function) { + input.nameIfAnonymFunction(function) + input.checkFunction(function) + input.functions += function + return function + } + def public add(LogicProblem input, FunctionDescription functionDescription) { input.add(FunctionDeclaration(functionDescription)) } + def protected nameIfAnonymFunction(LogicProblem problem, Function functionDeclaration) { + if(functionDeclaration.name.nullOrEmpty) { + functionDeclaration.name = problem.functions.map[it.name].generateUniqueName[i | "function"+i] + } + } + def protected checkFunction(LogicProblem problem, Function function) { + if(problem.functions.exists(x|x.name == function.name)) + throw new LogicProblemBuilderException('''Function with the following name is already defined: "«function.name»"!''') + for(ref : function.parameters.filter(typeof(ComplexTypeReference)).map[referred]) { + if(!problem.types.contains(ref)) + throw new LogicProblemBuilderException('''Type "«ref.name»" is not availabe in the logic problem!''') + } + val range = function.range + if(range instanceof ComplexTypeReference) { + if(!problem.types.contains(range.referred)) + throw new LogicProblemBuilderException('''Type "«range.referred.name»" is not availabe in the logic problem!''') + } + } + + // Constants + def public ConstantDeclaration(CharSequence name, TypeDescriptor type) { ConstantDeclaration(type) => [it.name = name.canonize] } + def public ConstantDeclaration(TypeDescriptor type) { createConstantDeclaration => [it.type = type.toTypeReference] } + + def public ConstantDefinition(CharSequence name, TypeDescriptor type, TermDescription value) { + createConstantDefinition => [it.name = name.canonize it.type = type.toTypeReference it.value = value.toTerm] + } + + // Add constant to a problem + def public add(LogicProblem problem, Constant constant) { + problem.nameIfAnonymConstant(constant); + problem.checkConstant(constant) + problem.constants += constant + return constant + } + def protected nameIfAnonymConstant(LogicProblem problem, Constant constant) { + if(constant.name.nullOrEmpty) { + constant.name = problem.constants.map[it.name].generateUniqueName[i | "constant"+i] + } + } + def protected checkConstant(LogicProblem problem, Constant constant) { + if(problem.constants.exists(x|x.name == constant.name)) + throw new LogicProblemBuilderException('''Constant with the following name is already defined: "«constant.name»"!''') + if((constant.type instanceof ComplexTypeReference) && ! (problem.types.contains((constant.type as ComplexTypeReference).referred))) + throw new LogicProblemBuilderException('''Type "«(constant.type as ComplexTypeReference).referred.name»" is not availabe in the logic problem!''') + } + + // Relations + def public RelationDeclaration(CharSequence name, TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable) } + def public RelationDeclaration(CharSequence name, Iterable parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] } + def public RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable) } + def public RelationDeclaration(Iterable parameters) { + val relation = createRelationDeclaration + for(parameter : parameters) { + relation.parameters+=parameter.toTypeReference + } + return relation + } + + def public RelationDefinition(CharSequence name, Function1 expression) { + val context = new VariableContext(this,logicFactiory); + val definition = expression.apply(context); + return RelationDefinition(name,context.variables,definition) + } + def public RelationDefinition(CharSequence name, Iterable variables, TermDescription definition) { + return createRelationDefinition => [ + it.name = name.canonize + it.parameters += variables.map[it.range.toTypeReference] + it.variables += variables + it.value = definition?.toTerm + ] + } + def public RelationDefinition(CharSequence name, Iterable parameters, Iterable> possibleValues) { + val res = createRelationDefinition => [it.name = name.canonize] + val variableMap = new ArrayList(parameters.size) + var index = 0 + for(parameter : parameters) { + val actualIndex = index + val newVar = createVariable=>[it.name ='''var «actualIndex»'''.canonize it.range = parameter.toTypeReference] + variableMap.add(index,newVar) + res.variables+=newVar + res.parameters+=newVar.range + index+=1 + } + res.value = possibleValues.map[possibleValue |(0.. [it.value = result] + } + def public Assertion(CharSequence name, TermDescription term) { + val result = term.toTerm + result.nameAnonymVariables(Collections.EMPTY_LIST) + createAssertion => [it.value = result it.name=name.canonize] + } + def public add(LogicProblem problem, Assertion assertion) { + if(assertion.name.nullOrEmpty) { + val name = problem.assertions.map[name].generateUniqueName["assertion"+it] + assertion.name=name + } + checkAssertion(assertion) + problem.assertions+=assertion + return assertion + } + + def public add(LogicProblem problem, TermDescription term) { + problem.add(Assertion(term)) + } + + + def checkAssertion(Assertion assertion) { + for(value : assertion.eAllContents.filter(SymbolicValue).toIterable) { + var referred = value.symbolicReference + if(referred instanceof Variable) { + if(!value.hasDeclaredVariable(referred)){ + throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''') + } + } + } + } + + def public checkDefinition(EObject definition) { + /*for(value : definition.eAllContents.filter(SymbolicValue).toIterable) { + var referred = value.symbolicReference + if(referred instanceof Variable) { + if(!value.hasDeclaredVariable(referred)){ + throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''') + } + } + }*/ + } + + // Containment + def public ContainmentHierarchy( + Iterable typesInHierarchy, + Iterable containmentFunctions, + Iterable containmentRelations, + Constant rootConstant + ) { + val result = createContainmentHierarchy => [ + it.typesOrderedInHierarchy += typesInHierarchy + it.containmentFunctions += containmentFunctions + it.containmentRelations += containmentRelations + it.rootConstant = rootConstant + ] + return result + } + def public add(LogicProblem problem, ContainmentHierarchy hierarchy) { + problem.containmentHierarchies+=hierarchy + return hierarchy + } + + // Terms + + private dispatch def boolean hasDeclaredVariable(QuantifiedExpression term, Variable variable) { + return term.quantifiedVariables.contains(variable) || ((term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable)) + } + private dispatch def boolean hasDeclaredVariable(Term term, Variable variable) { + return (term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable) + } + private dispatch def boolean hasDeclaredVariable(RelationDefinition relation, Variable variable) { + relation.variables.contains(variable) + } + private dispatch def boolean hasDeclaredVariable(Void term, Variable variable) { + return false + } + + def protected void nameAnonymVariables(EObject termSegment, List previousNames) { + if(termSegment instanceof QuantifiedExpression) { + val newNames = new LinkedList(previousNames) + for(variable : termSegment.quantifiedVariables) { + var String newName + if(variable.name.nullOrEmpty) { + newName = newNames.generateUniqueName[i | + var x = variable.range.variableAnonymName + x+="var"+i.toString + //println(x) + return x + ] + variable.name = newName + } + else newName = variable.name + newNames+= newName + } + termSegment.expression.nameAnonymVariables(newNames) + } + else { + for(subTerm : termSegment.eContents) { + subTerm.nameAnonymVariables(previousNames) + } + } + } + def protected dispatch String variableAnonymName(BoolTypeReference ref) { "bool" } + def protected dispatch String variableAnonymName(IntTypeReference ref) { "int" } + def protected dispatch String variableAnonymName(RealTypeReference ref) { "real" } + def protected dispatch String variableAnonymName(ComplexTypeReference ref) { ref.referred.name.toLowerCase } + + def protected allSubterms(Term term) { + val content = term.eAllContents + val result = new ArrayList(content.size+1) + result+=term + result+=content.toIterable + return result; + } + + def public Term toTerm(TermDescription term) { + if(term instanceof Term) return term + else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] + else if (term instanceof Constant) return term.call() + else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term] + else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) + } + + def public !(TermDescription term) { Not(term) } + def public Not(TermDescription term) { createNot => [operand = term.toTerm] } + + def public &&(TermDescription a, TermDescription b) { And(a,b) } + def public And(TermDescription... terms) { return And(terms as Iterable) } + def public And(Iterable terms) { createAnd => [operands += terms.map[toTerm]] } + + def public ||(TermDescription a, TermDescription b) { Or(a,b) } + def public Or(TermDescription... terms) { Or(terms as Iterable) } + def public Or(Iterable terms) { createOr => [operands += terms.map[toTerm]] } + + def public =>(TermDescription a, TermDescription b) { Impl(a,b) } + def public Impl(TermDescription a, TermDescription b) { createImpl => [leftOperand = a.toTerm rightOperand = b.toTerm] } + + def public <=>(TermDescription a, TermDescription b) { Iff(a,b)} + def public Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] } + + def public ITE(TermDescription condition, TermDescription ifTrue, TermDescription ifFalse) { + createIfThenElse => [it.condition = condition.toTerm it.ifTrue = ifTrue.toTerm it.ifFalse = ifFalse.toTerm] + } + + def public >(TermDescription left, TermDescription right) { MoreThan(left,right)} + def public MoreThan(TermDescription left, TermDescription right) { createMoreThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public <(TermDescription left, TermDescription right) { LessThan(left,right)} + def public LessThan(TermDescription left, TermDescription right) { createLessThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public <=(TermDescription left, TermDescription right) { LessOrEqual(left,right) } + def public LessOrEqual(TermDescription left, TermDescription right) { createLessOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) } + def public MoreOrEqual(TermDescription left, TermDescription right) { createMoreOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public ==(TermDescription left, TermDescription right) {Equals(left,right)} + def public Equals(TermDescription left, TermDescription right) { createEquals => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public !=(TermDescription left, TermDescription right) { Distinct(left,right) } + def public Distinct(TermDescription... terms) { return Distinct(terms as Iterable) } + def public Distinct(Iterable terms) { createDistinct => [operands += terms.map[toTerm]] } + + def public +(TermDescription left, TermDescription right) { Plus(left,right) } + def public Plus(TermDescription left, TermDescription right) { createPlus => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public -(TermDescription left, TermDescription right) { Minus(left,right) } + def public Minus(TermDescription left, TermDescription right) { createMinus => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public *(TermDescription left, TermDescription right) { Multiply(left,right) } + def public Multiply(TermDescription left, TermDescription right) { createMultiply => [leftOperand=left.toTerm rightOperand=right.toTerm] } + + def public /(TermDescription left, TermDescription right) { Divide(left,right) } + def public Divide(TermDescription left, TermDescription right) { createDivison => [leftOperand = left.toTerm rightOperand = right.toTerm]} + + def public %(TermDescription left, TermDescription right) { Modulo(left,right) } + def public Modulo(TermDescription left, TermDescription right) { createMod => [leftOperand = left.toTerm rightOperand = right.toTerm]} + + def public asTerm(boolean value) { createBoolLiteral => [x|x.value = value] } + def public asTerm(int value) { createIntLiteral => [x|x.value = value] } + def public asTerm(double value) { createRealLiteral => [x|x.value = BigDecimal.valueOf(value)] } + + def public InstanceOf(TermDescription term, TypeDescriptor type) { + createInstanceOf => [ + it.value = term.toTerm + it.range = type.toTypeReference + ] + } + + // QuantifiedExpressions + + def public Forall(Function1 expression) { + val context = new VariableContext(this,logicFactiory) + val term = expression.apply(context) + return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] + } + def public Forall(TermDescription expression, Variable... variables) { + Forall(variables,expression) } + def public Forall(Iterable variables,TermDescription expression) { + val forallExpression = createForall + for(variable : variables) forallExpression.quantifiedVariables += variable + forallExpression.expression = expression.toTerm + return forallExpression + } + + def public Exists(Function1 expression) { + val context = new VariableContext(this,logicFactiory) + val term = expression.apply(context) + return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] + } + def public Exists(TermDescription expression, Variable... variables) { + Exists(variables,expression) } + def public Exists(Iterable variables, TermDescription expression) { + val existsExpression = createExists + for(variable : variables) existsExpression.quantifiedVariables += variable + existsExpression.expression = expression.toTerm + return existsExpression + } + + // Function calls + def public call(Function function, TermDescription... substitutions) { + call(function, substitutions as Iterable) } + def public call(Function function, Iterable substitutions) { + val functionReference = createSymbolicValue + functionReference.symbolicReference=function + val List l= new LinkedList() + l.addAll(substitutions) + for(substitution : l) + functionReference.parameterSubstitutions += substitution.toTerm + functionReference.checkFunctionCall(function) + return functionReference + } + def private checkFunctionCall(SymbolicValue value, Function referredFunction) { + if(value.parameterSubstitutions.size != referredFunction.parameters.size) + throw new LogicProblemBuilderException( + '''The function called has «referredFunction.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''') + } + + // Relation calls + def public call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable)} + def public call(Relation relation, Iterable substitution) { + val relationReference = createSymbolicValue + relationReference.symbolicReference = relation + //println('''«relation.name»(«substitution.size»->«relation.parameters»)''') + for(value : substitution) + relationReference.parameterSubstitutions += value.toTerm + relationReference.checkRelationCall(relation) + return relationReference + } + def private checkRelationCall(SymbolicValue value, Relation referredRelation) { + if(value.parameterSubstitutions.size != referredRelation.parameters.size) { + throw new LogicProblemBuilderException( + '''The relation "«referredRelation.name»" called has «referredRelation.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''') + } + } + + // constant evaluation + def public call(Constant constant) { + val constantReference = createSymbolicValue + constantReference.symbolicReference = constant + return constantReference + } + + +} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend new file mode 100644 index 00000000..2e3d57cf --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend @@ -0,0 +1,47 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace + +abstract class LogicReasoner { + def abstract LogicResult solve( + LogicProblem problem, + LogicSolverConfiguration configuration, + ReasonerWorkspace workspace) throws LogicReasonerException + def abstract LogicModelInterpretation getInterpretation(ModelResult modelResult) +} + +public class LogicReasonerException extends Exception { + new(String message, Exception cause) { super(message,cause) } + new(Exception cause) { super("The reasoner has failed",cause)} + new(String message) { super(message) } +} + +abstract class LogicSolverConfiguration { + public static val Unlimited = -1; + public static val String UndefinedPath = null + + /** The URI string to the independent solver application */ + public String solverPath = UndefinedPath + /** Max runtime limit in seconds. */ + public int runtimeLimit = Unlimited + /** Max runtime limit in seconds. */ + public int memoryLimit = Unlimited + + public var TypeScopes typeScopes = new TypeScopes; + public var SolutionScope solutionScope = new SolutionScope +} + +public class TypeScopes{ + public static val Unlimited = -1; + public var maxIntScope = Unlimited + public var minNewElements = 0 + public var maxNewElements = Unlimited +} + +public class SolutionScope{ + public static val Unlimited = -1; + public var numberOfRequiredSolution = 1 +} \ No newline at end of file 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 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import java.math.BigDecimal +import java.util.ArrayList +import java.util.Collection +import java.util.Collections +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import org.eclipse.xtend.lib.annotations.Data + +@Data class InterpretationValidationResult { + val List problems; + val List invalidAssertions; + def isValid() { return problems.empty && invalidAssertions.empty} +} + +class LogicStructureBuilder{ + val protected extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE + + def public dispatch Collection getElements(LogicModelInterpretation interpretation, TypeDeclaration type) { + return interpretation.getElements(type) + } + def public dispatch Collection getElements(LogicModelInterpretation interpretation, TypeDefinition type) { + return type.elements + } + + def public Term evalAsTerm(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap).toTerm } + def public boolean evalAsBool(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Boolean} + def public int evalAsInt(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Integer } + def public BigDecimal evalAsReal(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as BigDecimal } + /** + * Evaluate the expression on a solution to an logic element. + * @param interpretation The interpretation which the expression is evaluated on. + * @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} + /** + * Checks if the interpretation is a valid solution of the problem by checking the satisfactions of each assertion. + * Returns the collection of failed assertions. + * @param interpretation The checked interpretation. + * @param problem The interpretation is checked on this problem. + * @return The collection of failed assertions. + */ + def public validateInterpretationOnProblem(LogicModelInterpretation interpretation, LogicProblem problem) { + val List problems = new LinkedList + + // Checking types + val type2ElementsMap = problem.types.toInvertedMap[interpretation.getElements(it)] + + // Checking definition does not changed + for(type : problem.types.filter(TypeDefinition)) { + val elements = type2ElementsMap.get(type) + if(!type.elements.containsAll(elements)) + problems+='''The interpretation of «type.name» does not contains each elements of the problem''' + if(!elements.containsAll(type.elements)) + problems+='''The interpretation of «type.name» does not contains additional elements not specified in the problem''' + } + // Checking the type table + val allElements = type2ElementsMap.values.flatten.toSet + for (element : allElements) { + if(! checkElement(problem, type2ElementsMap, element)) { + problems += '''«element.name» does not follows the type hierarchy''' + } + } + + // Checking assertions + val List invalidAssertions = new LinkedList + for(assertion : problem.assertions) { + if(! interpretation.evalAsBool(assertion.value)) { + invalidAssertions+= assertion + problems += '''«assertion.name» is violated!''' + } + } + return new InterpretationValidationResult(problems,invalidAssertions) + //problem.assertions.filter[x | ! interpretation.evalAsBool(x.value)] + } + + private def checkElement(LogicProblem problem, Map> type2ElementsMap, DefinedElement element) { + val compatibleDynamicTypes = new LinkedList + for(possibleDynamicType: problem.types.filter[!it.isIsAbstract]) { + //println(possibleDynamicType.name) + val compatibleTypes = possibleDynamicType.transitiveClosureStar[it.supertypes] + //compatibleTypes.forEach[print(''' + «it.name»''')] + val incompatibleTypes = problem.types.filter[!compatibleTypes.contains(it)] + //incompatibleTypes.forEach[print(''' - «it.name»''')] + if(compatibleTypes.forall[ type2ElementsMap.get(it).contains(element)] && incompatibleTypes.forall[!type2ElementsMap.get(it).contains(element)]) { + //println("Ok") + compatibleDynamicTypes += possibleDynamicType + } + } + return compatibleDynamicTypes.size == 1 + } + + def protected dispatch Term toTerm(Integer o) { createIntLiteral=>[value = o] } + def protected dispatch Term toTerm(BigDecimal o) { createRealLiteral=>[value = o]} + def protected dispatch Term toTerm(Boolean o) { createBoolLiteral=>[value = o]} + def protected dispatch Term toTerm(SymbolicDeclaration o) { createSymbolicValue=>[symbolicReference = o]} + def public Term termDescriptiontoTerm(TermDescription term) { + if(term instanceof Term) return term + else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] + else if (term instanceof Constant) return createSymbolicValue=>[symbolicReference = term] + else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term] + else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) + } + /** + * Returns if the operation with the numbers in the parameter requires the use of BigDecimal. + */ + def private isBigDecimalRequired(Object... numbers) { return numbers.exists[it instanceof BigDecimal || it instanceof RealLiteral] } + def private dispatch BigDecimal asBigDecimal(IntLiteral i) { i.value.asBigDecimal } + def private dispatch BigDecimal asBigDecimal(RealLiteral i) { i.value.asBigDecimal } + def private dispatch BigDecimal asBigDecimal(Integer i) { BigDecimal.valueOf(i) } + def private dispatch BigDecimal asBigDecimal(BigDecimal i) { i } + def private dispatch Integer asInteger(Integer i) { i } + def private dispatch Integer asInteger(BigDecimal i) { i.intValue } + def private dispatch Integer asInteger(IntLiteral i) { i.value.asInteger } + + // Atomic resoulutions + def protected dispatch Object resolve(IntLiteral literal, LogicModelInterpretation interpretation, Map variableBinding) { return literal.value as Integer } + def protected dispatch Object resolve(BoolLiteral literal, LogicModelInterpretation interpretation, Map variableBinding) { return literal.value } + def protected dispatch Object resolve(RealLiteral literal, LogicModelInterpretation interpretation, Map variableBinding) { return literal.value as BigDecimal } + + def protected dispatch Object resolve(Not not, LogicModelInterpretation interpretation, Map variableBinding) { + return ! (not.operand.resolve(interpretation,variableBinding) as Boolean) } + def protected dispatch Object resolve(And and, LogicModelInterpretation interpretation, Map variableBinding) { + //for(operand : and.operands) { + //val r = operand.resolve(interpretation,variableBinding) as Boolean + //println(r) + //} + return and.operands.forall[resolve(interpretation,variableBinding) as Boolean] as Boolean } + def protected dispatch Object resolve(Or or, LogicModelInterpretation interpretation, Map variableBinding) { + //val resolved = or.operands.map[resolve(interpretation,variableBinding) as Boolean] + //println(resolved) + return or.operands.exists[resolve(interpretation,variableBinding) as Boolean] } + def protected dispatch Object resolve(Impl impl, LogicModelInterpretation interpretation, Map variableBinding) { + val left = impl.leftOperand. resolve(interpretation,variableBinding) as Boolean + val right = impl.rightOperand.resolve(interpretation,variableBinding) as Boolean + return (! left) || (right) } + def protected dispatch Object resolve(Iff iff, LogicModelInterpretation interpretation, Map variableBinding) { + return (iff.leftOperand.resolve(interpretation,variableBinding) as Boolean) == + (iff.rightOperand.resolve(interpretation,variableBinding) as Boolean) } + def protected dispatch Object resolve(IfThenElse ite, LogicModelInterpretation interpretation, Map variableBinding) { + val condition = ite.condition.resolve(interpretation,variableBinding) as Boolean + if(condition) return ite.ifTrue.resolve(interpretation,variableBinding) + else return ite.ifFalse.resolve(interpretation,variableBinding) + } + def protected dispatch Object resolve(MoreThan moreThan, LogicModelInterpretation interpretation, Map variableBinding) { + val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number + val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) { + return left.asBigDecimal.compareTo(right.asBigDecimal) > 0 } + else { return left.asInteger > right.asInteger } } + def protected dispatch Object resolve(LessThan lessThan, LogicModelInterpretation interpretation, Map variableBinding) { + val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number + val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) { + return left.asBigDecimal.compareTo(right.asBigDecimal) < 0 } + else { return left.asInteger < right.asInteger } } + def protected dispatch Object resolve(MoreOrEqualThan moreThan, LogicModelInterpretation interpretation, Map variableBinding) { + val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number + val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) { + return left.asBigDecimal.compareTo(right.asBigDecimal) >= 0 } + else { return left.asInteger >= right.asInteger } } + def protected dispatch Object resolve(LessOrEqualThan lessThan, LogicModelInterpretation interpretation, Map variableBinding) { + val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number + val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) return left.asBigDecimal.compareTo(right.asBigDecimal) <= 0 + else { return left.asInteger <= right.asInteger } } + + + def protected dispatch Object resolve(Equals equals, LogicModelInterpretation interpretation, Map variableBinding) { + val left = equals.leftOperand.resolve(interpretation,variableBinding) + val right = equals.rightOperand.resolve(interpretation,variableBinding) + return compare(left,right) + } + def protected dispatch Object resolve(Distinct distinct, LogicModelInterpretation interpretation, Map variableBinding) { + val elements = distinct.operands.map[it.resolve(interpretation,variableBinding)] + if(elements.size== 0) return true + else { + val res = (0.. variableBinding) { + val left = plus.leftOperand.resolve(interpretation,variableBinding) as Number + val right = plus.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) return left.asBigDecimal.add(right.asBigDecimal) + else return left.asInteger + right.asInteger + } + def protected dispatch Object resolve(Minus minus, LogicModelInterpretation interpretation, Map variableBinding) { + val left = minus.leftOperand.resolve(interpretation,variableBinding) as Number + val right = minus.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) return left.asBigDecimal.subtract(right.asBigDecimal) + else return left.asInteger - right.asInteger + } + def protected dispatch Object resolve(Multiply multiply, LogicModelInterpretation interpretation, Map variableBinding) { + val left = multiply.leftOperand.resolve(interpretation,variableBinding) + val right = multiply.rightOperand.resolve(interpretation,variableBinding) + if(isBigDecimalRequired(left,right)) return left.asBigDecimal.multiply(right.asBigDecimal) + else return left.asInteger * right.asInteger + } + def protected dispatch Object resolve(Divison divide, LogicModelInterpretation interpretation, Map variableBinding) { + val left = divide.leftOperand.resolve(interpretation,variableBinding) as Number + val right = divide.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) return left.asBigDecimal.divide(right.asBigDecimal) + return left.asInteger / right.asInteger + } + def protected dispatch Object resolve(Mod modulo, LogicModelInterpretation interpretation, Map variableBinding) { + val left = modulo.leftOperand.resolve(interpretation,variableBinding) as Number + val right = modulo.rightOperand.resolve(interpretation,variableBinding) as Number + if(isBigDecimalRequired(left,right)) return left.asBigDecimal.remainder(right.asBigDecimal) + else return left.asInteger % right.asInteger + } + + 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) { + executeForall(forall.expression,interpretation,variableBinding,forall.quantifiedVariables) } + + 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.. + if(! symbolicValue.parameterSubstitutions.empty) { + for(place : 0..symbolicValue.parameterSubstitutions.size-1) { + val variable = symbolicValue.parameterSubstitutions.get(place) + parameterSubstitunion += variable.resolve(interpretation,variableBinding) + } + } + return (interpretation.getInterpretation(referenced,parameterSubstitunion) as Boolean) + } else if(referenced instanceof RelationDefinition) { + val parameterSubstitution = new HashMap() + for(place: 0.. variableBinding) { + return variableBinding.get(variable) + } + + def protected dispatch resolve(DefinedElement definedElement, LogicModelInterpretation interpretation, Map variableBinding) { + return definedElement + } + + def private compare(Object left, Object right) { + if(left instanceof Number && right instanceof Number) { + if(isBigDecimalRequired(left as Number,right as Number)) { + return (left as Number).asBigDecimal.compareTo((right as Number).asBigDecimal) == 0 + } else { + return (left as Number).asInteger == (right as Number).asInteger + } + } else return left.equals(right) + } + + def allIntegers(LogicModelInterpretation interpretation) { + if(interpretation.minimalInteger <= interpretation.maximalInteger) { + (interpretation.minimalInteger .. interpretation.maximalInteger).map[asInteger] + } else return emptySet + } + + def private boolean executeExists( + Term expression, + LogicModelInterpretation interpretation, + Map variableBinding, + List variablesToBind) + { + if(variablesToBind.empty) { + val res = expression.resolve(interpretation,variableBinding) as Boolean + return res + } + else { + val unfoldedVariable = variablesToBind.head + val possibleValuesType = unfoldedVariable.range + if(possibleValuesType instanceof ComplexTypeReference) { + return this.getElements(interpretation,possibleValuesType.referred).exists[newBinding | + executeExists( + expression, + interpretation, + new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], + variablesToBind.subList(1,variablesToBind.size))] + } else if(possibleValuesType instanceof IntTypeReference) { + return interpretation.allIntegers.exists[newBinding | + executeExists( + expression, + interpretation, + new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], + variablesToBind.subList(1,variablesToBind.size))] + } + else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''') + } + } + + def private boolean executeForall( + Term expression, + LogicModelInterpretation interpretation, + Map variableBinding, + List variablesToBind) + { + if(variablesToBind.empty) { + return expression.resolve(interpretation,variableBinding) as Boolean + } + else { + val unfoldedVariable = variablesToBind.head + val possibleValuesType = unfoldedVariable.range + if(possibleValuesType instanceof ComplexTypeReference) { + return this.getElements(interpretation,possibleValuesType.referred).forall[newBinding | + executeForall( + expression, + interpretation, + new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], + variablesToBind.subList(1,variablesToBind.size))] + } else if(possibleValuesType instanceof IntTypeReference) { + return interpretation.allIntegers.forall[newBinding | + executeForall( + expression, + interpretation, + new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], + variablesToBind.subList(1,variablesToBind.size))] + } else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''') + } + } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedLogicProblem.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedLogicProblem.xtend new file mode 100644 index 00000000..9862a6c1 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedLogicProblem.xtend @@ -0,0 +1,26 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem + +class TracedLogicProblem { + val LogicProblemBuilder builder = new LogicProblemBuilder + val LogicProblem problem = builder.createProblem + + def public getProblem() { return problem } + + def public add(TypeDeclaration type) { builder.add(problem,type) } + def public add(TypeDefinition type) { builder.add(problem,type) } + def public add(Function function) { builder.add(problem,function) } + def public add(FunctionDescription functionDescription) { builder.add(problem,functionDescription) } + def public add(Relation relation) { builder.add(problem, relation) } + def public add(Constant constant) { builder.add(problem, constant) } + def public add(Assertion assertion) { builder.add(problem,assertion) } + def public add(TermDescription termDescription) { builder.add(problem,termDescription) } +} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedOutput.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedOutput.xtend new file mode 100644 index 00000000..6ffc3524 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/TracedOutput.xtend @@ -0,0 +1,6 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder + +@Data class TracedOutput { + OUTPUT output + TRACE trace +} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/VariableContext.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/VariableContext.xtend new file mode 100644 index 00000000..3073d88f --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/VariableContext.xtend @@ -0,0 +1,33 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import java.util.List +import java.util.LinkedList +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor + +class VariableContext { + val extension LogiclanguageFactory language; + val extension LogicProblemBuilder logicProblemBuilder; + + new(LogicProblemBuilder logicProblemBuilder, LogiclanguageFactory language) { + this.logicProblemBuilder = logicProblemBuilder + this.language = language + } + + private List variables = new LinkedList; + def public getVariables(){variables} + + + //def public -(TypeDescriptor type) { Variable(type) } + def public Variable addVar(TypeDescriptor type) { + return addVar(null, type); + } + + def public Variable addVar(CharSequence variableName, TypeDescriptor type) { + if(variables.exists[name.equals(variableName)]) throw new IllegalArgumentException("Variable with name " + variableName +" is already defined.") + val variable = createVariable => [name = variableName.canonize range = type.toTypeReference] + variables += variable + return variable + } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/consistencychecker/TypeConsistencyChecker.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/consistencychecker/TypeConsistencyChecker.xtend new file mode 100644 index 00000000..abb05e83 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/consistencychecker/TypeConsistencyChecker.xtend @@ -0,0 +1,75 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.builder.consistencychecker + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeSystemIsInconsistentMatcher +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementNotDefinedInSupertypeMatcher +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementWithNoPossibleDynamicTypeMatcher +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher + +class TypeConsistencyChecker extends LogicReasoner{ + val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE + + new() { + LogicproblemPackage.eINSTANCE.class + } + + override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { + val statistics = createStatistics => [ + it.transformationTime = 0 + it.solverMemory = -1 + ] + + val start = System.currentTimeMillis + + val queryEngine = ViatraQueryEngine.on(new EMFScope(problem)) + + val typeSystemInconsistencyMatcher = TypeSystemIsInconsistentMatcher.on(queryEngine) + val elementNotDefinedInSupertype = ElementNotDefinedInSupertypeMatcher.on(queryEngine) + val elementWithNoPossibleDynamicType = ElementWithNoPossibleDynamicTypeMatcher.on(queryEngine) + val possibleDynamicType = PossibleDynamicTypeMatcher.on(queryEngine) + + val hasErrorPatternMatch = typeSystemInconsistencyMatcher.hasMatch(problem) + + statistics.solverTime = (System.currentTimeMillis - start) as int + + val possibleDynamicTypeStatisticEntry = problem.elements.map[e| + '''«e.name»: [«possibleDynamicType.getAllValuesOfdynamic(problem,e).map[it.name].join(", ")»]''' + ].join("\n") + + if(hasErrorPatternMatch) { + return createInconsistencyResult =>[ + it.problem = problem + it.statistics = statistics + it.statistics.entries += createStringStatisticEntry => [ + it.name = "possibleDynamicType" + it.value = possibleDynamicTypeStatisticEntry + ] + it.statistics.entries += createStringStatisticEntry => [ + it.name = "elementNotDefinedInSupertype" + it.value=elementNotDefinedInSupertype.allValuesOfelement.map[it.name].join(", ") + ] + + it.statistics.entries += createStringStatisticEntry => [ + it.name = "elementWithNoPossibleDynamicType" + it.value=elementWithNoPossibleDynamicType.allValuesOfelement.map[it.name].join(", ") + ] + ] + } else { + return createUndecidableResult => + [it.problem = problem it.statistics = statistics] + } + } + + override getInterpretation(ModelResult modelResult) { + throw new UnsupportedOperationException('''This solver is unable to create interpretations!''') + } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend new file mode 100644 index 00000000..442de6d9 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2CSV.xtend @@ -0,0 +1,89 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.statistics + +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics +import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map + +class StatisticsData { + public var List> inputConfiguration + public var List> outputMetrics + public var Statistics solverStatistics +} + +class StatisticSections2CSV { + static val separator = ';' + static val empty = "" + + private def getValue(Map map,String key) { + if(map.containsKey(key)) return map.get(key) + else return empty + } + private def addKey(List list, String newValue) { + if(! list.contains(newValue)) list+=newValue + } + + public def CharSequence transformStatisticDatas2CSV( + List statistics) + { + val inputConfigurationColumns = new LinkedList + val inputConfigurationValues = new ArrayList(statistics.length) + val solverStatisticColumns = new LinkedList + val solverStatisticValues = new ArrayList(statistics.length) + val outputMetricColumns = new LinkedList + val outputMetricValues = new ArrayList(statistics.length) + + statistics.map[inputConfiguration].indexColumnsForPairs(inputConfigurationColumns, inputConfigurationValues) + statistics.map[it.solverStatistics].indexColumnsForEntries(solverStatisticColumns, solverStatisticValues) + statistics.map[outputMetrics].indexColumnsForPairs(outputMetricColumns,outputMetricValues) + + return ''' + ID« // Header + IF inputConfigurationColumns.length>0»«separator»«FOR name : inputConfigurationColumns SEPARATOR separator»«name»«ENDFOR»«ENDIF»« + separator»Transformation_Time«separator»Solver_Time«separator»Solver_Memory« + IF solverStatisticColumns.length>0»«separator»«ENDIF»« + FOR name:solverStatisticColumns SEPARATOR separator»«name»«ENDFOR»« + IF outputMetricColumns.length>0»«separator»«ENDIF»« + FOR name:outputMetricColumns SEPARATOR separator»«name»«ENDFOR» + « // Table + FOR index : 0..0»«separator»«ENDIF»« + FOR name : inputConfigurationColumns SEPARATOR separator»«inputConfigurationValues.get(index).getValue(name)»«ENDFOR»« + separator»«statistics.get(index).solverStatistics.transformationTime»« + separator»«statistics.get(index).solverStatistics.solverTime»« + separator»«statistics.get(index).solverStatistics.solverMemory»« + IF solverStatisticColumns.size>0»«separator»«ENDIF»« + FOR name:solverStatisticColumns SEPARATOR separator»«solverStatisticValues.get(index).getValue(name)»«ENDFOR»« + IF outputMetricColumns.size>0»«separator»«ENDIF»« + FOR name:outputMetricColumns SEPARATOR separator»«outputMetricValues.get(index).getValue(name)»«ENDFOR» + «ENDFOR»''' + } + + def private indexColumnsForPairs(List>> datas, List columns, List> values) { + for(inputConfiguration : datas) { + val map = new HashMap + for(entry : inputConfiguration) { + columns.addKey(entry.key) + map.put(entry.key,entry.value) + } + values+=map + } + } + def private indexColumnsForEntries(List datas, List columns, List> values) { + for(inputConfiguration : datas) { + val map = new HashMap + for(entry : inputConfiguration.entries) { + columns.addKey(entry.name) + map.put(entry.name,entry.readValue) + } + values+=map + } + } + private def dispatch String readValue(IntStatisticEntry e) { return e.value.toString } + private def dispatch String readValue(RealStatisticEntry e){ return e.value.toString } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend new file mode 100644 index 00000000..08efa811 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/statistics/StatisticSections2Print.xtend @@ -0,0 +1,23 @@ +package hu.bme.mit.inf.dslreasoner.logic.model.statistics + +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry +import java.util.List + +class StatisticSections2Print { + public def CharSequence transformStatisticDatas2CSV( + List statistics) + { + var result = ""; + for(statistic : statistics) { + result+= '''«statistic.readValue»;''' + } + return result + } + + private def dispatch String readValue(IntStatisticEntry e) { return e.value.toString } + private def dispatch String readValue(RealStatisticEntry e){ return e.value.toString } + private def dispatch String readValue(StringStatisticEntry e) { return "\n" + e.value } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/CollectionsUtil.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/CollectionsUtil.xtend new file mode 100644 index 00000000..25cddc05 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/CollectionsUtil.xtend @@ -0,0 +1,82 @@ +package hu.bme.mit.inf.dslreasoner.util + +import java.util.HashSet +import java.util.LinkedList +import java.util.List +import java.util.Map +import java.util.Set +import org.eclipse.xtext.xbase.lib.Functions.Function1 +import java.util.HashMap +import java.util.LinkedHashMap + +class CollectionsUtil { + public def static TO lookup(FROM from, Map map) { + if(map.containsKey(from)) { + return map.get(from) + } else throw new IllegalArgumentException(''' + The map does not contains the key "«from.toString»"! + --- Elements: --- + «FOR entry : map.entrySet SEPARATOR '\n'»«entry.key» -> «entry.value»«ENDFOR» + -----------------'''); + } + public def TO ifThenElse(FROM source, Function1 condition, Function1 ifTrue, Function1 ifFalse) { + if(condition.apply(source)) { + return ifTrue.apply(source) + } + else { + return ifFalse.apply(source) + } + } + public def static Union(Map a, Map b) { + (a.keySet + b.keySet).toInvertedMap[key | + if(a.containsKey(key)) a.get(key) + else b.get(key) + ] + } + public def static putOrAddToSet(Map> map, Key key, Value value) { + if(map.containsKey(key)) { + map.get(key).add(value) + }else{ + val set = new HashSet() => [it.add(value)] + map.put(key, set) + } + } + public def static putOrAddToList(Map> map, Key key, Value value) { + if(map.containsKey(key)) { + map.get(key).add(value) + }else{ + val set = new LinkedList() => [it.add(value)] + map.put(key, set) + } + } + def public static Map copyMap(Map oldMap, Iterable newValues, Function1 indexExtractor) { + val Map valueIndexes = oldMap.values.toMap[to|indexExtractor.apply(to)]; + val res = oldMap.mapValues[value | indexExtractor.apply(value).lookup(valueIndexes)] + return res + } + def public static Map bijectiveInverse(Map m) { m.keySet.toMap[x|x.lookup(m)] } + def public static Map> inverse(Map m) { + val res = new LinkedHashMap> + m.entrySet.forEach[res.putOrAddToList(it.value,it.key)] + return res + } + + def public static List transitiveClosurePlus(Type source, Function1> next) { + val res = new LinkedList() + transitiveClosureHelper(res,source,next) + return res + } + def public static List transitiveClosureStar(Type source, Function1> next) { + val res = new LinkedList() + res += source + transitiveClosureHelper(res,source,next) + return res + } + def private static void transitiveClosureHelper(List result, Type actual, Function1> next) { + val front = next.apply(actual) + for(elementInFront : front) { + result += elementInFront + transitiveClosureHelper(result,elementInFront,next) + } + } +} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/LogicProblemBuilder_AdvancedConstructs.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/LogicProblemBuilder_AdvancedConstructs.xtend new file mode 100644 index 00000000..3db0e2a6 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/LogicProblemBuilder_AdvancedConstructs.xtend @@ -0,0 +1,71 @@ +package hu.bme.mit.inf.dslreasoner.util + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import java.util.ArrayList +import java.util.Collection +import java.util.List +import java.util.Map + +class LogicProblemBuilder_AdvancedConstructs { + val extension LogicProblemBuilder builder; + public new(LogicProblemBuilder builder) { + this.builder = builder + } + + def public FunctionDefinitionBody(Iterable variables, Map,Term> parametersToValue, Term other) { + val variableList = variables.toList + val entryList = parametersToValue.entrySet.toList + + // Size = 0 + if(entryList.empty && other === null) { + throw new IllegalArgumentException('''No possible value is specified!''') + // Size = 1 + } else if(entryList.size == 1 && other === null) { + return entryList.head.value + // Size = 1 + } else if(entryList.empty && !(other === null)) { + return other + // Size > 1 + }else { + // Transforming values to IF-Then-Else structures + /**The number of IF-THEN-ELSE structures needed*/ + var int iteNumber + if(other === null) iteNumber = entryList.size-1 + else iteNumber = entryList.size + + val ites = new ArrayList(iteNumber) + for (element : 0 ..< iteNumber) { + ites += ITE( + entryList.get(element).key.substitutionIsEqual(variableList), + entryList.get(element).value, + null) + } + + // Linking the IF-Then-Else structures to a chain + for (optionIndex : 1 ..< ites.size) { + val prev = ites.get(optionIndex - 1) + val next = ites.get(optionIndex) + prev.ifFalse = next + } + + if(other === null) ites.last.ifFalse = entryList.last.value + else ites.last.ifFalse = other + + // return the head of the chain + return ites.head + } + } + + def public RelationDefinitionBody(Iterable variables, Collection> elements) { + val variableList = variables.toList + return elements.map[row | row.substitutionIsEqual(variableList)].Or + } + + def private substitutionIsEqual(List substitution, List variables) { + val parameterIndexes = 0.. implements Set{ + val Function1 representer; + val HashMap map + + public new(Function1 representer) { + this.representer = representer + this.map = new HashMap + } + public new(Function1 representer, Collection initialElements) { + this.representer = representer + this.map = new HashMap + initialElements.forEach[add] + } + + override add(Type arg0) { + val representation = representer.apply(arg0) + if(!map.containsKey(representation)) { + map.put(representation,arg0); + return true + } else return false + } + + override addAll(Collection arg0) { + val originalSize = this.size + arg0.forEach[add(it)] + return (this.size != originalSize) + } + + override clear() { + map.clear + } + + override contains(Object arg0) { + try { + val rep = this.representer.apply(arg0 as Type) + return map.containsKey(rep) + } catch (ClassCastException e) { + return false + } + } + + override containsAll(Collection arg0) { + arg0.forall[it.contains] + } + + override isEmpty() { + return map.isEmpty + } + + override iterator() { + return map.values.iterator + } + + override remove(Object arg0) { + try { + val rep = this.representer.apply(arg0 as Type) + return map.remove(rep) != null + } catch (ClassCastException e) { + return false + } + } + + override removeAll(Collection arg0) { + val originalSize = this.size + arg0.forEach[remove(it)] + return (this.size != originalSize) + } + + override retainAll(Collection arg0) { + val Set representationsOfArg0 = new HashSet + for(element: arg0) { + try { + representationsOfArg0 += this.representer.apply(element as Type) + } catch(ClassCastException e) {} + } + val originalSize = this.size + for(r:this.map.keySet) { + if(!representationsOfArg0.contains(r)) + this.map.remove(r) + } + return (this.size != originalSize) + } + + override size() { + return this.map.size + } + + override toArray() { + map.values.toArray + } + + override toArray(T[] arg0) { + map.values.toArray(arg0) + } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/visualisation/Interpretation2Gml.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/visualisation/Interpretation2Gml.xtend new file mode 100644 index 00000000..472799f9 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/visualisation/Interpretation2Gml.xtend @@ -0,0 +1,5 @@ +package hu.bme.mit.inf.dslreasoner.util.visualisation + +class Interpretation2Gml { + +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/FileSystemWorkspace.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/FileSystemWorkspace.xtend new file mode 100644 index 00000000..6041fdbf --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/FileSystemWorkspace.xtend @@ -0,0 +1,74 @@ +package hu.bme.mit.inf.dslreasoner.workspace + +import java.io.BufferedReader +import java.io.FileReader +import java.io.PrintWriter +import org.eclipse.emf.common.util.URI +import java.io.File + +class FileSystemWorkspace extends ReasonerWorkspace{ + + new(String targetFolder, String prefix) { + super(targetFolder/*.replaceAll("\\\\","/").replaceAll("/\\.","")*/, prefix) + } + + override protected getURI(String name) { + URI.createFileURI(targetFolder + "/" + prefix + name) + } + + def protected getFolderURI() { + URI.createFileURI(targetFolder) + } + + override getWorkspaceURI() { + getFolderURI + } + + override initAndClear() { + val folder = new File(folderURI.toFileString) + folder.mkdirs + for(file : folder.listFiles) { + file.deleteFile + } + } + + def void deleteFile(File file) { + if (file.isDirectory()) { + file.listFiles().forEach[deleteFile] + file.delete + } else { + file.delete; + } + } + + override writeText(String name, CharSequence content) { + val uri = getURI(name) + val writer = new PrintWriter(uri.toFileString, "UTF-8"); + writer.println(content); + writer.close(); + return uri + } + + override readText(String name) { + var String line; + var String result = ""; + val in = new BufferedReader(new FileReader(getURI(name).toFileString)) + while ((line = in.readLine()) != null) { + result = result.concat(line) + } + in.close + return result + } + + override protected renameFile(String name) { + val uri = getURI(name) + val uri2 = getURI(name+deactivationPostfix) + val file = new File(uri. toFileString) + val file2 = new File(uri2.toFileString) + file.renameTo(file2) + } + + override subWorkspace(String targetFolder, String prefix) { + return new FileSystemWorkspace(this.targetFolder + "/" + targetFolder, this.prefix + prefix) + } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ProjectWorkspace.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ProjectWorkspace.xtend new file mode 100644 index 00000000..5703bd5a --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ProjectWorkspace.xtend @@ -0,0 +1,105 @@ +package hu.bme.mit.inf.dslreasoner.workspace + +import java.io.BufferedReader +import java.io.ByteArrayInputStream +import java.io.IOException +import java.io.InputStreamReader +import org.eclipse.core.resources.IContainer +import org.eclipse.core.resources.IFolder +import org.eclipse.core.resources.IProject +import org.eclipse.core.resources.IWorkspaceRoot +import org.eclipse.core.resources.ResourcesPlugin +import org.eclipse.core.runtime.NullProgressMonitor +import org.eclipse.emf.common.util.URI + +class ProjectWorkspace extends ReasonerWorkspace{ + + val monitor = new NullProgressMonitor + var IContainer target; + + new(String targetFolder, String prefix) { + super(targetFolder, prefix) + } + + override protected getURI(String name) { + URI.createPlatformResourceURI(targetFolder + "/" + prefix + name,true); + } + + def protected getDirUri() { + URI.createPlatformResourceURI(targetFolder,true) + } + + override getWorkspaceURI() { + getDirUri + } + + override initAndClear() { + target = ResourcesPlugin.workspace.root + for(nameSegment : dirUri.segments) { + target = createContainer(target,nameSegment) + } + target.members.forEach[delete(false,monitor)] + } + + def protected dispatch createContainer(IWorkspaceRoot root, String name) { + val project = root.getProject(name) + if(project.exists) { + if(!project.open) { + project.open(monitor) + } + } else { + project.create(monitor) + } + return project + } + + def protected dispatch createContainer(IProject root, String name) { + val folder = root.getFolder(name); + if(folder.exists) { + folder.create(false,true,monitor) + } + return folder + } + + def protected dispatch createContainer(IFolder root, String name) { + val folder = root.getFolder(name); + if(folder.exists) { + folder.create(false,true,monitor) + } + return folder + } + + def dispatch getTargetFile(IFolder targetFolder, String name) { targetFolder.getFile(name) } + def dispatch getTargetFile(IProject targetProject, String name) { targetProject.getFile(name) } + + override writeText(String name, CharSequence content) { + val file = target.getTargetFile(name); + if(!file.exists()) { + file.create(new ByteArrayInputStream(content.toString().getBytes()),true, new NullProgressMonitor()); + return URI.createPlatformResourceURI(file.projectRelativePath.toString,true) + } + else throw new IOException("The file is already existing.") + } + + override readText(String name) { + val file = target.getTargetFile(name) + val in = new BufferedReader(new InputStreamReader(file.contents)) + + var result = "" + var String line; + + while ((line = in.readLine()) != null) { + result = result.concat(line) + } + + return result + } + + override protected renameFile(String name) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override subWorkspace(String targetFolder, String prefix) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } +} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ReasonerWorkspace.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ReasonerWorkspace.xtend new file mode 100644 index 00000000..a7e3a48b --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/workspace/ReasonerWorkspace.xtend @@ -0,0 +1,100 @@ +package hu.bme.mit.inf.dslreasoner.workspace + +import java.io.FileNotFoundException +import java.util.Collections +import org.eclipse.emf.common.util.URI +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl +import org.eclipse.emf.ecore.resource.Resource +import java.io.ByteArrayOutputStream +import java.io.IOException + +abstract class ReasonerWorkspace{ + + protected val String targetFolder; + protected val String prefix; + val ResourceSet resSet = new ResourceSetImpl(); + + public new(String targetFolder, String prefix) { + this.targetFolder = targetFolder + this.prefix = prefix + } + + public def ReasonerWorkspace subWorkspace(String targetFolder, String prefix); + + def URI getWorkspaceURI(); + + /** + * Creates the target folder and clears the workspace for the reasoning + */ + def public void initAndClear() + + def protected URI getURI(String name); + protected def Resource getResource(String name) { + val prevoius = resSet.getResource(getURI(name),false); + if(prevoius!= null) prevoius.delete(Collections.EMPTY_MAP) + + val URI resourceURI = getURI(name) + return resSet.createResource(resourceURI); + } + + + /** + * Writes a model + */ + def public URI writeModel(EObject modelRoot, String name) { + val resource = getResource(name); + resource.getContents().add(modelRoot); + resource.save(Collections.EMPTY_MAP); + return resource.URI + } + + + def public String writeModelToString(EObject modelRoot, String name) { + val resource = getResource(name); + resource.getContents().add(modelRoot); + val ByteArrayOutputStream outputStream = new ByteArrayOutputStream(); + resource.save(outputStream, null); + return outputStream.toString(); + } + + def public RootType reloadModel(Class type, String name) { + try { + val resource = resSet.getResource(getURI(name),false); + if(resource.loaded) { + resource.unload + } + resource.load(Collections.EMPTY_MAP) + if(resource == null) throw new FileNotFoundException(getURI(name).toString) + else return resource.contents.get(0) as RootType + } catch(Exception e) { + throw new FileNotFoundException(getURI(name).toString) + } + } + + def public RootType readModel(Class type, String name) { + try { + val resource = resSet.getResource(getURI(name),true); + if(resource == null) throw new FileNotFoundException(getURI(name).toString) + else return resource.contents.get(0) as RootType + } catch(Exception e) { + throw new FileNotFoundException(getURI(name).toString + "reason: " + e.message) + } + } + + def public deactivateModel(String name) { + val resource = resSet.getResource(getURI(name),true); + resource.unload + renameFile(name) + } + val static protected deactivationPostfix = ".deactivated" + def protected void renameFile(String name) + +// def void reactivate() +// def void deactivate() + + def public URI writeText(String name, CharSequence content); + + def public String readText(String name); +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf