diff options
Diffstat (limited to 'entries/funemy/z3/z3fib.sh')
| -rwxr-xr-x | entries/funemy/z3/z3fib.sh | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh index 9faa228..07ab418 100755 --- a/entries/funemy/z3/z3fib.sh +++ b/entries/funemy/z3/z3fib.sh @@ -1,7 +1,7 @@ #!/bin/bash -# Instruction: -# 1. having z3 installed and under you $PATH +# Instructions: +# 1. having z3 installed and put under your $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 :) @@ -14,6 +14,11 @@ else touch fib.smt2 fi +if [ "$1" -lt "0" ]; then + echo "Argument must be larger than 0." + exit 1 +fi + for i in $(seq 0 $1); do echo "(declare-const x$i Int)" >> fib.smt2 @@ -30,12 +35,16 @@ do done echo " (= x0 0)" >> fib.smt2 -echo " (= x1 1)" >> fib.smt2 +if [ "$1" -ge "1" ]; then + echo " (= x1 1)" >> fib.smt2 +fi -for i in $(seq 2 $1); -do - echo " (= x$i (+ x$(($i - 2)) x$(($i - 1))))" >> fib.smt2 -done +if [ "$1" -ge "2" ]; then + for i in $(seq 2 $1); + do + echo " (= x$i (+ x$(($i - 2)) x$(($i - 1))))" >> fib.smt2 + done +fi echo " )" >> fib.smt2 echo ")" >> fib.smt2 |