aboutsummaryrefslogtreecommitdiffstats
path: root/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-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/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicProblemBuilder.xtend563
1 files changed, 563 insertions, 0 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
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 @@
1package hu.bme.mit.inf.dslreasoner.logic.model.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
23import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
24import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
25import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemFactory
26import hu.bme.mit.inf.dslreasoner.util.LogicProblemBuilder_AdvancedConstructs
27import java.math.BigDecimal
28import java.util.ArrayList
29import java.util.Collections
30import java.util.LinkedList
31import java.util.List
32import java.util.Map
33import org.eclipse.emf.ecore.EObject
34import org.eclipse.emf.ecore.util.EcoreUtil
35import org.eclipse.xtend.lib.annotations.Data
36import org.eclipse.xtext.xbase.lib.Functions.Function1
37
38@Data class FunctionDescription {
39 Iterable<TypeReference> parameters
40 TypeReference range
41}
42
43class LogicProblemBuilderException extends Exception {
44 new(String reason) {
45 super(reason)
46 }
47}
48
49public 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-01 00:56:12 +0000