; Logic puzzle - Get next solution
; Author: Bruno Wolff III
; Last updated: 2020-08-10

; You may use/modify this code for any purpose

(set-option :auto-config false)
(set-option :produce-proofs true)
(set-option :produce-models true)
(set-option :produce-assertions 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))

; Possible weights
(declare-const weights (Array name Int))

; possible bait
(declare-datatypes () ((bait worm grub minnow lure dryfly)))
(declare-const baits (Array name bait))

; possible platforms
(declare-datatypes () ((platform boat raft bridge dam pier)))
(declare-const platforms (Array name platform))

; Import asserts with negations of previous solutions

(include "puzzle41.assert")

; Comment out check-sat reply.

(echo "(set-info :status")
(check-sat)
(echo ")")

; The assertion list will need to be fixed up to use in an and condition.

(echo "(assert (and")
(get-assertions)
(echo ")")

(echo "(assert (not (and")
(echo "(= (select fishes Filo)")
(eval (select fishes Filo))
(echo ")")
(echo "(= (select weights Filo)")
(eval (select weights Filo))
(echo ")")
(echo "(= (select baits Filo)")
(eval (select baits Filo))
(echo ")")
(echo "(= (select platforms Filo)")
(eval (select platforms Filo))
(echo ")")
(echo "(= (select fishes Frank)")
(eval (select fishes Frank))
(echo ")")
(echo "(= (select weights Frank)")
(eval (select weights Frank))
(echo ")")
(echo "(= (select baits Frank)")
(eval (select baits Frank))
(echo ")")
(echo "(= (select platforms Frank)")
(eval (select platforms Frank))
(echo ")")
(echo "(= (select fishes Fred)")
(eval (select fishes Fred))
(echo ")")
(echo "(= (select weights Fred)")
(eval (select weights Fred))
(echo ")")
(echo "(= (select baits Fred)")
(eval (select baits Fred))
(echo ")")
(echo "(= (select platforms Fred)")
(eval (select platforms Fred))
(echo ")")
(echo "(= (select fishes Farley)")
(eval (select fishes Farley))
(echo ")")
(echo "(= (select weights Farley)")
(eval (select weights Farley))
(echo ")")
(echo "(= (select baits Farley)")
(eval (select baits Farley))
(echo ")")
(echo "(= (select platforms Farley)")
(eval (select platforms Farley))
(echo ")")
(echo "(= (select fishes Febo)")
(eval (select fishes Febo))
(echo ")")
(echo "(= (select weights Febo)")
(eval (select weights Febo))
(echo ")")
(echo "(= (select baits Febo)")
(eval (select baits Febo))
(echo ")")
(echo "(= (select platforms Febo)")
(eval (select platforms Febo))
(echo ")")
(echo ")))")
(exit)