diff options
| -rw-r--r-- | entries/funemy/.gitignore | 2 | ||||
| -rw-r--r-- | entries/funemy/agda/fib1.agda | 2 | ||||
| -rwxr-xr-x | entries/funemy/z3/z3fib.sh | 48 |
3 files changed, 50 insertions, 2 deletions
diff --git a/entries/funemy/.gitignore b/entries/funemy/.gitignore index 171a389..acb903a 100644 --- a/entries/funemy/.gitignore +++ b/entries/funemy/.gitignore @@ -1 +1,3 @@ +.DS_Store *.agdai +*.smt2 diff --git a/entries/funemy/agda/fib1.agda b/entries/funemy/agda/fib1.agda index 9e7f82a..d8931a0 100644 --- a/entries/funemy/agda/fib1.agda +++ b/entries/funemy/agda/fib1.agda @@ -32,5 +32,3 @@ fib2 = refl fib8 : fib 8 ≡ 21 fib8 = refl - - diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh new file mode 100755 index 0000000..fdc8937 --- /dev/null +++ b/entries/funemy/z3/z3fib.sh @@ -0,0 +1,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. run 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 |