diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
commit | c3a6d4b9cf3657070d180aa65ddbf0459e880329 (patch) | |
tree | 780c4fc61578dcb309af53fb0c164c7627e51676 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend | |
parent | New configuration language parser WIP (diff) | |
parent | Scope unsat benchmarks (diff) | |
download | VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.gz VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.zst VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.zip |
Merge branch 'kris'
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend | 146 |
1 files changed, 83 insertions, 63 deletions
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 f3de4ccc..ac4a0855 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 | |||
@@ -2,78 +2,95 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
13 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 19 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
20 | import java.util.Collection | ||
21 | import java.util.HashMap | ||
14 | import java.util.Map | 22 | import java.util.Map |
23 | import java.util.Set | ||
15 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 24 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
16 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 25 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
17 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 26 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
18 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 28 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
19 | import org.eclipse.xtend.lib.annotations.Data | 29 | import org.eclipse.xtend.lib.annotations.Data |
20 | 30 | ||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
22 | import java.util.Collection | ||
23 | import java.util.Set | ||
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
25 | import java.util.HashMap | ||
26 | 32 | ||
27 | @Data class GeneratedPatterns { | 33 | @Data class GeneratedPatterns { |
28 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries | 34 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries |
29 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries | 35 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries |
30 | public Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> unfinishedContainmentMulticiplicityQueries | 36 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries |
31 | public Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> unfinishedNonContainmentMulticiplicityQueries | 37 | public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery |
32 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 38 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
33 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 39 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
34 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 40 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries |
35 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns | 41 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns |
36 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns | 42 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns |
43 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries | ||
37 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries | 44 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries |
38 | } | 45 | } |
39 | 46 | ||
47 | @Data | ||
48 | class ModalPatternQueries { | ||
49 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery | ||
50 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery | ||
51 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery | ||
52 | } | ||
53 | |||
54 | @Data | ||
55 | class UnifinishedMultiplicityQueries { | ||
56 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicityQuery | ||
57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unrepairableMultiplicityQuery | ||
58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingInverseMultiplicityQuery | ||
59 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQuery | ||
60 | } | ||
61 | |||
40 | class PatternProvider { | 62 | class PatternProvider { |
41 | 63 | ||
42 | val TypeAnalysis typeAnalysis = new TypeAnalysis | 64 | val TypeAnalysis typeAnalysis = new TypeAnalysis |
43 | 65 | ||
44 | public def generateQueries( | 66 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, |
45 | LogicProblem problem, | 67 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, |
46 | PartialInterpretation emptySolution, | 68 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, |
47 | ModelGenerationStatistics statistics, | 69 | Collection<LinearTypeConstraintHint> hints, boolean writeToFile) { |
48 | Set<PQuery> existingQueries, | ||
49 | ReasonerWorkspace workspace, | ||
50 | TypeInferenceMethod typeInferenceMethod, | ||
51 | boolean writeToFile) | ||
52 | { | ||
53 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] | 70 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] |
54 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod) | 71 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) |
55 | val typeAnalysisResult = if(patternGenerator.requiresTypeAnalysis) { | 72 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { |
56 | val startTime = System.nanoTime | 73 | val startTime = System.nanoTime |
57 | val result = typeAnalysis.performTypeAnalysis(problem,emptySolution) | 74 | val result = typeAnalysis.performTypeAnalysis(problem, emptySolution) |
58 | val typeAnalysisTime = System.nanoTime - startTime | 75 | val typeAnalysisTime = System.nanoTime - startTime |
59 | statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime | 76 | statistics.preliminaryTypeAnalisisTime = typeAnalysisTime |
60 | result | 77 | result |
61 | } else { | 78 | } else { |
62 | null | 79 | null |
63 | } | 80 | } |
64 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) | 81 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, |
65 | val baseIndexerFile = patternGeneratorResult.patternText | 82 | typeAnalysisResult, relationConstraints, hints) |
66 | val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName | 83 | if (writeToFile) { |
67 | val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName | 84 | workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText) |
68 | if(writeToFile) { | ||
69 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) | ||
70 | } | 85 | } |
71 | val ParseUtil parseUtil = new ParseUtil | 86 | val ParseUtil parseUtil = new ParseUtil |
72 | val generatedQueries = parseUtil.parse(baseIndexerFile) | 87 | val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) |
73 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,mustUnitPropagationTrace,currentUnitPropagationTrace,generatedQueries); | 88 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, |
89 | patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName, | ||
90 | relationConstraints, generatedQueries) | ||
74 | return runtimeQueries | 91 | return runtimeQueries |
75 | } | 92 | } |
76 | 93 | ||
77 | private def GeneratedPatterns calclulateRuntimeQueries( | 94 | private def GeneratedPatterns calclulateRuntimeQueries( |
78 | PatternGenerator patternGenerator, | 95 | PatternGenerator patternGenerator, |
79 | LogicProblem problem, | 96 | LogicProblem problem, |
@@ -81,31 +98,23 @@ class PatternProvider { | |||
81 | TypeAnalysisResult typeAnalysisResult, | 98 | TypeAnalysisResult typeAnalysisResult, |
82 | HashMap<PConstraint, String> mustUnitPropagationTrace, | 99 | HashMap<PConstraint, String> mustUnitPropagationTrace, |
83 | HashMap<PConstraint, String> currentUnitPropagationTrace, | 100 | HashMap<PConstraint, String> currentUnitPropagationTrace, |
101 | RelationConstraints relationConstraints, | ||
84 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 102 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries |
85 | ) { | 103 | ) { |
86 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 104 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
87 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 105 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] |
88 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 106 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
89 | unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] | 107 | unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] |
90 | 108 | ||
91 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem) | 109 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) |
92 | val unfinishedContainmentMultiplicities = new HashMap | 110 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ |
93 | val unfinishedNonContainmentMultiplicities = new HashMap | 111 | new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries), |
94 | for(entry : unfinishedMultiplicities.entrySet) { | 112 | unrepairableMultiplicityQueryName?.lookup(queries), |
95 | val relation = entry.key | 113 | remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) |
96 | val name = entry.value.key | 114 | ] |
97 | val amount = entry.value.value | 115 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( |
98 | val query = name.lookup(queries) | 116 | queries) |
99 | if(problem.containmentHierarchies.head.containmentRelations.contains(relation)) { | 117 | |
100 | unfinishedContainmentMultiplicities.put(relation,query->amount) | ||
101 | } else { | ||
102 | unfinishedNonContainmentMultiplicities.put(relation,query->amount) | ||
103 | } | ||
104 | } | ||
105 | // val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | ||
106 | // unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] | ||
107 | // | ||
108 | |||
109 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 118 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
110 | refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 119 | refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] |
111 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 120 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
@@ -116,16 +125,27 @@ class PatternProvider { | |||
116 | mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] | 125 | mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] |
117 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 126 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
118 | currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] | 127 | currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] |
128 | |||
129 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | | ||
130 | val indexer = patternGenerator.relationDefinitionIndexer | ||
131 | new ModalPatternQueries( | ||
132 | indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries), | ||
133 | indexer.relationDefinitionName(relationDefinition, Modality.MUST).lookup(queries), | ||
134 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) | ||
135 | ) | ||
136 | ]) | ||
137 | |||
119 | return new GeneratedPatterns( | 138 | return new GeneratedPatterns( |
120 | invalidWFQueries, | 139 | invalidWFQueries, |
121 | unfinishedWFQueries, | 140 | unfinishedWFQueries, |
122 | unfinishedContainmentMultiplicities, | 141 | multiplicityConstraintQueries, |
123 | unfinishedNonContainmentMultiplicities, | 142 | hasElementInContainmentQuery, |
124 | refineObjectsQueries, | 143 | refineObjectsQueries, |
125 | refineTypeQueries, | 144 | refineTypeQueries, |
126 | refineRelationQueries, | 145 | refineRelationQueries, |
127 | mustUnitPropagationPreconditionPatterns, | 146 | mustUnitPropagationPreconditionPatterns, |
128 | currentUnitPropagationPreconditionPatterns, | 147 | currentUnitPropagationPreconditionPatterns, |
148 | modalRelationQueries, | ||
129 | queries.values | 149 | queries.values |
130 | ) | 150 | ) |
131 | } | 151 | } |