from z3 import *

vegs = ["peas", "onions", "peppers", "broccoli", "potatoes", "tomatoes", "garlic"]

# dictionary mapping plant name to array of position variables
# e.g. poss["tomatoes"][2] is true iff tomatoes are planted in row 2
poss = {}
for v in vegs:
  poss[v] = [Bool(v + str(i)) for i in range(0,7)]

def not_next(v1, v2):
  c = []
  for i in range(0,7):
    neighbors = poss[v2][1] if i == 0 else poss[v2][5] if i == 6 else Or(poss[v2][i-1], poss[v2][i+1]) 
    c = c + [Implies(poss[v1][i], Not(neighbors))]
  return c

solver = Solver()
# add constraints expressing that plant is not next to enemy plants
solver.add(not_next("peppers", "onions"))
solver.add(not_next("broccoli", "onions"))
solver.add(not_next("peas", "tomatoes"))
solver.add(not_next("peas", "potatoes"))
solver.add(not_next("onions", "potatoes"))
solver.add(not_next("peppers", "potatoes"))
solver.add(not_next("tomatoes", "potatoes"))
solver.add(not_next("peppers", "garlic"))

for v in vegs:
  # at most plant per line
  for i in range(0,7):
    others = [v2 for v2 in vegs if v != v2]
    solver.add(Implies(poss[v][i], And([Not(poss[o][i]) for o in others])))
  # every plant must be somewhere
  solver.add(Or([poss[v][i] for i in range(0,7)]))

# check sat
if solver.check() == sat:
  model = solver.model()
  for v in vegs:
    for i in range(0,7):
      if model[poss[v][i]]:
        print(v + " planted at position " + str(i))