{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "limiting-apartment",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "301\n"
     ]
    }
   ],
   "source": [
    "import import_ipynb\n",
    "import helper\n",
    "f = helper.open_file('2021_8.txt')\n",
    "\n",
    "c = 0\n",
    "for l in f:\n",
    "    l = l.strip()\n",
    "    examples, output = l.split(' | ')\n",
    "    digits = output.split()\n",
    "    \n",
    "    for digit in digits:\n",
    "        if len(digit) in (2, 3, 4, 7):\n",
    "            c += 1\n",
    "\n",
    "print(c)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "wicked-sleeping",
   "metadata": {},
   "outputs": [],
   "source": [
    "from z3 import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "invalid-enhancement",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sat\n",
      "[y = -2, x = 1, z = -2]\n"
     ]
    }
   ],
   "source": [
    "x = Real('x')\n",
    "y = Real('y')\n",
    "z = Real('z')\n",
    "\n",
    "s = Solver()\n",
    "s.add(3*x + 2*y - z == 1)\n",
    "s.add(2*x - 2*y + 4*z == -2)\n",
    "s.add(-x + 0.5*y - z == 0)\n",
    "print(s.check())\n",
    "print(s.model())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "robust-bullet",
   "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.9.2"
  },
  "title": "Seven Segment Search"
 },
 "nbformat": 4,
 "nbformat_minor": 5
}