; Logic puzzle solution
; Author: Bruno Wolff III
; Last updated: 2020-08-05

; You may use/modify this code for any purpose

(set-option :auto-config false)
(set-option :produce-proofs true)
(set-option :produce-models true)

; Declare possible names to set size for arrays
(declare-datatypes () ((name Filo Frank Fred Farley Febo)))

; Possible fish
(declare-datatypes () ((fish carp sailfish bluefish salmon shark)))
(declare-const fishes (Array name fish))
(assert (forall ((n1 name) (n2 name)) (=> (distinct n1 n2) (distinct (select fishes n1) (select fishes n2)))))

; Possible weights
(declare-const weights (Array name Int))
(assert (forall ((n1 name) (n2 name)) (=> (distinct n1 n2) (distinct (select weights n1) (select weights n2)))))
(assert (forall ((n name)) (or (= (select weights n) 10) (= (select weights n) 15) (= (select weights n) 25) (= (select weights n) 33) (= (select weights n) 40))))

; possible bait
(declare-datatypes () ((bait worm grub minnow lure dryfly)))
(declare-const baits (Array name bait))
(assert (forall ((n1 name) (n2 name)) (=> (distinct n1 n2) (distinct (select baits n1) (select baits n2)))))

; possible platforms
(declare-datatypes () ((platform boat raft bridge dam pier)))
(declare-const platforms (Array name platform))
(assert (forall ((n1 name) (n2 name)) (=> (distinct n1 n2) (distinct (select platforms n1) (select platforms n2)))))

; The 10 lb. fish was a carp caught on a worm.
(assert (forall ((n name)) (=> (= (select weights n) 10) (and (= (select fishes n) carp) (= (select baits n) worm)))))

; The combined weight of Frank and Febo's fishes equaled Filo's bluefish.
(assert (and (= (+ (select weights Frank) (select weights Febo)) (select weights Filo)) (= (select fishes Filo) bluefish)))

; Febo didn't catch a carp and he didn't use grubs or lures.
(assert (and (not (= (select fishes Febo) carp)) (not (= (select baits Febo) grub)) (not (= (select baits Febo) lure))))

; Farley's shark wasn't the biggest fish and it wasn't caught on a grub or a dry fly or from a pier.
(assert (and (= (select fishes Farley) shark) (< (select weights Farley) 40) (not (= (select baits Farley) grub)) (not (= (select baits Farley) dryfly)) (not (= (select platforms Farley) pier))))

; The sailfish was caught on a minnow from a boat.
(assert (forall ((n name)) (=> (= (select fishes n) sailfish) (and (= (select baits n) minnow) (= (select platforms n) boat)))))

; The salmon was caught on a grub from a dam.
(assert (forall ((n name)) (=> (= (select fishes n) salmon) (and (= (select baits n) grub) (= (select platforms n) dam)))))

; Febo didn't catch a salmon and the 25 lb. fish was not caught from a raft.
(assert (and (not (= (select fishes Febo) salmon)) (forall ((n name)) (=> (= (select weights n) 25) (not (= (select platforms n) raft))))))

; The dry fly was not used from a pier.
(assert (forall ((n name)) (=> (= (select baits n) dryfly) (not (= (select platforms n) pier)))))

(echo "")
(echo "Solution 1")
(echo "")
(check-sat)
(echo "")
(eval Filo)
(eval (select fishes Filo))
(eval (select weights Filo))
(eval (select baits Filo))
(eval (select platforms Filo))
(echo "")
(eval Frank)
(eval (select fishes Frank))
(eval (select weights Frank))
(eval (select baits Frank))
(eval (select platforms Frank))
(echo "")
(eval Fred)
(eval (select fishes Fred))
(eval (select weights Fred))
(eval (select baits Fred))
(eval (select platforms Fred))
(echo "")
(eval Farley)
(eval (select fishes Farley))
(eval (select weights Farley))
(eval (select baits Farley))
(eval (select platforms Farley))
(echo "")
(eval Febo)
(eval (select fishes Febo))
(eval (select weights Febo))
(eval (select baits Febo))
(eval (select platforms Febo))
(echo "")

; Unfortunately z3 doesn't provide a way to extract a model and use it while reading smt-lib formatted input. So to check for other solutions requires and constraints and running again until there aren't any more.

(assert-not (and
  (= (select fishes Filo) bluefish)
  (= (select weights Filo) 40)
  (= (select baits Filo) dryfly)
  (= (select platforms Filo) bridge)
  (= (select fishes Frank) salmon)
  (= (select weights Frank) 15)
  (= (select baits Frank) grub)
  (= (select platforms Frank) dam)
  (= (select fishes Fred) carp)
  (= (select weights Fred) 10)
  (= (select baits Fred) worm)
  (= (select platforms Fred) pier)
  (= (select fishes Farley) shark)
  (= (select weights Farley) 33)
  (= (select baits Farley) lure)
  (= (select platforms Farley) raft)
  (= (select fishes Febo) sailfish)
  (= (select weights Febo) 25)
  (= (select baits Febo) minnow)
  (= (select platforms Febo) boat)
))

(echo "Solution 2")
(echo "")
(check-sat)
(echo "")
(eval Filo)
(eval (select fishes Filo))
(eval (select weights Filo))
(eval (select baits Filo))
(eval (select platforms Filo))
(echo "")
(eval Frank)
(eval (select fishes Frank))
(eval (select weights Frank))
(eval (select baits Frank))
(eval (select platforms Frank))
(echo "")
(eval Fred)
(eval (select fishes Fred))
(eval (select weights Fred))
(eval (select baits Fred))
(eval (select platforms Fred))
(echo "")
(eval Farley)
(eval (select fishes Farley))
(eval (select weights Farley))
(eval (select baits Farley))
(eval (select platforms Farley))
(echo "")
(eval Febo)
(eval (select fishes Febo))
(eval (select weights Febo))
(eval (select baits Febo))
(eval (select platforms Febo))
(echo "")

(assert-not (and
  (= (select fishes Filo) bluefish)
  (= (select weights Filo) 40)
  (= (select baits Filo) dryfly)
  (= (select platforms Filo) raft)
  (= (select fishes Frank) salmon)
  (= (select weights Frank) 15)
  (= (select baits Frank) grub)
  (= (select platforms Frank) dam)
  (= (select fishes Fred) carp)
  (= (select weights Fred) 10)
  (= (select baits Fred) worm)
  (= (select platforms Fred) pier)
  (= (select fishes Farley) shark)
  (= (select weights Farley) 33)
  (= (select baits Farley) lure)
  (= (select platforms Farley) bridge)
  (= (select fishes Febo) sailfish)
  (= (select weights Febo) 25)
  (= (select baits Febo) minnow)
  (= (select platforms Febo) boat)
))

(echo "Solution 3")
(echo "")
(check-sat)
(echo "")
(eval Filo)
(eval (select fishes Filo))
(eval (select weights Filo))
(eval (select baits Filo))
(eval (select platforms Filo))
(echo "")
(eval Frank)
(eval (select fishes Frank))
(eval (select weights Frank))
(eval (select baits Frank))
(eval (select platforms Frank))
(echo "")
(eval Fred)
(eval (select fishes Fred))
(eval (select weights Fred))
(eval (select baits Fred))
(eval (select platforms Fred))
(echo "")
(eval Farley)
(eval (select fishes Farley))
(eval (select weights Farley))
(eval (select baits Farley))
(eval (select platforms Farley))
(echo "")
(eval Febo)
(eval (select fishes Febo))
(eval (select weights Febo))
(eval (select baits Febo))
(eval (select platforms Febo))
(echo "")

(assert-not (and
  (= (select fishes Filo) bluefish)
  (= (select weights Filo) 40)
  (= (select baits Filo) dryfly)
  (= (select platforms Filo) raft)
  (= (select fishes Frank) salmon)
  (= (select weights Frank) 25)
  (= (select baits Frank) grub)
  (= (select platforms Frank) dam)
  (= (select fishes Fred) carp)
  (= (select weights Fred) 10)
  (= (select baits Fred) worm)
  (= (select platforms Fred) pier)
  (= (select fishes Farley) shark)
  (= (select weights Farley) 33)
  (= (select baits Farley) lure)
  (= (select platforms Farley) bridge)
  (= (select fishes Febo) sailfish)
  (= (select weights Febo) 15)
  (= (select baits Febo) minnow)
  (= (select platforms Febo) boat)
))

(echo "Solution 4")
(echo "")
(check-sat)
(echo "")
(eval Filo)
(eval (select fishes Filo))
(eval (select weights Filo))
(eval (select baits Filo))
(eval (select platforms Filo))
(echo "")
(eval Frank)
(eval (select fishes Frank))
(eval (select weights Frank))
(eval (select baits Frank))
(eval (select platforms Frank))
(echo "")
(eval Fred)
(eval (select fishes Fred))
(eval (select weights Fred))
(eval (select baits Fred))
(eval (select platforms Fred))
(echo "")
(eval Farley)
(eval (select fishes Farley))
(eval (select weights Farley))
(eval (select baits Farley))
(eval (select platforms Farley))
(echo "")
(eval Febo)
(eval (select fishes Febo))
(eval (select weights Febo))
(eval (select baits Febo))
(eval (select platforms Febo))
(echo "")

(assert-not (and
  (= (select fishes Filo) bluefish)
  (= (select weights Filo) 40)
  (= (select baits Filo) dryfly)
  (= (select platforms Filo) bridge)
  (= (select fishes Frank) salmon)
  (= (select weights Frank) 25)
  (= (select baits Frank) grub)
  (= (select platforms Frank) dam)
  (= (select fishes Fred) carp)
  (= (select weights Fred) 10)
  (= (select baits Fred) worm)
  (= (select platforms Fred) pier)
  (= (select fishes Farley) shark)
  (= (select weights Farley) 33)
  (= (select baits Farley) lure)
  (= (select platforms Farley) raft)
  (= (select fishes Febo) sailfish)
  (= (select weights Febo) 15)
  (= (select baits Febo) minnow)
  (= (select platforms Febo) boat)
))

(echo "Solution 5")
(echo "")
(check-sat)
(echo "")
(eval Filo)
(eval (select fishes Filo))
(eval (select weights Filo))
(eval (select baits Filo))
(eval (select platforms Filo))
(echo "")
(eval Frank)
(eval (select fishes Frank))
(eval (select weights Frank))
(eval (select baits Frank))
(eval (select platforms Frank))
(echo "")
(eval Fred)
(eval (select fishes Fred))
(eval (select weights Fred))
(eval (select baits Fred))
(eval (select platforms Fred))
(echo "")
(eval Farley)
(eval (select fishes Farley))
(eval (select weights Farley))
(eval (select baits Farley))
(eval (select platforms Farley))
(echo "")
(eval Febo)
(eval (select fishes Febo))
(eval (select weights Febo))
(eval (select baits Febo))
(eval (select platforms Febo))
(echo "")

(assert-not (and
  (= (select fishes Filo) bluefish)
  (= (select weights Filo) 25)
  (= (select baits Filo) dryfly)
  (= (select platforms Filo) bridge)
  (= (select fishes Frank) carp)
  (= (select weights Frank) 10)
  (= (select baits Frank) worm)
  (= (select platforms Frank) pier)
  (= (select fishes Fred) salmon)
  (= (select weights Fred) 40)
  (= (select baits Fred) grub)
  (= (select platforms Fred) dam)
  (= (select fishes Farley) shark)
  (= (select weights Farley) 33)
  (= (select baits Farley) lure)
  (= (select platforms Farley) raft)
  (= (select fishes Febo) sailfish)
  (= (select weights Febo) 15)
  (= (select baits Febo) minnow)
  (= (select platforms Febo) boat)
))

(echo "Solution 6")
(echo "")
(check-sat)
(echo "")

(exit)