From 72c87a2aafa2bd98952494463353b2a48c1a06f5 Mon Sep 17 00:00:00 2001
From: funemy
Date: Sun, 23 Oct 2022 15:30:17 -0700
Subject: boring one

---
 entries/funemy/.gitignore     |  1 +
 entries/funemy/agda/fib1.agda | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 entries/funemy/.gitignore
 create mode 100644 entries/funemy/agda/fib1.agda

(limited to 'entries/funemy')

diff --git a/entries/funemy/.gitignore b/entries/funemy/.gitignore
new file mode 100644
index 0000000..171a389
--- /dev/null
+++ b/entries/funemy/.gitignore
@@ -0,0 +1 @@
+*.agdai
diff --git a/entries/funemy/agda/fib1.agda b/entries/funemy/agda/fib1.agda
new file mode 100644
index 0000000..9e7f82a
--- /dev/null
+++ b/entries/funemy/agda/fib1.agda
@@ -0,0 +1,36 @@
+open import Agda.Builtin.Equality
+
+data Nat : Set where
+  zero : Nat
+  suc : Nat -> Nat
+
+{-# BUILTIN NATURAL Nat #-}
+
+z : Nat
+z = zero
+
+one : Nat
+one = suc zero
+
+add : Nat → Nat → Nat
+add zero y = y
+add (suc x) y = suc (add x y)
+
+fib : Nat → Nat
+fib zero = zero
+fib (suc zero) = suc zero
+fib (suc (suc x)) = add (fib x) (fib (suc x))
+
+fib0 : fib 0 ≡ 0
+fib0 = refl
+
+fib1 : fib 1 ≡ 1
+fib1 = refl
+
+fib2 : fib 2 ≡ 1
+fib2 = refl
+
+fib8 : fib 8 ≡ 21
+fib8 = refl
+
+
-- 
cgit v1.2.3-70-g09d2


From 679ee8faf561b6e53f582edef2d93b65615bcea7 Mon Sep 17 00:00:00 2001
From: funemy
Date: Sun, 23 Oct 2022 16:14:40 -0700
Subject: z3 fib impl

---
 entries/funemy/.gitignore     |  2 ++
 entries/funemy/agda/fib1.agda |  2 --
 entries/funemy/z3/z3fib.sh    | 48 +++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 50 insertions(+), 2 deletions(-)
 create mode 100755 entries/funemy/z3/z3fib.sh

(limited to 'entries/funemy')

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
-- 
cgit v1.2.3-70-g09d2


From a89c7847195a7b20e307b042fbc821e741ccdaa4 Mon Sep 17 00:00:00 2001
From: funemy
Date: Sun, 23 Oct 2022 16:16:41 -0700
Subject: minor

---
 entries/funemy/z3/z3fib.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
index fdc8937..9faa228 100755
--- a/entries/funemy/z3/z3fib.sh
+++ b/entries/funemy/z3/z3fib.sh
@@ -3,7 +3,7 @@
 # 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]`
+#  3. running as `./z3fib.sh [length of the fib sequence]`
 #  4. having fun :)
 
 if [ -e fib.smt2 ]
-- 
cgit v1.2.3-70-g09d2


From 201f9e290b59838ed249b7d1be03e5b8230bef3e Mon Sep 17 00:00:00 2001
From: funemy
Date: Sun, 23 Oct 2022 19:21:33 -0700
Subject: add proper bound check

---
 entries/funemy/z3/z3fib.sh | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
index 9faa228..03a7209 100755
--- a/entries/funemy/z3/z3fib.sh
+++ b/entries/funemy/z3/z3fib.sh
@@ -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
@@ -32,10 +37,13 @@ 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
+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
-- 
cgit v1.2.3-70-g09d2


From 31aa5baf3cc0935b579ac41b194f46e771443583 Mon Sep 17 00:00:00 2001
From: funemy
Date: Sun, 23 Oct 2022 19:24:26 -0700
Subject: minor

---
 entries/funemy/z3/z3fib.sh | 1 -
 1 file changed, 1 deletion(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
index 03a7209..d3a93c2 100755
--- a/entries/funemy/z3/z3fib.sh
+++ b/entries/funemy/z3/z3fib.sh
@@ -44,7 +44,6 @@ if [ "$1" -ge "2" ]; then
   done
 fi
 
-
 echo "  )" >> fib.smt2
 echo ")" >> fib.smt2
 
-- 
cgit v1.2.3-70-g09d2


From 08986a7a748a8ae747e076a3807e367f479b3ece Mon Sep 17 00:00:00 2001
From: funemy
Date: Sun, 23 Oct 2022 19:26:05 -0700
Subject: fix

---
 entries/funemy/z3/z3fib.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
index d3a93c2..ecf42b4 100755
--- a/entries/funemy/z3/z3fib.sh
+++ b/entries/funemy/z3/z3fib.sh
@@ -35,7 +35,9 @@ do
 done
 
 echo "    (= x0 0)" >> fib.smt2
-echo "    (= x1 1)" >> fib.smt2
+if [ "$1" -ge "1" ]; then
+  echo "    (= x1 1)" >> fib.smt2
+fi
 
 if [ "$1" -ge "2" ]; then
   for i in $(seq 2 $1);
-- 
cgit v1.2.3-70-g09d2


From dffabc78b6c1e4e01b2618f5ba274b375b5c7cc4 Mon Sep 17 00:00:00 2001
From: funemy
Date: Sun, 23 Oct 2022 19:27:25 -0700
Subject: minor

---
 entries/funemy/z3/z3fib.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
index ecf42b4..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 :)
-- 
cgit v1.2.3-70-g09d2