diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend | 261 |
1 files changed, 151 insertions, 110 deletions
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 index f6bd9541..09bfbb39 100644 --- 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 | |||
@@ -1,5 +1,6 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder | 1 | package hu.bme.mit.inf.dslreasoner.logic.model.builder |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.AggregateExpression | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | 4 | 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.BoolTypeReference |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference |
@@ -8,6 +9,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.Function |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | 10 | 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.LogiclanguageFactory |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ProjectedAggregateExpression | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
@@ -46,16 +48,16 @@ class LogicProblemBuilderException extends Exception { | |||
46 | } | 48 | } |
47 | } | 49 | } |
48 | 50 | ||
49 | public class LogicProblemBuilder{ | 51 | class LogicProblemBuilder{ |
50 | val protected extension LogiclanguageFactory logicFactiory = LogiclanguageFactory.eINSTANCE | 52 | val protected extension LogiclanguageFactory logicFactiory = LogiclanguageFactory.eINSTANCE |
51 | val protected extension LogicproblemFactory problemFactory = LogicproblemFactory.eINSTANCE | 53 | val protected extension LogicproblemFactory problemFactory = LogicproblemFactory.eINSTANCE |
52 | val protected advancedConstructs = new LogicProblemBuilder_AdvancedConstructs(this) | 54 | val protected advancedConstructs = new LogicProblemBuilder_AdvancedConstructs(this) |
53 | 55 | ||
54 | def public createProblem(){ createLogicProblem } | 56 | def createProblem(){ createLogicProblem } |
55 | 57 | ||
56 | // Names | 58 | // Names |
57 | def protected String canonize(CharSequence name) { | 59 | def protected String canonize(CharSequence name) { |
58 | if(name == null) return "" | 60 | if(name === null) return "" |
59 | val result = name.toString.split("\\s+"); | 61 | val result = name.toString.split("\\s+"); |
60 | if(result.size == 1) { | 62 | if(result.size == 1) { |
61 | val element = result.get(0); | 63 | val element = result.get(0); |
@@ -82,23 +84,23 @@ public class LogicProblemBuilder{ | |||
82 | } | 84 | } |
83 | 85 | ||
84 | // Type builders | 86 | // Type builders |
85 | def public Element(CharSequence elementName) { return createDefinedElement => [x|x.name = elementName.canonize] } | 87 | def Element(CharSequence elementName) { return createDefinedElement => [x|x.name = elementName.canonize] } |
86 | def public Element() { return createDefinedElement } | 88 | def Element() { return createDefinedElement } |
87 | def public TypeDeclaration(CharSequence name, boolean isAbstract) { TypeDeclaration => [x | x.name = name.canonize x.isAbstract = isAbstract] } | 89 | def TypeDeclaration(CharSequence name, boolean isAbstract) { TypeDeclaration => [x | x.name = name.canonize x.isAbstract = isAbstract] } |
88 | def public TypeDeclaration() { createTypeDeclaration } | 90 | def TypeDeclaration() { createTypeDeclaration } |
89 | def public TypeDefinition(CharSequence name, boolean isAbstract, DefinedElement... elements) { TypeDefinition(name, isAbstract, elements as Iterable<DefinedElement>) } | 91 | def TypeDefinition(CharSequence name, boolean isAbstract, DefinedElement... elements) { TypeDefinition(name, isAbstract, elements as Iterable<DefinedElement>) } |
90 | def public TypeDefinition(CharSequence name, boolean isAbstract, Iterable<DefinedElement> elements) { createTypeDefinition => [x | x.name = name.canonize x.isAbstract = isAbstract x.elements += elements ] } | 92 | def TypeDefinition(CharSequence name, boolean isAbstract, Iterable<DefinedElement> elements) { createTypeDefinition => [x | x.name = name.canonize x.isAbstract = isAbstract x.elements += elements ] } |
91 | 93 | ||
92 | def public Supertype(Type subtype, Type supertype) { | 94 | def Supertype(Type subtype, Type supertype) { |
93 | subtype.supertypes+=supertype | 95 | subtype.supertypes+=supertype |
94 | } | 96 | } |
95 | def public SetSupertype(Type subtype, Type supertype, boolean value) { | 97 | def SetSupertype(Type subtype, Type supertype, boolean value) { |
96 | if(value) subtype.supertypes+=supertype | 98 | if(value) subtype.supertypes+=supertype |
97 | else subtype.subtypes-=supertype | 99 | else subtype.subtypes-=supertype |
98 | } | 100 | } |
99 | 101 | ||
100 | // Type add | 102 | // Type add |
101 | def public add(LogicProblem problem, Type type) { | 103 | def add(LogicProblem problem, Type type) { |
102 | problem.nameIfAnonymType(type) | 104 | problem.nameIfAnonymType(type) |
103 | problem.types+=type | 105 | problem.types+=type |
104 | if(type instanceof TypeDefinition) { | 106 | if(type instanceof TypeDefinition) { |
@@ -118,10 +120,10 @@ public class LogicProblemBuilder{ | |||
118 | element.name = typeDefinition.elements.map[it.name].generateUniqueName[i | '''type «i.toString»'''] | 120 | element.name = typeDefinition.elements.map[it.name].generateUniqueName[i | '''type «i.toString»'''] |
119 | } | 121 | } |
120 | 122 | ||
121 | def public LogicBool() { createBoolTypeReference } | 123 | def LogicBool() { createBoolTypeReference } |
122 | def public LogicInt() { createIntTypeReference } | 124 | def LogicInt() { createIntTypeReference } |
123 | def public LogicReal() { createRealTypeReference } | 125 | def LogicReal() { createRealTypeReference } |
124 | def public LogicString() { createStringTypeReference } | 126 | def LogicString() { createStringTypeReference } |
125 | def toTypeReference(TypeDescriptor descriptor) { | 127 | def toTypeReference(TypeDescriptor descriptor) { |
126 | if(descriptor instanceof TypeReference) { return EcoreUtil.copy(descriptor); } | 128 | if(descriptor instanceof TypeReference) { return EcoreUtil.copy(descriptor); } |
127 | else if(descriptor instanceof Type) { return createComplexTypeReference => [referred = descriptor]} | 129 | else if(descriptor instanceof Type) { return createComplexTypeReference => [referred = descriptor]} |
@@ -129,31 +131,31 @@ public class LogicProblemBuilder{ | |||
129 | } | 131 | } |
130 | 132 | ||
131 | // Variables | 133 | // Variables |
132 | def public createVar(CharSequence name, TypeDescriptor range) { | 134 | def createVar(CharSequence name, TypeDescriptor range) { |
133 | return createVariable => [it.name = name.canonize it.range = range.toTypeReference] | 135 | return createVariable => [it.name = name.canonize it.range = range.toTypeReference] |
134 | } | 136 | } |
135 | 137 | ||
136 | // Functions | 138 | // Functions |
137 | def public FunctionDescription ->(TypeDescriptor parameter, TypeDescriptor range) { return #[parameter] -> range } | 139 | def FunctionDescription ->(TypeDescriptor parameter, TypeDescriptor range) { return #[parameter] -> range } |
138 | def public FunctionDescription ->(Iterable<? extends TypeDescriptor> parameters, TypeDescriptor range) { return new FunctionDescription(parameters.map[toTypeReference], range.toTypeReference); } | 140 | def FunctionDescription ->(Iterable<? extends TypeDescriptor> parameters, TypeDescriptor range) { return new FunctionDescription(parameters.map[toTypeReference], range.toTypeReference); } |
139 | def public FunctionDeclaration(CharSequence name, FunctionDescription functionDescription) { FunctionDeclaration(name,functionDescription.range, functionDescription.parameters) } | 141 | def FunctionDeclaration(CharSequence name, FunctionDescription functionDescription) { FunctionDeclaration(name,functionDescription.range, functionDescription.parameters) } |
140 | def public FunctionDeclaration(FunctionDescription functionDescription) { FunctionDeclaration(functionDescription.range, functionDescription.parameters) } | 142 | def FunctionDeclaration(FunctionDescription functionDescription) { FunctionDeclaration(functionDescription.range, functionDescription.parameters) } |
141 | def public FunctionDeclaration(CharSequence name, TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(name, range, parameters as Iterable<? extends TypeReference>) } | 143 | def FunctionDeclaration(CharSequence name, TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(name, range, parameters as Iterable<? extends TypeReference>) } |
142 | def public FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable<? extends TypeReference>) } | 144 | def FunctionDeclaration(TypeDescriptor range, TypeDescriptor... parameters) { FunctionDeclaration(range, parameters as Iterable<? extends TypeReference>) } |
143 | def public FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] } | 145 | def FunctionDeclaration(CharSequence name, TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) { return FunctionDeclaration(range,parameters) => [x|x.name = name.canonize] } |
144 | def public FunctionDeclaration(TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) { | 146 | def FunctionDeclaration(TypeDescriptor range, Iterable<? extends TypeDescriptor> parameters) { |
145 | val function = createFunctionDeclaration | 147 | val function = createFunctionDeclaration |
146 | for(parameter : parameters) function.parameters+=parameter.toTypeReference | 148 | for(parameter : parameters) function.parameters+=parameter.toTypeReference |
147 | function.range = range.toTypeReference | 149 | function.range = range.toTypeReference |
148 | return function | 150 | return function |
149 | } | 151 | } |
150 | 152 | ||
151 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Function1<VariableContext, ? extends TermDescription> expression) { | 153 | def FunctionDefinition(CharSequence name, TypeDescriptor range, Function1<VariableContext, ? extends TermDescription> expression) { |
152 | val context = new VariableContext(this,logicFactiory) | 154 | val context = new VariableContext(this,logicFactiory) |
153 | val definition = expression.apply(context) | 155 | val definition = expression.apply(context) |
154 | return FunctionDefinition(name,range,context.variables,definition); | 156 | return FunctionDefinition(name,range,context.variables,definition); |
155 | } | 157 | } |
156 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<Variable> variables, TermDescription definition) { | 158 | def FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<Variable> variables, TermDescription definition) { |
157 | return createFunctionDefinition => [ | 159 | return createFunctionDefinition => [ |
158 | it.name = name.canonize | 160 | it.name = name.canonize |
159 | it.parameters += variables.map[it.range.toTypeReference] | 161 | it.parameters += variables.map[it.range.toTypeReference] |
@@ -162,23 +164,23 @@ public class LogicProblemBuilder{ | |||
162 | it.value = definition.toTerm | 164 | it.value = definition.toTerm |
163 | ] | 165 | ] |
164 | } | 166 | } |
165 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue) { | 167 | def FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue) { |
166 | return FunctionDefinition(name,range,parameters,parametersToValue,null) | 168 | return FunctionDefinition(name,range,parameters,parametersToValue,null) |
167 | } | 169 | } |
168 | def public FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue, Term defaultValue) { | 170 | def FunctionDefinition(CharSequence name, TypeDescriptor range, Iterable<TypeDescriptor> parameters, Map<List<Term>,Term> parametersToValue, Term defaultValue) { |
169 | val parameterList = parameters.toList; | 171 | val parameterList = parameters.toList; |
170 | val variableList = (1..parameterList.size).map[index | '''param «index»'''.createVar(parameterList.get(index-1))].toList | 172 | val variableList = (1..parameterList.size).map[index | '''param «index»'''.createVar(parameterList.get(index-1))].toList |
171 | return FunctionDefinition(name,range,variableList,advancedConstructs.FunctionDefinitionBody(variableList,parametersToValue,defaultValue)) | 173 | return FunctionDefinition(name,range,variableList,advancedConstructs.FunctionDefinitionBody(variableList,parametersToValue,defaultValue)) |
172 | } | 174 | } |
173 | 175 | ||
174 | // Add function to a problem | 176 | // Add function to a problem |
175 | def public add(LogicProblem input, Function function) { | 177 | def add(LogicProblem input, Function function) { |
176 | input.nameIfAnonymFunction(function) | 178 | input.nameIfAnonymFunction(function) |
177 | input.checkFunction(function) | 179 | input.checkFunction(function) |
178 | input.functions += function | 180 | input.functions += function |
179 | return function | 181 | return function |
180 | } | 182 | } |
181 | def public add(LogicProblem input, FunctionDescription functionDescription) { input.add(FunctionDeclaration(functionDescription)) } | 183 | def add(LogicProblem input, FunctionDescription functionDescription) { input.add(FunctionDeclaration(functionDescription)) } |
182 | def protected nameIfAnonymFunction(LogicProblem problem, Function functionDeclaration) { | 184 | def protected nameIfAnonymFunction(LogicProblem problem, Function functionDeclaration) { |
183 | if(functionDeclaration.name.nullOrEmpty) { | 185 | if(functionDeclaration.name.nullOrEmpty) { |
184 | functionDeclaration.name = problem.functions.map[it.name].generateUniqueName[i | "function"+i] | 186 | functionDeclaration.name = problem.functions.map[it.name].generateUniqueName[i | "function"+i] |
@@ -199,15 +201,15 @@ public class LogicProblemBuilder{ | |||
199 | } | 201 | } |
200 | 202 | ||
201 | // Constants | 203 | // Constants |
202 | def public ConstantDeclaration(CharSequence name, TypeDescriptor type) { ConstantDeclaration(type) => [it.name = name.canonize] } | 204 | def ConstantDeclaration(CharSequence name, TypeDescriptor type) { ConstantDeclaration(type) => [it.name = name.canonize] } |
203 | def public ConstantDeclaration(TypeDescriptor type) { createConstantDeclaration => [it.type = type.toTypeReference] } | 205 | def ConstantDeclaration(TypeDescriptor type) { createConstantDeclaration => [it.type = type.toTypeReference] } |
204 | 206 | ||
205 | def public ConstantDefinition(CharSequence name, TypeDescriptor type, TermDescription value) { | 207 | def ConstantDefinition(CharSequence name, TypeDescriptor type, TermDescription value) { |
206 | createConstantDefinition => [it.name = name.canonize it.type = type.toTypeReference it.value = value.toTerm] | 208 | createConstantDefinition => [it.name = name.canonize it.type = type.toTypeReference it.value = value.toTerm] |
207 | } | 209 | } |
208 | 210 | ||
209 | // Add constant to a problem | 211 | // Add constant to a problem |
210 | def public add(LogicProblem problem, Constant constant) { | 212 | def add(LogicProblem problem, Constant constant) { |
211 | problem.nameIfAnonymConstant(constant); | 213 | problem.nameIfAnonymConstant(constant); |
212 | problem.checkConstant(constant) | 214 | problem.checkConstant(constant) |
213 | problem.constants += constant | 215 | problem.constants += constant |
@@ -226,10 +228,10 @@ public class LogicProblemBuilder{ | |||
226 | } | 228 | } |
227 | 229 | ||
228 | // Relations | 230 | // Relations |
229 | def public RelationDeclaration(CharSequence name, TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable<? extends TypeReference>) } | 231 | def RelationDeclaration(CharSequence name, TypeDescriptor... parameters) { return RelationDeclaration(name, parameters as Iterable<? extends TypeReference>) } |
230 | def public RelationDeclaration(CharSequence name, Iterable<? extends TypeDescriptor> parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] } | 232 | def RelationDeclaration(CharSequence name, Iterable<? extends TypeDescriptor> parameters) { return RelationDeclaration(parameters) => [x|x.name = name.canonize] } |
231 | def public RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable<? extends TypeReference>) } | 233 | def RelationDeclaration(TypeDescriptor... parameters) { RelationDeclaration( parameters as Iterable<? extends TypeReference>) } |
232 | def public RelationDeclaration(Iterable<? extends TypeDescriptor> parameters) { | 234 | def RelationDeclaration(Iterable<? extends TypeDescriptor> parameters) { |
233 | val relation = createRelationDeclaration | 235 | val relation = createRelationDeclaration |
234 | for(parameter : parameters) { | 236 | for(parameter : parameters) { |
235 | relation.parameters+=parameter.toTypeReference | 237 | relation.parameters+=parameter.toTypeReference |
@@ -237,12 +239,12 @@ public class LogicProblemBuilder{ | |||
237 | return relation | 239 | return relation |
238 | } | 240 | } |
239 | 241 | ||
240 | def public RelationDefinition(CharSequence name, Function1<VariableContext, ? extends TermDescription> expression) { | 242 | def RelationDefinition(CharSequence name, Function1<VariableContext, ? extends TermDescription> expression) { |
241 | val context = new VariableContext(this,logicFactiory); | 243 | val context = new VariableContext(this,logicFactiory); |
242 | val definition = expression.apply(context); | 244 | val definition = expression.apply(context); |
243 | return RelationDefinition(name,context.variables,definition) | 245 | return RelationDefinition(name,context.variables,definition) |
244 | } | 246 | } |
245 | def public RelationDefinition(CharSequence name, Iterable<Variable> variables, TermDescription definition) { | 247 | def RelationDefinition(CharSequence name, Iterable<Variable> variables, TermDescription definition) { |
246 | return createRelationDefinition => [ | 248 | return createRelationDefinition => [ |
247 | it.name = name.canonize | 249 | it.name = name.canonize |
248 | it.parameters += variables.map[it.range.toTypeReference] | 250 | it.parameters += variables.map[it.range.toTypeReference] |
@@ -250,7 +252,7 @@ public class LogicProblemBuilder{ | |||
250 | it.value = definition?.toTerm | 252 | it.value = definition?.toTerm |
251 | ] | 253 | ] |
252 | } | 254 | } |
253 | def public RelationDefinition(CharSequence name, Iterable<? extends TypeDescriptor> parameters, Iterable<? extends List<? extends TermDescription>> possibleValues) { | 255 | def RelationDefinition(CharSequence name, Iterable<? extends TypeDescriptor> parameters, Iterable<? extends List<? extends TermDescription>> possibleValues) { |
254 | val res = createRelationDefinition => [it.name = name.canonize] | 256 | val res = createRelationDefinition => [it.name = name.canonize] |
255 | val variableMap = new ArrayList(parameters.size) | 257 | val variableMap = new ArrayList(parameters.size) |
256 | var index = 0 | 258 | var index = 0 |
@@ -267,7 +269,7 @@ public class LogicProblemBuilder{ | |||
267 | } | 269 | } |
268 | 270 | ||
269 | // Add Relation to a problem | 271 | // Add Relation to a problem |
270 | def public add(LogicProblem input, Relation relation) { | 272 | def add(LogicProblem input, Relation relation) { |
271 | input.nameIfAnonymRelation(relation) | 273 | input.nameIfAnonymRelation(relation) |
272 | input.checkRelation(relation) | 274 | input.checkRelation(relation) |
273 | input.relations+=relation | 275 | input.relations+=relation |
@@ -293,17 +295,17 @@ public class LogicProblemBuilder{ | |||
293 | } | 295 | } |
294 | 296 | ||
295 | // Assertion | 297 | // Assertion |
296 | def public Assertion(TermDescription term) { | 298 | def Assertion(TermDescription term) { |
297 | val result = term.toTerm | 299 | val result = term.toTerm |
298 | result.nameAnonymVariables(Collections.EMPTY_LIST) | 300 | result.nameAnonymVariables(Collections.EMPTY_LIST) |
299 | createAssertion => [it.value = result] | 301 | createAssertion => [it.value = result] |
300 | } | 302 | } |
301 | def public Assertion(CharSequence name, TermDescription term) { | 303 | def Assertion(CharSequence name, TermDescription term) { |
302 | val result = term.toTerm | 304 | val result = term.toTerm |
303 | result.nameAnonymVariables(Collections.EMPTY_LIST) | 305 | result.nameAnonymVariables(Collections.EMPTY_LIST) |
304 | createAssertion => [it.value = result it.name=name.canonize] | 306 | createAssertion => [it.value = result it.name=name.canonize] |
305 | } | 307 | } |
306 | def public add(LogicProblem problem, Assertion assertion) { | 308 | def add(LogicProblem problem, Assertion assertion) { |
307 | if(assertion.name.nullOrEmpty) { | 309 | if(assertion.name.nullOrEmpty) { |
308 | val name = problem.assertions.map[name].generateUniqueName["assertion"+it] | 310 | val name = problem.assertions.map[name].generateUniqueName["assertion"+it] |
309 | assertion.name=name | 311 | assertion.name=name |
@@ -313,7 +315,7 @@ public class LogicProblemBuilder{ | |||
313 | return assertion | 315 | return assertion |
314 | } | 316 | } |
315 | 317 | ||
316 | def public add(LogicProblem problem, TermDescription term) { | 318 | def add(LogicProblem problem, TermDescription term) { |
317 | problem.add(Assertion(term)) | 319 | problem.add(Assertion(term)) |
318 | } | 320 | } |
319 | 321 | ||
@@ -329,7 +331,7 @@ public class LogicProblemBuilder{ | |||
329 | } | 331 | } |
330 | } | 332 | } |
331 | 333 | ||
332 | def public checkDefinition(EObject definition) { | 334 | def checkDefinition(EObject definition) { |
333 | /*for(value : definition.eAllContents.filter(SymbolicValue).toIterable) { | 335 | /*for(value : definition.eAllContents.filter(SymbolicValue).toIterable) { |
334 | var referred = value.symbolicReference | 336 | var referred = value.symbolicReference |
335 | if(referred instanceof Variable) { | 337 | if(referred instanceof Variable) { |
@@ -341,7 +343,7 @@ public class LogicProblemBuilder{ | |||
341 | } | 343 | } |
342 | 344 | ||
343 | // Containment | 345 | // Containment |
344 | def public ContainmentHierarchy( | 346 | def ContainmentHierarchy( |
345 | Iterable<? extends Type> typesInHierarchy, | 347 | Iterable<? extends Type> typesInHierarchy, |
346 | Iterable<? extends Function> containmentFunctions, | 348 | Iterable<? extends Function> containmentFunctions, |
347 | Iterable<? extends Relation> containmentRelations, | 349 | Iterable<? extends Relation> containmentRelations, |
@@ -355,7 +357,7 @@ public class LogicProblemBuilder{ | |||
355 | ] | 357 | ] |
356 | return result | 358 | return result |
357 | } | 359 | } |
358 | def public add(LogicProblem problem, ContainmentHierarchy hierarchy) { | 360 | def add(LogicProblem problem, ContainmentHierarchy hierarchy) { |
359 | problem.containmentHierarchies+=hierarchy | 361 | problem.containmentHierarchies+=hierarchy |
360 | return hierarchy | 362 | return hierarchy |
361 | } | 363 | } |
@@ -413,7 +415,7 @@ public class LogicProblemBuilder{ | |||
413 | return result; | 415 | return result; |
414 | } | 416 | } |
415 | 417 | ||
416 | def public Term toTerm(TermDescription term) { | 418 | def Term toTerm(TermDescription term) { |
417 | if(term instanceof Term) return term | 419 | if(term instanceof Term) return term |
418 | else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] | 420 | else if (term instanceof Variable) return createSymbolicValue => [symbolicReference = term] |
419 | else if (term instanceof Constant) return term.call() | 421 | else if (term instanceof Constant) return term.call() |
@@ -421,74 +423,74 @@ public class LogicProblemBuilder{ | |||
421 | else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) | 423 | else throw new UnsupportedOperationException("Can not create reference for symbolic declaration " + term.class.name) |
422 | } | 424 | } |
423 | 425 | ||
424 | def public !(TermDescription term) { Not(term) } | 426 | def !(TermDescription term) { Not(term) } |
425 | def public Not(TermDescription term) { createNot => [operand = term.toTerm] } | 427 | def Not(TermDescription term) { createNot => [operand = term.toTerm] } |
426 | 428 | ||
427 | def public &&(TermDescription a, TermDescription b) { And(a,b) } | 429 | def &&(TermDescription a, TermDescription b) { And(a,b) } |
428 | def public And(TermDescription... terms) { return And(terms as Iterable<? extends TermDescription>) } | 430 | def And(TermDescription... terms) { return And(terms as Iterable<? extends TermDescription>) } |
429 | def public And(Iterable<? extends TermDescription> terms) { createAnd => [operands += terms.map[toTerm]] } | 431 | def And(Iterable<? extends TermDescription> terms) { createAnd => [operands += terms.map[toTerm]] } |
430 | 432 | ||
431 | def public ||(TermDescription a, TermDescription b) { Or(a,b) } | 433 | def ||(TermDescription a, TermDescription b) { Or(a,b) } |
432 | def public Or(TermDescription... terms) { Or(terms as Iterable<? extends TermDescription>) } | 434 | def Or(TermDescription... terms) { Or(terms as Iterable<? extends TermDescription>) } |
433 | def public Or(Iterable<? extends TermDescription> terms) { createOr => [operands += terms.map[toTerm]] } | 435 | def Or(Iterable<? extends TermDescription> terms) { createOr => [operands += terms.map[toTerm]] } |
434 | 436 | ||
435 | def public =>(TermDescription a, TermDescription b) { Impl(a,b) } | 437 | def =>(TermDescription a, TermDescription b) { Impl(a,b) } |
436 | def public Impl(TermDescription a, TermDescription b) { createImpl => [leftOperand = a.toTerm rightOperand = b.toTerm] } | 438 | def Impl(TermDescription a, TermDescription b) { createImpl => [leftOperand = a.toTerm rightOperand = b.toTerm] } |
437 | 439 | ||
438 | def public <=>(TermDescription a, TermDescription b) { Iff(a,b)} | 440 | def <=>(TermDescription a, TermDescription b) { Iff(a,b)} |
439 | def public Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] } | 441 | def Iff(TermDescription a, TermDescription b) { createIff =>[leftOperand=a.toTerm rightOperand=b.toTerm] } |
440 | 442 | ||
441 | def public ITE(TermDescription condition, TermDescription ifTrue, TermDescription ifFalse) { | 443 | def ITE(TermDescription condition, TermDescription ifTrue, TermDescription ifFalse) { |
442 | createIfThenElse => [it.condition = condition.toTerm it.ifTrue = ifTrue.toTerm it.ifFalse = ifFalse.toTerm] | 444 | createIfThenElse => [it.condition = condition.toTerm it.ifTrue = ifTrue.toTerm it.ifFalse = ifFalse.toTerm] |
443 | } | 445 | } |
444 | 446 | ||
445 | def public >(TermDescription left, TermDescription right) { MoreThan(left,right)} | 447 | def >(TermDescription left, TermDescription right) { MoreThan(left,right)} |
446 | def public MoreThan(TermDescription left, TermDescription right) { createMoreThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 448 | def MoreThan(TermDescription left, TermDescription right) { createMoreThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
447 | 449 | ||
448 | def public <(TermDescription left, TermDescription right) { LessThan(left,right)} | 450 | def <(TermDescription left, TermDescription right) { LessThan(left,right)} |
449 | def public LessThan(TermDescription left, TermDescription right) { createLessThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 451 | def LessThan(TermDescription left, TermDescription right) { createLessThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
450 | 452 | ||
451 | def public <=(TermDescription left, TermDescription right) { LessOrEqual(left,right) } | 453 | def <=(TermDescription left, TermDescription right) { LessOrEqual(left,right) } |
452 | def public LessOrEqual(TermDescription left, TermDescription right) { createLessOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 454 | def LessOrEqual(TermDescription left, TermDescription right) { createLessOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
453 | 455 | ||
454 | def public >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) } | 456 | def >=(TermDescription left, TermDescription right) { MoreOrEqual(left,right) } |
455 | def public MoreOrEqual(TermDescription left, TermDescription right) { createMoreOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 457 | def MoreOrEqual(TermDescription left, TermDescription right) { createMoreOrEqualThan => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
456 | 458 | ||
457 | def public ==(TermDescription left, TermDescription right) {Equals(left,right)} | 459 | def ==(TermDescription left, TermDescription right) {Equals(left,right)} |
458 | def public Equals(TermDescription left, TermDescription right) { createEquals => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 460 | def Equals(TermDescription left, TermDescription right) { createEquals => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
459 | 461 | ||
460 | def public !=(TermDescription left, TermDescription right) { Distinct(left,right) } | 462 | def !=(TermDescription left, TermDescription right) { Distinct(left,right) } |
461 | def public Distinct(TermDescription... terms) { return Distinct(terms as Iterable<? extends TermDescription>) } | 463 | def Distinct(TermDescription... terms) { return Distinct(terms as Iterable<? extends TermDescription>) } |
462 | def public Distinct(Iterable<? extends TermDescription> terms) { createDistinct => [operands += terms.map[toTerm]] } | 464 | def Distinct(Iterable<? extends TermDescription> terms) { createDistinct => [operands += terms.map[toTerm]] } |
463 | 465 | ||
464 | def public +(TermDescription left, TermDescription right) { Plus(left,right) } | 466 | def +(TermDescription left, TermDescription right) { Plus(left,right) } |
465 | def public Plus(TermDescription left, TermDescription right) { createPlus => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 467 | def Plus(TermDescription left, TermDescription right) { createPlus => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
466 | 468 | ||
467 | def public -(TermDescription left, TermDescription right) { Minus(left,right) } | 469 | def -(TermDescription left, TermDescription right) { Minus(left,right) } |
468 | def public Minus(TermDescription left, TermDescription right) { createMinus => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 470 | def Minus(TermDescription left, TermDescription right) { createMinus => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
469 | 471 | ||
470 | def public *(TermDescription left, TermDescription right) { Multiply(left,right) } | 472 | def *(TermDescription left, TermDescription right) { Multiply(left,right) } |
471 | def public Multiply(TermDescription left, TermDescription right) { createMultiply => [leftOperand=left.toTerm rightOperand=right.toTerm] } | 473 | def Multiply(TermDescription left, TermDescription right) { createMultiply => [leftOperand=left.toTerm rightOperand=right.toTerm] } |
472 | 474 | ||
473 | def public /(TermDescription left, TermDescription right) { Divide(left,right) } | 475 | def /(TermDescription left, TermDescription right) { Divide(left,right) } |
474 | def public Divide(TermDescription left, TermDescription right) { createDivison => [leftOperand = left.toTerm rightOperand = right.toTerm]} | 476 | def Divide(TermDescription left, TermDescription right) { createDivison => [leftOperand = left.toTerm rightOperand = right.toTerm]} |
475 | 477 | ||
476 | def public %(TermDescription left, TermDescription right) { Modulo(left,right) } | 478 | def %(TermDescription left, TermDescription right) { Modulo(left,right) } |
477 | def public Modulo(TermDescription left, TermDescription right) { createMod => [leftOperand = left.toTerm rightOperand = right.toTerm]} | 479 | def Modulo(TermDescription left, TermDescription right) { createMod => [leftOperand = left.toTerm rightOperand = right.toTerm]} |
478 | 480 | ||
479 | def public asTerm(boolean value) { createBoolLiteral => [x|x.value = value] } | 481 | def asTerm(boolean value) { createBoolLiteral => [x|x.value = value] } |
480 | def public asTerm(int value) { createIntLiteral => [x|x.value = value] } | 482 | def asTerm(int value) { createIntLiteral => [x|x.value = value] } |
481 | def public asTerm(double value) { BigDecimal.valueOf(value).asTerm } | 483 | def asTerm(double value) { BigDecimal.valueOf(value).asTerm } |
482 | def public asTerm(float value) { BigDecimal.valueOf(value).asTerm } | 484 | def asTerm(float value) { BigDecimal.valueOf(value).asTerm } |
483 | def public asTerm(BigDecimal value) { createRealLiteral => [x|x.value = value] } | 485 | def asTerm(BigDecimal value) { createRealLiteral => [x|x.value = value] } |
484 | def public asTerm(String value) { createStringLiteral => [x|x.value = value]} | 486 | def asTerm(String value) { createStringLiteral => [x|x.value = value]} |
485 | def public InstanceOf(TermDescription term, TypeDescriptor type) { | 487 | def InstanceOf(TermDescription term, TypeDescriptor type) { |
486 | createInstanceOf => [ | 488 | createInstanceOf => [ |
487 | it.value = term.toTerm | 489 | it.value = term.toTerm |
488 | it.range = type.toTypeReference | 490 | it.range = type.toTypeReference |
489 | ] | 491 | ] |
490 | } | 492 | } |
491 | def public transitiveClosure(Relation relation, TermDescription source, TermDescription target) { | 493 | def transitiveClosure(Relation relation, TermDescription source, TermDescription target) { |
492 | createTransitiveClosure => [ | 494 | createTransitiveClosure => [ |
493 | it.relation = relation | 495 | it.relation = relation |
494 | it.leftOperand = leftOperand | 496 | it.leftOperand = leftOperand |
@@ -498,38 +500,79 @@ public class LogicProblemBuilder{ | |||
498 | 500 | ||
499 | // QuantifiedExpressions | 501 | // QuantifiedExpressions |
500 | 502 | ||
501 | def public Forall(Function1<VariableContext, ? extends TermDescription> expression) { | 503 | def Forall(Function1<VariableContext, ? extends TermDescription> expression) { |
502 | val context = new VariableContext(this,logicFactiory) | 504 | val context = new VariableContext(this,logicFactiory) |
503 | val term = expression.apply(context) | 505 | val term = expression.apply(context) |
504 | return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] | 506 | return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] |
505 | } | 507 | } |
506 | def public Forall(TermDescription expression, Variable... variables) { | 508 | def Forall(TermDescription expression, Variable... variables) { |
507 | Forall(variables,expression) } | 509 | Forall(variables,expression) } |
508 | def public Forall(Iterable<? extends Variable> variables,TermDescription expression) { | 510 | def Forall(Iterable<? extends Variable> variables,TermDescription expression) { |
509 | val forallExpression = createForall | 511 | val forallExpression = createForall |
510 | for(variable : variables) forallExpression.quantifiedVariables += variable | 512 | for(variable : variables) forallExpression.quantifiedVariables += variable |
511 | forallExpression.expression = expression.toTerm | 513 | forallExpression.expression = expression.toTerm |
512 | return forallExpression | 514 | return forallExpression |
513 | } | 515 | } |
514 | 516 | ||
515 | def public Exists(Function1<VariableContext, ? extends TermDescription> expression) { | 517 | def Exists(Function1<VariableContext, ? extends TermDescription> expression) { |
516 | val context = new VariableContext(this,logicFactiory) | 518 | val context = new VariableContext(this,logicFactiory) |
517 | val term = expression.apply(context) | 519 | val term = expression.apply(context) |
518 | return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] | 520 | return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] |
519 | } | 521 | } |
520 | def public Exists(TermDescription expression, Variable... variables) { | 522 | def Exists(TermDescription expression, Variable... variables) { |
521 | Exists(variables,expression) } | 523 | Exists(variables,expression) } |
522 | def public Exists(Iterable<? extends Variable> variables, TermDescription expression) { | 524 | def Exists(Iterable<? extends Variable> variables, TermDescription expression) { |
523 | val existsExpression = createExists | 525 | val existsExpression = createExists |
524 | for(variable : variables) existsExpression.quantifiedVariables += variable | 526 | for(variable : variables) existsExpression.quantifiedVariables += variable |
525 | existsExpression.expression = expression.toTerm | 527 | existsExpression.expression = expression.toTerm |
526 | return existsExpression | 528 | return existsExpression |
527 | } | 529 | } |
528 | 530 | ||
531 | // AggregatedExpression | ||
532 | |||
533 | private def <T extends AggregateExpression> configureAggregateExpression(T expression, Relation referred, List<Variable> terms) { | ||
534 | if(terms.size != referred.parameters.size) { | ||
535 | throw new LogicProblemBuilderException( | ||
536 | '''The function called has «referred.parameters.size» parameters but it is called with «terms.size»!''') | ||
537 | } else { | ||
538 | expression.relation = referred | ||
539 | for(var i=0; i<referred.parameters.size;i++) { | ||
540 | val target = terms.get(i) | ||
541 | val substitution = createAggregatedParameterSubstitution => [it.variable = target] | ||
542 | expression.parameterSubstitution += substitution | ||
543 | } | ||
544 | return expression | ||
545 | } | ||
546 | } | ||
547 | private def <T extends ProjectedAggregateExpression> configureProjectedAggregateExpression(T expression, Relation referred, List<Variable> terms, int projection) { | ||
548 | if(projection < 0 || projection >= referred.parameters.size) { | ||
549 | throw new LogicProblemBuilderException( | ||
550 | '''The function called has «referred.parameters.size» parameters but it is called with «terms.size»!''') | ||
551 | } else { | ||
552 | val res = expression.configureAggregateExpression(referred, terms) | ||
553 | if(res.parameterSubstitution.get(projection) !== null) { | ||
554 | throw new LogicProblemBuilderException( | ||
555 | '''Projection over set variable!''') | ||
556 | } | ||
557 | val projectionType = referred.parameters.get(projection) | ||
558 | if(!(projectionType instanceof IntTypeReference || projectionType instanceof RealTypeReference)) { | ||
559 | throw new LogicProblemBuilderException('''Projection over nunnumeric parameter!''' | ||
560 | ) | ||
561 | } | ||
562 | res.projectionIndex = projection | ||
563 | return res | ||
564 | } | ||
565 | |||
566 | } | ||
567 | def Count(Relation referred, List<Variable> terms) { createCount.configureAggregateExpression(referred,terms) } | ||
568 | def Sum(Relation referred, List<Variable> terms, int projection) { createSum.configureProjectedAggregateExpression(referred,terms,projection) } | ||
569 | def Min(Relation referred, List<Variable> terms, int projection) { createMin.configureProjectedAggregateExpression(referred,terms,projection) } | ||
570 | def Max(Relation referred, List<Variable> terms, int projection) { createMax.configureProjectedAggregateExpression(referred,terms,projection) } | ||
571 | |||
529 | // Function calls | 572 | // Function calls |
530 | def public call(Function function, TermDescription... substitutions) { | 573 | def call(Function function, TermDescription... substitutions) { |
531 | call(function, substitutions as Iterable<? extends TermDescription>) } | 574 | call(function, substitutions as Iterable<? extends TermDescription>) } |
532 | def public call(Function function, Iterable<? extends TermDescription> substitutions) { | 575 | def call(Function function, Iterable<? extends TermDescription> substitutions) { |
533 | val functionReference = createSymbolicValue | 576 | val functionReference = createSymbolicValue |
534 | functionReference.symbolicReference=function | 577 | functionReference.symbolicReference=function |
535 | val List<TermDescription> l= new LinkedList() | 578 | val List<TermDescription> l= new LinkedList() |
@@ -546,8 +589,8 @@ public class LogicProblemBuilder{ | |||
546 | } | 589 | } |
547 | 590 | ||
548 | // Relation calls | 591 | // Relation calls |
549 | def public call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable<? extends TermDescription>)} | 592 | def call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable<? extends TermDescription>)} |
550 | def public call(Relation relation, Iterable<? extends TermDescription> substitution) { | 593 | def call(Relation relation, Iterable<? extends TermDescription> substitution) { |
551 | val relationReference = createSymbolicValue | 594 | val relationReference = createSymbolicValue |
552 | relationReference.symbolicReference = relation | 595 | relationReference.symbolicReference = relation |
553 | //println('''«relation.name»(«substitution.size»->«relation.parameters»)''') | 596 | //println('''«relation.name»(«substitution.size»->«relation.parameters»)''') |
@@ -567,11 +610,9 @@ public class LogicProblemBuilder{ | |||
567 | } | 610 | } |
568 | 611 | ||
569 | // constant evaluation | 612 | // constant evaluation |
570 | def public call(Constant constant) { | 613 | def call(Constant constant) { |
571 | val constantReference = createSymbolicValue | 614 | val constantReference = createSymbolicValue |
572 | constantReference.symbolicReference = constant | 615 | constantReference.symbolicReference = constant |
573 | return constantReference | 616 | return constantReference |
574 | } | 617 | } |
575 | |||
576 | |||
577 | } | 618 | } |