|author||Benjamin Barenblat <firstname.lastname@example.org>||2017-08-17 13:57:50 -0400|
|committer||GitHub <email@example.com>||2017-08-17 13:57:50 -0400|
1 files changed, 64 insertions, 0 deletions
diff --git a/fish_riddle.smt2 b/fish_riddle.smt2
new file mode 100644
@@ -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
+; 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
+; 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))
+(get-model) \ No newline at end of file