PythonTutorial.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "rise": {
     "theme": "night"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "# Python - Numpy Tutorial\n",
    "### September 29, 2020"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Today's main focus\n",
    "* **Basic Python:**\n",
    "    * Basic data types (Containers, Lists, Dictionaries, Sets, Tuples)\n",
    "    * Flow Control (if, else)\n",
    "    * Loops\n",
    "    * Functions\n",
    "* **Numpy:** \n",
    "    * Arrays, Array indexing, Array math\n",
    "* **Sympy:**\n",
    "    * Symbolic expressions, Integrals, IsPrime.\n",
    "* **Z3 Solver**\n",
    "    * Explanation of functions found in the slides and previous HW solutions."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Python Installation\n",
    "* Just Python: https://www.python.org/\n",
    "* Python + Other Libraries (numpy, matplotlib, scipy..): https://www.anaconda.com/\n",
    "\n",
    "## Numpy installation\n",
    "* pip install numpy\n",
    "\n",
    "## Sympy Installation\n",
    "* pip install sympy\n",
    "\n",
    "## Z3\n",
    "* pip install z3-solver"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Basics of Python\n",
    "### Python versions\n",
    "\n",
    "There are currently two different supported versions of **Python, 2.7 and 3.7 - 3.8** \n",
    "\n",
    "**Python 3** is what will be used today. \n",
    "\n",
    "Check your Python version at the command line by running: `python --version`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "! python --version"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Python environments\n",
    "\n",
    "* Python can be run from the command line\n",
    "    * REPL (Read-Eval-Print-Loop)\n",
    "    * Run a script\n",
    "* Jupyter notebook"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Basic data types\n",
    "### Numbers\n",
    "Integers and floats work as you would expect from other languages:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    " x = 2\n",
    "print(x, type(x))\n",
    "\n",
    "x, type(x) # Notebook cell output"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "x = 2\n",
    "print(x + 1)   # Addition; \n",
    "print(x - 1)   # Subtraction; \n",
    "print(x * 2)   # Multiplication;\n",
    "print(x ** 2)  # Exponentiation; "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Variables are modified by the \"=\" sign."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "x = 3 \n",
    "x = x + 1\n",
    "print(x)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "x = 3\n",
    "x += 1  # The same as x = x + 1\n",
    "print(x)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "x *= 2    # The same as x = x*2\n",
    "print(x)  # Prints \"8\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "In python 3, even though we are dividing two integers the result can be a float, just like in Matlab. **This is not true for python 2**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print(type(x))\n",
    "print(x/2)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Python also has built-in types for **long integers and complex numbers**; you can find all of the details in the [documentation](https://docs.python.org/3.7/library/stdtypes.html#numeric-types-int-float-long-complex)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "c1 = 2 + 3j\n",
    "c2 = 1 - 2j\n",
    "print(c1 + c2)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Booleans\n",
    "Python implements all of the usual operators for Boolean logic, but uses **English words** rather than symbols (`&&`, `||`, etc.):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "t, f = True, False ## Simultaneous assignment of t and f\n",
    "print(type(t))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Now we let's look at the operations:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print(t and f) # Logical AND;\n",
    "print(t or f)# Logical OR;\n",
    "print(not t)   # Logical NOT;\n",
    "print(t ^ f)  # Logical XOR;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Containers\n",
    "Python includes several built-in container types: \n",
    "* Lists \n",
    "* Dictionaries\n",
    "* Sets\n",
    "* Tuples"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Lists\n",
    "A list is the Python equivalent of an array, but is resizeable and can contain elements of different types. **Indexes start at 0 not at 1.**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "xs = [3, 1, 2]   # Create a list\n",
    "print(xs)\n",
    "print(xs[0])\n",
    "print(xs[-1])     # Negative indices count from the end of the list; prints \"2\"\n",
    "                  # like gettin x(end) in MATLAB\n",
    "print(xs[-2])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "xs[2] = 'foo'\n",
    "print(xs)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": true,
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "xs.append('bar') # Add a new element to the end of the list\n",
    "                 # Modifies the list in place\n",
    "print(xs)\n",
    "# What happens if we run the cell multiple times?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "x = xs.pop()     # Remove and return the last element of the list\n",
    "print(\"Last element removed\", x)\n",
    "print(\"The list\", xs)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "One can also concatenate lists by using the *+* operator"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "a = [1,2]\n",
    "b = [3, 4, 5]\n",
    "c = [1, 2 , 3] + [\"a\", \"b\", \"c\"] + [[1,2], [1, 2,3]]\n",
    "print(c)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Slicing\n",
    "Python provides **concise syntax to access sublists**; this is known as slicing."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "nums = [1, 3, 5, 7, 10]    \n",
    "print(nums)         # Prints \"[0, 1, 2, 3, 4]\"\n",
    "print(nums[2:4])    # Get a slice from index 2 to 4 (exclusive)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print(nums[2:])     # Get a slice from index 2 to the end\n",
    "print(nums[:2])     # Get a slice from the start to index 2 (exclusive)  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print(nums[:])      # Get a slice of the whole list\n",
    "print(nums[:-1])    # Slice indices can be negative"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Loops"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "animals = ['cat', 'dog', 'monkey']\n",
    "for animal in animals:\n",
    "    print(animal)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "If you want access to the index of each element within the body of a loop, use the built-in `enumerate` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "animals = ['cat', 'dog', 'monkey']\n",
    "for idx, animal in enumerate(animals):\n",
    "    print(f\".{idx}. {animal}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Tuples\n",
    "* **Immutable** ordered list of values\n",
    "* Can be used as elements of sets, while lists cannot."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "## Create and print the tuple\n",
    "tup = (1, 2, 3)\n",
    "print(\"The tuple:\", tup)\n",
    "## Create a set with a tuple inside it\n",
    "set_w_tuple = {1, 2, (1, 2)}\n",
    "print(\"Set with tuple:\", set_w_tuple)\n",
    "## Create a set with a tuple inside it\n",
    "set_w_list = {1, 2, [1, 2]}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Tuples are *inmutable*. Cannot change its elements after creation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "tup = (1, 2, 3)\n",
    "tup[0] = 0"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Functions and flow control\n",
    "Python functions are defined using the `def` keyword. For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "def sign(x):\n",
    "    if x > 0:\n",
    "        return 'positive'\n",
    "    elif x < 0:\n",
    "        return 'negative'\n",
    "    else:\n",
    "        return 'zero'\n",
    "\n",
    "for x in [-1, 0, 1]:\n",
    "    print(sign(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## List comprehension vs Loop appending\n",
    "**Goal**: Create and \"populate\" a list with some given condition for the elements.\n",
    "\n",
    "**Example**: Create a list with the squares of the numbers 1 to 9."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Loop"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[1, 4, 9, 16, 25, 36, 49, 64, 81]\n"
     ]
    }
   ],
   "source": [
    "a = []\n",
    "for number in range(1, 10):\n",
    "    a.append(number**2)\n",
    "print(a)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### List comprehension"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[1, 4, 9, 16, 25, 36, 49, 64, 81]\n"
     ]
    }
   ],
   "source": [
    "a = [number**2 for number in range(1, 10)]\n",
    "print(a)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "# Short Assignmet 1 (FizzBuzz)\n",
    "* Define a function that receives a number and prints **Fizz** if the number is divisible by **3** and **Buzz** if it is divisible by **5**. \n",
    "* Run a `for` loop that uses the function on each iteration feeding it the numbers from 1 to 42. \n",
    "\n",
    "**Note**: The `modulo` operator in python is `%`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Numpy\n",
    "[Numpy](http://www.numpy.org/) is the core library for scientific computing in Python. It provides a high-performance multidimensional array object, and tools for working with these arrays. If you are already familiar with MATLAB, you might find this [tutorial](https://docs.scipy.org/doc/numpy-1.15.0/user/numpy-for-matlab-users.html) useful to get started with Numpy."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "To use Numpy, we first need to import the `numpy` package:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "import numpy as np"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Arrays\n",
    "* A numpy array is a grid of values, all of the same type, and is indexed by a tuple of nonnegative integers. \n",
    "* The number of dimensions is the rank of the array.\n",
    "* The shape of an array is a tuple of integers giving the size of the array along each dimension."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "We can initialize numpy arrays from nested Python lists, and access elements using square brackets:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "a = np.array([1, 2, 3])  # Create a rank 1 array\n",
    "print(a)\n",
    "a[0] = 5                 # Change an element of the array\n",
    "print(a)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "b = np.array([[1,2,3],[4,5,6]])   # Create a rank 2 array. A list of lists is used to create the array.\n",
    "print(b)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print(b.shape)\n",
    "print(b[0, 0], b[0, 1], b[1, 0])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "Numpy also provides many auxiliary functions to create common arrays."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "a = np.zeros((2, 2))  # Create an array of all zeros. The input must be a tuple or a list\n",
    "print(a)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "It also has one for ones."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "b = np.ones(2)\n",
    "print(b)\n",
    "b = np.ones((1,2))   # Create an array of all ones\n",
    "print(b)\n",
    "b = np.ones((2,1))   # Create an array of all ones\n",
    "print(b)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "**Suggestion:** Specify at least two dimensions when creating the arrays. It would ease thing when working with matrix multiplication."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "And one to create an identity matrix."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "d = np.eye(2)        # Create a 2x2 identity matrix\n",
    "print(d)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "e = np.random.random((2,2)) # Create an array filled with random values\n",
    "print(e)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "### Array math\n",
    "Basic mathematical functions operate **elementwise** on arrays, and are available both as operator overloads and as functions in the numpy module.\n",
    "\n",
    "No need to add \".\" as in MATLAB."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "x = np.array([[1,2],[3,4]], dtype=np.float64)\n",
    "y = np.array([[5,6],[7,8]], dtype=np.float64)\n",
    "\n",
    "# Elementwise sum; both produce the array\n",
    "print(f\"x = {x}\\n\")\n",
    "print(f\"y = {y}\\n\")\n",
    "print(f\"x + y = {x + y}\\n\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "print(f\"x = {x}\\n\")\n",
    "print(f\"y = {y}\\n\")\n",
    "print(f\"x*y = {x*y}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "Note that unlike MATLAB, `*` is **elementwise multiplication**, not matrix multiplication. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "We instead use the **`dot` function** to compute inner products of vectors, to multiply a vector by a matrix, and to multiply matrices. \n",
    "\n",
    "`dot` is available both as a function in the numpy module and as an instance method of array objects:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "A = np.array([[1,2],[3,4]])\n",
    "x = np.array([9,10]).reshape(2, 1)\n",
    "\n",
    "# Matrix vector product of vectors; both produce 219\n",
    "print(f\"A: {A},\\n\\n x: {x}\\n\")\n",
    "print(f\"Ax: {A@x}\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "outputs": [],
   "source": [
    "print(f\"x: {x}\")\n",
    "print(f\"x^T: {x.T}\\n\")\n",
    "print(f\"x^Tx: {x.T@x}\") # Inner product"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "print(A)\n",
    "print(f\"\\nAA:{A@A}\") # Matrix multiplication"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Sympy\n",
    "Is a Python library for symbolic mathematics. Similar capabilities to the ones found in Mathematica."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import sympy as sp"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "x = sp.Symbol('x')\n",
    "x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(x+4)*(x - 3)**2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "sp.expand((x+4)*(x - 3)**2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "sp.integrate((x+4)*(x - 3)**2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "sp.isprime(5)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "sp.isprime(8)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "## Z3\n",
    "Is a Python library for symbolic mathematics. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Z3-Solver\n",
    "### Import"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [],
   "source": [
    "from z3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Helper Function"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "metadata": {},
   "outputs": [],
   "source": [
    "def block_model(s, variable_array):\n",
    "    \"\"\"Returns a clause that blocks the \n",
    "        current solution.\"\"\"\n",
    "    m = s.model()\n",
    "    return Or([v != m[v] for v in variable_array])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [],
   "source": [
    "\n",
    "def print_model(s, variable_array):\n",
    "    \"\"\"Prints the current model.\"\"\"\n",
    "    m = s.model()\n",
    "    string_model = [str(m[v]) + ' ' for v in variable_array]\n",
    "    print(''.join(reversed(string_model)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [],
   "source": [
    "def solve_and_print(s, variable_array):\n",
    "    \"\"\"Solves constraints, prints model, and checks uniqueness.\"\"\"\n",
    "    result = s.check()\n",
    "    if result == sat:\n",
    "        print_model(s, x)\n",
    "        if s.check(block_model(s, variable_array)) == unsat:\n",
    "            print('unique solution')\n",
    "        else:\n",
    "            print('solution not unique')\n",
    "            print_model(s, variable_array)\n",
    "    elif result == unsat:\n",
    "        print('unsatisfiable constraints')\n",
    "    else:\n",
    "        print('unable to solve')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### HW4: Z3 Solution"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [],
   "source": [
    "\"\"\" Arrange the numbers from 1 to N so that the sum of\n",
    "every two consecutive numbers is a perfect square.\n",
    "\n",
    "Values of N for which solutions are known to exist:\n",
    "15, 16, 17, 23, 25, 26, 27, 28, ...\n",
    "\n",
    "The unique solution (modulo reversal) for 1 to 17 is\n",
    "16 9 7 2 14 11 5 4 12 13 3 6 10 15 1 8 17\n",
    "\"\"\"\n",
    "\n",
    "## Constraint creation\n",
    "        \n",
    "N = 15 # default value\n",
    "\n",
    "x = Ints([f'x_{i+1}' for i in range(N)])\n",
    "\n",
    "Squares = [k**2 for k in range(2,N) if k**2 < 2*N]\n",
    "\n",
    "areSquares = [Or([x[k] + x[k+1] == s for s in Squares]) for k in range(N-1)]\n",
    "\n",
    "inBounds = [And(0 < v, v <= N) for v in x]\n",
    "\n",
    "symmBreak = x[0] < x[N-1]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "9 7 2 14 11 5 4 12 13 3 6 10 15 1 8 \n",
      "unique solution\n"
     ]
    }
   ],
   "source": [
    "s = Solver()\n",
    "s.add(Distinct(x))\n",
    "s.add(inBounds)\n",
    "s.add(areSquares)\n",
    "s.add(symmBreak)\n",
    "\n",
    "solve_and_print(s, x)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Tip for HW5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<function z3.z3.ForAll(vs, body, weight=1, qid='', skid='', patterns=[], no_patterns=[])>"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ForAll"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<function z3.z3.Exists(vs, body, weight=1, qid='', skid='', patterns=[], no_patterns=[])>"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Exists"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}