(set-logic ALL)
;fox, goose, beans, human
; forward reachability: one copy of the state (fl ... br) and, inside the image,
; a bound copy for the previous state (flp ... brp). No per-move variables.

; initial setup: as in river-full.smt2, plus consistency, so that Init is exactly
; 'everything on the left' (river-full.smt2 leaves fb, fr, ... unconstrained in move 0)
(define-fun Init ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (and fl gl bl
       (xor fl fb fr) (xor gl gb gr) (xor bl bb br)
       (not (and fl fb fr)) (not (and gl gb gr)) (not (and bl bb br))))

; consistency, boat capacity and prevention of carnage (as in river-full.smt2)
; (move 0 of river-full.smt2 has none of these; see Init)
(define-fun Legal ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (and (xor fl fb fr) (xor gl gb gr) (xor bl bb br)
       (not (and bl bb br)) (not (and fl fb fr)) (not (and gl gb gr))
       (=> fb (and (not gb) (not bb)))
       (=> gb (and (not fb) (not bb)))
       (=> bb (and (not gb) (not fb)))
       (not (and fl gl))
       (not (and gl bl))
       (or (and fr gr br)
           (and (not (and fr gr)) (not (and gr br))))))

; possible moves from the previous state (suffix p) to the current one
(define-fun Step ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool) (fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (and (Legal fl fb fr gl gb gr bl bb br)
       (=> flp (or fl fb))
       (=> fbp (or fb fl fr))
       (=> frp (or fr fb))
       (=> glp (or gl gb))
       (=> gbp (or gb gl gr))
       (=> grp (or gr gb))
       (=> blp (or bl bb))
       (=> bbp (or bb bl br))
       (=> brp (or br bb))
  ))

(define-fun Goal ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (and fr gr br))

; R_0 = Init,  R_{j+1}(v) = R_j(v) or exists p. R_j(p) and Step(p, v)
(define-fun R0 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool (Init fl fb fr gl gb gr bl bb br))
(define-fun R1 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (or (R0 fl fb fr gl gb gr bl bb br)
      (exists ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool))
        (and (R0 flp fbp frp glp gbp grp blp bbp brp) (Step flp fbp frp glp gbp grp blp bbp brp fl fb fr gl gb gr bl bb br)))))
(define-fun R2 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (or (R1 fl fb fr gl gb gr bl bb br)
      (exists ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool))
        (and (R1 flp fbp frp glp gbp grp blp bbp brp) (Step flp fbp frp glp gbp grp blp bbp brp fl fb fr gl gb gr bl bb br)))))
(define-fun R3 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (or (R2 fl fb fr gl gb gr bl bb br)
      (exists ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool))
        (and (R2 flp fbp frp glp gbp grp blp bbp brp) (Step flp fbp frp glp gbp grp blp bbp brp fl fb fr gl gb gr bl bb br)))))
(define-fun R4 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (or (R3 fl fb fr gl gb gr bl bb br)
      (exists ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool))
        (and (R3 flp fbp frp glp gbp grp blp bbp brp) (Step flp fbp frp glp gbp grp blp bbp brp fl fb fr gl gb gr bl bb br)))))
(define-fun R5 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (or (R4 fl fb fr gl gb gr bl bb br)
      (exists ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool))
        (and (R4 flp fbp frp glp gbp grp blp bbp brp) (Step flp fbp frp glp gbp grp blp bbp brp fl fb fr gl gb gr bl bb br)))))
(define-fun R6 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (or (R5 fl fb fr gl gb gr bl bb br)
      (exists ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool))
        (and (R5 flp fbp frp glp gbp grp blp bbp brp) (Step flp fbp frp glp gbp grp blp bbp brp fl fb fr gl gb gr bl bb br)))))
(define-fun R7 ((fl Bool) (fb Bool) (fr Bool) (gl Bool) (gb Bool) (gr Bool) (bl Bool) (bb Bool) (br Bool)) Bool
  (or (R6 fl fb fr gl gb gr bl bb br)
      (exists ((flp Bool) (fbp Bool) (frp Bool) (glp Bool) (gbp Bool) (grp Bool) (blp Bool) (bbp Bool) (brp Bool))
        (and (R6 flp fbp frp glp gbp grp blp bbp brp) (Step flp fbp frp glp gbp grp blp bbp brp fl fb fr gl gb gr bl bb br)))))

; the one copy of the state
(declare-const fl Bool)
(declare-const fb Bool)
(declare-const fr Bool)
(declare-const gl Bool)
(declare-const gb Bool)
(declare-const gr Bool)
(declare-const bl Bool)
(declare-const bb Bool)
(declare-const br Bool)

(echo "R0 and Goal (sat = goal reachable within 0 moves):")
(push 1) (assert (and (R0 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)
(echo "R1 and not R0 (unsat = fixed point, nothing new):")
(push 1) (assert (and (R1 fl fb fr gl gb gr bl bb br) (not (R0 fl fb fr gl gb gr bl bb br)))) (check-sat) (pop 1)
(echo "R1 and Goal (sat = goal reachable within 1 moves):")
(push 1) (assert (and (R1 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)
(echo "R2 and not R1 (unsat = fixed point, nothing new):")
(push 1) (assert (and (R2 fl fb fr gl gb gr bl bb br) (not (R1 fl fb fr gl gb gr bl bb br)))) (check-sat) (pop 1)
(echo "R2 and Goal (sat = goal reachable within 2 moves):")
(push 1) (assert (and (R2 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)
(echo "R3 and not R2 (unsat = fixed point, nothing new):")
(push 1) (assert (and (R3 fl fb fr gl gb gr bl bb br) (not (R2 fl fb fr gl gb gr bl bb br)))) (check-sat) (pop 1)
(echo "R3 and Goal (sat = goal reachable within 3 moves):")
(push 1) (assert (and (R3 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)
(echo "R4 and not R3 (unsat = fixed point, nothing new):")
(push 1) (assert (and (R4 fl fb fr gl gb gr bl bb br) (not (R3 fl fb fr gl gb gr bl bb br)))) (check-sat) (pop 1)
(echo "R4 and Goal (sat = goal reachable within 4 moves):")
(push 1) (assert (and (R4 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)
(echo "R5 and not R4 (unsat = fixed point, nothing new):")
(push 1) (assert (and (R5 fl fb fr gl gb gr bl bb br) (not (R4 fl fb fr gl gb gr bl bb br)))) (check-sat) (pop 1)
(echo "R5 and Goal (sat = goal reachable within 5 moves):")
(push 1) (assert (and (R5 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)
(echo "R6 and not R5 (unsat = fixed point, nothing new):")
(push 1) (assert (and (R6 fl fb fr gl gb gr bl bb br) (not (R5 fl fb fr gl gb gr bl bb br)))) (check-sat) (pop 1)
(echo "R6 and Goal (sat = goal reachable within 6 moves):")
(push 1) (assert (and (R6 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)
(echo "R7 and not R6 (unsat = fixed point, nothing new):")
(push 1) (assert (and (R7 fl fb fr gl gb gr bl bb br) (not (R6 fl fb fr gl gb gr bl bb br)))) (check-sat) (pop 1)
(echo "R7 and Goal (sat = goal reachable within 7 moves):")
(push 1) (assert (and (R7 fl fb fr gl gb gr bl bb br) (Goal fl fb fr gl gb gr bl bb br))) (check-sat) (pop 1)