silly_giraffe

Using the Python bindings, the biggest performance impact I discovered was ensuring that my jobs and tasks were represented as z3.Bool and not z3.Int (requiring a roundabout way to do a summation on z3.Bools). Something like:

  tasks_this_tick = [(z3.Bool(task_id), 1) for task_id in current_tasks]
  model.add(z3.PbLe(tasks_this_tick, max_tasks_per_tick + 1)

Those have different use cases. `sorted` is for situations where you would use a list comprehension and immediately consume the result vs `.sort` where you need the iterable sorted for future use.

As a quick scribble, you can do something like the following to sort random numbers in a single line:

  result = sorted(random.random() for x in range(10))

  def list_sort(arr):
    return arr.sort()

  def sorted_builtin(arr):
    return sorted(arr)

  def list_sort(arr):
    arr.sort()
    return arr

Thanks for making this resource available and giving it some exposure.