pizza_puzzle.smt2

; Rachel's Pizza Ordering Puzzle
;
; Rachel is ordering pizza for seven people. She spilled coffee on her
; list but can reconstruct it from what she remembers about preferences.
; The coffee-stained list shows the 7 pizzas ordered and a visible "N"
; (end of a name) next to Sausage.

(set-logic QF_DT)

; --- Pizza types (from the coffee-stained list) ---
(declare-datatypes ((Pizza 0)) ((
  (Cheese) (Pepperoni) (Margherita) (Hawaiian) (BBQChicken) (PeppersOnions) (Sausage)
)))

; --- Each person's order ---
(declare-const rachel  Pizza)
(declare-const emily   Pizza)
(declare-const owen    Pizza)
(declare-const yasmine Pizza)
(declare-const nathan  Pizza)
(declare-const wendy   Pizza)
(declare-const kevin   Pizza)

; --- Pizza properties ---

(define-fun is-vegetarian ((p Pizza)) Bool
  (or (= p Cheese) (= p Margherita) (= p PeppersOnions)))

(define-fun has-meat ((p Pizza)) Bool
  (or (= p Pepperoni) (= p Hawaiian) (= p BBQChicken) (= p Sausage)))

(define-fun has-onions ((p Pizza)) Bool
  (= p PeppersOnions))

(define-fun has-pineapple ((p Pizza)) Bool
  (= p Hawaiian))

(define-fun is-classic ((p Pizza)) Bool
  (or (= p Cheese) (= p Pepperoni) (= p Margherita)))

; --- Constraints ---

; Everyone orders something different (7 people, 7 pizzas)
(assert (distinct rachel emily owen yasmine nathan wendy kevin))

; Emily and Owen are vegetarians
(assert (is-vegetarian emily))
(assert (is-vegetarian owen))

; Yasmine thinks plain Cheese is boring
(assert (not (= yasmine Cheese)))

; Nathan likes the classics: Cheese, Pepperoni, or Margherita
(assert (is-classic nathan))

; Emily hates onions
(assert (not (has-onions emily)))

; Wendy doesn't believe pineapple belongs on a pizza
(assert (not (has-pineapple wendy)))

; Rachel ordered Cheese
(assert (= rachel Cheese))

; Kevin always wants a pizza with meat on it
(assert (has-meat kevin))

; Visible "N" next to Sausage: the orderer's name ends in N
; (Nathan, Owen, or Kevin)
(assert (or (= nathan Sausage) (= owen Sausage) (= kevin Sausage)))

(check-sat)
(get-model)

sat
(
  (define-fun yasmine () Pizza
    Hawaiian)
  (define-fun owen () Pizza
    PeppersOnions)
  (define-fun emily () Pizza
    Margherita)
  (define-fun kevin () Pizza
    Sausage)
  (define-fun wendy () Pizza
    BBQChicken)
  (define-fun nathan () Pizza
    Pepperoni)
  (define-fun rachel () Pizza
    Cheese)
)