play package:sbv

Play a round of the game, making the solver guess the secret number 42. Note that you can generate a random-number and make the solver guess it too! We have:

>>> play
Current bounds: (0,1000)
Current bounds: (21,1000)
Current bounds: (31,1000)
Current bounds: (36,1000)
Current bounds: (39,1000)
Current bounds: (40,1000)
Current bounds: (41,1000)
Current bounds: (42,1000)
Solved in: 8 guesses:
8 21 31 36 39 40 41 42

Given an allSat call, we typically want to iterate over it and print the results in sequence. The displayModels function automates this task by calling disp on each result, consecutively. The first Int argument to disp 'is the current model number. The second argument is a tuple, where the first element indicates whether the model is alleged (i.e., if the solver is not sure, returning Unknown). The arrange argument can sort the results in any way you like, if necessary.