Add second set of z3py notes

notes/z3py-intro/z3py-intro.md

 
 To cast integers, we use `model[var].as_long()`.
 To cast booleans, you can directly cast the value: `bool(model[bool_var])`.
+We can also directly cast z3 values to strings: `str(model[var])`.
 We can also evaluate expressions in the context of the model; when `model.evaluate(expr)` is called with an expression, known variables are plugged in.
 
 [Here is a helpful StackOverflow post](https://stackoverflow.com/questions/12598408/z3-python-getting-python-values-from-model/12600208) that describes how to get Python values from various z3 types.

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

+# z3py Introduction, Continued
+
+## Sudoku
+
+[Sudoku](https://en.wikipedia.org/wiki/Sudoku) is a well-known logic puzzle with simple rules.
+Given some digits, the objective is to fill a 9x9 grid with one digit per cell so that each column, each row, and each of the nine 3x3 blocks contain every digit from 1-9.
+This means that there cannot be any repeated digits in a block, row, or column.
+
+Many Sudoku solvers exist online, but we're going to write our own!
+
+### 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:
+
+```python
+lst = []
+for elem in iterable:
+    # f is an arbitrary function
+    lst.append(f(elem))
+```
+
+This can be replaced by a *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
+dct = {}
+for elem in iterable:
+    dct[f1(elem)] = f2(elem)
+
+# Equivalent:
+dct = {f1(elem): f2(elem) for elem in iterable}
+```
+
+We can also handle nested for loops that build a single list:
+
+```python
+lst = []
+for e1 in iter1:
+    for e2 in iter2:
+        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:
+
+- Storing z3 variables in a list or 2D list
+- Storing z3 variables in a dictionary that maps string identifiers to variables
+- Asserting a common constraint that applies to each variable in an iterable (i.e. all cells must contain a number in a range)
+
+### Distinct
+
+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:
+
+```python
+# TODO
+```
+
+<!-- Mention that Distinct takes List or args -->
+
+### The Solver
+
+We'll work with input as a 2D list:
+
+```python
+sudoku = (
+    (0,0,0,0,0,0,7,0,1),
+    (8,0,4,0,0,3,5,0,6),
+    (0,0,0,0,0,0,0,0,0),
+    (1,0,0,0,2,4,0,0,0),
+    (3,9,0,0,6,0,0,0,0),
+    (0,0,0,0,0,5,0,0,0),
+    (0,0,0,0,0,0,0,2,0),
+    (7,1,0,5,0,0,8,0,9),
+    (0,9,0,0,8,0,1,3,0),
+)
+```
+
+Since we are placing integers 1-9 in a 9x9 grid, we can use an `Int` to represent the value we will place in each cell.
+We'll use a nested list comprehension to construct the grid.
+
+```python
+grid = [[Int(f'sudoku_{r}_{c}') for c in range(9)] for r in range(9)]
+solver = Solver()
+```
+
+Note that the variable corresponding to each cell must have a unique z3 identifier, which we've ensured by using the row and column.
+Then, we can only place digits from 1-9 in these cells.
+
+```python
+solver.add([
+    And(1 <= grid[r][c], grid[r][c]) <= 9
+    for r in range(9)
+    for c in range(9)
+])
+
+# Equivalent to
+for r in range(9):
+    for c in range(9):
+        # Note that I can expand into multiple conditions since the
+        # And is top-level
+        solver.add(1 <= grid[r][c])
+        solver.add(grid[r][c] <= 9)
+```
+
+We also need to make sure that our assignment agrees with the given values.
+
+```python
+solver.add([
+    grid[r][c] == sudoku[r][c]
+    for r in range(9)
+    for c in range(9)
+    # 0 is falsy!
+    if sudoku[r][c]
+])
+
+# Equivalent to
+for r in range(9):
+    for c in range(9):
+        # 0 is falsy!
+        if sudoku[r][c]:
+            solver.add(grid[r][c] == sudoku[r][c])
+```
+
+Next, each row and column and block must contain every value from 1-9.
+There's two different ways that this can be expressed as a z3 expression.
+We could take this condition literally, and assert that each value from 1-9 appears at least once in every row / column / block via an `And` of an `Or`s for each digit.
+Alternatively, we could use z3's `Distinct` - there are 9 values and 9 cells, so if every cell takes on a distinct value, then every value must appear.
+
+`Distinct` is much faster than the alternative expression.
+If we used an `And` of `Or`s, z3 would have to rederive the "obvious" fact that no two cells in a group can have the same value; it's not an immediate logical conclusion.
+
+The form in which we express our constraints matters.
+Additionally, making some implicit constraints explicit can speed up the solver, by allowing it to apply its heuristics earlier.
+While it's slightly contrived here, we'll see some more examples of this in other genres.
+
+Now, the conditions:
+
+```python
+# Rows
+solver.add([Distinct(grid[r]) for r in range(9)])
+
+# Equivalent 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
+for c in range(9):
+    # Extract the cell at the current column for each row
+    col = [grid[r][c] for r in range(9)] 
+    solver.add(Distinct(col))
+
+# Blocks
+solver.add([
+    Distinct([
+        grid[3 * r0 + r_offset][3 * c0 + c_offset]
+        for r_offset in range(3)
+        for c_offset in range(3)
+    ])
+    for r0 in range(3)
+    for c0 in range(3)
+])
+
+# Equivalent, more verbose / explicit blocks
+for r0 in range(3):
+    for c0 in range(3):
+        block_cells = []
+        for r_offset in range(3):
+            for c_offset in range(3):
+                block_cells.append(grid[3 * r0 + r_offset][3 * c0 + c_offset])
+        solver.add(Distinct(block_cells))
+```
+
+We've added all the constraints that make up a Sudoku puzzle!
+Now, we just need to run the solver and output the solution.
+
+```python
+if solver.check() == sat:
+    m = solver.model()
+    # Extract model into a grid of strings
+    str_grid = [[str(m[grid[r][c]]) for c in range(9)] for r in range(9)]
+    # Print the grid as a compressed grid of numbers
+    print("\n".join(["".join(str_grid)]))
+
+    # Equivalent to:
+    for r in range(9):
+        row = []
+        for c in range(9):
+            row.append(str(m[grid[r][c]]))
+        print("".join(row))
+else:
+    print("No solution")
+```
+
+NOTE: I repeated the same loops over rows and columns 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.
+
+### Modifying Your Solver
+
+Now that we've written our solver, it's possible to *modify* it to solve sudoku variants as well (something you can't do with online solvers)!
+For example, Killer Sudoku has the additional constraint that some regions of cells must add up to a particular number.
+This constraint has a direct SMT analogue!
+You may also be familiar with [Cracking the Cryptic's](https://www.youtube.com/c/CrackingTheCryptic) YouTube channel.
+Nearly *every* Sudoku variant they've presented (chess, thermometer, etc.) can be cleanly represented in an SMT framework.
+
+The annoying part of writing solvers for Sudoku variants is deciding what form the input should take...
+
+![notlikeduck](NotLikeDuck.png)
+
+## Conditionals
+
+In logic puzzles, depending on what the contents of a cell, are different constraints may apply.
+z3 provides functions to create conditional expressions:
+
+```python
+If(cond, then_expr, else_expr)
+```
+
+If `cond` evaluates to `True`, then `If` evaluates to `then_expr`.
+Otherwise, `If` evalutes to `else_expr`.
+This means that `then_expr` and `else_expr` must be of the same type.
+
+```python
+Implies(cond, expr)
+```
+
+`Implies` evalutes to true iff `If(cond, expr, True)`. evaluates to true.
+Note that `expr` must evaluate to a `Boolean`.
+
+WARNING: If `cond` evaluates to `False`, `expr` may take on any truth value, i.e. from a false proposition, anything can follow.
+This behavior is different from `cond == expr`.
+
+### Conditionals Example
+
+<!-- TODO -->
+
+## Pseudo Boolean Constraints
+
+<!-- TODO -->
\ No newline at end of file