{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "e37078c6",
   "metadata": {},
   "source": [
    "# Constraint *Regular*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5b671e35",
   "metadata": {},
   "source": [
    "A constraint *Regular* enforces the (sequence of) values assigned to the variables of a specified list to belong to a regular language specified by an automaton (i.e., forms a word that can be recognized by a deterministic, or non-deterministic, finite automaton).\n",
    "For such constraints, an automaton is then used to  determine whether or not a given tuple is accepted. \n",
    "This can be an attractive approach when constraint relations can be naturally represented by regular expressions in a known regular language, or when a high level of compression (with respect to a classical table) is possible.  "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c5745e72",
   "metadata": {},
   "source": [
    "Let us recall that a Deterministic Finite Automaton (DFA) is a 5-tuple $(Q,\\Sigma,\\delta,q_0,F)$ where $Q$ is a finite set of states, $\\Sigma$ is a finite set of symbols called the alphabet, $\\delta:Q \\times \\Sigma \\rightarrow Q$  is a transition function,  $q_0 \\in Q$ is the initial state, and $F \\subseteq Q$ is the set of final states."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "be49df3e",
   "metadata": {},
   "source": [
    "Given an input string (a finite sequence of symbols taken from the alphabet $\\Sigma$), the automaton starts in the initial state $q_0$, and for each symbol in sequence of the string, applies the transition function to update the current state. If the last state reached is a final state then the input string is accepted by the automaton. The set of strings that the automaton $A$ accepts constitutes a language, denoted by $L(A)$, which is technically a regular language. When the automaton is non-deterministic, we can find two transitions $(q_i,a,q_j)$ and $(q_i,a,q_k)$ such that $q_j \\neq q_k$."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e0db260a",
   "metadata": {},
   "source": [
    "Interestingly, in  PyCSP$^3$, we can directly write constraints *Regular* in mathematical form, by using tuples, automatas and the operator 'in'. The scope of a constraint is given by a tuple (or list) of variables on the left of the constraining expression and an automaton is given on the right of the constraining expression.\n",
    "Automatas are objects of the class *Automaton* that are built by specifying three named parameters, respectively denoting the initial state, the set of transitions and the set of final states."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "025ab799",
   "metadata": {},
   "source": [
    "These three required named parameters are:\n",
    "- *start* is the name of the initial state (a string)\n",
    "- *transitions* is a set (or list) of 3-tuples\n",
    "- *final* is the set (or list) of the names of final states (strings)\n",
    "\n",
    "Note that the set of states and the alphabet can be inferred from transitions."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dd5b8601",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "f56b76af",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "779e9b55",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 7 variables, each one with {0,1} as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "58f1651e",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=7, dom={0,1})"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8dc4d05d",
   "metadata": {},
   "source": [
    "We can display (the structure of) the array as well as the domain of the first variable."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "9d976ac9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2], x[3], x[4], x[5], x[6]]\n",
      "Domain of any variable:  0 1\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2961453e",
   "metadata": {},
   "source": [
    "Our objective is to impose that the sequence of values assigned to the variables of $x$ belongs to the regular expression $0^*1^20^+10^*$. This corresponds to the following automaton:"
   ]
  },
  {
   "attachments": {
    "automaton.png": {
     "image/png": "iVBORw0KGgoAAAANSUhEUgAAB9gAAAFNCAQAAADhznyhAAAAAmJLR0QA/4ePzL8AAAAJcEhZcwAAAlgAAAJYAJvGvrMAAAAHdElNRQflCwcPGCI8fbe5AABgmklEQVR42u39O4szz/63h35q8cfgB2PolWyMwRjdGIxD6wYnBjvoiRxrdmZ2YGvAkTPNS5DA8QMSzw7tYBQ7kgI7H/kFGEbgwMFOprNtcFIO+lQtdUstqburD9dVrHVr5qeRqrvr9KnvoYwVAAAAAAAAAPSNf/iuAAAAAAAAAABcg2AHAAAAAAAA6CEIdgAAAAAAAIAegmAHAAAAAJgQJjSB7zoAQD0MSecAAAAAAMaOWSjUXPPsF2cdddLeRr5rBgDVINgBAAAAAEaNWWqlmSQp0kmSNMt+3mmDaAfoKwh2AAAAAIDRYubaJnb1ozb26Px+qaUkKdKH3fuuJwCUgWAHAAAAABgpZqm1AlWIckfMb+yn77oCdIkJdRqCbwmCHQAAAABglJiltpKkSG/2VPqOQIdEsu/sh+/6ArTN8HI5INgBAAAAAEaImes7efle7fJuZvpWnDUeKzuMmmHmckCwAwAAAACMDhPoOxEje/t+852pHV56y2PcAcbEcHM5INhh4gwlegUAAADgEcxaq+TlH3u+896fRNqf7R/f9QZoniHnckCwwyQZXvQKAAAAQH3MTD/Jy6N9u/vu3Mb+aTe+6w7QLMPO5YBgh8kxzOgVAAAAgPqYbeLmK33Y3d135/I+sv/0XXeAJhl6LgcEO0yK4UavAAAAANTFBPrNfrjrEC9J5jvzPKwh8AGGwvBzOfzDdwUAusMsE2eXSO+20BHtyX7or06SAn2Zte+aAgAAALzAMnsV1ZHrkvJ10cJ35QEaJPWsle7Yze1OaV/Zqkcg2GEymKW2SbKJtzIbuj3pLXGRX5ledVMAAACAh8hF9+nhvw1N4Lv6AM1gZlnqxWONras0f8PMrO6+tzMQ7DARzDzbK/uwFVOXjfSuOIJ9iZUdAAAAhomZOYl16wp21wUYGzuMhVx41wl5PZb8nXcQ7DAJTKCv5OX+VoS6PWfOMisT+q41AAAAwBO8uoZhDQSjwAROcEiNqHR7zja4ArO8//5uQLDDNBh89AoAAABATebO67qn37juwgh2GAejyOWAYIcJMIboFQAAAICauIK9pkt8YYUUmFm9vwLoNaPI5YBghykwgugVAAAAgJrMe/AJAJ4ZSy4HBDuMnnFErwAAAADUwTQhthHsMHxGkssBwQ7jZxTRKwAAAAC1aMKRtyfOwAAvMJJcDgh2GD+jiF4BAAAAqMWzMsP1QySGHYbPSHI5INhh5IwlegUAAAAAAGozklwOCHYYOyOJXgEAAAB4HFsjf08JvRAqAM8znlwOCHYYOyOJXgEAAACoRRMig5BAGDqjyeWAYIexM5LoFQAAAAAAqMlocjkg2GHsjCR6BQAAAAAApgaCHUbNeKJXAAAAAADgGYacywHBDuNmNNErAAAAAABQk9HkckCww7gZTfQKAAAAAABMDQQ7AAAAAAAAQA9BsMOEGHL0CgAAAAAATA0EO4yb0USvAAAAAADA1ECwAwAAAACMFIPhAWDQINgBAAAAAMYKoX0AgwbBDgAAAAAwHk4NfEbk+yIAIAbBDgAAAAAAri2+CdEPAA2AYAcAAAAAAKLdYbQMOZcDgh0AAAAAYDw8d4xtkbPviwBolAHnckCwAwAAAACMhybiz4lhh6EzmlwOCHYAAAAAgNFgi0LlOcsiMewwVXqXywHBDhNiyNErAAAAADVxZUbN1Y8JCz/iEg9TpXd6AcEOU2LA0SsAAAAANXnVLhjZXlgWAV5gNLkcEOwwbkYTvQIAAABQE3f9M6v5N+77mpA6AH4ZTS4HBDtAGb2LXgEAAACoyd55XdfBF8EOo2I8uRwQ7ABl9C56BQAAAKAeNnIke12h4gr2fc2/AegzI8nlgGCHcTOa6BUAAACA2uQroMDUc4rPhf3R9sIRGOBFRpLLAcEO42Y00SsAAAAAtdk765fw/ttN4FjYsa/DOBhJLgcEO4ya8USvAAAAANTFRtplP9RZ/yyyV2e7q/F+gP4zklwOCHYYOyOJXgEAAAB4gE1mY1+a+yughfN3AKNgLLkcEOwwdkYSvQIAAABQHxs50nt1+71mlrnNH7Gvw4gYRS4HBDuMnZFErwAAAAA8gt1kq5jlHbGyTf6N9OG71gANMopcDgh2GDsjiV4BAAAAeJD3RK4EmSQvwawyKfNpCQSEETGOXA4Idhg5Y4leAQAAAHgMG+ktkeyhqZDsZql18vKjPxIFoCFGkMsBwQ7jZxTRKwAAAACPYk/6m4QHLs3hch1kArNObO8Rch3GyBhyOSDYYfyMInoFAAAA4HHs2f5NJEuoH7M1i9jOaEKz1k8iYY762yeBAtAcw8/lYKzvGgC0jllnO2o7e7cDmmXWXc/2j++6AwAAALyKmWmlRWk2n6M2low9MGJMoJ+k7R/tW+W7Vn0NDkGwwwRwuqn0z3tO7uaQ2eF71l0BAAAAnseECp3Av5PO2hP8B+PHzHVItECF8c4x2PVu/Y9gh0ng7Jlt7OfNd870k7y8sQcHAAAAAADDwMz0lWxWHfVRPA3BBFol3riRPvsm1xHsMBkyu3mkv7eOLKn7PgAAAAAAGApukKyOcWppEyrUMnWYv5Ty/QDBDhNh6NErAAAAAADwPMPM5YBgh8kw7OgVAAAAAAB4laHlckCww4QYcvQKAAAAAABMDQQ7TIyhRq8AAAAAAMDUQLDD5Bhm9AoAAAAAAEwNBDtMlKFFrwAAAAAAwNRAsAMAAAAAAAD0kH/4rgAAAAAAAAAAXINgBwAAAAAAAOghCHYAAAAAAACAHoJgBwAAAAAAAOghCHYAAAAAAACAHoJgBwAAAAAAAOghCHYAAAAAAACAHoJgBwAAAAAAAOghCHYAAAAAAACAHoJgBwAAAAAAAOghCHYAAAAAAACAHoJgBwAAAAAAAOghCHYAAAAAAACAHvIvvisAAAAAAADdYQLNnR9PNvJdIwCowljfNQAAAAAAgE4wC4VaKLj49Vl77ezZd+0A4BIEOwAAAADA6KmQ6i5H7e3Odz0BwAXBDgAAAAAwasxay5tSPSfSDls7QH9AsAMAAAAAjBYT6Eth4Vdn7XXUPJPwwYXlPdKbPfmuN0CbmEWJv8lRu/5ldECwAwAAAACMFDPXl2bZj2fttb8W4ybQQstCKroPnONhnNwJDtnpaPe+61ioL4IdAAAAAGCMmJXW2Q97bW7bzc1cC8d1fmM/fdcfoEnMTMtawSG9SsKIYAcAAAAAGB0m0FaL5IdIn/Us5maubWZp3+mzfw7CAM9hllpfiPWzXFEeXvxBT7xMEOwAAAAAACPDzPSVCe+TPurHpBdi3k96Q7LD8DGB1lo6vygJDjEzLbR0Akiknf3wXXMEO0yakngtSTpqrz2TEwAAAAwX8/2KndxsM3Fzsn99XwvAaxS2ryLtyvI4ZO8N5aajO+rdtypAsMMkMYHidBNVRNprR35UAAAAGCJmrVXy8tNunvqEPPqdWHYYNGahbSbA9/q4L8AL4SQP+ae0Un8EO0wNE2h9IzOky1m75yY5AAAAAF+Yhb6Sl2/22MCn/MWIAUPF2bx6aPvK+btI78/3owauAMEO08LMdbgQ6/tCuon5RcKJHjjCAAAAANTFzPSdrHVetI1nkgW3eBgor8hus9Q2++GFra+XrwHBDlOicLiJdNJe+8sjG8xMSy2chBPeHWEAAAAA6pJFrx/t24ufFOg7WRHhFg8DxIQ6JC+fMsE5hr6z/voy4SHYYTJcHG6yu326olkozNKtRPqwe9/1BwAAALhHZlGM9Od1geEIHtziYWCYQD+J3H4627uTrs7bphWCHSZC4VTRmjbzwmmNT6ZsAQAAAOiKZqLXC5+IWzwMFHNIAl1fartmru/kpSe3+H/4+FKArjELHZzDTd7q7RHbnd6U7k2vzbbO3wAAAAD4wQRZzO2mMWmxSXL9zM3qxU8C6BCzTuR6pPdXPseelBrttqZO0urmrwQLO4wfJ/nKw5ZyEzhSHys7AAAA9JZ2rOGZW3xk/+n7CgHq4QRzvL8e2JrlhfDiFo9ghwmQdbKz3h+PvzKB1kk0e6S/t+LeAQAAAPxhfpIUcX+aXa+YbbISakD6ALSPE73eiMT26xaPSzyMHrNO5Hr0XLoUG9kPxdNTINziAQAAoJeYZSLXd42bF3bJv+FLnwLQFV+JXM/d2V/CcYtfv/RBT4GFHUZOMw4xzj4dbvEAAADQQ7IUWy3kc09s9zjFwwDI7OFR3bxVtT419dj9sLsXP+pBsLDDqDFBlit184oTl42UHgaxMrPnPwcAAACgDcw8kevHVo5fS3wNzfLFzwFon7SVbhrtC6kW6NzPBMEO4yZziHk1fsXucYsHAACA3pKKlHaizHGKh4FggqQvnJv1irUnxfJ/0XWueAQ7jJimjnNI+EiOeAs51gQAAAD6hCNSWnHXtWdfYgXgQdJ1evNbV+knLrq9IAQ7jBYzyzrsRxPJV1y3eN/XBgAAAODQnkhJ8SRWAB4kbaHNZ51CsAM0TB6/0tDklbvFGyYrAAAA6A/tiZSUdDWFUzz0GOeshKjpz7ZnxUe6hd1mtEKww3hJz05vcupKP4vJCgAAAHpCmyIlBad4GATp1lU7mdy92NgR7DBSzDJJN7dvcuqyJ8XO9UsmKwAAAOgJqSGh3eOmsLFDz2n5rAQEO0CjZA7xDX9uOhXiFA8AAAD9ID4f+tSSSEk5Fr4NoH+0e1aCbJR88rxLp3gEO4wSEyaTybGJdHMF2F0GAACAHmGCxCG+XbmulrcDAF6k7bMSJOXbVsuXPuUhEOwwTlqLXyGCCwAAAHpFakRoX1DHYYZY2KGfpOv/9s5KkPbd9wIEO4wQM8v219rosOlndrizBgAAAFBBKh3aF+zxN3SaIRugNmnLbDGXg42SXtCh4Q7BDmMkldLtdFei2AEAAKA/JIK9A5f1ONAQwQ79JO4JUeMBsUWwsAM0QHqgWyuC3U+6CQAAAIBSkrw9HXxTcvIOKyDoJUmG+Ja/JdkO6C44FsEOo8OEbRzoViAdCJiuAAAAwCtmlqx7ukgJl1ouWQFB7zBpLod27evZtlV3NnYEO4yP9s8iTQcCMsUDAACAX7pLOYdghz6TCui2LexpT+usFyDYYXy0Hsllu3A6AwAAALhPKhsQ7DBtuuoJnfcCBDuMjy4iuTjWBAAAAPpAN4m2JEnZd3C0LfSP2Nfk1FpIbEL3vQDBDiOjo0iuzg90AAAAACihm0RbKeSJh15igqRVdudpgoUd4Em6ieTCwg4AAADe6SzRVgqCHfpJuirvoicg2AFeopv4lc4PdAAAAAC4Il33dJtfh/UP9I1066qLnoBgB3iJbiK5Oj/QAQAAAOAKP7buLtyOAR6h9aTTDokOMB31PgQ7jI0k4UTL39L5gQ4AAAAAlSChYdp0kXT6EgQ7wOOY1OI9ugMdAAAAAKpoOzM2QM/pIum0JxDsMC46il/hWBMAAACYIOHrHwEwEjraHkCww7joJuWcRJZUAAAAmCrY86FX+EkD3ZVfC4IdxkXsEn/uoAN1dXwKAAAAQBV+0t+yCoJ+Meo00Ah2GBeJYO/gm3AJAwAAgH6AxRtAGulWEoIdxkh3nZUJEgAAAHwzylRbAA/TjQbo2J6PYIcx0p2MHuU+HgAAAMA1ZtSOxwAP0ZkKQLADAAAAAMB9OB0HIAXBDgAAAAAAN/Fj8275+FyABxm17weCHUZEd45ahuPcAAAAwD/YvAFG3g8Q7DAmuuusCHYAAADoCySdA5Bku/H96PisKAQ7jJHuHLWYIAEAAGAqjNrxGOAhOktyjWAHeAWOdQMAAICpkHoYYrAAIOkcAAAAAAD0iFiwny0GC+gXHcawm87j5RHsMCa660CjTm0BAAAAg6Kr3Dpx7G5nlkWAmnSZXSoNDMHCDvAE3UVWEcMFAAAA/olFQ8OGBBOakrRaBod4gDzlHIId4AW62/lljxkAAAD80c5K5KSvkiNsO7csAtSklTZpyrPBJ9tjHWWkF4IdRoltfyKZdfZNAAAAALdp+JgpGynS11WsbirYsbBD32gnq8LSlLnaJ5kcurs4BDvAM8RTVnfHxwEAAABc05Z4Pmmu9cXvUnMFgh16iml26+pcsm2Vbo912AsQ7DBCmsveaGZmVfofOt9bAwAAAKii8czVZ0lLsyz8Ll79INehf7TTKs/X21bGQ2AIgh3GSGMp4exZq+u9uuw3HGoCAAAAfaDpdLixF+HWuJ8bv0awQ/9I1+TNblwdJS0vjHceUi8i2GFMtOGifipxhkm7Ki7xAAAA4JO21iKpHDmkqyDMFdBj0lbZ6MaVPSuStC7ZtsLCDvAiTZ7FeFKgQ8Xns8cMAAAAfaDhc6htlB0Y93XxDSVbBGZhvi7c5wE6pLW8CvHnHhzjnYdMDgh2GBPp7lqzgl2am23hd/HeWmTZYwYAAACftLH2iUkFSWjWhW8oWBbNzKzNj750sjvftwKgYZf4tBe4xrsbiadN0M62FYIdRkQre13xZxbTrhDDBQAAAD2gRTtf/skrs1SaGzvKj7Q1C/OlH600085ufN8JmDhxu2x64yrtBXOTJp+rSDxt5marn3Yu7V/a+VgArzTYWe3ZRAokrc0pnhRNkOzeIdgBAACgH7RnYZektfnfXcuimWmpRfadO/vh+/Jh8pxb6APFbauz3ZVlcjCBFlpqLumzHT8TLOwwLlLHlTY+M00+dyPZBDFcAAAA0CltrH0kWdfpN9D/N/02x66efv+n71sAkNDsOexp2rmYtZlnn5/0jsSuvtVcas/PBMEO46KNqPJ0b22WpF1Ju2p5DFdEDBcAAAB0RnsZdVwbeyrP/zt9aVF4zxs5faAHtJt2TpICbfWfxS/t0QRmab71rWWyWdainwmCHcZIs7treUeN066k2SGznedCDBdOYQAAANA1DVsWJZVLoP+g8FOkd+Q69AnTTtq5mLn+S0nS0bGrp+9q0c+EGHYYF6cWJizXJWxl0m+I49mLMVwn5DoAAAB0Shtrn5h7J01HerMdnkYNUIN5eQb3p7nctvq/9W9d9biW/UywsMMoMU2mnYsKE9a/SRxfjiUxXG++rxsAAACmSZNrn4R7TsbvXZ5FDXCTZmV6zmUb/7eu3hHpo10/EwQ7jIt2TiN1u+q/m/z7X1/EcEXEcAEAAEDntHYSu70tgT5sWxIJ4Hka7gf2fMfTJNJb2xtXCHYYF+10mLKO+u8VfkKuAwAAgA/StU9XUewxLR1gBfAkrW1c3VEXH+37mSDYYZzMX/8Ih/s7yK3vrQEAAABck9m52z2FukhrB1gBPEe2Em/8gMObFvYPu2//2hDsMC7SLtXGSezVdLC3BgAAAFBKvAppQ7CXS5U9SXahh8SttVmjnXTLcLfpxs8EwQ6jop1cpRdp5y75wCkMAAAAvBEL9uaFSrlUOQm5Dn2krX5Q7WfS4lFuLgh2GBtxBEvTnbXagr5DrgMAAIBHErOCaTyKvcSDsOUDrACepqV+UGG469DPBMEOY6Od3bUqC/sOpzAAAADwSiqr27ext36AFcDTtJfNoWzjqkMFgGCHsRF3qaDh00jLo1dO6sgVBgAAAKCcztLOdXCAFcDTpG2z+X5wabjr2M8EwQ5jI+1Sze4yn0p/h1MYAAAA+KetdFtFqUKSXegxmet622nnOvczQbDD2GjFLcxGV5I90jtyHQAAAHpAe2nn8vVPJwdYAbxA3Fobz+Xg288EwQ4jw7YVx1XsmpHe2slIPz3MzDR/YibAQKD9w/QwIa2+BdpPO9fRAVZTg1mgUdJ+0LAKKKSd8+BngmCH8RG7rbSbdu4dp7BmMKG+9dv0wAowDGj/MB3MwmzNt7HG6qBfY82P2ZolUqUxUpfdttLOdXaA1bRgFmiY9tIvpj3Mi5/Jv3T/lQAtc1IoKTCzRm3grkD/sMenPwcczEprSRJLNpggtH+YCmapVZIGKg0wm2mmpaS12WlDgFkDtJduSzop4kycNmAWaJy208558jPBwg7jI5XpjXZWR6J/4hTWBCY0h2SiApgctH+YCmZuvrXVTNJRb/af9s2+2Tf7R3+1kxRopR+z8F3L4ZO57LYh2I9dHmA1FZgF2sCeFW//NW9hP8mjnwmCHcZHurvWdBxX/Lk7u/F9gcPHLMxBhxaSggAMANo/TAez1EFzxYla31zvNHuyH/qrk6RAXwbh8jptpduSPeID0SzMAi3SUj+wRx39+ZngEg+jw55M/KLpXeaT5trhFPYKJtRcMy1w/oIpQvuHqWGW2kqqzKpsT+YtEfQrEzC/vkiWbossO32FWaAD4sDYFvqBffN3UQh2GCNHhWoj7dxJpFx5ArPUQvOL6emsgAkLpgDtH6aKmSdy/UZWZRuZd30rkLQ0EWnNXuKolSQpFIK9VzALdEoexT6ifoBLPIyRJKVNw9ln93rDKewpZgqdaSnSTu/2z5gGUoAb0P5hkphAX8nL/a2syvacbYWvmj+SbFK0lx8bXoNZoEtG2Q+wsMMYSWX1XA1mc+fc9ac566h4CD3rhKseTAzaP0yTVRaYdsdubncmfe9Wf3xXe7jYyMT+hTdT+JVsipxZ37QMs0CH2LOJFOhmFLuZl3k39PkEKAQ7jJE87VyPO990sDuRVx8mC+0fpoiZJe7Z0rGGHNwkzvMzsyKx6wuk0bthLj3MTGkJqiSMkU7JgXvHfsuWYcIs0DF7LSXN8+OdTaB50gdmmleFIpj42MlI57j0aSMLwQ4jxB5bSjsHAAAA91llr/Y13n10/g7B/jxZFLs5a6FQQW234Llii+Qqky1nHW2dZwfQNzKznYkUav6Ac3xhU8so7gfa+w+INdZ3DQBawCSHZVjjuyZQhXEPNHljR78bzLzSxnJSxFPoDto/jBkT6Df74U8dO5X5zhbVHxZr5NOYb/0f+lf6j/UfNvSB+37IlTHCLNAWZqafhj9yr5P2Pi3uWNhhnJS4hV1yGcfFYAnjwwSaK/7fDTew7N2SdFSkc2xf6ZM7GEAzmNmF7xXtvA2W2auo5v09ZoJ9gfvwc5iFQs1uWBMdt3eH1F2+fIZYaKGtOeroV64A1MPMtKgK/UiXQ6k7SZG8e0TX+QAXWmhtTjpq7ycHAYIdxkl+uEkxjisWLqU2xj7HrgA8SjJpPZ5z2XUHO2vva3ICaAqTOgbHMYzX/72wUqO9N0Ke9uzx+xmaAIvuI5ggGe2vBffxsTWNCaXkWNxiXwkV+pUrAPcwcy0UXm5YzbTIkjjcxokKURoVEmnvDmFzzbUyZ+117NrIh0s8jBTzq0DSUR+K95yfiWc/6ezbCWa84AzWFuWT1gtE2hPL2DS0/3YxgUKFmj2xZRWv1E460eafpeCQuql3troJdch+wCm+JibQUvOSrPCR9jrq+MrGR+VM4kWujBFmgaYwoUItLtf5TS2FzrE//OWvO14ZIdhhpJi1/iP9K/0n+g8a+DB2lVuAqap5zELz60kr4ayzTqqIVc9i2+c3khQRy9ggtP+2MDPFi7fXaUD0TBOzTHK+S88J9r19930N/ccEWml5ZVU/a9/kZpOZaVG6JXDUhnHrNZgFmsDMtL3cmF0k+7VNkkwHupgOOusHCHYYIWahUIsb8bqnsgAV3RYr7Co3DFNVc5ggWVJdt/m9Tjo96uabHIBS/onEMjYC7b95zEwLLW6M4amP4yXV8bsxsWynzdfGbJ0Y9s96x7QVrPKR/afva+g7ZqXVRZtt0bRQ4XS/1yf94nmYBV7FzLRyxhpVL4WaI5bthWZ/1Ef7/QDBDiPiZhzXOYnkOt2zltw5sxSbS0MwVTXD5YSVECXC+sV2Wu5oJumkT57ZK9D+m8TMtShtp6lfSa3YdCfWvUy+n7Rnq6oeTsb3B1p3YUFaK7P8VDFLrQqtvbNtVHNtutxpw7N6DmaBVyh6mFTFhlyT7tueLvZubyY6ueKkvfaubG+9HyDYYSSYZWleyBfldbIFUDYG7HUkyu4VmKpexwRaX4n1s45Nx1VVxDLiEvkCtP9mMHMtSw0qL8rrG1sAe23YsL1NYWn5nGB/J4NAOSbUqrDW2XTfHk2ordM3Iu3oE8/ALPA8Zu2K9bLYEJeTjqrI/l5KmqN6ficJykYbV/a32xcthTL4oqV+rn75o7UWjX3DQlv9Xv36oND3tQ+36OD8wH18/P4FWl+0yR+tNW/xG2da6evil1vNfN+JYRbafwP3cKZtya+/tGyqVWqmlb6vfv2rtQLfV9/fonnhx9qtu/DD2vdV9LFoVhg3vI6/F+uuX618353hFWaBJ+9boe0t7Y+t5ssu7SudJLBLu7W/lZ//a9fWmQx+2xu5sLDDwLnabW4xjqvU5nLUJ+nonoG95VcwS62dDeVIm66cdU2gxYU3y06fWFcehfb/GibQKjl9J6W1cKXSNHaRNvVis6dHIX3csxb2nf3wfR394ir4ybuH01XSu7M2+B0+ArPA45hQ69zbr+jq4VKRIi7nOpdV+eHsCbfS2J210a7wYyv9wPc+CYXyfLnabT5o1f5+s+ZXNhesjM/cR/aWn71ziwvLhgdrXx/qMOxC+3/p7hW9Sxr1p6r8zuDK0+pHS993oo9F68KP9S3sbp84+L6KPhUFF/f0uy9jxlXN8Dt85O4xCzx2v+buHQvtodTm/WPXtmQ6+NVBX1prqfDWil2BQi201laHa7/auV3b74pvLTzAFnqo99tPoTxXrpwhO54mFF6IdgTLo3eQqeqZuxZeuUR6a3daFqazX8TLQ3eP9v/snbt0xe3UeRqBUuMeIdibvZ/zwmqjd9tEV6sxwhnq3jlmgUfulrPimNlthXt6SVTgj9bP3l3Ntb4OiprZVakb/qEo2hvuB94fAIXyeLmK3v3xM9T5XTgOvTBVPXzHehS/mNTouie2buccS6H9P3XXihulnjw7SraL8bFy709BsD/wd26f+PV9FX0pCp0xtrerjKLt0+dG8pAKs8AD9yobVYJKsX7V6L6byetTnstkWRrZ/uVGzDfaD7w/Agrl0XIlEbzuNverNkMqTFUP3q9l4cfe2PUUXIiXL5Zqte4b7f/ROxb2acOqX7XpVynemfb/bsxFK+eHnvvxFbbTvvtd134UZoGa9ynI092uS2Xy9lKsfzUfIKtAy2La3aCiNs7WQYP9wPtjoFAeKZr3z6Z9ZWX8ZuFW674xVT1yt1xR7Mmj5EbtihZHekCde0b7f+x+XTqi96CNXQVGsV0b3xcEe1N3Mh9Xf9s8AWTKNfZ6t5gF6tylWTrOBvarVKwXJoMvLdvdLNLCXe+U2/u/c8neWD/w/iAolPrlIma2R7vNF4KFiarOPWOqqnunAude9daHo2BxpAfcv1+0//r3KigI4954l1hdBUZtfdenDwXB3shdDIZpry74BPR0tupLYRaocY/m6bp/VpLu7SJq/NDVyqO45i+LqP/No+kbyu/j/VFQKHVLwcLSQ/fDiwhjJqp794upqt59cr1Keu5uXnDbpwfcvle0/7p3yu0BvdywKvhYHfrdRzu5Hwj21++h2+oHFhGuhdMfeuAF2d/CLHD3DmVrivmV83n7ednv1O1Ozvpf60xWDfQD7w+DQqlTCnGyP/213hXSw2BruX2vmKrq3KWBLX0KPWAA9fV4p2j/9e7TIHqAG2PZ5xmqo7uBYH/1Dg6i1d+ov5vXvufbzF7vE7PA7fuTrfuXV2K9sHPrbSO3GBYVXuWOdzrvy/3A++OgUO6XPIJFvXcNK0xU2Fpu3Smmqvv3KHcuHMyhafSAmveJ9l/nLg2oBzg+YL/TPi0Bwf7i/XNbUs9bfeU1uIFcZDWpukvMAtX3xmlBlw7nBzfFnPdcVsWwqMu6frkJ6F7qB/8QQM8xc31rnvyws39t5LtGt7AnvWmf/BDqYOYvfRxMFhOYrdbJD5He7M53jepBD4BmGFoPsJ/6UDw7BfoyK9/1gSFiArNV2nbO/W/1VdjIvimt+1zfJvRdIxgSZq6DQinW7cvCf9vpLRloFWmjP/bTb13tzv7RJq3Sh4rVWeigWfzyxX6AYIeeY5b6VpD88GE/fNfnPjay79okP8x1YKKCxzHuLHXSH3vyXaP60APgdYbYA6yzktTabE3w0sfBFHFb/d8htPpq7IfSFVugg1n4rg8MBTPXITbTZbo9I29U2uuv/eyHCc9+6k+66tk400B8DZnNMXhlPYRgh15j1tomLwdgYcmxn4WJClsLPISZ62c4XiVl0APgFYbaA+xJf5SKrKUOSHZ4BLMdYquvxu70N9MuW7ytoA4m0DY204Wpbk+I9Ddz29CHfbdn33XNsZH9TJX6UW9y99oCfedeAl/P9gMEO/QWE5ivzDXspDd79F2jRyhMVGuzfenDYFKYuQ6ZV8nnELxKyrjoAUh2qI1ZDrcH2EiuK/APIoVNi7qYVbaqH1irr8ae9DfRLoHwOYE6fMUq3Z0GJClvSor0t48GPJsp9ZPeVJQs29T6+HQ/QLBDTzGBDkpdqI56G55rWNHWYr581weGgQn0lcxSkd7t5sWP84izVJPWOERCPcwyta8MswfYyOZhjAFZHDT166+JCbOMDZvhtfpq7DnzEJ6LdRDcwaxjH/hQRTvXXm9KDOo9DhaxmVKP9KZiN16m+3FzPWXCQ7BDX1ln0/zGvg3TNaxga1mY9UsfBlMhzVAS6c3uX/wsz9iz0wNwiIQamHwxcx5uD7AbvTsJ6KZmV2xiMT3IOf95TC5md76TaDWNjTLJHuJtCLcwy9iv9nJvJx9Qtddbn1zhL7GRzZR6HhkYs03j8Z/SAwh26CWOa9jHkCcvG9mPbJNtZZYvfRhMgCyGMRqiV8k1NtJn5hA5PeECD2ICHZKXPbai1MHuM5Eyy64JbuNu6Q342T9OHrWrkwa84qnC5le1ZB0EVaTbtXl3kKTIzby+se/9N+DlOXzcyEAp8/Z/Sg8g2KGHmEXmGvbZxziVx7CfmY1xjY0RblGIYRzJgtWxrsxwiIRbmCALWjxpoH5VOfaUuwJjV6zFdDf0vpyN2oG3+3LsLjNd4GsFpZhsa3Nb2LvL3PSi4Rjw8hw+p4Jkd7YiHu4HCHboHY5L5G4ckVz2I8k+EZA1GKopxDAOfqMqB4dIqMk6ky0fY5At9pR5RC4nlXaxiQSxPXZ6bRqTecqOVa5Lkv1UGuByMDPftYG+kWfvWctNePORJ5ob0ElRbg6fs96c3zsB7A/2AwQ79Awn5dZpLHlSJb0nyw8kO1Qw6hhGHCLhLmad+Ze8j8a/ZJ/ZFaeUdrEJ0Tla4XqJWToBgCNp9xV8EB4FlazT3PDu3uYmta6f9GdovcOe9RZvUp0KseyZC/GD/QDBDn3DSbnluyrNYaMsY8ZcJJ+DK0Yfw+g6RIYvfRSMEpOv0z6HdYTnbZyQqMm4Al8srJ+76oEtzp/F8SgclV9VGYV1EL5W4JBu1xYbxj5dDA00VMRG6SbVrpAxfpXni39ADyDYoVcUUm4NsHtWM1nnSKjH+GMYc4fILxwioYjJFy4jCYRy+JzgOdSu3K55zRcbeZNwic+jdrUfm19VGfas9+Ql5+ZARrpdW8zP6dilB7sqyjep8gWQ5ETpL+v3AwQ79AjHNWw0KbdybLZZOCnnSKjBNGIYcYiEckYaCJXg5HCYzjnUr87f0fhWAKVk7V6ja/fl2GN2pSvWQSBJZhZv1+bTgCTl7hjDDhWxWQj7R2FYTPOr1u8HCHboDSYcu2uY3UzPORLuM5UYRhwioYI0EOo8pkCoHJsHeE0l7aI7jtX1p3HfN6KgiGrMKvOrGsBRVU1hd/m5Ob7rAr1gmyabc5fFaeKn4euB1L820kchX3wm2Wv2AwQ79AQzG2/KLQfOpIYLzGzsG1U5+V6zFiSfgxgnEGq0sqUQEjWFlu96f9ad6SYm2E2QZW14t5MIAEjJzs2Z4RYPJoz9C/Oco5KUNpFxhIqkOXxOWUSIJM3TAWBWb05AsENfGHXKrZTCmdREsoOkrB2MYmK6hyNc1mxZgWTCMQdC5ThpFyfQ8m3kSPa63mSuYN/X/Jshs0rWPLsxJVmsSb59Nfq+AHdYSVJQkOu7PDf8SEJF0hw+x8IFrdJBr9acgGCHXpDusY3ZxhLjSPYVqbfAzJJ5KhrLxHQPu0sW4wFbVqB8w2r8/iWfk2r5uQgNas50ubA/jnsVIEkmVyhjS7JYA3tOFNk0+gJUYhbx2n/lOOJkonZceiDLF+9OdIl7Za1+gGCHfpAf6DN61zB7yvorUxWk7vC7EU1M98jPZMe6MnHMMtmqPU3BvyQLYZzCZu3eCdescZCjCRwL+xTs6+tEoWzGv+YpJd2mmEJfgGrWUtHhNMrdxkcVKmKzEPYPZzcztVXWWQ0h2KEHOIu2kdtYEjbJUmbJidTTJvMsOU9CriRgXYGMbKvWd0W6wEbT2ax1rrWeU3yeKfk8/nWA41k1Qfu6JNlzLtl91wV8YZbxNp3bBD7z3PAjCxWxWQh78Ux2SbVWQwh26AOTWrRJNsqulKlq2mTuwL4r0jGfE7I0QiUmDeE7jm1pVsmUNms3mY29ji/Nwvm78ZMmW5uSZ9UleV9gFpgkJoj7wdyJX09387Uf47adPcaj27FgY0+u/u5qCMEO3pngok12l5xYEU5g2VaHSU7Yk/MsyZiSpbEW02z/wfQ2rKa0WWtd6/GdqzWzzG3+OP7R0ITJ9sR5Oi3/GmcWmMZRh/eY3iywSo9zy8k6xFjNd5vULd69DZcvykGwg2emuGgrXO1EpyoTFOIapzdVSZPzLCkwJUtjCbR/TTRL9pQ2a+0mMyTds6Km8+A0km/miRana1+XZD+n0xfKmPYskKZdDJ2bcEz3cEab2SHdsj07EUNZBP+91ZClULwWrZMXW9816fzKD8mLpe+aeLj2mb4Kv/id3l3QKnlx8F0TT9e/nO710/6tFOg3eTnzXZeOrzxt+T++a9LpU77Rz7OxcBKzoRbTef537wWzQF4mNgtoG7842JwwvROB79q1euU/srIz57p/bXLBN/uBsb63G2DSmEA/iZXlz1h31CqvPdRBknS2f3zXpeUrnTkhSjMFmlXsJR8l5Scxjzr1kNPy36ZkXyzcg5+kHYz8DtD+S+/KNrkrmyklXEyu/ZAYlT7G/Ywlycx1yDwpSq3nZpnZ1ydwP6Yz7tXDfCcpCUf+7JkFru7HjyQtHSfTo97iFyOfE8xCX5K0dnzgN6mj5a1RwfdOA2XaJd1j09p3TbxcfWpjH/nVK3zqz0a95z5dzxLnHqTWlW/fNWn5Omn/1/dklrwYuS3lTouYhI1VM30nLw+X3hQKspFwIvbFKduUS+/HRPoCs8DF/UjW/j+OnTkZHH7GPyfEa//A/l7b2G/0Ayzs4JF0j02R/kwxlmsq15/4EpxU/xpnmulo33zXvLU7MmHPksJ9mISlkfZfck++krRbI7elVF5/2vIncv0mNybtdNTRRsmhlstkHDzqYxojIfb1S5gFKhjxLGDm+paklZNwbpemrxh1O0iuP/GvdW3s968fwQ4emfqibdpuoVPG/3NPkpuEkvb29NpnvVSLiYSFgEv+3PV3zFuVN+7ARDZrC1e80kJlx7sdtZmKeE2dYbW3777rUqO2cwWS5gq0a287JRsNRipO4Zp4Ay+3W0iR/sYZCCeyFkjVz48TGfEnvgOVYwOCHbyRLVkmu2iTzEzf8Yhlje+6QHeYXwXqeLFuQi00U7z8cvG6TMqsK3/9bRtA12RbtROwpVTeg3TT7tNO6HwUEypMYpYl6aSz9lOa/TNPg56Od2ahuebSVYR1qxsM2Szwzym1hSkTZy5w49ezGO53u/ddu07uQEkMf3oPqtTAv/iuNEyYRfLvhI82sWeziydws5jGMAWZ3ULaddryv0qtW26CGx9skqXawnM9oEviZz7ahEq12CSCfTGlA03tUROxpVcQr3qifsp1SVsvs8QxmwWmPCJMBjOLN+3yM8yidBA8TmUdbM9mp6W00zLbwUzvR5Ua4Bx28Ecq2CfSQStIr36S55BOlLTld7toq3Jp9LqAtsckpm/x4gfBYDCpY/SkR357Tq5/boIXPwoGgpknduv+tvyqLeR2ZwlWQdMime3zx71LG96ENi+1iS8636NKh4eqftCJYDcHY83oOuI4r6o7TJBsK03KIe4ae0qEFIJlOqRWlk6XbfavNdZYo78qHq7k29YT34WZmb/4OTAU0nmzv7KlG1IRxNg/FdIn3VsvA/snmyXc7CotewTYczILsaKeBov4//KdyqRDHKeSy0KS7DnW6u4lLwr/XIKFHXzhx8rYR+Jla8D2zzQwM79WFnuyO6fXnbxvmKXzFe1/KsRj/7m3bsFdQcufGvGT7nir9hnsqZBZoX0ZFX9DYNi8Gj2psc51iE8Fu++6dcxRks7Ocixp/kG5+aIbwT57/SN6yDivqjuwsqSwbJsWfbCy5NOB/ykSO+OkyDI4TH7kz+yKC5zip0AauduDMfdR2t9awyl+Olw5xO+vXkyDNCAwv+wsI3DpagjBzlX5Im6Qp2mcvXoLongnhnfBXvDl8G7ltFEWy8uYOgXwrcpBpkwJ7yP/IxRmidZrTGjghAglJ15bWfOaohrYZ/+XcMspvgPBPs7IxHFeVXcYEs65EMU7GTIri8/cDZ0uxWqAjX1KeMng0FPwrpoSw/IqdDyWOwleSUMDWQWNnUX2fwnJMDiMftEsiVN8vlORdLtSNdCFhX2cVpNxXlV3pJNBH+SCf1i2TYc+tHznHGTvEexSPlGzVBs9vjM49AvsitPBBMnYf+zFmHufrsOm0k0B+sKoMVcm5H2aIX6KauBqryK7LyVqoItz2Me5CBvnVXVHT9IOmTAXUP7yU9q9Se/KlA61mCZ9EOz5VNCLKdJG5qS5pIUJBrKYhWfpnVuwCTR3esSpY0G110pSYMIp5UeeJL1r+Xdw+0QH2L2JFEhaFPLTw9gIJWl27RDvWQ2YmeaZrot06mY8tpHZa5FOAzGLWL6XqIEuBPs498vGeVUdYUL/aYdMqIWWzi9W5qxPb26aey0kzc1sglE8E8IE/nM39CuCPWGfTJUL51BSGCM9ki0m0FKL6813s9euM/mcrtTCPtwRaJFBOcR3G8GesNdS0oxV0Ki5cojfF/7pHjPXQotLr2kTaadNB5u3Ry2kk6LskLswvhUlaqB1l3gzH6Pz+DivqkM8WxnN3Bx00FJSpI3e9KYP7TTTl9km71iYb2PNV2fZe4ninQZ9WLT1LYJdwil+IvQig0NSE7PVr9aaSzols8CbPrVTpIUOXY399kTK0YkQj7tDSazVdQS7xCpoAqTGuvwRn7w6xJul+da3VppJ2mfzwEYnBVrp0EFGhav9ihtO8bblom3yImz7m7os47yqDu/fj6ysfj19+zp7uVbg/D7Ur6zWVgqzX247qlOQvPjy/WworT7ndOSYeazDIXv57ft+OLXyOiZQOnrKy+TF0nM91vpNXn5pXlLLX3XWO7IxYd7N91F8FC2SF2vfNalZ33yWOHT2nekqqEfzEqXhZ7yWlQ1szir+Dx5mfoX6Tl7+an25JtNKVlY/rkZoqR7fsrIL554kwvJKDbRsYTezgtPxSBjnVXVH5p/gwcpoAnNIXBAj/bWfrp3HHvWmSCsz1zr7ZUeeFDbiRN5JkOZu8Gll6VkEe0KaI5jEi2OmBx4mZm6+tVIgKdK7fb+2H9qd3hRpbtZPfPzjYFecAqmlbhgO8UHXEeySe8Cn7+uH1phL/XCIN2sdkpZ21F/7ebkmsxt9SJqp/VkgOdotFyNh4Z+ctl3iu5nwumacV9UdqQjuXC6YQIekE0R6K1monbSTEjfJmO5ifHEKHj0m6EXuhpy+RLBL+WhA+x8z8dP1eDaBWWTLtJP+lucsMfMkoryTjfmsDoTZjZlkI953mt2a+AqbSkSToS+MlVn2f5KcA806VQMmMN9ZlredfSs3oNhdPAu0bkTbX96CZBF09b2tCnazHOOe8Tiv6hnMzGyfGljTJXnHVkYT6Dv57lK5LknaKJIfSZN+Exb2AWDWT1mC8xyk/uhjBLtE+x8UZm2eE7PxfOGt3ZmlvpIWdlLFMs1s9a21FurO3yNu+7T8AWAWZv3UAj5u+cOQ64Vt005PL0h7JIK995jAfD0xPl4I9rRxdZnu2cz1k7Xwjf248da4v7ZsRLDJrkU+HaUDzOX9bVGwm6W27V6mD8Z5Vc9hzzrr5wnR7mWv2QQ6ZOPEpuq7bXSRpbq7ySoVcVgYh8BeX+bw8HSVjsM+l219O4M9IasLS7UhsNHK/Dwq2jtI4HP7+/PZO9J7ees3aw8Bb3FNCAYZAHavmX6eEO2pqWAY+AqbQrAPBhtpp8NjqyBzZTpOOkSHKyIz1yGrwM7ePkKwK6PiuXgTqibKm4LdzMzSbM23sVn5NQezSocqszTWlMpXE5h1k8LWBFc1OZi1edjSbQITmtCEZn1tITBzszZrszarKgHa9FUNH7vRXsuHRXv83q6jeL+yXnC0t047d4eODiWNxcI4IOxJnwofna56ZmHvk31dws44IGykd820fVC0e92wKmy2v1dY1wPnONzuOGXfDv3nQ5FWD4v21K9jAJjAS1CghGAfFPaozYOroKTH5G9PHnhnKyITOHL9rM87b++qHZ4ub8LVjZJ04xx2M0ucwqST9lk3mmuuUGuz0UYLbcsuqPxMO61N+SP5vGdnNTOttEjqH7sOBJorVFj3pDyz1lzB1abFMbelmmWS1j+t614fxU9t+qpGw4fmmmmppdlpUzOVlgfBbtZO0/+4+Vb3yXW9uzwTU9VAsDsz11KhQnPUpqbboPc4xsLE2rfjhbAzDgh7Mp9aa6atWWljd7X+KH22HjasCqlEq/vr5Sqhm56ae1f1bRMNrrCRede3Aq2SVU+N1jywVJrewqbs2cQvWAUNAvtpYi1WdxUUSsU9+WQR0t2K6OB8/cfdvttVIEskFbtaxVRwK/W+frW6Tmmvhb5lk0N4Lo58cA7MqlvuHIyWHLDyq60Wzm8D51iWX/e/lH7GofTXh+yzvuIU+loqzI5Y+c6vvPmrGlPR3PlhW+e4qvS9vup4572h88OinfpUfHPcTn98P1FKzecVZIeCWB3q9Hn/T7gwlnk8Wu5W3XzXg1L7iX1lL3/qHNTm7wkryFYsVr/VB/UURv/OjuDKvrXT+YbywhNbZS9/i4fD3nnCg1gZurNE598dz6mdHSVHefF5BZkSq7EKiltW6BxglnSdrkZad/1z9wjl5JjBDtpiOj7kJNPpxXeXusSbrVaS9vpjS3YP7d7+1aabHTCz1VaBNvpjP9ykBDayn/qTHgSkL/OKo/pBCx31x77bnYIsfm1OLvh62JPjVlLDPd74cAt228fmznv9JeWKNxvZWx4INtJH1orrOYb5CQZxyS2IztFyZmaWSUDQ0n9+3oFZo6bMh+PCWsc93l8M+9oZV3fVdhV7dHrn6e5c0RTkLxkYdpOd9BHUco/v5ZiWBIeur1Ko+gybws9qUNhI79kP91dBc6loYU+Gvk7amZkVAp7uj+7bmu97navbkExXl6NK5R7EnV2FbKfiUOM9Vk/tLGqlO/bzzB5eY7fExiI8//GQfUJmc3UsZrZqb/HVqxpjcSwtcblhae/emqCl88P33Xcf6r+34XqmLWvu+3lSaj+z5cUvbu4xJ/906FtSUQOnFloWR71719Bi3bAzDq4UfJes7ljafVnPCnbz39v2UM201UGHOh4DDdYw/sfjyEB58Im5PhtWdyztffMecnxJ0/KTjruJXTEuHVk++3unKPWfWVYqVxDxDLDO7MjZEruTFUfB1/ruLJT0kI7G5Pifr+zOpIK27F3uL2Z1b2AyXLUm2JOaHLS4MQy6g2atocUZpg5WWhSv4OLNpaITwX7nOaSlQrRnzmSd3btC3e4uw5yXHU9WWnR9ZygNPLXt1a8qpqtM3HS+CMpq4AqXpZVmyRT2rZVChVplfcVDHf3fH8oTT2119atK0Z78U2NzveE6ultSvRTF91dTlL6Vq82qG6I9GWd/fdc5qXcqXH61VqhQS1ecZOsQKw9rkWx9zSpoQKUk7Lh0FRT/s81kaTrgdVLHYn9d3nlvujK6G+7SUO1+ZN2tjGwqKKio6z+LO26NKMvEttSeYM8Xwjes7IUlaJ0o0nwwOljpR7/uDSnKzjauaqylZPKyKhXt2f3rqiMUbaB3vtVfBLvz3SvfT5PywFMLrizUVqXTlX8LcjGCPckPclHTbNz1IGz8fTPlhaf2VfLLEtGeWe663ggtzgC99F/yn92C8sRTW5X8slS09ycy25kDCvVUqF9Zrf1GsPdhlqQ88dTcSPa8XK4tkhngkMnSZCroZCPrwrRSbQZeZDPatiuVks4Aq+zOZLekcAevY9jjzPA1oiztruUo5PzQtkDbqgihQsxZnQNZnDqbpWbaFTKbO3HyncWvjYJCJHtOWUx7EqfX2YFpblzl/WPanPgbN2tCF2Q5NjncZ0AUItlzyqK5/B/q5kSwK4zzg9i3Ym5Xm8YlL033WTzI4jBEPkrWC2Ux7b7av3v867mn57fQ8geIE8meUx7T3otT2E1gDskqOdJf++muhuxRb4q0MnPPB3+Sz2GAFCLZcy5XQckzvRrmuhmT3XngeHEK2MyEZmHW5mCsvrSQdNSbvZ9FvjkuTmLPho9CP7gQ7Gb2kFho9zYHhdfV6WzyITN8MGHSUlFRlttPbRRJirSx907ogwKlk5dUlYiuo6nAzAsN/r4E7+8p1dBTKjarrqcr/xsxbl22ivRROsqlY+Kq8/RvfTtoDmpQsVirTkTXqWQuCJA6M4AfPEs5eJKP0jGrKhGd1/HNBDokfSHS2/XGlT1pJ2nt7Qz2tBYwQOyxwsRZYrrIxUB3i2yzKKy/QmPdoh8d9KWVQsXJRv9eGjJap2oGKIwhl+ewp3cyNEGNvYVTh7kcqxe7R8eyHqreebCSNFdwnS/Wfqo3Qn1w2ZL/J/3n+vdK/8tj57Q3yaLw050uaAK/k1XC/2twT37qnPU/678q/S+PndPeKoVWFUh6r6jVPjtVYeVl2+rfpv0Pjn+j/6b094+d094GxRmgr4I9gZY/OP4H/evS3z90Tnv7mEDfyfq+VK5LkjZaejwlpwiroKFx1Jv+09L/kqyCvNau6LFx3bIjnRXpVMML1yP/UvlfVt6Fa1QQ6dXyyRWBj1jYA/XdinrwXYFGSUR7x9/qDvrR3d3bfkxW/6X+P96+G5qnD9NVXA+Xj6pNBBuZUzK9hWbuweLx749s5Js6iWj3ZF90Bfv9GcA3tPwxkYl23xUxgQ7Z6nhT1QtsZHZuYKnXbWZWQeMiVKj/zeP3u4I9sm++b8dzXMawO/Hgd89UjSVNe7sR7p78qTqe2D4r2NV9lPLkWepH/+zu6woW8zoS3Hl3H2yiMBpCHfRfeK6D2xdu2zzzUf3+LABwn5m2PmSLmRXWBIzp0Ab//xv/LdBK374rqK9s9D/aW/3QlfL0FmiW//T1j3ga11zR923bSi4Euz07S7Wt+bodE26PetNHW1XL4smlY0WM3DWPRYkyIHXNTn/02+H3Fd1g7ndTItihHY560//quQ5O676ToeNU8jcAz3PWR62ksE1TXMEMdqEGveZf3fhvkTb667d6Zu2M47dX7KeK1wCv49PC7jLYln3tEu+6xCy0MCftdax0oWlV1thPfZq5zq3FFPT9sQ3NbePf0b+uiGGXpCSG3XRZo6LcGEYEu/S/6H/0+O3wDP99RQy7JCUx7H5j8sxzqbdmtbKZNMv/qf+242+EV/l/V8SwS9I59ufw0v6L39n3GX94cz78RxUx7JIUKYlh73TVc4GZO2v63Z08Qv3xR2EVNDw2N2zocVCgp5Af86jprqdcC/aNlgU79VxzyUQ6xaXrtGG9jzlr89oHZuU1X5Vy3U/CuQseimD32e7+f0N78lPHLCvlek8SzkkP5cqeF153Xf//qyd3DGpi5pVy/ew14dwF/W9X/a8huJggS9B5SSbWvePW8F5Yinusrd+2yCpoYJh1pVz3b7Io+l4PVlVeCXYbmQ99lVxuGHdlc9ZRR/+x3yaUNHvx3FIGhAYxq4t8vCnlYr2brvt0BDttA+pi5io/sfxSrPtdvDneI71YRpbBOdQDxAQlKwapWqx3vwWU1qe/+D/yEZ5hWzpmVYl1D+ObWRZG/nt9IH+vpxWQ4fz1QWLCipCnEpPFOT+OzEsz8288LKFqBiiMIiVZ4u3efFTuGkozLbU0XnYPTaBQc801Z3rrGxWipUysJ4cBdu5q+0gE+4WkMUuF+mi7vtn+Y1/lFJRgAm1LxqMyy3raAv2MXo/kZ/C1aIrn8T5Op1BNmWgpE+t+23+/2xUtf4CUGinK18bxuRs+Wr4ro+77ujhrIA91lfJ7NFgr6BSp2LS9XAUlz/R8OWG0v944V7zuD7PijcgGkEI/KD3Wze5MVLoIzQm00sK8d+ewbpYKC4PjUSelS0+OQvFMaXetcoNPW6IvO0v1NVTvLq8006b1KYSpaoisr6abKjf4vOV37qFUcEa7M2GZwI+kymwrbFgNiBLRUmFZt1ESyevLj6LP4yqCfXCUGCmqDVnx7zrfCDXLQm+7M++YPhxri9liiHxdrRlKVkHpDJAPc0mHaH29Yc9OFol+jrKz4o3IJqtCbSvOYbd7c9T6zpE+M32bj/bj00yglRNXH2l/6ZLvM6EHSLq2sdyKWe/SznJ6wK5YGcFuZpp1coIvgmVwmOXFKHkjZt2ekpHKhxx+ZCnmy77OhtXguBItt2PWu7czDmUsRbAPjCsjxW2v03gl0v3I785O90Oh+hPB7v37oT6FUwikW6ugk+buoJx2CBO2/rzPPQ+4m2X/Jym/R0Ud9Y+qv7aR/dA/9aH9zSlv23bEiVnpR6vkuUb61B/74T+CHlwubCw7/bEfN6JEcjtjv6iWNKG62W9ORq8pJ1ocFhdy5ag3+3Zz4ol7hY+JI+9t57sRXMXJtzvJg21lYFyIlrM+7J+bW/jxk+0y9dALY6mZm1+zeP7vH/mm5AUtfzhsC6vrjf7Yz/tBc92m3TLzwirr/rq5D8fa9m1dCHe4iF6/vQqKJHdQ7vBhPz0TdDEPmCtXg3Nprf9x60NsZHf23f5Tf/WhTUUXPpjWdg1NYA5aZ9ew0x/bj6yb4FAQLffEuhw52sVu8yPTTmUEu+bqxuqHlWVQFKLX74t1yadgf2QpVqhf99tH2FYGQy5a7ot1yYPvhD0+K4JNoC8FHfVVfEsGhmOkqCfW/YxpRZkxjGNtgzp1hb5Q2LS9vwo6ScV9yWToa38jK6/VQ7sEHc0DV7chkQEXo8o/6nyWPdmd/bRv1uivPi+6clCRIfllzFzfTv0/bOtJv+BxnO5aQ6wndCdbak87Zu3U53LAWeiRk6ufB8E+LNLo9XpiXfIm2M1jBxb6Ot4Q28qgyERLPbHu/mWXdsZ85H6gfZlAB810sveOwWoGLOyDIjNS1LasZ3R7sJX7bfeD+voQwZ72BXrCUPjKtljqroIKi4rOJv18HgjqG5k7mweubsMTFvZr7Mlu7F+9FT5m+byN3ayNNaWC3wT6cha2HcTKN0f1VY2Q2MZSX6xLHcoWGznd9Mb3mWXBqaeYIX6hoIYbcRMg2AdEEr3+wDSlrGV1fnTNA0sxUzyDo8uFG7aVAZGIlsfEevpsu4zlzetWu9eZQAfNddJbR3XEwj4gEiPFQ2Ldh9dQwWL+4NkgvrycMi3BKmgQJNHr9VdBR6m4wE6W5a2viGzkzAQ1t806nAeCy2qVTwUXgt3MjDVfuoM92r+FAyLa8O935fp+SHJ9SpiVFg+KdalbO2Peciq/z4QXxxgW+0qoTuzrxDEOCTPX+kGxLvk72MqJtnwwgr17CzvtfwCYQF+PW9Z95C+xp3yboJ5l38z1Ey/TOvPpS+4HPoSDYKvgYcu6jzzxxe96xLPKt30dwT4ITKjVcyaL/O3J0qSLFVFuJe/fPDC/vAlXN0rStYV9ppry2348s3NdF7N0bmmkjxZvFDyNmWn2sFiXOrUz2mPW5CvatQn1JemjXJSbmZaqc37p62BlGRILvT8o1iV/CRerDyy89V4p6i7BJ7aVQbHS5kGxLm/pND+yfre6/2az1rcCHTuU6/iWDAiz0PlhsS6l83qXW7WXmbtvX1c/ItjznBjQc0yg5aMmi3QGuMoT34UWOGeSfWnumgs7ngcuTmGv6oClLvE1I8w+s07VvK3UPYxi99wNM6GxhhPaW8SenxDrUt4au7Gxfyajw8yUHFNoljoo0IfdXW/6SYqXeLtOHOKxsA8I+/mU06B/C/v9M9jdja0uz+Og/Q8I+/mk11vc/jqN5LXnbMs/NDePqjVL86OVpI3tUq7jWzIg7P4JsS6lLd9bno6BRLAj2AeDjez7E6ugc/Z/kvJm18V5HDbPwHYzZLnrecDMKg91u2Nhj6k1nRbig5uu/mOHUcCwSHtrJ8s2e9Jn8nJd3FczgfnSVlGcIcGR7FnrMwstFambxEPpgIWFfbTYKBmJOzksqpR7E2yxT3YZipR+M+1/zMRPd37fwtEkdp9J9m25ZDeBWZofbTXTUX/t5wMf/jLZUhWRMma6z18yuAh2ZZqlExMJ+OBCsM/SR97NJm6af21htmX/2dM8sLi8BVeOCAn/uPXnd6l3iNHjFB7dvZ3Bbk+2fOGqIMGeknvYkWyxu8QpMtB3ulwzc7PWjxY66y2zFb0nHWQZtymz0pekzy4mj8whbU8c46iJtx9n3QoWh4fsLJ26MMffHHGo26hJn27Hs7bd6W8y62zNV27NMYEJzdoc9Jss0t7sW+eO++m9wDQxZtJW5Wez9oUIdrM0X+0d3lz4ptS/i03b8XKSikPdovBPu9hIb8mXL823yRKme54HFvH/5Z3sWPgnp1ywzx7cBTzX+H35AnWuMkcw9733b1rXS99nrwpy4i5TMwnQ69id3nSUFGhrrLHG6jtxefmTd0sb6U/SRQ7GGqu1ujufAPv6NLiTUaFtbm8HXTjEd+NZEn9z6lWFaBk3ngS7ZE/6q40iSQt9xbOAsfrVQSuFOmunv09kpWiC5HA8TxH+0Al2n6wJO2/5dbgZwb7SoqNVNltX4yfJE583smTJ0ZEasJF9T+zsc231638eSPuem7atSrD/S8VnLB9K9FYl2Euy95fw6jTVdVRQN1c1bvZJ+p+wq2gpe9KbmWuhuWaa6ahIx2trto30ZkItNFOok07adOaaxVQ1DXLB3qEczri3jehu8u46FS9sWE0CezYnzSUtTNC1L5GN9KlPs9Bcc0lhsmo8KerYl6RAdowiI//YOWohaW5mHa0qTg/kfa+MYDczzWqc4d4MrIJGjz2aSIG0z4TbXEG8MOlODRz1N1EDfZgHrlwMsuZ/fT9soSjMXs6s7hUt771Xv9nLr9L/bmUVVH6ulZW9U4eg8OPh4loOV+8PnR/C+9fY3FVRSu7hj+969KUk/3z7rgel9Sf9lbyoMcI29p3pi8Od931nL3+7HcGyb2bcHHnRKnmx8F2TfhStkxdPrkYoQynZunbV0fetnR/utC5t8x9Kav3VXK1u1oJV4QRK3NZmNmdpp/zc4xXh3LkfydRYogb+Uan6b2bRK+wMHG/sF+Y7BCV2cLOQdCrZZz9evauatapcN2dqyzH9uasClzSW11vW1D6RtXF2lsePD6fg9DtvOjaahTOePZcJ+UnI4DAh0jGul67BHojHfnI3jJ+uW/4jLaraFj9XR35PZoGvySQ4StL5OlP8JNVAGoZYcjhPST+oFuyL2wegSCZM7vOtTHp5/O+sJEIhLK+UPRd+e6MeZqmldo5gD53kGOUDzazi9SM8dVVQwHMsb89IWxGLtvHjQ7DXOEjRBM4m7a6jzA0pOMRPBnvuNuVovzHzpE+yYhg9Ng1NDbtJ4VZ/NDVrZ2a4/KuFumqdqVyjL4wae6VHs0i8KW7ihuk9SLnhEH/DJd7KannDjD9P3FfWd8z9h+zloeS7KhwvNXPczitdiLTQr34UFBx6kvoo0K+uHCwVOE6fVj/PuqU+d1WUwp2K/8EJXLiCTat07/6tefay8jsdB8rvrscvH2ECFF8la2k4xRMgMKmSPe1lR9/3lb28tZYvhKAW36mFOluX6EdWVr++nxKl9Sf9gBP42MtjAQLVFvaNpK1Zl+8FmoUOCiTt7p5U9565pYfuyXdmri9Ju3IXSHvWm+POvjZXDvomMGt9SXq3kVyn+JVZmcDMdVCgTfzpZmnWZm3W5qCfghP7TD/m2xyS/7p+4Kilp64KCsQbSR2fyNtHTIgr2KTo3Ck4O0ix8jvNIkkDKZ301u34lR/mw+m7kyBt/xN0gLwiNazgWzUFuh75HV/QqreYUMUTqYtjcGf+oviaTIijJJ2uneKnqAYecIhXpYV9mdivrX61dhNWKNQqsRD91kueoblj1T5oqVCh1vqV1fbm3wXO/qDVj5ap/UXz5O+/c4vMxS6hdT/dsYffLg+kfXn2qihXT6yjFCz9LaQdmlbRLHnR4UiR9bbS78z8pTxY1xMrjhUjwWQKHkXJfUhHgo6SelF8l3Tt3Nn3pWvfir6mUL+yWjprbXe1H7fPTvye8LuZTklThW8zq3LWISa2BkgV93d2JzIng3np+0v/fJnd1m3F9/xqXX9hpyCRssWyrvGXc21L/jKpwcV7F4lLzdV/zQctHSqL1YOC6fmroiT3L34x+cUKrmBTKz6eeDYKXi2//Mp1J6Bp3v13U3wUnnhyH9JttI5cpCm+S9ey1BnbS9pY0v6WBYOX8z5t1dm2ctdbGRSfJX7aC8cRPBFfB5+18nAf1rJFh/hkx6KiH1z+ONPvRQxLoKW2OuhXqeBdPzPYZJ/zI6uDto9M1Qq11pcO+k7qUFkDLbR+rn5P3u4XroqSSYhJR/xn8cV4Zkym+LAmZHlBLkS5ltmSztNmI/bWqZXMp2Li29uZXXPSM+CUSvezfSbFf4tbtYkHa7bez1ZjuWfq4vqvWqslviaTKmk2h99MqGZTwYT8TNM12dIR7El3qxgfvFeZMt3SdQqWfhZcwaZXsmVbp4JF88Sy/522NS0c7yNPE2UWhjVx8TatwiaNI1ImmGppuqV776psSzYX52lQ6U9uYkrSNFslkilZnXWVHo+14KRKOvZ9OU7xya7lhGzsqadZiUN8lUnad5Up0y3ZguVnuhaG/DwE3zWhdPrc0yVUpy2/Isjpx+cyKdsywDtpQiWzLU94gZ71xYnFbU67ZBv0HY53mpfkcboOKg2u3tVZ78Tbcmoldop3bctZc5yI6SrVP2X3oOpv/nEvhR1AW9hzkglxlmWonh6rJEP85sXPgWERt/yg25ZvI/uhP/rUUSdJJx210V/7p+NT1x1MmCSIPVvOYJ8SaYtbdXQmde8wMy0lSZG89T7wQDrOdTjy25N9019tdNRZ0lF7fejP5QlPNrJvetNOR0kn7dTZvJDNAkfOV5oMR0naO4eBLdOjDNZPfd7wSK7THQiSDld5UoKxvisNE8bM9CNJivRnikP11K9/uphAP8lWzZ8pH2ZmDslS7cPfpgH4wHwlZ9ls7h4NO0qylj/R658u5idRJm+Ww/wkMQtMETPXtyStHH2+00f8YgLtwIQ6SNLaEez3rx8LO3jEnpMtpY4tjb0hPQF1h1yfFja3q02z5UuSzDJZqJ3GP0HDBalMXU7Rxu54liDXp0bqTTfhkd/F6QvMApPBnuIV0MY5jT2zsU/B72olxVnLU6J0SrzRDxDs4JfPxCdmZWa+q9I1LNomzSZp+UsT+q6KN9IlK+1/ckx8sza9ZkKhJofdJRolnPDI75KaWOkL02JT+EdSZsEafZCsWcRr/zQiVpJ2aXjAR/XfIdjBK5O2NLJomzA2mrqlxaQb6kdcQyfJZDdrM88SbIrTJN2g3L70KaPALDWXJB3pC9Mi3bKNkybEpDas0ftdraXivkS2HLy5GkKwg28mamlk0TZ17GbKlhYTYFmZNhPerE2v9+OlT4GBYveJRpmZ5YsfNXwwW0yXZMvWffRJcxi131VqqnAvMZVBt/sBgh08M1lLI4s2SFv+VPKiuqTeYDvs65Nlkpu1eJZAvuYZuSXxDmZNX5gu6ZbtsWBjT/awRut3lZoqZk78+jkdEO6shhDs4J0pWhpZtIFkU2+w+dQsLSbPtoJlZbJMcbMWzxKQ7JEjbQuzAGaLaZJs2bpJbLIOMVYzRmKqcONhNlcvykGwQx+YmKWRRRskTE6wJKwT+/pmyofawQQ3a/EsAWnipyQk5H2BWWCS2CQ1+kl5XGhmeV6M0Yxhwnitl0XrSzqmV393NcQ57NALpnUSp0kPX9xZdpYnzhTPYzYz/UiSIv3hQMNpY5aJqeFk//quSwdXG+gnESl/ECnTxmwTZTKhkb9w/fks8Je+MF3Mj2ZS2hgkKdKfNKL7bVzbmmauQzz+HxzB/hY7WtZYDWFhh36Q2djHGrmSY+a4A0NGumUzJUtL6l+yQ65PHScsZAr+VVs8SyBhsqckJKReZdjXp82n5ERxSwr0lb78GlPfMEE6/m8L9vVkT6LGagjBDr3Apq020Ne4hYsJ0j02Fm1QOI96Iof8mKUWkopzNEyXPAHXCF0gXcw6afkRLR8mfEqCJJN6PtMXJk56ZkKWJ11SmC6GxqUHtvERhku5E11isanVDxDs0Bc+kv46H7NwceQ6cgVi0nawmIKN0eT9e4N9HSSbhfBpbea+a9MeZpkJs09aPmiipyQkpLMAXlawkaRIbjRsJmpHowfS7drwIt1cYrWrNScQww69wYQ6JC9HG9WVxa1FerMn37WBfpDF8Y4+h4OZ6TvZsNrbd9+1gb5gvmPbg876O84FvJnrO3lJ5hJIMKskPGhicdzZOuhs//iuC/gnzeSzLdie31Jn8RHogXSNlwWxS5JOeov37Gr2AwQ79IixC5dsepbe7d53baA/mHym+jvejRwT6JAIs5PexinM4BlMoO/koMtRJp9zks0d7Zvv2kB/yLaqJjQiOus81kGgfCM/XyBIUqS/qf154Hog3a69vL4suV7NfoBLPPQIuxuzc6RZZHL9k2kKXOxHupmsw4hiti5JYrgU6X0qi1Oog430noZEmZG4QOY4gVAn4VcCLu9TCAV0MaETFMU6CCTZc5x6Lp8GpDj5XLIY2g5ZD5hZ6ju8lXsZb+m11u4HCHboFfZDsX0xGJtwcWJ3d5bodbjkfawtPyVLuSW9T8n9E+pgT87J1GNLwrXONqo+2KgCF3tW6nExjRwmsywF+H74js7QFHYXR7Ln3UEq7GINdlVksn2HfAEkSanU0a5+P0CwQ994S7xggiyifQTknVb5whQgw0ZO2sURLtyclFsf4zpbFZohXbJJWo8pCZdZZ+EuH+MNd4FnsafsaM/xn5PgroPI5AAO9jP2ry02jMwtdaCGDBPkueHdfehN6kz8kB4ghh16h8nzMowmPU+aVEOR/mBjgXLGm3ZxjH0ammd8STnNIrMofuJZBeVMI4eJZL6ygw0nlWQP6pDnuFkXxO1HKm4HNyuYmb7iK8pzjkrSPo2MelAPINihh4xtkTO+ZSi0g5OWcOBpVgpXRcotqMXY0hKyUQX1mMKWvsl12Ki3JeBZ8lNkvgru439T9/FIn8NZF+Wjf344juTkhn+4H+ASDz3E7jM3kfXwncQcl8hPpim4hd2ML+2ik3LrTMotuIWNsrXMfJgukC6OXD8h1+Em489h4gZFsQ6CEvKMDlmEtyTpkC6hA22HkunBLFOVPi/I9Tz28Yl+YCmUXhZts5dr33V54SqCcVwHpbui7+TFr+a+69LA1eQ9YBTXQ2m7aJ69/Blyi9FCv9l1BL5rQ+l70TxrL1vfdeHqKL6KlvGLuf21Ls7y+av/46nW6culLRKmb3lCD3i/LAqlvCjIhIvVof8d9O41fPmuDWUYRYF+kpe/WviuzYvXMnN6wMCvhdJVSZdsGnAP0Mq5hgFvO1C6K1pkL0e2ua8gk+sH33Wh9L2kYje8kLpfNpMB35r5ruWN+gc6pD+sL65hmb7pKT3g/dIolKqiQF/ZD9/DW/Q4e8rsKlMeKIWWs/JdG66D0nXRcsgtp+BXhVyn1C7ONs/gWv2Nq8q3bb+HaXqhdFtSwXtpnf62mU7v7biqedraA3u4qH8mA57sB94vjkK5VXLHEv0q9FmTh2u+dH4Y0eRL6aKMYbOHHkB5vgy3BxT8qhAolIeKs9UzqFZ/44ryntxbkUXpV8nH0PDCMf7XOk1o6ad2N2sepq19br+rrOtP9wPvl0eh3C6FZX8PO2hFrQe70UDpRxn6sp8eQHmtDLMHFDcahlJrSn/KEFv9jatx128DDW+hdF/ycfSG8LX66pNrvIJ81XNzo+Hp9ZD3S6RQ7pWh2VqG7spP6UcZrmMtPYDSRBleDxi2Kz+lD6XQ6geddrHgL8C2LeWhUsu13OpX635sa2mVj/2rW678L/QD7xdJodwvhdRVPd91zocZDTZZHqUvpZC6aiD+JfQASnNlSD2g4FWCNZHydCm0pJ63+sprcFJv9TtJGKWfxW1B2wsJfLDOwuLXd5JGLbNEwSV1bS5ZnvdHQqHUKUPZdc4jWDQIbwBK34tzONQgcgcXesAA6kvpexlGDyh4lfR4hqIMowyj1d+ov7ttO4BjuCj9LPm6/zIB3Y8t7GT9+NrYUui0dBvan4t6NnkcnffHQaHULc6us9W2fzu2mjk7ygOKt6f0u2ju7N72fOkzzIwTlH6XQg/wtjC7WcO1I6/wKqE0UAqtfmDZEIa+3UDpT8nXFJcns1v7Ywv+5d9dh11o7q75wyvX/V93U6GBfuD9YVAo9UshQtD2JXbFykozxwNgIPGWlKGUgnNhLwWLlZVCp5b0AEqDpZCAzurQp3jYojskflWUpsow0y4WwljYtqW8XPIsVrOrBHTWHoqi/dDVyqO45p9dOcIXEs01FNji/VFQKI+Uwq5zD2JXrJLckO5GAvFalMZLYUPop0+Cxepqw4oeQGm8FDysrA59aGNFd0ghTygNl6GlXRxijSl9L3kWq8B+2Wu2tjAZfGnZ7vaWFu56J7Drkjp955HrjfUD7w+CQnm0XMhjzxbHftWGMt5ScDfvkZWxkF/Cqvdu+5ShloIPh5XnwKh+1YYy1lKwV/fIq7C0ruEwfQIofS9ujpD1lWt8LNovmtuXVk2PyAq0dHKV2Fisl9Vm7Saaa6wfeH8MFMrjpcSm7UW8XDhD9sLeTxlvuciS0AOJcNUTf8iOTWmzKLwcc33IgguPkp7Y+ynjLIVEnr1dZRTjeYcWdU/pf8l9rIISB3Rrf12ZnJZvrZuwb2um1YU3lZVdlor1L9fe32g/8P4IKJTnSsmSqVPRfuUM2fO9b8o4Soldz1u7u8gpMdgDiCjDKn43ShVcOef3xNeFMtZSyLneQz++q9VYTzcVKMMu7opjVinaS/T5j9bPmhI01/paqs/s6ioffElEfcP9wFgBDBUz01ah84ujjtrbc8vfOleohebOr3batP2tAClmobVm2Y+RdtrYaHp1gOli1loqyH48a6+T3bf8nYFChVoUvndjd77vBYwfE2illfOLkz7t0XetSmt21KYfNYPxYeZa52v+UKuCAEg5a6+TrqaDSCdFOselesVuAs0V/2+muTPaS5LmWigsLP/zb/2Q0/Bb6KEIdhg45rrPnnTU3p5a+K65Flo4MkWSjvps47sAbmGWWjtTSaRN+1tVyTcHWmhR6HM7fSLWoVuuhIIUaa+jjs23RTNLpHrx2zZ24/suwHQwM620dH7hXRqbQKuLjTM2sKBlTKh1rphDbS+W5CnJdKDK6eCkSMW1+1wq3QGQJC0UKqz4rrM22hV+bKMfINhhBJilVlf9qFGbi1lcWFZivE+YMF2uFktxm29lqyr5xpkWml/IFrxLwBtXEiYmlu2NtEoz0+LCn0rCowQ8ceVV6HH8vVh3sYEFnVFse2UCICeW7c93kiBZ9gQV/z3STpt8WyDSzn62dNUIdhgHZnlh9Yt50eZiAi2uLCsxex3ZSwa/mEDrK8Fy1lHHZt2DTbkfGBtW4B0z06p0NXXS/hWvk1J/KineFkOsgzeuvAo3HkKiioZNNrCgc9ywqGvrxSUnHSUdr4zqVcwSf/h5tcldkrRxxXrLfRHBDiMikddhSb896pxEr5zudSczU1qC5rcAAJqlwsoYJRkdXmynJnYFvpYtvYmhBLgpr886SToquu97YkIFmkuaX8cu6uUtAICmuPIq7CR/j5R4GxY9gwmJAi8UvQwDLa8cAMuJdNI5CWl3SQf/2Q17fc5Je+1dy33r3i4IdhghFQ7sOaeKbbZ50mPLOWuvIyIF+oep9tra66RTHbFy8XlzzSo+sbOlIcBjVDiw56QrtUvKN2dzGnSyB2gGs9LqYnxuLX9PpTlkr0/6Bfjj0mBxz4G9CfY6al+cRo76aL8fINhhtFTaXB6nxWkQoDlMPFdV5UWJbY0nRdfbTmaeSJZbm1b7Jmz2AO1SmiLuOfCngh5jyj2BGz4zoTR3iURIFPSEq8wOup0i7lkq0th11g8Q7DByzEwLhTct59WcdNYJayIMC1N98shzRNo3HRUP0C7JIWyzOyGI5UQ66dT+QXEAr2ICLRW2E7xXOZPgbQg9ozx4r6ml0DmR6hd0vDJCsMNkMGkWiWr3x5rnNAL0n2Sr6hm5ktNy3nmALnBi06vCE9MwqVqx7gD94mb+nofWNCaUEl+rWWnuErwNobeUbzHNtFBQOzY9J42g2l9H0HrZskKww2QxF1KG/WIYHyZInNyDJJHifeIFXqQTm1YwRsxlP6Cdw0ionb+nuNqJU+zOSlMtppC7BAbCLWNFuhwqP3Ld2betyibvccsKwQ4AMBmyWPVrSmPbAQBgSDSYv0cidwkMkhuHMj/H3neALIIdAAAAAGA0vJS/J/UHJncJDByzeDqXScxJ535sWSHYAQAAAABGiJkpLbeOL3Tc5fG1grFh0jD2e8Efvc1lhWAHAAAAAJgA5lq090qYALSPKRXtfd6qQrADAAAAAAAA9JB/+K4AAAAAAAAAAFzz/wBkrKfgv+f4mQAAACV0RVh0ZGF0ZTpjcmVhdGUAMjAyMS0xMS0wN1QxNToyNDozNCswMTowMEcTThIAAAAldEVYdGRhdGU6bW9kaWZ5ADIwMjEtMTEtMDdUMTU6MjQ6MzQrMDE6MDA2TvauAAAAFHRFWHRwZGY6VmVyc2lvbgBQREYtMS41IAVcCzkAAAAASUVORK5CYII="
    }
   },
   "cell_type": "markdown",
   "id": "45844059",
   "metadata": {},
   "source": [
    "The automaton $A$:\n",
    "<img src=\"attachment:automaton.png\" alt=\"Automaton\" width=\"500\"/>"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7ec492f1",
   "metadata": {},
   "source": [
    "We can represent this automaton $A$ as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "1d2b06e5",
   "metadata": {},
   "outputs": [],
   "source": [
    "a, b, c, d, e = \"a\", \"b\", \"c\", \"d\", \"e\"  # names of states\n",
    "t = [(a,0,a), (a,1,b), (b,1,c), (c,0,d), (d,0,d), (d,1,e), (e,0,e)]\n",
    "A = Automaton(start=a, transitions=t, final=e)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "85ed5670",
   "metadata": {},
   "source": [
    "We can print the textual representation of the automaton:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "5ce2e76f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Automaton(start=a, transitions={(a,0,a),(a,1,b),(b,1,c),(c,0,d),(d,0,d),(d,1,e),(e,0,e)}, final=[e])\n"
     ]
    }
   ],
   "source": [
    "print(A)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8c9bf846",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Regular* on the variables of $x$ :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "6b5d50c6",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x in A\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "01af9fa5",
   "metadata": {},
   "source": [
    "Interestingly, we can also display the internal representation of the posted constraint; although a little bit technical, we can see that the information is correctly recorded."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "f8386754",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "regular(list:[x[0], x[1], x[2], x[3], x[4], x[5], x[6]], transitions:(a,0,a)(a,1,b)(b,1,c)(c,0,d)(d,0,d)(d,1,e)(e,0,e), start:a, final:[e])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9bfbf15e",
   "metadata": {},
   "source": [
    "By calling the function *solve()*, we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also print the values assigned to the variables in the found solution; we can call the function *values()* that collects the values assigned (in the last found solution) to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "ada3f261",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 1, 1, 0, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "206cdd3e",
   "metadata": {},
   "source": [
    "On can enumerate the solutions (supports) for this constraint as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "81d1ae7f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0, 1, 1, 0, 1]\n",
      "Solution 2: [0, 0, 1, 1, 0, 0, 1]\n",
      "Solution 3: [0, 0, 1, 1, 0, 1, 0]\n",
      "Solution 4: [0, 1, 1, 0, 0, 1, 0]\n",
      "Solution 5: [0, 1, 1, 0, 0, 0, 1]\n",
      "Solution 6: [0, 1, 1, 0, 1, 0, 0]\n",
      "Solution 7: [1, 1, 0, 0, 1, 0, 0]\n",
      "Solution 8: [1, 1, 0, 0, 0, 1, 0]\n",
      "Solution 9: [1, 1, 0, 1, 0, 0, 0]\n",
      "Solution 10: [1, 1, 0, 0, 0, 0, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "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.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}