aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver
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.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver
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.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend1
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend201
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend102
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend3
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend8
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend112
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend137
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend68
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend8
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend99
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend205
14 files changed, 821 insertions, 136 deletions
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2 2
3import org.eclipse.viatra.dse.objectives.IGlobalConstraint 3import org.eclipse.viatra.dse.objectives.IGlobalConstraint
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
5 4
6abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { 5abstract 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.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend
new file mode 100644
index 00000000..25137eba
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend
@@ -0,0 +1,201 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
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.ModelGenerationStatistics
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator
19import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
20import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
21import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
22import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider
23import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider
24import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider
25import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker
27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver
28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjectiveProvider
29import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
30import java.util.Collection
31import java.util.List
32import java.util.Map
33import java.util.Set
34import org.eclipse.viatra.dse.objectives.IObjective
35import org.eclipse.viatra.query.runtime.api.GenericQueryGroup
36import org.eclipse.viatra.query.runtime.api.IPatternMatch
37import org.eclipse.viatra.query.runtime.api.IQuerySpecification
38import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
39import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
40import org.eclipse.viatra.query.runtime.emf.EMFScope
41import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
42import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
43import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
44import org.eclipse.xtend.lib.annotations.Data
45import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedPolyhedronScopePropagatorStrategy
46
47@Data class ModelGenerationMethod {
48 ModelGenerationStatistics statistics
49
50 Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules
51 Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules
52
53 List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities
54
55 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF
56
57 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
58
59 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions
60 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions
61
62 Map<String, ModalPatternQueries> modalRelationQueries
63
64 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
65
66 Collection<IObjective> costObjectives
67 boolean optimizationProblem
68 ViatraReasonerSolutionSaver solutionSaver
69}
70
71class ModelGenerationMethodProvider {
72 val PatternProvider patternProvider = new PatternProvider
73 val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider
74 val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider
75 val relationConstraintCalculator = new RelationConstraintCalculator
76
77 def ModelGenerationMethod createModelGenerationMethod(
78 LogicProblem logicProblem,
79 PartialInterpretation emptySolution,
80 ReasonerWorkspace workspace,
81 ViatraReasonerConfiguration config
82 ) {
83 val statistics = new ModelGenerationStatistics
84 val debugLevel = config.documentationLevel
85 val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL)
86
87 val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery).
88 map[it.patternPQuery as PQuery].toSet
89
90 val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)
91 val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,
92 workspace, config.typeInferenceMethod, config.scopePropagatorStrategy, relationConstraints, config.hints,
93 config.unitPropagationPatternGenerators, writeFiles)
94
95 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries,
96 config.calculateObjectCreationCosts)
97 val unfinishedWF = queries.getUnfinishedWFQueries.values
98 val modalRelationQueriesBuilder = ImmutableMap.builder
99 for (entry : queries.modalRelationQueries.entrySet) {
100 val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head
101 if (annotation !== null) {
102 modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value)
103 }
104 }
105 val modalRelationQueries = modalRelationQueriesBuilder.build
106 val invalidWF = queries.getInvalidWFQueries.values
107 val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
108 val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
109 val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll(
110 queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(
111 queries.mustRelationPropagationQueries.values).addAll(queries.multiplicityConstraintQueries.values.flatMap [
112 allQueries
113 ]).addAll(queries.unfinishedWFQueries.values).addAll(queries.invalidWFQueries.values).addAll(
114 queries.mustUnitPropagationPreconditionPatterns.values).addAll(
115 queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build
116 val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution))
117 GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine)
118
119 val objectiveProvider = new ThreeValuedCostObjectiveProvider(queryEngine, emptySolution, modalRelationQueries)
120 val transformedObjectives = objectiveProvider.getCostObjectives(config.costObjectives)
121
122 val solutionSaver = new ViatraReasonerSolutionSaver(transformedObjectives.leveledExtremalObjectives,
123 config.solutionScope.numberOfRequiredSolutions, DiversityChecker.of(config.diversityRequirement))
124
125 val allHints = ImmutableSet.builder
126 allHints.addAll(config.hints)
127 for (hint : transformedObjectives.hints) {
128 hint.boundsProvider = solutionSaver
129 allHints.add(hint)
130 }
131
132 val scopePropagator = createScopePropagator(config.scopePropagatorStrategy, emptySolution, allHints.build,
133 transformedObjectives.extensionOperators, queries, statistics)
134 scopePropagator.propagateAllScopeConstraints
135 val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, queries,
136 scopePropagator, statistics)
137 val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution,
138 queries, unitRulePropagator, config.nameNewElements, statistics)
139 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator,
140 statistics)
141
142 return new ModelGenerationMethod(
143 statistics,
144 objectRefinementRules.values,
145 relationRefinementRules.values,
146 unfinishedMultiplicities,
147 unfinishedWF,
148 invalidWF,
149 mustUnitPropagationPreconditions,
150 currentUnitPropagationPreconditions,
151 modalRelationQueries,
152 queries.allQueries,
153 transformedObjectives.objectives,
154 transformedObjectives.optimizationProblem,
155 solutionSaver
156 )
157 }
158
159 private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,
160 PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints,
161 Collection<PolyhedronExtensionOperator> extensionOperators, GeneratedPatterns queries,
162 ModelGenerationStatistics statistics) {
163 if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) {
164 throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.")
165 }
166 switch (scopePropagatorStrategy) {
167 case ScopePropagatorStrategy.None,
168 case ScopePropagatorStrategy.Basic:
169 new ScopePropagator(emptySolution, statistics)
170 case ScopePropagatorStrategy.BasicTypeHierarchy:
171 new TypeHierarchyScopePropagator(emptySolution, statistics)
172 ScopePropagatorStrategy.Polyhedral: {
173 val types = queries.refineObjectQueries.keySet.map[newType].toSet
174 val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName]
175 val solver = switch (scopePropagatorStrategy.solver) {
176 case Z3Integer:
177 new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds)
178 case Z3Real:
179 new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds)
180 case Cbc:
181 new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true)
182 case Clp:
183 new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true)
184 default:
185 throw new IllegalArgumentException("Unknown polyhedron solver: " +
186 scopePropagatorStrategy.solver)
187 }
188 val strategy = if (extensionOperators.empty) {
189 new CachingSimplePolyhedronScopePropagatorStrategy(solver, statistics)
190 } else {
191 new ExtendedPolyhedronScopePropagatorStrategy(solver, extensionOperators, statistics)
192 }
193 new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries,
194 queries.hasElementInContainmentQuery, allPatternsByName, hints, strategy,
195 scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic)
196 }
197 default:
198 throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy)
199 }
200 }
201}
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2 2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.Lists
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 3import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 4import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException 5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
@@ -11,7 +9,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
11import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage 9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory 10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
13import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult 11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy 12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser 13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
@@ -22,7 +19,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.sta
22import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory 19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint 20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration 21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker
26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint 22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint
27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler 23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler
28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective 24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
@@ -32,11 +28,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective
32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective 28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective
33import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint 29import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint
34import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective 30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective
35import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver
36import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter 31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter
37import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind 32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
38import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement
39import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective
40import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 33import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
41import java.util.List 34import java.util.List
42import java.util.Map 35import 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
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration 4import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod 7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint 8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints
@@ -12,6 +11,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr
12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy 11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator 12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser 13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser
14import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint
15import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind 15import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold 16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
17import java.util.LinkedList 17import 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
119class CostObjectiveElementConfiguration { 120class 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;
28import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; 28import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;
29import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; 29import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler;
30import org.eclipse.viatra.dse.solutionstore.SolutionStore; 30import org.eclipse.viatra.dse.solutionstore.SolutionStore;
31import org.eclipse.viatra.query.runtime.api.IPatternMatch;
32import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
33 31
34import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; 32import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
35import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; 33import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
@@ -37,12 +35,11 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
37import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; 35import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;
38import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; 36import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
39import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; 37import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
40import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
41import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; 38import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
42import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; 39import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
43import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder;
44import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; 40import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation;
45import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; 41import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser;
42import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod;
46import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; 43import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration;
47import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; 44import 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator 3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement 4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement 5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement 7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement 8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod
11import java.math.BigDecimal 11import java.math.BigDecimal
12import java.util.HashMap 12import java.util.HashMap
13import java.util.LinkedHashMap 13import 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
22import java.util.Map 22import java.util.Map
23import java.util.TreeSet 23import java.util.TreeSet
24import org.eclipse.emf.ecore.EObject 24import org.eclipse.emf.ecore.EObject
25import org.eclipse.xtend.lib.annotations.Accessors
25import org.eclipse.xtext.xbase.lib.Functions.Function1 26import org.eclipse.xtext.xbase.lib.Functions.Function1
26 27
27import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
28 29
29class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ 30class 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 */
28class SolutionCopier { 28class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds
4import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective
5import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider
6import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
3import java.util.HashMap 7import java.util.HashMap
4import java.util.Map 8import java.util.Map
5import org.eclipse.viatra.dse.api.DSEException 9import 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 */
21class ViatraReasonerSolutionSaver implements ISolutionSaver { 25class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
6import java.util.List
7import org.eclipse.emf.ecore.EObject
8import org.eclipse.viatra.query.runtime.api.IPatternMatch
9import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
10import org.eclipse.xtend.lib.annotations.Data
11import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
13
14@FunctionalInterface
15interface ParameterScopeBound {
16 def double getUpperBound()
17}
18
19@Data
20class CostElementMatch {
21 val IPatternMatch match
22 val boolean must
23
24 def isMulti() {
25 CostElementMatchers.isMultiMatch(match)
26 }
27}
28
29@Data
30class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilder
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
9import java.util.Map
10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
11import org.eclipse.xtend.lib.annotations.Accessors
12
13abstract 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds
4import org.eclipse.viatra.dse.objectives.IObjective
5
6interface 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2 2
3import com.google.common.collect.ImmutableList 3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener
4import java.util.Collection 4import java.util.Map
5import org.eclipse.viatra.dse.base.ThreadContext 5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.query.runtime.api.IPatternMatch 6import org.eclipse.xtend.lib.annotations.Accessors
7import org.eclipse.viatra.query.runtime.api.IQuerySpecification
8import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
9import org.eclipse.xtend.lib.annotations.Data
10 7
11@Data 8class ThreeValuedCostObjective extends AbstractThreeValuedObjective implements BoundSaturationListener {
12class 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
19class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.ImmutableMap
5import com.google.common.collect.Lists
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
14import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation
20import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
21import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation
22import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation
23import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration
26import java.util.Collection
27import java.util.Map
28import org.eclipse.viatra.dse.objectives.IObjective
29import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
30import org.eclipse.xtend.lib.annotations.Data
31
32@Data
33class 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
41class 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:27:09 +0000