diff options
Diffstat (limited to 'entries')
-rw-r--r-- | entries/adirar111/y86/fib.s (renamed from entries/adirar111/y86/fib.ys) | 11 | ||||
-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 |
4 files changed, 58 insertions, 5 deletions
diff --git a/entries/adirar111/y86/fib.ys b/entries/adirar111/y86/fib.s index 156c1ae..8aa62d2 100644 --- a/entries/adirar111/y86/fib.ys +++ b/entries/adirar111/y86/fib.s @@ -1,8 +1,13 @@ # y86 implementation of +# # def fibonacci(n): -# if n <= 1: -# return n -# return fibonacci(n-1) + fibonacci(n-2) +# if n <= 1: +# return n +# return fibonacci(n-1) + fibonacci(n-2) +# +# run it: +# * https://www.students.cs.ubc.ca/~cs-313/simulator/?arch=y86&impl=seq +# * https://www.eecs.yorku.ca/~jonatan/simulator/?arch=y86&impl=seq .pos 0 main: 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..9faa228 --- /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. 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 |