From 274071368cb659a236fc5914b94117302fe9256c Mon Sep 17 00:00:00 2001
From: Brandon Rozek <rozekbrandon@gmail.com>
Date: Fri, 18 Jun 2021 00:59:45 -0400
Subject: [PATCH] New Posts

---
 content/blog/human-readable-sizes.md | 47 ++++++++++++++++++++++++++++
 content/blog/z3constraintsolving.md  | 45 ++++++++++++++++++++++++++
 2 files changed, 92 insertions(+)
 create mode 100644 content/blog/human-readable-sizes.md
 create mode 100644 content/blog/z3constraintsolving.md

diff --git a/content/blog/human-readable-sizes.md b/content/blog/human-readable-sizes.md
new file mode 100644
index 0000000..a5ffad6
--- /dev/null
+++ b/content/blog/human-readable-sizes.md
@@ -0,0 +1,47 @@
+---
+title: "Human Readable Sizes"
+date: 2021-03-15T19:11:35-04:00
+draft: false
+tags: []
+---
+
+When playing with large and small values, it is useful to convert them to a different unit in scientific notation. Let's look at bytes.
+
+```python
+size_categories = ["B", "KB", "MB", "GB", "TB"]
+```
+
+You can figure out how to best represent it by seeing how many of the base (in this case 1000) fits into the value.
+$$
+category = \lfloor \frac{\log{(size_{bytes})}}{\log{(base)}} \rfloor
+$$
+You'll want to make sure that you don't overflow in the number of categories you have
+
+```python
+category_num = min(category_num, len(size_categories))
+```
+
+You can then get its category representation by
+$$
+size = \frac{size_{bytes}}{(2^{category})}
+$$
+We can wrap this all up info a nice python function
+
+```python
+def humanReadableBytes(num_bytes: int) -> str:
+    base = 1000
+    
+    # Zero Case
+    if num_bytes == 0:
+        return "0"
+    
+    size_categories = ["B", "KB", "MB", "GB", "TB"]
+    category_num = int(math.log(num_bytes) / math.log(base))
+    
+    # Make sure it doesn't overflow
+    category_num = min(category_num, len(size_categories) - 1)
+    
+    return "{:.2f} ".format(num_bytes / (base ** category_num)) + \
+			size_categories[category_num]
+```
+
diff --git a/content/blog/z3constraintsolving.md b/content/blog/z3constraintsolving.md
new file mode 100644
index 0000000..042f1b6
--- /dev/null
+++ b/content/blog/z3constraintsolving.md
@@ -0,0 +1,45 @@
+---
+title: "Z3 Constraint solving"
+date: 2021-06-18T00:53:20-04:00
+draft: false
+tags: []
+---
+
+I've been looking for an easy to use constraint solver for a while and recently I've landed on using the python bindings for the SMT solver Z3.
+
+To install:
+
+```bash
+pip install z3-solver
+```
+
+Let's say you want to find non-negative solutions for the following Diophantine equation:
+$$
+9x - 100y = 1
+$$
+To do that, we import Z3, declare our integer variables, and pass it into a solve function:
+
+```python
+from z3 import *
+x, y = Ints("x y")
+solve(9 * x - 100 * y == 1, x >= 0, y >= 0)
+```
+
+This will print out: `[y = 8, x = 89]`
+
+If you want to use these values for later computations, you'll have to setup a Z3 model:
+
+```python
+from z3 import *
+x, y = Ints("x y")
+s = Solver
+s.add(9 * x - 100 * y == 1)
+s.add(x >= 0)
+s.add(y >= 0)
+
+s.check()
+m = s.model()
+x_val = m.eval(x)
+y_val = m.eval(y)
+```
+