bokit_tutorial.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "e7b1b834",
   "metadata": {},
   "source": [
    "# Bokit tutorial\n",
    "\n",
    "This notebook provides an overview of the bokit Python API to create and manipulate Boolean functions.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "3f161887",
   "metadata": {},
   "outputs": [],
   "source": [
    "import bokit"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "076cf946",
   "metadata": {},
   "source": [
    "# Variables and expressions\n",
    "\n",
    "Boolean variables are identified by positive integers used as unique identifiers (UIDs).\n",
    "Note that the UIDs can be any positive integer (including 0). It is OK to skip some values,\n",
    "but it may have a cost of the readability and memory usage of states and patterns.\n",
    "\n",
    "\n",
    "Variables don't do much by themselves, but they can be used to define Boolean rules\n",
    "using the ``&``,``|`` and ``~`` operators. If the obects ``a``, ``b``, and ``c`` represent\n",
    "Boolean variables, then the expression ``a & (b | ~c)`` is a Boolean expression which is\n",
    "true if the variable ``a`` is true and either ``b`` is true or ``c`` is false."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "7fa17591",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "_0_\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "0"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# We can create some variables associated to integer UIDs\n",
    "a,b,c,d,e = [ bokit.Variable(i) for i in range(5) ]\n",
    "\n",
    "# Printing a variable gives a generic name based on the UID\n",
    "print(a)\n",
    "\n",
    "# We can retrieve the internal integer UID (but not change it)\n",
    "a.uid()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "fb453c7e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "__0__ | __1__ & !__2__"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Variables can be combined into expressions\n",
    "expr = a | (b & ~c)\n",
    "expr"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "efa92544",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "__1__ & !(__2__ | __4__ & !__3__)"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr2 = bokit.Expr(\"_1 & !(_2 | (!_3 & _4))\")\n",
    "expr2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "2f4a3bc6-2817-454d-b55e-28ff36098915",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "__1__ & !__2__ & (!__4__ | __3__)"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# NNF: propagate negations to the atoms\n",
    "expr2.nnf()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "77f71635-18b7-4205-9c1b-93a8a0601705",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Some simplifications are automatic\n",
    "bokit.Expr(\"_1 & !(_1 | !_2)\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "b1833e89-9b34-4b28-a4f3-0c253a851afd",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "__1__ & !(__2__ | __4__ & !__3__)"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "a44abdf7-3100-4688-8800-d55e591d67a5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "__1__ | !(__2__ & (!__3__ | __4__))"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# We can also compute the dual expression: flipping the AND and OR operations (as well as TRUE and FALSE for fixed expressions)\n",
    "dual2 = expr2.dual()\n",
    "dual2"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a44df631",
   "metadata": {},
   "source": [
    "# States\n",
    "\n",
    "A state is a set of active variables, which can be used to evaluate a Boolean expression.\n",
    "All variables missing from the state are considered as inactive.\n",
    "\n",
    "Note that as states do not keep track of the list of variables, the set of inactive variables\n",
    "depends on additional external information.\n",
    "\n",
    "We can create an empty set and use associated functions to add or remove active variables\n",
    "(using variable objects defined above) from the set.\n",
    "We can also parse a textual representation directly into a state object."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "cfbf0cd9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0101\n",
      "1001\n"
     ]
    }
   ],
   "source": [
    "# Create a default state (all variables are inactive)\n",
    "state = bokit.State()\n",
    "\n",
    "# Enable some variables in a state\n",
    "state.activate(d)\n",
    "state.activate(b)\n",
    "print(state)\n",
    "\n",
    "# Add and remove more variables\n",
    "state.activate(a)\n",
    "state.disable(b)\n",
    "print(state)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "c5090db6",
   "metadata": {},
   "outputs": [],
   "source": [
    "# A state can also be created by parsing a string\n",
    "state1 = bokit.State(\"101\")\n",
    "state2 = bokit.State(\"111\")\n",
    "state3 = bokit.State(\"110\")\n",
    "\n",
    "state2.activate(e)\n",
    "state1.disable(a)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "dee261a1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "001\n",
      "11101\n"
     ]
    }
   ],
   "source": [
    "# Printing a state gives a text representation that can be parsed\n",
    "# Note that an empty state gives an empty string, and that this representation\n",
    "# stops at the active variable with the largest UID\n",
    "print(state1)\n",
    "print(state2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "76af6b49",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "State { active: VarSet({0, 3}) }"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Here again, the raw representation gives more details\n",
    "state"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "36604bb5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "# States can be used to evaluate an expression\n",
    "print(expr.eval(state))\n",
    "print(expr.eval(state1))\n",
    "print(expr.eval(state2))\n",
    "print(expr.eval(state3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "49451e6f",
   "metadata": {},
   "source": [
    "# Patterns\n",
    "\n",
    "A pattern defines two sets set of active and inactive variables.\n",
    "All other variables are considered as \"free\".\n",
    "\n",
    "A pattern represents all the states which satisfy the constraints, forming an hypercube with the free variables.\n",
    "It can be turned into an expression, which is a conjunction of the included constraints.\n",
    "This expression will be true for all states in the pattern and false for all other states. \n",
    "\n",
    "Note that like the states, patterns do not carry information about the number of variables.\n",
    "The set of free variables and the number of states contained in a pattern depend on additional information."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "c85a0d01",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Create patterns described as strings\n",
    "pattern1 = bokit.Pattern(\"01-\")\n",
    "pattern2 = bokit.Pattern(\"110\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "3c372d35",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "__1__ & !__0__"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Turn a pattern into an expression\n",
    "expr2 = bokit.Expr(pattern1)\n",
    "expr2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "c79965ee",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "False\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "# A pattern can be evaluated just like an expression\n",
    "# This amounts to testing if the pattern contains the given state\n",
    "print(expr2.eval(state1))\n",
    "print(expr2.eval(state2))\n",
    "print(expr2.eval(state3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "49d4dbd6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "False\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "print(pattern1.contains_state(state1))\n",
    "print(pattern1.contains_state(state2))\n",
    "print(pattern1.contains_state(state3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4bf75954",
   "metadata": {},
   "source": [
    "# Prime implicants\n",
    "\n",
    "A pattern is an implicant of an exression, if this expression is true for all states in the pattern.\n",
    "An implicant is prime if it is not contained in a more general implicant.\n",
    "The prime implicants of an expression provide a normalized reresentation of the expression, and can\n",
    "be used to optimize some computations.\n",
    "\n",
    "Bokit provides an efficient method to compute all prime implicants of an expression."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "1e8f33d5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Implicants:\n",
      "11--1-0\n",
      "--01--1\n",
      "\n",
      "Primes:\n",
      "11--1-0\n",
      "--01--1\n",
      "11011\n",
      "\n"
     ]
    }
   ],
   "source": [
    "s_implicants = \"\"\"\n",
    "11--1-0\n",
    "--01--1\n",
    "\"\"\"\n",
    "\n",
    "implicants = bokit.Implicants(s_implicants)\n",
    "print(f\"Implicants:\\n{implicants}\")\n",
    "\n",
    "primes = bokit.Primes(s_implicants)\n",
    "print(f\"Primes:\\n{primes}\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "af89a48f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1\n",
       "-10"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Turn an expression into a set of prime implicants\n",
    "pis = bokit.Primes(expr)\n",
    "pis"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "9645dad6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "# The set of prime imnplicants can be also used to evaluate a function\n",
    "print(pis.eval(state1))\n",
    "print(pis.eval(state2))\n",
    "print(pis.eval(state3))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "efd72ee1",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, True)"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# It further enables fuzzy evaluation over a pattern\n",
    "pis.satisfiable_in_pattern(pattern1), pis.satisfiable_in_pattern(pattern2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "417e809f",
   "metadata": {},
   "source": [
    "# Variable groups: human-friendlier display with named variables"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "f66b3ff3",
   "metadata": {},
   "outputs": [],
   "source": [
    "vs = bokit.VarSpace()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "80c796f6",
   "metadata": {},
   "outputs": [],
   "source": [
    "v = vs.provide(\"test\")\n",
    "k = vs.provide(\"other\")\n",
    "v2 = vs.provide(\"other:1\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "f24e7001",
   "metadata": {},
   "outputs": [],
   "source": [
    "mye = vs.parse_expression(\"test | ~other\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "2f4e11cd",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "!__1__ | __0__\n",
      "!other:0 | test\n"
     ]
    }
   ],
   "source": [
    "print( mye )\n",
    "print(vs.display(mye))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "f223ff92",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'!other:0 | test'"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "vs.display(mye)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "4a3fa18a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Variable(1)"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "vs.rename('test', 'valid')\n",
    "vs.set_name(k, 'last')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "fa191e09",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'!last:0 | valid'"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "vs.display(mye)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "ae4b8cb1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Error while parsing as expected\n"
     ]
    }
   ],
   "source": [
    "try:\n",
    "    vs.parse_expression(\"test | ~other & pipo\")\n",
    "    print(\"This should have failed!!\")\n",
    "except:\n",
    "    print(\"Error while parsing as expected\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "71ebc47c",
   "metadata": {},
   "outputs": [],
   "source": [
    "e = vs.parse_expression(\"test | ~(plop | alternate & test)\", True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "d48b7f33",
   "metadata": {},
   "outputs": [],
   "source": [
    "state = vs.parse_state(\"test alternate\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "ff9842ed",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "000101\n"
     ]
    }
   ],
   "source": [
    "print(state)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "adc5fd94",
   "metadata": {},
   "source": [
    "# Multi-valued variables\n",
    "\n",
    "While raw variables are purely Boolean, variable collections let us create ordered groups of associated variables, that can be used to account for multi-valued variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "5671ee08",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'test'"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "v = vs['test']\n",
    "vs.display(v)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "id": "50ec6612",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'test:1'"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Add an associated variable\n",
    "v1 = vs.provide(\"test:1\")\n",
    "vs.display(v1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "id": "f31a8302",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'test:0'"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# The original variable is now associated to order 0\n",
    "vs.display(v)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "id": "a5f3148f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'test:2'"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Add an associated variable to an existing variable\n",
    "v2 = vs.provide(\"test:2\")\n",
    "vs.display(v2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "id": "e1ae6130",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('another:0', 'another:1', 'another:2')"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Renaming affects all variables of the group\n",
    "vs.rename('test', 'another')\n",
    "vs.display(v), vs.display(v1), vs.display(v2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "id": "4675ddc0",
   "metadata": {},
   "outputs": [],
   "source": [
    "vl = vs.get_variables('another')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "id": "289a1da0",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "VarList { varset: VarSet({3}), varlist: [Variable(3)] }"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "vl"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "id": "4ab844cb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "_3_\n",
      "explicit release for a borrowed item\n"
     ]
    }
   ],
   "source": [
    "it = vl.__iter__()\n",
    "for v in it:\n",
    "    print(v)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "id": "06a7c9f1",
   "metadata": {},
   "outputs": [],
   "source": [
    "vl.push(bokit.Variable(27))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "id": "facb6b14",
   "metadata": {},
   "outputs": [],
   "source": [
    "state = vs.parse_state('another')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "id": "1878d0ca",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "_3_\n",
      "_27_\n",
      "explicit release for a borrowed item\n",
      "Dropping a borrowed item\n"
     ]
    }
   ],
   "source": [
    "for v in vl:\n",
    "    print(v)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "id": "79b9a7d6",
   "metadata": {},
   "outputs": [],
   "source": [
    "vl.push(bokit.Variable(42))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "id": "27f32f14",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "_3_\n",
      "_27_\n",
      "_42_\n",
      "explicit release for a borrowed item\n",
      "Dropping a borrowed item\n"
     ]
    }
   ],
   "source": [
    "for v in vl:\n",
    "    print(v)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "id": "437a8943",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "_3_\n",
      "explicit release for a borrowed item\n",
      "Dropping a borrowed item\n"
     ]
    }
   ],
   "source": [
    "for v in state:\n",
    "    print(v)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "id": "a2255771",
   "metadata": {},
   "outputs": [],
   "source": [
    "state.activate(bokit.Variable(12))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "id": "c3df9a6e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Dropping a borrowed item\n",
      "explicit release for a borrowed item\n"
     ]
    }
   ],
   "source": [
    "it = state.__iter__()\n",
    "it.close()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "id": "bac63b74",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "explicit release for a borrowed item\n",
      "Dropping a borrowed item\n"
     ]
    }
   ],
   "source": [
    "l = [v for v in state]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "id": "e973dbe7",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[Variable(3), Variable(12)]"
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "l"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c514427f-f727-4d78-9d37-0f2d2ca7bb1b",
   "metadata": {},
   "source": [
    "## Constraints on range of values\n",
    "\n",
    "Multivalued variables can be used to describe range constraints (inequalities) as Boolean constraints"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "id": "0041a653-9095-4439-b564-59a20f031dd3",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1\n",
      "0\n",
      "\n",
      "__3__\n",
      "__3__\n",
      "\n",
      "__6__\n",
      "!__6__\n",
      "\n",
      "__3__ & !__6__\n"
     ]
    }
   ],
   "source": [
    "print(vs.restrict_range(\"another\", \">=\", 0))\n",
    "print(vs.restrict_range(\"another\", \">\", 10))\n",
    "\n",
    "print()\n",
    "print(vs.restrict_range(\"another\", \">\", 0))\n",
    "print(vs.restrict_range(\"another\", \">=\", 1))\n",
    "\n",
    "print()\n",
    "print(vs.restrict_range(\"another\", \">=\", 2))\n",
    "print(vs.restrict_range(\"another\", \"<\", 2))\n",
    "\n",
    "print()\n",
    "print(vs.restrict_range(\"another\", \"==\", 1))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2e38534e",
   "metadata": {},
   "source": [
    "# Complexity analysis and decomposition\n",
    "\n",
    "The ```estimate_complexity``` method on expressions provides a fast estimation (exploring all expression nodes only once) of the required number of implicants to cover this expression (it is expected to be an upper bound). It returns a report object with the estimated complexity, the number of atoms and max depth of the expression tree.\n",
    "This provides a rough estimate of how hard formal analysis of this expression will be.\n",
    "\n",
    "The ```decompose``` method can then be used to extract selected sub-expressions and replace the single expression with a system of related expressions such that the sum of the complexities is much lower than the complexity of the original expression.\n",
    "It returns a decomposed expression as well as a report on its estimated complexity. \n",
    "\n",
    "This is illustrated on a more complex example in [the decompose notebook](decompose.ipynb)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "id": "559dfbeb",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "ExprComplexity { score: Some(81), atoms: 12, depth: 4 }"
      ]
     },
     "execution_count": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "vs = bokit.VarSpace()\n",
    "e = vs.parse_expression(\"!((A & B & C) | (D & E & F) | (G & H & I) | (J & K & L))\", extend=True)\n",
    "\n",
    "e.estimate_complexity()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "id": "c737bc82-c754-4850-bdb5-7381e5eee3df",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "81"
      ]
     },
     "execution_count": 53,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# In this case, the estimated complexity corresponds to the number of prime implicants\n",
    "pe = bokit.Primes(e)\n",
    "pe.len()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "id": "5bb55268-7b15-4067-9485-30c3f0c72f51",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "DecomposeReport { root_score: 81, sum_sub_score: 0 }\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "!(__0__ & __1__ & __2__ | __3__ & __4__ & __5__ | __6__ & __7__ & __8__ | __9__ & __10__ & __11__)"
      ]
     },
     "execution_count": 54,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# This expression has an acceptable complexity and is not decomposed\n",
    "dc,rep = e.decompose()\n",
    "print(rep)\n",
    "dc"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "id": "0f583135-c5ab-431c-a205-98b391e5f5b3",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "DecomposeReport { root_score: 3, sum_sub_score: 27 }\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "Expanded __12__ & (!__9__ | !__10__ | !__11__)\n",
       "  _12_ <- (!__0__ | !__1__ | !__2__) & (!__3__ | !__4__ | !__5__) & (!__6__ | !__7__ | !__8__)"
      ]
     },
     "execution_count": 55,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# By selecting a lower penalty, we can decompose it\n",
    "dc,rep = e.decompose(50)\n",
    "print(rep)\n",
    "dc"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "id": "48eeca82-477c-49ec-917b-0308cff00482",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(!__0__ | !__1__ | !__2__) & (!__3__ | !__4__ | !__5__) & (!__6__ | !__7__ | !__8__) & (!__9__ | !__10__ | !__11__)"
      ]
     },
     "execution_count": 56,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# A decomposed expression can be merged into a single expression\n",
    "dc.merge()"
   ]
  }
 ],
 "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.9.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}