blob: f7a1e48b63251f27818db32cbcf427f944e5e6f3 (
plain) (
blame)
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
|
#!/bin/bash
# z3 fib, but better
# Instructions:
# 1. having z3 installed and put under your $PATH
# 2. making sure z4fib.sh is executable, by `chmod +x z4fib.sh`
# 3. running as `./z4fib.sh [length of the fib sequence]`
# 4. having fun :)
if [ -e fib.smt2 ]
then
rm -f fib.smt2
touch fib.smt2
else
touch fib.smt2
fi
if [ "$1" -lt "0" ]; then
echo "Argument must be larger or equal to 0."
exit 1
fi
echo "(declare-const fib (Seq Int))" >> fib.smt2
echo "" >> fib.smt2
echo "(assert" >> fib.smt2
echo " (and" >> fib.smt2
echo " (= (seq.len fib) $1)" >> fib.smt2
echo " (= (seq.nth fib 0) 0)" >> fib.smt2
echo " (= (seq.nth fib 1) 1)" >> fib.smt2
echo " (forall ((i Int))" >> fib.smt2
echo " (=> (and (> i 1) (< i (seq.len fib)))" >> fib.smt2
echo " (= (seq.nth fib i)" >> fib.smt2
echo " (+ (seq.nth fib (- i 1))" >> fib.smt2
echo " (seq.nth fib (- i 2))))))))" >> fib.smt2
echo "" >> fib.smt2
echo "(check-sat)" >> fib.smt2
echo "(get-model)" >> fib.smt2
z3 fib.smt2
|
