diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra')
7 files changed, 512 insertions, 211 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend index e511a961..fd4374f5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend | |||
@@ -11,7 +11,5 @@ import org.eclipse.xtend.lib.annotations.Data | |||
11 | class CanonisedFormulae { | 11 | class CanonisedFormulae { |
12 | CharSequence viatraCode | 12 | CharSequence viatraCode |
13 | Map<Assertion,String> assertion2ConstraintPattern | 13 | Map<Assertion,String> assertion2ConstraintPattern |
14 | Map<ConstantDefinition,String> constant2ValuePattern | ||
15 | Map<RelationDefinition,String> relation2ValuePattern | 14 | Map<RelationDefinition,String> relation2ValuePattern |
16 | Map<FunctionDefinition,String> function2ValuePattern | ||
17 | } \ No newline at end of file | 15 | } \ No newline at end of file |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend index 0af0b36a..182f3a3a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend | |||
@@ -5,17 +5,35 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | |||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
7 | import java.util.List | 7 | import java.util.List |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | 11 | ||
9 | /** | 12 | /** |
10 | * Translates a set of assertions and definitions to viatra patterns. | 13 | * Translates a Terms into format |
14 | * <P(x1,...,xn)> := Bodies(x1,...,xn) | ||
15 | * <Bodies(x1,...,xn)> := <Body(x1,...,xn)> | <Body(x1,...,xn)> or <Bodies(x1,...,xn)> | ||
16 | * <Body(x1,...,xn)> := Exists y1,...,ym : <Constraints(x1,...,xn,y1,....,ym)> | ||
17 | * <Constraints(x1,...,xn)> := Constraint(x1,...xn) | Constraint(x1,...,xn) and <Constraints(x1,...,xn)> | ||
11 | */ | 18 | */ |
12 | class FormulaCanoniser { | 19 | class FormulaCanoniser { |
13 | def canonise( | 20 | // def canonise( |
14 | List<Assertion> assertions, | 21 | // List<Assertion> assertions, |
15 | List<RelationDefinition> relations, | 22 | // List<RelationDefinition> relations) |
16 | List<ConstantDefinition> constants, | 23 | // { |
17 | List<FunctionDefinition> functions) | 24 | // |
18 | { | 25 | // } |
19 | 26 | // | |
20 | } | 27 | // |
28 | // def canoniseToConstraintBlock(Term predicate, List<Variable> variables) { | ||
29 | // val | ||
30 | // } | ||
31 | // | ||
32 | // def freeVariables(Term t) { | ||
33 | // val subterms = #[t]+t.eAllContents.toList | ||
34 | // val variables = subterms.filter(Variable).toSet | ||
35 | // val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable] | ||
36 | // val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)] | ||
37 | // return freeVariables.map | ||
38 | // } | ||
21 | } \ No newline at end of file | 39 | } \ No newline at end of file |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend new file mode 100644 index 00000000..a421d1fd --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend | |||
@@ -0,0 +1,243 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
5 | import org.eclipse.emf.ecore.EAttribute | ||
6 | import org.eclipse.emf.ecore.EEnumLiteral | ||
7 | import org.eclipse.emf.ecore.EReference | ||
8 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
9 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
10 | import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey | ||
11 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
12 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
13 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality | ||
14 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter | ||
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
16 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality | ||
17 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | ||
18 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint | ||
19 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure | ||
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue | ||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall | ||
22 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint | ||
23 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping | ||
24 | import java.util.List | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
31 | |||
32 | class PConstraintTransformer { | ||
33 | val extension RelationDefinitionIndexer relationDefinitionIndexer; | ||
34 | val expressionExtractor = new XExpressionExtractor | ||
35 | val expressionGenerator = new PExpressionGenerator | ||
36 | |||
37 | new(RelationDefinitionIndexer relationDefinitionIndexer) { | ||
38 | this.relationDefinitionIndexer = relationDefinitionIndexer | ||
39 | } | ||
40 | |||
41 | dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List<VariableMapping> variableMapping) { | ||
42 | val touple = constraint.variablesTuple | ||
43 | if(touple.size == 1) { | ||
44 | val inputKey = constraint.equivalentJudgement.inputKey | ||
45 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
46 | return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
47 | constraint.getVariableInTuple(0).canonizeName) | ||
48 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
49 | return '''// type constraint is enforced by construction''' | ||
50 | } | ||
51 | |||
52 | } else if(touple.size == 2){ | ||
53 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
54 | if(key instanceof EReference) { | ||
55 | return base.referRelationByName( | ||
56 | key, | ||
57 | constraint.getVariableInTuple(0).canonizeName, | ||
58 | constraint.getVariableInTuple(1).canonizeName, | ||
59 | modality.toMustMay) | ||
60 | } else if (key instanceof EAttribute) { | ||
61 | return base.referAttributeByName(key, | ||
62 | constraint.getVariableInTuple(0).canonizeName, | ||
63 | constraint.getVariableInTuple(1).canonizeName, | ||
64 | modality.toMustMay) | ||
65 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
66 | } else { | ||
67 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
68 | } | ||
69 | } | ||
70 | dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List<VariableMapping> variableMapping) { | ||
71 | val touple = constraint.variablesTuple | ||
72 | if(touple.size == 1) { | ||
73 | val inputKey = constraint.equivalentJudgement.inputKey | ||
74 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
75 | return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
76 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName) | ||
77 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
78 | return '''// type constraint is enforced by construction''' | ||
79 | } | ||
80 | |||
81 | } else if(touple.size == 2){ | ||
82 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
83 | if(key instanceof EReference) { | ||
84 | return base.referRelationByName( | ||
85 | key, | ||
86 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
87 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
88 | modality.toMustMay) | ||
89 | } else if (key instanceof EAttribute) { | ||
90 | return base.referAttributeByName(key, | ||
91 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
92 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
93 | modality.toMustMay) | ||
94 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
95 | } else { | ||
96 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
97 | } | ||
98 | } | ||
99 | |||
100 | dispatch def transformConstraint(Equality equality, Modality modality, List<VariableMapping> variableMapping) { | ||
101 | val a = equality.who | ||
102 | val b = equality.withWhom | ||
103 | transformEquality(modality.toMustMay, a, b) | ||
104 | } | ||
105 | |||
106 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { | ||
107 | if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
108 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
109 | } | ||
110 | |||
111 | dispatch def transformConstraint(Inequality inequality, Modality modality, List<VariableMapping> variableMapping) { | ||
112 | val a = inequality.who | ||
113 | val b = inequality.withWhom | ||
114 | if(modality.isCurrent) { | ||
115 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
116 | } else if(modality.isMust) { | ||
117 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
118 | } else { // modality.isMay | ||
119 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
120 | } | ||
121 | } | ||
122 | |||
123 | dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) { | ||
124 | val params = (0..<pcall.actualParametersTuple.size).map[index | | ||
125 | val variable = pcall.actualParametersTuple.get(index) as PVariable | ||
126 | return variable.canonizeName | ||
127 | ] | ||
128 | return referPattern(pcall.referredQuery,params,modality.dual,false,false) | ||
129 | } | ||
130 | |||
131 | dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) { | ||
132 | val params = (0..<pcall.variablesTuple.size).map[index | | ||
133 | val variable = pcall.variablesTuple.get(index) as PVariable | ||
134 | return variable.canonizeName | ||
135 | ] | ||
136 | return referPattern(pcall.referredQuery,params,modality,true,false) | ||
137 | } | ||
138 | dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> variableMapping) { | ||
139 | val params = (0..1).map[index | | ||
140 | val variable = pcall.getVariableInTuple(index) as PVariable | ||
141 | return variable.canonizeName | ||
142 | ] | ||
143 | return referPattern(pcall.referredQuery,params,modality,true,true) | ||
144 | } | ||
145 | dispatch def transformConstraint(ExportedParameter e, Modality modality, List<VariableMapping> variableMapping) { | ||
146 | return '''// «e.parameterName» is exported''' | ||
147 | } | ||
148 | dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> variableMapping) { | ||
149 | val target = c.supplierKey | ||
150 | |||
151 | var String targetString; | ||
152 | var String additionalDefinition; | ||
153 | if(target instanceof EEnumLiteral) { | ||
154 | targetString = '''const_«target.name»_«target.EEnum.name»''' | ||
155 | additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);''' | ||
156 | } else if(target instanceof Integer) { | ||
157 | targetString = '''const_«target»_Integer''' | ||
158 | additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);''' | ||
159 | } else if(target instanceof Boolean) { | ||
160 | targetString = '''const_«target»_Boolean''' | ||
161 | additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);''' | ||
162 | } else if(target instanceof String) { | ||
163 | targetString = '''const_«target»_String''' | ||
164 | additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");''' | ||
165 | } else if(target instanceof Double) { | ||
166 | targetString = '''const_«target»_Real''' | ||
167 | additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);''' | ||
168 | } else if(target instanceof Float) { | ||
169 | targetString = '''const_«target»_Real''' | ||
170 | additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);''' | ||
171 | } else { | ||
172 | throw new UnsupportedOperationException('''Unknown constant type: «target.class»''') | ||
173 | } | ||
174 | |||
175 | val source = c.variablesTuple | ||
176 | var String sourceName | ||
177 | if(source.size == 1) | ||
178 | sourceName = (source.get(0) as PVariable).canonizeName | ||
179 | else throw new UnsupportedOperationException("unknown source") | ||
180 | return '''«sourceName» == «targetString»;«additionalDefinition»'''; | ||
181 | } | ||
182 | |||
183 | protected def valueVariable(PVariable v) { | ||
184 | "value_"+v.canonizeName | ||
185 | } | ||
186 | protected def valueSetted(PVariable v) { | ||
187 | "setted_"+v.canonizeName | ||
188 | } | ||
189 | def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) { | ||
190 | val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference | ||
191 | if(m.isMay) { | ||
192 | '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpression(typeReference,v,v.valueVariable)» check(!«v.valueSetted»||«v.valueVariable»==«target»));''' | ||
193 | } else { // Must or current | ||
194 | '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpression(typeReference,v,target)»''' | ||
195 | } | ||
196 | } | ||
197 | |||
198 | private def hasValueExpression(List<VariableMapping> variableMapping, PVariable v, String target) { | ||
199 | hasValueExpression( | ||
200 | variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range, | ||
201 | v, | ||
202 | target | ||
203 | ) | ||
204 | } | ||
205 | private def dispatch hasValueExpression(BoolTypeReference typeReference, PVariable v, String target) '''BooleanElement.value(«v.canonizeName»,«target»);''' | ||
206 | private def dispatch hasValueExpression(IntTypeReference typeReference, PVariable v, String target) '''IntegerElement.value(«v.canonizeName»,«target»);''' | ||
207 | private def dispatch hasValueExpression(RealTypeReference typeReference, PVariable v, String target) '''RealElement.value(«v.canonizeName»,«target»);''' | ||
208 | private def dispatch hasValueExpression(StringTypeReference typeReference, PVariable v, String target) '''StringElement.value(«v.canonizeName»,«target»);''' | ||
209 | private def dispatch hasValueExpression(TypeReference typeReference, PVariable v, String target) { | ||
210 | throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''') | ||
211 | } | ||
212 | |||
213 | dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List<VariableMapping> variableMapping) { | ||
214 | if(e.outputVariable!==null) { | ||
215 | throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''') | ||
216 | } else { | ||
217 | val expression = expressionExtractor.extractExpression(e.evaluator) | ||
218 | if(modality.isMay) { | ||
219 | return ''' | ||
220 | «FOR variable: e.affectedVariables» | ||
221 | PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)» | ||
222 | «ENDFOR» | ||
223 | check( | ||
224 | «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR» | ||
225 | || | ||
226 | («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])») | ||
227 | ); | ||
228 | ''' | ||
229 | } else { // Must or Current | ||
230 | return ''' | ||
231 | «FOR variable: e.affectedVariables» | ||
232 | PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)» | ||
233 | «ENDFOR» | ||
234 | check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»); | ||
235 | ''' | ||
236 | } | ||
237 | } | ||
238 | } | ||
239 | |||
240 | dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) { | ||
241 | throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''') | ||
242 | } | ||
243 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend new file mode 100644 index 00000000..303c87b9 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend | |||
@@ -0,0 +1,109 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | ||
2 | |||
3 | import java.util.Map | ||
4 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | ||
5 | import org.eclipse.xtext.xbase.XBinaryOperation | ||
6 | import org.eclipse.xtext.xbase.XExpression | ||
7 | import org.eclipse.xtext.xbase.XFeatureCall | ||
8 | import org.eclipse.xtext.xbase.XMemberFeatureCall | ||
9 | import org.eclipse.xtext.xbase.XNumberLiteral | ||
10 | import org.eclipse.xtext.xbase.XUnaryOperation | ||
11 | |||
12 | class PExpressionGenerator { | ||
13 | static val N_Base = "org.eclipse.xtext.xbase.lib." | ||
14 | |||
15 | static val N_PLUS1 = "operator_plus" | ||
16 | static val N_MINUS1 = "operator_minus" | ||
17 | |||
18 | static val N_MINUS2 = "operator_minus" | ||
19 | static val N_PLUS2 = "operator_plus" | ||
20 | static val N_POWER = "operator_power" | ||
21 | static val N_MULTIPLY = "operator_multiply" | ||
22 | static val N_DIVIDE = "operator_divide" | ||
23 | static val N_MODULO = "operator_modulo" | ||
24 | static val N_LESSTHAN = "operator_lessThan" | ||
25 | static val N_LESSEQUALSTHAN = "operator_lessEqualsThan" | ||
26 | static val N_GREATERTHAN = "operator_greaterThan" | ||
27 | static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan" | ||
28 | static val N_EQUALS = "operator_equals" | ||
29 | static val N_NOTEQUALS = "operator_notEquals" | ||
30 | static val N_EQUALS3 = "operator_tripleEquals" | ||
31 | static val N_NOTEQUALS3 = "operator_tripleNotEquals" | ||
32 | |||
33 | protected def isN(String name, String s) { | ||
34 | val res = name.startsWith(N_Base) && name.endsWith(s) | ||
35 | //println('''[«res»] «name» ?= «N_Base»*«s»''') | ||
36 | return res | ||
37 | } | ||
38 | |||
39 | static val N_POWER2 = "java.lang.Math.pow" | ||
40 | |||
41 | def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName) { | ||
42 | val left = e.leftOperand.translateExpression(valueName) | ||
43 | val right = e.rightOperand.translateExpression(valueName) | ||
44 | val feature = e.feature.qualifiedName | ||
45 | if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''} | ||
46 | else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' } | ||
47 | else if(feature.isN(N_POWER)) { return '''(«left»^«right»)''' } | ||
48 | else if(feature.isN(N_MULTIPLY)) { return '''(«left»*«right»)''' } | ||
49 | else if(feature.isN(N_DIVIDE)) { return '''(«left»/«right»)''' } | ||
50 | else if(feature.isN(N_MODULO)) { return '''(«left»%«right»)''' } | ||
51 | else if(feature.isN(N_LESSTHAN)) { return '''(«left»<«right»)''' } | ||
52 | else if(feature.isN(N_LESSEQUALSTHAN)) { return '''(«left»<=«right»)''' } | ||
53 | else if(feature.isN(N_GREATERTHAN)) { return '''(«left»>«right»)''' } | ||
54 | else if(feature.isN(N_GREATEREQUALTHAN)) { return '''(«left»>=«right»)''' } | ||
55 | else if(feature.isN(N_EQUALS)) { return '''(«left»==«right»)''' } | ||
56 | else if(feature.isN(N_NOTEQUALS)) { return '''(«left»!=«right»)''' } | ||
57 | else if(feature.isN(N_EQUALS3)) { return '''(«left»===«right»)''' } | ||
58 | else if(feature.isN(N_NOTEQUALS3)) { return '''(«left»!==«right»)''' } | ||
59 | else { | ||
60 | println("-> " + e.feature+","+e.class) | ||
61 | println("-> " + e.leftOperand) | ||
62 | println("-> " + e.rightOperand) | ||
63 | println("-> " + e.feature.qualifiedName) | ||
64 | throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''') | ||
65 | } | ||
66 | } | ||
67 | |||
68 | def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName) { | ||
69 | val operand = e.operand.translateExpression(valueName) | ||
70 | val feature = e.feature.qualifiedName | ||
71 | if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''} | ||
72 | else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''} | ||
73 | else{ | ||
74 | println("-> " + e.feature+","+e.class) | ||
75 | println("-> " + e.operand) | ||
76 | println("-> " + e.feature.qualifiedName) | ||
77 | throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''') | ||
78 | } | ||
79 | } | ||
80 | |||
81 | def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName) { | ||
82 | val transformedArguments = e.actualArguments.map[translateExpression(valueName)] | ||
83 | val feature = e.feature.qualifiedName | ||
84 | if(feature == N_POWER2) { | ||
85 | return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)''' | ||
86 | }else { | ||
87 | println(e.feature+","+e.class) | ||
88 | println(e.actualArguments.join(", ")) | ||
89 | println(e.feature.qualifiedName) | ||
90 | throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''') | ||
91 | } | ||
92 | } | ||
93 | |||
94 | def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName) { | ||
95 | val featureName = e.feature.qualifiedName | ||
96 | val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head | ||
97 | if(entryWithName !== null) { | ||
98 | return entryWithName.value | ||
99 | } else { | ||
100 | throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''') | ||
101 | } | ||
102 | } | ||
103 | |||
104 | def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName) '''«l.value»''' | ||
105 | |||
106 | def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName) { | ||
107 | throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''') | ||
108 | } | ||
109 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index d4c76bb4..379e334a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | |||
@@ -170,6 +170,7 @@ class PatternGenerator { | |||
170 | ///////////////////////// | 170 | ///////////////////////// |
171 | // 0.1 Existence | 171 | // 0.1 Existence |
172 | ///////////////////////// | 172 | ///////////////////////// |
173 | /** [[exist(element)]]=1 */ | ||
173 | private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 174 | private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { |
174 | find interpretation(problem,interpretation); | 175 | find interpretation(problem,interpretation); |
175 | LogicProblem.elements(problem,element); | 176 | LogicProblem.elements(problem,element); |
@@ -178,6 +179,7 @@ class PatternGenerator { | |||
178 | PartialInterpretation.newElements(interpretation,element); | 179 | PartialInterpretation.newElements(interpretation,element); |
179 | } | 180 | } |
180 | 181 | ||
182 | /** [[exist(element)]]>=1/2 */ | ||
181 | private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 183 | private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { |
182 | find mustExist(problem,interpretation,element); | 184 | find mustExist(problem,interpretation,element); |
183 | } or { | 185 | } or { |
@@ -198,57 +200,143 @@ class PatternGenerator { | |||
198 | //////////////////////// | 200 | //////////////////////// |
199 | // 0.2 Equivalence | 201 | // 0.2 Equivalence |
200 | //////////////////////// | 202 | //////////////////////// |
201 | pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | 203 | pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) |
204 | // For non-primitive type. Boolean types always must equivalent or cannot equivalent | ||
205 | { | ||
202 | find mayExist(problem,interpretation,a); | 206 | find mayExist(problem,interpretation,a); |
203 | find mayExist(problem,interpretation,b); | 207 | find mayExist(problem,interpretation,b); |
204 | a == b; | 208 | a == b; |
209 | } or { | ||
210 | find mayExist(problem,interpretation,a); | ||
211 | find mayExist(problem,interpretation,b); | ||
212 | IntegerElement(a); | ||
213 | IntegerElement(b); | ||
214 | PrimitiveElement.valueSet(a,false); | ||
215 | } or { | ||
216 | find mayExist(problem,interpretation,a); | ||
217 | find mayExist(problem,interpretation,b); | ||
218 | IntegerElement(a); | ||
219 | IntegerElement(b); | ||
220 | PrimitiveElement.valueSet(b,false); | ||
221 | } or { | ||
222 | find mayExist(problem,interpretation,a); | ||
223 | find mayExist(problem,interpretation,b); | ||
224 | RealElement(a); | ||
225 | RealElement(b); | ||
226 | PrimitiveElement.valueSet(a,false); | ||
227 | } or { | ||
228 | find mayExist(problem,interpretation,a); | ||
229 | find mayExist(problem,interpretation,b); | ||
230 | RealElement(a); | ||
231 | RealElement(b); | ||
232 | PrimitiveElement.valueSet(b,false); | ||
233 | } or { | ||
234 | find mayExist(problem,interpretation,a); | ||
235 | find mayExist(problem,interpretation,b); | ||
236 | RealElement(a); | ||
237 | IntegerElement(b); | ||
238 | PrimitiveElement.valueSet(a,false); | ||
239 | } or { | ||
240 | find mayExist(problem,interpretation,a); | ||
241 | find mayExist(problem,interpretation,b); | ||
242 | RealElement(a); | ||
243 | IntegerElement(b); | ||
244 | PrimitiveElement.valueSet(b,false); | ||
245 | } or { | ||
246 | find mayExist(problem,interpretation,a); | ||
247 | find mayExist(problem,interpretation,b); | ||
248 | IntegerElement(a); | ||
249 | RealElement(b); | ||
250 | PrimitiveElement.valueSet(a,false); | ||
251 | } or { | ||
252 | find mayExist(problem,interpretation,a); | ||
253 | find mayExist(problem,interpretation,b); | ||
254 | IntegerElement(a); | ||
255 | RealElement(b); | ||
256 | PrimitiveElement.valueSet(b,false); | ||
257 | } or { | ||
258 | find mayExist(problem,interpretation,a); | ||
259 | find mayExist(problem,interpretation,b); | ||
260 | StringElement(a); | ||
261 | StringElement(b); | ||
262 | PrimitiveElement.valueSet(a,false); | ||
263 | } or { | ||
264 | find mayExist(problem,interpretation,a); | ||
265 | find mayExist(problem,interpretation,b); | ||
266 | StringElement(a); | ||
267 | StringElement(b); | ||
268 | PrimitiveElement.valueSet(b,false); | ||
205 | } | 269 | } |
270 | |||
206 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | 271 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { |
272 | // For non-primitive and Boolean primitive type | ||
207 | find mustExist(problem,interpretation,a); | 273 | find mustExist(problem,interpretation,a); |
208 | find mustExist(problem,interpretation,b); | 274 | find mustExist(problem,interpretation,b); |
209 | a == b; | 275 | a == b; |
276 | } or { | ||
277 | find mustExist(problem,interpretation,a); | ||
278 | find mustExist(problem,interpretation,b); | ||
279 | PrimitiveElement.valueSet(a,true); | ||
280 | PrimitiveElement.valueSet(b,true); | ||
281 | IntegerElement.value(a,value); | ||
282 | IntegerElement.value(b,value); | ||
283 | } or { | ||
284 | find mustExist(problem,interpretation,a); | ||
285 | find mustExist(problem,interpretation,b); | ||
286 | PrimitiveElement.valueSet(a,true); | ||
287 | PrimitiveElement.valueSet(b,true); | ||
288 | RealElement.value(a,value); | ||
289 | RealElement.value(b,value); | ||
290 | } or { | ||
291 | find mustExist(problem,interpretation,a); | ||
292 | find mustExist(problem,interpretation,b); | ||
293 | PrimitiveElement.valueSet(a,true); | ||
294 | PrimitiveElement.valueSet(b,true); | ||
295 | RealElement.value(a,value); | ||
296 | IntegerElement.value(b,value); | ||
297 | } or { | ||
298 | find mustExist(problem,interpretation,a); | ||
299 | find mustExist(problem,interpretation,b); | ||
300 | PrimitiveElement.valueSet(a,true); | ||
301 | PrimitiveElement.valueSet(b,true); | ||
302 | IntegerElement.value(a,value); | ||
303 | RealElement.value(b,value); | ||
304 | } or { | ||
305 | find mustExist(problem,interpretation,a); | ||
306 | find mustExist(problem,interpretation,b); | ||
307 | PrimitiveElement.valueSet(a,true); | ||
308 | PrimitiveElement.valueSet(b,true); | ||
309 | StringElement.value(a,value); | ||
310 | StringElement.value(b,value); | ||
210 | } | 311 | } |
211 | 312 | ||
212 | //////////////////////// | ||
213 | // 0.3 Required Patterns by TypeIndexer | ||
214 | //////////////////////// | ||
215 | «typeIndexer.requiredQueries» | ||
216 | |||
217 | ////////// | 313 | ////////// |
218 | // 1. Problem-Specific Base Indexers | 314 | // 1. Problem-Specific Base Indexers |
219 | ////////// | 315 | ////////// |
220 | // 1.1 Type Indexers | 316 | // 1.1 Type Indexers |
221 | ////////// | 317 | ////////// |
222 | // 1.1.1 primitive Type Indexers | 318 | // 1.1.1 Required Patterns by TypeIndexer |
223 | ////////// | 319 | ////////// |
224 | ««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 320 | «typeIndexer.requiredQueries» |
225 | ««« find interpretation(problem,interpretation); | 321 | ////////// |
226 | ««« PartialInterpretation.booleanelements(interpretation,element); | 322 | // 1.1.2 primitive Type Indexers |
227 | ««« } | 323 | ////////// |
228 | ««« pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 324 | // Currently unused. Refer primitive types as: |
229 | ««« find interpretation(problem,interpretation); | 325 | // > PrimitiveElement(element) |
230 | ««« PartialInterpretation.integerelements(interpretation,element); | 326 | // specific types are referred as: |
231 | ««« } or { | 327 | // > BooleanElement(variableName) |
232 | ««« find interpretation(problem,interpretation); | 328 | // > IntegerElement(variableName) |
233 | ««« PartialInterpretation.newIntegers(interpetation,element); | 329 | // > RealElement(variableName) |
234 | ««« } | 330 | // > StringElement(variableName) |
235 | ««« pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 331 | // And their value as |
236 | ««« find interpretation(problem,interpretation); | 332 | // > BooleanElement.value(variableName,value) |
237 | ««« PartialInterpretation.realelements(interpretation,element); | 333 | // > IntegerElement.value(variableName,value) |
238 | ««« } or { | 334 | // > RealElement.value(variableName,value) |
239 | ««« find interpretation(problem,interpretation); | 335 | // > StringElement.value(variableName,value) |
240 | ««« PartialInterpretation.newReals(interpetation,element); | 336 | // Whether a value is set is defined by: |
241 | ««« } | 337 | // > PrimitiveElement.valueSet(variableName,isFilled); |
242 | ««« pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
243 | ««« find interpretation(problem,interpretation); | ||
244 | ««« PartialInterpretation.stringelements(interpretation,element); | ||
245 | ««« } or { | ||
246 | ««« find interpretation(problem,interpretation); | ||
247 | ««« PartialInterpretation.newStrings(interpetation,element); | ||
248 | ««« } | ||
249 | |||
250 | ////////// | 338 | ////////// |
251 | // 1.1.2 domain-specific Type Indexers | 339 | // 1.1.3 domain-specific Type Indexers |
252 | ////////// | 340 | ////////// |
253 | «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» | 341 | «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» |
254 | 342 | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 9723373f..bd6e3e6e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend | |||
@@ -5,35 +5,22 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | |||
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
7 | import java.util.Map | 7 | import java.util.Map |
8 | import org.eclipse.emf.ecore.EAttribute | ||
9 | import org.eclipse.emf.ecore.EEnumLiteral | ||
10 | import org.eclipse.emf.ecore.EReference | ||
11 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | ||
12 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | ||
13 | import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey | ||
14 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | 8 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable |
16 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality | ||
17 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter | ||
18 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality | ||
19 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | ||
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure | 9 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure |
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue | ||
22 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall | ||
23 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint | ||
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 10 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
25 | 11 | ||
26 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint | ||
28 | 13 | ||
29 | class RelationDefinitionIndexer { | 14 | class RelationDefinitionIndexer { |
30 | val PatternGenerator base; | 15 | public val PatternGenerator base; |
16 | val PConstraintTransformer constraintTransformer; | ||
31 | 17 | ||
32 | new(PatternGenerator base) { | 18 | new(PatternGenerator base) { |
33 | this.base = base | 19 | this.base = base |
20 | this.constraintTransformer = new PConstraintTransformer(this); | ||
34 | } | 21 | } |
35 | 22 | ||
36 | public def generateRelationDefinitions( | 23 | def generateRelationDefinitions( |
37 | LogicProblem problem, | 24 | LogicProblem problem, |
38 | Iterable<RelationDefinition> relations, | 25 | Iterable<RelationDefinition> relations, |
39 | Map<String,PQuery> fqn2PQuery) { | 26 | Map<String,PQuery> fqn2PQuery) { |
@@ -74,7 +61,7 @@ class RelationDefinitionIndexer { | |||
74 | private def relationDefinitionName(RelationDefinition relation, Modality modality) | 61 | private def relationDefinitionName(RelationDefinition relation, Modality modality) |
75 | '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' | 62 | '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' |
76 | 63 | ||
77 | private def canonizeName(PVariable v) { | 64 | def canonizeName(PVariable v) { |
78 | return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' | 65 | return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' |
79 | } | 66 | } |
80 | 67 | ||
@@ -87,7 +74,7 @@ class RelationDefinitionIndexer { | |||
87 | «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ | 74 | «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ |
88 | find interpretation(problem,interpretation); | 75 | find interpretation(problem,interpretation); |
89 | «FOR constraint : body.constraints» | 76 | «FOR constraint : body.constraints» |
90 | «constraint.transformConstraint(modality)» | 77 | «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
91 | «ENDFOR» | 78 | «ENDFOR» |
92 | }«ENDFOR» | 79 | }«ENDFOR» |
93 | ''' | 80 | ''' |
@@ -104,158 +91,14 @@ class RelationDefinitionIndexer { | |||
104 | ''' | 91 | ''' |
105 | } | 92 | } |
106 | 93 | ||
107 | private def toMustMay(Modality modality) { | 94 | def toMustMay(Modality modality) { |
108 | if(modality == Modality::MAY) return Modality::MAY | 95 | if(modality == Modality::MAY) return Modality::MAY |
109 | else return Modality::MUST | 96 | else return Modality::MUST |
110 | } | 97 | } |
111 | 98 | ||
112 | def public referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' | 99 | def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' |
113 | «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); | 100 | «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); |
114 | ''' | 101 | ''' |
115 | 102 | ||
116 | private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) { | ||
117 | val touple = constraint.variablesTuple | ||
118 | if(touple.size == 1) { | ||
119 | val inputKey = constraint.equivalentJudgement.inputKey | ||
120 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
121 | return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
122 | constraint.getVariableInTuple(0).canonizeName) | ||
123 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
124 | return '''// type constraint is enforced by construction''' | ||
125 | } | ||
126 | |||
127 | } else if(touple.size == 2){ | ||
128 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
129 | if(key instanceof EReference) { | ||
130 | return base.referRelationByName( | ||
131 | key, | ||
132 | constraint.getVariableInTuple(0).canonizeName, | ||
133 | constraint.getVariableInTuple(1).canonizeName, | ||
134 | modality.toMustMay) | ||
135 | } else if (key instanceof EAttribute) { | ||
136 | return base.referAttributeByName(key, | ||
137 | constraint.getVariableInTuple(0).canonizeName, | ||
138 | constraint.getVariableInTuple(1).canonizeName, | ||
139 | modality.toMustMay) | ||
140 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
141 | } else { | ||
142 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
143 | } | ||
144 | } | ||
145 | private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) { | ||
146 | val touple = constraint.variablesTuple | ||
147 | if(touple.size == 1) { | ||
148 | val inputKey = constraint.equivalentJudgement.inputKey | ||
149 | if(inputKey instanceof EClassTransitiveInstancesKey) { | ||
150 | return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, | ||
151 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName) | ||
152 | } else if(inputKey instanceof EDataTypeInSlotsKey){ | ||
153 | return '''// type constraint is enforced by construction''' | ||
154 | } | ||
155 | |||
156 | } else if(touple.size == 2){ | ||
157 | val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey | ||
158 | if(key instanceof EReference) { | ||
159 | return base.referRelationByName( | ||
160 | key, | ||
161 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
162 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
163 | modality.toMustMay) | ||
164 | } else if (key instanceof EAttribute) { | ||
165 | return base.referAttributeByName(key, | ||
166 | (constraint.getVariablesTuple.get(0) as PVariable).canonizeName, | ||
167 | (constraint.getVariablesTuple.get(1) as PVariable).canonizeName, | ||
168 | modality.toMustMay) | ||
169 | } else throw new UnsupportedOperationException('''unknown key: «key.class»''') | ||
170 | } else { | ||
171 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | ||
172 | } | ||
173 | } | ||
174 | |||
175 | private dispatch def transformConstraint(Equality equality, Modality modality) { | ||
176 | val a = equality.who | ||
177 | val b = equality.withWhom | ||
178 | transformEquality(modality.toMustMay, a, b) | ||
179 | } | ||
180 | |||
181 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { | ||
182 | if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
183 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
184 | } | ||
185 | |||
186 | private dispatch def transformConstraint(Inequality inequality, Modality modality) { | ||
187 | val a = inequality.who | ||
188 | val b = inequality.withWhom | ||
189 | if(modality.isCurrent) { | ||
190 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
191 | } else if(modality.isMust) { | ||
192 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
193 | } else { // modality.isMay | ||
194 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | ||
195 | } | ||
196 | } | ||
197 | |||
198 | private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) { | ||
199 | val params = (0..<pcall.actualParametersTuple.size).map[index | | ||
200 | val variable = pcall.actualParametersTuple.get(index) as PVariable | ||
201 | return variable.canonizeName | ||
202 | ] | ||
203 | return referPattern(pcall.referredQuery,params,modality.dual,false,false) | ||
204 | } | ||
205 | 103 | ||
206 | private dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) { | ||
207 | val params = (0..<pcall.variablesTuple.size).map[index | | ||
208 | val variable = pcall.variablesTuple.get(index) as PVariable | ||
209 | return variable.canonizeName | ||
210 | ] | ||
211 | return referPattern(pcall.referredQuery,params,modality,true,false) | ||
212 | } | ||
213 | private dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) { | ||
214 | val params = (0..1).map[index | | ||
215 | val variable = pcall.getVariableInTuple(index) as PVariable | ||
216 | return variable.canonizeName | ||
217 | ] | ||
218 | return referPattern(pcall.referredQuery,params,modality,true,true) | ||
219 | } | ||
220 | private dispatch def transformConstraint(ExportedParameter e, Modality modality) { | ||
221 | return '''// «e.parameterName» is exported''' | ||
222 | } | ||
223 | private dispatch def transformConstraint(ConstantValue c, Modality modality) { | ||
224 | val target = c.supplierKey | ||
225 | |||
226 | var String targetString; | ||
227 | var String additionalDefinition; | ||
228 | if(target instanceof EEnumLiteral) { | ||
229 | targetString = '''const_«target.name»_«target.EEnum.name»''' | ||
230 | additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);''' | ||
231 | } else if(target instanceof Integer) { | ||
232 | targetString = '''const_«target»_Integer''' | ||
233 | additionalDefinition = '''IntegerElement.value(«targetString»,«target»);''' | ||
234 | } else if(target instanceof Boolean) { | ||
235 | targetString = '''const_«target»_Boolean''' | ||
236 | additionalDefinition = '''BooleanElement.value(«targetString»,«target»);''' | ||
237 | } else if(target instanceof String) { | ||
238 | targetString = '''const_«target»_String''' | ||
239 | additionalDefinition = '''StringElement.value(«targetString»,"«target»");''' | ||
240 | } else if(target instanceof Double) { | ||
241 | targetString = '''const_«target»_Number''' | ||
242 | additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' | ||
243 | } else if(target instanceof Float) { | ||
244 | targetString = '''const_«target»_Number''' | ||
245 | additionalDefinition = '''RealElement.value(«targetString»,"«target»");''' | ||
246 | } else { | ||
247 | throw new UnsupportedOperationException('''Unknown constant type: «target.class»''') | ||
248 | } | ||
249 | |||
250 | val source = c.variablesTuple | ||
251 | var String sourceName | ||
252 | if(source.size == 1) | ||
253 | sourceName = (source.get(0) as PVariable).canonizeName | ||
254 | else throw new UnsupportedOperationException("unknown source") | ||
255 | return '''«sourceName» == «targetString»;«additionalDefinition»'''; | ||
256 | } | ||
257 | |||
258 | private dispatch def transformConstraint(PConstraint c, Modality modality) { | ||
259 | throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''') | ||
260 | } | ||
261 | } \ No newline at end of file | 104 | } \ No newline at end of file |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend index d1d57189..41eb75a8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend | |||
@@ -48,5 +48,7 @@ abstract class TypeIndexer { | |||
48 | public def dispatch CharSequence referPrimitiveValue(String variableName, String value) { | 48 | public def dispatch CharSequence referPrimitiveValue(String variableName, String value) { |
49 | '''StringElement.value(«variableName»,"«value»");''' | 49 | '''StringElement.value(«variableName»,"«value»");''' |
50 | } | 50 | } |
51 | 51 | public def CharSequence referPrimitiveFilled(String variableName, boolean isFilled) { | |
52 | '''PrimitiveElement.valueSet(«variableName»,«isFilled»);''' | ||
53 | } | ||
52 | } \ No newline at end of file | 54 | } \ No newline at end of file |