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/logic2viatra/patterns/PatternProvider.xtend | |
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/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 | 56 |
1 files changed, 31 insertions, 25 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 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, |