diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
4 files changed, 60 insertions, 23 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 975ace2f..be11ed78 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 | |||
@@ -38,7 +38,8 @@ class ModelGenerationStatistics { | |||
38 | 38 | ||
39 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | 39 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF |
40 | 40 | ||
41 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions | 41 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions |
42 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | ||
42 | 43 | ||
43 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | 44 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns |
44 | } | 45 | } |
@@ -81,7 +82,8 @@ class ModelGenerationMethodProvider { | |||
81 | 82 | ||
82 | val invalidWF = queries.getInvalidWFQueries.values | 83 | val invalidWF = queries.getInvalidWFQueries.values |
83 | 84 | ||
84 | val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns | 85 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns |
86 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | ||
85 | 87 | ||
86 | return new ModelGenerationMethod( | 88 | return new ModelGenerationMethod( |
87 | statistics, | 89 | statistics, |
@@ -90,7 +92,8 @@ class ModelGenerationMethodProvider { | |||
90 | unfinishedMultiplicities, | 92 | unfinishedMultiplicities, |
91 | unfinishedWF, | 93 | unfinishedWF, |
92 | invalidWF, | 94 | invalidWF, |
93 | unitPropagationPreconditions, | 95 | mustUnitPropagationPreconditions, |
96 | currentUnitPropagationPreconditions, | ||
94 | queries.allQueries | 97 | queries.allQueries |
95 | ) | 98 | ) |
96 | } | 99 | } |
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 d5ebe318..219f99e9 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 | |||
@@ -26,6 +26,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
26 | import org.eclipse.xtend.lib.annotations.Accessors | 26 | import org.eclipse.xtend.lib.annotations.Accessors |
27 | 27 | ||
28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
29 | import org.eclipse.xtend.lib.annotations.Data | ||
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
31 | |||
32 | @Data class PatternGeneratorResult { | ||
33 | CharSequence patternText | ||
34 | HashMap<PConstraint,String> constraint2MustPreconditionName | ||
35 | HashMap<PConstraint,String> constraint2CurrentPreconditionName | ||
36 | } | ||
29 | 37 | ||
30 | class PatternGenerator { | 38 | class PatternGenerator { |
31 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) | 39 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) |
@@ -149,7 +157,7 @@ class PatternGenerator { | |||
149 | problem.allTypeReferences.exists[it instanceof StringTypeReference] | 157 | problem.allTypeReferences.exists[it instanceof StringTypeReference] |
150 | } | 158 | } |
151 | 159 | ||
152 | public def transformBaseProperties( | 160 | public def PatternGeneratorResult transformBaseProperties( |
153 | LogicProblem problem, | 161 | LogicProblem problem, |
154 | PartialInterpretation emptySolution, | 162 | PartialInterpretation emptySolution, |
155 | Map<String,PQuery> fqn2PQuery, | 163 | Map<String,PQuery> fqn2PQuery, |
@@ -398,6 +406,6 @@ class PatternGenerator { | |||
398 | ''' | 406 | ''' |
399 | val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) | 407 | val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) |
400 | val second = up.definitions | 408 | val second = up.definitions |
401 | return (first+second) -> up.constraint2PreconditionName | 409 | return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName) |
402 | } | 410 | } |
403 | } | 411 | } |
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 18e3018a..750107f6 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 | |||
@@ -31,7 +31,8 @@ import java.util.HashMap | |||
31 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 31 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
32 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 32 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
33 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 33 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries |
34 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditionPatterns | 34 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns |
35 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns | ||
35 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries | 36 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries |
36 | } | 37 | } |
37 | 38 | ||
@@ -60,14 +61,15 @@ class PatternProvider { | |||
60 | null | 61 | null |
61 | } | 62 | } |
62 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) | 63 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) |
63 | val baseIndexerFile = patternGeneratorResult.key | 64 | val baseIndexerFile = patternGeneratorResult.patternText |
64 | val unitPropagationTrace = patternGeneratorResult.value | 65 | val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName |
66 | val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName | ||
65 | if(writeToFile) { | 67 | if(writeToFile) { |
66 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) | 68 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) |
67 | } | 69 | } |
68 | val ParseUtil parseUtil = new ParseUtil | 70 | val ParseUtil parseUtil = new ParseUtil |
69 | val generatedQueries = parseUtil.parse(baseIndexerFile) | 71 | val generatedQueries = parseUtil.parse(baseIndexerFile) |
70 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); | 72 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,mustUnitPropagationTrace,currentUnitPropagationTrace,generatedQueries); |
71 | return runtimeQueries | 73 | return runtimeQueries |
72 | } | 74 | } |
73 | 75 | ||
@@ -76,7 +78,8 @@ class PatternProvider { | |||
76 | LogicProblem problem, | 78 | LogicProblem problem, |
77 | PartialInterpretation emptySolution, | 79 | PartialInterpretation emptySolution, |
78 | TypeAnalysisResult typeAnalysisResult, | 80 | TypeAnalysisResult typeAnalysisResult, |
79 | HashMap<PConstraint, String> unitPropagationTrace, | 81 | HashMap<PConstraint, String> mustUnitPropagationTrace, |
82 | HashMap<PConstraint, String> currentUnitPropagationTrace, | ||
80 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 83 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries |
81 | ) { | 84 | ) { |
82 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 85 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
@@ -92,7 +95,9 @@ class PatternProvider { | |||
92 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 95 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
93 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 96 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] |
94 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 97 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
95 | unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] | 98 | mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] |
99 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | ||
100 | currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] | ||
96 | return new GeneratedPatterns( | 101 | return new GeneratedPatterns( |
97 | invalidWFQueries, | 102 | invalidWFQueries, |
98 | unfinishedWFQueries, | 103 | unfinishedWFQueries, |
@@ -100,7 +105,8 @@ class PatternProvider { | |||
100 | refineObjectsQueries, | 105 | refineObjectsQueries, |
101 | refineTypeQueries, | 106 | refineTypeQueries, |
102 | refineRelationQueries, | 107 | refineRelationQueries, |
103 | unitPropagationPreconditionPatterns, | 108 | mustUnitPropagationPreconditionPatterns, |
109 | currentUnitPropagationPreconditionPatterns, | ||
104 | queries.values | 110 | queries.values |
105 | ) | 111 | ) |
106 | } | 112 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend index d487db64..91a7a2c2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend | |||
@@ -61,7 +61,8 @@ class UnitPropagationPreconditionGenerationResult { | |||
61 | @Data | 61 | @Data |
62 | class UnitPropagationPreconditionFinalResult { | 62 | class UnitPropagationPreconditionFinalResult { |
63 | CharSequence definitions | 63 | CharSequence definitions |
64 | HashMap<PConstraint,String> constraint2PreconditionName | 64 | HashMap<PConstraint,String> constraint2MustPreconditionName |
65 | HashMap<PConstraint,String> constraint2CurrentPreconditionName | ||
65 | } | 66 | } |
66 | 67 | ||
67 | class UnitPropagationPreconditionGenerator { | 68 | class UnitPropagationPreconditionGenerator { |
@@ -81,25 +82,34 @@ class UnitPropagationPreconditionGenerator { | |||
81 | // Create an empty result | 82 | // Create an empty result |
82 | val res = new UnitPropagationPreconditionGenerationResult | 83 | val res = new UnitPropagationPreconditionGenerationResult |
83 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] | 84 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] |
84 | val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap | 85 | val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap |
86 | val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap | ||
85 | for(wf : wfs) { | 87 | for(wf : wfs) { |
86 | val query = wf.patternPQuery as PQuery | 88 | val query = wf.patternPQuery as PQuery |
87 | val relation = wf.target | 89 | val relation = wf.target |
88 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) | 90 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) |
89 | 91 | ||
90 | for(referredCheck : allReferredChecks) { | 92 | for(referredCheck : allReferredChecks) { |
91 | val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) | 93 | val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) |
92 | if(!mainPropagationNames.containsKey(referredCheck)) { | 94 | val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT) |
93 | mainPropagationNames.put(referredCheck,new LinkedList) | 95 | if(!mainMustPropagationNames.containsKey(referredCheck)) { |
96 | mainMustPropagationNames.put(referredCheck,new LinkedList) | ||
94 | } | 97 | } |
95 | if(propagationPrecondition !== null) { | 98 | if(!mainCurrentPropagationNames.containsKey(referredCheck)) { |
96 | mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) | 99 | mainCurrentPropagationNames.put(referredCheck,new LinkedList) |
100 | } | ||
101 | if(mustPropagationPrecondition !== null) { | ||
102 | mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size) | ||
103 | } | ||
104 | if(currentPropagationPrecondition !== null) { | ||
105 | mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size) | ||
97 | } | 106 | } |
98 | } | 107 | } |
99 | } | 108 | } |
100 | val preconditions = new LinkedList | 109 | val preconditions = new LinkedList |
101 | val constraint2Precondition = new HashMap | 110 | val constraint2MustPrecondition = new HashMap |
102 | for(entry : mainPropagationNames.entrySet) { | 111 | val constraint2CurrentPrecondition = new HashMap |
112 | for(entry : mainMustPropagationNames.entrySet) { | ||
103 | val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; | 113 | val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; |
104 | val def = ''' | 114 | val def = ''' |
105 | pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») | 115 | pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») |
@@ -107,7 +117,17 @@ class UnitPropagationPreconditionGenerator { | |||
107 | { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } | 117 | { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } |
108 | «ENDFOR»''' | 118 | «ENDFOR»''' |
109 | preconditions+=def | 119 | preconditions+=def |
110 | constraint2Precondition.put(entry.key,name) | 120 | constraint2MustPrecondition.put(entry.key,name) |
121 | } | ||
122 | for(entry : mainCurrentPropagationNames.entrySet) { | ||
123 | val name = '''UPCurrentPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; | ||
124 | val def = ''' | ||
125 | pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») | ||
126 | «FOR propagation : entry.value SEPARATOR " or "» | ||
127 | { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } | ||
128 | «ENDFOR»''' | ||
129 | preconditions+=def | ||
130 | constraint2CurrentPrecondition.put(entry.key,name) | ||
111 | } | 131 | } |
112 | 132 | ||
113 | val definitions = ''' | 133 | val definitions = ''' |
@@ -121,7 +141,7 @@ class UnitPropagationPreconditionGenerator { | |||
121 | «predondition» | 141 | «predondition» |
122 | «ENDFOR» | 142 | «ENDFOR» |
123 | ''' | 143 | ''' |
124 | return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition) | 144 | return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition) |
125 | } | 145 | } |
126 | def allReferredConstraints(Relation relation, PQuery query) { | 146 | def allReferredConstraints(Relation relation, PQuery query) { |
127 | val allReferredQueries = query.allReferredQueries | 147 | val allReferredQueries = query.allReferredQueries |