diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-08-06 16:07:16 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-08-06 16:07:16 +0200 |
commit | a620f07468780778bd55dcffc30245def37ece69 (patch) | |
tree | 57189ad9c8bf15211a05a3cd50ee90e90f434557 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver | |
parent | Fix time measurement (diff) | |
download | VIATRA-Generator-a620f07468780778bd55dcffc30245def37ece69.tar.gz VIATRA-Generator-a620f07468780778bd55dcffc30245def37ece69.tar.zst VIATRA-Generator-a620f07468780778bd55dcffc30245def37ece69.zip |
MoDeS3 unit propagation WIP
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
4 files changed, 135 insertions, 105 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 56beacfa..431ae386 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 | |||
@@ -17,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3Polyhe | |||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider |
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
@@ -116,6 +117,7 @@ class ModelGenerationMethodProvider { | |||
116 | boolean calculateObjectCreationCosts, | 117 | boolean calculateObjectCreationCosts, |
117 | ScopePropagatorStrategy scopePropagatorStrategy, | 118 | ScopePropagatorStrategy scopePropagatorStrategy, |
118 | Collection<LinearTypeConstraintHint> hints, | 119 | Collection<LinearTypeConstraintHint> hints, |
120 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, | ||
119 | DocumentationLevel debugLevel | 121 | DocumentationLevel debugLevel |
120 | ) { | 122 | ) { |
121 | val statistics = new ModelGenerationStatistics | 123 | val statistics = new ModelGenerationStatistics |
@@ -126,7 +128,8 @@ class ModelGenerationMethodProvider { | |||
126 | 128 | ||
127 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 129 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
128 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 130 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
129 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) | 131 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, |
132 | unitPropagationPatternGenerators, writeFiles) | ||
130 | 133 | ||
131 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) | 134 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) |
132 | scopePropagator.propagateAllScopeConstraints | 135 | scopePropagator.propagateAllScopeConstraints |
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 80bc3844..a3efcf76 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 | |||
@@ -25,12 +25,13 @@ import java.util.HashMap | |||
25 | import java.util.Map | 25 | import java.util.Map |
26 | import org.eclipse.emf.ecore.EAttribute | 26 | import org.eclipse.emf.ecore.EAttribute |
27 | import org.eclipse.emf.ecore.EReference | 27 | import org.eclipse.emf.ecore.EReference |
28 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
28 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
29 | import org.eclipse.xtend.lib.annotations.Accessors | 30 | import org.eclipse.xtend.lib.annotations.Accessors |
31 | import org.eclipse.xtend.lib.annotations.Data | ||
32 | import org.eclipse.xtend2.lib.StringConcatenationClient | ||
30 | 33 | ||
31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 34 | 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 | ||
35 | @Data class PatternGeneratorResult { | 36 | @Data class PatternGeneratorResult { |
36 | CharSequence patternText | 37 | CharSequence patternText |
@@ -38,6 +39,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | |||
38 | HashMap<PConstraint,String> constraint2CurrentPreconditionName | 39 | HashMap<PConstraint,String> constraint2CurrentPreconditionName |
39 | } | 40 | } |
40 | 41 | ||
42 | interface UnitPropagationPatternGenerator { | ||
43 | def Map<Relation, String> getMustPatterns() | ||
44 | |||
45 | def Map<Relation, String> getMustNotPatterns() | ||
46 | |||
47 | def StringConcatenationClient getAdditionalPatterns(PatternGenerator generator, Map<String, PQuery> fqn2PQuery) | ||
48 | } | ||
49 | |||
41 | class PatternGenerator { | 50 | class PatternGenerator { |
42 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) | 51 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) |
43 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( | 52 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( |
@@ -157,7 +166,8 @@ class PatternGenerator { | |||
157 | Map<String, PQuery> fqn2PQuery, | 166 | Map<String, PQuery> fqn2PQuery, |
158 | TypeAnalysisResult typeAnalysisResult, | 167 | TypeAnalysisResult typeAnalysisResult, |
159 | RelationConstraints constraints, | 168 | RelationConstraints constraints, |
160 | Collection<LinearTypeConstraintHint> hints | 169 | Collection<LinearTypeConstraintHint> hints, |
170 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators | ||
161 | ) { | 171 | ) { |
162 | val first = | 172 | val first = |
163 | ''' | 173 | ''' |
@@ -313,7 +323,7 @@ class PatternGenerator { | |||
313 | ////////// | 323 | ////////// |
314 | // 1.2 Relation Declaration Indexers | 324 | // 1.2 Relation Declaration Indexers |
315 | ////////// | 325 | ////////// |
316 | «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),fqn2PQuery)» | 326 | «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),unitPropagationPatternGenerators,fqn2PQuery)» |
317 | 327 | ||
318 | ////////// | 328 | ////////// |
319 | // 1.3 Relation Definition Indexers | 329 | // 1.3 Relation Definition Indexers |
@@ -367,6 +377,9 @@ class PatternGenerator { | |||
367 | «FOR hint : hints» | 377 | «FOR hint : hints» |
368 | «hint.getAdditionalPatterns(this)» | 378 | «hint.getAdditionalPatterns(this)» |
369 | «ENDFOR» | 379 | «ENDFOR» |
380 | «FOR generator : unitPropagationPatternGenerators» | ||
381 | «generator.getAdditionalPatterns(this, fqn2PQuery)» | ||
382 | «ENDFOR» | ||
370 | 383 | ||
371 | ////////// | 384 | ////////// |
372 | // 6 Unit Propagations | 385 | // 6 Unit Propagations |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index d57705ce..21fd1989 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend | |||
@@ -36,9 +36,9 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
36 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries | 36 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries |
37 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries | 37 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries |
38 | public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery | 38 | public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery |
39 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 39 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
40 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 40 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
41 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 41 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries |
42 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns | 42 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns |
43 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns | 43 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns |
44 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries | 44 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries |
@@ -56,7 +56,7 @@ class ModalPatternQueries { | |||
56 | class UnifinishedMultiplicityQueries { | 56 | class UnifinishedMultiplicityQueries { |
57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery | 57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery |
58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery | 58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery |
59 | 59 | ||
60 | def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() { | 60 | def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() { |
61 | val builder = ImmutableSet.builder | 61 | val builder = ImmutableSet.builder |
62 | if (existingMultiplicityQuery !== null) { | 62 | if (existingMultiplicityQuery !== null) { |
@@ -75,8 +75,9 @@ class PatternProvider { | |||
75 | 75 | ||
76 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, | 76 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, |
77 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, | 77 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, |
78 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, | 78 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, |
79 | Collection<LinearTypeConstraintHint> hints, boolean writeToFile) { | 79 | Collection<LinearTypeConstraintHint> hints, |
80 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, boolean writeToFile) { | ||
80 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] | 81 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] |
81 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) | 82 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) |
82 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { | 83 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { |
@@ -89,15 +90,15 @@ class PatternProvider { | |||
89 | null | 90 | null |
90 | } | 91 | } |
91 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, | 92 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, |
92 | typeAnalysisResult, relationConstraints, hints) | 93 | typeAnalysisResult, relationConstraints, hints, unitPropagationPatternGenerators) |
93 | if (writeToFile) { | 94 | if (writeToFile) { |
94 | workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText) | 95 | workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText) |
95 | } | 96 | } |
96 | val ParseUtil parseUtil = new ParseUtil | 97 | val ParseUtil parseUtil = new ParseUtil |
97 | val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) | 98 | val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) |
98 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, | 99 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, |
99 | patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName, | 100 | patternGeneratorResult.constraint2MustPreconditionName, |
100 | relationConstraints, generatedQueries) | 101 | patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints, generatedQueries) |
101 | return runtimeQueries | 102 | return runtimeQueries |
102 | } | 103 | } |
103 | 104 | ||
@@ -111,12 +112,13 @@ class PatternProvider { | |||
111 | RelationConstraints relationConstraints, | 112 | RelationConstraints relationConstraints, |
112 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 113 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries |
113 | ) { | 114 | ) { |
114 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 115 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries = patternGenerator. |
115 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 116 | invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] |
116 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 117 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries = patternGenerator. |
117 | unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] | 118 | unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] |
118 | 119 | ||
119 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) | 120 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries( |
121 | relationConstraints.multiplicityConstraints) | ||
120 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ | 122 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ |
121 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), | 123 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), |
122 | existingInverseMultiplicityQueryName?.lookup(queries)) | 124 | existingInverseMultiplicityQueryName?.lookup(queries)) |
@@ -124,16 +126,20 @@ class PatternProvider { | |||
124 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( | 126 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( |
125 | queries) | 127 | queries) |
126 | 128 | ||
127 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 129 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectsQueries = patternGenerator. |
128 | refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 130 | typeRefinementGenerator.getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [ |
129 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 131 | it.lookup(queries) |
130 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 132 | ] |
131 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 133 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries = patternGenerator. |
132 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 134 | typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [ |
133 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 135 | it.lookup(queries) |
134 | mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] | 136 | ] |
135 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 137 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries = patternGenerator. |
136 | currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] | 138 | relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] |
139 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace. | ||
140 | mapValues[it.lookup(queries)] | ||
141 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace. | ||
142 | mapValues[it.lookup(queries)] | ||
137 | 143 | ||
138 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | | 144 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | |
139 | val indexer = patternGenerator.relationDefinitionIndexer | 145 | val indexer = patternGenerator.relationDefinitionIndexer |
@@ -143,7 +149,7 @@ class PatternProvider { | |||
143 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) | 149 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) |
144 | ) | 150 | ) |
145 | ]) | 151 | ]) |
146 | 152 | ||
147 | return new GeneratedPatterns( | 153 | return new GeneratedPatterns( |
148 | invalidWFQueries, | 154 | invalidWFQueries, |
149 | unfinishedWFQueries, | 155 | unfinishedWFQueries, |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend index b4403979..29d3eb61 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend | |||
@@ -1,10 +1,13 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import com.google.common.collect.ImmutableSet | ||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | 5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
10 | import java.util.Collection | ||
8 | import java.util.HashMap | 11 | import java.util.HashMap |
9 | import java.util.List | 12 | import java.util.List |
10 | import java.util.Map | 13 | import java.util.Map |
@@ -14,41 +17,40 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
14 | 17 | ||
15 | class RelationDeclarationIndexer { | 18 | class RelationDeclarationIndexer { |
16 | val PatternGenerator base; | 19 | val PatternGenerator base; |
17 | 20 | ||
18 | new(PatternGenerator base) { | 21 | new(PatternGenerator base) { |
19 | this.base = base | 22 | this.base = base |
20 | } | 23 | } |
21 | 24 | ||
22 | def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, Map<String,PQuery> fqn2PQuery) { | 25 | def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, |
26 | Iterable<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, Map<String, PQuery> fqn2PQuery) { | ||
23 | val upperMultiplicities = new HashMap | 27 | val upperMultiplicities = new HashMap |
24 | problem.annotations.filter(UpperMultiplicityAssertion).forEach[ | 28 | problem.annotations.filter(UpperMultiplicityAssertion).forEach [ |
25 | upperMultiplicities.put(it.relation,it.upper) | 29 | upperMultiplicities.put(it.relation, it.upper) |
26 | ] | 30 | ] |
27 | 31 | val mustNotRelations = ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustNotPatterns.entrySet]. | |
32 | groupBy[key].mapValues[ImmutableSet.copyOf(map[value])]) | ||
33 | |||
28 | return ''' | 34 | return ''' |
29 | «FOR relation : relations» | 35 | «FOR relation : relations» |
30 | «IF base.isDerived(relation)» | 36 | «IF base.isDerived(relation)» |
31 | «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» | 37 | «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» |
32 | «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» | 38 | «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» |
33 | «ELSE» | 39 | «ELSE» |
34 | «generateMustRelation(problem,relation)» | 40 | «generateMustRelation(problem, relation)» |
35 | «generateMayRelation(problem,relation,upperMultiplicities,base.getContainments(problem),base.getInverseRelations(problem),fqn2PQuery)» | 41 | «generateMayRelation(problem, relation, upperMultiplicities, base.getContainments(problem), base.getInverseRelations(problem), mustNotRelations.get(relation) ?: emptySet, fqn2PQuery)» |
36 | «ENDIF» | 42 | «ENDIF» |
37 | «ENDFOR» | 43 | «ENDFOR» |
38 | ''' | 44 | ''' |
39 | } | 45 | } |
40 | 46 | ||
41 | def private patternName(RelationDeclaration r, Modality modality) { | 47 | def private patternName(RelationDeclaration r, Modality modality) { |
42 | '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' | 48 | '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' |
43 | } | 49 | } |
44 | 50 | ||
45 | def referRelation( | 51 | def referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable, |
46 | RelationDeclaration referred, | 52 | Modality modality) '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);''' |
47 | String sourceVariable, | 53 | |
48 | String targetVariable, | ||
49 | Modality modality) | ||
50 | '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);''' | ||
51 | |||
52 | def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' | 54 | def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' |
53 | /** | 55 | /** |
54 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 56 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -65,59 +67,64 @@ class RelationDeclarationIndexer { | |||
65 | BinaryElementRelationLink.param2(link,target); | 67 | BinaryElementRelationLink.param2(link,target); |
66 | } | 68 | } |
67 | ''' | 69 | ''' |
70 | |||
68 | def generateMayRelation(LogicProblem problem, RelationDeclaration relation, | 71 | def generateMayRelation(LogicProblem problem, RelationDeclaration relation, |
69 | Map<Relation, Integer> upperMultiplicities, | 72 | Map<Relation, Integer> upperMultiplicities, List<Relation> containments, |
70 | List<Relation> containments, | 73 | HashMap<Relation, Relation> inverseRelations, Collection<String> mustNotRelations, |
71 | HashMap<Relation, Relation> inverseRelations, | 74 | Map<String, PQuery> fqn2PQuery) { |
72 | Map<String,PQuery> fqn2PQuery) | ||
73 | { | ||
74 | return ''' | 75 | return ''' |
75 | /** | 76 | /** |
76 | * Matcher for detecting tuples t where <>«relation.name»(source,target) | 77 | * Matcher for detecting tuples t where <>«relation.name»(source,target) |
77 | */ | 78 | */ |
78 | private pattern «relation.patternName(Modality.MAY)»( | 79 | private pattern «relation.patternName(Modality.MAY)»( |
79 | problem:LogicProblem, interpretation:PartialInterpretation, | 80 | problem:LogicProblem, interpretation:PartialInterpretation, |
80 | source: DefinedElement, target:DefinedElement) | 81 | source: DefinedElement, target:DefinedElement) |
81 | { | 82 | { |
82 | find interpretation(problem,interpretation); | 83 | find interpretation(problem,interpretation); |
83 | // The two endpoint of the link have to exist | 84 | // The two endpoint of the link have to exist |
84 | find mayExist(problem, interpretation, source); | 85 | find mayExist(problem, interpretation, source); |
85 | find mayExist(problem, interpretation, target); | 86 | find mayExist(problem, interpretation, target); |
86 | // Type consistency | 87 | // Type consistency |
87 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» | 88 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» |
88 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» | 89 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» |
89 | «IF upperMultiplicities.containsKey(relation)» | 90 | «IF upperMultiplicities.containsKey(relation)» |
90 | // There are "numberOfExistingReferences" currently existing instances of the reference from the source, | 91 | // There are "numberOfExistingReferences" currently existing instances of the reference from the source, |
91 | // the upper bound of the multiplicity should be considered. | 92 | // the upper bound of the multiplicity should be considered. |
92 | numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» | 93 | numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» |
93 | numberOfExistingReferences != «upperMultiplicities.get(relation)»; | 94 | numberOfExistingReferences != «upperMultiplicities.get(relation)»; |
94 | «ENDIF» | 95 | «ENDIF» |
95 | «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» | 96 | «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» |
96 | // There are "numberOfExistingReferences" currently existing instances of the reference to the target, | 97 | // There are "numberOfExistingReferences" currently existing instances of the reference to the target, |
97 | // the upper bound of the opposite reference multiplicity should be considered. | 98 | // the upper bound of the opposite reference multiplicity should be considered. |
98 | numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» | 99 | numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» |
99 | numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»; | 100 | numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»; |
100 | «ENDIF» | 101 | «ENDIF» |
101 | «IF containments.contains(relation)» | 102 | «IF containments.contains(relation)» |
102 | // The reference is containment, then a new reference cannot be create if: | 103 | // The reference is containment, then a new reference cannot be create if: |
103 | // 1. Multiple parents | 104 | // 1. Multiple parents |
104 | neg «base.containmentIndexer.referMustContaint("_","target")» | 105 | neg «base.containmentIndexer.referMustContaint("_","target")» |
105 | // 2. Circle in the containment hierarchy | 106 | // 2. Circle in the containment hierarchy |
106 | neg «base.containmentIndexer.referTransitiveMustContains("target","source")» | 107 | neg «base.containmentIndexer.referTransitiveMustContains("target","source")» |
107 | «ENDIF» | 108 | «ENDIF» |
108 | «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» | 109 | «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» |
109 | // The eOpposite of the reference is containment, then a referene cannot be created if | 110 | // The eOpposite of the reference is containment, then a referene cannot be created if |
110 | // 1. Multiple parents | 111 | // 1. Multiple parents |
111 | neg «base.containmentIndexer.referMustContaint("source","_")» | 112 | neg «base.containmentIndexer.referMustContaint("source","_")» |
112 | // 2. Circle in the containment hierarchy | 113 | // 2. Circle in the containment hierarchy |
113 | neg «base.containmentIndexer.referTransitiveMustContains("source","target")» | 114 | neg «base.containmentIndexer.referTransitiveMustContains("source","target")» |
114 | «ENDIF» | 115 | «ENDIF» |
115 | } or { | 116 | «IF mustNotRelations.empty» |
116 | «relation.referRelation("source","target",Modality.MUST)» | 117 | // ![] unit propagation relations |
117 | } | 118 | «FOR mustNotRelation : mustNotRelations» |
118 | ''' | 119 | neg find «mustNotRelation»(problem, interpretation, source, target); |
120 | «ENDFOR» | ||
121 | «ENDIF» | ||
122 | } or { | ||
123 | «relation.referRelation("source","target",Modality.MUST)» | ||
124 | } | ||
125 | ''' | ||
119 | } | 126 | } |
120 | 127 | ||
121 | def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' | 128 | def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' |
122 | /** | 129 | /** |
123 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 130 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -129,6 +136,7 @@ class RelationDeclarationIndexer { | |||
129 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» | 136 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» |
130 | } | 137 | } |
131 | ''' | 138 | ''' |
139 | |||
132 | def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' | 140 | def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' |
133 | /** | 141 | /** |
134 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 142 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -140,4 +148,4 @@ class RelationDeclarationIndexer { | |||
140 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» | 148 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» |
141 | } | 149 | } |
142 | ''' | 150 | ''' |
143 | } \ No newline at end of file | 151 | } |