blob: e3f4a2f8df39a23644e661e77760d6ed607c3dd8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
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)
|
