aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--README.md3
-rw-r--r--entries/adirar111/y86/fib.s (renamed from entries/adirar111/y86/fib.ys)11
-rw-r--r--entries/funemy/.gitignore2
-rw-r--r--entries/funemy/agda/fib1.agda2
-rwxr-xr-xentries/funemy/z3/z3fib.sh48
5 files changed, 60 insertions, 6 deletions
diff --git a/README.md b/README.md
index b3dd74f..e2c309e 100644
--- a/README.md
+++ b/README.md
@@ -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