aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
diff options
context:
space:
mode:
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.xtend152
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
29import org.eclipse.xtend.lib.annotations.Accessors 29import org.eclipse.xtend.lib.annotations.Accessors
30 30
31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
32import org.eclipse.xtend.lib.annotations.Data
33import 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
33class PatternGenerator { 41class 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}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-08-26 16:46:52 +0000