11/// This file implements the driver loop which attempts Knuth-Bendix completion
22/// with various strategies on all instances in parallel.
33
4+ let numTasks = 32
5+
46struct Dispatcher {
57 let subset : [ Int ]
68 let strategies : [ Strategy ]
@@ -48,7 +50,7 @@ struct Solver {
4850 mutating func solve( ) async {
4951 if output {
5052 print ( " # Remaining \( subset. count) " )
51- print ( " # n: \t presentation: \t cardinality: \t complete presentation : \t strategy: " )
53+ print ( " # n: \t presentation: \t cardinality: \t complete: \t strategy: " )
5254 }
5355
5456 // The shortlex order with identity permutation of generators solves
@@ -173,9 +175,8 @@ struct Solver {
173175 mutating func attempt( _ strategies: [ Strategy ] ) async {
174176 if subset. isEmpty { return }
175177
176- let solved = await withTaskGroup ( of: ( Int, Int, Solution? ) . self) { group in
177- var dispatcher = Dispatcher ( subset: subset,
178- strategies: strategies)
178+ await withTaskGroup ( of: ( Int, Int, Solution? ) . self) { group in
179+ var dispatcher = Dispatcher ( subset: subset, strategies: strategies)
179180 var solved : [ Int : ( Int , Solution ) ] = [ : ]
180181 var pending : [ Int : Int ] = [ : ]
181182
@@ -216,6 +217,7 @@ struct Solver {
216217 // The lowest-numbered strategy is the 'official' solution for the instance.
217218 var betterStrategy = true
218219 if let ( oldStrategyIndex, _) = solved [ instance] {
220+ precondition ( oldStrategyIndex != strategyIndex)
219221 if oldStrategyIndex < strategyIndex {
220222 betterStrategy = false
221223 }
@@ -226,67 +228,64 @@ struct Solver {
226228 }
227229 }
228230
229- retireStrategies ( )
231+ while retireStrategy ( ) { }
230232 }
231233
232- func retireStrategies( ) {
233- var retired : [ Int : [ Int ] ] = [ : ]
234- let pendingInOrder = pending. sorted { $0. key < $1. key }
235- for (strategyIndex, numTasks) in pendingInOrder {
236- precondition ( strategyIndex <= dispatcher. currentStrategy)
237- if dispatcher. currentStrategy == strategyIndex { break }
238- if numTasks > 0 { break }
234+ func retireStrategy( ) -> Bool {
235+ // Check if nothing remains.
236+ guard let minPending = pending. keys. min ( ) else { return false }
239237
240- pending [ strategyIndex ] = nil
241- retired [ strategyIndex ] = [ ]
242- }
238+ // Check if we're going to dispatch more instances with this strategy.
239+ precondition ( minPending <= dispatcher . currentStrategy )
240+ if minPending == dispatcher . currentStrategy { return false }
243241
244- if retired. isEmpty { return }
245-
246- // If we are done dispatching a strategy, look at all instances solved
247- // by that strategy and print them out.
248- for n in subset {
249- if let ( strategyIndex, solution) = solved [ n] {
250- if retired [ strategyIndex] != nil {
251- retired [ strategyIndex] !. append ( n)
252-
253- // Print the instance and solution.
254- var str = " \( n + 1 ) \t \( instances [ n] ) \t "
255-
256- if let cardinality = solution. cardinality {
257- str += " finite: \( cardinality) "
258- finite [ cardinality, default: 0 ] += 1
259- } else {
260- str += " infinite "
261- }
262- str += " \t fcrs: \( solution. presentation) "
263-
264- // Print the extra generators that were added, if any.
265- if !solution. extra. isEmpty {
266- str += " \t \( printRules ( solution. extra) ) "
267- }
268-
269- if output {
270- print ( str)
271- }
272- }
242+ // Check if we're still waiting for instances to finish with this
243+ // strategy.
244+ if pending [ minPending] ! > 0 { return false }
245+
246+ // Otherwise, retire this strategy.
247+ pending [ minPending] = nil
248+
249+ // Print out all instances solved by this strategy and remove them
250+ // from the list.
251+ subset = subset. filter { n in
252+ guard let ( strategyIndex, solution) = solved [ n] else { return true }
253+ guard strategyIndex == minPending else { return true }
254+
255+ // Print the instance and solution.
256+ var str = " \( n + 1 ) \t \( instances [ n] ) \t "
257+
258+ if let cardinality = solution. cardinality {
259+ str += " finite: \( cardinality) "
260+ finite [ cardinality, default: 0 ] += 1
261+ } else {
262+ str += " infinite "
273263 }
264+ str += " \t fcrs: \( solution. presentation) "
265+
266+ // Print the extra generators that were added, if any.
267+ if !solution. extra. isEmpty {
268+ str += " \t \( printRules ( solution. extra) ) "
269+ }
270+
271+ if output {
272+ print ( str)
273+ }
274+
275+ return false
274276 }
277+
278+ return true
275279 }
276280
277- // We run 32 tasks at a time.
278- for _ in 0 ..< 32 {
281+ for _ in 0 ..< numTasks {
279282 startTask ( )
280283 }
281284
282285 for await (instance, strategyIndex, solution) in group {
283286 startTask ( )
284287 completeTask ( instance, strategyIndex, solution)
285288 }
286-
287- return solved
288289 }
289-
290- subset = subset. filter { solved [ $0] == nil }
291290 }
292291}
0 commit comments