From 31c1cf935f5c0ef7423266d0d1a7c9e0421312a8 Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <benjamin@barenblat.name>
Date: Thu, 17 Aug 2017 13:57:50 -0400
Subject:

---
 fish_riddle.smt2 | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 fish_riddle.smt2

diff --git a/fish_riddle.smt2 b/fish_riddle.smt2
new file mode 100644
index 0000000..e3f4a2f
--- /dev/null
+++ b/fish_riddle.smt2
@@ -0,0 +1,64 @@
+; 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)
\ No newline at end of file
-- 
cgit v1.2.3