blob: 9faa22852927608bcfab09ef6b501b0ed4d34712 (
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
41
42
43
44
45
46
47
48
|
#!/bin/bash
# Instruction:
# 1. having z3 installed and under you $PATH
# 2. making sure z3fib.sh is executable, by `chmod +x z3fib.sh`
# 3. running as `./z3fib.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
for i in $(seq 0 $1);
do
echo "(declare-const x$i Int)" >> fib.smt2
done
echo "" >> fib.smt2
echo "(assert" >> fib.smt2
echo " (and" >> fib.smt2
for i in $(seq 0 $1);
do
echo " (>= x$i 0)" >> fib.smt2
done
echo " (= x0 0)" >> fib.smt2
echo " (= x1 1)" >> fib.smt2
for i in $(seq 2 $1);
do
echo " (= x$i (+ x$(($i - 2)) x$(($i - 1))))" >> fib.smt2
done
echo " )" >> fib.smt2
echo ")" >> fib.smt2
echo "" >> fib.smt2
echo "(check-sat)" >> fib.smt2
echo "(get-model)" >> fib.smt2
z3 fib.smt2
|
