diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | 152 |
1 files changed, 110 insertions, 42 deletions
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 5c35fb54..f3125b80 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 | |||
@@ -29,6 +29,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
29 | import org.eclipse.xtend.lib.annotations.Accessors | 29 | import org.eclipse.xtend.lib.annotations.Accessors |
30 | 30 | ||
31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
32 | import org.eclipse.xtend.lib.annotations.Data | ||
33 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
34 | |||
35 | @Data class PatternGeneratorResult { | ||
36 | CharSequence patternText | ||
37 | HashMap<PConstraint,String> constraint2MustPreconditionName | ||
38 | HashMap<PConstraint,String> constraint2CurrentPreconditionName | ||
39 | } | ||
32 | 40 | ||
33 | class PatternGenerator { | 41 | class PatternGenerator { |
34 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) | 42 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) |
@@ -39,12 +47,12 @@ class PatternGenerator { | |||
39 | @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) | 47 | @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) |
40 | @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) | 48 | @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) |
41 | @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer | 49 | @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer |
42 | @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator // = new RefinementGenerator(this) | 50 | @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this) |
43 | @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator( | 51 | @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this) |
44 | this) | 52 | @Accessors(PUBLIC_GETTER) val UnitPropagationPreconditionGenerator unitPropagationPreconditionGenerator = new UnitPropagationPreconditionGenerator(this) |
45 | 53 | ||
46 | new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) { | 54 | public new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) { |
47 | if (typeInferenceMethod == TypeInferenceMethod.Generic) { | 55 | if(typeInferenceMethod == TypeInferenceMethod.Generic) { |
48 | this.typeIndexer = new GenericTypeIndexer(this) | 56 | this.typeIndexer = new GenericTypeIndexer(this) |
49 | this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) | 57 | this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) |
50 | } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { | 58 | } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { |
@@ -151,8 +159,8 @@ class PatternGenerator { | |||
151 | RelationConstraints constraints, | 159 | RelationConstraints constraints, |
152 | Collection<LinearTypeConstraintHint> hints | 160 | Collection<LinearTypeConstraintHint> hints |
153 | ) { | 161 | ) { |
154 | 162 | val first = | |
155 | return ''' | 163 | ''' |
156 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" | 164 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" |
157 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" | 165 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" |
158 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" | 166 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" |
@@ -167,6 +175,7 @@ class PatternGenerator { | |||
167 | ///////////////////////// | 175 | ///////////////////////// |
168 | // 0.1 Existence | 176 | // 0.1 Existence |
169 | ///////////////////////// | 177 | ///////////////////////// |
178 | /** [[exist(element)]]=1 */ | ||
170 | private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 179 | private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { |
171 | find interpretation(problem,interpretation); | 180 | find interpretation(problem,interpretation); |
172 | LogicProblem.elements(problem,element); | 181 | LogicProblem.elements(problem,element); |
@@ -175,6 +184,7 @@ class PatternGenerator { | |||
175 | PartialInterpretation.newElements(interpretation,element); | 184 | PartialInterpretation.newElements(interpretation,element); |
176 | } | 185 | } |
177 | 186 | ||
187 | /** [[exist(element)]]>=1/2 */ | ||
178 | private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 188 | private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { |
179 | find mustExist(problem,interpretation,element); | 189 | find mustExist(problem,interpretation,element); |
180 | } or { | 190 | } or { |
@@ -195,57 +205,108 @@ class PatternGenerator { | |||
195 | //////////////////////// | 205 | //////////////////////// |
196 | // 0.2 Equivalence | 206 | // 0.2 Equivalence |
197 | //////////////////////// | 207 | //////////////////////// |
198 | pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | 208 | pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) |
209 | // For non-primitive type. Boolean types always must equivalent or cannot equivalent | ||
210 | { | ||
199 | find mayExist(problem,interpretation,a); | 211 | find mayExist(problem,interpretation,a); |
200 | find mayExist(problem,interpretation,b); | 212 | find mayExist(problem,interpretation,b); |
201 | a == b; | 213 | a == b; |
214 | ««« } or { | ||
215 | ««« find mayExist(problem,interpretation,a); | ||
216 | ««« find mayExist(problem,interpretation,b); | ||
217 | ««« IntegerElement(a); | ||
218 | ««« IntegerElement(b); | ||
219 | ««« PrimitiveElement.valueSet(a,false); | ||
220 | ««« } or { | ||
221 | ««« find mayExist(problem,interpretation,a); | ||
222 | ««« find mayExist(problem,interpretation,b); | ||
223 | ««« IntegerElement(a); | ||
224 | ««« IntegerElement(b); | ||
225 | ««« PrimitiveElement.valueSet(b,false); | ||
226 | ««« } or { | ||
227 | ««« find mayExist(problem,interpretation,a); | ||
228 | ««« find mayExist(problem,interpretation,b); | ||
229 | ««« RealElement(a); | ||
230 | ««« RealElement(b); | ||
231 | ««« PrimitiveElement.valueSet(a,false); | ||
232 | ««« } or { | ||
233 | ««« find mayExist(problem,interpretation,a); | ||
234 | ««« find mayExist(problem,interpretation,b); | ||
235 | ««« RealElement(a); | ||
236 | ««« RealElement(b); | ||
237 | ««« PrimitiveElement.valueSet(b,false); | ||
238 | ««« } or { | ||
239 | ««« find mayExist(problem,interpretation,a); | ||
240 | ««« find mayExist(problem,interpretation,b); | ||
241 | ««« StringElement(a); | ||
242 | ««« StringElement(b); | ||
243 | ««« PrimitiveElement.valueSet(a,false); | ||
244 | ««« } or { | ||
245 | ««« find mayExist(problem,interpretation,a); | ||
246 | ««« find mayExist(problem,interpretation,b); | ||
247 | ««« StringElement(a); | ||
248 | ««« StringElement(b); | ||
249 | ««« PrimitiveElement.valueSet(b,false); | ||
202 | } | 250 | } |
251 | |||
203 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | 252 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { |
253 | // For non-primitive and Boolean primitive type | ||
204 | find mustExist(problem,interpretation,a); | 254 | find mustExist(problem,interpretation,a); |
205 | find mustExist(problem,interpretation,b); | 255 | find mustExist(problem,interpretation,b); |
206 | a == b; | 256 | a == b; |
257 | ««« } or { | ||
258 | ««« find mustExist(problem,interpretation,a); | ||
259 | ««« find mustExist(problem,interpretation,b); | ||
260 | ««« PrimitiveElement.valueSet(a,true); | ||
261 | ««« PrimitiveElement.valueSet(b,true); | ||
262 | ««« IntegerElement.value(a,value); | ||
263 | ««« IntegerElement.value(b,value); | ||
264 | ««« } or { | ||
265 | ««« find mustExist(problem,interpretation,a); | ||
266 | ««« find mustExist(problem,interpretation,b); | ||
267 | ««« PrimitiveElement.valueSet(a,true); | ||
268 | ««« PrimitiveElement.valueSet(b,true); | ||
269 | ««« RealElement.value(a,value); | ||
270 | ««« RealElement.value(b,value); | ||
271 | ««« } or { | ||
272 | ««« find mustExist(problem,interpretation,a); | ||
273 | ««« find mustExist(problem,interpretation,b); | ||
274 | ««« PrimitiveElement.valueSet(a,true); | ||
275 | ««« PrimitiveElement.valueSet(b,true); | ||
276 | ««« StringElement.value(a,value); | ||
277 | ««« StringElement.value(b,value); | ||
207 | } | 278 | } |
208 | 279 | ||
209 | //////////////////////// | ||
210 | // 0.3 Required Patterns by TypeIndexer | ||
211 | //////////////////////// | ||
212 | «typeIndexer.requiredQueries» | ||
213 | |||
214 | ////////// | 280 | ////////// |
215 | // 1. Problem-Specific Base Indexers | 281 | // 1. Problem-Specific Base Indexers |
216 | ////////// | 282 | ////////// |
217 | // 1.1 Type Indexers | 283 | // 1.1 Type Indexers |
218 | ////////// | 284 | ////////// |
219 | // 1.1.1 primitive Type Indexers | 285 | // 1.1.1 Required Patterns by TypeIndexer |
220 | ////////// | 286 | ////////// |
221 | ««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 287 | |
222 | ««« find interpretation(problem,interpretation); | 288 | «typeIndexer.requiredQueries» |
223 | ««« PartialInterpretation.booleanelements(interpretation,element); | 289 | |
224 | ««« } | 290 | ////////// |
225 | ««« pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 291 | // 1.1.2 primitive Type Indexers |
226 | ««« find interpretation(problem,interpretation); | 292 | ////////// |
227 | ««« PartialInterpretation.integerelements(interpretation,element); | 293 | // Currently unused. Refer primitive types as: |
228 | ««« } or { | 294 | // > PrimitiveElement(element) |
229 | ««« find interpretation(problem,interpretation); | 295 | // specific types are referred as: |
230 | ««« PartialInterpretation.newIntegers(interpetation,element); | 296 | // > BooleanElement(variableName) |
231 | ««« } | 297 | // > IntegerElement(variableName) |
232 | ««« pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 298 | // > RealElement(variableName) |
233 | ««« find interpretation(problem,interpretation); | 299 | // > StringElement(variableName) |
234 | ««« PartialInterpretation.realelements(interpretation,element); | 300 | // And their value as |
235 | ««« } or { | 301 | // > BooleanElement.value(variableName,value) |
236 | ««« find interpretation(problem,interpretation); | 302 | // > IntegerElement.value(variableName,value) |
237 | ««« PartialInterpretation.newReals(interpetation,element); | 303 | // > RealElement.value(variableName,value) |
238 | ««« } | 304 | // > StringElement.value(variableName,value) |
239 | ««« pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 305 | // Whether a value is set is defined by: |
240 | ««« find interpretation(problem,interpretation); | 306 | // > PrimitiveElement.valueSet(variableName,isFilled); |
241 | ««« PartialInterpretation.stringelements(interpretation,element); | ||
242 | ««« } or { | ||
243 | ««« find interpretation(problem,interpretation); | ||
244 | ««« PartialInterpretation.newStrings(interpetation,element); | ||
245 | ««« } | ||
246 | 307 | ||
247 | ////////// | 308 | ////////// |
248 | // 1.1.2 domain-specific Type Indexers | 309 | // 1.1.3 domain-specific Type Indexers |
249 | ////////// | 310 | ////////// |
250 | «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» | 311 | «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» |
251 | 312 | ||
@@ -306,6 +367,13 @@ class PatternGenerator { | |||
306 | «FOR hint : hints» | 367 | «FOR hint : hints» |
307 | «hint.getAdditionalPatterns(this)» | 368 | «hint.getAdditionalPatterns(this)» |
308 | «ENDFOR» | 369 | «ENDFOR» |
309 | ''' | 370 | |
371 | ////////// | ||
372 | // 6 Unit Propagations | ||
373 | ////////// | ||
374 | ''' | ||
375 | val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) | ||
376 | val second = up.definitions | ||
377 | return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName) | ||
310 | } | 378 | } |
311 | } | 379 | } |