diff options
author | 2020-05-10 22:13:21 +0200 | |
---|---|---|
committer | 2020-05-10 22:13:21 +0200 | |
commit | 5a6eea9bd15597eab77bbcedb4b5116020f0a67d (patch) | |
tree | 6c86f7e5bd3d86fde29d3fee4fb4f912f35057bc /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf | |
parent | Add satellite case study (diff) | |
parent | Merge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff) | |
download | VIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.tar.gz VIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.tar.zst VIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.zip |
Merge branch 'master' of github.com:viatra/VIATRA-Generator
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf')
5 files changed, 147 insertions, 90 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 e7342ff7..975ace2f 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,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | |||
17 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 17 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
18 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 18 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
19 | import org.eclipse.xtend.lib.annotations.Data | 19 | import org.eclipse.xtend.lib.annotations.Data |
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
21 | import java.util.Map | ||
20 | 22 | ||
21 | class ModelGenerationStatistics { | 23 | class ModelGenerationStatistics { |
22 | public var long transformationExecutionTime = 0 | 24 | public var long transformationExecutionTime = 0 |
@@ -36,6 +38,8 @@ class ModelGenerationStatistics { | |||
36 | 38 | ||
37 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | 39 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF |
38 | 40 | ||
41 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions | ||
42 | |||
39 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | 43 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns |
40 | } | 44 | } |
41 | enum TypeInferenceMethod { | 45 | enum TypeInferenceMethod { |
@@ -77,6 +81,8 @@ class ModelGenerationMethodProvider { | |||
77 | 81 | ||
78 | val invalidWF = queries.getInvalidWFQueries.values | 82 | val invalidWF = queries.getInvalidWFQueries.values |
79 | 83 | ||
84 | val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns | ||
85 | |||
80 | return new ModelGenerationMethod( | 86 | return new ModelGenerationMethod( |
81 | statistics, | 87 | statistics, |
82 | objectRefinementRules.values, | 88 | objectRefinementRules.values, |
@@ -84,6 +90,7 @@ class ModelGenerationMethodProvider { | |||
84 | unfinishedMultiplicities, | 90 | unfinishedMultiplicities, |
85 | unfinishedWF, | 91 | unfinishedWF, |
86 | invalidWF, | 92 | invalidWF, |
93 | unitPropagationPreconditions, | ||
87 | queries.allQueries | 94 | queries.allQueries |
88 | ) | 95 | ) |
89 | } | 96 | } |
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 56138ee8..d5ebe318 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 | |||
@@ -155,8 +155,8 @@ class PatternGenerator { | |||
155 | Map<String,PQuery> fqn2PQuery, | 155 | Map<String,PQuery> fqn2PQuery, |
156 | TypeAnalysisResult typeAnalysisResult | 156 | TypeAnalysisResult typeAnalysisResult |
157 | ) { | 157 | ) { |
158 | 158 | val first = | |
159 | return ''' | 159 | ''' |
160 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" | 160 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" |
161 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" | 161 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" |
162 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" | 162 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" |
@@ -395,7 +395,9 @@ class PatternGenerator { | |||
395 | ////////// | 395 | ////////// |
396 | // 5 Unit Propagations | 396 | // 5 Unit Propagations |
397 | ////////// | 397 | ////////// |
398 | «unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)» | ||
399 | ''' | 398 | ''' |
399 | val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) | ||
400 | val second = up.definitions | ||
401 | return (first+second) -> up.constraint2PreconditionName | ||
400 | } | 402 | } |
401 | } | 403 | } |
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 0e13a5e1..18e3018a 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 | |||
@@ -21,6 +21,8 @@ import org.eclipse.xtend.lib.annotations.Data | |||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
22 | import java.util.Collection | 22 | import java.util.Collection |
23 | import java.util.Set | 23 | import java.util.Set |
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
25 | import java.util.HashMap | ||
24 | 26 | ||
25 | @Data class GeneratedPatterns { | 27 | @Data class GeneratedPatterns { |
26 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries | 28 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries |
@@ -29,6 +31,7 @@ import java.util.Set | |||
29 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 31 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
30 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 32 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
31 | 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 | ||
32 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries | 35 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries |
33 | } | 36 | } |
34 | 37 | ||
@@ -56,13 +59,15 @@ class PatternProvider { | |||
56 | } else { | 59 | } else { |
57 | null | 60 | null |
58 | } | 61 | } |
59 | val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) | 62 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) |
63 | val baseIndexerFile = patternGeneratorResult.key | ||
64 | val unitPropagationTrace = patternGeneratorResult.value | ||
60 | if(writeToFile) { | 65 | if(writeToFile) { |
61 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) | 66 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) |
62 | } | 67 | } |
63 | val ParseUtil parseUtil = new ParseUtil | 68 | val ParseUtil parseUtil = new ParseUtil |
64 | val generatedQueries = parseUtil.parse(baseIndexerFile) | 69 | val generatedQueries = parseUtil.parse(baseIndexerFile) |
65 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); | 70 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); |
66 | return runtimeQueries | 71 | return runtimeQueries |
67 | } | 72 | } |
68 | 73 | ||
@@ -71,7 +76,8 @@ class PatternProvider { | |||
71 | LogicProblem problem, | 76 | LogicProblem problem, |
72 | PartialInterpretation emptySolution, | 77 | PartialInterpretation emptySolution, |
73 | TypeAnalysisResult typeAnalysisResult, | 78 | TypeAnalysisResult typeAnalysisResult, |
74 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 79 | HashMap<PConstraint, String> unitPropagationTrace, |
80 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | ||
75 | ) { | 81 | ) { |
76 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 82 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
77 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 83 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] |
@@ -85,6 +91,8 @@ class PatternProvider { | |||
85 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 91 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] |
86 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 92 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
87 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 93 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] |
94 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | ||
95 | unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] | ||
88 | return new GeneratedPatterns( | 96 | return new GeneratedPatterns( |
89 | invalidWFQueries, | 97 | invalidWFQueries, |
90 | unfinishedWFQueries, | 98 | unfinishedWFQueries, |
@@ -92,6 +100,7 @@ class PatternProvider { | |||
92 | refineObjectsQueries, | 100 | refineObjectsQueries, |
93 | refineTypeQueries, | 101 | refineTypeQueries, |
94 | refineRelationQueries, | 102 | refineRelationQueries, |
103 | unitPropagationPreconditionPatterns, | ||
95 | queries.values | 104 | queries.values |
96 | ) | 105 | ) |
97 | } | 106 | } |
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 f726a24f..d487db64 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 | |||
@@ -22,6 +22,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativeP | |||
22 | import java.util.Comparator | 22 | import java.util.Comparator |
23 | import java.util.ArrayList | 23 | import java.util.ArrayList |
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction | 24 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction |
25 | import java.util.LinkedHashSet | ||
25 | 26 | ||
26 | @Data class UnitPropagation { | 27 | @Data class UnitPropagation { |
27 | val PQuery q | 28 | val PQuery q |
@@ -57,6 +58,11 @@ class UnitPropagationPreconditionGenerationResult { | |||
57 | return unitPropagation2PatternName.get(key) !== null | 58 | return unitPropagation2PatternName.get(key) !== null |
58 | } | 59 | } |
59 | } | 60 | } |
61 | @Data | ||
62 | class UnitPropagationPreconditionFinalResult { | ||
63 | CharSequence definitions | ||
64 | HashMap<PConstraint,String> constraint2PreconditionName | ||
65 | } | ||
60 | 66 | ||
61 | class UnitPropagationPreconditionGenerator { | 67 | class UnitPropagationPreconditionGenerator { |
62 | val PatternGenerator base | 68 | val PatternGenerator base |
@@ -75,30 +81,59 @@ class UnitPropagationPreconditionGenerator { | |||
75 | // Create an empty result | 81 | // Create an empty result |
76 | val res = new UnitPropagationPreconditionGenerationResult | 82 | val res = new UnitPropagationPreconditionGenerationResult |
77 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] | 83 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] |
78 | val mainPropagationNames = new LinkedList | 84 | val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap |
79 | for(wf : wfs) { | 85 | for(wf : wfs) { |
80 | val query = wf.patternPQuery as PQuery | 86 | val query = wf.patternPQuery as PQuery |
81 | val relation = wf.target | 87 | val relation = wf.target |
82 | val allReferredChecks = query.allReferredConstraints.filter(ExpressionEvaluation) | 88 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) |
83 | 89 | ||
84 | for(referredCheck : allReferredChecks) { | 90 | for(referredCheck : allReferredChecks) { |
85 | mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) | 91 | val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) |
92 | if(!mainPropagationNames.containsKey(referredCheck)) { | ||
93 | mainPropagationNames.put(referredCheck,new LinkedList) | ||
94 | } | ||
95 | if(propagationPrecondition !== null) { | ||
96 | mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) | ||
97 | } | ||
86 | } | 98 | } |
87 | } | 99 | } |
88 | return ''' | 100 | val preconditions = new LinkedList |
101 | val constraint2Precondition = new HashMap | ||
102 | for(entry : mainPropagationNames.entrySet) { | ||
103 | val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; | ||
104 | val def = ''' | ||
105 | pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») | ||
106 | «FOR propagation : entry.value SEPARATOR " or "» | ||
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»); } | ||
108 | «ENDFOR»''' | ||
109 | preconditions+=def | ||
110 | constraint2Precondition.put(entry.key,name) | ||
111 | } | ||
112 | |||
113 | val definitions = ''' | ||
89 | «FOR def : res.definitions» | 114 | «FOR def : res.definitions» |
90 | «def» | 115 | «def» |
91 | «ENDFOR» | 116 | «ENDFOR» |
92 | 117 | ||
93 | // Main propagations: | 118 | // Collected propagation preconditions: |
94 | «FOR name : mainPropagationNames» | 119 | |
95 | «name» | 120 | «FOR predondition : preconditions» |
121 | «predondition» | ||
96 | «ENDFOR» | 122 | «ENDFOR» |
97 | ''' | 123 | ''' |
124 | return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition) | ||
98 | } | 125 | } |
99 | def allReferredConstraints(PQuery query) { | 126 | def allReferredConstraints(Relation relation, PQuery query) { |
100 | val allReferredQueries = query.allReferredQueries | 127 | val allReferredQueries = query.allReferredQueries |
101 | return (#[query]+allReferredQueries).map[it.disjunctBodies.bodies].flatten.map[constraints].flatten | 128 | val problem = relation.eContainer as LogicProblem |
129 | val constraints = new LinkedHashSet | ||
130 | for(referredQuery: #[query]+allReferredQueries) { | ||
131 | val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target | ||
132 | val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies | ||
133 | constraints.addAll(bodies.map[getConstraints].flatten) | ||
134 | } | ||
135 | |||
136 | return constraints | ||
102 | } | 137 | } |
103 | 138 | ||
104 | def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { | 139 | def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { |
@@ -141,64 +176,67 @@ class UnitPropagationPreconditionGenerator { | |||
141 | // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied | 176 | // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied |
142 | } else { | 177 | } else { |
143 | val positives = body.constraints.filter(PositivePatternCall) | 178 | val positives = body.constraints.filter(PositivePatternCall) |
144 | val positiveRefers = positives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] | 179 | for(positive: positives) { |
145 | for(positiveRefer: positiveRefers) { | 180 | val referredPQuery = positive.referredQuery |
146 | val referredPQuery = positiveRefer.referredQuery | ||
147 | val referredRelation = (relation.eContainer as LogicProblem) | 181 | val referredRelation = (relation.eContainer as LogicProblem) |
148 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | 182 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target |
149 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) | 183 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { |
150 | if(referredName !== null) { | 184 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) |
151 | generatedBodies += ''' | 185 | if(referredName !== null) { |
152 | // Original Constraints | 186 | generatedBodies += ''' |
153 | «FOR constraint : body.constraints.filter[it !== positiveRefer]» | 187 | // Original Constraints |
154 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 188 | «FOR constraint : body.constraints.filter[it !== positive]» |
155 | «ENDFOR» | 189 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
156 | // Propagation for constraint referred indirectly from this pattern through «referredName» | 190 | «ENDFOR» |
157 | find «referredName»(problem, interpretation, | 191 | // Propagation for constraint referred indirectly from this pattern through «referredName» |
158 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positiveRefer.getVariableInTuple(index).canonizeName»«ENDFOR», | 192 | find «referredName»(problem, interpretation, |
159 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | 193 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR», |
160 | ''' | 194 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); |
195 | ''' | ||
196 | } | ||
197 | // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either | ||
161 | } | 198 | } |
162 | // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either | ||
163 | } | 199 | } |
200 | |||
164 | val negatives = body.constraints.filter(NegativePatternCall) | 201 | val negatives = body.constraints.filter(NegativePatternCall) |
165 | val negativeRefers = negatives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] | 202 | for(negative : negatives) { |
166 | for(negativeRefer : negativeRefers) { | 203 | val referredPQuery = negative.referredQuery |
167 | val referredPQuery = negativeRefer.referredQuery | ||
168 | val referredRelation = (relation.eContainer as LogicProblem) | 204 | val referredRelation = (relation.eContainer as LogicProblem) |
169 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target | 205 | .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target |
170 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) | 206 | if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) { |
171 | if(referredName !== null) { | 207 | val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) |
172 | generatedBodies += ''' | 208 | if(referredName !== null) { |
173 | // Original Constraints | 209 | generatedBodies += ''' |
174 | «FOR constraint : body.constraints.filter[it !== negativeRefer]» | 210 | // Original Constraints |
175 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 211 | «FOR constraint : body.constraints.filter[it !== negative]» |
176 | «ENDFOR» | 212 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
177 | // Propagation for constraint referred indirectly from this pattern through «referredName» | 213 | «ENDFOR» |
178 | find «referredName»(problem, interpretation, | 214 | // Propagation for constraint referred indirectly from this pattern through «referredName» |
179 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negativeRefer.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», | 215 | find «referredName»(problem, interpretation, |
180 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); | 216 | «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», |
181 | ''' | 217 | «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); |
182 | } else { | 218 | ''' |
183 | generatedBodies += ''' | 219 | } else { |
184 | // Original Constraints | 220 | generatedBodies += ''' |
185 | «FOR constraint : body.constraints.filter[it !== negativeRefer]» | 221 | // Original Constraints |
186 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» | 222 | «FOR constraint : body.constraints.filter[it !== negative]» |
187 | «ENDFOR» | 223 | «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» |
188 | // Propagation for constraint referred indirectly from this pattern through «referredName», | 224 | «ENDFOR» |
189 | // which was unsatisfiable | 225 | // Propagation for constraint referred indirectly from this pattern through «referredName», |
190 | ''' | 226 | // which was unsatisfiable |
227 | ''' | ||
228 | } | ||
191 | } | 229 | } |
192 | } | 230 | } |
193 | } | 231 | } |
194 | } | 232 | } |
195 | 233 | ||
196 | // Register the result | 234 | // Register the result |
197 | if(generatedBodies.size>=0) { | 235 | if(generatedBodies.empty) { |
198 | res.registerUnsatQuery(q,c,pm,m3) | 236 | res.registerUnsatQuery(q,c,pm,m3) |
199 | } else { | 237 | } else { |
200 | val definition = ''' | 238 | val definition = ''' |
201 | pattern «name»( | 239 | private pattern «name»( |
202 | problem:LogicProblem, interpretation:PartialInterpretation, | 240 | problem:LogicProblem, interpretation:PartialInterpretation, |
203 | «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», | 241 | «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», |
204 | «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») | 242 | «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») |
@@ -229,7 +267,7 @@ class UnitPropagationPreconditionGenerator { | |||
229 | } | 267 | } |
230 | val variablesInOrder = new ArrayList(c.affectedVariables) | 268 | val variablesInOrder = new ArrayList(c.affectedVariables) |
231 | variablesInOrder.toList.sort(comparator) | 269 | variablesInOrder.toList.sort(comparator) |
232 | return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).name»==«canonizeName(variableIndex,m)»;«ENDFOR»''' | 270 | return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»''' |
233 | } | 271 | } |
234 | def dispatch propagateVariables(PConstraint c, PropagationModality m) { | 272 | def dispatch propagateVariables(PConstraint c, PropagationModality m) { |
235 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') | 273 | throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index b4cb9ec7..db0e17b9 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | |||
@@ -90,7 +90,7 @@ class RefinementRuleProvider { | |||
90 | if(containmentRelation !== null) { | 90 | if(containmentRelation !== null) { |
91 | if(inverseRelation!== null) { | 91 | if(inverseRelation!== null) { |
92 | ruleBuilder.action[match | | 92 | ruleBuilder.action[match | |
93 | println(name) | 93 | //println(name) |
94 | val startTime = System.nanoTime | 94 | val startTime = System.nanoTime |
95 | //val problem = match.get(0) as LogicProblem | 95 | //val problem = match.get(0) as LogicProblem |
96 | val interpretation = match.get(1) as PartialInterpretation | 96 | val interpretation = match.get(1) as PartialInterpretation |
@@ -115,7 +115,7 @@ class RefinementRuleProvider { | |||
115 | ] | 115 | ] |
116 | } else { | 116 | } else { |
117 | ruleBuilder.action[match | | 117 | ruleBuilder.action[match | |
118 | println(name) | 118 | //println(name) |
119 | val startTime = System.nanoTime | 119 | val startTime = System.nanoTime |
120 | //val problem = match.get(0) as LogicProblem | 120 | //val problem = match.get(0) as LogicProblem |
121 | val interpretation = match.get(1) as PartialInterpretation | 121 | val interpretation = match.get(1) as PartialInterpretation |
@@ -139,7 +139,7 @@ class RefinementRuleProvider { | |||
139 | } | 139 | } |
140 | } else { | 140 | } else { |
141 | ruleBuilder.action[match | | 141 | ruleBuilder.action[match | |
142 | println(name) | 142 | //println(name) |
143 | val startTime = System.nanoTime | 143 | val startTime = System.nanoTime |
144 | //val problem = match.get(0) as LogicProblem | 144 | //val problem = match.get(0) as LogicProblem |
145 | val interpretation = match.get(1) as PartialInterpretation | 145 | val interpretation = match.get(1) as PartialInterpretation |
@@ -179,36 +179,37 @@ class RefinementRuleProvider { | |||
179 | 179 | ||
180 | if(containmentReferences.contains(relation)) { | 180 | if(containmentReferences.contains(relation)) { |
181 | val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) | 181 | val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) |
182 | 182 | if(!(targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.isIsAbstract) { | |
183 | val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] | 183 | val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] |
184 | if(!inverseAnnotation.empty) { | 184 | if(!inverseAnnotation.empty) { |
185 | val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { | 185 | val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { |
186 | inverseAnnotation.head.inverseB | 186 | inverseAnnotation.head.inverseB |
187 | } else { | ||
188 | inverseAnnotation.head.inverseA | ||
189 | } | ||
190 | val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head | ||
191 | for(var times=0; times<number; times++) { | ||
192 | recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += | ||
193 | new ObjectCreationInterpretationData( | ||
194 | i, | ||
195 | targetTypeInterpretation, | ||
196 | relationInterpretation, | ||
197 | inverseRelationInterpretation, | ||
198 | targetTypeInterpretation.getTypeConstructor | ||
199 | ) | ||
200 | } | ||
201 | |||
187 | } else { | 202 | } else { |
188 | inverseAnnotation.head.inverseA | 203 | for(var times=0; times<number; times++) { |
189 | } | 204 | recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += |
190 | val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head | 205 | new ObjectCreationInterpretationData( |
191 | for(var times=0; times<number; times++) { | 206 | i, |
192 | recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += | 207 | targetTypeInterpretation, |
193 | new ObjectCreationInterpretationData( | 208 | relationInterpretation, |
194 | i, | 209 | null, |
195 | targetTypeInterpretation, | 210 | targetTypeInterpretation.getTypeConstructor |
196 | relationInterpretation, | 211 | ) |
197 | inverseRelationInterpretation, | 212 | } |
198 | targetTypeInterpretation.getTypeConstructor | ||
199 | ) | ||
200 | } | ||
201 | |||
202 | } else { | ||
203 | for(var times=0; times<number; times++) { | ||
204 | recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += | ||
205 | new ObjectCreationInterpretationData( | ||
206 | i, | ||
207 | targetTypeInterpretation, | ||
208 | relationInterpretation, | ||
209 | null, | ||
210 | targetTypeInterpretation.getTypeConstructor | ||
211 | ) | ||
212 | } | 213 | } |
213 | } | 214 | } |
214 | } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) { | 215 | } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) { |