basic_logical_error.py

"""
A basic logical error in Z3/python code.

In order to enumerate all valid solutions, a solution is added as a constraint that should not be
matched.

Two ways of writing; which is correct (bug present in code on stackoverflow...)
"""
  def not_again(self, model) -> None:
      """Exclude a current solution from the future results."""
      block = []
      for d in model:
          c = d()
          block.append(c != model[d])

      self.optimize.add(And(*block, self.context))

# Versus
  def not_again(self, model) -> None:
      """Exclude a current solution from the future results."""
      block = []
      for d in model:
          c = d()
          block.append(c == model[d])

      self.optimize.add(Not(And(*block, self.context)))

      
      
      
      
 """
 One of these is too strict and would remove all solutions that have *an*
 identical *assignment* to the model being blocked. Instead, only solutions
 that have *all* assignments identical to the model should be blocked.
 """