diff options
author | 2017-06-10 19:05:05 +0200 | |
---|---|---|
committer | 2017-06-10 19:05:05 +0200 | |
commit | 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch) | |
tree | 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.logic.model/src | |
parent | Initial commit, migrating from SVN (diff) | |
download | VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip |
Migrating Additional projects
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src')
17 files changed, 1911 insertions, 0 deletions
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
10 | import java.util.List | ||
11 | |||
12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
13 | |||
14 | interface LogicModelInterpretation{ | ||
15 | |||
16 | /** | ||
17 | * Returns the elements of a type. | ||
18 | */ | ||
19 | def List<DefinedElement> getElements(Type type) | ||
20 | /** | ||
21 | * Returns the interpretation of a function. The parameters and the return values are encoded to primitive java objects defined by the following table: | ||
22 | * <p><table> | ||
23 | * <tr><th>Term type</th><th>Java object type</th></tr> | ||
24 | * <tr><td>Element of a type </td><td>DefinedElement </td></tr> | ||
25 | * <tr><td>Boolean literal </td><td>Boolean </td></tr> | ||
26 | * <tr><td>Integer literal </td><td>Integer </td></tr> | ||
27 | * <tr><td>Real literal </td><td>BigDecimal </td></tr> | ||
28 | * </table></p> | ||
29 | * @param function The target function to be interpreted. | ||
30 | * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table. | ||
31 | * @return The result of the function call encoded as defined in the table. | ||
32 | */ | ||
33 | def Object getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) | ||
34 | /** | ||
35 | * Returns the interpretation of a relation. The parameters are encoded to primitive java objects defined by the following table: | ||
36 | * <p><table> | ||
37 | * <tr><th>Term type</th><th>Java object type</th></tr> | ||
38 | * <tr><td>Element of a type </td><td>DefinedElement </td></tr> | ||
39 | * <tr><td>Boolean literal </td><td>Boolean </td></tr> | ||
40 | * <tr><td>Integer literal </td><td>Integer </td></tr> | ||
41 | * <tr><td>Real literal </td><td>BigDecimal </td></tr> | ||
42 | * </table></p> | ||
43 | * @param relation The target relation to be interpreted. | ||
44 | * @param parameterSubstitution The array of the substituted parameters encoded as defined in the table. | ||
45 | * @return If the parameter tuple is in the relation. | ||
46 | */ | ||
47 | def boolean getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) | ||
48 | /** | ||
49 | * Returns the interpretation of a constant. The value is encoded to primitive java objects defined by the following table: | ||
50 | * <p><table> | ||
51 | * <tr><th>Term type</th><th>Java object type</th></tr> | ||
52 | * <tr><td>Element of a type </td><td>DefinedElement </td></tr> | ||
53 | * <tr><td>Boolean literal </td><td>Boolean </td></tr> | ||
54 | * <tr><td>Integer literal </td><td>Integer </td></tr> | ||
55 | * <tr><td>Real literal </td><td>BigDecimal </td></tr> | ||
56 | * </table></p> | ||
57 | * @param constant The target constant to be interpreted. | ||
58 | * @return The value of the constant encoded as specified in the table. | ||
59 | */ | ||
60 | def Object getInterpretation(ConstantDeclaration constant) | ||
61 | def int getMinimalInteger() | ||
62 | def int getMaximalInteger() | ||
63 | } | ||
64 | |||
65 | class Uninterpreted implements LogicModelInterpretation { | ||
66 | /*private val static unknownBecauseUninterpreted = LogiclanguageFactory.eINSTANCE.createUnknownBecauseUninterpreted | ||
67 | public def static getUnknownBecauseUninterpreted() {return Uninterpreted.unknownBecauseUninterpreted}*/ | ||
68 | |||
69 | override getElements(Type type) { | ||
70 | throw new UnsupportedOperationException("The interpteration is unknown.") | ||
71 | } | ||
72 | |||
73 | def getKnownElements(Type type) { | ||
74 | val allSubtypes = type.transitiveClosureStar[it.subtypes] | ||
75 | return allSubtypes.filter(TypeDefinition).map[elements].flatten.toList | ||
76 | } | ||
77 | |||
78 | def allElementsAreInterpreted(Type type) { | ||
79 | val allSubtypes = type.transitiveClosureStar[it.subtypes] | ||
80 | return allSubtypes.exists[it instanceof TypeDeclaration] | ||
81 | } | ||
82 | |||
83 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
84 | throw new UnsupportedOperationException("The interpteration is unknown.") | ||
85 | } | ||
86 | |||
87 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
88 | throw new UnsupportedOperationException("The interpteration is unknown.") | ||
89 | } | ||
90 | |||
91 | override getInterpretation(ConstantDeclaration constant) { | ||
92 | throw new UnsupportedOperationException("The interpteration is unknown.") | ||
93 | } | ||
94 | |||
95 | override getMinimalInteger() { | ||
96 | throw new UnsupportedOperationException("The interpteration is unknown.") | ||
97 | } | ||
98 | |||
99 | override getMaximalInteger() { | ||
100 | throw new UnsupportedOperationException("The interpteration is unknown.") | ||
101 | } | ||
102 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemFactory | ||
26 | import hu.bme.mit.inf.dslreasoner.util.LogicProblemBuilder_AdvancedConstructs | ||
27 | import java.math.BigDecimal | ||
28 | import java.util.ArrayList | ||
29 | import java.util.Collections | ||
30 | import java.util.LinkedList | ||
31 | import java.util.List | ||
32 | import java.util.Map | ||
33 | import org.eclipse.emf.ecore.EObject | ||
34 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
35 | import org.eclipse.xtend.lib.annotations.Data | ||
36 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
37 | |||
38 | @Data class FunctionDescription { | ||
39 | Iterable<TypeReference> parameters | ||
40 | TypeReference range | ||
41 | } | ||
42 | |||
43 | class LogicProblemBuilderException extends Exception { | ||
44 | new(String reason) { | ||
45 | super(reason) | ||
46 | } | ||
47 | } | ||
48 | |||
49 | public class LogicProblemBuilder{ | ||
50 | val protected extension LogiclanguageFactory logicFactiory = LogiclanguageFactory.eINSTANCE | ||
51 | val protected extension LogicproblemFactory problemFactory = LogicproblemFactory.eINSTANCE | ||
52 | val protected advancedConstructs = new LogicProblemBuilder_AdvancedConstructs(this) | ||
53 | |||
54 | def public createProblem(){ createLogicProblem } | ||
55 | |||
56 | // Names | ||
57 | def protected String canonize(CharSequence name) { | ||
58 | if(name == null) return "" | ||
59 | val result = name.toString.split("\\s+"); | ||
60 | if(result.size == 1) { | ||
61 | val element = result.get(0); | ||
62 | if(element == "bool" || | ||
63 | element == "int" || | ||
64 | element == "real") throw new LogicProblemBuilderException('''Reserved keyword "«element»"!''') | ||
65 | else return result.join(' ') | ||
66 | } | ||
67 | else return result.join(' ') | ||
68 | } | ||
69 | def protected String generateUniqueName(Iterable<String> previous, Function1<Integer,String> namer) { | ||
70 | var int i = 0 | ||
71 | var generateNew = false; | ||
72 | var String finalName; | ||
73 | do { | ||
74 | i = i+1; | ||
75 | val nameCandidate = namer.apply(i) | ||
76 | finalName = nameCandidate | ||
77 | generateNew = previous.exists[equals(nameCandidate)] | ||
78 | } | ||
79 | while(generateNew) | ||
80 | return finalName | ||
81 | } | ||
82 | |||
83 | // Type builders | ||
84 | def public Element(CharSequence elementName) { return createDefinedElement => [x|x.name = elementName.canonize] } | ||
85 | def public Element() { return createDefinedElement } | ||
86 | def public TypeDeclaration(CharSequence name, boolean isAbstract) { TypeDeclaration => [x | x.name = name.canonize x.isAbstract = isAbstract] } | ||
87 | def public TypeDeclaration() { createTypeDeclaration } | ||
88 | def public TypeDefinition(CharSequence name, boolean isAbstract, DefinedElement... elements) { TypeDefinition(name, isAbstract, elements as Iterable<DefinedElement>) } | ||
89 | def public TypeDefinition(CharSequence name, boolean isAbstract, Iterable<DefinedElement> elements) { createTypeDefinition => [x | x.name = name.canonize x.isAbstract = isAbstract x.elements += elements ] } | ||
90 | |||
91 | def public Supertype(Type subtype, Type supertype) { | ||
92 | subtype.supertypes+=supertype | ||
93 | } | ||
94 | def public SetSupertype(Type subtype, Type supertype, boolean value) { | ||
95 | if(value) subtype.supertypes+=supertype | ||
96 | else subtype.subtypes-=supertype | ||
97 | } | ||
98 | |||
99 | // Type add | ||
100 | def public add(LogicProblem problem, Type type) { | ||
101 | problem.nameIfAnonymType(type) | ||
102 | problem.types+=type | ||
103 | if(type instanceof TypeDefinition) { | ||
104 | problem.elements+=type.elements | ||
105 | } | ||
106 | return type | ||
107 | } | ||
108 | def protected dispatch nameIfAnonymType(LogicProblem problem, Type typeDeclaration) { | ||
109 | if(typeDeclaration.name.nullOrEmpty) | ||
110 | typeDeclaration.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»'''] | ||
111 | } | ||
112 | def protected dispatch nameIfAnonymType(LogicProblem problem, TypeDefinition typeDefinition) { | ||
113 | if(typeDefinition.name.nullOrEmpty) | ||
114 | typeDefinition.name = problem.types.map[it.name].generateUniqueName[i | '''type «i.toString»'''] | ||
115 | for(element : typeDefinition.elements) | ||
116 | if(element.name.nullOrEmpty) | ||
117 | element.name = typeDefinition.elements.map[it.name].generateUniqueName[i | '''type «i.toString»'''] | ||
118 | } | ||
119 | |||
120 | def public LogicBool() { createBoolTypeReference } | ||
121 | def public LogicInt() { createIntTypeReference } | ||
122 | def public LogicReal() { createRealTypeReference } | ||
123 | def toTypeReference(TypeDescriptor descriptor) { | ||
124 | if(descriptor instanceof TypeReference) { return EcoreUtil.copy(descriptor); } | ||
125 | else if(descriptor instanceof Type) { return createComplexTypeReference => [referred = descriptor]} | ||
126 | else throw new UnsupportedOperationException("Unsupported type descriptor: " + descriptor.class) | ||
127 | } | ||
128 | |||
129 | // Variables | ||
130 | def public createVar(CharSequence name, TypeDescriptor range) { | ||
131 | return createVariable => [it.name = name.canonize it.range = range.toTypeReference] | ||
132 | } | ||
133 | |||
134 | // Functions | ||
135 | def public FunctionDescription ->(TypeDescriptor parameter, TypeDescriptor range) { return #[parameter] -> range } | ||
136 | def public FunctionDescription ->(Iterable<? extends TypeDescriptor> parameters, TypeDescriptor range) { return new FunctionDescription(parameters.map[toTypeReference], range.toTypeReference); } | ||
137 | def public FunctionDeclaration(CharSequence name, FunctionDescription functionDescription) { FunctionDeclaration(name,functionDescription.range, functionDescription.parameters) } | ||
138 | def public FunctionDeclaration(FunctionDescription functionDescription) { FunctionDeclaration(functionDescription.range, functionDescription.parameters) } | ||
139 | def public FunctionDeclaration(CharSequence name, TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(name, range, parameters as Iterable<? extends TypeReference>) } | ||
140 | def public FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable<? extends TypeReference>) } | ||
141 | def public FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] } | ||
142 | def public FunctionDeclaration(TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) { | ||
143 | val function = createFunctionDeclaration | ||
144 | for(parameter : parameters) function.parameters+=parameter.toTypeReference | ||
145 | function.range = range.toTypeReference | ||
146 | return function | ||
147 | } | ||
148 | |||
149 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Function1<VariableContext, ? extends TermDescription> expression) { | ||
150 | val context = new VariableContext(this,logicFactiory) | ||
151 | val definition = expression.apply(context) | ||
152 | return FunctionDefinition(name,range,context.variables,definition); | ||
153 | } | ||
154 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<Variable> variables, TermDescription definition) { | ||
155 | return createFunctionDefinition => [ | ||
156 | it.name = name.canonize | ||
157 | it.parameters += variables.map[it.range.toTypeReference] | ||
158 | it.variable += variables | ||
159 | it.range = range.toTypeReference | ||
160 | it.value = definition.toTerm | ||
161 | ] | ||
162 | } | ||
163 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue) { | ||
164 | return FunctionDefinition(name,range,parameters,parametersToValue,null) | ||
165 | } | ||
166 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue, Term defaultValue) { | ||
167 | val parameterList = parameters.toList; | ||
168 | val variableList = (1..parameterList.size).map[index | '''param «index»'''.createVar(parameterList.get(index-1))].toList | ||
169 | return FunctionDefinition(name,range,variableList,advancedConstructs.FunctionDefinitionBody(variableList,parametersToValue,defaultValue)) | ||
170 | } | ||
171 | |||
172 | // Add function to a problem | ||
173 | def public add(LogicProblem input, Function function) { | ||
174 | input.nameIfAnonymFunction(function) | ||
175 | input.checkFunction(function) | ||
176 | input.functions += function | ||
177 | return function | ||
178 | } | ||
179 | def public add(LogicProblem input, FunctionDescription functionDescription) { input.add(FunctionDeclaration(functionDescription)) } | ||
180 | def protected nameIfAnonymFunction(LogicProblem problem, Function functionDeclaration) { | ||
181 | if(functionDeclaration.name.nullOrEmpty) { | ||
182 | functionDeclaration.name = problem.functions.map[it.name].generateUniqueName[i | "function"+i] | ||
183 | } | ||
184 | } | ||
185 | def protected checkFunction(LogicProblem problem, Function function) { | ||
186 | if(problem.functions.exists(x|x.name == function.name)) | ||
187 | throw new LogicProblemBuilderException('''Function with the following name is already defined: "«function.name»"!''') | ||
188 | for(ref : function.parameters.filter(typeof(ComplexTypeReference)).map[referred]) { | ||
189 | if(!problem.types.contains(ref)) | ||
190 | throw new LogicProblemBuilderException('''Type "«ref.name»" is not availabe in the logic problem!''') | ||
191 | } | ||
192 | val range = function.range | ||
193 | if(range instanceof ComplexTypeReference) { | ||
194 | if(!problem.types.contains(range.referred)) | ||
195 | throw new LogicProblemBuilderException('''Type "«range.referred.name»" is not availabe in the logic problem!''') | ||
196 | } | ||
197 | } | ||
198 | |||
199 | // Constants | ||
200 | def public ConstantDeclaration(CharSequence name, TypeDescriptor type) { ConstantDeclaration(type) => [it.name = name.canonize] } | ||
201 | def public ConstantDeclaration(TypeDescriptor type) { createConstantDeclaration => [it.type = type.toTypeReference] } | ||
202 | |||
203 | def public ConstantDefinition(CharSequence name, TypeDescriptor type, TermDescription value) { | ||
204 | createConstantDefinition => [it.name = name.canonize it.type = type.toTypeReference it.value = value.toTerm] | ||
205 | } | ||
206 | |||
207 | // Add constant to a problem | ||
208 | def public add(LogicProblem problem, Constant constant) { | ||
209 | problem.nameIfAnonymConstant(constant); | ||
210 | problem.checkConstant(constant) | ||
211 | problem.constants += constant | ||
212 | return constant | ||
213 | } | ||
214 | def protected nameIfAnonymConstant(LogicProblem problem, Constant constant) { | ||
215 | if(constant.name.nullOrEmpty) { | ||
216 | constant.name = problem.constants.map[it.name].generateUniqueName[i | "constant"+i] | ||
217 | } | ||
218 | } | ||
219 | def protected checkConstant(LogicProblem problem, Constant constant) { | ||
220 | if(problem.constants.exists(x|x.name == constant.name)) | ||
221 | throw new LogicProblemBuilderException('''Constant with the following name is already defined: "«constant.name»"!''') | ||
222 | if((constant.type instanceof ComplexTypeReference) && ! (problem.types.contains((constant.type as ComplexTypeReference).referred))) | ||
223 | throw new LogicProblemBuilderException('''Type "«(constant.type as ComplexTypeReference).referred.name»" is not availabe in the logic problem!''') | ||
224 | } | ||
225 | |||
226 | // Relations | ||
227 | def public RelationDeclaration(CharSequence name, TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable<? extends TypeReference>) } | ||
228 | def public RelationDeclaration(CharSequence name, Iterable<? extends TypeDescriptor> parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] } | ||
229 | def public RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable<? extends TypeReference>) } | ||
230 | def public RelationDeclaration(Iterable<? extends TypeDescriptor> parameters) { | ||
231 | val relation = createRelationDeclaration | ||
232 | for(parameter : parameters) { | ||
233 | relation.parameters+=parameter.toTypeReference | ||
234 | } | ||
235 | return relation | ||
236 | } | ||
237 | |||
238 | def public RelationDefinition(CharSequence name, Function1<VariableContext, ? extends TermDescription> expression) { | ||
239 | val context = new VariableContext(this,logicFactiory); | ||
240 | val definition = expression.apply(context); | ||
241 | return RelationDefinition(name,context.variables,definition) | ||
242 | } | ||
243 | def public RelationDefinition(CharSequence name, Iterable<Variable> variables, TermDescription definition) { | ||
244 | return createRelationDefinition => [ | ||
245 | it.name = name.canonize | ||
246 | it.parameters += variables.map[it.range.toTypeReference] | ||
247 | it.variables += variables | ||
248 | it.value = definition?.toTerm | ||
249 | ] | ||
250 | } | ||
251 | def public RelationDefinition(CharSequence name, Iterable<? extends TypeDescriptor> parameters, Iterable<? extends List<? extends TermDescription>> possibleValues) { | ||
252 | val res = createRelationDefinition => [it.name = name.canonize] | ||
253 | val variableMap = new ArrayList(parameters.size) | ||
254 | var index = 0 | ||
255 | for(parameter : parameters) { | ||
256 | val actualIndex = index | ||
257 | val newVar = createVariable=>[it.name ='''var «actualIndex»'''.canonize it.range = parameter.toTypeReference] | ||
258 | variableMap.add(index,newVar) | ||
259 | res.variables+=newVar | ||
260 | res.parameters+=newVar.range | ||
261 | index+=1 | ||
262 | } | ||
263 | res.value = possibleValues.map[possibleValue |(0..<parameters.size).map[i| variableMap.get(i) == possibleValue.get(i).toTerm].And].Or | ||
264 | return res | ||
265 | } | ||
266 | |||
267 | // Add Relation to a problem | ||
268 | def public add(LogicProblem input, Relation relation) { | ||
269 | input.nameIfAnonymRelation(relation) | ||
270 | input.checkRelation(relation) | ||
271 | input.relations+=relation | ||
272 | //println('''«relation.name» - [«relation.parameters»]''') | ||
273 | return relation | ||
274 | } | ||
275 | |||
276 | def protected nameIfAnonymRelation(LogicProblem problem, Relation relation) { | ||
277 | if(relation.name.nullOrEmpty) { | ||
278 | relation.name = problem.relations.map[it.name].generateUniqueName[i | "relation"+i] | ||
279 | } | ||
280 | } | ||
281 | def protected checkRelation(LogicProblem problem, Relation relation) { | ||
282 | if(problem.relations.exists(x|x.name == relation.name)) | ||
283 | throw new LogicProblemBuilderException('''Relation with the following name is already defined: "«relation.name»"!''') | ||
284 | for(ref : relation.parameters.filter(typeof(ComplexTypeReference)).map[referred]) { | ||
285 | if(!problem.types.contains(ref)) | ||
286 | throw new LogicProblemBuilderException('''Type "«ref.name»" is not availabe in the logic problem!''') | ||
287 | } | ||
288 | if(relation instanceof RelationDefinition) { | ||
289 | checkDefinition(relation) | ||
290 | } | ||
291 | } | ||
292 | |||
293 | // Assertion | ||
294 | def public Assertion(TermDescription term) { | ||
295 | val result = term.toTerm | ||
296 | result.nameAnonymVariables(Collections.EMPTY_LIST) | ||
297 | createAssertion => [it.value = result] | ||
298 | } | ||
299 | def public Assertion(CharSequence name, TermDescription term) { | ||
300 | val result = term.toTerm | ||
301 | result.nameAnonymVariables(Collections.EMPTY_LIST) | ||
302 | createAssertion => [it.value = result it.name=name.canonize] | ||
303 | } | ||
304 | def public add(LogicProblem problem, Assertion assertion) { | ||
305 | if(assertion.name.nullOrEmpty) { | ||
306 | val name = problem.assertions.map[name].generateUniqueName["assertion"+it] | ||
307 | assertion.name=name | ||
308 | } | ||
309 | checkAssertion(assertion) | ||
310 | problem.assertions+=assertion | ||
311 | return assertion | ||
312 | } | ||
313 | |||
314 | def public add(LogicProblem problem, TermDescription term) { | ||
315 | problem.add(Assertion(term)) | ||
316 | } | ||
317 | |||
318 | |||
319 | def checkAssertion(Assertion assertion) { | ||
320 | for(value : assertion.eAllContents.filter(SymbolicValue).toIterable) { | ||
321 | var referred = value.symbolicReference | ||
322 | if(referred instanceof Variable) { | ||
323 | if(!value.hasDeclaredVariable(referred)){ | ||
324 | throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''') | ||
325 | } | ||
326 | } | ||
327 | } | ||
328 | } | ||
329 | |||
330 | def public checkDefinition(EObject definition) { | ||
331 | /*for(value : definition.eAllContents.filter(SymbolicValue).toIterable) { | ||
332 | var referred = value.symbolicReference | ||
333 | if(referred instanceof Variable) { | ||
334 | if(!value.hasDeclaredVariable(referred)){ | ||
335 | throw new LogicProblemBuilderException('''Variable "«referred.name»" is not availabe in the logic problem!''') | ||
336 | } | ||
337 | } | ||
338 | }*/ | ||
339 | } | ||
340 | |||
341 | // Containment | ||
342 | def public ContainmentHierarchy( | ||
343 | Iterable<? extends Type> typesInHierarchy, | ||
344 | Iterable<? extends Function> containmentFunctions, | ||
345 | Iterable<? extends Relation> containmentRelations, | ||
346 | Constant rootConstant | ||
347 | ) { | ||
348 | val result = createContainmentHierarchy => [ | ||
349 | it.typesOrderedInHierarchy += typesInHierarchy | ||
350 | it.containmentFunctions += containmentFunctions | ||
351 | it.containmentRelations += containmentRelations | ||
352 | it.rootConstant = rootConstant | ||
353 | ] | ||
354 | return result | ||
355 | } | ||
356 | def public add(LogicProblem problem, ContainmentHierarchy hierarchy) { | ||
357 | problem.containmentHierarchies+=hierarchy | ||
358 | return hierarchy | ||
359 | } | ||
360 | |||
361 | // Terms | ||
362 | |||
363 | private dispatch def boolean hasDeclaredVariable(QuantifiedExpression term, Variable variable) { | ||
364 | return term.quantifiedVariables.contains(variable) || ((term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable)) | ||
365 | } | ||
366 | private dispatch def boolean hasDeclaredVariable(Term term, Variable variable) { | ||
367 | return (term.eContainer instanceof Term) && (term.eContainer as Term).hasDeclaredVariable(variable) | ||
368 | } | ||
369 | private dispatch def boolean hasDeclaredVariable(RelationDefinition relation, Variable variable) { | ||
370 | relation.variables.contains(variable) | ||
371 | } | ||
372 | private dispatch def boolean hasDeclaredVariable(Void term, Variable variable) { | ||
373 | return false | ||
374 | } | ||
375 | |||
376 | def protected void nameAnonymVariables(EObject termSegment, List<String> previousNames) { | ||
377 | if(termSegment instanceof QuantifiedExpression) { | ||
378 | val newNames = new LinkedList(previousNames) | ||
379 | for(variable : termSegment.quantifiedVariables) { | ||
380 | var String newName | ||
381 | if(variable.name.nullOrEmpty) { | ||
382 | newName = newNames.generateUniqueName[i | | ||
383 | var x = variable.range.variableAnonymName | ||
384 | x+="var"+i.toString | ||
385 | //println(x) | ||
386 | return x | ||
387 | ] | ||
388 | variable.name = newName | ||
389 | } | ||
390 | else newName = variable.name | ||
391 | newNames+= newName | ||
392 | } | ||
393 | termSegment.expression.nameAnonymVariables(newNames) | ||
394 | } | ||
395 | else { | ||
396 | for(subTerm : termSegment.eContents) { | ||
397 | subTerm.nameAnonymVariables(previousNames) | ||
398 | } | ||
399 | } | ||
400 | } | ||
401 | def protected dispatch String variableAnonymName(BoolTypeReference ref) { "bool" } | ||
402 | def protected dispatch String variableAnonymName(IntTypeReference ref) { "int" } | ||
403 | def protected dispatch String variableAnonymName(RealTypeReference ref) { "real" } | ||
404 | def protected dispatch String variableAnonymName(ComplexTypeReference ref) { ref.referred.name.toLowerCase } | ||
405 | |||
406 | def protected allSubterms(Term term) { | ||
407 | val content = term.eAllContents | ||
408 | val result = new ArrayList<EObject>(content.size+1) | ||
409 | result+=term | ||
410 | result+=content.toIterable | ||
411 | return result; | ||
412 | } | ||
413 | |||
414 | def public Term toTerm(TermDescription term) { | ||
415 | if(term instanceof Term) return term | ||
416 | else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] | ||
417 | else if (term instanceof Constant) return term.call() | ||
418 | else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term] | ||
419 | else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) | ||
420 | } | ||
421 | |||
422 | def public !(TermDescription term) { Not(term) } | ||
423 | def public Not(TermDescription term) { createNot => [operand = term.toTerm] } | ||
424 | |||
425 | def public &&(TermDescription a, TermDescription b) { And(a,b) } | ||
426 | def public And(TermDescription... terms) { return And(terms as Iterable<? extends TermDescription>) } | ||
427 | def public And(Iterable<? extends TermDescription> terms) { createAnd => [operands += terms.map[toTerm]] } | ||
428 | |||
429 | def public ||(TermDescription a, TermDescription b) { Or(a,b) } | ||
430 | def public Or(TermDescription... terms) { Or(terms as Iterable<? extends TermDescription>) } | ||
431 | def public Or(Iterable<? extends TermDescription> terms) { createOr => [operands += terms.map[toTerm]] } | ||
432 | |||
433 | def public =>(TermDescription a, TermDescription b) { Impl(a,b) } | ||
434 | def public Impl(TermDescription a, TermDescription b) { createImpl => [leftOperand = a.toTerm rightOperand = b.toTerm] } | ||
435 | |||
436 | def public <=>(TermDescription a, TermDescription b) { Iff(a,b)} | ||
437 | def public Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] } | ||
438 | |||
439 | def public ITE(TermDescription condition, TermDescription ifTrue, TermDescription ifFalse) { | ||
440 | createIfThenElse => [it.condition = condition.toTerm it.ifTrue = ifTrue.toTerm it.ifFalse = ifFalse.toTerm] | ||
441 | } | ||
442 | |||
443 | def public >(TermDescription left, TermDescription right) { MoreThan(left,right)} | ||
444 | def public MoreThan(TermDescription left, TermDescription right) { createMoreThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
445 | |||
446 | def public <(TermDescription left, TermDescription right) { LessThan(left,right)} | ||
447 | def public LessThan(TermDescription left, TermDescription right) { createLessThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
448 | |||
449 | def public <=(TermDescription left, TermDescription right) { LessOrEqual(left,right) } | ||
450 | def public LessOrEqual(TermDescription left, TermDescription right) { createLessOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
451 | |||
452 | def public >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) } | ||
453 | def public MoreOrEqual(TermDescription left, TermDescription right) { createMoreOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
454 | |||
455 | def public ==(TermDescription left, TermDescription right) {Equals(left,right)} | ||
456 | def public Equals(TermDescription left, TermDescription right) { createEquals => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
457 | |||
458 | def public !=(TermDescription left, TermDescription right) { Distinct(left,right) } | ||
459 | def public Distinct(TermDescription... terms) { return Distinct(terms as Iterable<? extends TermDescription>) } | ||
460 | def public Distinct(Iterable<? extends TermDescription> terms) { createDistinct => [operands += terms.map[toTerm]] } | ||
461 | |||
462 | def public +(TermDescription left, TermDescription right) { Plus(left,right) } | ||
463 | def public Plus(TermDescription left, TermDescription right) { createPlus => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
464 | |||
465 | def public -(TermDescription left, TermDescription right) { Minus(left,right) } | ||
466 | def public Minus(TermDescription left, TermDescription right) { createMinus => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
467 | |||
468 | def public *(TermDescription left, TermDescription right) { Multiply(left,right) } | ||
469 | def public Multiply(TermDescription left, TermDescription right) { createMultiply => [leftOperand=left.toTerm rightOperand=right.toTerm] } | ||
470 | |||
471 | def public /(TermDescription left, TermDescription right) { Divide(left,right) } | ||
472 | def public Divide(TermDescription left, TermDescription right) { createDivison => [leftOperand = left.toTerm rightOperand = right.toTerm]} | ||
473 | |||
474 | def public %(TermDescription left, TermDescription right) { Modulo(left,right) } | ||
475 | def public Modulo(TermDescription left, TermDescription right) { createMod => [leftOperand = left.toTerm rightOperand = right.toTerm]} | ||
476 | |||
477 | def public asTerm(boolean value) { createBoolLiteral => [x|x.value = value] } | ||
478 | def public asTerm(int value) { createIntLiteral => [x|x.value = value] } | ||
479 | def public asTerm(double value) { createRealLiteral => [x|x.value = BigDecimal.valueOf(value)] } | ||
480 | |||
481 | def public InstanceOf(TermDescription term, TypeDescriptor type) { | ||
482 | createInstanceOf => [ | ||
483 | it.value = term.toTerm | ||
484 | it.range = type.toTypeReference | ||
485 | ] | ||
486 | } | ||
487 | |||
488 | // QuantifiedExpressions | ||
489 | |||
490 | def public Forall(Function1<VariableContext, ? extends TermDescription> expression) { | ||
491 | val context = new VariableContext(this,logicFactiory) | ||
492 | val term = expression.apply(context) | ||
493 | return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] | ||
494 | } | ||
495 | def public Forall(TermDescription expression, Variable... variables) { | ||
496 | Forall(variables,expression) } | ||
497 | def public Forall(Iterable<? extends Variable> variables,TermDescription expression) { | ||
498 | val forallExpression = createForall | ||
499 | for(variable : variables) forallExpression.quantifiedVariables += variable | ||
500 | forallExpression.expression = expression.toTerm | ||
501 | return forallExpression | ||
502 | } | ||
503 | |||
504 | def public Exists(Function1<VariableContext, ? extends TermDescription> expression) { | ||
505 | val context = new VariableContext(this,logicFactiory) | ||
506 | val term = expression.apply(context) | ||
507 | return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] | ||
508 | } | ||
509 | def public Exists(TermDescription expression, Variable... variables) { | ||
510 | Exists(variables,expression) } | ||
511 | def public Exists(Iterable<? extends Variable> variables, TermDescription expression) { | ||
512 | val existsExpression = createExists | ||
513 | for(variable : variables) existsExpression.quantifiedVariables += variable | ||
514 | existsExpression.expression = expression.toTerm | ||
515 | return existsExpression | ||
516 | } | ||
517 | |||
518 | // Function calls | ||
519 | def public call(Function function, TermDescription... substitutions) { | ||
520 | call(function, substitutions as Iterable<? extends TermDescription>) } | ||
521 | def public call(Function function, Iterable<? extends TermDescription> substitutions) { | ||
522 | val functionReference = createSymbolicValue | ||
523 | functionReference.symbolicReference=function | ||
524 | val List<TermDescription> l= new LinkedList() | ||
525 | l.addAll(substitutions) | ||
526 | for(substitution : l) | ||
527 | functionReference.parameterSubstitutions += substitution.toTerm | ||
528 | functionReference.checkFunctionCall(function) | ||
529 | return functionReference | ||
530 | } | ||
531 | def private checkFunctionCall(SymbolicValue value, Function referredFunction) { | ||
532 | if(value.parameterSubstitutions.size != referredFunction.parameters.size) | ||
533 | throw new LogicProblemBuilderException( | ||
534 | '''The function called has «referredFunction.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''') | ||
535 | } | ||
536 | |||
537 | // Relation calls | ||
538 | def public call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable<? extends TermDescription>)} | ||
539 | def public call(Relation relation, Iterable<? extends TermDescription> substitution) { | ||
540 | val relationReference = createSymbolicValue | ||
541 | relationReference.symbolicReference = relation | ||
542 | //println('''«relation.name»(«substitution.size»->«relation.parameters»)''') | ||
543 | for(value : substitution) | ||
544 | relationReference.parameterSubstitutions += value.toTerm | ||
545 | relationReference.checkRelationCall(relation) | ||
546 | return relationReference | ||
547 | } | ||
548 | def private checkRelationCall(SymbolicValue value, Relation referredRelation) { | ||
549 | if(value.parameterSubstitutions.size != referredRelation.parameters.size) { | ||
550 | throw new LogicProblemBuilderException( | ||
551 | '''The relation "«referredRelation.name»" called has «referredRelation.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''') | ||
552 | } | ||
553 | } | ||
554 | |||
555 | // constant evaluation | ||
556 | def public call(Constant constant) { | ||
557 | val constantReference = createSymbolicValue | ||
558 | constantReference.symbolicReference = constant | ||
559 | return constantReference | ||
560 | } | ||
561 | |||
562 | |||
563 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
6 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
7 | |||
8 | abstract class LogicReasoner { | ||
9 | def abstract LogicResult solve( | ||
10 | LogicProblem problem, | ||
11 | LogicSolverConfiguration configuration, | ||
12 | ReasonerWorkspace workspace) throws LogicReasonerException | ||
13 | def abstract LogicModelInterpretation getInterpretation(ModelResult modelResult) | ||
14 | } | ||
15 | |||
16 | public class LogicReasonerException extends Exception { | ||
17 | new(String message, Exception cause) { super(message,cause) } | ||
18 | new(Exception cause) { super("The reasoner has failed",cause)} | ||
19 | new(String message) { super(message) } | ||
20 | } | ||
21 | |||
22 | abstract class LogicSolverConfiguration { | ||
23 | public static val Unlimited = -1; | ||
24 | public static val String UndefinedPath = null | ||
25 | |||
26 | /** The URI string to the independent solver application */ | ||
27 | public String solverPath = UndefinedPath | ||
28 | /** Max runtime limit in seconds. */ | ||
29 | public int runtimeLimit = Unlimited | ||
30 | /** Max runtime limit in seconds. */ | ||
31 | public int memoryLimit = Unlimited | ||
32 | |||
33 | public var TypeScopes typeScopes = new TypeScopes; | ||
34 | public var SolutionScope solutionScope = new SolutionScope | ||
35 | } | ||
36 | |||
37 | public class TypeScopes{ | ||
38 | public static val Unlimited = -1; | ||
39 | public var maxIntScope = Unlimited | ||
40 | public var minNewElements = 0 | ||
41 | public var maxNewElements = Unlimited | ||
42 | } | ||
43 | |||
44 | public class SolutionScope{ | ||
45 | public static val Unlimited = -1; | ||
46 | public var numberOfRequiredSolution = 1 | ||
47 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
46 | import java.math.BigDecimal | ||
47 | import java.util.ArrayList | ||
48 | import java.util.Collection | ||
49 | import java.util.Collections | ||
50 | import java.util.HashMap | ||
51 | import java.util.LinkedList | ||
52 | import java.util.List | ||
53 | import java.util.Map | ||
54 | |||
55 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
56 | import org.eclipse.xtend.lib.annotations.Data | ||
57 | |||
58 | @Data class InterpretationValidationResult { | ||
59 | val List<String> problems; | ||
60 | val List<Assertion> invalidAssertions; | ||
61 | def isValid() { return problems.empty && invalidAssertions.empty} | ||
62 | } | ||
63 | |||
64 | class LogicStructureBuilder{ | ||
65 | val protected extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
66 | |||
67 | def public dispatch Collection<DefinedElement> getElements(LogicModelInterpretation interpretation, TypeDeclaration type) { | ||
68 | return interpretation.getElements(type) | ||
69 | } | ||
70 | def public dispatch Collection<DefinedElement> getElements(LogicModelInterpretation interpretation, TypeDefinition type) { | ||
71 | return type.elements | ||
72 | } | ||
73 | |||
74 | def public Term evalAsTerm(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap).toTerm } | ||
75 | def public boolean evalAsBool(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Boolean} | ||
76 | def public int evalAsInt(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as Integer } | ||
77 | def public BigDecimal evalAsReal(LogicModelInterpretation interpretation, TermDescription term) { term.termDescriptiontoTerm.resolve(interpretation, emptyMap) as BigDecimal } | ||
78 | /** | ||
79 | * Evaluate the expression on a solution to an logic element. | ||
80 | * @param interpretation The interpretation which the expression is evaluated on. | ||
81 | * @param term An expression which results in a logic element. | ||
82 | * @return The logic element value of the expression. Returns the element directly, not a symbolic reference! | ||
83 | */ | ||
84 | def public DefinedElement evalAsElement(LogicModelInterpretation interpretation, TermDescription term) { term.resolve(interpretation,emptyMap) as DefinedElement} | ||
85 | /** | ||
86 | * Checks if the interpretation is a valid solution of the problem by checking the satisfactions of each assertion. | ||
87 | * Returns the collection of failed assertions. | ||
88 | * @param interpretation The checked interpretation. | ||
89 | * @param problem The interpretation is checked on this problem. | ||
90 | * @return The collection of failed assertions. | ||
91 | */ | ||
92 | def public validateInterpretationOnProblem(LogicModelInterpretation interpretation, LogicProblem problem) { | ||
93 | val List<String> problems = new LinkedList | ||
94 | |||
95 | // Checking types | ||
96 | val type2ElementsMap = problem.types.toInvertedMap[interpretation.getElements(it)] | ||
97 | |||
98 | // Checking definition does not changed | ||
99 | for(type : problem.types.filter(TypeDefinition)) { | ||
100 | val elements = type2ElementsMap.get(type) | ||
101 | if(!type.elements.containsAll(elements)) | ||
102 | problems+='''The interpretation of «type.name» does not contains each elements of the problem''' | ||
103 | if(!elements.containsAll(type.elements)) | ||
104 | problems+='''The interpretation of «type.name» does not contains additional elements not specified in the problem''' | ||
105 | } | ||
106 | // Checking the type table | ||
107 | val allElements = type2ElementsMap.values.flatten.toSet | ||
108 | for (element : allElements) { | ||
109 | if(! checkElement(problem, type2ElementsMap, element)) { | ||
110 | problems += '''«element.name» does not follows the type hierarchy''' | ||
111 | } | ||
112 | } | ||
113 | |||
114 | // Checking assertions | ||
115 | val List<Assertion> invalidAssertions = new LinkedList | ||
116 | for(assertion : problem.assertions) { | ||
117 | if(! interpretation.evalAsBool(assertion.value)) { | ||
118 | invalidAssertions+= assertion | ||
119 | problems += '''«assertion.name» is violated!''' | ||
120 | } | ||
121 | } | ||
122 | return new InterpretationValidationResult(problems,invalidAssertions) | ||
123 | //problem.assertions.filter[x | ! interpretation.evalAsBool(x.value)] | ||
124 | } | ||
125 | |||
126 | private def checkElement(LogicProblem problem, Map<Type, List<DefinedElement>> type2ElementsMap, DefinedElement element) { | ||
127 | val compatibleDynamicTypes = new LinkedList | ||
128 | for(possibleDynamicType: problem.types.filter[!it.isIsAbstract]) { | ||
129 | //println(possibleDynamicType.name) | ||
130 | val compatibleTypes = possibleDynamicType.transitiveClosureStar[it.supertypes] | ||
131 | //compatibleTypes.forEach[print(''' + «it.name»''')] | ||
132 | val incompatibleTypes = problem.types.filter[!compatibleTypes.contains(it)] | ||
133 | //incompatibleTypes.forEach[print(''' - «it.name»''')] | ||
134 | if(compatibleTypes.forall[ type2ElementsMap.get(it).contains(element)] && incompatibleTypes.forall[!type2ElementsMap.get(it).contains(element)]) { | ||
135 | //println("Ok") | ||
136 | compatibleDynamicTypes += possibleDynamicType | ||
137 | } | ||
138 | } | ||
139 | return compatibleDynamicTypes.size == 1 | ||
140 | } | ||
141 | |||
142 | def protected dispatch Term toTerm(Integer o) { createIntLiteral=>[value = o] } | ||
143 | def protected dispatch Term toTerm(BigDecimal o) { createRealLiteral=>[value = o]} | ||
144 | def protected dispatch Term toTerm(Boolean o) { createBoolLiteral=>[value = o]} | ||
145 | def protected dispatch Term toTerm(SymbolicDeclaration o) { createSymbolicValue=>[symbolicReference = o]} | ||
146 | def public Term termDescriptiontoTerm(TermDescription term) { | ||
147 | if(term instanceof Term) return term | ||
148 | else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] | ||
149 | else if (term instanceof Constant) return createSymbolicValue=>[symbolicReference = term] | ||
150 | else if (term instanceof DefinedElement) return createSymbolicValue => [symbolicReference = term] | ||
151 | else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) | ||
152 | } | ||
153 | /** | ||
154 | * Returns if the operation with the numbers in the parameter requires the use of <code>BigDecimal</code>. | ||
155 | */ | ||
156 | def private isBigDecimalRequired(Object... numbers) { return numbers.exists[it instanceof BigDecimal || it instanceof RealLiteral] } | ||
157 | def private dispatch BigDecimal asBigDecimal(IntLiteral i) { i.value.asBigDecimal } | ||
158 | def private dispatch BigDecimal asBigDecimal(RealLiteral i) { i.value.asBigDecimal } | ||
159 | def private dispatch BigDecimal asBigDecimal(Integer i) { BigDecimal.valueOf(i) } | ||
160 | def private dispatch BigDecimal asBigDecimal(BigDecimal i) { i } | ||
161 | def private dispatch Integer asInteger(Integer i) { i } | ||
162 | def private dispatch Integer asInteger(BigDecimal i) { i.intValue } | ||
163 | def private dispatch Integer asInteger(IntLiteral i) { i.value.asInteger } | ||
164 | |||
165 | // Atomic resoulutions | ||
166 | def protected dispatch Object resolve(IntLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value as Integer } | ||
167 | def protected dispatch Object resolve(BoolLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value } | ||
168 | def protected dispatch Object resolve(RealLiteral literal, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { return literal.value as BigDecimal } | ||
169 | |||
170 | def protected dispatch Object resolve(Not not, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
171 | return ! (not.operand.resolve(interpretation,variableBinding) as Boolean) } | ||
172 | def protected dispatch Object resolve(And and, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
173 | //for(operand : and.operands) { | ||
174 | //val r = operand.resolve(interpretation,variableBinding) as Boolean | ||
175 | //println(r) | ||
176 | //} | ||
177 | return and.operands.forall[resolve(interpretation,variableBinding) as Boolean] as Boolean } | ||
178 | def protected dispatch Object resolve(Or or, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
179 | //val resolved = or.operands.map[resolve(interpretation,variableBinding) as Boolean] | ||
180 | //println(resolved) | ||
181 | return or.operands.exists[resolve(interpretation,variableBinding) as Boolean] } | ||
182 | def protected dispatch Object resolve(Impl impl, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
183 | val left = impl.leftOperand. resolve(interpretation,variableBinding) as Boolean | ||
184 | val right = impl.rightOperand.resolve(interpretation,variableBinding) as Boolean | ||
185 | return (! left) || (right) } | ||
186 | def protected dispatch Object resolve(Iff iff, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
187 | return (iff.leftOperand.resolve(interpretation,variableBinding) as Boolean) == | ||
188 | (iff.rightOperand.resolve(interpretation,variableBinding) as Boolean) } | ||
189 | def protected dispatch Object resolve(IfThenElse ite, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
190 | val condition = ite.condition.resolve(interpretation,variableBinding) as Boolean | ||
191 | if(condition) return ite.ifTrue.resolve(interpretation,variableBinding) | ||
192 | else return ite.ifFalse.resolve(interpretation,variableBinding) | ||
193 | } | ||
194 | def protected dispatch Object resolve(MoreThan moreThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
195 | val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
196 | val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
197 | if(isBigDecimalRequired(left,right)) { | ||
198 | return left.asBigDecimal.compareTo(right.asBigDecimal) > 0 } | ||
199 | else { return left.asInteger > right.asInteger } } | ||
200 | def protected dispatch Object resolve(LessThan lessThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
201 | val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
202 | val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
203 | if(isBigDecimalRequired(left,right)) { | ||
204 | return left.asBigDecimal.compareTo(right.asBigDecimal) < 0 } | ||
205 | else { return left.asInteger < right.asInteger } } | ||
206 | def protected dispatch Object resolve(MoreOrEqualThan moreThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
207 | val left = moreThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
208 | val right = moreThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
209 | if(isBigDecimalRequired(left,right)) { | ||
210 | return left.asBigDecimal.compareTo(right.asBigDecimal) >= 0 } | ||
211 | else { return left.asInteger >= right.asInteger } } | ||
212 | def protected dispatch Object resolve(LessOrEqualThan lessThan, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
213 | val left = lessThan.leftOperand.resolve(interpretation,variableBinding) as Number | ||
214 | val right = lessThan.rightOperand.resolve(interpretation,variableBinding) as Number | ||
215 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.compareTo(right.asBigDecimal) <= 0 | ||
216 | else { return left.asInteger <= right.asInteger } } | ||
217 | |||
218 | |||
219 | def protected dispatch Object resolve(Equals equals, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
220 | val left = equals.leftOperand.resolve(interpretation,variableBinding) | ||
221 | val right = equals.rightOperand.resolve(interpretation,variableBinding) | ||
222 | return compare(left,right) | ||
223 | } | ||
224 | def protected dispatch Object resolve(Distinct distinct, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
225 | val elements = distinct.operands.map[it.resolve(interpretation,variableBinding)] | ||
226 | if(elements.size== 0) return true | ||
227 | else { | ||
228 | val res = (0..<elements.size).forall[i | | ||
229 | (0..<i).forall[j| | ||
230 | ! this.compare(elements.get(i),elements.get(j))]] | ||
231 | //println('''«elements» = «res»''') | ||
232 | return res | ||
233 | } | ||
234 | |||
235 | //return elements.forall[x| elements.filter[it!=x].forall[y | x != y ]] | ||
236 | } | ||
237 | |||
238 | def protected dispatch Object resolve(Plus plus, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
239 | val left = plus.leftOperand.resolve(interpretation,variableBinding) as Number | ||
240 | val right = plus.rightOperand.resolve(interpretation,variableBinding) as Number | ||
241 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.add(right.asBigDecimal) | ||
242 | else return left.asInteger + right.asInteger | ||
243 | } | ||
244 | def protected dispatch Object resolve(Minus minus, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
245 | val left = minus.leftOperand.resolve(interpretation,variableBinding) as Number | ||
246 | val right = minus.rightOperand.resolve(interpretation,variableBinding) as Number | ||
247 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.subtract(right.asBigDecimal) | ||
248 | else return left.asInteger - right.asInteger | ||
249 | } | ||
250 | def protected dispatch Object resolve(Multiply multiply, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
251 | val left = multiply.leftOperand.resolve(interpretation,variableBinding) | ||
252 | val right = multiply.rightOperand.resolve(interpretation,variableBinding) | ||
253 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.multiply(right.asBigDecimal) | ||
254 | else return left.asInteger * right.asInteger | ||
255 | } | ||
256 | def protected dispatch Object resolve(Divison divide, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
257 | val left = divide.leftOperand.resolve(interpretation,variableBinding) as Number | ||
258 | val right = divide.rightOperand.resolve(interpretation,variableBinding) as Number | ||
259 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.divide(right.asBigDecimal) | ||
260 | return left.asInteger / right.asInteger | ||
261 | } | ||
262 | def protected dispatch Object resolve(Mod modulo, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
263 | val left = modulo.leftOperand.resolve(interpretation,variableBinding) as Number | ||
264 | val right = modulo.rightOperand.resolve(interpretation,variableBinding) as Number | ||
265 | if(isBigDecimalRequired(left,right)) return left.asBigDecimal.remainder(right.asBigDecimal) | ||
266 | else return left.asInteger % right.asInteger | ||
267 | } | ||
268 | |||
269 | def protected dispatch Object resolve(Exists exists, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
270 | executeExists(exists.expression,interpretation,variableBinding,exists.quantifiedVariables) } | ||
271 | def protected dispatch Object resolve(Forall forall, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
272 | executeForall(forall.expression,interpretation,variableBinding,forall.quantifiedVariables) } | ||
273 | |||
274 | def protected dispatch Object resolve(SymbolicValue symbolicValue, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
275 | val referenced = symbolicValue.symbolicReference | ||
276 | if(referenced instanceof DefinedElement) { | ||
277 | return referenced | ||
278 | } else if(referenced instanceof Variable) { | ||
279 | return variableBinding.get(referenced) | ||
280 | } else if(referenced instanceof FunctionDeclaration) { | ||
281 | val parameterSubstitution = new ArrayList<Object> | ||
282 | if(! symbolicValue.parameterSubstitutions.empty) { | ||
283 | for(place : 0..symbolicValue.parameterSubstitutions.size-1) { | ||
284 | val variable = symbolicValue.parameterSubstitutions.get(place) | ||
285 | parameterSubstitution += variable.resolve(interpretation,variableBinding) | ||
286 | } | ||
287 | } | ||
288 | return interpretation.getInterpretation(referenced,parameterSubstitution) | ||
289 | } else if(referenced instanceof FunctionDefinition) { | ||
290 | val parameterSubstitution = new HashMap<Variable,Object>() | ||
291 | for(place: 0..<referenced.variable.size) { | ||
292 | parameterSubstitution.put( | ||
293 | referenced.variable.get(place), | ||
294 | symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding)) | ||
295 | } | ||
296 | return referenced.value.resolve(interpretation,parameterSubstitution) | ||
297 | } else if(referenced instanceof RelationDeclaration) { | ||
298 | val parameterSubstitunion = new ArrayList<Object> | ||
299 | if(! symbolicValue.parameterSubstitutions.empty) { | ||
300 | for(place : 0..symbolicValue.parameterSubstitutions.size-1) { | ||
301 | val variable = symbolicValue.parameterSubstitutions.get(place) | ||
302 | parameterSubstitunion += variable.resolve(interpretation,variableBinding) | ||
303 | } | ||
304 | } | ||
305 | return (interpretation.getInterpretation(referenced,parameterSubstitunion) as Boolean) | ||
306 | } else if(referenced instanceof RelationDefinition) { | ||
307 | val parameterSubstitution = new HashMap<Variable,Object>() | ||
308 | for(place: 0..<referenced.variables.size) { | ||
309 | parameterSubstitution.put( | ||
310 | referenced.variables.get(place), | ||
311 | symbolicValue.parameterSubstitutions.get(place).resolve(interpretation,variableBinding)) | ||
312 | } | ||
313 | return referenced.value.resolve(interpretation,parameterSubstitution) | ||
314 | } else if(referenced instanceof ConstantDeclaration) { | ||
315 | return interpretation.getInterpretation(referenced) | ||
316 | } else if(referenced instanceof ConstantDefinition) { | ||
317 | return referenced.value.resolve(interpretation,Collections.emptyMap); | ||
318 | } else throw new IllegalArgumentException('''Unknown referred symbol: «referenced»''') | ||
319 | } | ||
320 | |||
321 | // TermDescriptions are reduced to terms | ||
322 | def protected dispatch resolve(Variable variable, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
323 | return variableBinding.get(variable) | ||
324 | } | ||
325 | |||
326 | def protected dispatch resolve(DefinedElement definedElement, LogicModelInterpretation interpretation, Map<Variable,Object> variableBinding) { | ||
327 | return definedElement | ||
328 | } | ||
329 | |||
330 | def private compare(Object left, Object right) { | ||
331 | if(left instanceof Number && right instanceof Number) { | ||
332 | if(isBigDecimalRequired(left as Number,right as Number)) { | ||
333 | return (left as Number).asBigDecimal.compareTo((right as Number).asBigDecimal) == 0 | ||
334 | } else { | ||
335 | return (left as Number).asInteger == (right as Number).asInteger | ||
336 | } | ||
337 | } else return left.equals(right) | ||
338 | } | ||
339 | |||
340 | def allIntegers(LogicModelInterpretation interpretation) { | ||
341 | if(interpretation.minimalInteger <= interpretation.maximalInteger) { | ||
342 | (interpretation.minimalInteger .. interpretation.maximalInteger).map[asInteger] | ||
343 | } else return emptySet | ||
344 | } | ||
345 | |||
346 | def private boolean executeExists( | ||
347 | Term expression, | ||
348 | LogicModelInterpretation interpretation, | ||
349 | Map<Variable,Object> variableBinding, | ||
350 | List<Variable> variablesToBind) | ||
351 | { | ||
352 | if(variablesToBind.empty) { | ||
353 | val res = expression.resolve(interpretation,variableBinding) as Boolean | ||
354 | return res | ||
355 | } | ||
356 | else { | ||
357 | val unfoldedVariable = variablesToBind.head | ||
358 | val possibleValuesType = unfoldedVariable.range | ||
359 | if(possibleValuesType instanceof ComplexTypeReference) { | ||
360 | return this.getElements(interpretation,possibleValuesType.referred).exists[newBinding | | ||
361 | executeExists( | ||
362 | expression, | ||
363 | interpretation, | ||
364 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
365 | variablesToBind.subList(1,variablesToBind.size))] | ||
366 | } else if(possibleValuesType instanceof IntTypeReference) { | ||
367 | return interpretation.allIntegers.exists[newBinding | | ||
368 | executeExists( | ||
369 | expression, | ||
370 | interpretation, | ||
371 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
372 | variablesToBind.subList(1,variablesToBind.size))] | ||
373 | } | ||
374 | else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''') | ||
375 | } | ||
376 | } | ||
377 | |||
378 | def private boolean executeForall( | ||
379 | Term expression, | ||
380 | LogicModelInterpretation interpretation, | ||
381 | Map<Variable,Object> variableBinding, | ||
382 | List<Variable> variablesToBind) | ||
383 | { | ||
384 | if(variablesToBind.empty) { | ||
385 | return expression.resolve(interpretation,variableBinding) as Boolean | ||
386 | } | ||
387 | else { | ||
388 | val unfoldedVariable = variablesToBind.head | ||
389 | val possibleValuesType = unfoldedVariable.range | ||
390 | if(possibleValuesType instanceof ComplexTypeReference) { | ||
391 | return this.getElements(interpretation,possibleValuesType.referred).forall[newBinding | | ||
392 | executeForall( | ||
393 | expression, | ||
394 | interpretation, | ||
395 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
396 | variablesToBind.subList(1,variablesToBind.size))] | ||
397 | } else if(possibleValuesType instanceof IntTypeReference) { | ||
398 | return interpretation.allIntegers.forall[newBinding | | ||
399 | executeForall( | ||
400 | expression, | ||
401 | interpretation, | ||
402 | new HashMap(variableBinding) => [put(unfoldedVariable,newBinding)], | ||
403 | variablesToBind.subList(1,variablesToBind.size))] | ||
404 | } else throw new UnsupportedOperationException('''Quantifying over type "«possibleValuesType»" is unsupported.''') | ||
405 | } | ||
406 | } | ||
407 | } \ No newline at end of file | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
11 | |||
12 | class TracedLogicProblem { | ||
13 | val LogicProblemBuilder builder = new LogicProblemBuilder | ||
14 | val LogicProblem problem = builder.createProblem | ||
15 | |||
16 | def public getProblem() { return problem } | ||
17 | |||
18 | def public add(TypeDeclaration type) { builder.add(problem,type) } | ||
19 | def public add(TypeDefinition type) { builder.add(problem,type) } | ||
20 | def public add(Function function) { builder.add(problem,function) } | ||
21 | def public add(FunctionDescription functionDescription) { builder.add(problem,functionDescription) } | ||
22 | def public add(Relation relation) { builder.add(problem, relation) } | ||
23 | def public add(Constant constant) { builder.add(problem, constant) } | ||
24 | def public add(Assertion assertion) { builder.add(problem,assertion) } | ||
25 | def public add(TermDescription termDescription) { builder.add(problem,termDescription) } | ||
26 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | @Data class TracedOutput<OUTPUT,TRACE> { | ||
4 | OUTPUT output | ||
5 | TRACE trace | ||
6 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
4 | import java.util.List | ||
5 | import java.util.LinkedList | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor | ||
8 | |||
9 | class VariableContext { | ||
10 | val extension LogiclanguageFactory language; | ||
11 | val extension LogicProblemBuilder logicProblemBuilder; | ||
12 | |||
13 | new(LogicProblemBuilder logicProblemBuilder, LogiclanguageFactory language) { | ||
14 | this.logicProblemBuilder = logicProblemBuilder | ||
15 | this.language = language | ||
16 | } | ||
17 | |||
18 | private List<Variable> variables = new LinkedList; | ||
19 | def public getVariables(){variables} | ||
20 | |||
21 | |||
22 | //def public -(TypeDescriptor type) { Variable(type) } | ||
23 | def public Variable addVar(TypeDescriptor type) { | ||
24 | return addVar(null, type); | ||
25 | } | ||
26 | |||
27 | def public Variable addVar(CharSequence variableName, TypeDescriptor type) { | ||
28 | if(variables.exists[name.equals(variableName)]) throw new IllegalArgumentException("Variable with name " + variableName +" is already defined.") | ||
29 | val variable = createVariable => [name = variableName.canonize range = type.toTypeReference] | ||
30 | variables += variable | ||
31 | return variable | ||
32 | } | ||
33 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder.consistencychecker | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
6 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
9 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
10 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.TypeSystemIsInconsistentMatcher | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementNotDefinedInSupertypeMatcher | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.ElementWithNoPossibleDynamicTypeMatcher | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher | ||
17 | |||
18 | class TypeConsistencyChecker extends LogicReasoner{ | ||
19 | val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE | ||
20 | |||
21 | new() { | ||
22 | LogicproblemPackage.eINSTANCE.class | ||
23 | } | ||
24 | |||
25 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
26 | val statistics = createStatistics => [ | ||
27 | it.transformationTime = 0 | ||
28 | it.solverMemory = -1 | ||
29 | ] | ||
30 | |||
31 | val start = System.currentTimeMillis | ||
32 | |||
33 | val queryEngine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
34 | |||
35 | val typeSystemInconsistencyMatcher = TypeSystemIsInconsistentMatcher.on(queryEngine) | ||
36 | val elementNotDefinedInSupertype = ElementNotDefinedInSupertypeMatcher.on(queryEngine) | ||
37 | val elementWithNoPossibleDynamicType = ElementWithNoPossibleDynamicTypeMatcher.on(queryEngine) | ||
38 | val possibleDynamicType = PossibleDynamicTypeMatcher.on(queryEngine) | ||
39 | |||
40 | val hasErrorPatternMatch = typeSystemInconsistencyMatcher.hasMatch(problem) | ||
41 | |||
42 | statistics.solverTime = (System.currentTimeMillis - start) as int | ||
43 | |||
44 | val possibleDynamicTypeStatisticEntry = problem.elements.map[e| | ||
45 | '''«e.name»: [«possibleDynamicType.getAllValuesOfdynamic(problem,e).map[it.name].join(", ")»]''' | ||
46 | ].join("\n") | ||
47 | |||
48 | if(hasErrorPatternMatch) { | ||
49 | return createInconsistencyResult =>[ | ||
50 | it.problem = problem | ||
51 | it.statistics = statistics | ||
52 | it.statistics.entries += createStringStatisticEntry => [ | ||
53 | it.name = "possibleDynamicType" | ||
54 | it.value = possibleDynamicTypeStatisticEntry | ||
55 | ] | ||
56 | it.statistics.entries += createStringStatisticEntry => [ | ||
57 | it.name = "elementNotDefinedInSupertype" | ||
58 | it.value=elementNotDefinedInSupertype.allValuesOfelement.map[it.name].join(", ") | ||
59 | ] | ||
60 | |||
61 | it.statistics.entries += createStringStatisticEntry => [ | ||
62 | it.name = "elementWithNoPossibleDynamicType" | ||
63 | it.value=elementWithNoPossibleDynamicType.allValuesOfelement.map[it.name].join(", ") | ||
64 | ] | ||
65 | ] | ||
66 | } else { | ||
67 | return createUndecidableResult => | ||
68 | [it.problem = problem it.statistics = statistics] | ||
69 | } | ||
70 | } | ||
71 | |||
72 | override getInterpretation(ModelResult modelResult) { | ||
73 | throw new UnsupportedOperationException('''This solver is unable to create interpretations!''') | ||
74 | } | ||
75 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.statistics | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics | ||
6 | import java.util.ArrayList | ||
7 | import java.util.HashMap | ||
8 | import java.util.LinkedList | ||
9 | import java.util.List | ||
10 | import java.util.Map | ||
11 | |||
12 | class StatisticsData { | ||
13 | public var List<Pair<String,String>> inputConfiguration | ||
14 | public var List<Pair<String,String>> outputMetrics | ||
15 | public var Statistics solverStatistics | ||
16 | } | ||
17 | |||
18 | class StatisticSections2CSV { | ||
19 | static val separator = ';' | ||
20 | static val empty = "" | ||
21 | |||
22 | private def getValue(Map<String, String> map,String key) { | ||
23 | if(map.containsKey(key)) return map.get(key) | ||
24 | else return empty | ||
25 | } | ||
26 | private def addKey(List<String> list, String newValue) { | ||
27 | if(! list.contains(newValue)) list+=newValue | ||
28 | } | ||
29 | |||
30 | public def CharSequence transformStatisticDatas2CSV( | ||
31 | List<StatisticsData> statistics) | ||
32 | { | ||
33 | val inputConfigurationColumns = new LinkedList | ||
34 | val inputConfigurationValues = new ArrayList(statistics.length) | ||
35 | val solverStatisticColumns = new LinkedList | ||
36 | val solverStatisticValues = new ArrayList(statistics.length) | ||
37 | val outputMetricColumns = new LinkedList | ||
38 | val outputMetricValues = new ArrayList(statistics.length) | ||
39 | |||
40 | statistics.map[inputConfiguration].indexColumnsForPairs(inputConfigurationColumns, inputConfigurationValues) | ||
41 | statistics.map[it.solverStatistics].indexColumnsForEntries(solverStatisticColumns, solverStatisticValues) | ||
42 | statistics.map[outputMetrics].indexColumnsForPairs(outputMetricColumns,outputMetricValues) | ||
43 | |||
44 | return ''' | ||
45 | ID« // Header | ||
46 | IF inputConfigurationColumns.length>0»«separator»«FOR name : inputConfigurationColumns SEPARATOR separator»«name»«ENDFOR»«ENDIF»« | ||
47 | separator»Transformation_Time«separator»Solver_Time«separator»Solver_Memory« | ||
48 | IF solverStatisticColumns.length>0»«separator»«ENDIF»« | ||
49 | FOR name:solverStatisticColumns SEPARATOR separator»«name»«ENDFOR»« | ||
50 | IF outputMetricColumns.length>0»«separator»«ENDIF»« | ||
51 | FOR name:outputMetricColumns SEPARATOR separator»«name»«ENDFOR» | ||
52 | « // Table | ||
53 | FOR index : 0..<statistics.size» | ||
54 | «index+1 /*ID*/»« | ||
55 | IF inputConfigurationColumns.size>0»«separator»«ENDIF»« | ||
56 | FOR name : inputConfigurationColumns SEPARATOR separator»«inputConfigurationValues.get(index).getValue(name)»«ENDFOR»« | ||
57 | separator»«statistics.get(index).solverStatistics.transformationTime»« | ||
58 | separator»«statistics.get(index).solverStatistics.solverTime»« | ||
59 | separator»«statistics.get(index).solverStatistics.solverMemory»« | ||
60 | IF solverStatisticColumns.size>0»«separator»«ENDIF»« | ||
61 | FOR name:solverStatisticColumns SEPARATOR separator»«solverStatisticValues.get(index).getValue(name)»«ENDFOR»« | ||
62 | IF outputMetricColumns.size>0»«separator»«ENDIF»« | ||
63 | FOR name:outputMetricColumns SEPARATOR separator»«outputMetricValues.get(index).getValue(name)»«ENDFOR» | ||
64 | «ENDFOR»''' | ||
65 | } | ||
66 | |||
67 | def private indexColumnsForPairs(List<List<Pair<String, String>>> datas, List<String> columns, List<Map<String, String>> values) { | ||
68 | for(inputConfiguration : datas) { | ||
69 | val map = new HashMap | ||
70 | for(entry : inputConfiguration) { | ||
71 | columns.addKey(entry.key) | ||
72 | map.put(entry.key,entry.value) | ||
73 | } | ||
74 | values+=map | ||
75 | } | ||
76 | } | ||
77 | def private indexColumnsForEntries(List<Statistics> datas, List<String> columns, List<Map<String, String>> values) { | ||
78 | for(inputConfiguration : datas) { | ||
79 | val map = new HashMap | ||
80 | for(entry : inputConfiguration.entries) { | ||
81 | columns.addKey(entry.name) | ||
82 | map.put(entry.name,entry.readValue) | ||
83 | } | ||
84 | values+=map | ||
85 | } | ||
86 | } | ||
87 | private def dispatch String readValue(IntStatisticEntry e) { return e.value.toString } | ||
88 | private def dispatch String readValue(RealStatisticEntry e){ return e.value.toString } | ||
89 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.statistics | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry | ||
7 | import java.util.List | ||
8 | |||
9 | class StatisticSections2Print { | ||
10 | public def CharSequence transformStatisticDatas2CSV( | ||
11 | List<StatisticEntry> statistics) | ||
12 | { | ||
13 | var result = ""; | ||
14 | for(statistic : statistics) { | ||
15 | result+= '''«statistic.readValue»;''' | ||
16 | } | ||
17 | return result | ||
18 | } | ||
19 | |||
20 | private def dispatch String readValue(IntStatisticEntry e) { return e.value.toString } | ||
21 | private def dispatch String readValue(RealStatisticEntry e){ return e.value.toString } | ||
22 | private def dispatch String readValue(StringStatisticEntry e) { return "\n" + e.value } | ||
23 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.util | ||
2 | |||
3 | import java.util.HashSet | ||
4 | import java.util.LinkedList | ||
5 | import java.util.List | ||
6 | import java.util.Map | ||
7 | import java.util.Set | ||
8 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
9 | import java.util.HashMap | ||
10 | import java.util.LinkedHashMap | ||
11 | |||
12 | class CollectionsUtil { | ||
13 | public def static <FROM,TO> TO lookup(FROM from, Map<? super FROM,TO> map) { | ||
14 | if(map.containsKey(from)) { | ||
15 | return map.get(from) | ||
16 | } else throw new IllegalArgumentException(''' | ||
17 | The map does not contains the key "«from.toString»"! | ||
18 | --- Elements: --- | ||
19 | «FOR entry : map.entrySet SEPARATOR '\n'»«entry.key» -> «entry.value»«ENDFOR» | ||
20 | -----------------'''); | ||
21 | } | ||
22 | public def <FROM,TO> TO ifThenElse(FROM source, Function1<FROM,Boolean> condition, Function1<FROM,TO> ifTrue, Function1<FROM,TO> ifFalse) { | ||
23 | if(condition.apply(source)) { | ||
24 | return ifTrue.apply(source) | ||
25 | } | ||
26 | else { | ||
27 | return ifFalse.apply(source) | ||
28 | } | ||
29 | } | ||
30 | public def static <Key,Value> Union(Map<Key,Value> a, Map<Key,Value> b) { | ||
31 | (a.keySet + b.keySet).toInvertedMap[key | | ||
32 | if(a.containsKey(key)) a.get(key) | ||
33 | else b.get(key) | ||
34 | ] | ||
35 | } | ||
36 | public def static <Key,Value> putOrAddToSet(Map<Key,Set<Value>> map, Key key, Value value) { | ||
37 | if(map.containsKey(key)) { | ||
38 | map.get(key).add(value) | ||
39 | }else{ | ||
40 | val set = new HashSet<Value>() => [it.add(value)] | ||
41 | map.put(key, set) | ||
42 | } | ||
43 | } | ||
44 | public def static <Key,Value> putOrAddToList(Map<Key,List<Value>> map, Key key, Value value) { | ||
45 | if(map.containsKey(key)) { | ||
46 | map.get(key).add(value) | ||
47 | }else{ | ||
48 | val set = new LinkedList<Value>() => [it.add(value)] | ||
49 | map.put(key, set) | ||
50 | } | ||
51 | } | ||
52 | def public static <From,To,Property> Map<From,To> copyMap(Map<From,To> oldMap, Iterable<To> newValues, Function1<To,Property> indexExtractor) { | ||
53 | val Map<Property,To> valueIndexes = oldMap.values.toMap[to|indexExtractor.apply(to)]; | ||
54 | val res = oldMap.mapValues[value | indexExtractor.apply(value).lookup(valueIndexes)] | ||
55 | return res | ||
56 | } | ||
57 | def public static <From,To> Map<To,From> bijectiveInverse(Map<From,To> m) { m.keySet.toMap[x|x.lookup(m)] } | ||
58 | def public static <From,To> Map<To,List<From>> inverse(Map<From,To> m) { | ||
59 | val res = new LinkedHashMap<To,List<From>> | ||
60 | m.entrySet.forEach[res.putOrAddToList(it.value,it.key)] | ||
61 | return res | ||
62 | } | ||
63 | |||
64 | def public static <Type> List<Type> transitiveClosurePlus(Type source, Function1<Type,Iterable<Type>> next) { | ||
65 | val res = new LinkedList() | ||
66 | transitiveClosureHelper(res,source,next) | ||
67 | return res | ||
68 | } | ||
69 | def public static <Type> List<Type> transitiveClosureStar(Type source, Function1<Type,Iterable<Type>> next) { | ||
70 | val res = new LinkedList() | ||
71 | res += source | ||
72 | transitiveClosureHelper(res,source,next) | ||
73 | return res | ||
74 | } | ||
75 | def private static <Type> void transitiveClosureHelper(List<Type> result, Type actual, Function1<Type,Iterable<Type>> next) { | ||
76 | val front = next.apply(actual) | ||
77 | for(elementInFront : front) { | ||
78 | result += elementInFront | ||
79 | transitiveClosureHelper(result,elementInFront,next) | ||
80 | } | ||
81 | } | ||
82 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.util | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
7 | import java.util.ArrayList | ||
8 | import java.util.Collection | ||
9 | import java.util.List | ||
10 | import java.util.Map | ||
11 | |||
12 | class LogicProblemBuilder_AdvancedConstructs { | ||
13 | val extension LogicProblemBuilder builder; | ||
14 | public new(LogicProblemBuilder builder) { | ||
15 | this.builder = builder | ||
16 | } | ||
17 | |||
18 | def public FunctionDefinitionBody(Iterable<Variable> variables, Map<List<Term>,Term> parametersToValue, Term other) { | ||
19 | val variableList = variables.toList | ||
20 | val entryList = parametersToValue.entrySet.toList | ||
21 | |||
22 | // Size = 0 | ||
23 | if(entryList.empty && other === null) { | ||
24 | throw new IllegalArgumentException('''No possible value is specified!''') | ||
25 | // Size = 1 | ||
26 | } else if(entryList.size == 1 && other === null) { | ||
27 | return entryList.head.value | ||
28 | // Size = 1 | ||
29 | } else if(entryList.empty && !(other === null)) { | ||
30 | return other | ||
31 | // Size > 1 | ||
32 | }else { | ||
33 | // Transforming values to IF-Then-Else structures | ||
34 | /**The number of IF-THEN-ELSE structures needed*/ | ||
35 | var int iteNumber | ||
36 | if(other === null) iteNumber = entryList.size-1 | ||
37 | else iteNumber = entryList.size | ||
38 | |||
39 | val ites = new ArrayList<IfThenElse>(iteNumber) | ||
40 | for (element : 0 ..< iteNumber) { | ||
41 | ites += ITE( | ||
42 | entryList.get(element).key.substitutionIsEqual(variableList), | ||
43 | entryList.get(element).value, | ||
44 | null) | ||
45 | } | ||
46 | |||
47 | // Linking the IF-Then-Else structures to a chain | ||
48 | for (optionIndex : 1 ..< ites.size) { | ||
49 | val prev = ites.get(optionIndex - 1) | ||
50 | val next = ites.get(optionIndex) | ||
51 | prev.ifFalse = next | ||
52 | } | ||
53 | |||
54 | if(other === null) ites.last.ifFalse = entryList.last.value | ||
55 | else ites.last.ifFalse = other | ||
56 | |||
57 | // return the head of the chain | ||
58 | return ites.head | ||
59 | } | ||
60 | } | ||
61 | |||
62 | def public RelationDefinitionBody(Iterable<Variable> variables, Collection<List<Term>> elements) { | ||
63 | val variableList = variables.toList | ||
64 | return elements.map[row | row.substitutionIsEqual(variableList)].Or | ||
65 | } | ||
66 | |||
67 | def private substitutionIsEqual(List<Term> substitution, List<Variable> variables) { | ||
68 | val parameterIndexes = 0..<variables.size | ||
69 | return And(parameterIndexes.map[index | substitution.get(index) == variables.get(index)]) | ||
70 | } | ||
71 | } \ No newline at end of file | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/SetWithCustomEquivalence.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/SetWithCustomEquivalence.xtend new file mode 100644 index 00000000..ae2cfb04 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/util/SetWithCustomEquivalence.xtend | |||
@@ -0,0 +1,103 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.util | ||
2 | |||
3 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
4 | import java.util.HashMap | ||
5 | import java.util.Set | ||
6 | import java.util.Collection | ||
7 | import java.util.HashSet | ||
8 | |||
9 | class SetWithCustomEquivalence<Type,Representation> implements Set<Type>{ | ||
10 | val Function1<Type,Representation> representer; | ||
11 | val HashMap<Representation,Type> map | ||
12 | |||
13 | public new(Function1<Type,Representation> representer) { | ||
14 | this.representer = representer | ||
15 | this.map = new HashMap<Representation,Type> | ||
16 | } | ||
17 | public new(Function1<Type,Representation> representer, Collection<? extends Type> initialElements) { | ||
18 | this.representer = representer | ||
19 | this.map = new HashMap | ||
20 | initialElements.forEach[add] | ||
21 | } | ||
22 | |||
23 | override add(Type arg0) { | ||
24 | val representation = representer.apply(arg0) | ||
25 | if(!map.containsKey(representation)) { | ||
26 | map.put(representation,arg0); | ||
27 | return true | ||
28 | } else return false | ||
29 | } | ||
30 | |||
31 | override addAll(Collection<? extends Type> arg0) { | ||
32 | val originalSize = this.size | ||
33 | arg0.forEach[add(it)] | ||
34 | return (this.size != originalSize) | ||
35 | } | ||
36 | |||
37 | override clear() { | ||
38 | map.clear | ||
39 | } | ||
40 | |||
41 | override contains(Object arg0) { | ||
42 | try { | ||
43 | val rep = this.representer.apply(arg0 as Type) | ||
44 | return map.containsKey(rep) | ||
45 | } catch (ClassCastException e) { | ||
46 | return false | ||
47 | } | ||
48 | } | ||
49 | |||
50 | override containsAll(Collection<?> arg0) { | ||
51 | arg0.forall[it.contains] | ||
52 | } | ||
53 | |||
54 | override isEmpty() { | ||
55 | return map.isEmpty | ||
56 | } | ||
57 | |||
58 | override iterator() { | ||
59 | return map.values.iterator | ||
60 | } | ||
61 | |||
62 | override remove(Object arg0) { | ||
63 | try { | ||
64 | val rep = this.representer.apply(arg0 as Type) | ||
65 | return map.remove(rep) != null | ||
66 | } catch (ClassCastException e) { | ||
67 | return false | ||
68 | } | ||
69 | } | ||
70 | |||
71 | override removeAll(Collection<?> arg0) { | ||
72 | val originalSize = this.size | ||
73 | arg0.forEach[remove(it)] | ||
74 | return (this.size != originalSize) | ||
75 | } | ||
76 | |||
77 | override retainAll(Collection<?> arg0) { | ||
78 | val Set<Representation> representationsOfArg0 = new HashSet | ||
79 | for(element: arg0) { | ||
80 | try { | ||
81 | representationsOfArg0 += this.representer.apply(element as Type) | ||
82 | } catch(ClassCastException e) {} | ||
83 | } | ||
84 | val originalSize = this.size | ||
85 | for(r:this.map.keySet) { | ||
86 | if(!representationsOfArg0.contains(r)) | ||
87 | this.map.remove(r) | ||
88 | } | ||
89 | return (this.size != originalSize) | ||
90 | } | ||
91 | |||
92 | override size() { | ||
93 | return this.map.size | ||
94 | } | ||
95 | |||
96 | override toArray() { | ||
97 | map.values.toArray | ||
98 | } | ||
99 | |||
100 | override <T> toArray(T[] arg0) { | ||
101 | map.values.toArray(arg0) | ||
102 | } | ||
103 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.util.visualisation | ||
2 | |||
3 | class Interpretation2Gml { | ||
4 | |||
5 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.workspace | ||
2 | |||
3 | import java.io.BufferedReader | ||
4 | import java.io.FileReader | ||
5 | import java.io.PrintWriter | ||
6 | import org.eclipse.emf.common.util.URI | ||
7 | import java.io.File | ||
8 | |||
9 | class FileSystemWorkspace extends ReasonerWorkspace{ | ||
10 | |||
11 | new(String targetFolder, String prefix) { | ||
12 | super(targetFolder/*.replaceAll("\\\\","/").replaceAll("/\\.","")*/, prefix) | ||
13 | } | ||
14 | |||
15 | override protected getURI(String name) { | ||
16 | URI.createFileURI(targetFolder + "/" + prefix + name) | ||
17 | } | ||
18 | |||
19 | def protected getFolderURI() { | ||
20 | URI.createFileURI(targetFolder) | ||
21 | } | ||
22 | |||
23 | override getWorkspaceURI() { | ||
24 | getFolderURI | ||
25 | } | ||
26 | |||
27 | override initAndClear() { | ||
28 | val folder = new File(folderURI.toFileString) | ||
29 | folder.mkdirs | ||
30 | for(file : folder.listFiles) { | ||
31 | file.deleteFile | ||
32 | } | ||
33 | } | ||
34 | |||
35 | def void deleteFile(File file) { | ||
36 | if (file.isDirectory()) { | ||
37 | file.listFiles().forEach[deleteFile] | ||
38 | file.delete | ||
39 | } else { | ||
40 | file.delete; | ||
41 | } | ||
42 | } | ||
43 | |||
44 | override writeText(String name, CharSequence content) { | ||
45 | val uri = getURI(name) | ||
46 | val writer = new PrintWriter(uri.toFileString, "UTF-8"); | ||
47 | writer.println(content); | ||
48 | writer.close(); | ||
49 | return uri | ||
50 | } | ||
51 | |||
52 | override readText(String name) { | ||
53 | var String line; | ||
54 | var String result = ""; | ||
55 | val in = new BufferedReader(new FileReader(getURI(name).toFileString)) | ||
56 | while ((line = in.readLine()) != null) { | ||
57 | result = result.concat(line) | ||
58 | } | ||
59 | in.close | ||
60 | return result | ||
61 | } | ||
62 | |||
63 | override protected renameFile(String name) { | ||
64 | val uri = getURI(name) | ||
65 | val uri2 = getURI(name+deactivationPostfix) | ||
66 | val file = new File(uri. toFileString) | ||
67 | val file2 = new File(uri2.toFileString) | ||
68 | file.renameTo(file2) | ||
69 | } | ||
70 | |||
71 | override subWorkspace(String targetFolder, String prefix) { | ||
72 | return new FileSystemWorkspace(this.targetFolder + "/" + targetFolder, this.prefix + prefix) | ||
73 | } | ||
74 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.workspace | ||
2 | |||
3 | import java.io.BufferedReader | ||
4 | import java.io.ByteArrayInputStream | ||
5 | import java.io.IOException | ||
6 | import java.io.InputStreamReader | ||
7 | import org.eclipse.core.resources.IContainer | ||
8 | import org.eclipse.core.resources.IFolder | ||
9 | import org.eclipse.core.resources.IProject | ||
10 | import org.eclipse.core.resources.IWorkspaceRoot | ||
11 | import org.eclipse.core.resources.ResourcesPlugin | ||
12 | import org.eclipse.core.runtime.NullProgressMonitor | ||
13 | import org.eclipse.emf.common.util.URI | ||
14 | |||
15 | class ProjectWorkspace extends ReasonerWorkspace{ | ||
16 | |||
17 | val monitor = new NullProgressMonitor | ||
18 | var IContainer target; | ||
19 | |||
20 | new(String targetFolder, String prefix) { | ||
21 | super(targetFolder, prefix) | ||
22 | } | ||
23 | |||
24 | override protected getURI(String name) { | ||
25 | URI.createPlatformResourceURI(targetFolder + "/" + prefix + name,true); | ||
26 | } | ||
27 | |||
28 | def protected getDirUri() { | ||
29 | URI.createPlatformResourceURI(targetFolder,true) | ||
30 | } | ||
31 | |||
32 | override getWorkspaceURI() { | ||
33 | getDirUri | ||
34 | } | ||
35 | |||
36 | override initAndClear() { | ||
37 | target = ResourcesPlugin.workspace.root | ||
38 | for(nameSegment : dirUri.segments) { | ||
39 | target = createContainer(target,nameSegment) | ||
40 | } | ||
41 | target.members.forEach[delete(false,monitor)] | ||
42 | } | ||
43 | |||
44 | def protected dispatch createContainer(IWorkspaceRoot root, String name) { | ||
45 | val project = root.getProject(name) | ||
46 | if(project.exists) { | ||
47 | if(!project.open) { | ||
48 | project.open(monitor) | ||
49 | } | ||
50 | } else { | ||
51 | project.create(monitor) | ||
52 | } | ||
53 | return project | ||
54 | } | ||
55 | |||
56 | def protected dispatch createContainer(IProject root, String name) { | ||
57 | val folder = root.getFolder(name); | ||
58 | if(folder.exists) { | ||
59 | folder.create(false,true,monitor) | ||
60 | } | ||
61 | return folder | ||
62 | } | ||
63 | |||
64 | def protected dispatch createContainer(IFolder root, String name) { | ||
65 | val folder = root.getFolder(name); | ||
66 | if(folder.exists) { | ||
67 | folder.create(false,true,monitor) | ||
68 | } | ||
69 | return folder | ||
70 | } | ||
71 | |||
72 | def dispatch getTargetFile(IFolder targetFolder, String name) { targetFolder.getFile(name) } | ||
73 | def dispatch getTargetFile(IProject targetProject, String name) { targetProject.getFile(name) } | ||
74 | |||
75 | override writeText(String name, CharSequence content) { | ||
76 | val file = target.getTargetFile(name); | ||
77 | if(!file.exists()) { | ||
78 | file.create(new ByteArrayInputStream(content.toString().getBytes()),true, new NullProgressMonitor()); | ||
79 | return URI.createPlatformResourceURI(file.projectRelativePath.toString,true) | ||
80 | } | ||
81 | else throw new IOException("The file is already existing.") | ||
82 | } | ||
83 | |||
84 | override readText(String name) { | ||
85 | val file = target.getTargetFile(name) | ||
86 | val in = new BufferedReader(new InputStreamReader(file.contents)) | ||
87 | |||
88 | var result = "" | ||
89 | var String line; | ||
90 | |||
91 | while ((line = in.readLine()) != null) { | ||
92 | result = result.concat(line) | ||
93 | } | ||
94 | |||
95 | return result | ||
96 | } | ||
97 | |||
98 | override protected renameFile(String name) { | ||
99 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
100 | } | ||
101 | |||
102 | override subWorkspace(String targetFolder, String prefix) { | ||
103 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
104 | } | ||
105 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.workspace | ||
2 | |||
3 | import java.io.FileNotFoundException | ||
4 | import java.util.Collections | ||
5 | import org.eclipse.emf.common.util.URI | ||
6 | import org.eclipse.emf.ecore.EObject | ||
7 | import org.eclipse.emf.ecore.resource.ResourceSet | ||
8 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | ||
9 | import org.eclipse.emf.ecore.resource.Resource | ||
10 | import java.io.ByteArrayOutputStream | ||
11 | import java.io.IOException | ||
12 | |||
13 | abstract class ReasonerWorkspace{ | ||
14 | |||
15 | protected val String targetFolder; | ||
16 | protected val String prefix; | ||
17 | val ResourceSet resSet = new ResourceSetImpl(); | ||
18 | |||
19 | public new(String targetFolder, String prefix) { | ||
20 | this.targetFolder = targetFolder | ||
21 | this.prefix = prefix | ||
22 | } | ||
23 | |||
24 | public def ReasonerWorkspace subWorkspace(String targetFolder, String prefix); | ||
25 | |||
26 | def URI getWorkspaceURI(); | ||
27 | |||
28 | /** | ||
29 | * Creates the target folder and clears the workspace for the reasoning | ||
30 | */ | ||
31 | def public void initAndClear() | ||
32 | |||
33 | def protected URI getURI(String name); | ||
34 | protected def Resource getResource(String name) { | ||
35 | val prevoius = resSet.getResource(getURI(name),false); | ||
36 | if(prevoius!= null) prevoius.delete(Collections.EMPTY_MAP) | ||
37 | |||
38 | val URI resourceURI = getURI(name) | ||
39 | return resSet.createResource(resourceURI); | ||
40 | } | ||
41 | |||
42 | |||
43 | /** | ||
44 | * Writes a model | ||
45 | */ | ||
46 | def public URI writeModel(EObject modelRoot, String name) { | ||
47 | val resource = getResource(name); | ||
48 | resource.getContents().add(modelRoot); | ||
49 | resource.save(Collections.EMPTY_MAP); | ||
50 | return resource.URI | ||
51 | } | ||
52 | |||
53 | |||
54 | def public String writeModelToString(EObject modelRoot, String name) { | ||
55 | val resource = getResource(name); | ||
56 | resource.getContents().add(modelRoot); | ||
57 | val ByteArrayOutputStream outputStream = new ByteArrayOutputStream(); | ||
58 | resource.save(outputStream, null); | ||
59 | return outputStream.toString(); | ||
60 | } | ||
61 | |||
62 | def public <RootType extends EObject> RootType reloadModel(Class<RootType> type, String name) { | ||
63 | try { | ||
64 | val resource = resSet.getResource(getURI(name),false); | ||
65 | if(resource.loaded) { | ||
66 | resource.unload | ||
67 | } | ||
68 | resource.load(Collections.EMPTY_MAP) | ||
69 | if(resource == null) throw new FileNotFoundException(getURI(name).toString) | ||
70 | else return resource.contents.get(0) as RootType | ||
71 | } catch(Exception e) { | ||
72 | throw new FileNotFoundException(getURI(name).toString) | ||
73 | } | ||
74 | } | ||
75 | |||
76 | def public <RootType extends EObject> RootType readModel(Class<RootType> type, String name) { | ||
77 | try { | ||
78 | val resource = resSet.getResource(getURI(name),true); | ||
79 | if(resource == null) throw new FileNotFoundException(getURI(name).toString) | ||
80 | else return resource.contents.get(0) as RootType | ||
81 | } catch(Exception e) { | ||
82 | throw new FileNotFoundException(getURI(name).toString + "reason: " + e.message) | ||
83 | } | ||
84 | } | ||
85 | |||
86 | def public deactivateModel(String name) { | ||
87 | val resource = resSet.getResource(getURI(name),true); | ||
88 | resource.unload | ||
89 | renameFile(name) | ||
90 | } | ||
91 | val static protected deactivationPostfix = ".deactivated" | ||
92 | def protected void renameFile(String name) | ||
93 | |||
94 | // def void reactivate() | ||
95 | // def void deactivate() | ||
96 | |||
97 | def public URI writeText(String name, CharSequence content); | ||
98 | |||
99 | def public String readText(String name); | ||
100 | } \ No newline at end of file | ||