diff options
Diffstat (limited to 'Solvers/VIATRA-Solver')
32 files changed, 1760 insertions, 668 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index b9da0f0b..f5eb5514 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF | |||
@@ -8,7 +8,8 @@ Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, | |||
8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, | 8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, |
9 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, | 9 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, |
10 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, | 10 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, |
11 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries | 11 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries, |
12 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules | ||
12 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 13 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
13 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", | 14 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", |
14 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 15 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
@@ -24,9 +25,8 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | |||
24 | org.eclipse.xtext;bundle-version="2.10.0", | 25 | org.eclipse.xtext;bundle-version="2.10.0", |
25 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="2.0.0", | 26 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="2.0.0", |
26 | org.eclipse.xtext.xbase;bundle-version="2.10.0", | 27 | org.eclipse.xtext.xbase;bundle-version="2.10.0", |
27 | com.microsoft.z3;bundle-version="4.8.5", | ||
28 | hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0", | 28 | hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0", |
29 | org.eclipse.viatra.query.runtime.rete;bundle-version="2.0.0" | 29 | org.eclipse.viatra.query.runtime.rete;bundle-version="2.0.0", |
30 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | 30 | com.microsoft.z3 |
31 | Bundle-RequiredExecutionEnvironment: JavaSE-11 | ||
31 | Import-Package: org.apache.log4j | 32 | Import-Package: org.apache.log4j |
32 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend new file mode 100644 index 00000000..bd5bf807 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend | |||
@@ -0,0 +1,47 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | ||
2 | |||
3 | class ModelGenerationStatistics { | ||
4 | public var long transformationExecutionTime = 0 | ||
5 | |||
6 | synchronized def addExecutionTime(long amount) { | ||
7 | transformationExecutionTime += amount | ||
8 | } | ||
9 | |||
10 | public var long scopePropagationTime = 0 | ||
11 | |||
12 | synchronized def addScopePropagationTime(long amount) { | ||
13 | scopePropagationTime += amount | ||
14 | } | ||
15 | |||
16 | public var long mustRelationPropagationTime = 0 | ||
17 | |||
18 | synchronized def addMustRelationPropagationTime(long amount) { | ||
19 | mustRelationPropagationTime += amount | ||
20 | } | ||
21 | |||
22 | public var long preliminaryTypeAnalisisTime = 0 | ||
23 | |||
24 | public var int decisionsTried = 0 | ||
25 | |||
26 | synchronized def incrementDecisionCount() { | ||
27 | decisionsTried++ | ||
28 | } | ||
29 | |||
30 | public var int transformationInvocations | ||
31 | |||
32 | synchronized def incrementTransformationCount() { | ||
33 | transformationInvocations++ | ||
34 | } | ||
35 | |||
36 | public var int scopePropagatorInvocations | ||
37 | |||
38 | synchronized def incrementScopePropagationCount() { | ||
39 | scopePropagatorInvocations++ | ||
40 | } | ||
41 | |||
42 | public var int scopePropagatorSolverInvocations | ||
43 | |||
44 | synchronized def incrementScopePropagationSolverCount() { | ||
45 | scopePropagatorSolverInvocations++ | ||
46 | } | ||
47 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend new file mode 100644 index 00000000..9296a0be --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend | |||
@@ -0,0 +1,44 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | ||
2 | |||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
25 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
26 | import java.util.Collection | ||
27 | import java.util.List | ||
28 | import java.util.Map | ||
29 | import java.util.Set | ||
30 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | ||
31 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
32 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
33 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
34 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
35 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
36 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
37 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
38 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | ||
39 | import org.eclipse.xtend.lib.annotations.Data | ||
40 | |||
41 | enum TypeInferenceMethod { | ||
42 | Generic, | ||
43 | PreliminaryAnalysis | ||
44 | } \ 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/cardinality/ExtendedLinearExpressionBuilderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend new file mode 100644 index 00000000..6054affe --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend | |||
@@ -0,0 +1,140 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import java.util.ArrayList | ||
7 | import java.util.HashMap | ||
8 | import java.util.HashSet | ||
9 | import java.util.List | ||
10 | import java.util.Map | ||
11 | import java.util.Set | ||
12 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
13 | import org.eclipse.xtend.lib.annotations.Accessors | ||
14 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
15 | |||
16 | interface BoundSaturationListener { | ||
17 | def void boundsSaturated(Integer lower, Integer upper) | ||
18 | } | ||
19 | |||
20 | interface ExtendedLinearExpressionBuilderFactory { | ||
21 | def ExtendedLinearExpressionBuilder createBuilder() | ||
22 | |||
23 | def Dimension getDimension(IPatternMatch patternMatch) | ||
24 | } | ||
25 | |||
26 | interface ExtendedLinearExpressionBuilder extends LinearTypeExpressionBuilder { | ||
27 | override ExtendedLinearExpressionBuilder add(int scale, Type type) | ||
28 | |||
29 | def ExtendedLinearExpressionBuilder add(int scale, IPatternMatch patternMatch) | ||
30 | |||
31 | def ExtendedLinearExpressionBuilder add(int scale, Dimension dimension) | ||
32 | |||
33 | def LinearBoundedExpression build(BoundSaturationListener listener) | ||
34 | } | ||
35 | |||
36 | class ExtendedPolyhedronBuilder implements ExtendedLinearExpressionBuilderFactory { | ||
37 | val Map<Type, LinearBoundedExpression> typeBounds | ||
38 | val Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache | ||
39 | |||
40 | val ImmutableList.Builder<Dimension> dimensions = ImmutableList.builder | ||
41 | val Set<LinearConstraint> constraints = new HashSet | ||
42 | val Set<LinearBoundedExpression> expressionsToSaturate = new HashSet | ||
43 | val Map<IPatternMatch, Dimension> patternMatchCounts = new HashMap | ||
44 | @Accessors(PUBLIC_GETTER) val List<Pair<LinearBoundedExpression, BoundSaturationListener>> saturationListeners = new ArrayList | ||
45 | |||
46 | new(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
47 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
48 | this.typeBounds = typeBounds | ||
49 | this.expressionsCache = new HashMap(initialExpressionsCache) | ||
50 | dimensions.addAll(polyhedron.dimensions) | ||
51 | constraints.addAll(polyhedron.constraints) | ||
52 | expressionsToSaturate.addAll(polyhedron.expressionsToSaturate) | ||
53 | } | ||
54 | |||
55 | override createBuilder() { | ||
56 | new ExtendedLinearExpressionBuilderImpl(this) | ||
57 | } | ||
58 | |||
59 | override getDimension(IPatternMatch patternMatch) { | ||
60 | patternMatchCounts.computeIfAbsent(patternMatch) [ key | | ||
61 | val dimension = new Dimension(key.toString, 0, null) | ||
62 | dimensions.add(dimension) | ||
63 | dimension | ||
64 | ] | ||
65 | } | ||
66 | |||
67 | def buildPolyhedron() { | ||
68 | new Polyhedron( | ||
69 | dimensions.build, | ||
70 | ImmutableList.copyOf(constraints), | ||
71 | ImmutableList.copyOf(expressionsToSaturate) | ||
72 | ) | ||
73 | } | ||
74 | |||
75 | @FinalFieldsConstructor | ||
76 | private static class ExtendedLinearExpressionBuilderImpl implements ExtendedLinearExpressionBuilder { | ||
77 | val ExtendedPolyhedronBuilder polyhedronBuilder | ||
78 | |||
79 | val Map<Dimension, Integer> coefficients = new HashMap | ||
80 | |||
81 | override add(int scale, Type type) { | ||
82 | val expression = polyhedronBuilder.typeBounds.get(type) | ||
83 | if (expression === null) { | ||
84 | throw new IllegalArgumentException("Unknown Type: " + type) | ||
85 | } | ||
86 | add(scale, expression) | ||
87 | } | ||
88 | |||
89 | override add(int scale, IPatternMatch patternMatch) { | ||
90 | val dimension = polyhedronBuilder.getDimension(patternMatch) | ||
91 | add(scale, dimension) | ||
92 | } | ||
93 | |||
94 | private def add(int scale, LinearBoundedExpression expression) { | ||
95 | switch (expression) { | ||
96 | Dimension: add(scale, expression) | ||
97 | LinearConstraint: add(scale, expression.coefficients) | ||
98 | default: throw new IllegalArgumentException("Unknown LinearBoundedExpression: " + expression) | ||
99 | } | ||
100 | } | ||
101 | |||
102 | private def add(int scale, Map<Dimension, Integer> coefficients) { | ||
103 | for (pair : coefficients.entrySet) { | ||
104 | add(scale * pair.value, pair.key) | ||
105 | } | ||
106 | this | ||
107 | } | ||
108 | |||
109 | override add(int scale, Dimension dimension) { | ||
110 | coefficients.merge(dimension, scale)[a, b|a + b] | ||
111 | this | ||
112 | } | ||
113 | |||
114 | override build() { | ||
115 | val filteredCoefficients = ImmutableMap.copyOf(coefficients.filter [ _, coefficient | | ||
116 | coefficient != 0 | ||
117 | ]) | ||
118 | polyhedronBuilder.expressionsCache.computeIfAbsent(filteredCoefficients) [ map | | ||
119 | if (map.size == 1) { | ||
120 | val pair = map.entrySet.head | ||
121 | if (pair.value == 1) { | ||
122 | return pair.key | ||
123 | } | ||
124 | } | ||
125 | val constraint = new LinearConstraint(map) | ||
126 | polyhedronBuilder.constraints.add(constraint) | ||
127 | constraint | ||
128 | ] | ||
129 | } | ||
130 | |||
131 | override build(BoundSaturationListener listener) { | ||
132 | val expression = build() | ||
133 | if (listener !== null) { | ||
134 | polyhedronBuilder.expressionsToSaturate.add(expression) | ||
135 | polyhedronBuilder.saturationListeners.add(expression -> listener) | ||
136 | } | ||
137 | expression | ||
138 | } | ||
139 | } | ||
140 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..32923396 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,63 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
5 | import java.util.Collection | ||
6 | import java.util.Map | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
8 | |||
9 | interface PolyhedronExtensionOperator { | ||
10 | def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory) | ||
11 | } | ||
12 | |||
13 | class ExtendedPolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { | ||
14 | val PolyhedronSolver solver | ||
15 | val Collection<PolyhedronExtensionOperator> extensionOperators | ||
16 | |||
17 | var Map<Type, LinearBoundedExpression> typeBounds | ||
18 | var Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache | ||
19 | |||
20 | new(PolyhedronSolver solver, Collection<PolyhedronExtensionOperator> extensionOperators, | ||
21 | ModelGenerationStatistics statistics) { | ||
22 | super(statistics) | ||
23 | this.solver = solver | ||
24 | this.extensionOperators = extensionOperators | ||
25 | } | ||
26 | |||
27 | override setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
28 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
29 | super.setPolyhedron(polyhedron, typeBounds, initialExpressionsCache) | ||
30 | this.typeBounds = typeBounds | ||
31 | this.initialExpressionsCache = initialExpressionsCache | ||
32 | } | ||
33 | |||
34 | override isRelevantRelation(Relation relation) { | ||
35 | true | ||
36 | } | ||
37 | |||
38 | override protected doSaturate() { | ||
39 | val builder = new ExtendedPolyhedronBuilder(polyhedron, typeBounds, initialExpressionsCache) | ||
40 | for (extensionOperator : extensionOperators) { | ||
41 | extensionOperator.extendPolyhedron(builder) | ||
42 | } | ||
43 | val extendedPolyhedron = builder.buildPolyhedron() | ||
44 | val saturationOperator = solver.createSaturationOperator(extendedPolyhedron) | ||
45 | val result = try { | ||
46 | saturationOperator.saturate() | ||
47 | } finally { | ||
48 | saturationOperator.close() | ||
49 | } | ||
50 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
51 | // The partial model cannot be refined any more, we can't provide objective bounds. | ||
52 | for (pair : builder.saturationListeners) { | ||
53 | pair.value.boundsSaturated(null, null) | ||
54 | } | ||
55 | return false | ||
56 | } | ||
57 | for (pair : builder.saturationListeners) { | ||
58 | val expression = pair.key | ||
59 | pair.value.boundsSaturated(expression.lowerBound, expression.upperBound) | ||
60 | } | ||
61 | true | ||
62 | } | ||
63 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend index 8c21ca1d..31f98e36 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend | |||
@@ -3,8 +3,10 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
6 | import java.util.Map | ||
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 7 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
7 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
8 | 10 | ||
9 | interface LinearTypeExpressionBuilderFactory { | 11 | interface LinearTypeExpressionBuilderFactory { |
10 | def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName) | 12 | def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName) |
@@ -24,7 +26,7 @@ interface RelationConstraintUpdater { | |||
24 | } | 26 | } |
25 | 27 | ||
26 | interface LinearTypeConstraintHint { | 28 | interface LinearTypeConstraintHint { |
27 | def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator) | 29 | def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) |
28 | 30 | ||
29 | def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) | 31 | def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) |
30 | } | 32 | } |
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 c28d4caa..ad8f94ab 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 | |||
@@ -1,7 +1,5 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import com.google.common.cache.Cache | ||
4 | import com.google.common.cache.CacheBuilder | ||
5 | import com.google.common.collect.ImmutableList | 3 | import com.google.common.collect.ImmutableList |
6 | import com.google.common.collect.ImmutableMap | 4 | import com.google.common.collect.ImmutableMap |
7 | import com.google.common.collect.ImmutableSet | 5 | import com.google.common.collect.ImmutableSet |
@@ -23,7 +21,6 @@ import java.util.HashSet | |||
23 | import java.util.List | 21 | import java.util.List |
24 | import java.util.Map | 22 | import java.util.Map |
25 | import java.util.Set | 23 | import java.util.Set |
26 | import javax.naming.OperationNotSupportedException | ||
27 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 24 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 25 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 26 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
@@ -32,31 +29,29 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
33 | 30 | ||
34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | 31 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { |
35 | static val CACHE_SIZE = 10000 | ||
36 | |||
37 | val boolean updateHeuristic | 32 | val boolean updateHeuristic |
38 | val Map<Scope, LinearBoundedExpression> scopeBounds | 33 | val Map<Scope, LinearBoundedExpression> scopeBounds |
39 | val LinearBoundedExpression topLevelBounds | 34 | val LinearBoundedExpression topLevelBounds |
40 | val Polyhedron polyhedron | 35 | val Polyhedron polyhedron |
41 | val PolyhedronSaturationOperator operator | 36 | val PolyhedronScopePropagatorStrategy strategy |
42 | val Set<Relation> relevantRelations | 37 | val Set<Relation> relevantRelations |
43 | val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build | ||
44 | List<RelationConstraintUpdater> updaters = emptyList | 38 | List<RelationConstraintUpdater> updaters = emptyList |
45 | 39 | ||
46 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, | 40 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, |
47 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | 41 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, |
48 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 42 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
49 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | 43 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
50 | Collection<LinearTypeConstraintHint> hints, PolyhedronSolver solver, boolean propagateRelations, | 44 | Collection<LinearTypeConstraintHint> hints, PolyhedronScopePropagatorStrategy strategy, |
51 | boolean updateHeuristic) { | 45 | boolean propagateRelations, boolean updateHeuristic) { |
52 | super(p, statistics) | 46 | super(p, statistics) |
53 | this.updateHeuristic = updateHeuristic | 47 | this.updateHeuristic = updateHeuristic |
48 | this.strategy = strategy | ||
54 | val builder = new PolyhedronBuilder(p) | 49 | val builder = new PolyhedronBuilder(p) |
55 | builder.buildPolyhedron(possibleNewDynamicTypes) | 50 | builder.buildPolyhedron(possibleNewDynamicTypes) |
56 | scopeBounds = builder.scopeBounds | 51 | scopeBounds = builder.scopeBounds |
57 | topLevelBounds = builder.topLevelBounds | 52 | topLevelBounds = builder.topLevelBounds |
58 | polyhedron = builder.polyhedron | 53 | polyhedron = builder.polyhedron |
59 | operator = solver.createSaturationOperator(polyhedron) | 54 | strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache) |
60 | propagateAllScopeConstraints() | 55 | propagateAllScopeConstraints() |
61 | if (propagateRelations) { | 56 | if (propagateRelations) { |
62 | val maximumNumberOfNewNodes = topLevelBounds.upperBound | 57 | val maximumNumberOfNewNodes = topLevelBounds.upperBound |
@@ -80,30 +75,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
80 | resetBounds() | 75 | resetBounds() |
81 | populatePolyhedronFromScope() | 76 | populatePolyhedronFromScope() |
82 | // println(polyhedron) | 77 | // println(polyhedron) |
83 | val signature = polyhedron.createSignature | 78 | if (strategy.saturate) { |
84 | val cachedSignature = cache.getIfPresent(signature) | 79 | populateScopesFromPolyhedron() |
85 | switch (cachedSignature) { | 80 | } else { |
86 | case null: { | 81 | setScopesInvalid() |
87 | statistics.incrementScopePropagationSolverCount | ||
88 | val result = operator.saturate() | ||
89 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
90 | cache.put(signature, PolyhedronSignature.EMPTY) | ||
91 | // println("INVALID") | ||
92 | setScopesInvalid() | ||
93 | } else { | ||
94 | val resultSignature = polyhedron.createSignature | ||
95 | cache.put(signature, resultSignature) | ||
96 | populateScopesFromPolyhedron() | ||
97 | } | ||
98 | } | ||
99 | case PolyhedronSignature.EMPTY: | ||
100 | setScopesInvalid() | ||
101 | PolyhedronSignature.Bounds: { | ||
102 | polyhedron.applySignature(signature) | ||
103 | populateScopesFromPolyhedron() | ||
104 | } | ||
105 | default: | ||
106 | throw new IllegalStateException("Unknown polyhedron signature: " + signature) | ||
107 | } | 82 | } |
108 | // println(polyhedron) | 83 | // println(polyhedron) |
109 | if (updateHeuristic) { | 84 | if (updateHeuristic) { |
@@ -112,9 +87,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
112 | } | 87 | } |
113 | 88 | ||
114 | override isPropagationNeededAfterAdditionToRelation(Relation r) { | 89 | override isPropagationNeededAfterAdditionToRelation(Relation r) { |
115 | relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r) | 90 | relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r) |
116 | } | 91 | } |
117 | 92 | ||
118 | override isQueryEngineFlushRequiredBeforePropagation() { | 93 | override isQueryEngineFlushRequiredBeforePropagation() { |
119 | true | 94 | true |
120 | } | 95 | } |
@@ -253,7 +228,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
253 | } | 228 | } |
254 | buildRelevantRelations(constraints.keySet) | 229 | buildRelevantRelations(constraints.keySet) |
255 | for (hint : hints) { | 230 | for (hint : hints) { |
256 | updatersBuilder.add(hint.createConstraintUpdater(this)) | 231 | val updater = hint.createConstraintUpdater(this) |
232 | if (updater !== null) { | ||
233 | updatersBuilder.add(updater) | ||
234 | } | ||
257 | } | 235 | } |
258 | updaters = updatersBuilder.build | 236 | updaters = updatersBuilder.build |
259 | addCachedConstraintsToPolyhedron() | 237 | addCachedConstraintsToPolyhedron() |
@@ -410,7 +388,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
410 | for (scope : p.scopes) { | 388 | for (scope : p.scopes) { |
411 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | 389 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { |
412 | PartialPrimitiveInterpretation: | 390 | PartialPrimitiveInterpretation: |
413 | throw new OperationNotSupportedException("Primitive type scopes are not yet implemented") | 391 | throw new IllegalStateException("Primitive type scopes are not yet implemented") |
414 | PartialComplexTypeInterpretation: { | 392 | PartialComplexTypeInterpretation: { |
415 | val complexType = targetTypeInterpretation.interpretationOf | 393 | val complexType = targetTypeInterpretation.interpretationOf |
416 | val typeBound = typeBounds.get(complexType) | 394 | val typeBound = typeBounds.get(complexType) |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..f93dcd18 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,92 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.cache.Cache | ||
4 | import com.google.common.cache.CacheBuilder | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
8 | import java.util.Map | ||
9 | import org.eclipse.xtend.lib.annotations.Accessors | ||
10 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
11 | |||
12 | @FinalFieldsConstructor | ||
13 | abstract class PolyhedronScopePropagatorStrategy { | ||
14 | val ModelGenerationStatistics statistics | ||
15 | |||
16 | @Accessors(PUBLIC_GETTER) var Polyhedron polyhedron | ||
17 | |||
18 | def void setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
19 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
20 | if (this.polyhedron !== null) { | ||
21 | throw new IllegalStateException("polyhedron was already set") | ||
22 | } | ||
23 | this.polyhedron = polyhedron | ||
24 | initialize() | ||
25 | } | ||
26 | |||
27 | def boolean saturate() { | ||
28 | if (polyhedron === null) { | ||
29 | throw new IllegalStateException("polyhedron was not set") | ||
30 | } | ||
31 | doSaturate() | ||
32 | } | ||
33 | |||
34 | def boolean isRelevantRelation(Relation relation) { | ||
35 | false | ||
36 | } | ||
37 | |||
38 | protected def incrementScopePropagationSolverCount() { | ||
39 | statistics.incrementScopePropagationSolverCount() | ||
40 | } | ||
41 | |||
42 | protected def void initialize() { | ||
43 | } | ||
44 | |||
45 | protected def boolean doSaturate() | ||
46 | } | ||
47 | |||
48 | @FinalFieldsConstructor | ||
49 | class CachingSimplePolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { | ||
50 | static val CACHE_SIZE = 10000 | ||
51 | |||
52 | val PolyhedronSolver solver | ||
53 | |||
54 | val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build | ||
55 | var PolyhedronSaturationOperator operator | ||
56 | |||
57 | new(PolyhedronSolver solver, ModelGenerationStatistics statistics) { | ||
58 | super(statistics) | ||
59 | this.solver = solver | ||
60 | } | ||
61 | |||
62 | override protected initialize() { | ||
63 | operator = solver.createSaturationOperator(polyhedron) | ||
64 | } | ||
65 | |||
66 | override protected doSaturate() { | ||
67 | val signature = polyhedron.createSignature | ||
68 | val cachedSignature = cache.getIfPresent(signature) | ||
69 | switch (cachedSignature) { | ||
70 | case null: { | ||
71 | incrementScopePropagationSolverCount() | ||
72 | val result = operator.saturate() | ||
73 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
74 | cache.put(signature, PolyhedronSignature.EMPTY) | ||
75 | false | ||
76 | } else { | ||
77 | val resultSignature = polyhedron.createSignature | ||
78 | cache.put(signature, resultSignature) | ||
79 | true | ||
80 | } | ||
81 | } | ||
82 | case PolyhedronSignature.EMPTY: | ||
83 | false | ||
84 | PolyhedronSignature.Bounds: { | ||
85 | polyhedron.applySignature(signature) | ||
86 | true | ||
87 | } | ||
88 | default: | ||
89 | throw new IllegalStateException("Unknown polyhedron signature: " + signature) | ||
90 | } | ||
91 | } | ||
92 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend index 4e046190..21bd2d9e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend | |||
@@ -116,7 +116,7 @@ abstract class PolyhedronSignature { | |||
116 | } | 116 | } |
117 | 117 | ||
118 | @Accessors | 118 | @Accessors |
119 | abstract class LinearBoundedExpression { | 119 | class Bounds { |
120 | var Integer lowerBound | 120 | var Integer lowerBound |
121 | var Integer upperBound | 121 | var Integer upperBound |
122 | 122 | ||
@@ -132,12 +132,19 @@ abstract class LinearBoundedExpression { | |||
132 | } | 132 | } |
133 | } | 133 | } |
134 | 134 | ||
135 | def void assertBetween(Integer tighterLowerBound, Integer tighterUpperBound) { | ||
136 | tightenLowerBound(tighterLowerBound) | ||
137 | tightenUpperBound(tighterUpperBound) | ||
138 | } | ||
139 | |||
135 | def void assertEqualsTo(int bound) { | 140 | def void assertEqualsTo(int bound) { |
136 | tightenLowerBound(bound) | 141 | assertBetween(bound, bound) |
137 | tightenUpperBound(bound) | ||
138 | } | 142 | } |
139 | } | 143 | } |
140 | 144 | ||
145 | abstract class LinearBoundedExpression extends Bounds { | ||
146 | } | ||
147 | |||
141 | @Accessors | 148 | @Accessors |
142 | class Dimension extends LinearBoundedExpression { | 149 | class Dimension extends LinearBoundedExpression { |
143 | val String name | 150 | val String name |
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 93b83577..cacba3c6 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 | |||
@@ -19,6 +19,8 @@ class ScopePropagator { | |||
19 | val Map<PartialTypeInterpratation, Scope> type2Scope | 19 | val Map<PartialTypeInterpratation, Scope> type2Scope |
20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes | 20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes |
21 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes | 21 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes |
22 | |||
23 | @Accessors(PUBLIC_GETTER) var scopePropagationNeeded = false | ||
22 | 24 | ||
23 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { | 25 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { |
24 | partialInterpretation = p | 26 | partialInterpretation = p |
@@ -64,7 +66,8 @@ class ScopePropagator { | |||
64 | copyScopeBoundsToHeuristic() | 66 | copyScopeBoundsToHeuristic() |
65 | } | 67 | } |
66 | 68 | ||
67 | def propagateAllScopeConstraints() { | 69 | def void propagateAllScopeConstraints() { |
70 | scopePropagationNeeded = false | ||
68 | if (!valid) { | 71 | if (!valid) { |
69 | return | 72 | return |
70 | } | 73 | } |
@@ -93,6 +96,7 @@ class ScopePropagator { | |||
93 | if (isPrimitive) { | 96 | if (isPrimitive) { |
94 | return | 97 | return |
95 | } | 98 | } |
99 | scopePropagationNeeded = true | ||
96 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 100 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
97 | val targetScope = type2Scope.get(t) | 101 | val targetScope = type2Scope.get(t) |
98 | if (targetScope !== null) { | 102 | if (targetScope !== null) { |
@@ -117,6 +121,12 @@ class ScopePropagator { | |||
117 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | 121 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] |
118 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 122 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
119 | } | 123 | } |
124 | |||
125 | def addedToRelation(Relation r) { | ||
126 | if (isPropagationNeededAfterAdditionToRelation(r)) { | ||
127 | scopePropagationNeeded = true | ||
128 | } | ||
129 | } | ||
120 | 130 | ||
121 | protected def setScopesInvalid() { | 131 | protected def setScopesInvalid() { |
122 | partialInterpretation.minNewElements = Integer.MAX_VALUE | 132 | partialInterpretation.minNewElements = Integer.MAX_VALUE |
@@ -127,7 +137,7 @@ class ScopePropagator { | |||
127 | } | 137 | } |
128 | } | 138 | } |
129 | 139 | ||
130 | def isPropagationNeededAfterAdditionToRelation(Relation r) { | 140 | protected def isPropagationNeededAfterAdditionToRelation(Relation r) { |
131 | false | 141 | false |
132 | } | 142 | } |
133 | 143 | ||
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 80bc3844..edf92343 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 | |||
@@ -25,12 +25,13 @@ import java.util.HashMap | |||
25 | import java.util.Map | 25 | import java.util.Map |
26 | import org.eclipse.emf.ecore.EAttribute | 26 | import org.eclipse.emf.ecore.EAttribute |
27 | import org.eclipse.emf.ecore.EReference | 27 | import org.eclipse.emf.ecore.EReference |
28 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
28 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
29 | import org.eclipse.xtend.lib.annotations.Accessors | 30 | import org.eclipse.xtend.lib.annotations.Accessors |
31 | import org.eclipse.xtend.lib.annotations.Data | ||
32 | import org.eclipse.xtend2.lib.StringConcatenationClient | ||
30 | 33 | ||
31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 34 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
32 | import org.eclipse.xtend.lib.annotations.Data | ||
33 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
34 | 35 | ||
35 | @Data class PatternGeneratorResult { | 36 | @Data class PatternGeneratorResult { |
36 | CharSequence patternText | 37 | CharSequence patternText |
@@ -38,6 +39,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | |||
38 | HashMap<PConstraint,String> constraint2CurrentPreconditionName | 39 | HashMap<PConstraint,String> constraint2CurrentPreconditionName |
39 | } | 40 | } |
40 | 41 | ||
42 | interface UnitPropagationPatternGenerator { | ||
43 | def Map<Relation, String> getMustPatterns() | ||
44 | |||
45 | def Map<Relation, String> getMustNotPatterns() | ||
46 | |||
47 | def StringConcatenationClient getAdditionalPatterns(PatternGenerator generator, Map<String, PQuery> fqn2PQuery) | ||
48 | } | ||
49 | |||
41 | class PatternGenerator { | 50 | class PatternGenerator { |
42 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) | 51 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) |
43 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( | 52 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( |
@@ -157,7 +166,8 @@ class PatternGenerator { | |||
157 | Map<String, PQuery> fqn2PQuery, | 166 | Map<String, PQuery> fqn2PQuery, |
158 | TypeAnalysisResult typeAnalysisResult, | 167 | TypeAnalysisResult typeAnalysisResult, |
159 | RelationConstraints constraints, | 168 | RelationConstraints constraints, |
160 | Collection<LinearTypeConstraintHint> hints | 169 | Collection<LinearTypeConstraintHint> hints, |
170 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators | ||
161 | ) { | 171 | ) { |
162 | val first = | 172 | val first = |
163 | ''' | 173 | ''' |
@@ -313,7 +323,7 @@ class PatternGenerator { | |||
313 | ////////// | 323 | ////////// |
314 | // 1.2 Relation Declaration Indexers | 324 | // 1.2 Relation Declaration Indexers |
315 | ////////// | 325 | ////////// |
316 | «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),fqn2PQuery)» | 326 | «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),unitPropagationPatternGenerators,fqn2PQuery)» |
317 | 327 | ||
318 | ////////// | 328 | ////////// |
319 | // 1.3 Relation Definition Indexers | 329 | // 1.3 Relation Definition Indexers |
@@ -359,13 +369,16 @@ class PatternGenerator { | |||
359 | ////////// | 369 | ////////// |
360 | // 4.3 Relation refinement | 370 | // 4.3 Relation refinement |
361 | ////////// | 371 | ////////// |
362 | «relationRefinementGenerator.generateRefineReference(problem)» | 372 | «relationRefinementGenerator.generateRefineReference(problem, unitPropagationPatternGenerators)» |
363 | 373 | ||
364 | ////////// | 374 | ////////// |
365 | // 5 Hints | 375 | // 5 Hints |
366 | ////////// | 376 | ////////// |
367 | «FOR hint : hints» | 377 | «FOR hint : hints» |
368 | «hint.getAdditionalPatterns(this)» | 378 | «hint.getAdditionalPatterns(this, fqn2PQuery)» |
379 | «ENDFOR» | ||
380 | «FOR generator : unitPropagationPatternGenerators» | ||
381 | «generator.getAdditionalPatterns(this, fqn2PQuery)» | ||
369 | «ENDFOR» | 382 | «ENDFOR» |
370 | 383 | ||
371 | ////////// | 384 | ////////// |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index d57705ce..2e786286 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend | |||
@@ -36,9 +36,10 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
36 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries | 36 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries |
37 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries | 37 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries |
38 | public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery | 38 | public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery |
39 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 39 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
40 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 40 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
41 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 41 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries |
42 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries | ||
42 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns | 43 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns |
43 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns | 44 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns |
44 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries | 45 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries |
@@ -56,7 +57,7 @@ class ModalPatternQueries { | |||
56 | class UnifinishedMultiplicityQueries { | 57 | class UnifinishedMultiplicityQueries { |
57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery | 58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery |
58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery | 59 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery |
59 | 60 | ||
60 | def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() { | 61 | def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() { |
61 | val builder = ImmutableSet.builder | 62 | val builder = ImmutableSet.builder |
62 | if (existingMultiplicityQuery !== null) { | 63 | if (existingMultiplicityQuery !== null) { |
@@ -70,13 +71,13 @@ class UnifinishedMultiplicityQueries { | |||
70 | } | 71 | } |
71 | 72 | ||
72 | class PatternProvider { | 73 | class PatternProvider { |
73 | |||
74 | val TypeAnalysis typeAnalysis = new TypeAnalysis | 74 | val TypeAnalysis typeAnalysis = new TypeAnalysis |
75 | 75 | ||
76 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, | 76 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, |
77 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, | 77 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, |
78 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, | 78 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, |
79 | Collection<LinearTypeConstraintHint> hints, boolean writeToFile) { | 79 | Collection<LinearTypeConstraintHint> hints, |
80 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, boolean writeToFile) { | ||
80 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] | 81 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] |
81 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) | 82 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) |
82 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { | 83 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { |
@@ -89,15 +90,16 @@ class PatternProvider { | |||
89 | null | 90 | null |
90 | } | 91 | } |
91 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, | 92 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, |
92 | typeAnalysisResult, relationConstraints, hints) | 93 | typeAnalysisResult, relationConstraints, hints, unitPropagationPatternGenerators) |
93 | if (writeToFile) { | 94 | if (writeToFile) { |
94 | workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText) | 95 | workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText) |
95 | } | 96 | } |
96 | val ParseUtil parseUtil = new ParseUtil | 97 | val ParseUtil parseUtil = new ParseUtil |
97 | val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) | 98 | val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) |
98 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, | 99 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, |
99 | patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName, | 100 | patternGeneratorResult.constraint2MustPreconditionName, |
100 | relationConstraints, generatedQueries) | 101 | patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints, |
102 | unitPropagationPatternGenerators, generatedQueries) | ||
101 | return runtimeQueries | 103 | return runtimeQueries |
102 | } | 104 | } |
103 | 105 | ||
@@ -109,14 +111,16 @@ class PatternProvider { | |||
109 | HashMap<PConstraint, String> mustUnitPropagationTrace, | 111 | HashMap<PConstraint, String> mustUnitPropagationTrace, |
110 | HashMap<PConstraint, String> currentUnitPropagationTrace, | 112 | HashMap<PConstraint, String> currentUnitPropagationTrace, |
111 | RelationConstraints relationConstraints, | 113 | RelationConstraints relationConstraints, |
114 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, | ||
112 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 115 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries |
113 | ) { | 116 | ) { |
114 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 117 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries = patternGenerator. |
115 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 118 | invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] |
116 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 119 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries = patternGenerator. |
117 | unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] | 120 | unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] |
118 | 121 | ||
119 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) | 122 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries( |
123 | relationConstraints.multiplicityConstraints) | ||
120 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ | 124 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ |
121 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), | 125 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), |
122 | existingInverseMultiplicityQueryName?.lookup(queries)) | 126 | existingInverseMultiplicityQueryName?.lookup(queries)) |
@@ -124,16 +128,22 @@ class PatternProvider { | |||
124 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( | 128 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( |
125 | queries) | 129 | queries) |
126 | 130 | ||
127 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 131 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectsQueries = patternGenerator. |
128 | refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 132 | typeRefinementGenerator.getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [ |
129 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 133 | it.lookup(queries) |
130 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 134 | ] |
131 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 135 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries = patternGenerator. |
132 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 136 | typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [ |
133 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 137 | it.lookup(queries) |
134 | mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] | 138 | ] |
135 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 139 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries = patternGenerator. |
136 | currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] | 140 | relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] |
141 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries = patternGenerator. | ||
142 | relationRefinementGenerator.getMustPropagationQueries(problem, unitPropagationPatternGenerators).mapValues[it.lookup(queries)] | ||
143 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace. | ||
144 | mapValues[it.lookup(queries)] | ||
145 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace. | ||
146 | mapValues[it.lookup(queries)] | ||
137 | 147 | ||
138 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | | 148 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | |
139 | val indexer = patternGenerator.relationDefinitionIndexer | 149 | val indexer = patternGenerator.relationDefinitionIndexer |
@@ -143,7 +153,7 @@ class PatternProvider { | |||
143 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) | 153 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) |
144 | ) | 154 | ) |
145 | ]) | 155 | ]) |
146 | 156 | ||
147 | return new GeneratedPatterns( | 157 | return new GeneratedPatterns( |
148 | invalidWFQueries, | 158 | invalidWFQueries, |
149 | unfinishedWFQueries, | 159 | unfinishedWFQueries, |
@@ -152,6 +162,7 @@ class PatternProvider { | |||
152 | refineObjectsQueries, | 162 | refineObjectsQueries, |
153 | refineTypeQueries, | 163 | refineTypeQueries, |
154 | refineRelationQueries, | 164 | refineRelationQueries, |
165 | mustRelationPropagationQueries, | ||
155 | mustUnitPropagationPreconditionPatterns, | 166 | mustUnitPropagationPreconditionPatterns, |
156 | currentUnitPropagationPreconditionPatterns, | 167 | currentUnitPropagationPreconditionPatterns, |
157 | modalRelationQueries, | 168 | modalRelationQueries, |
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 b4403979..23ba3cad 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 | |||
@@ -1,10 +1,13 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import com.google.common.collect.ImmutableSet | ||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | 5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
10 | import java.util.Collection | ||
8 | import java.util.HashMap | 11 | import java.util.HashMap |
9 | import java.util.List | 12 | import java.util.List |
10 | import java.util.Map | 13 | import java.util.Map |
@@ -14,41 +17,40 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
14 | 17 | ||
15 | class RelationDeclarationIndexer { | 18 | class RelationDeclarationIndexer { |
16 | val PatternGenerator base; | 19 | val PatternGenerator base; |
17 | 20 | ||
18 | new(PatternGenerator base) { | 21 | new(PatternGenerator base) { |
19 | this.base = base | 22 | this.base = base |
20 | } | 23 | } |
21 | 24 | ||
22 | def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, Map<String,PQuery> fqn2PQuery) { | 25 | def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, |
26 | Iterable<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, Map<String, PQuery> fqn2PQuery) { | ||
23 | val upperMultiplicities = new HashMap | 27 | val upperMultiplicities = new HashMap |
24 | problem.annotations.filter(UpperMultiplicityAssertion).forEach[ | 28 | problem.annotations.filter(UpperMultiplicityAssertion).forEach [ |
25 | upperMultiplicities.put(it.relation,it.upper) | 29 | upperMultiplicities.put(it.relation, it.upper) |
26 | ] | 30 | ] |
27 | 31 | val mustNotRelations = ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustNotPatterns.entrySet]. | |
32 | groupBy[key].mapValues[ImmutableSet.copyOf(map[value])]) | ||
33 | |||
28 | return ''' | 34 | return ''' |
29 | «FOR relation : relations» | 35 | «FOR relation : relations» |
30 | «IF base.isDerived(relation)» | 36 | «IF base.isDerived(relation)» |
31 | «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» | 37 | «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» |
32 | «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» | 38 | «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» |
33 | «ELSE» | 39 | «ELSE» |
34 | «generateMustRelation(problem,relation)» | 40 | «generateMustRelation(problem, relation)» |
35 | «generateMayRelation(problem,relation,upperMultiplicities,base.getContainments(problem),base.getInverseRelations(problem),fqn2PQuery)» | 41 | «generateMayRelation(problem, relation, upperMultiplicities, base.getContainments(problem), base.getInverseRelations(problem), mustNotRelations.get(relation) ?: emptySet, fqn2PQuery)» |
36 | «ENDIF» | 42 | «ENDIF» |
37 | «ENDFOR» | 43 | «ENDFOR» |
38 | ''' | 44 | ''' |
39 | } | 45 | } |
40 | 46 | ||
41 | def private patternName(RelationDeclaration r, Modality modality) { | 47 | def private patternName(RelationDeclaration r, Modality modality) { |
42 | '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' | 48 | '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' |
43 | } | 49 | } |
44 | 50 | ||
45 | def referRelation( | 51 | def referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable, |
46 | RelationDeclaration referred, | 52 | Modality modality) '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);''' |
47 | String sourceVariable, | 53 | |
48 | String targetVariable, | ||
49 | Modality modality) | ||
50 | '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);''' | ||
51 | |||
52 | def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' | 54 | def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' |
53 | /** | 55 | /** |
54 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 56 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -65,59 +67,64 @@ class RelationDeclarationIndexer { | |||
65 | BinaryElementRelationLink.param2(link,target); | 67 | BinaryElementRelationLink.param2(link,target); |
66 | } | 68 | } |
67 | ''' | 69 | ''' |
70 | |||
68 | def generateMayRelation(LogicProblem problem, RelationDeclaration relation, | 71 | def generateMayRelation(LogicProblem problem, RelationDeclaration relation, |
69 | Map<Relation, Integer> upperMultiplicities, | 72 | Map<Relation, Integer> upperMultiplicities, List<Relation> containments, |
70 | List<Relation> containments, | 73 | HashMap<Relation, Relation> inverseRelations, Collection<String> mustNotRelations, |
71 | HashMap<Relation, Relation> inverseRelations, | 74 | Map<String, PQuery> fqn2PQuery) { |
72 | Map<String,PQuery> fqn2PQuery) | ||
73 | { | ||
74 | return ''' | 75 | return ''' |
75 | /** | 76 | /** |
76 | * Matcher for detecting tuples t where <>«relation.name»(source,target) | 77 | * Matcher for detecting tuples t where <>«relation.name»(source,target) |
77 | */ | 78 | */ |
78 | private pattern «relation.patternName(Modality.MAY)»( | 79 | private pattern «relation.patternName(Modality.MAY)»( |
79 | problem:LogicProblem, interpretation:PartialInterpretation, | 80 | problem:LogicProblem, interpretation:PartialInterpretation, |
80 | source: DefinedElement, target:DefinedElement) | 81 | source: DefinedElement, target:DefinedElement) |
81 | { | 82 | { |
82 | find interpretation(problem,interpretation); | 83 | find interpretation(problem,interpretation); |
83 | // The two endpoint of the link have to exist | 84 | // The two endpoint of the link have to exist |
84 | find mayExist(problem, interpretation, source); | 85 | find mayExist(problem, interpretation, source); |
85 | find mayExist(problem, interpretation, target); | 86 | find mayExist(problem, interpretation, target); |
86 | // Type consistency | 87 | // Type consistency |
87 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» | 88 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» |
88 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» | 89 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» |
89 | «IF upperMultiplicities.containsKey(relation)» | 90 | «IF upperMultiplicities.containsKey(relation)» |
90 | // There are "numberOfExistingReferences" currently existing instances of the reference from the source, | 91 | // There are "numberOfExistingReferences" currently existing instances of the reference from the source, |
91 | // the upper bound of the multiplicity should be considered. | 92 | // the upper bound of the multiplicity should be considered. |
92 | numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» | 93 | numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» |
93 | numberOfExistingReferences != «upperMultiplicities.get(relation)»; | 94 | numberOfExistingReferences != «upperMultiplicities.get(relation)»; |
94 | «ENDIF» | 95 | «ENDIF» |
95 | «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» | 96 | «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» |
96 | // There are "numberOfExistingReferences" currently existing instances of the reference to the target, | 97 | // There are "numberOfExistingReferences" currently existing instances of the reference to the target, |
97 | // the upper bound of the opposite reference multiplicity should be considered. | 98 | // the upper bound of the opposite reference multiplicity should be considered. |
98 | numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» | 99 | numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» |
99 | numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»; | 100 | numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»; |
100 | «ENDIF» | 101 | «ENDIF» |
101 | «IF containments.contains(relation)» | 102 | «IF containments.contains(relation)» |
102 | // The reference is containment, then a new reference cannot be create if: | 103 | // The reference is containment, then a new reference cannot be create if: |
103 | // 1. Multiple parents | 104 | // 1. Multiple parents |
104 | neg «base.containmentIndexer.referMustContaint("_","target")» | 105 | neg «base.containmentIndexer.referMustContaint("_","target")» |
105 | // 2. Circle in the containment hierarchy | 106 | // 2. Circle in the containment hierarchy |
106 | neg «base.containmentIndexer.referTransitiveMustContains("target","source")» | 107 | neg «base.containmentIndexer.referTransitiveMustContains("target","source")» |
107 | «ENDIF» | 108 | «ENDIF» |
108 | «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» | 109 | «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» |
109 | // The eOpposite of the reference is containment, then a referene cannot be created if | 110 | // The eOpposite of the reference is containment, then a referene cannot be created if |
110 | // 1. Multiple parents | 111 | // 1. Multiple parents |
111 | neg «base.containmentIndexer.referMustContaint("source","_")» | 112 | neg «base.containmentIndexer.referMustContaint("source","_")» |
112 | // 2. Circle in the containment hierarchy | 113 | // 2. Circle in the containment hierarchy |
113 | neg «base.containmentIndexer.referTransitiveMustContains("source","target")» | 114 | neg «base.containmentIndexer.referTransitiveMustContains("source","target")» |
114 | «ENDIF» | 115 | «ENDIF» |
115 | } or { | 116 | «IF !mustNotRelations.empty» |
116 | «relation.referRelation("source","target",Modality.MUST)» | 117 | // ![] unit propagation relations |
117 | } | 118 | «FOR mustNotRelation : mustNotRelations» |
118 | ''' | 119 | neg find «mustNotRelation»(problem, interpretation, source, target); |
120 | «ENDFOR» | ||
121 | «ENDIF» | ||
122 | } or { | ||
123 | «relation.referRelation("source","target",Modality.MUST)» | ||
124 | } | ||
125 | ''' | ||
119 | } | 126 | } |
120 | 127 | ||
121 | def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' | 128 | def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' |
122 | /** | 129 | /** |
123 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 130 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -129,6 +136,7 @@ class RelationDeclarationIndexer { | |||
129 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» | 136 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» |
130 | } | 137 | } |
131 | ''' | 138 | ''' |
139 | |||
132 | def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' | 140 | def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' |
133 | /** | 141 | /** |
134 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 142 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -140,4 +148,4 @@ class RelationDeclarationIndexer { | |||
140 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» | 148 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» |
141 | } | 149 | } |
142 | ''' | 150 | ''' |
143 | } \ No newline at end of file | 151 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend index 783cd36b..6f5f2402 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend | |||
@@ -1,10 +1,17 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import com.google.common.collect.ImmutableSet | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
10 | import java.util.Collection | ||
7 | import java.util.LinkedList | 11 | import java.util.LinkedList |
12 | import java.util.Map | ||
13 | import java.util.Set | ||
14 | import org.eclipse.xtend2.lib.StringConcatenationClient | ||
8 | 15 | ||
9 | class RelationRefinementGenerator { | 16 | class RelationRefinementGenerator { |
10 | PatternGenerator base; | 17 | PatternGenerator base; |
@@ -13,53 +20,61 @@ class RelationRefinementGenerator { | |||
13 | this.base = base | 20 | this.base = base |
14 | } | 21 | } |
15 | 22 | ||
16 | def CharSequence generateRefineReference(LogicProblem p) ''' | 23 | def CharSequence generateRefineReference(LogicProblem p, |
17 | «FOR relationRefinement : this.getRelationRefinements(p)» | 24 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) { |
18 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( | 25 | val mustRelations = getMustRelations(unitPropagationPatternGenerators) |
19 | problem:LogicProblem, interpretation:PartialInterpretation, | 26 | |
20 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», | 27 | ''' |
21 | from: DefinedElement, to: DefinedElement) | 28 | «FOR relationRefinement : this.getRelationRefinements(p)» |
22 | { | 29 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( |
23 | find interpretation(problem,interpretation); | 30 | problem:LogicProblem, interpretation:PartialInterpretation, |
24 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); | 31 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», |
25 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); | 32 | from: DefinedElement, to: DefinedElement) |
26 | «IF relationRefinement.value !== null» | 33 | { |
27 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); | 34 | find interpretation(problem,interpretation); |
28 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); | 35 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); |
36 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); | ||
37 | «IF relationRefinement.value !== null» | ||
38 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); | ||
39 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); | ||
40 | «ENDIF» | ||
41 | find mustExist(problem, interpretation, from); | ||
42 | find mustExist(problem, interpretation, to); | ||
43 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» | ||
44 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» | ||
45 | «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» | ||
46 | neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» | ||
47 | } | ||
48 | |||
49 | «IF isMustPropagationQueryNeeded(relationRefinement.key, relationRefinement.value, mustRelations)» | ||
50 | pattern «mustPropagationQueryName(relationRefinement.key)»( | ||
51 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
52 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», | ||
53 | from: DefinedElement, to: DefinedElement) | ||
54 | «FOR body : getMustPropagationBodies(relationRefinement.key, relationRefinement.value, mustRelations) SEPARATOR " or "» | ||
55 | { | ||
56 | «referRefinementQuery(relationRefinement.key, relationRefinement.value, "relationIterpretation", "oppositeInterpretation", "from", "to")» | ||
57 | «body» | ||
58 | } | ||
59 | «ENDFOR» | ||
29 | «ENDIF» | 60 | «ENDIF» |
30 | find mustExist(problem, interpretation, from); | 61 | «ENDFOR» |
31 | find mustExist(problem, interpretation, to); | 62 | ''' |
32 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» | 63 | } |
33 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» | ||
34 | «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» | ||
35 | neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» | ||
36 | } | ||
37 | «ENDFOR» | ||
38 | ''' | ||
39 | 64 | ||
40 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { | 65 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { |
41 | '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' | 66 | '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' |
42 | } | 67 | } |
43 | 68 | ||
69 | def String mustPropagationQueryName(RelationDeclaration relation) { | ||
70 | '''mustPropagation_«base.canonizeName(relation.name)»''' | ||
71 | } | ||
72 | |||
44 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, | 73 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, |
45 | String inverseInterpretationName, String sourceName, | 74 | String inverseInterpretationName, String sourceName, |
46 | String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);''' | 75 | String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);''' |
47 | 76 | ||
48 | def getRefineRelationQueries(LogicProblem p) { | 77 | def getRefineRelationQueries(LogicProblem p) { |
49 | // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet | ||
50 | // p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] | ||
51 | /* | ||
52 | * val res = new LinkedHashMap | ||
53 | * for(relation: getRelationRefinements(p)) { | ||
54 | * if(inverseRelations.containsKey(relation)) { | ||
55 | * val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' | ||
56 | * res.put(relation -> inverseRelations.get(relation),name) | ||
57 | * } else { | ||
58 | * val name = '''refineRelation_«base.canonizeName(relation.name)»''' | ||
59 | * res.put(relation -> null,name) | ||
60 | * } | ||
61 | * } | ||
62 | return res*/ | ||
63 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] | 78 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] |
64 | } | 79 | } |
65 | 80 | ||
@@ -83,4 +98,54 @@ class RelationRefinementGenerator { | |||
83 | } | 98 | } |
84 | return list | 99 | return list |
85 | } | 100 | } |
101 | |||
102 | def getMustPropagationQueries(LogicProblem p, | ||
103 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) { | ||
104 | val refinements = getRelationRefinements(p) | ||
105 | val mustRelations = getMustRelations(unitPropagationPatternGenerators) | ||
106 | refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [ | ||
107 | mustPropagationQueryName(key) | ||
108 | ] | ||
109 | } | ||
110 | |||
111 | private def getMustRelations(Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) { | ||
112 | ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [ | ||
113 | ImmutableSet.copyOf(map[value]) | ||
114 | ]) | ||
115 | } | ||
116 | |||
117 | private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation, | ||
118 | Map<Relation, ? extends Set<String>> mustRelations) { | ||
119 | val mustSet = mustRelations.get(relation) | ||
120 | if (mustSet !== null && !mustSet.empty) { | ||
121 | return true | ||
122 | } | ||
123 | if (inverseRelation !== null) { | ||
124 | val inverseMustSet = mustRelations.get(inverseRelation) | ||
125 | if (inverseMustSet !== null && !inverseMustSet.empty) { | ||
126 | return true | ||
127 | } | ||
128 | } | ||
129 | false | ||
130 | } | ||
131 | |||
132 | private def getMustPropagationBodies(Relation relation, Relation inverseRelation, | ||
133 | Map<Relation, ? extends Set<String>> mustRelations) { | ||
134 | val builder = ImmutableList.<StringConcatenationClient>builder() | ||
135 | val mustSet = mustRelations.get(relation) | ||
136 | if (mustSet !== null) { | ||
137 | for (refinementQuery : mustSet) { | ||
138 | builder.add('''find «refinementQuery»(problem, interpretation, from, to);''') | ||
139 | } | ||
140 | } | ||
141 | if (inverseRelation !== null && inverseRelation != relation) { | ||
142 | val inverseMustSet = mustRelations.get(inverseRelation) | ||
143 | if (inverseMustSet !== null) { | ||
144 | for (refinementQuery : inverseMustSet) { | ||
145 | builder.add('''find «refinementQuery»(problem, interpretation, to, from);''') | ||
146 | } | ||
147 | } | ||
148 | } | ||
149 | builder.build | ||
150 | } | ||
86 | } | 151 | } |
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 f7fe97a3..dca10baf 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,5 +1,6 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | 4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion |
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | 5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference |
@@ -29,12 +30,14 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory |
30 | import java.lang.reflect.Field | 31 | import java.lang.reflect.Field |
31 | import java.util.HashMap | 32 | import java.util.HashMap |
33 | import java.util.Iterator | ||
32 | import java.util.LinkedHashMap | 34 | import java.util.LinkedHashMap |
33 | import java.util.LinkedList | 35 | import java.util.LinkedList |
34 | import java.util.List | 36 | import java.util.List |
35 | import java.util.Map | 37 | import java.util.Map |
36 | import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine | 38 | import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine |
37 | import org.eclipse.viatra.query.runtime.api.GenericPatternMatch | 39 | import org.eclipse.viatra.query.runtime.api.GenericPatternMatch |
40 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
38 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 41 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
39 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 42 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
40 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 43 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
@@ -43,6 +46,7 @@ import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory | |||
43 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 46 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
44 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory | 47 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory |
45 | import org.eclipse.xtend.lib.annotations.Data | 48 | import org.eclipse.xtend.lib.annotations.Data |
49 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
46 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | 50 | import org.eclipse.xtext.xbase.lib.Functions.Function0 |
47 | 51 | ||
48 | class RefinementRuleProvider { | 52 | class RefinementRuleProvider { |
@@ -50,57 +54,55 @@ class RefinementRuleProvider { | |||
50 | val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE | 54 | val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE |
51 | val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE | 55 | val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE |
52 | 56 | ||
53 | var AdvancedViatraQueryEngine queryEngine | ||
54 | var Field delayMessageDelivery | ||
55 | |||
56 | def canonizeName(String name) { | 57 | def canonizeName(String name) { |
57 | return name.replace(' ', '_') | 58 | return name.replace(' ', '_') |
58 | } | 59 | } |
59 | 60 | ||
61 | def createUnitPrulePropagator(LogicProblem p, PartialInterpretation i, GeneratedPatterns patterns, | ||
62 | ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { | ||
63 | new UnitRulePropagator(p, i, this, scopePropagator, patterns.mustRelationPropagationQueries, statistics) | ||
64 | } | ||
65 | |||
60 | def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> createObjectRefinementRules( | 66 | def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> createObjectRefinementRules( |
61 | LogicProblem p, | 67 | LogicProblem p, |
62 | PartialInterpretation i, | 68 | PartialInterpretation i, |
63 | GeneratedPatterns patterns, | 69 | GeneratedPatterns patterns, |
64 | ScopePropagator scopePropagator, | 70 | UnitRulePropagator unitRulePropagator, |
65 | boolean nameNewElement, | 71 | boolean nameNewElement, |
66 | ModelGenerationStatistics statistics | 72 | ModelGenerationStatistics statistics |
67 | ) { | 73 | ) { |
68 | val res = new LinkedHashMap | 74 | val res = new LinkedHashMap |
69 | val recursiveObjectCreation = recursiveObjectCreation(p, i) | 75 | val recursiveObjectCreation = recursiveObjectCreation(p, i) |
70 | queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine | ||
71 | delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery") | ||
72 | delayMessageDelivery.accessible = true | ||
73 | for (LHSEntry : patterns.refineObjectQueries.entrySet) { | 76 | for (LHSEntry : patterns.refineObjectQueries.entrySet) { |
74 | val containmentRelation = LHSEntry.key.containmentRelation | 77 | val containmentRelation = LHSEntry.key.containmentRelation |
75 | val inverseRelation = LHSEntry.key.inverseContainment | 78 | val inverseRelation = LHSEntry.key.inverseContainment |
76 | val type = LHSEntry.key.newType | 79 | val type = LHSEntry.key.newType |
77 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> | 80 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> |
78 | val rule = createObjectCreationRule(p, containmentRelation, inverseRelation, type, | 81 | val rule = createObjectCreationRule(p, containmentRelation, inverseRelation, type, |
79 | recursiveObjectCreation.get(type), lhs, nameNewElement, scopePropagator, statistics) | 82 | recursiveObjectCreation.get(type), lhs, nameNewElement, unitRulePropagator, statistics) |
80 | res.put(LHSEntry.key, rule) | 83 | res.put(LHSEntry.key, rule) |
81 | } | 84 | } |
82 | return res | 85 | return res |
83 | } | 86 | } |
84 | 87 | ||
85 | def private createObjectCreationRule(LogicProblem p, Relation containmentRelation, Relation inverseRelation, | 88 | def private createObjectCreationRule(LogicProblem p, Relation containmentRelation, Relation inverseRelation, |
86 | Type type, List<ObjectCreationInterpretationData> recursiceObjectCreations, | 89 | Type type, List<ObjectCreationInterpretationData> recursiveObjectCreations, |
87 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, boolean nameNewElement, | 90 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, boolean nameNewElement, |
88 | ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { | 91 | UnitRulePropagator unitRulePropagator, ModelGenerationStatistics statistics) { |
89 | val name = '''addObject_«type.name.canonizeName»«IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' | 92 | val name = '''addObject_«type.name.canonizeName»«IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' |
90 | val ruleBuilder = factory.createRule(lhs).name(name) | 93 | val ruleBuilder = factory.createRule(lhs).name(name) |
91 | if (containmentRelation !== null) { | 94 | if (containmentRelation !== null) { |
92 | if (inverseRelation !== null) { | 95 | if (inverseRelation !== null) { |
93 | ruleBuilder.action [ match | | 96 | ruleBuilder.action [ match | |
94 | statistics.incrementTransformationCount | 97 | statistics.incrementTransformationCount |
95 | // println(name) | 98 | // println(name) |
99 | val startTime = System.nanoTime | ||
96 | // val problem = match.get(0) as LogicProblem | 100 | // val problem = match.get(0) as LogicProblem |
97 | val interpretation = match.get(1) as PartialInterpretation | 101 | val interpretation = match.get(1) as PartialInterpretation |
98 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 102 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |
99 | val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation | 103 | val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation |
100 | val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation | 104 | val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation |
101 | val container = match.get(5) as DefinedElement | 105 | val container = match.get(5) as DefinedElement |
102 | |||
103 | val startTime = System.nanoTime | ||
104 | createObjectActionWithContainmentAndInverse( | 106 | createObjectActionWithContainmentAndInverse( |
105 | nameNewElement, | 107 | nameNewElement, |
106 | interpretation, | 108 | interpretation, |
@@ -109,29 +111,24 @@ class RefinementRuleProvider { | |||
109 | relationInterpretation, | 111 | relationInterpretation, |
110 | inverseRelationInterpretation, | 112 | inverseRelationInterpretation, |
111 | [createDefinedElement], | 113 | [createDefinedElement], |
112 | recursiceObjectCreations, | 114 | recursiveObjectCreations, |
113 | scopePropagator | 115 | unitRulePropagator |
114 | ) | 116 | ) |
115 | statistics.addExecutionTime(System.nanoTime - startTime) | 117 | statistics.addExecutionTime(System.nanoTime - startTime) |
116 | 118 | ||
117 | flushQueryEngine(scopePropagator) | 119 | unitRulePropagator.propagate |
118 | |||
119 | // Scope propagation | ||
120 | val propagatorStartTime = System.nanoTime | ||
121 | scopePropagator.propagateAllScopeConstraints() | ||
122 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
123 | ] | 120 | ] |
124 | } else { | 121 | } else { |
125 | ruleBuilder.action [ match | | 122 | ruleBuilder.action [ match | |
126 | statistics.incrementTransformationCount | 123 | statistics.incrementTransformationCount |
127 | // println(name) | 124 | // println(name) |
125 | val startTime = System.nanoTime | ||
128 | // val problem = match.get(0) as LogicProblem | 126 | // val problem = match.get(0) as LogicProblem |
129 | val interpretation = match.get(1) as PartialInterpretation | 127 | val interpretation = match.get(1) as PartialInterpretation |
130 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 128 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |
131 | val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation | 129 | val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation |
132 | val container = match.get(4) as DefinedElement | 130 | val container = match.get(4) as DefinedElement |
133 | 131 | ||
134 | val startTime = System.nanoTime | ||
135 | createObjectActionWithContainment( | 132 | createObjectActionWithContainment( |
136 | nameNewElement, | 133 | nameNewElement, |
137 | interpretation, | 134 | interpretation, |
@@ -139,44 +136,34 @@ class RefinementRuleProvider { | |||
139 | container, | 136 | container, |
140 | relationInterpretation, | 137 | relationInterpretation, |
141 | [createDefinedElement], | 138 | [createDefinedElement], |
142 | recursiceObjectCreations, | 139 | recursiveObjectCreations, |
143 | scopePropagator | 140 | unitRulePropagator |
144 | ) | 141 | ) |
145 | statistics.addExecutionTime(System.nanoTime - startTime) | 142 | statistics.addExecutionTime(System.nanoTime - startTime) |
146 | 143 | ||
147 | flushQueryEngine(scopePropagator) | 144 | unitRulePropagator.propagate |
148 | |||
149 | // Scope propagation | ||
150 | val propagatorStartTime = System.nanoTime | ||
151 | scopePropagator.propagateAllScopeConstraints() | ||
152 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
153 | ] | 145 | ] |
154 | } | 146 | } |
155 | } else { | 147 | } else { |
156 | ruleBuilder.action [ match | | 148 | ruleBuilder.action [ match | |
157 | statistics.incrementTransformationCount | 149 | statistics.incrementTransformationCount |
158 | // println(name) | 150 | // println(name) |
151 | val startTime = System.nanoTime | ||
159 | // val problem = match.get(0) as LogicProblem | 152 | // val problem = match.get(0) as LogicProblem |
160 | val interpretation = match.get(1) as PartialInterpretation | 153 | val interpretation = match.get(1) as PartialInterpretation |
161 | val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation | 154 | val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation |
162 | 155 | ||
163 | val startTime = System.nanoTime | ||
164 | createObjectAction( | 156 | createObjectAction( |
165 | nameNewElement, | 157 | nameNewElement, |
166 | interpretation, | 158 | interpretation, |
167 | typeInterpretation, | 159 | typeInterpretation, |
168 | [createDefinedElement], | 160 | [createDefinedElement], |
169 | recursiceObjectCreations, | 161 | recursiveObjectCreations, |
170 | scopePropagator | 162 | unitRulePropagator |
171 | ) | 163 | ) |
172 | statistics.addExecutionTime(System.nanoTime - startTime) | 164 | statistics.addExecutionTime(System.nanoTime - startTime) |
173 | 165 | ||
174 | flushQueryEngine(scopePropagator) | 166 | unitRulePropagator.propagate |
175 | |||
176 | // Scope propagation | ||
177 | val propagatorStartTime = System.nanoTime | ||
178 | scopePropagator.propagateAllScopeConstraints() | ||
179 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
180 | ] | 167 | ] |
181 | } | 168 | } |
182 | return ruleBuilder.build | 169 | return ruleBuilder.build |
@@ -342,14 +329,14 @@ class RefinementRuleProvider { | |||
342 | [createStringElement] | 329 | [createStringElement] |
343 | } | 330 | } |
344 | 331 | ||
345 | def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, | 332 | def createRelationRefinementRules(GeneratedPatterns patterns, UnitRulePropagator unitRulePropagator, |
346 | ModelGenerationStatistics statistics) { | 333 | ModelGenerationStatistics statistics) { |
347 | val res = new LinkedHashMap | 334 | val res = new LinkedHashMap |
348 | for (LHSEntry : patterns.refinerelationQueries.entrySet) { | 335 | for (LHSEntry : patterns.refineRelationQueries.entrySet) { |
349 | val declaration = LHSEntry.key.key | 336 | val declaration = LHSEntry.key.key |
350 | val inverseReference = LHSEntry.key.value | 337 | val inverseReference = LHSEntry.key.value |
351 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> | 338 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> |
352 | val rule = createRelationRefinementRule(declaration, inverseReference, lhs, scopePropagator, statistics) | 339 | val rule = createRelationRefinementRule(declaration, inverseReference, lhs, unitRulePropagator, statistics) |
353 | res.put(LHSEntry.key, rule) | 340 | res.put(LHSEntry.key, rule) |
354 | } | 341 | } |
355 | return res | 342 | return res |
@@ -357,59 +344,29 @@ class RefinementRuleProvider { | |||
357 | 344 | ||
358 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> createRelationRefinementRule( | 345 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> createRelationRefinementRule( |
359 | RelationDeclaration declaration, Relation inverseRelation, | 346 | RelationDeclaration declaration, Relation inverseRelation, |
360 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator, | 347 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, UnitRulePropagator unitRulePropagator, |
361 | ModelGenerationStatistics statistics) { | 348 | ModelGenerationStatistics statistics) { |
362 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' | 349 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' |
363 | val ruleBuilder = factory.createRule(lhs).name(name) | 350 | val ruleBuilder = factory.createRule(lhs).name(name) |
364 | if (inverseRelation === null) { | 351 | if (inverseRelation === null) { |
365 | ruleBuilder.action [ match | | 352 | ruleBuilder.action [ match | |
366 | statistics.incrementTransformationCount | 353 | statistics.incrementTransformationCount |
367 | |||
368 | // println(name) | 354 | // println(name) |
369 | // val problem = match.get(0) as LogicProblem | 355 | val startTime = System.nanoTime |
370 | // val interpretation = match.get(1) as PartialInterpretation | 356 | createRelationLinkAction(match, unitRulePropagator) |
371 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 357 | statistics.addExecutionTime(System.nanoTime - startTime) |
372 | val src = match.get(3) as DefinedElement | ||
373 | val trg = match.get(4) as DefinedElement | ||
374 | |||
375 | queryEngine.delayUpdatePropagation [ | ||
376 | val startTime = System.nanoTime | ||
377 | createRelationLinkAction(src, trg, relationInterpretation) | ||
378 | statistics.addExecutionTime(System.nanoTime - startTime) | ||
379 | ] | ||
380 | 358 | ||
381 | // Scope propagation | 359 | unitRulePropagator.propagate |
382 | if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { | ||
383 | queryEngine.delayUpdatePropagation [ | ||
384 | val propagatorStartTime = System.nanoTime | ||
385 | scopePropagator.propagateAllScopeConstraints() | ||
386 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
387 | ] | ||
388 | } | ||
389 | ] | 360 | ] |
390 | } else { | 361 | } else { |
391 | ruleBuilder.action [ match | | 362 | ruleBuilder.action [ match | |
392 | statistics.incrementTransformationCount | 363 | statistics.incrementTransformationCount |
393 | // println(name) | 364 | // println(name) |
394 | // val problem = match.get(0) as LogicProblem | ||
395 | // val interpretation = match.get(1) as PartialInterpretation | ||
396 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | ||
397 | val inverseInterpretation = match.get(3) as PartialRelationInterpretation | ||
398 | val src = match.get(4) as DefinedElement | ||
399 | val trg = match.get(5) as DefinedElement | ||
400 | |||
401 | val startTime = System.nanoTime | 365 | val startTime = System.nanoTime |
402 | createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) | 366 | createRelationLinkWithInverse(match, unitRulePropagator) |
403 | statistics.addExecutionTime(System.nanoTime - startTime) | 367 | statistics.addExecutionTime(System.nanoTime - startTime) |
404 | 368 | ||
405 | // Scope propagation | 369 | unitRulePropagator.propagate |
406 | if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { | ||
407 | flushQueryEngine(scopePropagator) | ||
408 | |||
409 | val propagatorStartTime = System.nanoTime | ||
410 | scopePropagator.propagateAllScopeConstraints() | ||
411 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
412 | } | ||
413 | ] | 370 | ] |
414 | } | 371 | } |
415 | 372 | ||
@@ -420,7 +377,7 @@ class RefinementRuleProvider { | |||
420 | // Actions | 377 | // Actions |
421 | // /////////////////////// | 378 | // /////////////////////// |
422 | protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, | 379 | protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, |
423 | DefinedElement container, ScopePropagator scopePropagator) { | 380 | DefinedElement container, UnitRulePropagator unitRulePropagator) { |
424 | if (data.containerInterpretation !== null) { | 381 | if (data.containerInterpretation !== null) { |
425 | if (data.containerInverseInterpretation !== null) { | 382 | if (data.containerInverseInterpretation !== null) { |
426 | createObjectActionWithContainmentAndInverse( | 383 | createObjectActionWithContainmentAndInverse( |
@@ -432,7 +389,7 @@ class RefinementRuleProvider { | |||
432 | data.containerInverseInterpretation, | 389 | data.containerInverseInterpretation, |
433 | data.constructor, | 390 | data.constructor, |
434 | data.recursiveConstructors, | 391 | data.recursiveConstructors, |
435 | scopePropagator | 392 | unitRulePropagator |
436 | ) | 393 | ) |
437 | } else { | 394 | } else { |
438 | createObjectActionWithContainment( | 395 | createObjectActionWithContainment( |
@@ -443,7 +400,7 @@ class RefinementRuleProvider { | |||
443 | data.containerInterpretation, | 400 | data.containerInterpretation, |
444 | data.constructor, | 401 | data.constructor, |
445 | data.recursiveConstructors, | 402 | data.recursiveConstructors, |
446 | scopePropagator | 403 | unitRulePropagator |
447 | ) | 404 | ) |
448 | } | 405 | } |
449 | } else { | 406 | } else { |
@@ -453,7 +410,7 @@ class RefinementRuleProvider { | |||
453 | data.typeInterpretation, | 410 | data.typeInterpretation, |
454 | data.constructor, | 411 | data.constructor, |
455 | data.recursiveConstructors, | 412 | data.recursiveConstructors, |
456 | scopePropagator | 413 | unitRulePropagator |
457 | ) | 414 | ) |
458 | } | 415 | } |
459 | 416 | ||
@@ -468,7 +425,7 @@ class RefinementRuleProvider { | |||
468 | PartialRelationInterpretation inverseRelationInterpretation, | 425 | PartialRelationInterpretation inverseRelationInterpretation, |
469 | Function0<DefinedElement> constructor, | 426 | Function0<DefinedElement> constructor, |
470 | List<ObjectCreationInterpretationData> recursiceObjectCreations, | 427 | List<ObjectCreationInterpretationData> recursiceObjectCreations, |
471 | ScopePropagator scopePropagator | 428 | UnitRulePropagator unitRulePropagator |
472 | ) { | 429 | ) { |
473 | val newElement = constructor.apply | 430 | val newElement = constructor.apply |
474 | if (nameNewElement) { | 431 | if (nameNewElement) { |
@@ -488,14 +445,16 @@ class RefinementRuleProvider { | |||
488 | inverseRelationInterpretation.relationlinks += newLink2 | 445 | inverseRelationInterpretation.relationlinks += newLink2 |
489 | 446 | ||
490 | // Scope propagation | 447 | // Scope propagation |
491 | scopePropagator.decrementTypeScope(typeInterpretation) | 448 | unitRulePropagator.decrementTypeScope(typeInterpretation) |
449 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
450 | unitRulePropagator.addedToRelation(inverseRelationInterpretation.interpretationOf) | ||
492 | 451 | ||
493 | // Existence | 452 | // Existence |
494 | interpretation.newElements += newElement | 453 | interpretation.newElements += newElement |
495 | 454 | ||
496 | // Do recursive object creation | 455 | // Do recursive object creation |
497 | for (newConstructor : recursiceObjectCreations) { | 456 | for (newConstructor : recursiceObjectCreations) { |
498 | createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) | 457 | createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) |
499 | } | 458 | } |
500 | 459 | ||
501 | return newElement | 460 | return newElement |
@@ -509,7 +468,7 @@ class RefinementRuleProvider { | |||
509 | PartialRelationInterpretation relationInterpretation, | 468 | PartialRelationInterpretation relationInterpretation, |
510 | Function0<DefinedElement> constructor, | 469 | Function0<DefinedElement> constructor, |
511 | List<ObjectCreationInterpretationData> recursiceObjectCreations, | 470 | List<ObjectCreationInterpretationData> recursiceObjectCreations, |
512 | ScopePropagator scopePropagator | 471 | UnitRulePropagator unitRulePropagator |
513 | ) { | 472 | ) { |
514 | val newElement = constructor.apply | 473 | val newElement = constructor.apply |
515 | if (nameNewElement) { | 474 | if (nameNewElement) { |
@@ -524,16 +483,17 @@ class RefinementRuleProvider { | |||
524 | // ContainmentRelation | 483 | // ContainmentRelation |
525 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] | 484 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] |
526 | relationInterpretation.relationlinks += newLink | 485 | relationInterpretation.relationlinks += newLink |
486 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
527 | 487 | ||
528 | // Scope propagation | 488 | // Scope propagation |
529 | scopePropagator.decrementTypeScope(typeInterpretation) | 489 | unitRulePropagator.decrementTypeScope(typeInterpretation) |
530 | 490 | ||
531 | // Existence | 491 | // Existence |
532 | interpretation.newElements += newElement | 492 | interpretation.newElements += newElement |
533 | 493 | ||
534 | // Do recursive object creation | 494 | // Do recursive object creation |
535 | for (newConstructor : recursiceObjectCreations) { | 495 | for (newConstructor : recursiceObjectCreations) { |
536 | createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) | 496 | createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) |
537 | } | 497 | } |
538 | 498 | ||
539 | return newElement | 499 | return newElement |
@@ -541,7 +501,7 @@ class RefinementRuleProvider { | |||
541 | 501 | ||
542 | protected def createObjectAction(boolean nameNewElement, PartialInterpretation interpretation, | 502 | protected def createObjectAction(boolean nameNewElement, PartialInterpretation interpretation, |
543 | PartialTypeInterpratation typeInterpretation, Function0<DefinedElement> constructor, | 503 | PartialTypeInterpratation typeInterpretation, Function0<DefinedElement> constructor, |
544 | List<ObjectCreationInterpretationData> recursiceObjectCreations, ScopePropagator scopePropagator) { | 504 | List<ObjectCreationInterpretationData> recursiceObjectCreations, UnitRulePropagator unitRulePropagator) { |
545 | val newElement = constructor.apply | 505 | val newElement = constructor.apply |
546 | if (nameNewElement) { | 506 | if (nameNewElement) { |
547 | newElement.name = '''new «interpretation.newElements.size»''' | 507 | newElement.name = '''new «interpretation.newElements.size»''' |
@@ -554,38 +514,220 @@ class RefinementRuleProvider { | |||
554 | } | 514 | } |
555 | 515 | ||
556 | // Scope propagation | 516 | // Scope propagation |
557 | scopePropagator.decrementTypeScope(typeInterpretation) | 517 | unitRulePropagator.decrementTypeScope(typeInterpretation) |
558 | 518 | ||
559 | // Existence | 519 | // Existence |
560 | interpretation.newElements += newElement | 520 | interpretation.newElements += newElement |
561 | 521 | ||
562 | // Do recursive object creation | 522 | // Do recursive object creation |
563 | for (newConstructor : recursiceObjectCreations) { | 523 | for (newConstructor : recursiceObjectCreations) { |
564 | createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) | 524 | createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) |
565 | } | 525 | } |
566 | 526 | ||
567 | return newElement | 527 | return newElement |
568 | } | 528 | } |
569 | 529 | ||
570 | protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg, | 530 | protected def createRelationLinkAction(IPatternMatch match, UnitRulePropagator unitRulePropagator) { |
571 | PartialRelationInterpretation relationInterpretation) { | 531 | // val problem = match.get(0) as LogicProblem |
532 | // val interpretation = match.get(1) as PartialInterpretation | ||
533 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | ||
534 | val src = match.get(3) as DefinedElement | ||
535 | val trg = match.get(4) as DefinedElement | ||
536 | createRelationLinkAction(src, trg, relationInterpretation, unitRulePropagator) | ||
537 | } | ||
538 | |||
539 | protected def void createRelationLinkAction(DefinedElement src, DefinedElement trg, | ||
540 | PartialRelationInterpretation relationInterpretation, UnitRulePropagator unitRulePropagator) { | ||
572 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] | 541 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] |
573 | relationInterpretation.relationlinks += link | 542 | relationInterpretation.relationlinks += link |
543 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
574 | } | 544 | } |
575 | 545 | ||
576 | protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, | 546 | protected def void createRelationLinkWithInverse(IPatternMatch match, UnitRulePropagator unitRulePropagator) { |
577 | PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) { | 547 | // val problem = match.get(0) as LogicProblem |
548 | // val interpretation = match.get(1) as PartialInterpretation | ||
549 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | ||
550 | val inverseInterpretation = match.get(3) as PartialRelationInterpretation | ||
551 | val src = match.get(4) as DefinedElement | ||
552 | val trg = match.get(5) as DefinedElement | ||
553 | createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation, unitRulePropagator) | ||
554 | } | ||
555 | |||
556 | protected def void createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, | ||
557 | PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation, | ||
558 | UnitRulePropagator unitRulePropagator) { | ||
578 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] | 559 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] |
579 | relationInterpretation.relationlinks += link | 560 | relationInterpretation.relationlinks += link |
580 | val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] | 561 | val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] |
581 | inverseInterpretation.relationlinks += inverseLink | 562 | inverseInterpretation.relationlinks += inverseLink |
563 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
564 | unitRulePropagator.addedToRelation(inverseInterpretation.interpretationOf) | ||
582 | } | 565 | } |
583 | 566 | ||
584 | protected def flushQueryEngine(ScopePropagator scopePropagator) { | 567 | static class UnitRulePropagator { |
585 | if (scopePropagator.queryEngineFlushRequiredBeforePropagation && queryEngine.updatePropagationDelayed) { | 568 | val LogicProblem p |
586 | delayMessageDelivery.setBoolean(queryEngine, false) | 569 | val PartialInterpretation i |
587 | queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates | 570 | val RefinementRuleProvider refinementRuleProvider |
588 | delayMessageDelivery.setBoolean(queryEngine, true) | 571 | var AdvancedViatraQueryEngine queryEngine |
572 | var Field delayMessageDelivery | ||
573 | val ScopePropagator scopePropagator | ||
574 | val List<AbstractMustRelationPropagator<? extends IPatternMatch>> propagators | ||
575 | val ModelGenerationStatistics statistics | ||
576 | |||
577 | new(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider, | ||
578 | ScopePropagator scopePropagator, | ||
579 | Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries, | ||
580 | ModelGenerationStatistics statistics) { | ||
581 | this.p = p | ||
582 | this.i = i | ||
583 | this.refinementRuleProvider = refinementRuleProvider | ||
584 | queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine | ||
585 | delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery") | ||
586 | delayMessageDelivery.accessible = true | ||
587 | this.scopePropagator = scopePropagator | ||
588 | propagators = ImmutableList.copyOf(mustRelationPropagationQueries.entrySet.map [ entry | | ||
589 | val matcher = queryEngine.getMatcher(entry.value) | ||
590 | getPropagator(entry.key.key, entry.key.value, matcher) | ||
591 | ]) | ||
592 | this.statistics = statistics | ||
593 | } | ||
594 | |||
595 | def decrementTypeScope(PartialTypeInterpratation partialTypeInterpratation) { | ||
596 | scopePropagator.decrementTypeScope(partialTypeInterpratation) | ||
597 | } | ||
598 | |||
599 | def addedToRelation(Relation r) { | ||
600 | scopePropagator.addedToRelation(r) | ||
601 | } | ||
602 | |||
603 | def propagate() { | ||
604 | var boolean changed | ||
605 | do { | ||
606 | val scopeChanged = propagateScope() | ||
607 | val mustChanged = propagateMustRelations() | ||
608 | changed = scopeChanged || mustChanged | ||
609 | } while (changed) | ||
610 | } | ||
611 | |||
612 | protected def flushQueryEngine() { | ||
613 | if (queryEngine.updatePropagationDelayed) { | ||
614 | delayMessageDelivery.setBoolean(queryEngine, false) | ||
615 | queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates | ||
616 | delayMessageDelivery.setBoolean(queryEngine, true) | ||
617 | } | ||
618 | } | ||
619 | |||
620 | protected def propagateScope() { | ||
621 | if (scopePropagator.scopePropagationNeeded) { | ||
622 | if (scopePropagator.queryEngineFlushRequiredBeforePropagation) { | ||
623 | flushQueryEngine() | ||
624 | } | ||
625 | val propagatorStartTime = System.nanoTime | ||
626 | scopePropagator.propagateAllScopeConstraints() | ||
627 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
628 | true | ||
629 | } else { | ||
630 | false | ||
631 | } | ||
632 | } | ||
633 | |||
634 | protected def propagateMustRelations() { | ||
635 | if (propagators.empty) { | ||
636 | return false | ||
637 | } | ||
638 | flushQueryEngine() | ||
639 | val propagatorStartTime = System.nanoTime | ||
640 | var changed = false | ||
641 | for (propagator : propagators) { | ||
642 | changed = propagator.propagate(p, i, refinementRuleProvider, this) || changed | ||
643 | } | ||
644 | statistics.addMustRelationPropagationTime(System.nanoTime - propagatorStartTime) | ||
645 | changed | ||
646 | } | ||
647 | |||
648 | private static def <T extends IPatternMatch> getPropagator(Relation relation, Relation inverseRelation, | ||
649 | ViatraQueryMatcher<T> matcher) { | ||
650 | if (inverseRelation === null) { | ||
651 | new MustRelationPropagator(matcher) | ||
652 | } else if (relation == inverseRelation) { | ||
653 | new MustRelationPropagatorWithSelfInverse(matcher) | ||
654 | } else { | ||
655 | new MustRelationPropagatorWithInverse(matcher) | ||
656 | } | ||
657 | } | ||
658 | |||
659 | @FinalFieldsConstructor | ||
660 | private static abstract class AbstractMustRelationPropagator<T extends IPatternMatch> { | ||
661 | val ViatraQueryMatcher<T> matcher | ||
662 | |||
663 | def propagate(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider, | ||
664 | UnitRulePropagator unitRulePropagator) { | ||
665 | val iterator = getIterator(p, i) | ||
666 | if (!iterator.hasNext) { | ||
667 | return false | ||
668 | } | ||
669 | iterate(iterator, refinementRuleProvider, unitRulePropagator) | ||
670 | true | ||
671 | } | ||
672 | |||
673 | def iterate(Iterator<T> iterator, RefinementRuleProvider refinementRuleProvider, | ||
674 | UnitRulePropagator unitRulePropagator) { | ||
675 | while (iterator.hasNext) { | ||
676 | doPropagate(iterator.next, refinementRuleProvider, unitRulePropagator) | ||
677 | } | ||
678 | } | ||
679 | |||
680 | protected def getIterator(LogicProblem p, PartialInterpretation i) { | ||
681 | val partialMatch = matcher.newEmptyMatch | ||
682 | partialMatch.set(0, p) | ||
683 | partialMatch.set(1, i) | ||
684 | matcher.streamAllMatches(partialMatch).iterator | ||
685 | } | ||
686 | |||
687 | protected def void doPropagate(T match, RefinementRuleProvider refinementRuleProvider, | ||
688 | UnitRulePropagator unitRulePropagator) | ||
689 | } | ||
690 | |||
691 | private static class MustRelationPropagator<T extends IPatternMatch> extends AbstractMustRelationPropagator<T> { | ||
692 | new(ViatraQueryMatcher<T> matcher) { | ||
693 | super(matcher) | ||
694 | } | ||
695 | |||
696 | override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider, | ||
697 | UnitRulePropagator unitRulePropagator) { | ||
698 | refinementRuleProvider.createRelationLinkAction(match, unitRulePropagator) | ||
699 | } | ||
700 | } | ||
701 | |||
702 | private static class MustRelationPropagatorWithInverse<T extends IPatternMatch> extends AbstractMustRelationPropagator<T> { | ||
703 | new(ViatraQueryMatcher<T> matcher) { | ||
704 | super(matcher) | ||
705 | } | ||
706 | |||
707 | override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider, | ||
708 | UnitRulePropagator unitRulePropagator) { | ||
709 | refinementRuleProvider.createRelationLinkWithInverse(match, unitRulePropagator) | ||
710 | } | ||
711 | } | ||
712 | |||
713 | private static class MustRelationPropagatorWithSelfInverse<T extends IPatternMatch> extends MustRelationPropagatorWithInverse<T> { | ||
714 | new(ViatraQueryMatcher<T> matcher) { | ||
715 | super(matcher) | ||
716 | } | ||
717 | |||
718 | override iterate(Iterator<T> iterator, RefinementRuleProvider refinementRuleProvider, | ||
719 | UnitRulePropagator unitRulePropagator) { | ||
720 | val pairs = newHashSet | ||
721 | while (iterator.hasNext) { | ||
722 | val match = iterator.next | ||
723 | val src = match.get(4) as DefinedElement | ||
724 | val trg = match.get(5) as DefinedElement | ||
725 | if (!pairs.contains(trg -> src)) { | ||
726 | pairs.add(src -> trg) | ||
727 | doPropagate(match, refinementRuleProvider, unitRulePropagator) | ||
728 | } | ||
729 | } | ||
730 | } | ||
589 | } | 731 | } |
590 | } | 732 | } |
591 | } | 733 | } |
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 26ec7091..69b54b8a 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 | |||
@@ -6,7 +6,6 @@ import com.google.inject.Inject | |||
6 | import com.google.inject.Injector | 6 | import com.google.inject.Injector |
7 | import com.google.inject.multibindings.Multibinder | 7 | import com.google.inject.multibindings.Multibinder |
8 | import com.google.inject.name.Names | 8 | import com.google.inject.name.Names |
9 | import com.google.inject.util.Modules | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
@@ -46,7 +45,6 @@ import org.eclipse.xtext.scoping.IScope | |||
46 | import org.eclipse.xtext.scoping.IScopeProvider | 45 | import org.eclipse.xtext.scoping.IScopeProvider |
47 | import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider | 46 | import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider |
48 | import org.eclipse.xtext.scoping.impl.SimpleScope | 47 | import org.eclipse.xtext.scoping.impl.SimpleScope |
49 | import org.eclipse.xtext.service.AbstractGenericModule | ||
50 | import org.eclipse.xtext.service.SingletonBinding | 48 | import org.eclipse.xtext.service.SingletonBinding |
51 | import org.eclipse.xtext.workspace.IProjectConfigProvider | 49 | import org.eclipse.xtext.workspace.IProjectConfigProvider |
52 | 50 | ||
@@ -65,35 +63,32 @@ package class StandaloneParserWithFixedMetamodelProviderModule extends Standalon | |||
65 | Multibinder::newSetBinder(binder, IMetamodelProviderInstance); | 63 | Multibinder::newSetBinder(binder, IMetamodelProviderInstance); |
66 | } | 64 | } |
67 | 65 | ||
68 | } | 66 | @SingletonBinding |
69 | 67 | override IResourceServiceProvider.Registry bindIResourceServiceProvider$Registry() { | |
70 | package class StandaloneParserOverridesModule extends AbstractGenericModule { | 68 | new VqlDeactivatedServiceProviderRegistry |
71 | 69 | } | |
72 | def Class<? extends IMetamodelProvider> bindIMetamodelProvider() { | 70 | |
71 | override Class<? extends IMetamodelProvider> bindIMetamodelProvider() { | ||
73 | FixedMetamodelProvider | 72 | FixedMetamodelProvider |
74 | } | 73 | } |
75 | 74 | ||
76 | def Class<? extends IProjectConfigProvider> bindProjectConfigProvider() { | 75 | override Class<? extends IProjectConfigProvider> bindProjectConfigProvider() { |
77 | NullProjectConfigProvider | 76 | NullProjectConfigProvider |
78 | } | 77 | } |
79 | 78 | ||
80 | @SingletonBinding | 79 | @SingletonBinding |
81 | def Class<? extends IResourceServiceProvider.Registry> bindIResourceServiceProvider$Registry() { | 80 | override EValidator.Registry bindEValidatorRegistry() { |
82 | VqlDeactivatedServiceProviderRegistry | ||
83 | } | ||
84 | |||
85 | def EValidator.Registry bindEValidator$Registry() { | ||
86 | // org.eclipse.xtext.validation.EValidatorRegistrar modifies EValidators already in the registry, | 81 | // org.eclipse.xtext.validation.EValidatorRegistrar modifies EValidators already in the registry, |
87 | // so it is not safe to populate the registry from the EValidator.Registry.INSTANCE singleton. | 82 | // so it is not safe to populate the registry from the EValidator.Registry.INSTANCE singleton. |
88 | // There is no need to execute any EValiator other than EMFPatternLanguageValidator, | 83 | // There is no need to execute any EValiator other than EMFPatternLanguageValidator, |
89 | // so we can start with a blank registry instead. | 84 | // so we can start with a blank registry instead. |
90 | new EValidatorRegistryImpl() | 85 | new EValidatorRegistryImpl |
91 | } | 86 | } |
92 | 87 | ||
93 | def EPackage.Registry bindEPackage$Registry() { | 88 | @SingletonBinding |
89 | override EPackage.Registry bindEPackageRegistry() { | ||
94 | new EPackageRegistryImpl(EPackage.Registry.INSTANCE) | 90 | new EPackageRegistryImpl(EPackage.Registry.INSTANCE) |
95 | } | 91 | } |
96 | |||
97 | } | 92 | } |
98 | 93 | ||
99 | package class NullProjectConfigProvider implements IProjectConfigProvider { | 94 | package class NullProjectConfigProvider implements IProjectConfigProvider { |
@@ -136,10 +131,8 @@ class ParseUtil { | |||
136 | 131 | ||
137 | def protected Injector internalCreateInjector() { | 132 | def protected Injector internalCreateInjector() { |
138 | ensureViatraInitialized(); | 133 | ensureViatraInitialized(); |
139 | val runtimeModulemodule = new StandaloneParserWithFixedMetamodelProviderModule | 134 | val runtimeModule = new StandaloneParserWithFixedMetamodelProviderModule |
140 | val overridesModule = new StandaloneParserOverridesModule | 135 | val newInjector = Guice.createInjector(runtimeModule) |
141 | val module = Modules.override(runtimeModulemodule).with(overridesModule) | ||
142 | val newInjector = Guice.createInjector(module) | ||
143 | return newInjector | 136 | return newInjector |
144 | } | 137 | } |
145 | 138 | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF index 4ad61ccb..402a0b7d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF | |||
@@ -4,6 +4,7 @@ Bundle-Name: Reasoner | |||
4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
5 | Bundle-Version: 1.0.0.qualifier | 5 | Bundle-Version: 1.0.0.qualifier |
6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner, | 6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner, |
7 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse, | ||
7 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | 8 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization |
8 | Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 9 | Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
9 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 10 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend index 9ef5e091..691e0645 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend | |||
@@ -1,7 +1,6 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
2 | 2 | ||
3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | 3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | 4 | ||
6 | abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { | 5 | abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { |
7 | val protected ModelGenerationMethod method | 6 | val protected ModelGenerationMethod method |
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.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend index 56beacfa..25137eba 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.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend | |||
@@ -1,215 +1,201 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableMap | 3 | import com.google.common.collect.ImmutableMap |
4 | import com.google.common.collect.ImmutableSet | 4 | import com.google.common.collect.ImmutableSet |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
7 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 7 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator |
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver |
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | 21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries |
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
24 | import java.util.Collection | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider |
25 | import java.util.List | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
26 | import java.util.Map | 26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker |
27 | import java.util.Set | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver |
28 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjectiveProvider |
29 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 29 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
30 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 30 | import java.util.Collection |
31 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 31 | import java.util.List |
32 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 32 | import java.util.Map |
33 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 33 | import java.util.Set |
34 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | 34 | import org.eclipse.viatra.dse.objectives.IObjective |
35 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 35 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup |
36 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 36 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
37 | import org.eclipse.xtend.lib.annotations.Data | 37 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
38 | 38 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | |
39 | class ModelGenerationStatistics { | 39 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
40 | public var long transformationExecutionTime = 0 | 40 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
41 | 41 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | |
42 | synchronized def addExecutionTime(long amount) { | 42 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
43 | transformationExecutionTime += amount | 43 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
44 | } | 44 | import org.eclipse.xtend.lib.annotations.Data |
45 | 45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedPolyhedronScopePropagatorStrategy | |
46 | public var long scopePropagationTime = 0 | 46 | |
47 | 47 | @Data class ModelGenerationMethod { | |
48 | synchronized def addScopePropagationTime(long amount) { | 48 | ModelGenerationStatistics statistics |
49 | scopePropagationTime += amount | 49 | |
50 | } | 50 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules |
51 | 51 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules | |
52 | public var long preliminaryTypeAnalisisTime = 0 | 52 | |
53 | 53 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | |
54 | public var int decisionsTried = 0 | 54 | |
55 | 55 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | |
56 | synchronized def incrementDecisionCount() { | 56 | |
57 | decisionsTried++ | 57 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF |
58 | } | 58 | |
59 | 59 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | |
60 | public var int transformationInvocations | 60 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions |
61 | 61 | ||
62 | synchronized def incrementTransformationCount() { | 62 | Map<String, ModalPatternQueries> modalRelationQueries |
63 | transformationInvocations++ | 63 | |
64 | } | 64 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns |
65 | 65 | ||
66 | public var int scopePropagatorInvocations | 66 | Collection<IObjective> costObjectives |
67 | 67 | boolean optimizationProblem | |
68 | synchronized def incrementScopePropagationCount() { | 68 | ViatraReasonerSolutionSaver solutionSaver |
69 | scopePropagatorInvocations++ | 69 | } |
70 | } | 70 | |
71 | 71 | class ModelGenerationMethodProvider { | |
72 | public var int scopePropagatorSolverInvocations | 72 | val PatternProvider patternProvider = new PatternProvider |
73 | 73 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | |
74 | synchronized def incrementScopePropagationSolverCount() { | 74 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider |
75 | scopePropagatorSolverInvocations++ | 75 | val relationConstraintCalculator = new RelationConstraintCalculator |
76 | } | 76 | |
77 | } | 77 | def ModelGenerationMethod createModelGenerationMethod( |
78 | 78 | LogicProblem logicProblem, | |
79 | @Data class ModelGenerationMethod { | 79 | PartialInterpretation emptySolution, |
80 | ModelGenerationStatistics statistics | 80 | ReasonerWorkspace workspace, |
81 | 81 | ViatraReasonerConfiguration config | |
82 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules | 82 | ) { |
83 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules | 83 | val statistics = new ModelGenerationStatistics |
84 | 84 | val debugLevel = config.documentationLevel | |
85 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | 85 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) |
86 | 86 | ||
87 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | 87 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). |
88 | 88 | map[it.patternPQuery as PQuery].toSet | |
89 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | 89 | |
90 | 90 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | |
91 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | 91 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
92 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | 92 | workspace, config.typeInferenceMethod, config.scopePropagatorStrategy, relationConstraints, config.hints, |
93 | 93 | config.unitPropagationPatternGenerators, writeFiles) | |
94 | Map<String, ModalPatternQueries> modalRelationQueries | 94 | |
95 | 95 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | |
96 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | 96 | config.calculateObjectCreationCosts) |
97 | } | 97 | val unfinishedWF = queries.getUnfinishedWFQueries.values |
98 | 98 | val modalRelationQueriesBuilder = ImmutableMap.builder | |
99 | enum TypeInferenceMethod { | 99 | for (entry : queries.modalRelationQueries.entrySet) { |
100 | Generic, | 100 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head |
101 | PreliminaryAnalysis | 101 | if (annotation !== null) { |
102 | } | 102 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) |
103 | 103 | } | |
104 | class ModelGenerationMethodProvider { | 104 | } |
105 | val PatternProvider patternProvider = new PatternProvider | 105 | val modalRelationQueries = modalRelationQueriesBuilder.build |
106 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | 106 | val invalidWF = queries.getInvalidWFQueries.values |
107 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | 107 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns |
108 | val relationConstraintCalculator = new RelationConstraintCalculator | 108 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns |
109 | 109 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( | |
110 | def ModelGenerationMethod createModelGenerationMethod( | 110 | queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll( |
111 | LogicProblem logicProblem, | 111 | queries.mustRelationPropagationQueries.values).addAll(queries.multiplicityConstraintQueries.values.flatMap [ |
112 | PartialInterpretation emptySolution, | 112 | allQueries |
113 | ReasonerWorkspace workspace, | 113 | ]).addAll(queries.unfinishedWFQueries.values).addAll(queries.invalidWFQueries.values).addAll( |
114 | boolean nameNewElements, | 114 | queries.mustUnitPropagationPreconditionPatterns.values).addAll( |
115 | TypeInferenceMethod typeInferenceMethod, | 115 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build |
116 | boolean calculateObjectCreationCosts, | 116 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) |
117 | ScopePropagatorStrategy scopePropagatorStrategy, | 117 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) |
118 | Collection<LinearTypeConstraintHint> hints, | 118 | |
119 | DocumentationLevel debugLevel | 119 | val objectiveProvider = new ThreeValuedCostObjectiveProvider(queryEngine, emptySolution, modalRelationQueries) |
120 | ) { | 120 | val transformedObjectives = objectiveProvider.getCostObjectives(config.costObjectives) |
121 | val statistics = new ModelGenerationStatistics | 121 | |
122 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | 122 | val solutionSaver = new ViatraReasonerSolutionSaver(transformedObjectives.leveledExtremalObjectives, |
123 | 123 | config.solutionScope.numberOfRequiredSolutions, DiversityChecker.of(config.diversityRequirement)) | |
124 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). | 124 | |
125 | map[it.patternPQuery as PQuery].toSet | 125 | val allHints = ImmutableSet.builder |
126 | 126 | allHints.addAll(config.hints) | |
127 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 127 | for (hint : transformedObjectives.hints) { |
128 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 128 | hint.boundsProvider = solutionSaver |
129 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) | 129 | allHints.add(hint) |
130 | 130 | } | |
131 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) | 131 | |
132 | scopePropagator.propagateAllScopeConstraints | 132 | val scopePropagator = createScopePropagator(config.scopePropagatorStrategy, emptySolution, allHints.build, |
133 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | 133 | transformedObjectives.extensionOperators, queries, statistics) |
134 | queries, scopePropagator, nameNewElements, statistics) | 134 | scopePropagator.propagateAllScopeConstraints |
135 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, | 135 | val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, queries, |
136 | statistics) | 136 | scopePropagator, statistics) |
137 | 137 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | |
138 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | 138 | queries, unitRulePropagator, config.nameNewElements, statistics) |
139 | calculateObjectCreationCosts) | 139 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, |
140 | 140 | statistics) | |
141 | val unfinishedWF = queries.getUnfinishedWFQueries.values | 141 | |
142 | 142 | return new ModelGenerationMethod( | |
143 | val modalRelationQueriesBuilder = ImmutableMap.builder | 143 | statistics, |
144 | for (entry : queries.modalRelationQueries.entrySet) { | 144 | objectRefinementRules.values, |
145 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | 145 | relationRefinementRules.values, |
146 | if (annotation !== null) { | 146 | unfinishedMultiplicities, |
147 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | 147 | unfinishedWF, |
148 | } | 148 | invalidWF, |
149 | } | 149 | mustUnitPropagationPreconditions, |
150 | val modalRelationQueries = modalRelationQueriesBuilder.build | 150 | currentUnitPropagationPreconditions, |
151 | 151 | modalRelationQueries, | |
152 | val invalidWF = queries.getInvalidWFQueries.values | 152 | queries.allQueries, |
153 | 153 | transformedObjectives.objectives, | |
154 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns | 154 | transformedObjectives.optimizationProblem, |
155 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | 155 | solutionSaver |
156 | 156 | ) | |
157 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( | 157 | } |
158 | queries.refineTypeQueries.values).addAll(queries.refinerelationQueries.values).addAll(queries. | 158 | |
159 | multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll( | 159 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, |
160 | queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll( | 160 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, |
161 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build | 161 | Collection<PolyhedronExtensionOperator> extensionOperators, GeneratedPatterns queries, |
162 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | 162 | ModelGenerationStatistics statistics) { |
163 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) | 163 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { |
164 | 164 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | |
165 | return new ModelGenerationMethod( | 165 | } |
166 | statistics, | 166 | switch (scopePropagatorStrategy) { |
167 | objectRefinementRules.values, | 167 | case ScopePropagatorStrategy.None, |
168 | relationRefinementRules.values, | 168 | case ScopePropagatorStrategy.Basic: |
169 | unfinishedMultiplicities, | 169 | new ScopePropagator(emptySolution, statistics) |
170 | unfinishedWF, | 170 | case ScopePropagatorStrategy.BasicTypeHierarchy: |
171 | invalidWF, | 171 | new TypeHierarchyScopePropagator(emptySolution, statistics) |
172 | mustUnitPropagationPreconditions, | 172 | ScopePropagatorStrategy.Polyhedral: { |
173 | currentUnitPropagationPreconditions, | 173 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
174 | modalRelationQueries, | 174 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] |
175 | queries.allQueries | 175 | val solver = switch (scopePropagatorStrategy.solver) { |
176 | ) | 176 | case Z3Integer: |
177 | } | 177 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) |
178 | 178 | case Z3Real: | |
179 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | 179 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) |
180 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries, | 180 | case Cbc: |
181 | ModelGenerationStatistics statistics) { | 181 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) |
182 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | 182 | case Clp: |
183 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | 183 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) |
184 | } | 184 | default: |
185 | switch (scopePropagatorStrategy) { | 185 | throw new IllegalArgumentException("Unknown polyhedron solver: " + |
186 | case ScopePropagatorStrategy.None, | 186 | scopePropagatorStrategy.solver) |
187 | case ScopePropagatorStrategy.Basic: | 187 | } |
188 | new ScopePropagator(emptySolution, statistics) | 188 | val strategy = if (extensionOperators.empty) { |
189 | case ScopePropagatorStrategy.BasicTypeHierarchy: | 189 | new CachingSimplePolyhedronScopePropagatorStrategy(solver, statistics) |
190 | new TypeHierarchyScopePropagator(emptySolution, statistics) | 190 | } else { |
191 | ScopePropagatorStrategy.Polyhedral: { | 191 | new ExtendedPolyhedronScopePropagatorStrategy(solver, extensionOperators, statistics) |
192 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 192 | } |
193 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | 193 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, |
194 | val solver = switch (scopePropagatorStrategy.solver) { | 194 | queries.hasElementInContainmentQuery, allPatternsByName, hints, strategy, |
195 | case Z3Integer: | 195 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) |
196 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | 196 | } |
197 | case Z3Real: | 197 | default: |
198 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | 198 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) |
199 | case Cbc: | 199 | } |
200 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | 200 | } |
201 | case Clp: | 201 | } |
202 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
203 | default: | ||
204 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
205 | scopePropagatorStrategy.solver) | ||
206 | } | ||
207 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
208 | queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, | ||
209 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
210 | } | ||
211 | default: | ||
212 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
213 | } | ||
214 | } | ||
215 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index c333feca..8e992741 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |||
@@ -1,7 +1,5 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.Lists | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
@@ -11,7 +9,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | |||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
@@ -22,7 +19,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.sta | |||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory |
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint |
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration | 21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration |
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint |
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective |
@@ -32,11 +28,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective | |||
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective |
33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint | 29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint |
34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective |
35 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver | ||
36 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter | 31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter |
37 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | 32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind |
38 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement | ||
39 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective | ||
40 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 33 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
41 | import java.util.List | 34 | import java.util.List |
42 | import java.util.Map | 35 | import java.util.Map |
@@ -86,12 +79,7 @@ class ViatraReasoner extends LogicReasoner { | |||
86 | problem, | 79 | problem, |
87 | emptySolution, | 80 | emptySolution, |
88 | workspace, | 81 | workspace, |
89 | viatraConfig.nameNewElements, | 82 | viatraConfig |
90 | viatraConfig.typeInferenceMethod, | ||
91 | viatraConfig.calculateObjectCreationCosts, | ||
92 | viatraConfig.scopePropagatorStrategy, | ||
93 | viatraConfig.hints, | ||
94 | viatraConfig.documentationLevel | ||
95 | ) | 83 | ) |
96 | 84 | ||
97 | val compositeObjective = new ModelGenerationCompositeObjective( | 85 | val compositeObjective = new ModelGenerationCompositeObjective( |
@@ -111,45 +99,21 @@ class ViatraReasoner extends LogicReasoner { | |||
111 | dse.addObjective(punishObjective) | 99 | dse.addObjective(punishObjective) |
112 | } | 100 | } |
113 | 101 | ||
114 | val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) | 102 | for (costObjective : method.costObjectives) { |
115 | for (entry : viatraConfig.costObjectives.indexed) { | ||
116 | val objectiveName = '''costObjective«entry.key»''' | ||
117 | val objectiveConfig = entry.value | ||
118 | val elementsBuilder = ImmutableList.builder | ||
119 | for (elementConfig : objectiveConfig.elements) { | ||
120 | val relationName = elementConfig.patternQualifiedName | ||
121 | val modalQueries = method.modalRelationQueries.get(relationName) | ||
122 | if (modalQueries === null) { | ||
123 | throw new IllegalArgumentException("Unknown relation: " + relationName) | ||
124 | } | ||
125 | elementsBuilder.add(new ThreeValuedCostElement( | ||
126 | modalQueries.currentQuery, | ||
127 | modalQueries.mayQuery, | ||
128 | modalQueries.mustQuery, | ||
129 | elementConfig.weight | ||
130 | )) | ||
131 | } | ||
132 | val costElements = elementsBuilder.build | ||
133 | val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind, | ||
134 | objectiveConfig.threshold, 3) | ||
135 | dse.addObjective(costObjective) | 103 | dse.addObjective(costObjective) |
136 | if (objectiveConfig.findExtremum) { | ||
137 | extremalObjectives += costObjective | ||
138 | } | ||
139 | } | 104 | } |
140 | |||
141 | val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions | 105 | val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions |
142 | val solutionStore = if (extremalObjectives.empty) { | 106 | val solutionStore = if (method.optimizationProblem) { |
143 | new SolutionStore(numberOfRequiredSolutions) | ||
144 | } else { | ||
145 | new SolutionStore() | 107 | new SolutionStore() |
108 | } else { | ||
109 | new SolutionStore(numberOfRequiredSolutions) | ||
146 | } | 110 | } |
147 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) | 111 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) |
148 | val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement) | ||
149 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) | 112 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) |
150 | val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, | 113 | val solutionSaver = method.solutionSaver |
151 | diversityChecker, numericSolver) | 114 | solutionSaver.numericSolver = numericSolver |
152 | val solutionCopier = solutionSaver.solutionCopier | 115 | val solutionCopier = solutionSaver.solutionCopier |
116 | val diversityChecker = solutionSaver.diversityChecker | ||
153 | solutionStore.withSolutionSaver(solutionSaver) | 117 | solutionStore.withSolutionSaver(solutionSaver) |
154 | dse.solutionStore = solutionStore | 118 | dse.solutionStore = solutionStore |
155 | 119 | ||
@@ -184,7 +148,8 @@ class ViatraReasoner extends LogicReasoner { | |||
184 | dse.addTransformationRule(rule) | 148 | dse.addTransformationRule(rule) |
185 | } | 149 | } |
186 | 150 | ||
187 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver) | 151 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, |
152 | numericSolver) | ||
188 | viatraConfig.progressMonitor.workedForwardTransformation | 153 | viatraConfig.progressMonitor.workedForwardTransformation |
189 | val transformationFinished = System.nanoTime | 154 | val transformationFinished = System.nanoTime |
190 | val transformationTime = transformationFinished - transformationStartTime | 155 | val transformationTime = transformationFinished - transformationStartTime |
@@ -210,14 +175,15 @@ class ViatraReasoner extends LogicReasoner { | |||
210 | it.value = (pair.value / 1000000) as int | 175 | it.value = (pair.value / 1000000) as int |
211 | ] | 176 | ] |
212 | } | 177 | } |
213 | for(x: 0..<strategy.times.size) { | 178 | for (x : 0 ..< strategy.times.size) { |
214 | it.entries += createStringStatisticEntry => [ | 179 | it.entries += createStringStatisticEntry => [ |
215 | it.name = '''Solution«x+1»DetailedStatistics''' | 180 | it.name = '''Solution«x+1»DetailedStatistics''' |
216 | it.value = strategy.times.get(x) | 181 | it.value = strategy.times.get(x) |
217 | ] | 182 | ] |
218 | } | 183 | } |
219 | it.entries += createIntStatisticEntry => [ | 184 | it.entries += createIntStatisticEntry => [ |
220 | it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int | 185 | it.name = "ExplorationInitializationTime" |
186 | it.value = ((strategy.explorationStarted - transformationFinished) / 1000000) as int | ||
221 | ] | 187 | ] |
222 | it.entries += createIntStatisticEntry => [ | 188 | it.entries += createIntStatisticEntry => [ |
223 | it.name = "TransformationExecutionTime" | 189 | it.name = "TransformationExecutionTime" |
@@ -228,6 +194,10 @@ class ViatraReasoner extends LogicReasoner { | |||
228 | it.value = (method.statistics.scopePropagationTime / 1000000) as int | 194 | it.value = (method.statistics.scopePropagationTime / 1000000) as int |
229 | ] | 195 | ] |
230 | it.entries += createIntStatisticEntry => [ | 196 | it.entries += createIntStatisticEntry => [ |
197 | it.name = "MustRelationPropagationTime" | ||
198 | it.value = (method.statistics.mustRelationPropagationTime / 1000000) as int | ||
199 | ] | ||
200 | it.entries += createIntStatisticEntry => [ | ||
231 | it.name = "TypeAnalysisTime" | 201 | it.name = "TypeAnalysisTime" |
232 | it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int | 202 | it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int |
233 | ] | 203 | ] |
@@ -248,22 +218,28 @@ class ViatraReasoner extends LogicReasoner { | |||
248 | it.value = dse.numberOfStates as int | 218 | it.value = dse.numberOfStates as int |
249 | ] | 219 | ] |
250 | it.entries += createIntStatisticEntry => [ | 220 | it.entries += createIntStatisticEntry => [ |
251 | it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int | 221 | it.name = "ForwardTime" |
222 | it.value = (strategy.forwardTime / 1000000) as int | ||
252 | ] | 223 | ] |
253 | it.entries += createIntStatisticEntry => [ | 224 | it.entries += createIntStatisticEntry => [ |
254 | it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int | 225 | it.name = "BacktrackingTime" |
226 | it.value = (strategy.backtrackingTime / 1000000) as int | ||
255 | ] | 227 | ] |
256 | it.entries += createIntStatisticEntry => [ | 228 | it.entries += createIntStatisticEntry => [ |
257 | it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int | 229 | it.name = "GlobalConstraintEvaluationTime" |
230 | it.value = (strategy.globalConstraintEvaluationTime / 1000000) as int | ||
258 | ] | 231 | ] |
259 | it.entries += createIntStatisticEntry => [ | 232 | it.entries += createIntStatisticEntry => [ |
260 | it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int | 233 | it.name = "FitnessCalculationTime" |
234 | it.value = (strategy.fitnessCalculationTime / 1000000) as int | ||
261 | ] | 235 | ] |
262 | it.entries += createIntStatisticEntry => [ | 236 | it.entries += createIntStatisticEntry => [ |
263 | it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int | 237 | it.name = "SolutionCopyTime" |
238 | it.value = (solutionSaver.totalCopierRuntime / 1000000) as int | ||
264 | ] | 239 | ] |
265 | it.entries += createIntStatisticEntry => [ | 240 | it.entries += createIntStatisticEntry => [ |
266 | it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int | 241 | it.name = "ActivationSelectionTime" |
242 | it.value = (strategy.activationSelector.runtime / 1000000) as int | ||
267 | ] | 243 | ] |
268 | it.entries += createIntStatisticEntry => [ | 244 | it.entries += createIntStatisticEntry => [ |
269 | it.name = "Decisions" | 245 | it.name = "Decisions" |
@@ -282,27 +258,34 @@ class ViatraReasoner extends LogicReasoner { | |||
282 | it.value = method.statistics.scopePropagatorSolverInvocations | 258 | it.value = method.statistics.scopePropagatorSolverInvocations |
283 | ] | 259 | ] |
284 | it.entries += createIntStatisticEntry => [ | 260 | it.entries += createIntStatisticEntry => [ |
285 | it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int | 261 | it.name = "NumericalSolverSumTime" |
262 | it.value = (strategy.numericSolver.runtime / 1000000) as int | ||
286 | ] | 263 | ] |
287 | it.entries += createIntStatisticEntry => [ | 264 | it.entries += createIntStatisticEntry => [ |
288 | it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int | 265 | it.name = "NumericalSolverProblemFormingTime" |
266 | it.value = (strategy.numericSolver.solverFormingProblem / 1000000) as int | ||
289 | ] | 267 | ] |
290 | it.entries += createIntStatisticEntry => [ | 268 | it.entries += createIntStatisticEntry => [ |
291 | it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int | 269 | it.name = "NumericalSolverSolvingTime" |
270 | it.value = (strategy.numericSolver.solverSolvingProblem / 1000000) as int | ||
292 | ] | 271 | ] |
293 | it.entries += createIntStatisticEntry => [ | 272 | it.entries += createIntStatisticEntry => [ |
294 | it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int | 273 | it.name = "NumericalSolverInterpretingSolution" |
274 | it.value = (strategy.numericSolver.solverSolution / 1000000) as int | ||
295 | ] | 275 | ] |
296 | it.entries += createIntStatisticEntry => [ | 276 | it.entries += createIntStatisticEntry => [ |
297 | it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int | 277 | it.name = "NumericalSolverCachingTime" |
278 | it.value = (strategy.numericSolver.cachingTime / 1000000) as int | ||
298 | ] | 279 | ] |
299 | it.entries += createIntStatisticEntry => [ | 280 | it.entries += createIntStatisticEntry => [ |
300 | it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls | 281 | it.name = "NumericalSolverCallNumber" |
282 | it.value = strategy.numericSolver.numberOfSolverCalls | ||
301 | ] | 283 | ] |
302 | it.entries += createIntStatisticEntry => [ | 284 | it.entries += createIntStatisticEntry => [ |
303 | it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls | 285 | it.name = "NumericalSolverCachedAnswerNumber" |
286 | it.value = strategy.numericSolver.numberOfCachedSolverCalls | ||
304 | ] | 287 | ] |
305 | if(diversityChecker.active) { | 288 | if (diversityChecker.active) { |
306 | it.entries += createIntStatisticEntry => [ | 289 | it.entries += createIntStatisticEntry => [ |
307 | it.name = "SolutionDiversityCheckTime" | 290 | it.name = "SolutionDiversityCheckTime" |
308 | it.value = (diversityChecker.totalRuntime / 1000000) as int | 291 | it.value = (diversityChecker.totalRuntime / 1000000) as int |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index 0173124c..fbe6da9d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | |||
@@ -4,19 +4,20 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold |
15 | import java.util.LinkedList | 17 | import java.util.LinkedList |
16 | import java.util.List | 18 | import java.util.List |
17 | import java.util.Set | 19 | import java.util.Set |
18 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 20 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
20 | 21 | ||
21 | enum StateCoderStrategy { | 22 | enum StateCoderStrategy { |
22 | Neighbourhood, | 23 | Neighbourhood, |
@@ -77,6 +78,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
77 | public var List<LinearTypeConstraintHint> hints = newArrayList | 78 | public var List<LinearTypeConstraintHint> hints = newArrayList |
78 | 79 | ||
79 | public var List<CostObjectiveConfiguration> costObjectives = newArrayList | 80 | public var List<CostObjectiveConfiguration> costObjectives = newArrayList |
81 | |||
82 | public var List<UnitPropagationPatternGenerator> unitPropagationPatternGenerators = newArrayList | ||
80 | } | 83 | } |
81 | 84 | ||
82 | class DiversityDescriptor { | 85 | class DiversityDescriptor { |
@@ -111,9 +114,11 @@ class CostObjectiveConfiguration { | |||
111 | public var ObjectiveKind kind | 114 | public var ObjectiveKind kind |
112 | public var ObjectiveThreshold threshold | 115 | public var ObjectiveThreshold threshold |
113 | public var boolean findExtremum | 116 | public var boolean findExtremum |
117 | public var CostObjectiveHint hint | ||
114 | } | 118 | } |
115 | 119 | ||
116 | class CostObjectiveElementConfiguration { | 120 | class CostObjectiveElementConfiguration { |
117 | public var String patternQualifiedName | 121 | public var String patternQualifiedName |
118 | public var int weight | 122 | public var int weight |
119 | } | 123 | } |
124 | |||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index a2de1abc..4b7cead1 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java | |||
@@ -28,8 +28,6 @@ import org.eclipse.viatra.dse.objectives.Fitness; | |||
28 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; | 28 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; |
29 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; | 29 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; |
30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; | 30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; |
31 | import org.eclipse.viatra.query.runtime.api.IPatternMatch; | ||
32 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; | ||
33 | 31 | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 32 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
35 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 33 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
@@ -37,12 +35,11 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; | 35 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; |
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 36 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 37 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
40 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; | ||
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | 38 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; |
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | 39 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; |
43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder; | ||
44 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; | 40 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; |
45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; | 41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; |
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod; | ||
46 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; | 43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; |
47 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 44 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
48 | 45 | ||
@@ -301,13 +298,12 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
301 | return activationIds; | 298 | return activationIds; |
302 | } | 299 | } |
303 | 300 | ||
304 | private void checkForSolution(final Fitness fittness) { | 301 | private void checkForSolution(final Fitness fitness) { |
305 | solutionStore.newSolution(context); | 302 | solutionStore.newSolution(context); |
306 | } | 303 | } |
307 | 304 | ||
308 | public List<String> times = new LinkedList<String>(); | 305 | public List<String> times = new LinkedList<String>(); |
309 | private void saveTimes() { | 306 | private void saveTimes() { |
310 | long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder<?, ?>)this.context.getStateCoder()).getStatecoderRuntime()/1000000; | ||
311 | long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000; | 307 | long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000; |
312 | long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000; | 308 | long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000; |
313 | long activationSelection = this.activationSelector.getRuntime()/1000000; | 309 | long activationSelection = this.activationSelector.getRuntime()/1000000; |
@@ -317,8 +313,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
317 | long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; | 313 | long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; |
318 | long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; | 314 | long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; |
319 | this.times.add( | 315 | this.times.add( |
320 | "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ | 316 | "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ |
321 | "|StateCoderTime:"+statecoderTime+ | ||
322 | "|ForwardTime:"+forwardTime+ | 317 | "|ForwardTime:"+forwardTime+ |
323 | "|Backtrackingtime:"+backtrackingTime+ | 318 | "|Backtrackingtime:"+backtrackingTime+ |
324 | "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+ | 319 | "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+ |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 066040a0..70e8e9c2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -1,13 +1,13 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | ||
11 | import java.math.BigDecimal | 11 | import java.math.BigDecimal |
12 | import java.util.HashMap | 12 | import java.util.HashMap |
13 | import java.util.LinkedHashMap | 13 | import java.util.LinkedHashMap |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index cfd11816..b48d0831 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | |||
@@ -22,12 +22,13 @@ import java.util.List | |||
22 | import java.util.Map | 22 | import java.util.Map |
23 | import java.util.TreeSet | 23 | import java.util.TreeSet |
24 | import org.eclipse.emf.ecore.EObject | 24 | import org.eclipse.emf.ecore.EObject |
25 | import org.eclipse.xtend.lib.annotations.Accessors | ||
25 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 26 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
26 | 27 | ||
27 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
28 | 29 | ||
29 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | 30 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ |
30 | val PartialInterpretation partialInterpretation | 31 | @Accessors val PartialInterpretation partialInterpretation |
31 | val Map<EObject, EObject> trace; | 32 | val Map<EObject, EObject> trace; |
32 | val Map<TypeDeclaration,PartialComplexTypeInterpretation> type2Interpretation | 33 | val Map<TypeDeclaration,PartialComplexTypeInterpretation> type2Interpretation |
33 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation | 34 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend index 38c8f5a1..33b69436 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend | |||
@@ -26,16 +26,12 @@ class CopiedSolution { | |||
26 | * using the supplied {@link NumericSolver}. | 26 | * using the supplied {@link NumericSolver}. |
27 | */ | 27 | */ |
28 | class SolutionCopier { | 28 | class SolutionCopier { |
29 | val NumericSolver numericSolver | ||
30 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> | 29 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> |
31 | 30 | ||
31 | @Accessors NumericSolver numericSolver | ||
32 | long startTime = System.nanoTime | 32 | long startTime = System.nanoTime |
33 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 | 33 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 |
34 | 34 | ||
35 | new(NumericSolver numericSolver) { | ||
36 | this.numericSolver = numericSolver | ||
37 | } | ||
38 | |||
39 | def void copySolution(ThreadContext context, Object solutionId) { | 35 | def void copySolution(ThreadContext context, Object solutionId) { |
40 | val existingCopy = copiedSolutions.get(solutionId) | 36 | val existingCopy = copiedSolutions.get(solutionId) |
41 | if (existingCopy === null) { | 37 | if (existingCopy === null) { |
@@ -47,7 +43,7 @@ class SolutionCopier { | |||
47 | totalCopierRuntime += System.nanoTime - copyStart | 43 | totalCopierRuntime += System.nanoTime - copyStart |
48 | val copierRuntime = System.nanoTime - startTime | 44 | val copierRuntime = System.nanoTime - startTime |
49 | val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) | 45 | val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) |
50 | numericSolver.fillSolutionCopy(copiedSolution.trace) | 46 | numericSolver?.fillSolutionCopy(copiedSolution.trace) |
51 | copiedSolutions.put(solutionId, copiedSolution) | 47 | copiedSolutions.put(solutionId, copiedSolution) |
52 | } else { | 48 | } else { |
53 | existingCopy.current = true | 49 | existingCopy.current = true |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend index c0b5008c..e00f76ff 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend | |||
@@ -1,5 +1,9 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | ||
3 | import java.util.HashMap | 7 | import java.util.HashMap |
4 | import java.util.Map | 8 | import java.util.Map |
5 | import org.eclipse.viatra.dse.api.DSEException | 9 | import org.eclipse.viatra.dse.api.DSEException |
@@ -18,24 +22,32 @@ import org.eclipse.xtend.lib.annotations.Accessors | |||
18 | * Will also automatically fill any missing numerical values in the saved solutions | 22 | * Will also automatically fill any missing numerical values in the saved solutions |
19 | * using the supplied {@link NumericSolver}. | 23 | * using the supplied {@link NumericSolver}. |
20 | */ | 24 | */ |
21 | class ViatraReasonerSolutionSaver implements ISolutionSaver { | 25 | class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider { |
26 | static val TOLERANCE = 1e-10 | ||
27 | |||
22 | @Accessors val SolutionCopier solutionCopier | 28 | @Accessors val SolutionCopier solutionCopier |
23 | val NumericSolver numericSolver | ||
24 | @Accessors val DiversityChecker diversityChecker | 29 | @Accessors val DiversityChecker diversityChecker |
30 | val IObjective[][] leveledExtremalObjectives | ||
25 | val boolean hasExtremalObjectives | 31 | val boolean hasExtremalObjectives |
26 | val int numberOfRequiredSolutions | 32 | val int numberOfRequiredSolutions |
27 | val ObjectiveComparatorHelper comparatorHelper | 33 | val ObjectiveComparatorHelper comparatorHelper |
28 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap | 34 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap |
29 | 35 | ||
30 | @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection | 36 | @Accessors var NumericSolver numericSolver |
37 | @Accessors var Map<Object, Solution> solutionsCollection | ||
31 | 38 | ||
32 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) { | 39 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { |
33 | this.diversityChecker = diversityChecker | 40 | this.diversityChecker = diversityChecker |
34 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) | 41 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) |
42 | this.leveledExtremalObjectives = leveledExtremalObjectives | ||
35 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] | 43 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] |
36 | this.numberOfRequiredSolutions = numberOfRequiredSolutions | 44 | this.numberOfRequiredSolutions = numberOfRequiredSolutions |
37 | this.solutionCopier = new SolutionCopier(numericSolver) | 45 | this.solutionCopier = new SolutionCopier |
46 | } | ||
47 | |||
48 | def setNumericSolver(NumericSolver numericSolver) { | ||
38 | this.numericSolver = numericSolver | 49 | this.numericSolver = numericSolver |
50 | solutionCopier.numericSolver = numericSolver | ||
39 | } | 51 | } |
40 | 52 | ||
41 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | 53 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { |
@@ -51,6 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
51 | if (!shouldSaveSolution(fitness, context)) { | 63 | if (!shouldSaveSolution(fitness, context)) { |
52 | return false | 64 | return false |
53 | } | 65 | } |
66 | println("Found: " + fitness) | ||
54 | val dominatedTrajectories = newArrayList | 67 | val dominatedTrajectories = newArrayList |
55 | for (entry : trajectories.entrySet) { | 68 | for (entry : trajectories.entrySet) { |
56 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) | 69 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) |
@@ -99,7 +112,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
99 | } | 112 | } |
100 | 113 | ||
101 | private def shouldSaveSolution(Fitness fitness, ThreadContext context) { | 114 | private def shouldSaveSolution(Fitness fitness, ThreadContext context) { |
102 | return fitness.satisifiesHardObjectives && numericSolver.currentSatisfiable | 115 | fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable) |
103 | } | 116 | } |
104 | 117 | ||
105 | private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, | 118 | private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, |
@@ -145,8 +158,93 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
145 | } | 158 | } |
146 | solutionsCollection.size < numberOfRequiredSolutions | 159 | solutionsCollection.size < numberOfRequiredSolutions |
147 | } | 160 | } |
148 | 161 | ||
149 | def getTotalCopierRuntime() { | 162 | def getTotalCopierRuntime() { |
150 | solutionCopier.totalCopierRuntime | 163 | solutionCopier.totalCopierRuntime |
151 | } | 164 | } |
165 | |||
166 | override computeRequiredBounds(IObjective objective, Bounds bounds) { | ||
167 | if (!hasExtremalObjectives) { | ||
168 | return | ||
169 | } | ||
170 | if (objective instanceof DirectionalThresholdObjective) { | ||
171 | switch (threshold : objective.threshold) { | ||
172 | case ObjectiveThreshold.NO_THRESHOLD: { | ||
173 | // No threshold to set. | ||
174 | } | ||
175 | ObjectiveThreshold.Exclusive: { | ||
176 | switch (kind : objective.kind) { | ||
177 | case HIGHER_IS_BETTER: | ||
178 | bounds.tightenLowerBound(Math.floor(threshold.threshold + 1) as int) | ||
179 | case LOWER_IS_BETTER: | ||
180 | bounds.tightenUpperBound(Math.ceil(threshold.threshold - 1) as int) | ||
181 | default: | ||
182 | throw new IllegalArgumentException("Unknown objective kind" + kind) | ||
183 | } | ||
184 | if (threshold.clampToThreshold) { | ||
185 | return | ||
186 | } | ||
187 | } | ||
188 | ObjectiveThreshold.Inclusive: { | ||
189 | switch (kind : objective.kind) { | ||
190 | case HIGHER_IS_BETTER: | ||
191 | bounds.tightenLowerBound(Math.ceil(threshold.threshold) as int) | ||
192 | case LOWER_IS_BETTER: | ||
193 | bounds.tightenUpperBound(Math.floor(threshold.threshold) as int) | ||
194 | default: | ||
195 | throw new IllegalArgumentException("Unknown objective kind" + kind) | ||
196 | } | ||
197 | if (threshold.clampToThreshold) { | ||
198 | return | ||
199 | } | ||
200 | } | ||
201 | default: | ||
202 | throw new IllegalArgumentException("Unknown threshold: " + threshold) | ||
203 | } | ||
204 | for (level : leveledExtremalObjectives) { | ||
205 | switch (level.size) { | ||
206 | case 0: { | ||
207 | // Nothing to do, wait for the next level. | ||
208 | } | ||
209 | case 1: { | ||
210 | val primaryObjective = level.get(0) | ||
211 | if (primaryObjective != objective) { | ||
212 | // There are no worst-case bounds for secondary objectives. | ||
213 | return | ||
214 | } | ||
215 | } | ||
216 | default: | ||
217 | // There are no worst-case bounds for Pareto front calculation. | ||
218 | return | ||
219 | } | ||
220 | } | ||
221 | val fitnessIterator = trajectories.values.iterator | ||
222 | if (!fitnessIterator.hasNext) { | ||
223 | return | ||
224 | } | ||
225 | val fitness = fitnessIterator.next.get(objective.name) | ||
226 | while (fitnessIterator.hasNext) { | ||
227 | val otherFitness = fitnessIterator.next.get(objective.name) | ||
228 | if (Math.abs(fitness - otherFitness) > TOLERANCE) { | ||
229 | throw new IllegalStateException("Inconsistent fitness: " + objective.name) | ||
230 | } | ||
231 | } | ||
232 | switch (kind : objective.kind) { | ||
233 | case HIGHER_IS_BETTER: | ||
234 | if (needsMoreSolutionsWithSameFitness) { | ||
235 | bounds.tightenLowerBound(Math.floor(fitness) as int) | ||
236 | } else { | ||
237 | bounds.tightenLowerBound(Math.floor(fitness + 1) as int) | ||
238 | } | ||
239 | case LOWER_IS_BETTER: | ||
240 | if (needsMoreSolutionsWithSameFitness) { | ||
241 | bounds.tightenUpperBound(Math.ceil(fitness) as int) | ||
242 | } else { | ||
243 | bounds.tightenUpperBound(Math.ceil(fitness - 1) as int) | ||
244 | } | ||
245 | default: | ||
246 | throw new IllegalArgumentException("Unknown objective kind" + kind) | ||
247 | } | ||
248 | } | ||
249 | } | ||
152 | } | 250 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend new file mode 100644 index 00000000..885b14e8 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend | |||
@@ -0,0 +1,137 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | ||
6 | import java.util.List | ||
7 | import org.eclipse.emf.ecore.EObject | ||
8 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
9 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
10 | import org.eclipse.xtend.lib.annotations.Data | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
13 | |||
14 | @FunctionalInterface | ||
15 | interface ParameterScopeBound { | ||
16 | def double getUpperBound() | ||
17 | } | ||
18 | |||
19 | @Data | ||
20 | class CostElementMatch { | ||
21 | val IPatternMatch match | ||
22 | val boolean must | ||
23 | |||
24 | def isMulti() { | ||
25 | CostElementMatchers.isMultiMatch(match) | ||
26 | } | ||
27 | } | ||
28 | |||
29 | @Data | ||
30 | class CostElementMatchers { | ||
31 | val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher | ||
32 | val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher | ||
33 | val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher | ||
34 | val List<ParameterScopeBound> parameterScopeBounds | ||
35 | val int weight | ||
36 | |||
37 | def getCurrentNumberOfMatches() { | ||
38 | currentMatcher.countMatches | ||
39 | } | ||
40 | |||
41 | def getMinimumNumberOfMatches() { | ||
42 | mustMatcher.countMatches | ||
43 | } | ||
44 | |||
45 | def getMaximumNumberOfMatches() { | ||
46 | var double sum = 0 | ||
47 | val iterator = mayMatcher.streamAllMatches.iterator | ||
48 | while (iterator.hasNext) { | ||
49 | val match = iterator.next | ||
50 | var double product = 1 | ||
51 | val numberOfParameters = parameterScopeBounds.size | ||
52 | for (var int i = 0; i < numberOfParameters; i++) { | ||
53 | if (isMulti(match.get(i + 2))) { | ||
54 | val scopeBound = parameterScopeBounds.get(i) | ||
55 | product *= scopeBound.upperBound | ||
56 | } | ||
57 | |||
58 | } | ||
59 | sum += product | ||
60 | } | ||
61 | sum | ||
62 | } | ||
63 | |||
64 | def getMatches() { | ||
65 | ImmutableList.copyOf(mayMatcher.streamAllMatches.iterator.map [ match | | ||
66 | new CostElementMatch(match, mustMatcher.isMatch(match)) | ||
67 | ]) | ||
68 | } | ||
69 | |||
70 | def projectMayMatch(IPatternMatch match, int... indices) { | ||
71 | mayMatcher.projectMatch(match, indices) | ||
72 | } | ||
73 | |||
74 | private static def <T extends IPatternMatch> projectMatch(ViatraQueryMatcher<T> matcher, IPatternMatch match, int... indices) { | ||
75 | checkMatch(match) | ||
76 | val n = matcher.specification.parameters.length - 2 | ||
77 | if (indices.length != n) { | ||
78 | throw new IllegalArgumentException("Invalid number of projection indices") | ||
79 | } | ||
80 | val newMatch = matcher.newEmptyMatch | ||
81 | newMatch.set(0, match.get(0)) | ||
82 | newMatch.set(1, match.get(1)) | ||
83 | for (var int i = 0; i < n; i++) { | ||
84 | newMatch.set(i + 2, match.get(indices.get(i))) | ||
85 | } | ||
86 | if (!matcher.hasMatch(newMatch)) { | ||
87 | throw new IllegalArgumentException("Projected match does not exist") | ||
88 | } | ||
89 | return newMatch | ||
90 | } | ||
91 | |||
92 | private static def <T extends IPatternMatch> isMatch(ViatraQueryMatcher<T> matcher, IPatternMatch match) { | ||
93 | val n = matcher.specification.parameters.length | ||
94 | if (n != match.specification.parameters.length) { | ||
95 | throw new IllegalArgumentException("Invalid number of match arguments") | ||
96 | } | ||
97 | val newMatch = matcher.newEmptyMatch | ||
98 | for (var int i = 0; i < n; i++) { | ||
99 | newMatch.set(i, match.get(i)) | ||
100 | } | ||
101 | return matcher.hasMatch(newMatch) | ||
102 | } | ||
103 | |||
104 | static def isMulti(Object o) { | ||
105 | if (o instanceof EObject) { | ||
106 | switch (feature : o.eContainmentFeature) { | ||
107 | case LogicproblemPackage.eINSTANCE.logicProblem_Elements, | ||
108 | case PartialinterpretationPackage.eINSTANCE.partialInterpretation_NewElements: | ||
109 | false | ||
110 | case PartialinterpretationPackage.eINSTANCE.partialInterpretation_OpenWorldElements: | ||
111 | true | ||
112 | default: | ||
113 | throw new IllegalStateException("Unknown containment feature for element: " + feature) | ||
114 | } | ||
115 | } else { | ||
116 | false | ||
117 | } | ||
118 | } | ||
119 | |||
120 | static def isMultiMatch(IPatternMatch match) { | ||
121 | checkMatch(match) | ||
122 | val n = match.specification.parameters.length | ||
123 | for (var int i = 2; i < n; i++) { | ||
124 | if (isMulti(match.get(i))) { | ||
125 | return true | ||
126 | } | ||
127 | } | ||
128 | false | ||
129 | } | ||
130 | |||
131 | private static def checkMatch(IPatternMatch match) { | ||
132 | val n = match.specification.parameters.length | ||
133 | if (n < 2 || !(match.get(0) instanceof LogicProblem) || !(match.get(1) instanceof PartialInterpretation)) { | ||
134 | throw new IllegalArgumentException("Match is not from the partial interpretation") | ||
135 | } | ||
136 | } | ||
137 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend new file mode 100644 index 00000000..2434073d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend | |||
@@ -0,0 +1,68 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilder | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
9 | import java.util.Map | ||
10 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | |||
13 | abstract class CostObjectiveHint implements LinearTypeConstraintHint, BoundSaturationListener { | ||
14 | @Accessors ThreeValuedCostObjective objective | ||
15 | @Accessors IObjectiveBoundsProvider boundsProvider | ||
16 | |||
17 | Integer bestUpper = null | ||
18 | |||
19 | override getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) { | ||
20 | '''''' | ||
21 | } | ||
22 | |||
23 | override createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) { | ||
24 | null | ||
25 | } | ||
26 | |||
27 | def isExact() { | ||
28 | false | ||
29 | } | ||
30 | |||
31 | def PolyhedronExtensionOperator createPolyhedronExtensionOperator( | ||
32 | Map<String, CostElementMatchers> costElementMatchers) { | ||
33 | null | ||
34 | } | ||
35 | |||
36 | def setObjective(ThreeValuedCostObjective objective) { | ||
37 | if (this.objective !== null) { | ||
38 | throw new IllegalStateException("Objective was already set") | ||
39 | } | ||
40 | this.objective = objective | ||
41 | } | ||
42 | |||
43 | def setBoundsProvider(IObjectiveBoundsProvider boundsProvider) { | ||
44 | if (this.boundsProvider !== null) { | ||
45 | throw new IllegalStateException("Objective bounds provider was already set") | ||
46 | } | ||
47 | this.boundsProvider = boundsProvider | ||
48 | } | ||
49 | |||
50 | protected def buildWithBounds(ExtendedLinearExpressionBuilder builder) { | ||
51 | val bounds = builder.build(this) | ||
52 | if (objective !== null && boundsProvider !== null) { | ||
53 | boundsProvider.computeRequiredBounds(objective, bounds) | ||
54 | } | ||
55 | if (exact && bestUpper !== null) { | ||
56 | bounds.tightenLowerBound(bestUpper) | ||
57 | } | ||
58 | bounds | ||
59 | } | ||
60 | |||
61 | override boundsSaturated(Integer lower, Integer upper) { | ||
62 | if (upper !== null && (bestUpper === null || bestUpper < upper)) { | ||
63 | bestUpper = upper | ||
64 | } | ||
65 | objective?.boundsSaturated(lower, upper) | ||
66 | } | ||
67 | |||
68 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend new file mode 100644 index 00000000..3c4d36a5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend | |||
@@ -0,0 +1,8 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds | ||
4 | import org.eclipse.viatra.dse.objectives.IObjective | ||
5 | |||
6 | interface IObjectiveBoundsProvider { | ||
7 | def void computeRequiredBounds(IObjective objective, Bounds bounds) | ||
8 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend index 0a6fd55b..9b1a7e9f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend | |||
@@ -1,85 +1,80 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener |
4 | import java.util.Collection | 4 | import java.util.Map |
5 | import org.eclipse.viatra.dse.base.ThreadContext | 5 | import org.eclipse.viatra.dse.base.ThreadContext |
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 6 | import org.eclipse.xtend.lib.annotations.Accessors |
7 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.xtend.lib.annotations.Data | ||
10 | 7 | ||
11 | @Data | 8 | class ThreeValuedCostObjective extends AbstractThreeValuedObjective implements BoundSaturationListener { |
12 | class ThreeValuedCostElement { | 9 | @Accessors val Map<String, CostElementMatchers> matchers |
13 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentMatchQuery | 10 | double lowerBoundHint = Double.NEGATIVE_INFINITY |
14 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayMatchQuery | 11 | double upperBoundHint = Double.POSITIVE_INFINITY |
15 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustMatchQuery | ||
16 | val int weight | ||
17 | } | ||
18 | |||
19 | class ThreeValuedCostObjective extends AbstractThreeValuedObjective { | ||
20 | val Collection<ThreeValuedCostElement> costElements | ||
21 | Collection<CostElementMatchers> matchers | ||
22 | 12 | ||
23 | new(String name, Collection<ThreeValuedCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold, | 13 | new(String name, Map<String, CostElementMatchers> matchers, ObjectiveKind kind, ObjectiveThreshold threshold, |
24 | int level) { | 14 | int level) { |
25 | super(name, kind, threshold, level) | 15 | super(name, kind, threshold, level) |
26 | this.costElements = costElements | 16 | this.matchers = matchers |
27 | } | 17 | } |
28 | 18 | ||
29 | override createNew() { | 19 | override createNew() { |
30 | new ThreeValuedCostObjective(name, costElements, kind, threshold, level) | 20 | // new ThreeValuedCostObjective(name, matchers, kind, threshold, level) |
21 | throw new UnsupportedOperationException("ThreeValuedCostObjective can only be used from a single thread") | ||
31 | } | 22 | } |
32 | 23 | ||
33 | override init(ThreadContext context) { | 24 | override init(ThreadContext context) { |
34 | val queryEngine = context.queryEngine | ||
35 | matchers = ImmutableList.copyOf(costElements.map [ element | | ||
36 | new CostElementMatchers( | ||
37 | queryEngine.getMatcher(element.currentMatchQuery), | ||
38 | queryEngine.getMatcher(element.mayMatchQuery), | ||
39 | queryEngine.getMatcher(element.mustMatchQuery), | ||
40 | element.weight | ||
41 | ) | ||
42 | ]) | ||
43 | } | 25 | } |
44 | 26 | ||
45 | override getRawFitness(ThreadContext context) { | 27 | override getRawFitness(ThreadContext context) { |
46 | var int cost = 0 | 28 | var double cost = 0 |
47 | for (matcher : matchers) { | 29 | for (matcher : matchers.values) { |
48 | cost += matcher.weight * matcher.currentMatcher.countMatches | 30 | cost += matcher.weight * matcher.currentNumberOfMatches |
49 | } | 31 | } |
50 | cost as double | 32 | cost |
51 | } | 33 | } |
52 | 34 | ||
53 | override getLowestPossibleFitness(ThreadContext threadContext) { | 35 | override getLowestPossibleFitness(ThreadContext threadContext) { |
54 | var int cost = 0 | 36 | var double cost = 0 |
55 | for (matcher : matchers) { | 37 | for (matcher : matchers.values) { |
56 | if (matcher.weight >= 0) { | 38 | if (matcher.weight >= 0) { |
57 | cost += matcher.weight * matcher.mustMatcher.countMatches | 39 | cost += matcher.weight * matcher.minimumNumberOfMatches |
58 | } else if (matcher.mayMatcher.countMatches > 0) { | 40 | } else { |
59 | // TODO Count may matches. | 41 | cost += matcher.weight * matcher.maximumNumberOfMatches |
60 | return Double.NEGATIVE_INFINITY | ||
61 | } | 42 | } |
62 | } | 43 | } |
63 | cost as double | 44 | val boundWithHint = Math.max(lowerBoundHint, cost) |
45 | if (boundWithHint > upperBoundHint) { | ||
46 | throw new IllegalStateException("Inconsistent cost bounds") | ||
47 | } | ||
48 | boundWithHint | ||
64 | } | 49 | } |
65 | 50 | ||
66 | override getHighestPossibleFitness(ThreadContext threadContext) { | 51 | override getHighestPossibleFitness(ThreadContext threadContext) { |
67 | var int cost = 0 | 52 | var double cost = 0 |
68 | for (matcher : matchers) { | 53 | for (matcher : matchers.values) { |
69 | if (matcher.weight <= 0) { | 54 | if (matcher.weight <= 0) { |
70 | cost += matcher.weight * matcher.mustMatcher.countMatches | 55 | cost += matcher.weight * matcher.minimumNumberOfMatches |
71 | } else if (matcher.mayMatcher.countMatches > 0) { | 56 | } else { |
72 | return Double.POSITIVE_INFINITY | 57 | cost += matcher.weight * matcher.maximumNumberOfMatches |
73 | } | 58 | } |
74 | } | 59 | } |
75 | cost as double | 60 | val boundWithHint = Math.min(upperBoundHint, cost) |
61 | if (boundWithHint < lowerBoundHint) { | ||
62 | throw new IllegalStateException("Inconsistent cost bounds") | ||
63 | } | ||
64 | boundWithHint | ||
76 | } | 65 | } |
77 | 66 | ||
78 | @Data | 67 | override boundsSaturated(Integer lower, Integer upper) { |
79 | private static class CostElementMatchers { | 68 | lowerBoundHint = if (lower === null) { |
80 | val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher | 69 | Double.NEGATIVE_INFINITY |
81 | val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher | 70 | } else { |
82 | val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher | 71 | lower |
83 | val int weight | 72 | } |
73 | upperBoundHint = if (upper === null) { | ||
74 | Double.POSITIVE_INFINITY | ||
75 | } else { | ||
76 | upper | ||
77 | } | ||
78 | println('''Bounds saturated: «lower»..«upper»''') | ||
84 | } | 79 | } |
85 | } | 80 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend new file mode 100644 index 00000000..c2750acd --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend | |||
@@ -0,0 +1,205 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import com.google.common.collect.Lists | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration | ||
26 | import java.util.Collection | ||
27 | import java.util.Map | ||
28 | import org.eclipse.viatra.dse.objectives.IObjective | ||
29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
30 | import org.eclipse.xtend.lib.annotations.Data | ||
31 | |||
32 | @Data | ||
33 | class ThreeValuedCostObjectiveProviderResult { | ||
34 | val Collection<IObjective> objectives | ||
35 | val Collection<CostObjectiveHint> hints | ||
36 | val Collection<PolyhedronExtensionOperator> extensionOperators | ||
37 | val IObjective[][] leveledExtremalObjectives | ||
38 | val boolean optimizationProblem | ||
39 | } | ||
40 | |||
41 | class ThreeValuedCostObjectiveProvider { | ||
42 | static val COST_OBJECTIVE_LEVEL = 3 | ||
43 | |||
44 | val ViatraQueryEngine queryEngine | ||
45 | val Map<String, ModalPatternQueries> modalRelationQueries | ||
46 | val Map<String, Relation> qualifiedNameToRelationMap | ||
47 | val ParameterScopeBound defaultBounds | ||
48 | val ParameterScopeBound booleanBounds | ||
49 | val ParameterScopeBound integerBounds | ||
50 | val ParameterScopeBound realBounds | ||
51 | val ParameterScopeBound stringBounds | ||
52 | val Map<TypeDeclaration, ParameterScopeBound> typeDeclarationToBoundsMap | ||
53 | |||
54 | new(ViatraQueryEngine queryEngine, PartialInterpretation interpretation, | ||
55 | Map<String, ModalPatternQueries> modalRelationQueries) { | ||
56 | this.queryEngine = queryEngine | ||
57 | this.modalRelationQueries = modalRelationQueries | ||
58 | qualifiedNameToRelationMap = ImmutableMap.copyOf( | ||
59 | interpretation.problem.annotations.filter(TransfomedViatraQuery). | ||
60 | toMap([patternFullyQualifiedName], [target])) | ||
61 | defaultBounds = new PartialInterpretationBasedParameterScopeBound(interpretation) | ||
62 | var ParameterScopeBound booleanBounds = null | ||
63 | var ParameterScopeBound integerBounds = null | ||
64 | var ParameterScopeBound realBounds = null | ||
65 | var ParameterScopeBound stringBounds = null | ||
66 | val typeDeclarationToBoundsMapBuilder = ImmutableMap.builder | ||
67 | for (scope : interpretation.scopes) { | ||
68 | val bounds = new ScopeBasedParameterScopeBound(scope) | ||
69 | switch (typeInterpretation : scope.targetTypeInterpretation) { | ||
70 | PartialBooleanInterpretation: | ||
71 | if (booleanBounds === null) { | ||
72 | booleanBounds = bounds | ||
73 | } else { | ||
74 | throw new IllegalStateException("Duplicate partial boolean interpretation") | ||
75 | } | ||
76 | PartialIntegerInterpretation: | ||
77 | if (integerBounds === null) { | ||
78 | integerBounds = bounds | ||
79 | } else { | ||
80 | throw new IllegalStateException("Duplicate partial integer interpretation") | ||
81 | } | ||
82 | PartialRealInterpretation: | ||
83 | if (realBounds === null) { | ||
84 | realBounds = bounds | ||
85 | } else { | ||
86 | throw new IllegalStateException("Duplicate partial real interpretation") | ||
87 | } | ||
88 | PartialStringInterpretation: | ||
89 | if (stringBounds === null) { | ||
90 | stringBounds = bounds | ||
91 | } else { | ||
92 | throw new IllegalStateException("Duplicate partial string interpretation") | ||
93 | } | ||
94 | PartialComplexTypeInterpretation: | ||
95 | typeDeclarationToBoundsMapBuilder.put(typeInterpretation.interpretationOf, bounds) | ||
96 | } | ||
97 | } | ||
98 | this.booleanBounds = booleanBounds ?: defaultBounds | ||
99 | this.integerBounds = integerBounds ?: defaultBounds | ||
100 | this.realBounds = realBounds ?: defaultBounds | ||
101 | this.stringBounds = stringBounds ?: defaultBounds | ||
102 | typeDeclarationToBoundsMap = typeDeclarationToBoundsMapBuilder.build | ||
103 | } | ||
104 | |||
105 | def getCostObjectives(Collection<CostObjectiveConfiguration> costObjectives) { | ||
106 | val objectives = ImmutableList.<IObjective>builder | ||
107 | val hints = ImmutableList.<CostObjectiveHint>builder | ||
108 | val extensionOperators = ImmutableList.<PolyhedronExtensionOperator>builder | ||
109 | val extremalObjectives = Lists.newArrayListWithExpectedSize(costObjectives.size) | ||
110 | for (entry : costObjectives.indexed) { | ||
111 | val objectiveName = '''costObjective«entry.key»''' | ||
112 | val objectiveConfig = entry.value | ||
113 | val costObjective = transformCostObjective(objectiveConfig, objectiveName) | ||
114 | objectives.add(costObjective) | ||
115 | if (objectiveConfig.findExtremum) { | ||
116 | extremalObjectives += costObjective | ||
117 | } | ||
118 | val hint = objectiveConfig.hint | ||
119 | if (hint !== null) { | ||
120 | hints.add(hint) | ||
121 | hint.objective = costObjective | ||
122 | val extensionOperator = hint.createPolyhedronExtensionOperator(costObjective.matchers) | ||
123 | if (extensionOperator !== null) { | ||
124 | extensionOperators.add(extensionOperator) | ||
125 | } | ||
126 | } | ||
127 | } | ||
128 | new ThreeValuedCostObjectiveProviderResult( | ||
129 | objectives.build, | ||
130 | hints.build, | ||
131 | extensionOperators.build, | ||
132 | newArrayList(extremalObjectives), | ||
133 | !extremalObjectives.empty | ||
134 | ) | ||
135 | } | ||
136 | |||
137 | private def transformCostObjective(CostObjectiveConfiguration configuration, String name) { | ||
138 | val costElements = ImmutableMap.copyOf(configuration.elements.toMap([patternQualifiedName], [ | ||
139 | transformCostElement | ||
140 | ])) | ||
141 | new ThreeValuedCostObjective(name, costElements, configuration.kind, configuration.threshold, | ||
142 | COST_OBJECTIVE_LEVEL) | ||
143 | } | ||
144 | |||
145 | private def transformCostElement(CostObjectiveElementConfiguration elementConfig) { | ||
146 | val relationName = elementConfig.patternQualifiedName | ||
147 | val modalQueries = modalRelationQueries.get(relationName) | ||
148 | if (modalQueries === null) { | ||
149 | throw new IllegalArgumentException("Unknown relation queries: " + relationName) | ||
150 | } | ||
151 | val relation = qualifiedNameToRelationMap.get(relationName) | ||
152 | if (relation === null) { | ||
153 | throw new IllegalArgumentException("Unknown transformed relation: " + relationName) | ||
154 | } | ||
155 | val parameterBounds = ImmutableList.copyOf(relation.parameters.map[parameterBound]) | ||
156 | new CostElementMatchers( | ||
157 | queryEngine.getMatcher(modalQueries.currentQuery), | ||
158 | queryEngine.getMatcher(modalQueries.mayQuery), | ||
159 | queryEngine.getMatcher(modalQueries.mustQuery), | ||
160 | parameterBounds, | ||
161 | elementConfig.weight | ||
162 | ) | ||
163 | } | ||
164 | |||
165 | private def getParameterBound(TypeReference typeReference) { | ||
166 | switch (typeReference) { | ||
167 | BoolTypeReference: booleanBounds | ||
168 | IntTypeReference: integerBounds | ||
169 | RealTypeReference: realBounds | ||
170 | StringTypeReference: stringBounds | ||
171 | ComplexTypeReference: typeDeclarationToBoundsMap.getOrDefault(typeReference.referred, defaultBounds) | ||
172 | } | ||
173 | } | ||
174 | |||
175 | private static abstract class AbstractParameterScopeBound implements ParameterScopeBound { | ||
176 | override getUpperBound() { | ||
177 | val rawValue = rawUpperBound | ||
178 | if (rawValue < 0) { | ||
179 | Double.POSITIVE_INFINITY | ||
180 | } else { | ||
181 | rawValue | ||
182 | } | ||
183 | } | ||
184 | |||
185 | protected def int getRawUpperBound() | ||
186 | } | ||
187 | |||
188 | @Data | ||
189 | private static class ScopeBasedParameterScopeBound extends AbstractParameterScopeBound { | ||
190 | val Scope scope | ||
191 | |||
192 | override protected getRawUpperBound() { | ||
193 | scope.maxNewElements | ||
194 | } | ||
195 | } | ||
196 | |||
197 | @Data | ||
198 | private static class PartialInterpretationBasedParameterScopeBound extends AbstractParameterScopeBound { | ||
199 | val PartialInterpretation interpretation | ||
200 | |||
201 | override protected getRawUpperBound() { | ||
202 | interpretation.maxNewElements | ||
203 | } | ||
204 | } | ||
205 | } | ||
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java index 7e7a6e51..133ef948 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java | |||
@@ -369,6 +369,7 @@ public class DesignSpaceManager implements IBacktrackListener { | |||
369 | } catch (InvocationTargetException e) { | 369 | } catch (InvocationTargetException e) { |
370 | throw new RuntimeException(e); | 370 | throw new RuntimeException(e); |
371 | } | 371 | } |
372 | backtrackingTime += System.nanoTime() - start; | ||
372 | updateActivationCodes(); | 373 | updateActivationCodes(); |
373 | 374 | ||
374 | Object lastActivationId = trajectory.getLastActivationId(); | 375 | Object lastActivationId = trajectory.getLastActivationId(); |
@@ -382,7 +383,6 @@ public class DesignSpaceManager implements IBacktrackListener { | |||
382 | } | 383 | } |
383 | 384 | ||
384 | logger.debug("Backtrack."); | 385 | logger.debug("Backtrack."); |
385 | backtrackingTime += System.nanoTime() - start; | ||
386 | 386 | ||
387 | return true; | 387 | return true; |
388 | } | 388 | } |