diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit')
6 files changed, 229 insertions, 11 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index ff8ab437..f43ab96d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |||
@@ -2,6 +2,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 4 | 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.viatrasolver.logic2viatra.patterns.PatternProvider | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider |
@@ -9,14 +10,13 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
9 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 10 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
10 | import java.util.Collection | 11 | import java.util.Collection |
11 | import java.util.List | 12 | import java.util.List |
13 | import java.util.Set | ||
12 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 14 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
13 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 15 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
14 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 16 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 17 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
16 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 18 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
17 | import org.eclipse.xtend.lib.annotations.Data | 19 | import org.eclipse.xtend.lib.annotations.Data |
18 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
19 | import java.util.Set | ||
20 | 20 | ||
21 | class ModelGenerationStatistics { | 21 | class ModelGenerationStatistics { |
22 | public var long transformationExecutionTime = 0 | 22 | public var long transformationExecutionTime = 0 |
@@ -53,6 +53,7 @@ class ModelGenerationMethodProvider { | |||
53 | ReasonerWorkspace workspace, | 53 | ReasonerWorkspace workspace, |
54 | boolean nameNewElements, | 54 | boolean nameNewElements, |
55 | TypeInferenceMethod typeInferenceMethod, | 55 | TypeInferenceMethod typeInferenceMethod, |
56 | ScopePropagator scopePropagator, | ||
56 | DocumentationLevel debugLevel | 57 | DocumentationLevel debugLevel |
57 | ) { | 58 | ) { |
58 | val statistics = new ModelGenerationStatistics | 59 | val statistics = new ModelGenerationStatistics |
@@ -66,10 +67,9 @@ class ModelGenerationMethodProvider { | |||
66 | .map[it.patternPQuery as PQuery] | 67 | .map[it.patternPQuery as PQuery] |
67 | .toSet | 68 | .toSet |
68 | 69 | ||
69 | val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) | 70 | val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) |
70 | |||
71 | val //LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 71 | val //LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> |
72 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,nameNewElements,statistics) | 72 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,scopePropagator,nameNewElements,statistics) |
73 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) | 73 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) |
74 | 74 | ||
75 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) | 75 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend new file mode 100644 index 00000000..38633c07 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend | |||
@@ -0,0 +1,156 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
6 | import java.util.HashMap | ||
7 | import java.util.Map | ||
8 | import java.util.Set | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
10 | import java.util.HashSet | ||
11 | |||
12 | class ScopePropagator { | ||
13 | PartialInterpretation partialInterpretation | ||
14 | Map<PartialTypeInterpratation,Scope> type2Scope | ||
15 | |||
16 | val Map<Scope, Set<Scope>> superScopes | ||
17 | val Map<Scope, Set<Scope>> subScopes | ||
18 | |||
19 | public new(PartialInterpretation p) { | ||
20 | partialInterpretation = p | ||
21 | type2Scope = new HashMap | ||
22 | for(scope : p.scopes) { | ||
23 | type2Scope.put(scope.targetTypeInterpretation,scope) | ||
24 | } | ||
25 | |||
26 | superScopes = new HashMap | ||
27 | subScopes = new HashMap | ||
28 | for(scope : p.scopes) { | ||
29 | superScopes.put(scope,new HashSet) | ||
30 | subScopes.put(scope,new HashSet) | ||
31 | } | ||
32 | |||
33 | for(scope : p.scopes) { | ||
34 | val target = scope.targetTypeInterpretation | ||
35 | if(target instanceof PartialComplexTypeInterpretation) { | ||
36 | val supertypeInterpretations = target.supertypeInterpretation | ||
37 | for(supertypeInterpretation : supertypeInterpretations) { | ||
38 | val supertypeScope = type2Scope.get(supertypeInterpretation) | ||
39 | superScopes.get(scope).add(supertypeScope) | ||
40 | subScopes.get(supertypeScope).add(scope) | ||
41 | } | ||
42 | } | ||
43 | } | ||
44 | } | ||
45 | |||
46 | def public propagateAllScopeConstraints() { | ||
47 | var boolean hadChanged | ||
48 | do{ | ||
49 | hadChanged = false | ||
50 | for(superScopeEntry : superScopes.entrySet) { | ||
51 | val sub = superScopeEntry.key | ||
52 | hadChanged = propagateLowerLimitUp(sub,partialInterpretation) || hadChanged | ||
53 | hadChanged = propagateUpperLimitDown(sub,partialInterpretation) || hadChanged | ||
54 | for(sup: superScopeEntry.value) { | ||
55 | hadChanged = propagateLowerLimitUp(sub,sup) || hadChanged | ||
56 | hadChanged = propagateUpperLimitDown(sub,sup) || hadChanged | ||
57 | } | ||
58 | } | ||
59 | } while(hadChanged) | ||
60 | // println('''All constraints are propagated.''') | ||
61 | } | ||
62 | |||
63 | def public propagateAdditionToType(PartialTypeInterpratation t) { | ||
64 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
65 | val targetScope = type2Scope.get(t) | ||
66 | targetScope.removeOne | ||
67 | val sups = superScopes.get(targetScope) | ||
68 | sups.forEach[removeOne] | ||
69 | if(this.partialInterpretation.minNewElements > 0) { | ||
70 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1 | ||
71 | } | ||
72 | if(this.partialInterpretation.maxNewElements > 0) { | ||
73 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 | ||
74 | } else if(this.partialInterpretation.maxNewElements === 0) { | ||
75 | throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') | ||
76 | } | ||
77 | |||
78 | // subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)] | ||
79 | // for(sup: sups) { | ||
80 | // subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)] | ||
81 | // } | ||
82 | // for(scope : type2Scope.values) { | ||
83 | // propagateUpperLimitDown(scope,partialInterpretation) | ||
84 | // } | ||
85 | |||
86 | propagateAllScopeConstraints | ||
87 | |||
88 | // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') | ||
89 | // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') | ||
90 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | ||
91 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
92 | } | ||
93 | |||
94 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | ||
95 | if(subScope.minNewElements>superScope.minNewElements) { | ||
96 | // println(''' | ||
97 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
98 | // superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
99 | // ''') | ||
100 | superScope.minNewElements = subScope.minNewElements | ||
101 | return true | ||
102 | } else { | ||
103 | return false | ||
104 | } | ||
105 | } | ||
106 | |||
107 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | ||
108 | if(superScope.maxNewElements>=0 && (superScope.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) { | ||
109 | // println(''' | ||
110 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
111 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» | ||
112 | // ''') | ||
113 | subScope.maxNewElements = superScope.maxNewElements | ||
114 | return true | ||
115 | } else { | ||
116 | return false | ||
117 | } | ||
118 | } | ||
119 | |||
120 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | ||
121 | if(subScope.minNewElements>p.minNewElements) { | ||
122 | // println(''' | ||
123 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
124 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
125 | // ''') | ||
126 | p.minNewElements = subScope.minNewElements | ||
127 | return true | ||
128 | } else { | ||
129 | return false | ||
130 | } | ||
131 | } | ||
132 | |||
133 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | ||
134 | if(p.maxNewElements>=0 && (p.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) { | ||
135 | // println(''' | ||
136 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
137 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» | ||
138 | // ''') | ||
139 | subScope.maxNewElements = p.maxNewElements | ||
140 | return true | ||
141 | } else { | ||
142 | return false | ||
143 | } | ||
144 | } | ||
145 | private def removeOne(Scope scope) { | ||
146 | if(scope.maxNewElements===0) { | ||
147 | throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') | ||
148 | } else if(scope.maxNewElements>0) { | ||
149 | scope.maxNewElements= scope.maxNewElements-1 | ||
150 | } | ||
151 | if(scope.minNewElements>0) { | ||
152 | scope.minNewElements= scope.minNewElements-1 | ||
153 | } | ||
154 | } | ||
155 | } | ||
156 | \ 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/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend index d11b5960..d6a15c1a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend | |||
@@ -155,6 +155,11 @@ class GenericTypeIndexer extends TypeIndexer { | |||
155 | find supertypeStar(type,definedSupertype); | 155 | find supertypeStar(type,definedSupertype); |
156 | TypeDefinition(definedSupertype); | 156 | TypeDefinition(definedSupertype); |
157 | } | 157 | } |
158 | |||
159 | private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { | ||
160 | Scope.targetTypeInterpretation(scope,typeInterpretation); | ||
161 | Scope.maxNewElements(scope,0); | ||
162 | } | ||
158 | ''' | 163 | ''' |
159 | 164 | ||
160 | public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { | 165 | public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { |
@@ -190,6 +195,7 @@ class GenericTypeIndexer extends TypeIndexer { | |||
190 | Type.name(type,"«type.name»"); | 195 | Type.name(type,"«type.name»"); |
191 | find possibleDynamicType(problem,interpretation,dynamic,element); | 196 | find possibleDynamicType(problem,interpretation,dynamic,element); |
192 | find supertypeStar(dynamic,type); | 197 | find supertypeStar(dynamic,type); |
198 | neg find scopeDisallowsNewElementsFromType(dynamic); | ||
193 | } | 199 | } |
194 | ''' | 200 | ''' |
195 | } | 201 | } |
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 39b6fbc0..329d3658 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 | |||
@@ -24,6 +24,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo | |||
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
25 | 25 | ||
26 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 26 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint | ||
27 | 28 | ||
28 | class RelationDefinitionIndexer { | 29 | class RelationDefinitionIndexer { |
29 | val PatternGenerator base; | 30 | val PatternGenerator base; |
@@ -141,6 +142,35 @@ class RelationDefinitionIndexer { | |||
141 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') | 142 | throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''') |
142 | } | 143 | } |
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 | } | ||
144 | 174 | ||
145 | private dispatch def transformConstraint(Equality equality, Modality modality) { | 175 | private dispatch def transformConstraint(Equality equality, Modality modality) { |
146 | val a = equality.who | 176 | val a = equality.who |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend index 67a886d1..d3af0426 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend | |||
@@ -72,6 +72,15 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ | |||
72 | null | 72 | null |
73 | } | 73 | } |
74 | ''' | 74 | ''' |
75 | private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { | ||
76 | find interpretation(problem,interpretation); | ||
77 | PartialInterpretation.scopes(interpretation,scope); | ||
78 | Scope.targetTypeInterpretation(scope,typeInterpretation); | ||
79 | Scope.maxNewElements(scope,0); | ||
80 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); | ||
81 | Type.name(type,"«type.name»"); | ||
82 | } | ||
83 | |||
75 | /** | 84 | /** |
76 | * An element may be an instance of type "«type.name»". | 85 | * An element may be an instance of type "«type.name»". |
77 | */ | 86 | */ |
@@ -82,6 +91,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ | |||
82 | «FOR inhibitorType : inhibitorTypes» | 91 | «FOR inhibitorType : inhibitorTypes» |
83 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» | 92 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» |
84 | «ENDFOR» | 93 | «ENDFOR» |
94 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); | ||
85 | neg find isPrimitive(element); | 95 | neg find isPrimitive(element); |
86 | } or { | 96 | } or { |
87 | find interpretation(problem,interpretation); | 97 | find interpretation(problem,interpretation); |
@@ -89,6 +99,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ | |||
89 | «FOR inhibitorType : inhibitorTypes» | 99 | «FOR inhibitorType : inhibitorTypes» |
90 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» | 100 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» |
91 | «ENDFOR» | 101 | «ENDFOR» |
102 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); | ||
92 | neg find isPrimitive(element); | 103 | neg find isPrimitive(element); |
93 | } or | 104 | } or |
94 | «ENDIF» | 105 | «ENDIF» |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 0a21d99e..20d24b77 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | |||
@@ -6,6 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | |||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
@@ -31,6 +32,7 @@ class RefinementRuleProvider { | |||
31 | def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 32 | def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> |
32 | createObjectRefinementRules( | 33 | createObjectRefinementRules( |
33 | GeneratedPatterns patterns, | 34 | GeneratedPatterns patterns, |
35 | ScopePropagator scopePropagator, | ||
34 | boolean nameNewElement, | 36 | boolean nameNewElement, |
35 | ModelGenerationStatistics statistics | 37 | ModelGenerationStatistics statistics |
36 | ) | 38 | ) |
@@ -41,7 +43,7 @@ class RefinementRuleProvider { | |||
41 | val inverseRelation = LHSEntry.key.inverseContainment | 43 | val inverseRelation = LHSEntry.key.inverseContainment |
42 | val type = LHSEntry.key.newType | 44 | val type = LHSEntry.key.newType |
43 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> | 45 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> |
44 | val rule = createObjectCreationRule(containmentRelation,inverseRelation,type,lhs,nameNewElement,statistics) | 46 | val rule = createObjectCreationRule(containmentRelation,inverseRelation,type,lhs,nameNewElement,scopePropagator,statistics) |
45 | res.put(LHSEntry.key,rule) | 47 | res.put(LHSEntry.key,rule) |
46 | } | 48 | } |
47 | return res | 49 | return res |
@@ -53,6 +55,7 @@ class RefinementRuleProvider { | |||
53 | Type type, | 55 | Type type, |
54 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, | 56 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, |
55 | boolean nameNewElement, | 57 | boolean nameNewElement, |
58 | ScopePropagator scopePropagator, | ||
56 | ModelGenerationStatistics statistics) | 59 | ModelGenerationStatistics statistics) |
57 | { | 60 | { |
58 | val name = '''addObject_«type.name.canonizeName»« | 61 | val name = '''addObject_«type.name.canonizeName»« |
@@ -80,10 +83,10 @@ class RefinementRuleProvider { | |||
80 | 83 | ||
81 | // Existence | 84 | // Existence |
82 | interpretation.newElements+=newElement | 85 | interpretation.newElements+=newElement |
83 | interpretation.maxNewElements=interpretation.maxNewElements-1 | 86 | /*interpretation.maxNewElements=interpretation.maxNewElements-1 |
84 | if(interpretation.minNewElements > 0) { | 87 | if(interpretation.minNewElements > 0) { |
85 | interpretation.minNewElements=interpretation.minNewElements-1 | 88 | interpretation.minNewElements=interpretation.minNewElements-1 |
86 | } | 89 | }*/ |
87 | 90 | ||
88 | // Types | 91 | // Types |
89 | typeInterpretation.elements += newElement | 92 | typeInterpretation.elements += newElement |
@@ -94,6 +97,10 @@ class RefinementRuleProvider { | |||
94 | // Inverse Containment | 97 | // Inverse Containment |
95 | val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] | 98 | val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] |
96 | inverseRelationInterpretation.relationlinks+=newLink2 | 99 | inverseRelationInterpretation.relationlinks+=newLink2 |
100 | |||
101 | // Scope propagation | ||
102 | scopePropagator.propagateAdditionToType(typeInterpretation) | ||
103 | |||
97 | statistics.addExecutionTime(System.nanoTime-startTime) | 104 | statistics.addExecutionTime(System.nanoTime-startTime) |
98 | ] | 105 | ] |
99 | } else { | 106 | } else { |
@@ -113,10 +120,10 @@ class RefinementRuleProvider { | |||
113 | 120 | ||
114 | // Existence | 121 | // Existence |
115 | interpretation.newElements+=newElement | 122 | interpretation.newElements+=newElement |
116 | interpretation.maxNewElements=interpretation.maxNewElements-1 | 123 | /*interpretation.maxNewElements=interpretation.maxNewElements-1 |
117 | if(interpretation.minNewElements > 0) { | 124 | if(interpretation.minNewElements > 0) { |
118 | interpretation.minNewElements=interpretation.minNewElements-1 | 125 | interpretation.minNewElements=interpretation.minNewElements-1 |
119 | } | 126 | }*/ |
120 | 127 | ||
121 | // Types | 128 | // Types |
122 | typeInterpretation.elements += newElement | 129 | typeInterpretation.elements += newElement |
@@ -124,6 +131,10 @@ class RefinementRuleProvider { | |||
124 | // ContainmentRelation | 131 | // ContainmentRelation |
125 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] | 132 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] |
126 | relationInterpretation.relationlinks+=newLink | 133 | relationInterpretation.relationlinks+=newLink |
134 | |||
135 | // Scope propagation | ||
136 | scopePropagator.propagateAdditionToType(typeInterpretation) | ||
137 | |||
127 | statistics.addExecutionTime(System.nanoTime-startTime) | 138 | statistics.addExecutionTime(System.nanoTime-startTime) |
128 | ] | 139 | ] |
129 | } | 140 | } |
@@ -141,15 +152,19 @@ class RefinementRuleProvider { | |||
141 | 152 | ||
142 | // Existence | 153 | // Existence |
143 | interpretation.newElements+=newElement | 154 | interpretation.newElements+=newElement |
155 | /* | ||
144 | interpretation.maxNewElements=interpretation.maxNewElements-1 | 156 | interpretation.maxNewElements=interpretation.maxNewElements-1 |
145 | if(interpretation.minNewElements > 0) { | 157 | if(interpretation.minNewElements > 0) { |
146 | interpretation.minNewElements=interpretation.minNewElements-1 | 158 | interpretation.minNewElements=interpretation.minNewElements-1 |
147 | } | 159 | }*/ |
148 | 160 | ||
149 | // Types | 161 | // Types |
150 | typeInterpretation.elements += newElement | 162 | typeInterpretation.elements += newElement |
151 | typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] | 163 | typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] |
152 | 164 | ||
165 | // Scope propagation | ||
166 | scopePropagator.propagateAdditionToType(typeInterpretation) | ||
167 | |||
153 | statistics.addExecutionTime(System.nanoTime-startTime) | 168 | statistics.addExecutionTime(System.nanoTime-startTime) |
154 | ] | 169 | ] |
155 | } | 170 | } |