Color to number

#!/usr/bin/env ruby

require "z3"

b = Z3.Int("b")
w = Z3.Int("w")
g = Z3.Int("g")
r = Z3.Int("r")

solver = Z3::Solver.new

solver.assert b+w == g
solver.assert b*r == w
solver.assert w-r == r
solver.assert b*4 == g
solver.assert Z3.Distinct(b,w,r,g)

p solver.check
puts solver.model