diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
5 files changed, 90 insertions, 71 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 8e061b63..23632d4d 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 | |||
@@ -10,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr | |||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries |
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
@@ -27,7 +29,6 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | |||
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
28 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 30 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
29 | import org.eclipse.xtend.lib.annotations.Data | 31 | import org.eclipse.xtend.lib.annotations.Data |
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
31 | 32 | ||
32 | class ModelGenerationStatistics { | 33 | class ModelGenerationStatistics { |
33 | public var long transformationExecutionTime = 0 | 34 | public var long transformationExecutionTime = 0 |
@@ -139,8 +140,10 @@ class ModelGenerationMethodProvider { | |||
139 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | 140 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, |
140 | PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { | 141 | PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { |
141 | switch (scopePropagatorStrategy) { | 142 | switch (scopePropagatorStrategy) { |
142 | case ScopePropagatorStrategy.BasicTypeHierarchy: | 143 | case ScopePropagatorStrategy.Count: |
143 | new ScopePropagator(emptySolution, statistics) | 144 | new ScopePropagator(emptySolution, statistics) |
145 | case ScopePropagatorStrategy.BasicTypeHierarchy: | ||
146 | new TypeHierarchyScopePropagator(emptySolution, statistics) | ||
144 | ScopePropagatorStrategy.Polyhedral: { | 147 | ScopePropagatorStrategy.Polyhedral: { |
145 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 148 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
146 | val solver = switch (scopePropagatorStrategy.solver) { | 149 | val solver = switch (scopePropagatorStrategy.solver) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index e7e40ab0..7c05e818 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -28,7 +28,7 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | |||
28 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 28 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
30 | 30 | ||
31 | class PolyhedronScopePropagator extends ScopePropagator { | 31 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { |
32 | val Map<Scope, LinearBoundedExpression> scopeBounds | 32 | val Map<Scope, LinearBoundedExpression> scopeBounds |
33 | val LinearBoundedExpression topLevelBounds | 33 | val LinearBoundedExpression topLevelBounds |
34 | val Polyhedron polyhedron | 34 | val Polyhedron polyhedron |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 7be6635c..0bdb202e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | |||
@@ -16,8 +16,8 @@ class ScopePropagator { | |||
16 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation | 16 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation |
17 | val ModelGenerationStatistics statistics | 17 | val ModelGenerationStatistics statistics |
18 | val Map<PartialTypeInterpratation, Scope> type2Scope | 18 | val Map<PartialTypeInterpratation, Scope> type2Scope |
19 | val Map<Scope, Set<Scope>> superScopes | 19 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes |
20 | val Map<Scope, Set<Scope>> subScopes | 20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes |
21 | 21 | ||
22 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { | 22 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { |
23 | partialInterpretation = p | 23 | partialInterpretation = p |
@@ -60,26 +60,14 @@ class ScopePropagator { | |||
60 | } | 60 | } |
61 | } while (changed) | 61 | } while (changed) |
62 | } | 62 | } |
63 | 63 | ||
64 | def propagateAllScopeConstraints() { | 64 | def propagateAllScopeConstraints() { |
65 | statistics.incrementScopePropagationCount() | 65 | statistics.incrementScopePropagationCount() |
66 | doPropagateAllScopeConstraints() | 66 | doPropagateAllScopeConstraints() |
67 | } | 67 | } |
68 | 68 | ||
69 | protected def doPropagateAllScopeConstraints() { | 69 | protected def void doPropagateAllScopeConstraints() { |
70 | var boolean hadChanged | 70 | // Nothing to propagate. |
71 | do { | ||
72 | hadChanged = false | ||
73 | for (superScopeEntry : superScopes.entrySet) { | ||
74 | val sub = superScopeEntry.key | ||
75 | hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged | ||
76 | hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged | ||
77 | for (sup : superScopeEntry.value) { | ||
78 | hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged | ||
79 | hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged | ||
80 | } | ||
81 | } | ||
82 | } while (hadChanged) | ||
83 | } | 71 | } |
84 | 72 | ||
85 | def propagateAdditionToType(PartialTypeInterpratation t) { | 73 | def propagateAdditionToType(PartialTypeInterpratation t) { |
@@ -103,60 +91,11 @@ class ScopePropagator { | |||
103 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | 91 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] |
104 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 92 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
105 | } | 93 | } |
106 | 94 | ||
107 | def void propagateAdditionToRelation(Relation r) { | 95 | def void propagateAdditionToRelation(Relation r) { |
108 | // Nothing to propagate. | 96 | // Nothing to propagate. |
109 | } | 97 | } |
110 | 98 | ||
111 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | ||
112 | if (subScope.minNewElements > superScope.minNewElements) { | ||
113 | superScope.minNewElements = subScope.minNewElements | ||
114 | return true | ||
115 | } else { | ||
116 | return false | ||
117 | } | ||
118 | } | ||
119 | |||
120 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | ||
121 | if (superScope.maxNewElements >= 0 && | ||
122 | (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
123 | // println(''' | ||
124 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
125 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» | ||
126 | // ''') | ||
127 | subScope.maxNewElements = superScope.maxNewElements | ||
128 | return true | ||
129 | } else { | ||
130 | return false | ||
131 | } | ||
132 | } | ||
133 | |||
134 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | ||
135 | if (subScope.minNewElements > p.minNewElements) { | ||
136 | // println(''' | ||
137 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
138 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
139 | // ''') | ||
140 | p.minNewElements = subScope.minNewElements | ||
141 | return true | ||
142 | } else { | ||
143 | return false | ||
144 | } | ||
145 | } | ||
146 | |||
147 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | ||
148 | if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
149 | // println(''' | ||
150 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
151 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» | ||
152 | // ''') | ||
153 | subScope.maxNewElements = p.maxNewElements | ||
154 | return true | ||
155 | } else { | ||
156 | return false | ||
157 | } | ||
158 | } | ||
159 | |||
160 | private def removeOne(Scope scope) { | 99 | private def removeOne(Scope scope) { |
161 | if (scope.maxNewElements === 0) { | 100 | if (scope.maxNewElements === 0) { |
162 | throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') | 101 | throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend index 37e56c9a..b0ed75cb 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend | |||
@@ -16,7 +16,7 @@ enum PolyhedralScopePropagatorSolver { | |||
16 | } | 16 | } |
17 | 17 | ||
18 | abstract class ScopePropagatorStrategy { | 18 | abstract class ScopePropagatorStrategy { |
19 | public static val BasicCount = new Simple("BasicCount") | 19 | public static val Count = new Simple("Count") |
20 | 20 | ||
21 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") | 21 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") |
22 | 22 | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend new file mode 100644 index 00000000..be8ef00a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend | |||
@@ -0,0 +1,77 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
6 | |||
7 | class TypeHierarchyScopePropagator extends ScopePropagator { | ||
8 | |||
9 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { | ||
10 | super(p, statistics) | ||
11 | } | ||
12 | |||
13 | protected override doPropagateAllScopeConstraints() { | ||
14 | var boolean hadChanged | ||
15 | do { | ||
16 | hadChanged = false | ||
17 | for (superScopeEntry : superScopes.entrySet) { | ||
18 | val sub = superScopeEntry.key | ||
19 | hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged | ||
20 | hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged | ||
21 | for (sup : superScopeEntry.value) { | ||
22 | hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged | ||
23 | hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged | ||
24 | } | ||
25 | } | ||
26 | } while (hadChanged) | ||
27 | } | ||
28 | |||
29 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | ||
30 | if (subScope.minNewElements > superScope.minNewElements) { | ||
31 | superScope.minNewElements = subScope.minNewElements | ||
32 | return true | ||
33 | } else { | ||
34 | return false | ||
35 | } | ||
36 | } | ||
37 | |||
38 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | ||
39 | if (superScope.maxNewElements >= 0 && | ||
40 | (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
41 | // println(''' | ||
42 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
43 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» | ||
44 | // ''') | ||
45 | subScope.maxNewElements = superScope.maxNewElements | ||
46 | return true | ||
47 | } else { | ||
48 | return false | ||
49 | } | ||
50 | } | ||
51 | |||
52 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | ||
53 | if (subScope.minNewElements > p.minNewElements) { | ||
54 | // println(''' | ||
55 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
56 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
57 | // ''') | ||
58 | p.minNewElements = subScope.minNewElements | ||
59 | return true | ||
60 | } else { | ||
61 | return false | ||
62 | } | ||
63 | } | ||
64 | |||
65 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | ||
66 | if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
67 | // println(''' | ||
68 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
69 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» | ||
70 | // ''') | ||
71 | subScope.maxNewElements = p.maxNewElements | ||
72 | return true | ||
73 | } else { | ||
74 | return false | ||
75 | } | ||
76 | } | ||
77 | } | ||