aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend16
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java8
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend37
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend11
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend14
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend36
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend275
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend116
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend152
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend63
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend183
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend302
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend22
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend480
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend29
18 files changed, 1381 insertions, 373 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 e45ec1c8..6fbbc779 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
@@ -27,6 +27,7 @@ import java.util.Set
27import org.eclipse.viatra.query.runtime.api.IPatternMatch 27import org.eclipse.viatra.query.runtime.api.IPatternMatch
28import org.eclipse.viatra.query.runtime.api.IQuerySpecification 28import org.eclipse.viatra.query.runtime.api.IQuerySpecification
29import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 29import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
30import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
30import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 31import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
31import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule 32import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
32import org.eclipse.xtend.lib.annotations.Data 33import org.eclipse.xtend.lib.annotations.Data
@@ -83,6 +84,9 @@ class ModelGenerationStatistics {
83 84
84 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF 85 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
85 86
87 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions
88 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions
89
86 Map<String, ModalPatternQueries> modalRelationQueries 90 Map<String, ModalPatternQueries> modalRelationQueries
87 91
88 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns 92 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
@@ -120,12 +124,13 @@ class ModelGenerationMethodProvider {
120 workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) 124 workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles)
121 val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) 125 val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics)
122 scopePropagator.propagateAllScopeConstraints 126 scopePropagator.propagateAllScopeConstraints
123 val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, 127 val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution,
124 nameNewElements, statistics) 128 queries, scopePropagator, nameNewElements, statistics)
125 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, 129 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator,
126 statistics) 130 statistics)
127 131
128 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) 132 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries)
133
129 val unfinishedWF = queries.getUnfinishedWFQueries.values 134 val unfinishedWF = queries.getUnfinishedWFQueries.values
130 135
131 val modalRelationQueriesBuilder = ImmutableMap.builder 136 val modalRelationQueriesBuilder = ImmutableMap.builder
@@ -138,6 +143,9 @@ class ModelGenerationMethodProvider {
138 val modalRelationQueries = modalRelationQueriesBuilder.build 143 val modalRelationQueries = modalRelationQueriesBuilder.build
139 144
140 val invalidWF = queries.getInvalidWFQueries.values 145 val invalidWF = queries.getInvalidWFQueries.values
146
147 val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
148 val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
141 149
142 return new ModelGenerationMethod( 150 return new ModelGenerationMethod(
143 statistics, 151 statistics,
@@ -146,6 +154,8 @@ class ModelGenerationMethodProvider {
146 unfinishedMultiplicities, 154 unfinishedMultiplicities,
147 unfinishedWF, 155 unfinishedWF,
148 invalidWF, 156 invalidWF,
157 mustUnitPropagationPreconditions,
158 currentUnitPropagationPreconditions,
149 modalRelationQueries, 159 modalRelationQueries,
150 queries.allQueries 160 queries.allQueries
151 ) 161 )
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java
new file mode 100644
index 00000000..2288ad7e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/PropagationModality.java
@@ -0,0 +1,8 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra;
2
3public enum PropagationModality {
4 /**The value was originally ? and set to 1 */
5 UP,
6 /**The value was originally ? and set to 0 */
7 DOWN
8}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
index 86a59aa1..034420d6 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend
@@ -7,26 +7,39 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
7import org.eclipse.viatra.query.runtime.emf.EMFScope 7import org.eclipse.viatra.query.runtime.emf.EMFScope
8 8
9class MultiplicityGoalConstraintCalculator { 9class MultiplicityGoalConstraintCalculator {
10 val String targetRelationName; 10 val String targetRelationName
11 val IQuerySpecification<?> querySpecification; 11 val IQuerySpecification<?> querySpecification
12 var ViatraQueryMatcher<?> matcher; 12 var ViatraQueryMatcher<?> matcher
13 val int minValue
14 val boolean containment
15 val int cost
13 16
14 new(String targetRelationName, IQuerySpecification<?> querySpecification) { 17 public new(String targetRelationName, IQuerySpecification<?> querySpecification, int minValue, boolean containment, int cost) {
15 this.targetRelationName = targetRelationName 18 this.targetRelationName = targetRelationName
16 this.querySpecification = querySpecification 19 this.querySpecification = querySpecification
17 this.matcher = null 20 this.matcher = null
21 this.minValue = minValue
22 this.containment = containment
23 this.cost = cost
18 } 24 }
19 25
20 new(MultiplicityGoalConstraintCalculator other) { 26 new(MultiplicityGoalConstraintCalculator other) {
21 this.targetRelationName = other.targetRelationName 27 this.targetRelationName = other.targetRelationName
22 this.querySpecification = other.querySpecification 28 this.querySpecification = other.querySpecification
23 this.matcher = null 29 this.matcher = null
30 this.minValue = other.minValue
31 this.containment = other.containment
32 this.cost = other.cost
24 } 33 }
25 34
26 def getName() { 35 def getName() {
27 targetRelationName 36 targetRelationName
28 } 37 }
29 38
39 def isContainment() {
40 return containment
41 }
42
30 def init(Notifier notifier) { 43 def init(Notifier notifier) {
31 val engine = ViatraQueryEngine.on(new EMFScope(notifier)) 44 val engine = ViatraQueryEngine.on(new EMFScope(notifier))
32 matcher = querySpecification.getMatcher(engine) 45 matcher = querySpecification.getMatcher(engine)
@@ -36,11 +49,17 @@ class MultiplicityGoalConstraintCalculator {
36 var res = 0 49 var res = 0
37 val allMatches = this.matcher.allMatches 50 val allMatches = this.matcher.allMatches
38 for(match : allMatches) { 51 for(match : allMatches) {
39 //println(targetRelationName+ " missing multiplicity: "+match.get(3)) 52 val existingMultiplicity = match.get(4) as Integer
40 val missingMultiplicity = match.get(2) as Integer 53 if(existingMultiplicity < this.minValue) {
41 res += missingMultiplicity 54 val missingMultiplicity = this.minValue-existingMultiplicity
55 res += missingMultiplicity
56 }
57// if(missingMultiplicity!=0) {
58// println(targetRelationName+ " missing multiplicity: "+missingMultiplicity)
59// }
42 } 60 }
43 //println(targetRelationName+ " all missing multiplicities: "+res) 61// if(res>0)
44 return res 62// println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost)
63 return res*cost
45 } 64 }
46} 65}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
index 51dba244..120fb18a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
@@ -187,16 +187,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator {
187 if (bounds.upperBound !== null && bounds.upperBound < 0) { 187 if (bounds.upperBound !== null && bounds.upperBound < 0) {
188 throw new IllegalArgumentException("Negative upper bound: " + bounds) 188 throw new IllegalArgumentException("Negative upper bound: " + bounds)
189 } 189 }
190 } 190 }
191
192 private def setScopesInvalid() {
193 partialInterpretation.minNewElements = Integer.MAX_VALUE
194 partialInterpretation.maxNewElements = 0
195 for (scope : partialInterpretation.scopes) {
196 scope.minNewElements = Integer.MAX_VALUE
197 scope.maxNewElements = 0
198 }
199 }
200 191
201 private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, 192 private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher,
202 PartialInterpretation p) { 193 PartialInterpretation p) {
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
index 2376fb38..8f3a5bb0 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -79,7 +79,7 @@ class ScopePropagator {
79 // Nothing to propagate. 79 // Nothing to propagate.
80 } 80 }
81 81
82 def propagateAdditionToType(PartialTypeInterpratation t) { 82 def decrementTypeScope(PartialTypeInterpratation t) {
83// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') 83// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
84 val targetScope = type2Scope.get(t) 84 val targetScope = type2Scope.get(t)
85 if (targetScope !== null) { 85 if (targetScope !== null) {
@@ -96,15 +96,23 @@ class ScopePropagator {
96 if (this.partialInterpretation.maxNewElements > 0) { 96 if (this.partialInterpretation.maxNewElements > 0) {
97 this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 97 this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1
98 } else if (this.partialInterpretation.maxNewElements === 0) { 98 } else if (this.partialInterpretation.maxNewElements === 0) {
99 throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') 99 setScopesInvalid()
100 } 100 }
101 propagateAllScopeConstraints
102 101
103// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') 102// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
104// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') 103// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
105// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] 104// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
106// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') 105// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
107 } 106 }
107
108 protected def setScopesInvalid() {
109 partialInterpretation.minNewElements = Integer.MAX_VALUE
110 partialInterpretation.maxNewElements = 0
111 for (scope : partialInterpretation.scopes) {
112 scope.minNewElements = Integer.MAX_VALUE
113 scope.maxNewElements = 0
114 }
115 }
108 116
109 def void propagateAdditionToRelation(Relation r) { 117 def void propagateAdditionToRelation(Relation r) {
110 // Nothing to propagate. 118 // Nothing to propagate.
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
index e511a961..fd4374f5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
@@ -11,7 +11,5 @@ import org.eclipse.xtend.lib.annotations.Data
11class CanonisedFormulae { 11class CanonisedFormulae {
12 CharSequence viatraCode 12 CharSequence viatraCode
13 Map<Assertion,String> assertion2ConstraintPattern 13 Map<Assertion,String> assertion2ConstraintPattern
14 Map<ConstantDefinition,String> constant2ValuePattern
15 Map<RelationDefinition,String> relation2ValuePattern 14 Map<RelationDefinition,String> relation2ValuePattern
16 Map<FunctionDefinition,String> function2ValuePattern
17} \ No newline at end of file 15} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
index 0af0b36a..182f3a3a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
@@ -5,17 +5,35 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
7import java.util.List 7import java.util.List
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
8 11
9/** 12/**
10 * Translates a set of assertions and definitions to viatra patterns. 13 * Translates a Terms into format
14 * <P(x1,...,xn)> := Bodies(x1,...,xn)
15 * <Bodies(x1,...,xn)> := <Body(x1,...,xn)> | <Body(x1,...,xn)> or <Bodies(x1,...,xn)>
16 * <Body(x1,...,xn)> := Exists y1,...,ym : <Constraints(x1,...,xn,y1,....,ym)>
17 * <Constraints(x1,...,xn)> := Constraint(x1,...xn) | Constraint(x1,...,xn) and <Constraints(x1,...,xn)>
11 */ 18 */
12class FormulaCanoniser { 19class FormulaCanoniser {
13 def canonise( 20// def canonise(
14 List<Assertion> assertions, 21// List<Assertion> assertions,
15 List<RelationDefinition> relations, 22// List<RelationDefinition> relations)
16 List<ConstantDefinition> constants, 23// {
17 List<FunctionDefinition> functions) 24//
18 { 25// }
19 26//
20 } 27//
28// def canoniseToConstraintBlock(Term predicate, List<Variable> variables) {
29// val
30// }
31//
32// def freeVariables(Term t) {
33// val subterms = #[t]+t.eAllContents.toList
34// val variables = subterms.filter(Variable).toSet
35// val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable]
36// val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)]
37// return freeVariables.map
38// }
21} \ No newline at end of file 39} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
new file mode 100644
index 00000000..dd5cade1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
@@ -0,0 +1,275 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
5import org.eclipse.emf.ecore.EAttribute
6import org.eclipse.emf.ecore.EEnumLiteral
7import org.eclipse.emf.ecore.EReference
8import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
9import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
10import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
11import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
12import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
13import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
14import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
15import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
16import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
23import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping
24import java.util.List
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
31import java.util.Map
32
33class PConstraintTransformer {
34 val extension RelationDefinitionIndexer relationDefinitionIndexer;
35 val expressionExtractor = new XExpressionExtractor
36 val expressionGenerator = new PExpressionGenerator
37
38 new(RelationDefinitionIndexer relationDefinitionIndexer) {
39 this.relationDefinitionIndexer = relationDefinitionIndexer
40 }
41
42 dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
43 val touple = constraint.variablesTuple
44 if(touple.size == 1) {
45 val inputKey = constraint.equivalentJudgement.inputKey
46 if(inputKey instanceof EClassTransitiveInstancesKey) {
47 return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
48 constraint.getVariableInTuple(0).canonizeName)
49 } else if(inputKey instanceof EDataTypeInSlotsKey){
50 return '''// type constraint is enforced by construction'''
51 }
52
53 } else if(touple.size == 2){
54 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
55 if(key instanceof EReference) {
56 return base.referRelationByName(
57 key,
58 constraint.getVariableInTuple(0).canonizeName,
59 constraint.getVariableInTuple(1).canonizeName,
60 modality.toMustMay)
61 } else if (key instanceof EAttribute) {
62 return base.referAttributeByName(key,
63 constraint.getVariableInTuple(0).canonizeName,
64 constraint.getVariableInTuple(1).canonizeName,
65 modality.toMustMay)
66 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
67 } else {
68 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
69 }
70 }
71 dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
72 val touple = constraint.variablesTuple
73 if(touple.size == 1) {
74 val inputKey = constraint.equivalentJudgement.inputKey
75 if(inputKey instanceof EClassTransitiveInstancesKey) {
76 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
77 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
78 } else if(inputKey instanceof EDataTypeInSlotsKey){
79 return '''// type constraint is enforced by construction'''
80 }
81
82 } else if(touple.size == 2){
83 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
84 if(key instanceof EReference) {
85 return base.referRelationByName(
86 key,
87 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
88 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
89 modality.toMustMay)
90 } else if (key instanceof EAttribute) {
91 return base.referAttributeByName(key,
92 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
93 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
94 modality.toMustMay)
95 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
96 } else {
97 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
98 }
99 }
100
101 dispatch def transformConstraint(Equality equality, Modality modality, List<VariableMapping> variableMapping) {
102 val a = equality.who
103 val b = equality.withWhom
104 transformEquality(modality.toMustMay, a, b)
105 }
106
107 private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
108 if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
109 else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
110 }
111
112 dispatch def transformConstraint(Inequality inequality, Modality modality, List<VariableMapping> variableMapping) {
113 val a = inequality.who
114 val b = inequality.withWhom
115 if(modality.isCurrent) {
116 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
117 } else if(modality.isMust) {
118 return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
119 } else { // modality.isMay
120 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
121 }
122 }
123
124 dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
125 val params = (0..<pcall.actualParametersTuple.size).map[index |
126 val variable = pcall.actualParametersTuple.get(index) as PVariable
127 return variable.canonizeName
128 ]
129 return referPattern(pcall.referredQuery,params,modality.dual,false,false)
130 }
131
132 dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
133 val params = (0..<pcall.variablesTuple.size).map[index |
134 val variable = pcall.variablesTuple.get(index) as PVariable
135 return variable.canonizeName
136 ]
137 return referPattern(pcall.referredQuery,params,modality,true,false)
138 }
139 dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> variableMapping) {
140 val params = (0..1).map[index |
141 val variable = pcall.getVariableInTuple(index) as PVariable
142 return variable.canonizeName
143 ]
144 return referPattern(pcall.referredQuery,params,modality,true,true)
145 }
146 dispatch def transformConstraint(ExportedParameter e, Modality modality, List<VariableMapping> variableMapping) {
147 val v1 = '''var_«e.parameterName»'''
148 val v2 = e.parameterVariable.canonizeName
149 if(v1.compareTo(v2) == 0) {
150 return '''// «v1» exported'''
151 } else {
152 return '''«v1» == «v2»;'''
153 }
154 }
155 dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> variableMapping) {
156 val target = c.supplierKey
157
158 var String targetString;
159 var String additionalDefinition;
160 if(target instanceof EEnumLiteral) {
161 targetString = '''const_«target.name»_«target.EEnum.name»'''
162 additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
163 } else if(target instanceof Integer) {
164 targetString = '''const_«target»_Integer'''
165 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);'''
166 } else if(target instanceof Boolean) {
167 targetString = '''const_«target»_Boolean'''
168 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);'''
169 } else if(target instanceof String) {
170 targetString = '''const_«target»_String'''
171 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");'''
172 } else if(target instanceof Double) {
173 targetString = '''const_«target»_Real'''
174 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
175 } else if(target instanceof Float) {
176 targetString = '''const_«target»_Real'''
177 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
178 } else {
179 throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
180 }
181
182 val source = c.variablesTuple
183 var String sourceName
184 if(source.size == 1)
185 sourceName = (source.get(0) as PVariable).canonizeName
186 else throw new UnsupportedOperationException("unknown source")
187 return '''«sourceName» == «targetString»;«additionalDefinition»''';
188 }
189
190 protected def valueVariable(PVariable v) {
191 "value_"+v.canonizeName
192 }
193 protected def valueSetted(PVariable v) {
194 "setted_"+v.canonizeName
195 }
196 def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) {
197 val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference
198 if(m.isMay) {
199 '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)»
200««« check(!«v.valueSetted»||«v.valueVariable»==«target»));
201'''
202 } else { // Must or current
203 '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpressionByRef(typeReference,v,target)»'''
204 }
205 }
206
207 private def hasValueExpression(List<VariableMapping> variableMapping, PVariable v, String target) {
208 val mapping = variableMapping.filter[
209 val v2 = (it.sourcePVariable as PVariable)
210 v2 === v
211 ].head
212 val range = mapping.targetLogicVariable.range
213 hasValueExpressionByRef(
214 range,
215 v,
216 target
217 )
218 }
219 private def dispatch hasValueExpressionByRef(BoolTypeReference typeReference, PVariable v, String target) '''BooleanElement.value(«v.canonizeName»,«target»);'''
220 private def dispatch hasValueExpressionByRef(IntTypeReference typeReference, PVariable v, String target) '''IntegerElement.value(«v.canonizeName»,«target»);'''
221 private def dispatch hasValueExpressionByRef(RealTypeReference typeReference, PVariable v, String target) '''RealElement.value(«v.canonizeName»,«target»);'''
222 private def dispatch hasValueExpressionByRef(StringTypeReference typeReference, PVariable v, String target) '''StringElement.value(«v.canonizeName»,«target»);'''
223 private def dispatch hasValueExpressionByRef(TypeReference typeReference, PVariable v, String target) {
224 throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''')
225 }
226
227 dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List<VariableMapping> variableMapping) {
228 if(e.outputVariable!==null) {
229 throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')
230 } else {
231 val expression = expressionExtractor.extractExpression(e.evaluator)
232 val Map<PVariable, PrimitiveTypeReference> variable2Type = e.affectedVariables.toInvertedMap[v|variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference]
233 if(modality.isMay) {
234 return '''
235 «FOR variable: e.affectedVariables»
236 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
237 «ENDFOR»
238««« check(
239««« «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»
240««« «IF variable2Type.values.filter(RealTypeReference).empty»
241««« ||
242««« («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»)
243««« «ENDIF»
244««« );
245 '''
246 } else { // Must or Current
247 return '''
248 «FOR variable: e.affectedVariables»
249 PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
250 «ENDFOR»
251««« «IF variable2Type.values.filter(RealTypeReference).empty»
252««« check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»);
253««« «ENDIF»
254 '''
255 }
256 }
257 }
258
259 dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) {
260 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
261 }
262
263 dispatch def transformConstraintUnset(ExpressionEvaluation e, List<VariableMapping> variableMapping) {
264 return '''
265 «FOR variable: e.affectedVariables»
266 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
267 «ENDFOR»
268««« check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»);
269 '''
270 }
271
272 dispatch def transformConstraintUnset(PConstraint c, List<VariableMapping> variableMapping) {
273 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
274 }
275} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
new file mode 100644
index 00000000..62ff92b2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
@@ -0,0 +1,116 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import java.util.Map
4import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
5import org.eclipse.xtext.xbase.XBinaryOperation
6import org.eclipse.xtext.xbase.XExpression
7import org.eclipse.xtext.xbase.XFeatureCall
8import org.eclipse.xtext.xbase.XMemberFeatureCall
9import org.eclipse.xtext.xbase.XNumberLiteral
10import org.eclipse.xtext.xbase.XUnaryOperation
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
13
14class PExpressionGenerator {
15 static val N_Base = "org.eclipse.xtext.xbase.lib."
16
17 static val N_PLUS1 = "operator_plus"
18 static val N_MINUS1 = "operator_minus"
19
20 static val N_MINUS2 = "operator_minus"
21 static val N_PLUS2 = "operator_plus"
22 static val N_POWER = "operator_power"
23 static val N_MULTIPLY = "operator_multiply"
24 static val N_DIVIDE = "operator_divide"
25 static val N_MODULO = "operator_modulo"
26 static val N_LESSTHAN = "operator_lessThan"
27 static val N_LESSEQUALSTHAN = "operator_lessEqualsThan"
28 static val N_GREATERTHAN = "operator_greaterThan"
29 static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan"
30 static val N_EQUALS = "operator_equals"
31 static val N_NOTEQUALS = "operator_notEquals"
32 static val N_EQUALS3 = "operator_tripleEquals"
33 static val N_NOTEQUALS3 = "operator_tripleNotEquals"
34
35 protected def isN(String name, String s) {
36 val res = name.startsWith(N_Base) && name.endsWith(s)
37 //println('''[«res»] «name» ?= «N_Base»*«s»''')
38 return res
39 }
40
41 static val N_POWER2 = "java.lang.Math.pow"
42
43 def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
44 val left = e.leftOperand.translateExpression(valueName,variable2Type)
45 val right = e.rightOperand.translateExpression(valueName,variable2Type)
46 val feature = e.feature.qualifiedName
47 if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''}
48 else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' }
49 else if(feature.isN(N_POWER)) { return '''(«left»^«right»)''' }
50 else if(feature.isN(N_MULTIPLY)) { return '''(«left»*«right»)''' }
51 else if(feature.isN(N_DIVIDE)) { return '''(«left»/«right»)''' }
52 else if(feature.isN(N_MODULO)) { return '''(«left»%«right»)''' }
53 else if(feature.isN(N_LESSTHAN)) { return '''(«left»<«right»)''' }
54 else if(feature.isN(N_LESSEQUALSTHAN)) { return '''(«left»<=«right»)''' }
55 else if(feature.isN(N_GREATERTHAN)) { return '''(«left»>«right»)''' }
56 else if(feature.isN(N_GREATEREQUALTHAN)) { return '''(«left»>=«right»)''' }
57 else if(feature.isN(N_EQUALS)) { return '''(«left»==«right»)''' }
58 else if(feature.isN(N_NOTEQUALS)) { return '''(«left»!=«right»)''' }
59 else if(feature.isN(N_EQUALS3)) { return '''(«left»===«right»)''' }
60 else if(feature.isN(N_NOTEQUALS3)) { return '''(«left»!==«right»)''' }
61 else {
62 println("-> " + e.feature+","+e.class)
63 println("-> " + e.leftOperand)
64 println("-> " + e.rightOperand)
65 println("-> " + e.feature.qualifiedName)
66 throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''')
67 }
68 }
69
70 def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
71 val operand = e.operand.translateExpression(valueName,variable2Type)
72 val feature = e.feature.qualifiedName
73 if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''}
74 else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''}
75 else{
76 println("-> " + e.feature+","+e.class)
77 println("-> " + e.operand)
78 println("-> " + e.feature.qualifiedName)
79 throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''')
80 }
81 }
82
83 def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
84 val transformedArguments = e.actualArguments.map[translateExpression(valueName,variable2Type)]
85 val feature = e.feature.qualifiedName
86 if(feature == N_POWER2) {
87 return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)'''
88 }else {
89 println(e.feature+","+e.class)
90 println(e.actualArguments.join(", "))
91 println(e.feature.qualifiedName)
92 throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''')
93 }
94 }
95
96 def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
97 val featureName = e.feature.qualifiedName
98 val type = variable2Type.entrySet.filter[it.key.name===featureName].head.value
99 val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head
100 if(entryWithName !== null) {
101 if(type instanceof RealTypeReference) {
102 return '''(«entryWithName.value».doubleValue)'''
103 } else {
104 return entryWithName.value
105 }
106 } else {
107 throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
108 }
109 }
110
111 def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) '''«l.value»'''
112
113 def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
114 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
115 }
116} \ No newline at end of file
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 5c35fb54..f3125b80 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
@@ -29,6 +29,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
29import org.eclipse.xtend.lib.annotations.Accessors 29import org.eclipse.xtend.lib.annotations.Accessors
30 30
31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
32import org.eclipse.xtend.lib.annotations.Data
33import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
34
35@Data class PatternGeneratorResult {
36 CharSequence patternText
37 HashMap<PConstraint,String> constraint2MustPreconditionName
38 HashMap<PConstraint,String> constraint2CurrentPreconditionName
39}
32 40
33class PatternGenerator { 41class PatternGenerator {
34 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) 42 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this)
@@ -39,12 +47,12 @@ class PatternGenerator {
39 @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) 47 @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this)
40 @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) 48 @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this)
41 @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer 49 @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer
42 @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator // = new RefinementGenerator(this) 50 @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this)
43 @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator( 51 @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this)
44 this) 52 @Accessors(PUBLIC_GETTER) val UnitPropagationPreconditionGenerator unitPropagationPreconditionGenerator = new UnitPropagationPreconditionGenerator(this)
45 53
46 new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) { 54 public new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) {
47 if (typeInferenceMethod == TypeInferenceMethod.Generic) { 55 if(typeInferenceMethod == TypeInferenceMethod.Generic) {
48 this.typeIndexer = new GenericTypeIndexer(this) 56 this.typeIndexer = new GenericTypeIndexer(this)
49 this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) 57 this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this)
50 } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { 58 } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) {
@@ -151,8 +159,8 @@ class PatternGenerator {
151 RelationConstraints constraints, 159 RelationConstraints constraints,
152 Collection<LinearTypeConstraintHint> hints 160 Collection<LinearTypeConstraintHint> hints
153 ) { 161 ) {
154 162 val first =
155 return ''' 163 '''
156 import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" 164 import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
157 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" 165 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
158 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" 166 import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
@@ -167,6 +175,7 @@ class PatternGenerator {
167 ///////////////////////// 175 /////////////////////////
168 // 0.1 Existence 176 // 0.1 Existence
169 ///////////////////////// 177 /////////////////////////
178 /** [[exist(element)]]=1 */
170 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 179 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
171 find interpretation(problem,interpretation); 180 find interpretation(problem,interpretation);
172 LogicProblem.elements(problem,element); 181 LogicProblem.elements(problem,element);
@@ -175,6 +184,7 @@ class PatternGenerator {
175 PartialInterpretation.newElements(interpretation,element); 184 PartialInterpretation.newElements(interpretation,element);
176 } 185 }
177 186
187 /** [[exist(element)]]>=1/2 */
178 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 188 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
179 find mustExist(problem,interpretation,element); 189 find mustExist(problem,interpretation,element);
180 } or { 190 } or {
@@ -195,57 +205,108 @@ class PatternGenerator {
195 //////////////////////// 205 ////////////////////////
196 // 0.2 Equivalence 206 // 0.2 Equivalence
197 //////////////////////// 207 ////////////////////////
198 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 208 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement)
209 // For non-primitive type. Boolean types always must equivalent or cannot equivalent
210 {
199 find mayExist(problem,interpretation,a); 211 find mayExist(problem,interpretation,a);
200 find mayExist(problem,interpretation,b); 212 find mayExist(problem,interpretation,b);
201 a == b; 213 a == b;
214««« } or {
215««« find mayExist(problem,interpretation,a);
216««« find mayExist(problem,interpretation,b);
217««« IntegerElement(a);
218««« IntegerElement(b);
219««« PrimitiveElement.valueSet(a,false);
220««« } or {
221««« find mayExist(problem,interpretation,a);
222««« find mayExist(problem,interpretation,b);
223««« IntegerElement(a);
224««« IntegerElement(b);
225««« PrimitiveElement.valueSet(b,false);
226««« } or {
227««« find mayExist(problem,interpretation,a);
228««« find mayExist(problem,interpretation,b);
229««« RealElement(a);
230««« RealElement(b);
231««« PrimitiveElement.valueSet(a,false);
232««« } or {
233««« find mayExist(problem,interpretation,a);
234««« find mayExist(problem,interpretation,b);
235««« RealElement(a);
236««« RealElement(b);
237««« PrimitiveElement.valueSet(b,false);
238««« } or {
239««« find mayExist(problem,interpretation,a);
240««« find mayExist(problem,interpretation,b);
241««« StringElement(a);
242««« StringElement(b);
243««« PrimitiveElement.valueSet(a,false);
244««« } or {
245««« find mayExist(problem,interpretation,a);
246««« find mayExist(problem,interpretation,b);
247««« StringElement(a);
248««« StringElement(b);
249««« PrimitiveElement.valueSet(b,false);
202 } 250 }
251
203 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 252 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
253 // For non-primitive and Boolean primitive type
204 find mustExist(problem,interpretation,a); 254 find mustExist(problem,interpretation,a);
205 find mustExist(problem,interpretation,b); 255 find mustExist(problem,interpretation,b);
206 a == b; 256 a == b;
257««« } or {
258««« find mustExist(problem,interpretation,a);
259««« find mustExist(problem,interpretation,b);
260««« PrimitiveElement.valueSet(a,true);
261««« PrimitiveElement.valueSet(b,true);
262««« IntegerElement.value(a,value);
263««« IntegerElement.value(b,value);
264««« } or {
265««« find mustExist(problem,interpretation,a);
266««« find mustExist(problem,interpretation,b);
267««« PrimitiveElement.valueSet(a,true);
268««« PrimitiveElement.valueSet(b,true);
269««« RealElement.value(a,value);
270««« RealElement.value(b,value);
271««« } or {
272««« find mustExist(problem,interpretation,a);
273««« find mustExist(problem,interpretation,b);
274««« PrimitiveElement.valueSet(a,true);
275««« PrimitiveElement.valueSet(b,true);
276««« StringElement.value(a,value);
277««« StringElement.value(b,value);
207 } 278 }
208 279
209 ////////////////////////
210 // 0.3 Required Patterns by TypeIndexer
211 ////////////////////////
212 «typeIndexer.requiredQueries»
213
214 ////////// 280 //////////
215 // 1. Problem-Specific Base Indexers 281 // 1. Problem-Specific Base Indexers
216 ////////// 282 //////////
217 // 1.1 Type Indexers 283 // 1.1 Type Indexers
218 ////////// 284 //////////
219 // 1.1.1 primitive Type Indexers 285 // 1.1.1 Required Patterns by TypeIndexer
220 ////////// 286 //////////
221 ««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 287
222««« find interpretation(problem,interpretation); 288 «typeIndexer.requiredQueries»
223««« PartialInterpretation.booleanelements(interpretation,element); 289
224««« } 290 //////////
225««« pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 291 // 1.1.2 primitive Type Indexers
226««« find interpretation(problem,interpretation); 292 //////////
227««« PartialInterpretation.integerelements(interpretation,element); 293 // Currently unused. Refer primitive types as:
228««« } or { 294 // > PrimitiveElement(element)
229««« find interpretation(problem,interpretation); 295 // specific types are referred as:
230««« PartialInterpretation.newIntegers(interpetation,element); 296 // > BooleanElement(variableName)
231««« } 297 // > IntegerElement(variableName)
232««« pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 298 // > RealElement(variableName)
233««« find interpretation(problem,interpretation); 299 // > StringElement(variableName)
234««« PartialInterpretation.realelements(interpretation,element); 300 // And their value as
235««« } or { 301 // > BooleanElement.value(variableName,value)
236««« find interpretation(problem,interpretation); 302 // > IntegerElement.value(variableName,value)
237««« PartialInterpretation.newReals(interpetation,element); 303 // > RealElement.value(variableName,value)
238««« } 304 // > StringElement.value(variableName,value)
239««« pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 305 // Whether a value is set is defined by:
240««« find interpretation(problem,interpretation); 306 // > PrimitiveElement.valueSet(variableName,isFilled);
241««« PartialInterpretation.stringelements(interpretation,element);
242««« } or {
243««« find interpretation(problem,interpretation);
244««« PartialInterpretation.newStrings(interpetation,element);
245««« }
246 307
247 ////////// 308 //////////
248 // 1.1.2 domain-specific Type Indexers 309 // 1.1.3 domain-specific Type Indexers
249 ////////// 310 //////////
250 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» 311 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)»
251 312
@@ -306,6 +367,13 @@ class PatternGenerator {
306 «FOR hint : hints» 367 «FOR hint : hints»
307 «hint.getAdditionalPatterns(this)» 368 «hint.getAdditionalPatterns(this)»
308 «ENDFOR» 369 «ENDFOR»
309 ''' 370
371 //////////
372 // 6 Unit Propagations
373 //////////
374 '''
375 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)
376 val second = up.definitions
377 return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName)
310 } 378 }
311} 379}
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 f5c85524..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
@@ -10,6 +10,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStati
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis 10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult 11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod 12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints 14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint 15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy 16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
@@ -17,27 +18,28 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
18import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 19import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
19import java.util.Collection 20import java.util.Collection
21import java.util.HashMap
20import java.util.Map 22import java.util.Map
21import java.util.Set 23import java.util.Set
22import org.eclipse.viatra.query.runtime.api.IPatternMatch 24import org.eclipse.viatra.query.runtime.api.IPatternMatch
23import org.eclipse.viatra.query.runtime.api.IQuerySpecification 25import org.eclipse.viatra.query.runtime.api.IQuerySpecification
24import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 26import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
27import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
25import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 28import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
26import org.eclipse.xtend.lib.annotations.Data 29import org.eclipse.xtend.lib.annotations.Data
27 30
28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
29import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
30 32
31@Data 33@Data class GeneratedPatterns {
32class GeneratedPatterns {
33 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries 34 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries
34 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries 35 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries
35 public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries 36 public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries
36 public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery 37 public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery
37 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries 38 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
38 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
39 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries 39 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
40 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries 40 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries
41 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns
42 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns
41 public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries 43 public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries
42 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries 44 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
43} 45}
@@ -76,14 +78,15 @@ class PatternProvider {
76 } else { 78 } else {
77 null 79 null
78 } 80 }
79 val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, 81 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,
80 typeAnalysisResult, relationConstraints, hints) 82 typeAnalysisResult, relationConstraints, hints)
81 if (writeToFile) { 83 if (writeToFile) {
82 workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile) 84 workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText)
83 } 85 }
84 val ParseUtil parseUtil = new ParseUtil 86 val ParseUtil parseUtil = new ParseUtil
85 val generatedQueries = parseUtil.parse(baseIndexerFile) 87 val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText)
86 val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, 88 val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult,
89 patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName,
87 relationConstraints, generatedQueries) 90 relationConstraints, generatedQueries)
88 return runtimeQueries 91 return runtimeQueries
89 } 92 }
@@ -93,32 +96,36 @@ class PatternProvider {
93 LogicProblem problem, 96 LogicProblem problem,
94 PartialInterpretation emptySolution, 97 PartialInterpretation emptySolution,
95 TypeAnalysisResult typeAnalysisResult, 98 TypeAnalysisResult typeAnalysisResult,
99 HashMap<PConstraint, String> mustUnitPropagationTrace,
100 HashMap<PConstraint, String> currentUnitPropagationTrace,
96 RelationConstraints relationConstraints, 101 RelationConstraints relationConstraints,
97 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries 102 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
98 ) { 103 ) {
99 val invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues [ 104 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
100 it.lookup(queries) 105 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]
101 ] 106 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
102 val unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues [ 107 unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]
103 it.lookup(queries) 108
104 ] 109 val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints)
105 val multiplicityConstraintQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries( 110 val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [
106 relationConstraints.multiplicityConstraints).mapValues [
107 new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries), 111 new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries),
108 unrepairableMultiplicityQueryName?.lookup(queries), 112 unrepairableMultiplicityQueryName?.lookup(queries),
109 remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) 113 remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries))
110 ] 114 ]
111 val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( 115 val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup(
112 queries) 116 queries)
113 val unfinishedMultiplicityQueries = multiplicityConstraintQueries.entrySet.filter [ 117
114 value.unfinishedMultiplicityQuery !== null 118 val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
115 ].toMap([key.relation], [value.unfinishedMultiplicityQuery]) 119 refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
116 val refineObjectsQueries = patternGenerator.typeRefinementGenerator. 120 val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
117 getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues[it.lookup(queries)] 121 refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
118 val refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, 122 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
119 typeAnalysisResult).mapValues[it.lookup(queries)] 123 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
120 val refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem). 124 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
121 mapValues[it.lookup(queries)] 125 mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)]
126 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
127 currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)]
128
122 val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | 129 val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |
123 val indexer = patternGenerator.relationDefinitionIndexer 130 val indexer = patternGenerator.relationDefinitionIndexer
124 new ModalPatternQueries( 131 new ModalPatternQueries(
@@ -127,15 +134,17 @@ class PatternProvider {
127 indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) 134 indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries)
128 ) 135 )
129 ]) 136 ])
137
130 return new GeneratedPatterns( 138 return new GeneratedPatterns(
131 invalidWFQueries, 139 invalidWFQueries,
132 unfinishedWFQueries, 140 unfinishedWFQueries,
133 multiplicityConstraintQueries, 141 multiplicityConstraintQueries,
134 hasElementInContainmentQuery, 142 hasElementInContainmentQuery,
135 unfinishedMultiplicityQueries,
136 refineObjectsQueries, 143 refineObjectsQueries,
137 refineTypeQueries, 144 refineTypeQueries,
138 refineRelationQueries, 145 refineRelationQueries,
146 mustUnitPropagationPreconditionPatterns,
147 currentUnitPropagationPreconditionPatterns,
139 modalRelationQueries, 148 modalRelationQueries,
140 queries.values 149 queries.values
141 ) 150 )
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 f384cd50..cef707c5 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
@@ -90,13 +90,13 @@ class RelationDeclarationIndexer {
90 // There are "numberOfExistingReferences" currently existing instances of the reference from the source, 90 // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
91 // the upper bound of the multiplicity should be considered. 91 // the upper bound of the multiplicity should be considered.
92 numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» 92 numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)»
93 check(numberOfExistingReferences < «upperMultiplicities.get(relation)»); 93 numberOfExistingReferences != «upperMultiplicities.get(relation)»;
94 «ENDIF» 94 «ENDIF»
95 «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» 95 «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))»
96 // There are "numberOfExistingReferences" currently existing instances of the reference to the target, 96 // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
97 // the upper bound of the opposite reference multiplicity should be considered. 97 // the upper bound of the opposite reference multiplicity should be considered.
98 numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» 98 numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)»
99 check(numberOfExistingOppositeReferences < «upperMultiplicities.get(inverseRelations.get(relation))»); 99 numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»;
100 «ENDIF» 100 «ENDIF»
101 «IF containments.contains(relation)» 101 «IF containments.contains(relation)»
102 // The reference is containment, then a new reference cannot be create if: 102 // The reference is containment, then a new reference cannot be create if:
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
index 0ae28b66..338a9af2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
@@ -5,39 +5,27 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import java.util.Map 7import java.util.Map
8import org.eclipse.emf.common.util.Enumerator
9import org.eclipse.emf.ecore.EAttribute
10import org.eclipse.emf.ecore.EEnumLiteral
11import org.eclipse.emf.ecore.EReference
12import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
13import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
14import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
15import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
16import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable 8import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure 9import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
23import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue 10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
24import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
25import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
26import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 11import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
27 12
28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
29 14
30class RelationDefinitionIndexer { 15class RelationDefinitionIndexer {
31 val PatternGenerator base; 16 public val PatternGenerator base;
17 val PConstraintTransformer constraintTransformer;
32 18
33 new(PatternGenerator base) { 19 new(PatternGenerator base) {
34 this.base = base 20 this.base = base
21 this.constraintTransformer = new PConstraintTransformer(this);
35 } 22 }
36 23
37 def generateRelationDefinitions( 24 def generateRelationDefinitions(
38 LogicProblem problem, 25 LogicProblem problem,
39 Iterable<RelationDefinition> relations, 26 Iterable<RelationDefinition> relations,
40 Map<String,PQuery> fqn2PQuery) { 27 Map<String,PQuery> fqn2PQuery)
28 {
41 val relation2PQuery = relations.toInvertedMap[ 29 val relation2PQuery = relations.toInvertedMap[
42 annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery) 30 annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery)
43 ] 31 ]
@@ -75,20 +63,21 @@ class RelationDefinitionIndexer {
75 def String relationDefinitionName(RelationDefinition relation, Modality modality) 63 def String relationDefinitionName(RelationDefinition relation, Modality modality)
76 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' 64 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»'''
77 65
78 private def canonizeName(PVariable v) { 66 def canonizeName(PVariable v) {
79 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' 67 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
80 } 68 }
81 69
82 private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) { 70 private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) {
83 try { 71 try {
72 val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
84 return ''' 73 return '''
85 private pattern «relationDefinitionName(relation,modality)»( 74 private pattern «relationDefinitionName(relation,modality)»(
86 problem:LogicProblem, interpretation:PartialInterpretation, 75 problem:LogicProblem, interpretation:PartialInterpretation,
87 «FOR param : p.parameters SEPARATOR ', '»var_«param.name»«ENDFOR») 76 «FOR param : p.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»)
88 «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ 77 «FOR body : bodies SEPARATOR "or"»{
89 find interpretation(problem,interpretation); 78 find interpretation(problem,interpretation);
90 «FOR constraint : body.constraints» 79 «FOR constraint : body.constraints»
91 «constraint.transformConstraint(modality)» 80 «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
92 «ENDFOR» 81 «ENDFOR»
93 }«ENDFOR» 82 }«ENDFOR»
94 ''' 83 '''
@@ -105,7 +94,7 @@ class RelationDefinitionIndexer {
105 ''' 94 '''
106 } 95 }
107 96
108 private def toMustMay(Modality modality) { 97 def toMustMay(Modality modality) {
109 if(modality == Modality::MAY) return Modality::MAY 98 if(modality == Modality::MAY) return Modality::MAY
110 else return Modality::MUST 99 else return Modality::MUST
111 } 100 }
@@ -113,154 +102,4 @@ class RelationDefinitionIndexer {
113 def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' 102 def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) '''
114 «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); 103 «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»);
115 ''' 104 '''
116
117 private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) {
118 val touple = constraint.variablesTuple
119 if(touple.size == 1) {
120 val inputKey = constraint.equivalentJudgement.inputKey
121 if(inputKey instanceof EClassTransitiveInstancesKey) {
122 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
123 constraint.getVariableInTuple(0).canonizeName)
124 } else if(inputKey instanceof EDataTypeInSlotsKey){
125 return '''// type constraint is enforced by construction'''
126 }
127
128 } else if(touple.size == 2){
129 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
130 if(key instanceof EReference) {
131 return base.referRelationByName(
132 key,
133 constraint.getVariableInTuple(0).canonizeName,
134 constraint.getVariableInTuple(1).canonizeName,
135 modality.toMustMay)
136 } else if (key instanceof EAttribute) {
137 return base.referAttributeByName(key,
138 constraint.getVariableInTuple(0).canonizeName,
139 constraint.getVariableInTuple(1).canonizeName,
140 modality.toMustMay)
141 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
142 } else {
143 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
144 }
145 }
146 private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) {
147 val touple = constraint.variablesTuple
148 if(touple.size == 1) {
149 val inputKey = constraint.equivalentJudgement.inputKey
150 if(inputKey instanceof EClassTransitiveInstancesKey) {
151 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
152 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
153 } else if(inputKey instanceof EDataTypeInSlotsKey){
154 return '''// type constraint is enforced by construction'''
155 }
156
157 } else if(touple.size == 2){
158 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
159 if(key instanceof EReference) {
160 return base.referRelationByName(
161 key,
162 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
163 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
164 modality.toMustMay)
165 } else if (key instanceof EAttribute) {
166 return base.referAttributeByName(key,
167 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
168 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
169 modality.toMustMay)
170 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
171 } else {
172 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
173 }
174 }
175
176 private dispatch def transformConstraint(Equality equality, Modality modality) {
177 val a = equality.who
178 val b = equality.withWhom
179 transformEquality(modality.toMustMay, a, b)
180 }
181
182 private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
183 if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
184 else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
185 }
186
187 private dispatch def transformConstraint(Inequality inequality, Modality modality) {
188 val a = inequality.who
189 val b = inequality.withWhom
190 if(modality.isCurrent) {
191 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
192 } else if(modality.isMust) {
193 return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
194 } else { // modality.isMay
195 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
196 }
197 }
198
199 private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) {
200 val params = (0..<pcall.actualParametersTuple.size).map[index |
201 val variable = pcall.actualParametersTuple.get(index) as PVariable
202 return variable.canonizeName
203 ]
204 return referPattern(pcall.referredQuery,params,modality.dual,false,false)
205 }
206
207 private dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) {
208 val params = (0..<pcall.variablesTuple.size).map[index |
209 val variable = pcall.variablesTuple.get(index) as PVariable
210 return variable.canonizeName
211 ]
212 return referPattern(pcall.referredQuery,params,modality,true,false)
213 }
214 private dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) {
215 val params = (0..1).map[index |
216 val variable = pcall.getVariableInTuple(index) as PVariable
217 return variable.canonizeName
218 ]
219 return referPattern(pcall.referredQuery,params,modality,true,true)
220 }
221 private dispatch def transformConstraint(ExportedParameter e, Modality modality) {
222 return '''// «e.parameterName» is exported'''
223 }
224 private dispatch def transformConstraint(ConstantValue c, Modality modality) {
225 val target = c.supplierKey
226
227 var String targetString;
228 var String additionalDefinition;
229 if(target instanceof EEnumLiteral) {
230 targetString = '''const_«target.name»_«target.EEnum.name»'''
231 additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» literal «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
232 } else if(target instanceof Enumerator) {
233 // XXX We should get the corresponding EEnum name instead of the java class name.
234 targetString = '''const_«target.name»_«target.class.simpleName»'''
235 additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» literal «target.class.simpleName»"); //LogicProblem.elements(problem,«targetString»);'''
236 } else if(target instanceof Integer) {
237 targetString = '''const_«target»_Integer'''
238 additionalDefinition = '''IntegerElement.value(«targetString»,«target»);'''
239 } else if(target instanceof Boolean) {
240 targetString = '''const_«target»_Boolean'''
241 additionalDefinition = '''BooleanElement.value(«targetString»,«target»);'''
242 } else if(target instanceof String) {
243 targetString = '''const_«target»_String'''
244 additionalDefinition = '''StringElement.value(«targetString»,"«target»");'''
245 } else if(target instanceof Double) {
246 targetString = '''const_«target»_Number'''
247 additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
248 } else if(target instanceof Float) {
249 targetString = '''const_«target»_Number'''
250 additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
251 } else {
252 throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
253 }
254
255 val source = c.variablesTuple
256 var String sourceName
257 if(source.size == 1)
258 sourceName = (source.get(0) as PVariable).canonizeName
259 else throw new UnsupportedOperationException("unknown source")
260 return '''«sourceName» == «targetString»;«additionalDefinition»''';
261 }
262
263 private dispatch def transformConstraint(PConstraint c, Modality modality) {
264 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
265 }
266} \ No newline at end of file 105} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
index 7d687e99..e4e2aa30 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
@@ -119,4 +119,8 @@ abstract class TypeIndexer {
119 '''StringElement.value(«variableName»,"«value»");''' 119 '''StringElement.value(«variableName»,"«value»");'''
120 } 120 }
121 121
122 def CharSequence referPrimitiveFilled(String variableName, boolean isFilled) {
123 '''PrimitiveElement.valueSet(«variableName»,«isFilled»);'''
124 }
122} 125}
126
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
new file mode 100644
index 00000000..400f47bc
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
@@ -0,0 +1,302 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.PropagationModality
9import java.util.Map
10import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
11import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
12import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
13import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
14
15import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16import java.util.LinkedList
17import java.util.List
18import org.eclipse.xtend.lib.annotations.Data
19import java.util.HashMap
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
22import java.util.Comparator
23import java.util.ArrayList
24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
25import java.util.LinkedHashSet
26
27@Data class UnitPropagation {
28 val PQuery q
29 val PConstraint c
30 val PropagationModality pm
31 val Modality m3
32}
33@Data
34class UnitPropagationPreconditionGenerationResult {
35 List<CharSequence> definitions= new LinkedList
36 Map<UnitPropagation,String> unitPropagation2PatternName = new HashMap
37 Map<PConstraint,String> constraintOccurence2Name = new HashMap
38
39 def registerQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3, String patternName, CharSequence definition) {
40 val key = new UnitPropagation(q,c,pm,m3)
41 definitions += definition
42 unitPropagation2PatternName.put(key,patternName)
43 }
44 def registerUnsatQuery(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
45 val key = new UnitPropagation(q,c,pm,m3)
46 unitPropagation2PatternName.put(key,null)
47 }
48 def contains(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
49 val key = new UnitPropagation(q,c,pm,m3)
50 return unitPropagation2PatternName.containsKey(key)
51 }
52 def getName(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
53 val key = new UnitPropagation(q,c,pm,m3)
54 return key.lookup(unitPropagation2PatternName)
55 }
56 def isDefined(PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
57 val key = new UnitPropagation(q,c,pm,m3)
58 return unitPropagation2PatternName.get(key) !== null
59 }
60}
61@Data
62class UnitPropagationPreconditionFinalResult {
63 CharSequence definitions
64 HashMap<PConstraint,String> constraint2MustPreconditionName
65 HashMap<PConstraint,String> constraint2CurrentPreconditionName
66}
67
68class UnitPropagationPreconditionGenerator {
69 val PatternGenerator base
70 val PConstraintTransformer constraintTransformer;
71
72 new(PatternGenerator patternGenerator) {
73 this.base = patternGenerator
74 this.constraintTransformer = new PConstraintTransformer(base.relationDefinitionIndexer)
75 }
76
77 def generateUnitPropagationRules(
78 LogicProblem problem,
79 Iterable<RelationDefinition> relations,
80 Map<String,PQuery> fqn2PQuery)
81 {
82 // Create an empty result
83 val res = new UnitPropagationPreconditionGenerationResult
84 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
85 val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap
86 val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap
87 for(wf : wfs) {
88 val query = wf.patternPQuery as PQuery
89 val relation = wf.target
90 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
91
92 for(referredCheck : allReferredChecks) {
93 val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
94 val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT)
95 if(!mainMustPropagationNames.containsKey(referredCheck)) {
96 mainMustPropagationNames.put(referredCheck,new LinkedList)
97 }
98 if(!mainCurrentPropagationNames.containsKey(referredCheck)) {
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)
106 }
107 }
108 }
109 val preconditions = new LinkedList
110 val constraint2MustPrecondition = new HashMap
111 val constraint2CurrentPrecondition = new HashMap
112 for(entry : mainMustPropagationNames.entrySet) {
113 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
114 val def = '''
115 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
116 «FOR propagation : entry.value SEPARATOR " or "»
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»); }
118 «ENDFOR»'''
119 preconditions+=def
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)
131 }
132
133 val definitions = '''
134 «FOR def : res.definitions»
135 «def»
136 «ENDFOR»
137
138 // Collected propagation preconditions:
139
140 «FOR predondition : preconditions»
141 «predondition»
142 «ENDFOR»
143 '''
144 return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition)
145 }
146 def allReferredConstraints(Relation relation, PQuery query) {
147 val allReferredQueries = query.allReferredQueries
148 val problem = relation.eContainer as LogicProblem
149 val constraints = new LinkedHashSet
150 for(referredQuery: #[query]+allReferredQueries) {
151 val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target
152 val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
153 constraints.addAll(bodies.map[getConstraints].flatten)
154 }
155
156 return constraints
157 }
158
159 def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
160 if(res.contains(q,c,pm,m3)) {
161 return res.getName(q,c,pm,m3)
162 } else {
163 res.generatePropagationRule(relation,q,c,pm,m3)
164 return res.getName(q,c,pm,m3)
165 }
166 }
167 def getOrGenerateConstraintName(UnitPropagationPreconditionGenerationResult res, PConstraint c){
168 if(res.constraintOccurence2Name.containsKey(c)) {
169 return res.constraintOccurence2Name.get(c)
170 } else {
171 val constraintName = '''Constraint«res.constraintOccurence2Name.size»'''
172 res.constraintOccurence2Name.put(c,constraintName)
173 return constraintName
174 }
175 }
176
177 def void generatePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
178 val name = relationDefinitionName(res,relation,q,c,pm,m3)
179 val constraintArity = c.arity
180 val bodies = (relation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
181 val generatedBodies = new LinkedList
182 for(body : bodies) {
183 if(body.constraints.contains(c)) {
184 if(pm === PropagationModality::UP) {
185 generatedBodies += '''
186 // Original Constraints
187 «FOR constraint : body.constraints.filter[it !== c]»
188 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
189 «ENDFOR»
190 // Propagation for constraint
191 «this.constraintTransformer.transformConstraintUnset(c as ExpressionEvaluation,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
192 // Matching variables
193 «this.propagateVariables(c,pm)»
194 '''
195 }
196 // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied
197 } else {
198 val positives = body.constraints.filter(PositivePatternCall)
199 for(positive: positives) {
200 val referredPQuery = positive.referredQuery
201 val referredRelation = (relation.eContainer as LogicProblem)
202 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
203 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
204 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3)
205 if(referredName !== null) {
206 generatedBodies += '''
207 // Original Constraints
208 «FOR constraint : body.constraints.filter[it !== positive]»
209 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
210 «ENDFOR»
211 // Propagation for constraint referred indirectly from this pattern through «referredName»
212 find «referredName»(problem, interpretation,
213 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR»,
214 «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
215 '''
216 }
217 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
218 }
219 }
220
221 val negatives = body.constraints.filter(NegativePatternCall)
222 for(negative : negatives) {
223 val referredPQuery = negative.referredQuery
224 val referredRelation = (relation.eContainer as LogicProblem)
225 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
226 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
227 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual)
228 if(referredName !== null) {
229 generatedBodies += '''
230 // Original Constraints
231 «FOR constraint : body.constraints.filter[it !== negative]»
232 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
233 «ENDFOR»
234 // Propagation for constraint referred indirectly from this pattern through «referredName»
235 find «referredName»(problem, interpretation,
236 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
237 «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
238 '''
239 } else {
240 generatedBodies += '''
241 // Original Constraints
242 «FOR constraint : body.constraints.filter[it !== negative]»
243 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
244 «ENDFOR»
245 // Propagation for constraint referred indirectly from this pattern through «referredName»,
246 // which was unsatisfiable
247 '''
248 }
249 }
250 }
251 }
252 }
253
254 // Register the result
255 if(generatedBodies.empty) {
256 res.registerUnsatQuery(q,c,pm,m3)
257 } else {
258 val definition = '''
259 private pattern «name»(
260 problem:LogicProblem, interpretation:PartialInterpretation,
261 «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,
262 «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)
263 «FOR generatedBody: generatedBodies SEPARATOR " or "»{
264 «generatedBody»
265 }«ENDFOR»
266 '''
267 res.registerQuery(q,c,pm,m3,name,definition)
268 }
269 }
270
271 private def String relationDefinitionName(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3)
272 '''«pm.name»«m3.name»Propagate«res.getOrGenerateConstraintName(c)»_«base.canonizeName(relation.name)»'''
273
274 def canonizeName(PVariable v) {
275 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
276 }
277
278 def canonizeName(int index, PropagationModality m) {
279 return '''«m.name.toLowerCase»_«index»'''
280 }
281
282 def dispatch propagateVariables(ExpressionEvaluation c, PropagationModality m) {
283 val comparator = new Comparator<PVariable>(){
284 override compare(PVariable o1, PVariable o2) {
285 o1.name.compareTo(o2.name)
286 }
287 }
288 val variablesInOrder = new ArrayList(c.affectedVariables)
289 variablesInOrder.toList.sort(comparator)
290 return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»'''
291 }
292 def dispatch propagateVariables(PConstraint c, PropagationModality m) {
293 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
294 }
295
296 def dispatch arity(ExpressionEvaluation c) {
297 c.affectedVariables.size
298 }
299 def dispatch arity(PConstraint c) {
300 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
301 }
302} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
index b6fdbe06..238ade5b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
@@ -1,18 +1,26 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator 4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns 5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
5import java.util.ArrayList 6import java.util.ArrayList
6 7
7class GoalConstraintProvider { 8class GoalConstraintProvider {
8 def public getUnfinishedMultiplicityQueries(GeneratedPatterns patterns) { 9
9 val multiplicityQueries = patterns.unfinishedMulticiplicityQueries 10 def getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns) {
10 val res = new ArrayList(multiplicityQueries.size) 11 val res = new ArrayList()
11 for(multiplicityQuery : multiplicityQueries.entrySet) { 12 for (entry : patterns.multiplicityConstraintQueries.entrySet) {
12 val targetRelationName = multiplicityQuery.key.name 13 val constraint = entry.key
13 val query = multiplicityQuery.value 14 if (constraint.constrainsUnfinished) {
14 res += new MultiplicityGoalConstraintCalculator(targetRelationName,query); 15 val queries = entry.value
16 val targetRelationName = constraint.relation.name
17 val query = queries.unfinishedMultiplicityQuery
18 val minValue = constraint.lowerBound
19 val containment = constraint.containment
20 res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, minValue, containment, 1)
21 }
15 } 22 }
16 return res 23 return res
17 } 24 }
25
18} \ No newline at end of file 26} \ No newline at end of file
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 7891ebd8..0b8a9019 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
@@ -1,71 +1,93 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules
2 2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion
4import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory 9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation 12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
16import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics 17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator 18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns 19import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition 20import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition
21import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation 22import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
23import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 24import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
25import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation 26import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation
28import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory 29import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory
30import java.util.HashMap
16import java.util.LinkedHashMap 31import java.util.LinkedHashMap
32import java.util.LinkedList
33import java.util.List
34import java.util.Map
17import org.eclipse.viatra.query.runtime.api.GenericPatternMatch 35import org.eclipse.viatra.query.runtime.api.GenericPatternMatch
18import org.eclipse.viatra.query.runtime.api.IQuerySpecification 36import org.eclipse.viatra.query.runtime.api.IQuerySpecification
19import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 37import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
20import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule 38import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
21import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory 39import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory
40import org.eclipse.xtend.lib.annotations.Data
41import org.eclipse.xtext.xbase.lib.Functions.Function0
22 42
23class RefinementRuleProvider { 43class RefinementRuleProvider {
24 private extension BatchTransformationRuleFactory factory = new BatchTransformationRuleFactory 44 val extension BatchTransformationRuleFactory factory = new BatchTransformationRuleFactory
25 private extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE 45 val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE
26 private extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE 46 val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE
27 47
28 def canonizeName(String name) { 48 def canonizeName(String name) {
29 return name.replace(' ','_') 49 return name.replace(' ','_')
30 } 50 }
31 51
32 def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> 52 def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> createObjectRefinementRules(
33 createObjectRefinementRules( 53 LogicProblem p,
54 PartialInterpretation i,
34 GeneratedPatterns patterns, 55 GeneratedPatterns patterns,
35 ScopePropagator scopePropagator, 56 ScopePropagator scopePropagator,
36 boolean nameNewElement, 57 boolean nameNewElement,
37 ModelGenerationStatistics statistics 58 ModelGenerationStatistics statistics
38 ) 59 )
39 { 60 {
40 val res = new LinkedHashMap 61 val res = new LinkedHashMap
62 val recursiveObjectCreation = recursiveObjectCreation(p,i)
41 for(LHSEntry: patterns.refineObjectQueries.entrySet) { 63 for(LHSEntry: patterns.refineObjectQueries.entrySet) {
42 val containmentRelation = LHSEntry.key.containmentRelation 64 val containmentRelation = LHSEntry.key.containmentRelation
43 val inverseRelation = LHSEntry.key.inverseContainment 65 val inverseRelation = LHSEntry.key.inverseContainment
44 val type = LHSEntry.key.newType 66 val type = LHSEntry.key.newType
45 val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> 67 val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>>
46 val rule = createObjectCreationRule(containmentRelation,inverseRelation,type,lhs,nameNewElement,scopePropagator,statistics) 68 val rule = createObjectCreationRule(p,containmentRelation,inverseRelation,type,recursiveObjectCreation.get(type),lhs,nameNewElement,scopePropagator,statistics)
47 res.put(LHSEntry.key,rule) 69 res.put(LHSEntry.key,rule)
48 } 70 }
49 return res 71 return res
50 } 72 }
51 73
52 def private createObjectCreationRule( 74 def private createObjectCreationRule(
75 LogicProblem p,
53 Relation containmentRelation, 76 Relation containmentRelation,
54 Relation inverseRelation, 77 Relation inverseRelation,
55 Type type, 78 Type type,
79 List<ObjectCreationInterpretationData> recursiceObjectCreations,
56 IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, 80 IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs,
57 boolean nameNewElement, 81 boolean nameNewElement,
58 ScopePropagator scopePropagator, 82 ScopePropagator scopePropagator,
59 ModelGenerationStatistics statistics) 83 ModelGenerationStatistics statistics)
60 { 84 {
61 val name = '''addObject_«type.name.canonizeName»« 85 val name = '''addObject_«type.name.canonizeName»«
62 IF containmentRelation!=null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' 86 IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»'''
63 //println("Rule created: " + name + "> " + lhs.fullyQualifiedName) 87 val ruleBuilder = factory.createRule(lhs)
64 val ruleBuilder = factory.createRule
65 .name(name) 88 .name(name)
66 .precondition(lhs) 89 if(containmentRelation !== null) {
67 if(containmentRelation != null) { 90 if(inverseRelation!== null) {
68 if(inverseRelation!= null) {
69 ruleBuilder.action[match | 91 ruleBuilder.action[match |
70 statistics.incrementTransformationCount 92 statistics.incrementTransformationCount
71// println(name) 93// println(name)
@@ -77,33 +99,23 @@ class RefinementRuleProvider {
77 val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation 99 val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation
78 val container = match.get(5) as DefinedElement 100 val container = match.get(5) as DefinedElement
79 101
80 val newElement = createDefinedElement 102 createObjectActionWithContainmentAndInverse(
81 if(nameNewElement) { 103 nameNewElement,
82 newElement.name = '''new «interpretation.newElements.size»''' 104 interpretation,
83 } 105 typeInterpretation,
84 106 container,
85 // Existence 107 relationInterpretation,
86 interpretation.newElements+=newElement 108 inverseRelationInterpretation,
87 /*interpretation.maxNewElements=interpretation.maxNewElements-1 109 [createDefinedElement],
88 if(interpretation.minNewElements > 0) { 110 recursiceObjectCreations,
89 interpretation.minNewElements=interpretation.minNewElements-1 111 scopePropagator
90 }*/ 112 )
91
92 // Types
93 typeInterpretation.elements += newElement
94 typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
95 // ContainmentRelation
96 val newLink1 = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
97 relationInterpretation.relationlinks+=newLink1
98 // Inverse Containment
99 val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container]
100 inverseRelationInterpretation.relationlinks+=newLink2
101 113
102 val propagatorStartTime = System.nanoTime 114 val propagatorStartTime = System.nanoTime
103 statistics.addExecutionTime(propagatorStartTime-startTime) 115 statistics.addExecutionTime(propagatorStartTime-startTime)
104 116
105 // Scope propagation 117 // Scope propagation
106 scopePropagator.propagateAdditionToType(typeInterpretation) 118 scopePropagator.propagateAllScopeConstraints()
107 statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) 119 statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
108 ] 120 ]
109 } else { 121 } else {
@@ -117,30 +129,22 @@ class RefinementRuleProvider {
117 val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation 129 val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation
118 val container = match.get(4) as DefinedElement 130 val container = match.get(4) as DefinedElement
119 131
120 val newElement = createDefinedElement 132 createObjectActionWithContainment(
121 if(nameNewElement) { 133 nameNewElement,
122 newElement.name = '''new «interpretation.newElements.size»''' 134 interpretation,
123 } 135 typeInterpretation,
124 136 container,
125 // Existence 137 relationInterpretation,
126 interpretation.newElements+=newElement 138 [createDefinedElement],
127 /*interpretation.maxNewElements=interpretation.maxNewElements-1 139 recursiceObjectCreations,
128 if(interpretation.minNewElements > 0) { 140 scopePropagator
129 interpretation.minNewElements=interpretation.minNewElements-1 141 )
130 }*/
131
132 // Types
133 typeInterpretation.elements += newElement
134 typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
135 // ContainmentRelation
136 val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
137 relationInterpretation.relationlinks+=newLink
138 142
139 val propagatorStartTime = System.nanoTime 143 val propagatorStartTime = System.nanoTime
140 statistics.addExecutionTime(propagatorStartTime-startTime) 144 statistics.addExecutionTime(propagatorStartTime-startTime)
141 145
142 // Scope propagation 146 // Scope propagation
143 scopePropagator.propagateAdditionToType(typeInterpretation) 147 scopePropagator.propagateAllScopeConstraints()
144 statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) 148 statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
145 ] 149 ]
146 } 150 }
@@ -148,40 +152,175 @@ class RefinementRuleProvider {
148 ruleBuilder.action[match | 152 ruleBuilder.action[match |
149 statistics.incrementTransformationCount 153 statistics.incrementTransformationCount
150// println(name) 154// println(name)
151
152 val startTime = System.nanoTime 155 val startTime = System.nanoTime
153 //val problem = match.get(0) as LogicProblem 156 //val problem = match.get(0) as LogicProblem
154 val interpretation = match.get(1) as PartialInterpretation 157 val interpretation = match.get(1) as PartialInterpretation
155 val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation 158 val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation
156 159
157 val newElement = createDefinedElement 160 createObjectAction(
158 if(nameNewElement) { 161 nameNewElement,
159 newElement.name = '''new «interpretation.newElements.size»''' 162 interpretation,
160 } 163 typeInterpretation,
161 164 [createDefinedElement],
162 // Existence 165 recursiceObjectCreations,
163 interpretation.newElements+=newElement 166 scopePropagator
164 /* 167 )
165 interpretation.maxNewElements=interpretation.maxNewElements-1
166 if(interpretation.minNewElements > 0) {
167 interpretation.minNewElements=interpretation.minNewElements-1
168 }*/
169
170 // Types
171 typeInterpretation.elements += newElement
172 typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
173 168
174 val propagatorStartTime = System.nanoTime 169 val propagatorStartTime = System.nanoTime
175 statistics.addExecutionTime(propagatorStartTime-startTime) 170 statistics.addExecutionTime(propagatorStartTime-startTime)
176 171
177 // Scope propagation 172 // Scope propagation
178 scopePropagator.propagateAdditionToType(typeInterpretation) 173 scopePropagator.propagateAllScopeConstraints()
179 statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) 174 statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime)
180 ] 175 ]
181 } 176 }
182 return ruleBuilder.build 177 return ruleBuilder.build
183 } 178 }
184 179
180 def private recursiveObjectCreation(LogicProblem p, PartialInterpretation i) {
181 val Map<Type,List<ObjectCreationInterpretationData>> recursiveObjectCreation = new HashMap
182 for(type : p.types) {
183 recursiveObjectCreation.put(type,new LinkedList)
184 }
185
186 val containmentReferences = p.containmentHierarchies.head.containmentRelations
187
188 for(relationInterpretation : i.partialrelationinterpretation) {
189 val relation = relationInterpretation.interpretationOf
190 val lowermultiplicities = p.annotations.filter(LowerMultiplicityAssertion).filter[it.relation === relation]
191 if((!lowermultiplicities.empty)) {
192 val number = lowermultiplicities.head.lower
193 if(number > 0) {
194 val sourceTypeInterpretation = getTypeInterpretation(i, relation, 0) as PartialComplexTypeInterpretation
195 val subtypeInterpretations = i.partialtypeinterpratation.filter(PartialComplexTypeInterpretation).filter[
196 it === sourceTypeInterpretation ||
197 it.supertypeInterpretation.contains(sourceTypeInterpretation)
198 ]
199
200 if(containmentReferences.contains(relation)) {
201 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
202 val targetType = (targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf
203 if((!targetType.isIsAbstract) && (targetType.supertypes.empty)) {
204 val inverseAnnotation = p.annotations.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation]
205 if(!inverseAnnotation.empty) {
206 val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) {
207 inverseAnnotation.head.inverseB
208 } else {
209 inverseAnnotation.head.inverseA
210 }
211 val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head
212 for(subTypeInterpretation : subtypeInterpretations) {
213 for(var times=0; times<number; times++) {
214 recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) +=
215 new ObjectCreationInterpretationData(
216 i,
217 targetTypeInterpretation,
218 relationInterpretation,
219 inverseRelationInterpretation,
220 targetTypeInterpretation.getTypeConstructor
221 )
222 }
223 }
224 } else {
225 for(subTypeInterpretation : subtypeInterpretations) {
226 for(var times=0; times<number; times++) {
227 recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) +=
228 new ObjectCreationInterpretationData(
229 i,
230 targetTypeInterpretation,
231 relationInterpretation,
232 null,
233 targetTypeInterpretation.getTypeConstructor
234 )
235 }
236 }
237 }
238 }
239 } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) {
240 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
241 for(subTypeInterpretation : subtypeInterpretations) {
242 for(var times=0; times<number; times++) {
243 recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) +=
244 new ObjectCreationInterpretationData(
245 i,
246 targetTypeInterpretation,
247 relationInterpretation,
248 null,
249 targetTypeInterpretation.getTypeConstructor
250 )
251 }
252 }
253 }
254 }
255 }
256 }
257
258 // Doing the recursion
259 var objectCreations = new LinkedList(recursiveObjectCreation.values.flatten.toList)
260 for(objectCreation : objectCreations) {
261 val newInterpretation = objectCreation.typeInterpretation
262 if(newInterpretation instanceof PartialComplexTypeInterpretation) {
263 val newlyCreatedType = newInterpretation.interpretationOf
264 if(recursiveObjectCreation.containsKey(newlyCreatedType)) {
265 val actionsWhenTypeCreated = recursiveObjectCreation.get(newlyCreatedType)
266 objectCreation.recursiveConstructors+=actionsWhenTypeCreated
267 }
268 }
269 }
270
271 // checking acyclicity
272 for(objectCreation : objectCreations) {
273 var reachable = objectCreation.recursiveConstructors
274 do {
275 if(reachable.contains(objectCreation)) {
276 throw new IllegalArgumentException('''Cicrle in the containment!''')
277 } else {
278 reachable = reachable.map[it.recursiveConstructors].flatten.toList
279 }
280 } while(!reachable.empty)
281 }
282
283 return recursiveObjectCreation
284 }
285
286 private def getTypeInterpretation(PartialInterpretation i, RelationDeclaration relation, int index) {
287 val typeReference = relation.parameters.get(index)
288 return getTypeInterpretation(i,typeReference)
289
290 }
291 private dispatch def getTypeInterpretation(PartialInterpretation i, ComplexTypeReference reference) {
292 return i.partialtypeinterpratation
293 .filter(PartialComplexTypeInterpretation)
294 .filter[it.getInterpretationOf == reference.referred]
295 .head
296 }
297 private dispatch def getTypeInterpretation(PartialInterpretation i, BoolTypeReference reference) {
298 return i.partialtypeinterpratation
299 .filter(PartialBooleanInterpretation)
300 .head
301 }
302 private dispatch def getTypeInterpretation(PartialInterpretation i, IntTypeReference reference) {
303 return i.partialtypeinterpratation
304 .filter(PartialIntegerInterpretation)
305 .head
306 }
307 private dispatch def getTypeInterpretation(PartialInterpretation i, RealTypeReference reference) {
308 return i.partialtypeinterpratation
309 .filter(PartialRealInterpretation)
310 .head
311 }
312 private dispatch def getTypeInterpretation(PartialInterpretation i, StringTypeReference reference) {
313 return i.partialtypeinterpratation
314 .filter(PartialStringInterpretation)
315 .head
316 }
317 private dispatch def Function0<DefinedElement> getTypeConstructor(PartialComplexTypeInterpretation reference) { [createDefinedElement] }
318 private dispatch def Function0<DefinedElement> getTypeConstructor(PartialBooleanInterpretation reference) { [createBooleanElement] }
319 private dispatch def Function0<DefinedElement> getTypeConstructor(PartialIntegerInterpretation reference) { [createIntegerElement] }
320 private dispatch def Function0<DefinedElement> getTypeConstructor(PartialRealInterpretation reference) { [createRealElement] }
321 private dispatch def Function0<DefinedElement> getTypeConstructor(PartialStringInterpretation reference) { [createStringElement] }
322
323
185 def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { 324 def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) {
186 val res = new LinkedHashMap 325 val res = new LinkedHashMap
187 for(LHSEntry: patterns.refinerelationQueries.entrySet) { 326 for(LHSEntry: patterns.refinerelationQueries.entrySet) {
@@ -197,11 +336,10 @@ class RefinementRuleProvider {
197 def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> 336 def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>
198 createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) 337 createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator, ModelGenerationStatistics statistics)
199 { 338 {
200 val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation != null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' 339 val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»'''
201 val ruleBuilder = factory.createRule 340 val ruleBuilder = factory.createRule(lhs)
202 .name(name) 341 .name(name)
203 .precondition(lhs) 342 if (inverseRelation === null) {
204 if (inverseRelation == null) {
205 ruleBuilder.action [ match | 343 ruleBuilder.action [ match |
206 statistics.incrementTransformationCount 344 statistics.incrementTransformationCount
207 val startTime = System.nanoTime 345 val startTime = System.nanoTime
@@ -211,8 +349,8 @@ class RefinementRuleProvider {
211 val relationInterpretation = match.get(2) as PartialRelationInterpretation 349 val relationInterpretation = match.get(2) as PartialRelationInterpretation
212 val src = match.get(3) as DefinedElement 350 val src = match.get(3) as DefinedElement
213 val trg = match.get(4) as DefinedElement 351 val trg = match.get(4) as DefinedElement
214 val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] 352
215 relationInterpretation.relationlinks += link 353 createRelationLinkAction(src, trg, relationInterpretation)
216 354
217 val propagatorStartTime = System.nanoTime 355 val propagatorStartTime = System.nanoTime
218 statistics.addExecutionTime(propagatorStartTime-startTime) 356 statistics.addExecutionTime(propagatorStartTime-startTime)
@@ -232,10 +370,8 @@ class RefinementRuleProvider {
232 val inverseInterpretation = match.get(3) as PartialRelationInterpretation 370 val inverseInterpretation = match.get(3) as PartialRelationInterpretation
233 val src = match.get(4) as DefinedElement 371 val src = match.get(4) as DefinedElement
234 val trg = match.get(5) as DefinedElement 372 val trg = match.get(5) as DefinedElement
235 val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] 373
236 relationInterpretation.relationlinks += link 374 createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation)
237 val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src]
238 inverseInterpretation.relationlinks += inverseLink
239 375
240 val propagatorStartTime = System.nanoTime 376 val propagatorStartTime = System.nanoTime
241 statistics.addExecutionTime(propagatorStartTime-startTime) 377 statistics.addExecutionTime(propagatorStartTime-startTime)
@@ -248,4 +384,182 @@ class RefinementRuleProvider {
248 384
249 return ruleBuilder.build 385 return ruleBuilder.build
250 } 386 }
387
388 /////////////////////////
389 // Actions
390 /////////////////////////
391
392 protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, DefinedElement container, ScopePropagator scopePropagator) {
393 if(data.containerInterpretation !== null) {
394 if(data.containerInverseInterpretation !== null) {
395 createObjectActionWithContainmentAndInverse(
396 nameNewElement,
397 data.interpretation,
398 data.typeInterpretation,
399 container,
400 data.containerInterpretation,
401 data.containerInverseInterpretation,
402 data.constructor,
403 data.recursiveConstructors,
404 scopePropagator
405 )
406 } else {
407 createObjectActionWithContainment(
408 nameNewElement,
409 data.interpretation,
410 data.typeInterpretation,
411 container,
412 data.containerInterpretation,
413 data.constructor,
414 data.recursiveConstructors,
415 scopePropagator
416 )
417 }
418 } else {
419 createObjectAction(
420 nameNewElement,
421 data.interpretation,
422 data.typeInterpretation,
423 data.constructor,
424 data.recursiveConstructors,
425 scopePropagator
426 )
427 }
428
429 }
430
431 protected def createObjectActionWithContainmentAndInverse(
432 boolean nameNewElement,
433 PartialInterpretation interpretation,
434 PartialTypeInterpratation typeInterpretation,
435 DefinedElement container,
436 PartialRelationInterpretation relationInterpretation,
437 PartialRelationInterpretation inverseRelationInterpretation,
438 Function0<DefinedElement> constructor,
439 List<ObjectCreationInterpretationData> recursiceObjectCreations,
440 ScopePropagator scopePropagator
441 ) {
442 val newElement = constructor.apply
443 if(nameNewElement) {
444 newElement.name = '''new «interpretation.newElements.size»'''
445 }
446
447 // Types
448 typeInterpretation.elements += newElement
449 if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
450 typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
451 }
452 // ContainmentRelation
453 val newLink1 = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
454 relationInterpretation.relationlinks+=newLink1
455 // Inverse Containment
456 val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container]
457 inverseRelationInterpretation.relationlinks+=newLink2
458
459 // Scope propagation
460 scopePropagator.decrementTypeScope(typeInterpretation)
461
462 // Existence
463 interpretation.newElements+=newElement
464
465 // Do recursive object creation
466 for(newConstructor : recursiceObjectCreations) {
467 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
468 }
469
470 return newElement
471 }
472
473 protected def createObjectActionWithContainment(
474 boolean nameNewElement,
475 PartialInterpretation interpretation,
476 PartialTypeInterpratation typeInterpretation,
477 DefinedElement container,
478 PartialRelationInterpretation relationInterpretation,
479 Function0<DefinedElement> constructor,
480 List<ObjectCreationInterpretationData> recursiceObjectCreations,
481 ScopePropagator scopePropagator
482 ) {
483 val newElement = constructor.apply
484 if(nameNewElement) {
485 newElement.name = '''new «interpretation.newElements.size»'''
486 }
487
488 // Types
489 typeInterpretation.elements += newElement
490 if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
491 typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
492 }
493 // ContainmentRelation
494 val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement]
495 relationInterpretation.relationlinks+=newLink
496
497 // Scope propagation
498 scopePropagator.decrementTypeScope(typeInterpretation)
499
500 // Existence
501 interpretation.newElements+=newElement
502
503 // Do recursive object creation
504 for(newConstructor : recursiceObjectCreations) {
505 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
506 }
507
508 return newElement
509 }
510
511 protected def createObjectAction(
512 boolean nameNewElement,
513 PartialInterpretation interpretation,
514 PartialTypeInterpratation typeInterpretation,
515 Function0<DefinedElement> constructor,
516 List<ObjectCreationInterpretationData> recursiceObjectCreations,
517 ScopePropagator scopePropagator)
518 {
519 val newElement = constructor.apply
520 if(nameNewElement) {
521 newElement.name = '''new «interpretation.newElements.size»'''
522 }
523
524 // Types
525 typeInterpretation.elements += newElement
526 if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
527 typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement]
528 }
529
530 // Scope propagation
531 scopePropagator.decrementTypeScope(typeInterpretation)
532
533 // Existence
534 interpretation.newElements+=newElement
535
536 // Do recursive object creation
537 for(newConstructor : recursiceObjectCreations) {
538 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
539 }
540
541 return newElement
542 }
543
544 protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg, PartialRelationInterpretation relationInterpretation) {
545 val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]
546 relationInterpretation.relationlinks += link
547 }
548
549 protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) {
550 val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg]
551 relationInterpretation.relationlinks += link
552 val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src]
553 inverseInterpretation.relationlinks += inverseLink
554 }
555}
556
557@Data
558class ObjectCreationInterpretationData {
559 PartialInterpretation interpretation
560 PartialTypeInterpratation typeInterpretation
561 PartialRelationInterpretation containerInterpretation
562 PartialRelationInterpretation containerInverseInterpretation
563 Function0<DefinedElement> constructor
564 List<ObjectCreationInterpretationData> recursiveConstructors = new LinkedList
251} 565}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
index 8e264488..26ec7091 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend
@@ -196,8 +196,20 @@ class ParseUtil {
196} 196}
197 197
198class FixedMetamodelProvider implements IMetamodelProvider { 198class FixedMetamodelProvider implements IMetamodelProvider {
199
200 static val EPACKAGE_TO_PLUGIN_MAP = #{
201 PartialinterpretationPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage",
202 LogicproblemPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model",
203 LogiclanguagePackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model"
204 }
205
206 static val EPACKAGE_TO_JAVA_PACKAGE_MAP = #{
207 PartialinterpretationPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation",
208 LogicproblemPackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model.logicproblem",
209 LogiclanguagePackage.eINSTANCE -> "hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage"
210 }
199 211
200 protected val List<EPackage> packages = new LinkedList 212 val List<EPackage> packages = new LinkedList
201 213
202 new() { 214 new() {
203 packages += PartialinterpretationPackage.eINSTANCE 215 packages += PartialinterpretationPackage.eINSTANCE
@@ -213,15 +225,24 @@ class FixedMetamodelProvider implements IMetamodelProvider {
213 } 225 }
214 226
215 override boolean isGeneratedCodeAvailable(EPackage ePackage, ResourceSet set) { 227 override boolean isGeneratedCodeAvailable(EPackage ePackage, ResourceSet set) {
216 true 228 EPACKAGE_TO_PLUGIN_MAP.containsKey(ePackage)
217 } 229 }
218 230
219 override String getModelPluginId(EPackage ePackage, ResourceSet set) { 231 override String getModelPluginId(EPackage ePackage, ResourceSet set) {
220 return "hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage" 232 EPACKAGE_TO_PLUGIN_MAP.get(ePackage)
221 } 233 }
222 234
223 override String getQualifiedClassName(EClassifier classifier, EObject context) { 235 override String getQualifiedClassName(EClassifier classifier, EObject context) {
224 classifier.name 236 val instanceClassName = classifier.instanceClassName
237 if (instanceClassName !== null) {
238 return instanceClassName
239 }
240 val javaPackage = EPACKAGE_TO_JAVA_PACKAGE_MAP.get(classifier.EPackage)
241 if (javaPackage !== null) {
242 javaPackage + "." + classifier.name
243 } else {
244 null
245 }
225 } 246 }
226 247
227 override loadEPackage(String uri, ResourceSet resourceSet) { 248 override loadEPackage(String uri, ResourceSet resourceSet) {
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-05 20:55:13 +0000