diff options
Diffstat (limited to 'Solvers/VIATRA-Solver')
23 files changed, 1236 insertions, 404 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..ec1557e8 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", |
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/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.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 3bcd9116..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,226 +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.patterns.UnitPropagationPatternGenerator | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries |
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
24 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider |
25 | import java.util.Collection | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
26 | import java.util.List | 26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker |
27 | import java.util.Map | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver |
28 | import java.util.Set | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjectiveProvider |
29 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | 29 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
30 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 30 | import java.util.Collection |
31 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 31 | import java.util.List |
32 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 32 | import java.util.Map |
33 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 33 | import java.util.Set |
34 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 34 | import org.eclipse.viatra.dse.objectives.IObjective |
35 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | 35 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup |
36 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 36 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
37 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 37 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
38 | import org.eclipse.xtend.lib.annotations.Data | 38 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
39 | 39 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | |
40 | class ModelGenerationStatistics { | 40 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
41 | public var long transformationExecutionTime = 0 | 41 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint |
42 | 42 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |
43 | synchronized def addExecutionTime(long amount) { | 43 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
44 | transformationExecutionTime += amount | 44 | import org.eclipse.xtend.lib.annotations.Data |
45 | } | 45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedPolyhedronScopePropagatorStrategy |
46 | 46 | ||
47 | public var long scopePropagationTime = 0 | 47 | @Data class ModelGenerationMethod { |
48 | 48 | ModelGenerationStatistics statistics | |
49 | synchronized def addScopePropagationTime(long amount) { | 49 | |
50 | scopePropagationTime += amount | 50 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules |
51 | } | 51 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules |
52 | 52 | ||
53 | public var long mustRelationPropagationTime = 0 | 53 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities |
54 | 54 | ||
55 | synchronized def addMustRelationPropagationTime(long amount) { | 55 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF |
56 | mustRelationPropagationTime += amount | 56 | |
57 | } | 57 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF |
58 | 58 | ||
59 | public var long preliminaryTypeAnalisisTime = 0 | 59 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions |
60 | 60 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | |
61 | public var int decisionsTried = 0 | 61 | |
62 | 62 | Map<String, ModalPatternQueries> modalRelationQueries | |
63 | synchronized def incrementDecisionCount() { | 63 | |
64 | decisionsTried++ | 64 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns |
65 | } | 65 | |
66 | 66 | Collection<IObjective> costObjectives | |
67 | public var int transformationInvocations | 67 | boolean optimizationProblem |
68 | 68 | ViatraReasonerSolutionSaver solutionSaver | |
69 | synchronized def incrementTransformationCount() { | 69 | } |
70 | transformationInvocations++ | 70 | |
71 | } | 71 | class ModelGenerationMethodProvider { |
72 | 72 | val PatternProvider patternProvider = new PatternProvider | |
73 | public var int scopePropagatorInvocations | 73 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider |
74 | 74 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | |
75 | synchronized def incrementScopePropagationCount() { | 75 | val relationConstraintCalculator = new RelationConstraintCalculator |
76 | scopePropagatorInvocations++ | 76 | |
77 | } | 77 | def ModelGenerationMethod createModelGenerationMethod( |
78 | 78 | LogicProblem logicProblem, | |
79 | public var int scopePropagatorSolverInvocations | 79 | PartialInterpretation emptySolution, |
80 | 80 | ReasonerWorkspace workspace, | |
81 | synchronized def incrementScopePropagationSolverCount() { | 81 | ViatraReasonerConfiguration config |
82 | scopePropagatorSolverInvocations++ | 82 | ) { |
83 | } | 83 | val statistics = new ModelGenerationStatistics |
84 | } | 84 | val debugLevel = config.documentationLevel |
85 | 85 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | |
86 | @Data class ModelGenerationMethod { | 86 | |
87 | ModelGenerationStatistics statistics | 87 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). |
88 | 88 | map[it.patternPQuery as PQuery].toSet | |
89 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules | 89 | |
90 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules | 90 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
91 | 91 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | |
92 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | 92 | workspace, config.typeInferenceMethod, config.scopePropagatorStrategy, relationConstraints, config.hints, |
93 | 93 | config.unitPropagationPatternGenerators, writeFiles) | |
94 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | 94 | |
95 | 95 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | |
96 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | 96 | config.calculateObjectCreationCosts) |
97 | 97 | val unfinishedWF = queries.getUnfinishedWFQueries.values | |
98 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | 98 | val modalRelationQueriesBuilder = ImmutableMap.builder |
99 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | 99 | for (entry : queries.modalRelationQueries.entrySet) { |
100 | 100 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | |
101 | Map<String, ModalPatternQueries> modalRelationQueries | 101 | if (annotation !== null) { |
102 | 102 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | |
103 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | 103 | } |
104 | } | 104 | } |
105 | 105 | val modalRelationQueries = modalRelationQueriesBuilder.build | |
106 | enum TypeInferenceMethod { | 106 | val invalidWF = queries.getInvalidWFQueries.values |
107 | Generic, | 107 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns |
108 | PreliminaryAnalysis | 108 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns |
109 | } | 109 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( |
110 | 110 | queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll( | |
111 | class ModelGenerationMethodProvider { | 111 | queries.mustRelationPropagationQueries.values).addAll(queries.multiplicityConstraintQueries.values.flatMap [ |
112 | val PatternProvider patternProvider = new PatternProvider | 112 | allQueries |
113 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | 113 | ]).addAll(queries.unfinishedWFQueries.values).addAll(queries.invalidWFQueries.values).addAll( |
114 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | 114 | queries.mustUnitPropagationPreconditionPatterns.values).addAll( |
115 | val relationConstraintCalculator = new RelationConstraintCalculator | 115 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build |
116 | 116 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | |
117 | def ModelGenerationMethod createModelGenerationMethod( | 117 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) |
118 | LogicProblem logicProblem, | 118 | |
119 | PartialInterpretation emptySolution, | 119 | val objectiveProvider = new ThreeValuedCostObjectiveProvider(queryEngine, emptySolution, modalRelationQueries) |
120 | ReasonerWorkspace workspace, | 120 | val transformedObjectives = objectiveProvider.getCostObjectives(config.costObjectives) |
121 | boolean nameNewElements, | 121 | |
122 | TypeInferenceMethod typeInferenceMethod, | 122 | val solutionSaver = new ViatraReasonerSolutionSaver(transformedObjectives.leveledExtremalObjectives, |
123 | boolean calculateObjectCreationCosts, | 123 | config.solutionScope.numberOfRequiredSolutions, DiversityChecker.of(config.diversityRequirement)) |
124 | ScopePropagatorStrategy scopePropagatorStrategy, | 124 | |
125 | Collection<LinearTypeConstraintHint> hints, | 125 | val allHints = ImmutableSet.builder |
126 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, | 126 | allHints.addAll(config.hints) |
127 | DocumentationLevel debugLevel | 127 | for (hint : transformedObjectives.hints) { |
128 | ) { | 128 | hint.boundsProvider = solutionSaver |
129 | val statistics = new ModelGenerationStatistics | 129 | allHints.add(hint) |
130 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | 130 | } |
131 | 131 | ||
132 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). | 132 | val scopePropagator = createScopePropagator(config.scopePropagatorStrategy, emptySolution, allHints.build, |
133 | map[it.patternPQuery as PQuery].toSet | 133 | transformedObjectives.extensionOperators, queries, statistics) |
134 | 134 | scopePropagator.propagateAllScopeConstraints | |
135 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 135 | val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, queries, |
136 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 136 | scopePropagator, statistics) |
137 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, | 137 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, |
138 | unitPropagationPatternGenerators, writeFiles) | 138 | queries, unitRulePropagator, config.nameNewElements, statistics) |
139 | 139 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, | |
140 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) | 140 | statistics) |
141 | scopePropagator.propagateAllScopeConstraints | 141 | |
142 | val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, | 142 | return new ModelGenerationMethod( |
143 | queries, scopePropagator, statistics) | 143 | statistics, |
144 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | 144 | objectRefinementRules.values, |
145 | queries, unitRulePropagator, nameNewElements, statistics) | 145 | relationRefinementRules.values, |
146 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, | 146 | unfinishedMultiplicities, |
147 | statistics) | 147 | unfinishedWF, |
148 | 148 | invalidWF, | |
149 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | 149 | mustUnitPropagationPreconditions, |
150 | calculateObjectCreationCosts) | 150 | currentUnitPropagationPreconditions, |
151 | 151 | modalRelationQueries, | |
152 | val unfinishedWF = queries.getUnfinishedWFQueries.values | 152 | queries.allQueries, |
153 | 153 | transformedObjectives.objectives, | |
154 | val modalRelationQueriesBuilder = ImmutableMap.builder | 154 | transformedObjectives.optimizationProblem, |
155 | for (entry : queries.modalRelationQueries.entrySet) { | 155 | solutionSaver |
156 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | 156 | ) |
157 | if (annotation !== null) { | 157 | } |
158 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | 158 | |
159 | } | 159 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, |
160 | } | 160 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, |
161 | val modalRelationQueries = modalRelationQueriesBuilder.build | 161 | Collection<PolyhedronExtensionOperator> extensionOperators, GeneratedPatterns queries, |
162 | 162 | ModelGenerationStatistics statistics) { | |
163 | val invalidWF = queries.getInvalidWFQueries.values | 163 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { |
164 | 164 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | |
165 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns | 165 | } |
166 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | 166 | switch (scopePropagatorStrategy) { |
167 | 167 | case ScopePropagatorStrategy.None, | |
168 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( | 168 | case ScopePropagatorStrategy.Basic: |
169 | queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(queries. | 169 | new ScopePropagator(emptySolution, statistics) |
170 | multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll( | 170 | case ScopePropagatorStrategy.BasicTypeHierarchy: |
171 | queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll( | 171 | new TypeHierarchyScopePropagator(emptySolution, statistics) |
172 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build | 172 | ScopePropagatorStrategy.Polyhedral: { |
173 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | 173 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
174 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) | 174 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] |
175 | 175 | val solver = switch (scopePropagatorStrategy.solver) { | |
176 | return new ModelGenerationMethod( | 176 | case Z3Integer: |
177 | statistics, | 177 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) |
178 | objectRefinementRules.values, | 178 | case Z3Real: |
179 | relationRefinementRules.values, | 179 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) |
180 | unfinishedMultiplicities, | 180 | case Cbc: |
181 | unfinishedWF, | 181 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) |
182 | invalidWF, | 182 | case Clp: |
183 | mustUnitPropagationPreconditions, | 183 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) |
184 | currentUnitPropagationPreconditions, | 184 | default: |
185 | modalRelationQueries, | 185 | throw new IllegalArgumentException("Unknown polyhedron solver: " + |
186 | queries.allQueries | 186 | scopePropagatorStrategy.solver) |
187 | ) | 187 | } |
188 | } | 188 | val strategy = if (extensionOperators.empty) { |
189 | 189 | new CachingSimplePolyhedronScopePropagatorStrategy(solver, statistics) | |
190 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | 190 | } else { |
191 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries, | 191 | new ExtendedPolyhedronScopePropagatorStrategy(solver, extensionOperators, statistics) |
192 | ModelGenerationStatistics statistics) { | 192 | } |
193 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | 193 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, |
194 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | 194 | queries.hasElementInContainmentQuery, allPatternsByName, hints, strategy, |
195 | } | 195 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) |
196 | switch (scopePropagatorStrategy) { | 196 | } |
197 | case ScopePropagatorStrategy.None, | 197 | default: |
198 | case ScopePropagatorStrategy.Basic: | 198 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) |
199 | new ScopePropagator(emptySolution, statistics) | 199 | } |
200 | case ScopePropagatorStrategy.BasicTypeHierarchy: | 200 | } |
201 | new TypeHierarchyScopePropagator(emptySolution, statistics) | 201 | } |
202 | ScopePropagatorStrategy.Polyhedral: { | ||
203 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | ||
204 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
205 | val solver = switch (scopePropagatorStrategy.solver) { | ||
206 | case Z3Integer: | ||
207 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
208 | case Z3Real: | ||
209 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
210 | case Cbc: | ||
211 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
212 | case Clp: | ||
213 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
214 | default: | ||
215 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
216 | scopePropagatorStrategy.solver) | ||
217 | } | ||
218 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
219 | queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, | ||
220 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
221 | } | ||
222 | default: | ||
223 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
224 | } | ||
225 | } | ||
226 | } | ||
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 8e05665c..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,13 +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.unitPropagationPatternGenerators, | ||
95 | viatraConfig.documentationLevel | ||
96 | ) | 83 | ) |
97 | 84 | ||
98 | val compositeObjective = new ModelGenerationCompositeObjective( | 85 | val compositeObjective = new ModelGenerationCompositeObjective( |
@@ -112,45 +99,21 @@ class ViatraReasoner extends LogicReasoner { | |||
112 | dse.addObjective(punishObjective) | 99 | dse.addObjective(punishObjective) |
113 | } | 100 | } |
114 | 101 | ||
115 | val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) | 102 | for (costObjective : method.costObjectives) { |
116 | for (entry : viatraConfig.costObjectives.indexed) { | ||
117 | val objectiveName = '''costObjective«entry.key»''' | ||
118 | val objectiveConfig = entry.value | ||
119 | val elementsBuilder = ImmutableList.builder | ||
120 | for (elementConfig : objectiveConfig.elements) { | ||
121 | val relationName = elementConfig.patternQualifiedName | ||
122 | val modalQueries = method.modalRelationQueries.get(relationName) | ||
123 | if (modalQueries === null) { | ||
124 | throw new IllegalArgumentException("Unknown relation: " + relationName) | ||
125 | } | ||
126 | elementsBuilder.add(new ThreeValuedCostElement( | ||
127 | modalQueries.currentQuery, | ||
128 | modalQueries.mayQuery, | ||
129 | modalQueries.mustQuery, | ||
130 | elementConfig.weight | ||
131 | )) | ||
132 | } | ||
133 | val costElements = elementsBuilder.build | ||
134 | val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind, | ||
135 | objectiveConfig.threshold, 3) | ||
136 | dse.addObjective(costObjective) | 103 | dse.addObjective(costObjective) |
137 | if (objectiveConfig.findExtremum) { | ||
138 | extremalObjectives += costObjective | ||
139 | } | ||
140 | } | 104 | } |
141 | |||
142 | val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions | 105 | val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions |
143 | val solutionStore = if (extremalObjectives.empty) { | 106 | val solutionStore = if (method.optimizationProblem) { |
144 | new SolutionStore(numberOfRequiredSolutions) | ||
145 | } else { | ||
146 | new SolutionStore() | 107 | new SolutionStore() |
108 | } else { | ||
109 | new SolutionStore(numberOfRequiredSolutions) | ||
147 | } | 110 | } |
148 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) | 111 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) |
149 | val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement) | ||
150 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) | 112 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) |
151 | val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, | 113 | val solutionSaver = method.solutionSaver |
152 | diversityChecker, numericSolver) | 114 | solutionSaver.numericSolver = numericSolver |
153 | val solutionCopier = solutionSaver.solutionCopier | 115 | val solutionCopier = solutionSaver.solutionCopier |
116 | val diversityChecker = solutionSaver.diversityChecker | ||
154 | solutionStore.withSolutionSaver(solutionSaver) | 117 | solutionStore.withSolutionSaver(solutionSaver) |
155 | dse.solutionStore = solutionStore | 118 | dse.solutionStore = solutionStore |
156 | 119 | ||
@@ -185,7 +148,8 @@ class ViatraReasoner extends LogicReasoner { | |||
185 | dse.addTransformationRule(rule) | 148 | dse.addTransformationRule(rule) |
186 | } | 149 | } |
187 | 150 | ||
188 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver) | 151 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, |
152 | numericSolver) | ||
189 | viatraConfig.progressMonitor.workedForwardTransformation | 153 | viatraConfig.progressMonitor.workedForwardTransformation |
190 | val transformationFinished = System.nanoTime | 154 | val transformationFinished = System.nanoTime |
191 | val transformationTime = transformationFinished - transformationStartTime | 155 | val transformationTime = transformationFinished - transformationStartTime |
@@ -211,14 +175,15 @@ class ViatraReasoner extends LogicReasoner { | |||
211 | it.value = (pair.value / 1000000) as int | 175 | it.value = (pair.value / 1000000) as int |
212 | ] | 176 | ] |
213 | } | 177 | } |
214 | for(x: 0..<strategy.times.size) { | 178 | for (x : 0 ..< strategy.times.size) { |
215 | it.entries += createStringStatisticEntry => [ | 179 | it.entries += createStringStatisticEntry => [ |
216 | it.name = '''Solution«x+1»DetailedStatistics''' | 180 | it.name = '''Solution«x+1»DetailedStatistics''' |
217 | it.value = strategy.times.get(x) | 181 | it.value = strategy.times.get(x) |
218 | ] | 182 | ] |
219 | } | 183 | } |
220 | it.entries += createIntStatisticEntry => [ | 184 | it.entries += createIntStatisticEntry => [ |
221 | it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int | 185 | it.name = "ExplorationInitializationTime" |
186 | it.value = ((strategy.explorationStarted - transformationFinished) / 1000000) as int | ||
222 | ] | 187 | ] |
223 | it.entries += createIntStatisticEntry => [ | 188 | it.entries += createIntStatisticEntry => [ |
224 | it.name = "TransformationExecutionTime" | 189 | it.name = "TransformationExecutionTime" |
@@ -253,22 +218,28 @@ class ViatraReasoner extends LogicReasoner { | |||
253 | it.value = dse.numberOfStates as int | 218 | it.value = dse.numberOfStates as int |
254 | ] | 219 | ] |
255 | it.entries += createIntStatisticEntry => [ | 220 | it.entries += createIntStatisticEntry => [ |
256 | it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int | 221 | it.name = "ForwardTime" |
222 | it.value = (strategy.forwardTime / 1000000) as int | ||
257 | ] | 223 | ] |
258 | it.entries += createIntStatisticEntry => [ | 224 | it.entries += createIntStatisticEntry => [ |
259 | it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int | 225 | it.name = "BacktrackingTime" |
226 | it.value = (strategy.backtrackingTime / 1000000) as int | ||
260 | ] | 227 | ] |
261 | it.entries += createIntStatisticEntry => [ | 228 | it.entries += createIntStatisticEntry => [ |
262 | it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int | 229 | it.name = "GlobalConstraintEvaluationTime" |
230 | it.value = (strategy.globalConstraintEvaluationTime / 1000000) as int | ||
263 | ] | 231 | ] |
264 | it.entries += createIntStatisticEntry => [ | 232 | it.entries += createIntStatisticEntry => [ |
265 | it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int | 233 | it.name = "FitnessCalculationTime" |
234 | it.value = (strategy.fitnessCalculationTime / 1000000) as int | ||
266 | ] | 235 | ] |
267 | it.entries += createIntStatisticEntry => [ | 236 | it.entries += createIntStatisticEntry => [ |
268 | it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int | 237 | it.name = "SolutionCopyTime" |
238 | it.value = (solutionSaver.totalCopierRuntime / 1000000) as int | ||
269 | ] | 239 | ] |
270 | it.entries += createIntStatisticEntry => [ | 240 | it.entries += createIntStatisticEntry => [ |
271 | it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int | 241 | it.name = "ActivationSelectionTime" |
242 | it.value = (strategy.activationSelector.runtime / 1000000) as int | ||
272 | ] | 243 | ] |
273 | it.entries += createIntStatisticEntry => [ | 244 | it.entries += createIntStatisticEntry => [ |
274 | it.name = "Decisions" | 245 | it.name = "Decisions" |
@@ -287,27 +258,34 @@ class ViatraReasoner extends LogicReasoner { | |||
287 | it.value = method.statistics.scopePropagatorSolverInvocations | 258 | it.value = method.statistics.scopePropagatorSolverInvocations |
288 | ] | 259 | ] |
289 | it.entries += createIntStatisticEntry => [ | 260 | it.entries += createIntStatisticEntry => [ |
290 | it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int | 261 | it.name = "NumericalSolverSumTime" |
262 | it.value = (strategy.numericSolver.runtime / 1000000) as int | ||
291 | ] | 263 | ] |
292 | it.entries += createIntStatisticEntry => [ | 264 | it.entries += createIntStatisticEntry => [ |
293 | it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int | 265 | it.name = "NumericalSolverProblemFormingTime" |
266 | it.value = (strategy.numericSolver.solverFormingProblem / 1000000) as int | ||
294 | ] | 267 | ] |
295 | it.entries += createIntStatisticEntry => [ | 268 | it.entries += createIntStatisticEntry => [ |
296 | it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int | 269 | it.name = "NumericalSolverSolvingTime" |
270 | it.value = (strategy.numericSolver.solverSolvingProblem / 1000000) as int | ||
297 | ] | 271 | ] |
298 | it.entries += createIntStatisticEntry => [ | 272 | it.entries += createIntStatisticEntry => [ |
299 | it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int | 273 | it.name = "NumericalSolverInterpretingSolution" |
274 | it.value = (strategy.numericSolver.solverSolution / 1000000) as int | ||
300 | ] | 275 | ] |
301 | it.entries += createIntStatisticEntry => [ | 276 | it.entries += createIntStatisticEntry => [ |
302 | it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int | 277 | it.name = "NumericalSolverCachingTime" |
278 | it.value = (strategy.numericSolver.cachingTime / 1000000) as int | ||
303 | ] | 279 | ] |
304 | it.entries += createIntStatisticEntry => [ | 280 | it.entries += createIntStatisticEntry => [ |
305 | it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls | 281 | it.name = "NumericalSolverCallNumber" |
282 | it.value = strategy.numericSolver.numberOfSolverCalls | ||
306 | ] | 283 | ] |
307 | it.entries += createIntStatisticEntry => [ | 284 | it.entries += createIntStatisticEntry => [ |
308 | it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls | 285 | it.name = "NumericalSolverCachedAnswerNumber" |
286 | it.value = strategy.numericSolver.numberOfCachedSolverCalls | ||
309 | ] | 287 | ] |
310 | if(diversityChecker.active) { | 288 | if (diversityChecker.active) { |
311 | it.entries += createIntStatisticEntry => [ | 289 | it.entries += createIntStatisticEntry => [ |
312 | it.name = "SolutionDiversityCheckTime" | 290 | it.name = "SolutionDiversityCheckTime" |
313 | 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 a2ed6016..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,7 +4,6 @@ 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 |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints |
@@ -12,6 +11,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr | |||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator |
14 | 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 | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold |
17 | import java.util.LinkedList | 17 | import java.util.LinkedList |
@@ -114,9 +114,11 @@ class CostObjectiveConfiguration { | |||
114 | public var ObjectiveKind kind | 114 | public var ObjectiveKind kind |
115 | public var ObjectiveThreshold threshold | 115 | public var ObjectiveThreshold threshold |
116 | public var boolean findExtremum | 116 | public var boolean findExtremum |
117 | public var CostObjectiveHint hint | ||
117 | } | 118 | } |
118 | 119 | ||
119 | class CostObjectiveElementConfiguration { | 120 | class CostObjectiveElementConfiguration { |
120 | public var String patternQualifiedName | 121 | public var String patternQualifiedName |
121 | public var int weight | 122 | public var int weight |
122 | } | 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 4800f71d..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,7 +298,7 @@ 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 | ||
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 | } | ||