diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
commit | c3a6d4b9cf3657070d180aa65ddbf0459e880329 (patch) | |
tree | 780c4fc61578dcb309af53fb0c164c7627e51676 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend | |
parent | New configuration language parser WIP (diff) | |
parent | Scope unsat benchmarks (diff) | |
download | VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.gz VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.zst VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.zip |
Merge branch 'kris'
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend | 184 |
1 files changed, 184 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend new file mode 100644 index 00000000..fb1b2066 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend | |||
@@ -0,0 +1,184 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import com.google.common.collect.HashMultiset | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import com.google.common.collect.Multiset | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
11 | import java.util.Collection | ||
12 | import java.util.HashSet | ||
13 | import java.util.Map | ||
14 | import java.util.Set | ||
15 | import org.eclipse.viatra.dse.base.ThreadContext | ||
16 | import org.eclipse.xtend.lib.annotations.Accessors | ||
17 | |||
18 | interface DiversityChecker { | ||
19 | public static val NO_DIVERSITY_CHECKER = new DiversityChecker { | ||
20 | override isActive() { | ||
21 | false | ||
22 | } | ||
23 | |||
24 | override getTotalRuntime() { | ||
25 | 0 | ||
26 | } | ||
27 | |||
28 | override getSuccessRate() { | ||
29 | 1.0 | ||
30 | } | ||
31 | |||
32 | override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
33 | true | ||
34 | } | ||
35 | } | ||
36 | |||
37 | def boolean isActive() | ||
38 | |||
39 | def long getTotalRuntime() | ||
40 | |||
41 | def double getSuccessRate() | ||
42 | |||
43 | def boolean newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) | ||
44 | |||
45 | static def of(DiversityDescriptor descriptor) { | ||
46 | if (descriptor.ensureDiversity) { | ||
47 | new NodewiseDiversityChecker(descriptor) | ||
48 | } else { | ||
49 | NO_DIVERSITY_CHECKER | ||
50 | } | ||
51 | } | ||
52 | } | ||
53 | |||
54 | abstract class AbstractDiversityChecker implements DiversityChecker { | ||
55 | val DiversityDescriptor descriptor | ||
56 | val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice | ||
57 | |||
58 | @Accessors(PUBLIC_GETTER) var long totalRuntime = 0 | ||
59 | var int allCheckCount = 0 | ||
60 | var int successfulCheckCount = 0 | ||
61 | |||
62 | protected new(DiversityDescriptor descriptor) { | ||
63 | if (!descriptor.ensureDiversity) { | ||
64 | throw new IllegalArgumentException( | ||
65 | "Diversity description should enforce diversity or NO_DIVERSITY_CHECKER should be used instead.") | ||
66 | } | ||
67 | this.descriptor = descriptor | ||
68 | } | ||
69 | |||
70 | override isActive() { | ||
71 | true | ||
72 | } | ||
73 | |||
74 | override getTotalRuntime() { | ||
75 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
76 | } | ||
77 | |||
78 | override getSuccessRate() { | ||
79 | (allCheckCount as double) / (successfulCheckCount as double) | ||
80 | } | ||
81 | |||
82 | override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
83 | val start = System.nanoTime | ||
84 | val model = threadContext.model as PartialInterpretation | ||
85 | val representation = solutionCoder.createRepresentation(model, descriptor.range, descriptor.parallels, | ||
86 | descriptor.maxNumber, descriptor.relevantTypes, descriptor.relevantRelations) | ||
87 | val isDifferent = internalNewSolution(representation, solutionId, dominatedSolutionIds) | ||
88 | totalRuntime += System.nanoTime - start | ||
89 | allCheckCount++ | ||
90 | if (isDifferent) { | ||
91 | successfulCheckCount++ | ||
92 | } | ||
93 | isDifferent | ||
94 | } | ||
95 | |||
96 | protected abstract def boolean internalNewSolution( | ||
97 | NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation, | ||
98 | Object solutionId, Collection<Object> dominatedSolutionIds) | ||
99 | } | ||
100 | |||
101 | class NodewiseDiversityChecker extends AbstractDiversityChecker { | ||
102 | var Multiset<Integer> nodeCodes = HashMultiset.create | ||
103 | val Map<Object, Set<Integer>> tracedNodeCodes = newHashMap | ||
104 | |||
105 | new(DiversityDescriptor descriptor) { | ||
106 | super(descriptor) | ||
107 | } | ||
108 | |||
109 | override protected internalNewSolution( | ||
110 | NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation, | ||
111 | Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
112 | val nodeCodesInSolution = ImmutableSet.copyOf(representation.modelRepresentation.keySet.map[hashCode]) | ||
113 | val remainingNodeCodes = if (dominatedSolutionIds.empty) { | ||
114 | nodeCodes | ||
115 | } else { | ||
116 | getRemainingNodeCodes(dominatedSolutionIds) | ||
117 | } | ||
118 | val hasNewCode = nodeCodesInSolution.exists[!remainingNodeCodes.contains(it)] | ||
119 | if (hasNewCode) { | ||
120 | nodeCodes = remainingNodeCodes | ||
121 | nodeCodes.addAll(nodeCodesInSolution) | ||
122 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
123 | tracedNodeCodes.remove(dominatedSolutionId) | ||
124 | } | ||
125 | tracedNodeCodes.put(solutionId, nodeCodesInSolution) | ||
126 | } | ||
127 | hasNewCode | ||
128 | } | ||
129 | |||
130 | private def getRemainingNodeCodes(Collection<Object> dominatedSolutionIds) { | ||
131 | // TODO Optimize multiset operations. | ||
132 | val copyOfNodeCodes = HashMultiset.create(nodeCodes) | ||
133 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
134 | val dominatedModelCode = tracedNodeCodes.get(dominatedSolutionId) | ||
135 | if (dominatedModelCode === null) { | ||
136 | throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId) | ||
137 | } | ||
138 | copyOfNodeCodes.removeAll(dominatedModelCode) | ||
139 | } | ||
140 | copyOfNodeCodes | ||
141 | } | ||
142 | } | ||
143 | |||
144 | class GraphwiseDiversityChecker extends AbstractDiversityChecker { | ||
145 | var Set<Integer> modelCodes = newHashSet | ||
146 | val Map<Object, Integer> tracedModelCodes = newHashMap | ||
147 | |||
148 | new(DiversityDescriptor descriptor) { | ||
149 | super(descriptor) | ||
150 | } | ||
151 | |||
152 | override protected internalNewSolution( | ||
153 | NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation, | ||
154 | Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
155 | val modelCodeOfSolution = representation.modelRepresentation.hashCode | ||
156 | val remainingModelCodes = if (dominatedSolutionIds.empty) { | ||
157 | modelCodes | ||
158 | } else { | ||
159 | getRemainingModelCodes(dominatedSolutionIds) | ||
160 | } | ||
161 | val isNewCode = !remainingModelCodes.contains(modelCodeOfSolution) | ||
162 | if (isNewCode) { | ||
163 | modelCodes = remainingModelCodes | ||
164 | modelCodes += modelCodeOfSolution | ||
165 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
166 | tracedModelCodes.remove(dominatedSolutionId) | ||
167 | } | ||
168 | tracedModelCodes.put(solutionId, modelCodeOfSolution) | ||
169 | } | ||
170 | isNewCode | ||
171 | } | ||
172 | |||
173 | private def getRemainingModelCodes(Collection<Object> dominatedSolutionIds) { | ||
174 | val copyOfModelCodes = new HashSet(modelCodes) | ||
175 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
176 | val dominatedModelCode = tracedModelCodes.get(dominatedSolutionId) | ||
177 | if (dominatedModelCode === null) { | ||
178 | throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId) | ||
179 | } | ||
180 | copyOfModelCodes -= dominatedModelCode | ||
181 | } | ||
182 | copyOfModelCodes | ||
183 | } | ||
184 | } | ||