diff options
-rw-r--r-- | README.md | 3 | ||||
-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 |
5 files changed, 60 insertions, 6 deletions
@@ -5,7 +5,7 @@ Can you please give me a Fibonacci function? Ideally (but not necessarily) one t For a submission to the upcoming "Reclaim your space" exhibition at [Hatch Art Gallery](https://www.instagram.com/hatch_artgallery). ### [`adirar111`](https://github.com/adirar111) -- [`y86`](./entries/adirar111/y86/fib.ys) +- [`y86`](./entries/adirar111/y86/fib.s) ### [`braxtonhall`](https://github.com/braxtonhall) - [`adam`](./entries/braxtonhall/adam/main.py) (WIP) @@ -17,6 +17,7 @@ For a submission to the upcoming "Reclaim your space" exhibition at [Hatch Art G ### [`funemy`](https://github.com/funemy) - [`agda`](./entries/funemy/agda/fib1.agda) +- [`z3`](./entries/funemy/z3/z3fib.sh) ### [`jyoo980`](https://github.com/jyoo980) - [`scala`](./entries/jyoo980/scala/Fib.scala) 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 |