diff options
author | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:33:58 -0500 |
---|---|---|
committer | 20001LastOrder <boqi.chen@mail.mcgill.ca> | 2020-11-04 01:33:58 -0500 |
commit | a20af4d0dbf5eab84ee271d426528aabb5a8ac3b (patch) | |
tree | a9ab772ee313125aaf3a941d66e131b408d949ba /Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic | |
parent | changes in settings of measurements (diff) | |
parent | merge with current master, comment numerical solver related logging (diff) | |
download | VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.gz VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.zst VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.zip |
fix merging issue
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic')
5 files changed, 232 insertions, 141 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 index 905859eb..cdcbb48a 100644 --- 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 | |||
@@ -3,22 +3,27 @@ package hu.bme.mit.inf.dslreasoner.logic.model.builder | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
12 | import java.math.BigDecimal | ||
10 | import java.util.List | 13 | import java.util.List |
14 | import java.util.Map | ||
15 | import java.util.SortedSet | ||
16 | import java.util.TreeSet | ||
11 | 17 | ||
12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
13 | import java.util.SortedSet | ||
14 | import java.math.BigDecimal | ||
15 | 19 | ||
16 | interface LogicModelInterpretation{ | 20 | interface LogicModelInterpretation { |
17 | 21 | ||
18 | /** | 22 | /** |
19 | * Returns the elements of a type. | 23 | * Returns the elements of a type. |
20 | */ | 24 | */ |
21 | def List<DefinedElement> getElements(Type type) | 25 | def List<DefinedElement> getElements(Type type) |
26 | |||
22 | /** | 27 | /** |
23 | * Returns the interpretation of a function. The parameters and the return values are encoded to primitive java objects defined by the following table: | 28 | * Returns the interpretation of a function. The parameters and the return values are encoded to primitive java objects defined by the following table: |
24 | * <p><table> | 29 | * <p><table> |
@@ -34,6 +39,7 @@ interface LogicModelInterpretation{ | |||
34 | * @return The result of the function call encoded as defined in the table. | 39 | * @return The result of the function call encoded as defined in the table. |
35 | */ | 40 | */ |
36 | def Object getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) | 41 | def Object getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) |
42 | |||
37 | /** | 43 | /** |
38 | * Returns the interpretation of a relation. The parameters are encoded to primitive java objects defined by the following table: | 44 | * Returns the interpretation of a relation. The parameters are encoded to primitive java objects defined by the following table: |
39 | * <p><table> | 45 | * <p><table> |
@@ -49,6 +55,7 @@ interface LogicModelInterpretation{ | |||
49 | * @return If the parameter tuple is in the relation. | 55 | * @return If the parameter tuple is in the relation. |
50 | */ | 56 | */ |
51 | def boolean getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) | 57 | def boolean getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) |
58 | |||
52 | /** | 59 | /** |
53 | * Returns the interpretation of a constant. The value is encoded to primitive java objects defined by the following table: | 60 | * Returns the interpretation of a constant. The value is encoded to primitive java objects defined by the following table: |
54 | * <p><table> | 61 | * <p><table> |
@@ -63,60 +70,89 @@ interface LogicModelInterpretation{ | |||
63 | * @return The value of the constant encoded as specified in the table. | 70 | * @return The value of the constant encoded as specified in the table. |
64 | */ | 71 | */ |
65 | def Object getInterpretation(ConstantDeclaration constant) | 72 | def Object getInterpretation(ConstantDeclaration constant) |
66 | 73 | ||
67 | /** | 74 | /** |
68 | * Returns all integers relevant to the logic structure. Not all integer is necessarily used. | 75 | * Returns all integers relevant to the logic structure. Not all integer is necessarily used. |
69 | */ | 76 | */ |
70 | def SortedSet<Integer> getAllIntegersInStructure() | 77 | def SortedSet<Integer> getAllIntegersInStructure() |
78 | |||
79 | def Map<TermDescription, Integer> getAllIntegersWithInterpretation() { | ||
80 | allIntegersInStructure.toMap [ integer | | ||
81 | (LogiclanguageFactory.eINSTANCE.createIntLiteral => [value = integer]) as TermDescription | ||
82 | ] | ||
83 | } | ||
84 | |||
71 | /** | 85 | /** |
72 | * Returns all real numbers relevant to the logic structure. Not all integer is necessarily used. | 86 | * Returns all real numbers relevant to the logic structure. Not all integer is necessarily used. |
73 | */ | 87 | */ |
74 | def SortedSet<BigDecimal> getAllRealsInStructure() | 88 | def SortedSet<BigDecimal> getAllRealsInStructure() |
75 | /** | 89 | |
90 | def Map<TermDescription, BigDecimal> getAllRealsWithInterpretation() { | ||
91 | allRealsInStructure.toMap [ real | | ||
92 | (LogiclanguageFactory.eINSTANCE.createRealLiteral => [value = real]) as TermDescription | ||
93 | ] | ||
94 | } | ||
95 | |||
96 | /** | ||
76 | * Returns all string values relevant to the logic structure. Not all integer is necessarily used. | 97 | * Returns all string values relevant to the logic structure. Not all integer is necessarily used. |
77 | */ | 98 | */ |
78 | def SortedSet<String> getAllStringsInStructure() | 99 | def SortedSet<String> getAllStringsInStructure() |
100 | |||
101 | def Map<TermDescription, String> getAllStringsWithInterpretation() { | ||
102 | allStringsInStructure.toMap [ string | | ||
103 | (LogiclanguageFactory.eINSTANCE.createStringLiteral => [value = string]) as TermDescription | ||
104 | ] | ||
105 | } | ||
106 | |||
107 | def SortedSet<Boolean> getAllBooleansInStructure() { | ||
108 | new TreeSet(#{true, false}) | ||
109 | } | ||
110 | |||
111 | def Map<TermDescription, Boolean> getAllBooleansWithInterpretation() { | ||
112 | allBooleansInStructure.toMap [ bool | | ||
113 | (LogiclanguageFactory.eINSTANCE.createBoolLiteral => [value = bool]) as TermDescription | ||
114 | ] | ||
115 | } | ||
79 | } | 116 | } |
80 | 117 | ||
81 | class Uninterpreted implements LogicModelInterpretation { | 118 | class Uninterpreted implements LogicModelInterpretation { |
82 | /*private val static unknownBecauseUninterpreted = LogiclanguageFactory.eINSTANCE.createUnknownBecauseUninterpreted | 119 | /*private val static unknownBecauseUninterpreted = LogiclanguageFactory.eINSTANCE.createUnknownBecauseUninterpreted |
83 | public def static getUnknownBecauseUninterpreted() {return Uninterpreted.unknownBecauseUninterpreted}*/ | 120 | public def static getUnknownBecauseUninterpreted() {return Uninterpreted.unknownBecauseUninterpreted}*/ |
84 | |||
85 | override getElements(Type type) { | 121 | override getElements(Type type) { |
86 | throw new UnsupportedOperationException("The interpteration is unknown.") | 122 | throw new UnsupportedOperationException("The interpteration is unknown.") |
87 | } | 123 | } |
88 | 124 | ||
89 | def getKnownElements(Type type) { | 125 | def getKnownElements(Type type) { |
90 | val allSubtypes = type.transitiveClosureStar[it.subtypes] | 126 | val allSubtypes = type.transitiveClosureStar[it.subtypes] |
91 | return allSubtypes.filter(TypeDefinition).map[elements].flatten.toList | 127 | return allSubtypes.filter(TypeDefinition).map[elements].flatten.toList |
92 | } | 128 | } |
93 | 129 | ||
94 | def allElementsAreInterpreted(Type type) { | 130 | def allElementsAreInterpreted(Type type) { |
95 | val allSubtypes = type.transitiveClosureStar[it.subtypes] | 131 | val allSubtypes = type.transitiveClosureStar[it.subtypes] |
96 | return allSubtypes.exists[it instanceof TypeDeclaration] | 132 | return allSubtypes.exists[it instanceof TypeDeclaration] |
97 | } | 133 | } |
98 | 134 | ||
99 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | 135 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { |
100 | throw new UnsupportedOperationException("The interpteration is unknown.") | 136 | throw new UnsupportedOperationException("The interpteration is unknown.") |
101 | } | 137 | } |
102 | 138 | ||
103 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 139 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
104 | throw new UnsupportedOperationException("The interpteration is unknown.") | 140 | throw new UnsupportedOperationException("The interpteration is unknown.") |
105 | } | 141 | } |
106 | 142 | ||
107 | override getInterpretation(ConstantDeclaration constant) { | 143 | override getInterpretation(ConstantDeclaration constant) { |
108 | throw new UnsupportedOperationException("The interpteration is unknown.") | 144 | throw new UnsupportedOperationException("The interpteration is unknown.") |
109 | } | 145 | } |
110 | 146 | ||
111 | override getAllIntegersInStructure() { | 147 | override getAllIntegersInStructure() { |
112 | throw new UnsupportedOperationException("The interpteration is unknown.") | 148 | throw new UnsupportedOperationException("The interpteration is unknown.") |
113 | } | 149 | } |
114 | 150 | ||
115 | override getAllRealsInStructure() { | 151 | override getAllRealsInStructure() { |
116 | throw new UnsupportedOperationException("The interpteration is unknown.") | 152 | throw new UnsupportedOperationException("The interpteration is unknown.") |
117 | } | 153 | } |
118 | 154 | ||
119 | override getAllStringsInStructure() { | 155 | override getAllStringsInStructure() { |
120 | throw new UnsupportedOperationException("The interpteration is unknown.") | 156 | throw new UnsupportedOperationException("The interpteration is unknown.") |
121 | } | 157 | } |
122 | } \ No newline at end of file | 158 | } |
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..fa97cbef 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,115 +423,166 @@ 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 Pow(TermDescription left, TermDescription right) {createPow => [leftOperand = left.toTerm rightOperand = right.toTerm]} |
480 | def public asTerm(int value) { createIntLiteral => [x|x.value = value] } | 482 | def asTerm(boolean value) { createBoolLiteral => [x|x.value = value] } |
481 | def public asTerm(double value) { BigDecimal.valueOf(value).asTerm } | 483 | def asTerm(int value) { createIntLiteral => [x|x.value = value] } |
482 | def public asTerm(float value) { BigDecimal.valueOf(value).asTerm } | 484 | def asTerm(double value) { BigDecimal.valueOf(value).asTerm } |
483 | def public asTerm(BigDecimal value) { createRealLiteral => [x|x.value = value] } | 485 | def asTerm(float value) { BigDecimal.valueOf(value).asTerm } |
484 | def public asTerm(String value) { createStringLiteral => [x|x.value = value]} | 486 | def asTerm(BigDecimal value) { createRealLiteral => [x|x.value = value] } |
485 | def public InstanceOf(TermDescription term, TypeDescriptor type) { | 487 | def asTerm(String value) { createStringLiteral => [x|x.value = value]} |
488 | def InstanceOf(TermDescription term, TypeDescriptor type) { | ||
486 | createInstanceOf => [ | 489 | createInstanceOf => [ |
487 | it.value = term.toTerm | 490 | it.value = term.toTerm |
488 | it.range = type.toTypeReference | 491 | it.range = type.toTypeReference |
489 | ] | 492 | ] |
490 | } | 493 | } |
491 | def public transitiveClosure(Relation relation, TermDescription source, TermDescription target) { | 494 | def transitiveClosure(Relation relation, TermDescription source, TermDescription target) { |
492 | createTransitiveClosure => [ | 495 | createTransitiveClosure => [ |
493 | it.relation = relation | 496 | it.relation = relation |
494 | it.leftOperand = leftOperand | 497 | it.leftOperand = source.toTerm |
495 | it.rightOperand = rightOperand | 498 | it.rightOperand = target.toTerm |
496 | ] | 499 | ] |
497 | } | 500 | } |
498 | 501 | ||
499 | // QuantifiedExpressions | 502 | // QuantifiedExpressions |
500 | 503 | ||
501 | def public Forall(Function1<VariableContext, ? extends TermDescription> expression) { | 504 | def Forall(Function1<VariableContext, ? extends TermDescription> expression) { |
502 | val context = new VariableContext(this,logicFactiory) | 505 | val context = new VariableContext(this,logicFactiory) |
503 | val term = expression.apply(context) | 506 | val term = expression.apply(context) |
504 | return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] | 507 | return createForall => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] |
505 | } | 508 | } |
506 | def public Forall(TermDescription expression, Variable... variables) { | 509 | def Forall(TermDescription expression, Variable... variables) { |
507 | Forall(variables,expression) } | 510 | Forall(variables,expression) } |
508 | def public Forall(Iterable<? extends Variable> variables,TermDescription expression) { | 511 | def Forall(Iterable<? extends Variable> variables,TermDescription expression) { |
509 | val forallExpression = createForall | 512 | val forallExpression = createForall |
510 | for(variable : variables) forallExpression.quantifiedVariables += variable | 513 | for(variable : variables) forallExpression.quantifiedVariables += variable |
511 | forallExpression.expression = expression.toTerm | 514 | forallExpression.expression = expression.toTerm |
512 | return forallExpression | 515 | return forallExpression |
513 | } | 516 | } |
514 | 517 | ||
515 | def public Exists(Function1<VariableContext, ? extends TermDescription> expression) { | 518 | def Exists(Function1<VariableContext, ? extends TermDescription> expression) { |
516 | val context = new VariableContext(this,logicFactiory) | 519 | val context = new VariableContext(this,logicFactiory) |
517 | val term = expression.apply(context) | 520 | val term = expression.apply(context) |
518 | return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] | 521 | return createExists => [x| x.quantifiedVariables+=context.variables x.expression = term.toTerm] |
519 | } | 522 | } |
520 | def public Exists(TermDescription expression, Variable... variables) { | 523 | def Exists(TermDescription expression, Variable... variables) { |
521 | Exists(variables,expression) } | 524 | Exists(variables,expression) } |
522 | def public Exists(Iterable<? extends Variable> variables, TermDescription expression) { | 525 | def Exists(Iterable<? extends Variable> variables, TermDescription expression) { |
523 | val existsExpression = createExists | 526 | val existsExpression = createExists |
524 | for(variable : variables) existsExpression.quantifiedVariables += variable | 527 | for(variable : variables) existsExpression.quantifiedVariables += variable |
525 | existsExpression.expression = expression.toTerm | 528 | existsExpression.expression = expression.toTerm |
526 | return existsExpression | 529 | return existsExpression |
527 | } | 530 | } |
528 | 531 | ||
532 | // AggregatedExpression | ||
533 | |||
534 | private def <T extends AggregateExpression> configureAggregateExpression(T expression, Relation referred, List<Variable> terms, Variable target) { | ||
535 | if(terms.size != referred.parameters.size) { | ||
536 | throw new LogicProblemBuilderException( | ||
537 | '''The function called has «referred.parameters.size» parameters but it is called with «terms.size»!''') | ||
538 | } else { | ||
539 | expression.relation = referred | ||
540 | expression.resultVariable = target | ||
541 | for(var i=0; i<referred.parameters.size;i++) { | ||
542 | val targetRelation = terms.get(i) | ||
543 | val substitution = createAggregatedParameterSubstitution => [it.variable = targetRelation] | ||
544 | expression.parameterSubstitution += substitution | ||
545 | } | ||
546 | return expression | ||
547 | } | ||
548 | } | ||
549 | private def <T extends ProjectedAggregateExpression> configureProjectedAggregateExpression(T expression, Relation referred, List<Variable> terms, Variable target, int projection) { | ||
550 | if(projection < 0 || projection >= referred.parameters.size) { | ||
551 | throw new LogicProblemBuilderException( | ||
552 | '''The function called has «referred.parameters.size» parameters but it is called with «terms.size»!''') | ||
553 | } else { | ||
554 | val res = expression.configureAggregateExpression(referred, terms,target) | ||
555 | if(res.parameterSubstitution.get(projection).variable !== null) { | ||
556 | throw new LogicProblemBuilderException( | ||
557 | '''Projection over set variable!''') | ||
558 | } | ||
559 | val projectionType = referred.parameters.get(projection) | ||
560 | if(!(projectionType instanceof IntTypeReference || projectionType instanceof RealTypeReference)) { | ||
561 | throw new LogicProblemBuilderException('''Projection over nunnumeric parameter!''' | ||
562 | ) | ||
563 | } | ||
564 | res.projectionIndex = projection | ||
565 | return res | ||
566 | } | ||
567 | |||
568 | } | ||
569 | def Count(Relation referred, List<Variable> terms, Variable result) { | ||
570 | createCount.configureAggregateExpression(referred,terms,result) | ||
571 | } | ||
572 | def Sum(Relation referred, List<Variable> terms, int projection, Variable result) { | ||
573 | createSum.configureProjectedAggregateExpression(referred,terms,result,projection) | ||
574 | } | ||
575 | def Min(Relation referred, List<Variable> terms, int projection, Variable result) { | ||
576 | createMin.configureProjectedAggregateExpression(referred,terms,result,projection) | ||
577 | } | ||
578 | def Max(Relation referred, List<Variable> terms, int projection, Variable result) { | ||
579 | createMax.configureProjectedAggregateExpression(referred,terms,result,projection) | ||
580 | } | ||
581 | |||
529 | // Function calls | 582 | // Function calls |
530 | def public call(Function function, TermDescription... substitutions) { | 583 | def call(Function function, TermDescription... substitutions) { |
531 | call(function, substitutions as Iterable<? extends TermDescription>) } | 584 | call(function, substitutions as Iterable<? extends TermDescription>) } |
532 | def public call(Function function, Iterable<? extends TermDescription> substitutions) { | 585 | def call(Function function, Iterable<? extends TermDescription> substitutions) { |
533 | val functionReference = createSymbolicValue | 586 | val functionReference = createSymbolicValue |
534 | functionReference.symbolicReference=function | 587 | functionReference.symbolicReference=function |
535 | val List<TermDescription> l= new LinkedList() | 588 | val List<TermDescription> l= new LinkedList() |
@@ -546,20 +599,22 @@ public class LogicProblemBuilder{ | |||
546 | } | 599 | } |
547 | 600 | ||
548 | // Relation calls | 601 | // Relation calls |
549 | def public call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable<? extends TermDescription>)} | 602 | def call(Relation relation, TermDescription... substitution) { relation.call(substitution as Iterable<? extends TermDescription>)} |
550 | def public call(Relation relation, Iterable<? extends TermDescription> substitution) { | 603 | def call(Relation relation, Iterable<? extends TermDescription> substitution) { |
551 | val relationReference = createSymbolicValue | 604 | val relationReference = createSymbolicValue |
605 | if(relation === null) { | ||
606 | throw new LogicProblemBuilderException('''Call is referring to null!''') | ||
607 | } | ||
552 | relationReference.symbolicReference = relation | 608 | relationReference.symbolicReference = relation |
553 | //println('''«relation.name»(«substitution.size»->«relation.parameters»)''') | ||
554 | for(value : substitution) | 609 | for(value : substitution) |
555 | relationReference.parameterSubstitutions += value.toTerm | 610 | relationReference.parameterSubstitutions += value.toTerm |
556 | relationReference.checkRelationCall(relation) | 611 | relationReference.checkRelationCall(relation) |
557 | return relationReference | 612 | return relationReference |
558 | } | 613 | } |
559 | def private checkRelationCall(SymbolicValue value, Relation referredRelation) { | 614 | def private checkRelationCall(SymbolicValue value, Relation referredRelation) { |
560 | // if(value === null || referredRelation === null) { | 615 | if(value === null || referredRelation === null) { |
561 | // println("gebasz") | 616 | throw new LogicProblemBuilderException('''Call is referring to null!''') |
562 | // } | 617 | } |
563 | if(value.parameterSubstitutions.size != referredRelation.parameters.size) { | 618 | if(value.parameterSubstitutions.size != referredRelation.parameters.size) { |
564 | throw new LogicProblemBuilderException( | 619 | throw new LogicProblemBuilderException( |
565 | '''The relation "«referredRelation.name»" called has «referredRelation.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''') | 620 | '''The relation "«referredRelation.name»" called has «referredRelation.parameters.size» parameters but it is called with «value.parameterSubstitutions.size»!''') |
@@ -567,11 +622,9 @@ public class LogicProblemBuilder{ | |||
567 | } | 622 | } |
568 | 623 | ||
569 | // constant evaluation | 624 | // constant evaluation |
570 | def public call(Constant constant) { | 625 | def call(Constant constant) { |
571 | val constantReference = createSymbolicValue | 626 | val constantReference = createSymbolicValue |
572 | constantReference.symbolicReference = constant | 627 | constantReference.symbolicReference = constant |
573 | return constantReference | 628 | return constantReference |
574 | } | 629 | } |
575 | |||
576 | |||
577 | } | 630 | } |
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 index b4d9a8fa..3e0c86c4 100644 --- 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 | |||
@@ -34,7 +34,7 @@ public class LogicReasonerException extends Exception { | |||
34 | } | 34 | } |
35 | } | 35 | } |
36 | 36 | ||
37 | abstract class LogicSolverConfiguration { | 37 | abstract class SolverConfiguration { |
38 | public static val Unlimited = -1; | 38 | public static val Unlimited = -1; |
39 | public static val String UndefinedPath = null | 39 | public static val String UndefinedPath = null |
40 | 40 | ||
@@ -42,7 +42,7 @@ abstract class LogicSolverConfiguration { | |||
42 | public String solverPath = UndefinedPath | 42 | public String solverPath = UndefinedPath |
43 | /** Max runtime limit in seconds. */ | 43 | /** Max runtime limit in seconds. */ |
44 | public int runtimeLimit = Unlimited | 44 | public int runtimeLimit = Unlimited |
45 | /** Max runtime limit in seconds. */ | 45 | /** Max memory limit in megabytes. */ |
46 | public int memoryLimit = Unlimited | 46 | public int memoryLimit = Unlimited |
47 | /** Documentation level of the solver. */ | 47 | /** Documentation level of the solver. */ |
48 | public DocumentationLevel documentationLevel = DocumentationLevel::NONE | 48 | public DocumentationLevel documentationLevel = DocumentationLevel::NONE |
@@ -52,7 +52,9 @@ abstract class LogicSolverConfiguration { | |||
52 | * or via a listener registered by {@link progressMonitor.addCancelListener}</li> | 52 | * or via a listener registered by {@link progressMonitor.addCancelListener}</li> |
53 | */ | 53 | */ |
54 | public SolverProgressMonitor progressMonitor = new NullSolverProgressMonitor | 54 | public SolverProgressMonitor progressMonitor = new NullSolverProgressMonitor |
55 | } | ||
55 | 56 | ||
57 | abstract class LogicSolverConfiguration extends SolverConfiguration { | ||
56 | public var TypeScopes typeScopes = new TypeScopes; | 58 | public var TypeScopes typeScopes = new TypeScopes; |
57 | public var SolutionScope solutionScope = new SolutionScope | 59 | public var SolutionScope solutionScope = new SolutionScope |
58 | } | 60 | } |
@@ -157,7 +159,7 @@ public class TypeScopes { | |||
157 | */ | 159 | */ |
158 | public class SolutionScope { | 160 | public class SolutionScope { |
159 | public static val All = Integer.MAX_VALUE; | 161 | public static val All = Integer.MAX_VALUE; |
160 | public var numberOfRequiredSolution = 1 | 162 | public var numberOfRequiredSolutions = 1 |
161 | } | 163 | } |
162 | /** Progress monitor class for a solver to | 164 | /** Progress monitor class for a solver to |
163 | * <li>(optionally) report progress via {@link worked}</li> | 165 | * <li>(optionally) report progress via {@link worked}</li> |
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 index d673cb17..a78ceb19 100644 --- 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 | |||
@@ -17,7 +17,7 @@ class StatisticsData { | |||
17 | } | 17 | } |
18 | 18 | ||
19 | class StatisticSections2CSV { | 19 | class StatisticSections2CSV { |
20 | static val separator = ';' | 20 | static val separator = ',' |
21 | static val empty = "" | 21 | static val empty = "" |
22 | 22 | ||
23 | private def getValue(Map<String, String> map,String key) { | 23 | private def getValue(Map<String, String> map,String key) { |
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 index 39370d75..c5e81f94 100644 --- 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 | |||
@@ -12,7 +12,7 @@ class StatisticSections2Print { | |||
12 | { | 12 | { |
13 | var result = ""; | 13 | var result = ""; |
14 | for(statistic : statistics) { | 14 | for(statistic : statistics) { |
15 | result+= '''«statistic.readValue»;''' | 15 | result+= '''«statistic.readValue»,''' |
16 | } | 16 | } |
17 | return result | 17 | return result |
18 | } | 18 | } |