; Copyright 2017 Google Inc.
;
; Licensed under the Apache License, Version 2.0 (the "License");
; you may not use this file except in compliance with the License.
; You may obtain a copy of the License at
;
;     https://www.apache.org/licenses/LICENSE-2.0
;
; Unless required by applicable law or agreed to in writing, software
; distributed under the License is distributed on an "AS IS" BASIS,
; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
; See the License for the specific language governing permissions and
; limitations under the License.

; This is a SMT-LIB solution to
; https://ed.ted.com/lessons/can-you-solve-the-fish-riddle-steve-wyborney.

; There are fish tanks and sharks.
(declare-const tanks-a Int)
(declare-const tanks-b Int)
(declare-const tanks-c Int)
(declare-const sharks-a Int)
(declare-const sharks-b Int)
(declare-const sharks-c Int)
(assert (>= tanks-a 0))
(assert (>= tanks-b 0))
(assert (>= tanks-c 0))
(assert (>= sharks-a 0))
(assert (>= sharks-b 0))
(assert (>= sharks-c 0))

; There are fish in the tanks.
(declare-const fish-per-tank Int)
(assert (>= fish-per-tank 0))

(define-fun tanks () Int (+ tanks-a tanks-b tanks-c))
(define-fun fish () Int (* fish-per-tank tanks))
(define-fun sharks () Int (+ sharks-a sharks-b sharks-c))
(define-fun total-creatures () Int (+ fish sharks))

; There are 50 creatures total.
(assert (= total-creatures 50))

; Each sector has between 1 and 7 sharks.
(assert (<= 1 sharks-a 7))
(assert (<= 1 sharks-b 7))
(assert (<= 1 sharks-c 7))

; No two sectors have the same number of sharks.
(assert (not (= sharks-a sharks-b)))
(assert (not (= sharks-b sharks-c)))
(assert (not (= sharks-a sharks-c)))

; There are 13 or fewer tanks.
(assert (<= tanks 13))

; We know some stuff about sectors alpha and beta.
(assert (= sharks-a 2))
(assert (= tanks-a 4))
(assert (= sharks-b 4))
(assert (= tanks-b 2))

(check-sat)
(get-model)