Add second set of z3py notes

notes/z3py-intro-cont/z3py-intro-cont.md

 ### List Comprehensions
 
 Before we start writing the solver, let's look at an incredibly useful Python feature - the list comprehension.
-You're probably familiar with this method of creating a list based on the contents of an iterable:
+Often, we will want to create a list after calling some function on each element of an iterable:
 
 ```python
 lst = []
     lst.append(f(elem))
 ```
 
-This can be replaced by a *list comprehension*:
+This can be replaced by a more concise *list comprehension*:
 
 ```python
 lst = [f(elem) for elem in iterable]
 
 When solving logic puzzles, we will often want to work with grids.
 List comprehensions are very useful concise tools for constructing groups of variables at once, or constructing many related conditions at once.
-
 Another useful tool is the dictionary comprehension:
 
 ```python
         lst.append(f(e1, e2))
 
 lst = [f(e1, e2) for e1 in iter1 for e2 in iter2]
+```
 
 Some common z3 patterns that use  comprehensions include:
 
 
 A common constraint that appears in puzzles is that a set of cells must be filled with numbers so that no two cells contain the same number.
 It is possible to create such a constraint by asserting inequality for every pair of cells.
-However, since this is such a common pattern, z3 actually provides a function to assert that each cell must take on a *Distinct* value:
+However, since this is such a common pattern, z3 actually provides a function to assert that each variable must take on a *Distinct* value. Let's look at this in the context of cryptarithms:
 
 ```python
-# TODO
+# Solve the cryptarithm
+# SEND + MORE = MONEY
+
+letters = {c: Int(c) for c in set('SENDMOREMONEY')}
+s = Solver()
+
+# Each letter is a single digit
+s.add([And(0 <= c, c <= 9) for c in letters.values()])
+
+# The math must check out.
+send = Sum([10 ** i * letters[c] for i, c in enumerate('SEND'[::-1])])
+more = Sum([10 ** i * letters[c] for i, c in enumerate('MORE'[::-1])])
+money = Sum([10 ** i * letters[c] for i, c in enumerate('MONEY'[::-1])])
+s.add(send + more == money)
+
+# Leading digits shouldn't be 0
+s.add(letters['S'] != 0, letters['M'] != 0)
+
+# DISTINCT
+# Each letter must take on a distinct value
+# .values() isn't actually a list, so it has to be cast :(
+s.add(Distinct(list(letters.values())))
+
+if s.check():
+    print(s.model())
+    # [D = 7, R = 8, N = 6, S = 9, O = 0, M = 1, E = 5, Y = 2]
 ```
 
-<!-- Mention that Distinct takes List or args -->
+Similar to `And` and `Or`, `Distinct` can accept any number of arguments, or a list of variables.
 
 ### The Solver
 
 
 ```python
 solver.add([
-    And(1 <= grid[r][c], grid[r][c]) <= 9
+    And(1 <= grid[r][c], grid[r][c] <= 9)
     for r in range(9)
     for c in range(9)
 ])
 # Rows
 solver.add([Distinct(grid[r]) for r in range(9)])
 
-# Equivalent rows
+# Equivalent conditions for rows
 for r in range(9):
     solver.add(Distinct(grid[r]))
 
 # Columns
 solver.add([Distinct([grid[r][c] for r in range(9)]) for c in range(9)])
 
-# Equivalent columns
+# # Equivalent conditions for columns
 for c in range(9):
-    # Extract the cell at the current column for each row
-    col = [grid[r][c] for r in range(9)] 
+    col = []
+    for r in range(9):
+        col.append(grid[r][c])
     solver.add(Distinct(col))
 
 # Blocks
     print("No solution")
 ```
 
-NOTE: I repeated the same loops over rows and columns throughout this code.
+NOTE: I know that there are some occurences of repetition throughout this code.
 I wrote it this way to intentionally "separate" each "type" of condition from each other.
 If I had bugs in this, it is much easier to debug and tweak conditions when they are processed in separate blocks of code.
 Personally, a bit more boilerplate is much more preferable than code that is a pain to debug.