aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-11-02 02:02:40 +0100
committerLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-11-02 02:02:40 +0100
commitf06427cd7375551582461f91b3458339a8227f9b (patch)
tree97bc6ec85f4c384e5080a6611b492caf460b6ce9 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
parentMust unit propagation (diff)
downloadVIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.tar.gz
VIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.tar.zst
VIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.zip
Optimizing generator with linear objective functions
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF3
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend226
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend47
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend44
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend140
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend63
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend54
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend92
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend13
9 files changed, 414 insertions, 268 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
12Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", 13Require-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/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
deleted file mode 100644
index 3bcd9116..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ /dev/null
@@ -1,226 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
2
3import com.google.common.collect.ImmutableMap
4import com.google.common.collect.ImmutableSet
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
7import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator
12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
19import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider
20import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator
21import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider
22import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider
23import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
24import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
25import java.util.Collection
26import java.util.List
27import java.util.Map
28import java.util.Set
29import org.eclipse.viatra.query.runtime.api.GenericQueryGroup
30import org.eclipse.viatra.query.runtime.api.IPatternMatch
31import org.eclipse.viatra.query.runtime.api.IQuerySpecification
32import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
33import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
34import org.eclipse.viatra.query.runtime.emf.EMFScope
35import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
36import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
37import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
38import org.eclipse.xtend.lib.annotations.Data
39
40class ModelGenerationStatistics {
41 public var long transformationExecutionTime = 0
42
43 synchronized def addExecutionTime(long amount) {
44 transformationExecutionTime += amount
45 }
46
47 public var long scopePropagationTime = 0
48
49 synchronized def addScopePropagationTime(long amount) {
50 scopePropagationTime += amount
51 }
52
53 public var long mustRelationPropagationTime = 0
54
55 synchronized def addMustRelationPropagationTime(long amount) {
56 mustRelationPropagationTime += amount
57 }
58
59 public var long preliminaryTypeAnalisisTime = 0
60
61 public var int decisionsTried = 0
62
63 synchronized def incrementDecisionCount() {
64 decisionsTried++
65 }
66
67 public var int transformationInvocations
68
69 synchronized def incrementTransformationCount() {
70 transformationInvocations++
71 }
72
73 public var int scopePropagatorInvocations
74
75 synchronized def incrementScopePropagationCount() {
76 scopePropagatorInvocations++
77 }
78
79 public var int scopePropagatorSolverInvocations
80
81 synchronized def incrementScopePropagationSolverCount() {
82 scopePropagatorSolverInvocations++
83 }
84}
85
86@Data class ModelGenerationMethod {
87 ModelGenerationStatistics statistics
88
89 Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules
90 Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules
91
92 List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities
93
94 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF
95
96 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
97
98 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions
99 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions
100
101 Map<String, ModalPatternQueries> modalRelationQueries
102
103 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
104}
105
106enum TypeInferenceMethod {
107 Generic,
108 PreliminaryAnalysis
109}
110
111class ModelGenerationMethodProvider {
112 val PatternProvider patternProvider = new PatternProvider
113 val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider
114 val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider
115 val relationConstraintCalculator = new RelationConstraintCalculator
116
117 def ModelGenerationMethod createModelGenerationMethod(
118 LogicProblem logicProblem,
119 PartialInterpretation emptySolution,
120 ReasonerWorkspace workspace,
121 boolean nameNewElements,
122 TypeInferenceMethod typeInferenceMethod,
123 boolean calculateObjectCreationCosts,
124 ScopePropagatorStrategy scopePropagatorStrategy,
125 Collection<LinearTypeConstraintHint> hints,
126 Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators,
127 DocumentationLevel debugLevel
128 ) {
129 val statistics = new ModelGenerationStatistics
130 val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL)
131
132 val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery).
133 map[it.patternPQuery as PQuery].toSet
134
135 val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)
136 val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,
137 workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints,
138 unitPropagationPatternGenerators, writeFiles)
139
140 val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics)
141 scopePropagator.propagateAllScopeConstraints
142 val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution,
143 queries, scopePropagator, statistics)
144 val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution,
145 queries, unitRulePropagator, nameNewElements, statistics)
146 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator,
147 statistics)
148
149 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries,
150 calculateObjectCreationCosts)
151
152 val unfinishedWF = queries.getUnfinishedWFQueries.values
153
154 val modalRelationQueriesBuilder = ImmutableMap.builder
155 for (entry : queries.modalRelationQueries.entrySet) {
156 val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head
157 if (annotation !== null) {
158 modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value)
159 }
160 }
161 val modalRelationQueries = modalRelationQueriesBuilder.build
162
163 val invalidWF = queries.getInvalidWFQueries.values
164
165 val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
166 val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
167
168 val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll(
169 queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(queries.
170 multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll(
171 queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll(
172 queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build
173 val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution))
174 GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine)
175
176 return new ModelGenerationMethod(
177 statistics,
178 objectRefinementRules.values,
179 relationRefinementRules.values,
180 unfinishedMultiplicities,
181 unfinishedWF,
182 invalidWF,
183 mustUnitPropagationPreconditions,
184 currentUnitPropagationPreconditions,
185 modalRelationQueries,
186 queries.allQueries
187 )
188 }
189
190 private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,
191 PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries,
192 ModelGenerationStatistics statistics) {
193 if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) {
194 throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.")
195 }
196 switch (scopePropagatorStrategy) {
197 case ScopePropagatorStrategy.None,
198 case ScopePropagatorStrategy.Basic:
199 new ScopePropagator(emptySolution, statistics)
200 case ScopePropagatorStrategy.BasicTypeHierarchy:
201 new TypeHierarchyScopePropagator(emptySolution, statistics)
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.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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
2
3class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
2
3import com.google.common.collect.ImmutableMap
4import com.google.common.collect.ImmutableSet
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
7import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator
17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
19import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
20import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider
21import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator
22import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider
23import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider
24import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
25import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
26import java.util.Collection
27import java.util.List
28import java.util.Map
29import java.util.Set
30import org.eclipse.viatra.query.runtime.api.GenericQueryGroup
31import org.eclipse.viatra.query.runtime.api.IPatternMatch
32import org.eclipse.viatra.query.runtime.api.IQuerySpecification
33import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
34import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
35import org.eclipse.viatra.query.runtime.emf.EMFScope
36import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
37import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
38import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
39import org.eclipse.xtend.lib.annotations.Data
40
41enum 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.ImmutableMap
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import java.util.ArrayList
7import java.util.HashMap
8import java.util.HashSet
9import java.util.List
10import java.util.Map
11import java.util.Set
12import org.eclipse.viatra.query.runtime.api.IPatternMatch
13import org.eclipse.xtend.lib.annotations.Accessors
14import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
15
16interface BoundSaturationListener {
17 def void boundsSaturated(Integer lower, Integer upper)
18}
19
20interface ExtendedLinearExpressionBuilderFactory {
21 def ExtendedLinearExpressionBuilder createBuilder()
22
23 def Dimension getDimension(IPatternMatch patternMatch)
24}
25
26interface 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
36class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
5import java.util.Collection
6import java.util.Map
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
8
9interface PolyhedronExtensionOperator {
10 def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory)
11}
12
13class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2 2
3import com.google.common.cache.Cache
4import com.google.common.cache.CacheBuilder
5import com.google.common.collect.ImmutableList 3import com.google.common.collect.ImmutableList
6import com.google.common.collect.ImmutableMap 4import com.google.common.collect.ImmutableMap
7import com.google.common.collect.ImmutableSet 5import com.google.common.collect.ImmutableSet
@@ -23,7 +21,6 @@ import java.util.HashSet
23import java.util.List 21import java.util.List
24import java.util.Map 22import java.util.Map
25import java.util.Set 23import java.util.Set
26import javax.naming.OperationNotSupportedException
27import org.eclipse.viatra.query.runtime.api.IPatternMatch 24import org.eclipse.viatra.query.runtime.api.IPatternMatch
28import org.eclipse.viatra.query.runtime.api.IQuerySpecification 25import org.eclipse.viatra.query.runtime.api.IQuerySpecification
29import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine 26import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
@@ -32,31 +29,29 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope
32import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor 29import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
33 30
34class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { 31class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import com.google.common.cache.Cache
4import com.google.common.cache.CacheBuilder
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
8import java.util.Map
9import org.eclipse.xtend.lib.annotations.Accessors
10import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
11
12@FinalFieldsConstructor
13abstract 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
49class 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
119abstract class LinearBoundedExpression { 119class 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
145abstract class LinearBoundedExpression extends Bounds {
146}
147
141@Accessors 148@Accessors
142class Dimension extends LinearBoundedExpression { 149class Dimension extends LinearBoundedExpression {
143 val String name 150 val String name
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-16 21:30:09 +0000