python: give access to the "product-states" property

* python/spot/impl.i (get_product_states, set_product_states): New.
* tests/python/product.ipynb: Use it.
* NEWS: Mention it.

NEWS

@@ -212,6 +212,11 @@ New in spot 2.4.3.dev (not yet released)
   - The new function spot::check_determinism() sets both
     prop_semi_deterministic() and prop_universal() appropriately.
 
+  Python:
+
+  - The "product-states" property of automata is now accessible via
+    spot.twa.get_product_states() and spot.set.get_product_states().
+
   Deprecation notices:
 
   (These functions still work but compilers emit warnings.)

python/spot/impl.i

@@ -428,8 +428,10 @@ namespace swig
 
 namespace std {
   %template(liststr) list<std::string>;
+  %template(pairunsigned) pair<unsigned, unsigned>;
   %template(vectorformula) vector<spot::formula>;
   %template(vectorunsigned) vector<unsigned>;
+  %template(vectorpairunsigned) vector<pair<unsigned, unsigned>>;
   %template(vectorbool) vector<bool>;
   %template(vectorbdd) vector<bdd>;
   %template(vectorstring) vector<string>;
@@ -465,6 +467,19 @@ namespace std {
        DeprecationWarning)
 %}
 
+// Must occur before the twa declaration
+%typemap(out) SWIGTYPE* spot::twa::get_product_states %{
+  if (!$1)
+    $result = SWIG_Py_Void();
+  else
+    {
+      unsigned sz = $1->size();
+      $result = PyList_New(sz);
+      for (unsigned i = 0; i < sz; ++i)
+        PyList_SetItem($result, i, swig::from((*$1)[i]));
+    }
+%}
+
 %include <spot/twa/twa.hh>
 
 %include <spot/tl/apcollect.hh>
@@ -769,6 +784,21 @@ def state_is_accepting(self, src) -> "bool":
     return self->get_named_prop<std::vector<std::string>>("state-names");
   }
 
+
+  void set_product_states(std::vector<std::pair<unsigned, unsigned>> pairs)
+  {
+    self->set_named_prop("product-states", new
+                         std::vector<std::pair<unsigned,
+                                               unsigned>>(std::move(pairs)));
+  }
+
+  std::vector<std::pair<unsigned, unsigned>>* get_product_states()
+  {
+    return self->get_named_prop
+      <std::vector<std::pair<unsigned, unsigned>>>("product-states");
+  }
+
+
   twa* highlight_state(unsigned state, unsigned color)
   {
     auto hs =

tests/python/product.ipynb

@@ -15,7 +15,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.5.4"
+   "version": "3.6.4"
   },
   "name": ""
  },
@@ -34,6 +34,7 @@
       "spot.setup(show_default='.tavb')\n",
       "\n",
       "def horiz(*args):\n",
+      "    \"\"\"Display multiple arguments side by side in a table.\"\"\"\n",
       "    s = '<table><tr>'\n",
       "    for arg in args:\n",
       "        s += '<td style=\\\"vertical-align: top;\\\">' + arg.data + '</td>'\n",
@@ -1538,9 +1539,7 @@
       "- states are not presented as pairs\n",
       "- the properties of the resulting automaton are not set\n",
       "\n",
-      "The former point can be addressed by calling `set_state_names()` and passing an array of strings: if a state number is smaller than the size of that array, then the string at that position will be displayed instead of the state number in the dot output.  \n",
+      "The former point could be addressed by calling `set_state_names()` and passing an array of strings: if a state number is smaller than the size of that array, then the string at that position will be displayed instead of the state number in the dot output.  However we can do even better by using `set_product_states()` and passing an array of pairs of states.  Besides the output routines, some algorithms actually retrieve this vector of pair of states to work on the product.\n",
-      "\n",
-      "(Note: the original `spot.product()` is in fact *not* naming states.   The `spot.product()` function actually attaches a vector of pairs of integers to the automaton because some algorithms need to project a state of the product onto the original automaton.  The `dot` printer knows how to display those pairs for states that are not named.  Here we shall name states because (1) that is more flexible, and (2) there is a Python interface for this.)\n",
       "\n",
       "Regarding the latter point, consider for instance the deterministic nature of these automata.  In Spot an automaton is deterministic if it is both existential (no universal branching) and universal (no non-deterministic branching).  In our case we will restrict the algorithm to existantial input (by asserting `is_existential()` on both operands), so we can consider that the `prop_universal()` property is an indication of determinism:"
      ]
@@ -1662,7 +1661,7 @@
       "    result.copy_ap_of(left)\n",
       "    result.copy_ap_of(right)\n",
       "    \n",
-      "    names = []   # our array of state names\n",
+      "    pairs = []   # our array of state pairs\n",
       "    sdict = {}\n",
       "    todo = []\n",
       "    def dst(ls, rs):\n",
@@ -1672,7 +1671,7 @@
       "            p = result.new_state()\n",
       "            sdict[pair] = p\n",
       "            todo.append((ls, rs, p))\n",
-      "            names.append(\"{},{}\".format(ls, rs)) # name each state\n",
+      "            pairs.append((ls, rs)) # name each state\n",
       "        return p\n",
       "    \n",
       "    result.set_init_state(dst(left.get_init_state_number(), \n",
@@ -1691,8 +1690,8 @@
       "                    acc = lt.acc | (rt.acc << shift)\n",
       "                    result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)\n",
       "\n",
-      "    # Remember the names of our states\n",
+      "    # Remember the origin of our states\n",
-      "    result.set_state_names(names)\n",
+      "    result.set_product_states(pairs)\n",
       "    \n",
       "    # Loop over all the properties we want to preserve if they hold in both automata\n",
       "    for p in ('prop_universal', 'prop_complete', 'prop_weak', 'prop_inherently_weak', \n",
@@ -2038,6 +2037,218 @@
      ],
      "prompt_number": 9
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "For development, it is useful to know that we can force the automaton printer to show the real state numbers (not the pairs) by passing option `1`, and that we can retrieve the associated pairs ourselves."
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "display(p3.show('.1'))\n",
+      "pairs = p3.get_product_states()\n",
+      "for s in range(p3.num_states()):\n",
+      "    print(\"{}: {}\".format(s, pairs[s]))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"249pt\" viewBox=\"0.00 0.00 592.00 249.00\" width=\"592pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 245)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-245 588,-245 588,4 -4,4\" stroke=\"none\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-126\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-122.3\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.15491,-126C2.79388,-126 17.1543,-126 30.6317,-126\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-126 30.9419,-129.15 34.4419,-126 30.9419,-126 30.9419,-126 30.9419,-126 34.4419,-126 30.9418,-122.85 37.9419,-126 37.9419,-126\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"167.5\" cy=\"-177\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"167.5\" y=\"-173.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M69.3825,-138.379C75.7038,-144.118 83.782,-150.622 92,-155 107.854,-163.447 127.38,-169.06 142.464,-172.501\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"149.476,-174.019 141.968,-175.617 146.055,-173.278 142.635,-172.538 142.635,-172.538 142.635,-172.538 146.055,-173.278 143.301,-169.459 149.476,-174.019 149.476,-174.019\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-186.8\">!b &amp; c</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102.5\" y=\"-171.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
+        "<path d=\"M73.4593,-120.844C88.7526,-117.047 111.706,-113.955 129,-123 141.513,-129.545 150.69,-142.376 156.833,-153.888\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"160.101,-160.457 154.162,-155.593 158.542,-157.323 156.983,-154.19 156.983,-154.19 156.983,-154.19 158.542,-157.323 159.803,-152.787 160.101,-160.457 160.101,-160.457\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"106\" y=\"-140.8\">b</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.5\" y=\"-126.8\">\u2776</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.5\" y=\"-126.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"308\" cy=\"-126\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"308\" y=\"-122.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;2</title>\n",
+        "<path d=\"M72.7114,-118.909C78.6337,-116.574 85.5086,-114.255 92,-113 170.557,-97.8128 193.821,-92.9776 272,-110 276.456,-110.97 281.023,-112.56 285.326,-114.371\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"291.816,-117.34 284.14,-117.292 288.634,-115.884 285.451,-114.428 285.451,-114.428 285.451,-114.428 288.634,-115.884 286.761,-111.563 291.816,-117.34 291.816,-117.34\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"147\" y=\"-105.8\">!b &amp; !c</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
+        "<path d=\"M157.925,-192.541C155.23,-202.909 158.422,-213 167.5,-213 174.45,-213 177.95,-207.085 177.999,-199.659\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"177.075,-192.541 181.1,-199.077 177.526,-196.012 177.977,-199.483 177.977,-199.483 177.977,-199.483 177.526,-196.012 174.853,-199.889 177.075,-192.541 177.075,-192.541\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136.5\" y=\"-230.8\">a &amp; !b &amp; c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"151.5\" y=\"-216.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"167.5\" y=\"-216.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
+        "<path d=\"M185.802,-175.86C207.043,-173.902 243.724,-168.683 272,-155 278.155,-152.021 284.154,-147.736 289.397,-143.371\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"294.76,-138.66 291.58,-145.646 292.131,-140.97 289.501,-143.279 289.501,-143.279 289.501,-143.279 292.131,-140.97 287.422,-140.912 294.76,-138.66 294.76,-138.66\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206\" y=\"-191.8\">a &amp; !b &amp; !c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231\" y=\"-176.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"560\" cy=\"-122\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"560\" y=\"-118.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
+        "<path d=\"M180.347,-189.973C187.141,-196.432 196.244,-203.578 206,-207 247.446,-221.538 369.129,-210.747 458,-192 488.395,-185.588 498.955,-187.376 524,-169 533.197,-162.252 541.052,-152.399 546.976,-143.455\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"550.762,-137.458 549.689,-145.059 548.893,-140.417 547.025,-143.377 547.025,-143.377 547.025,-143.377 548.893,-140.417 544.361,-141.696 550.762,-137.458 550.762,-137.458\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"363.5\" y=\"-226.8\">b</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"344\" y=\"-212.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"360\" y=\"-212.8\">\u2776</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"376\" y=\"-212.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
+        "<path d=\"M290.514,-120.823C269.563,-115.249 232.892,-108.934 206,-123 193.487,-129.545 184.31,-142.376 178.167,-153.888\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.899,-160.457 175.197,-152.787 176.458,-157.323 178.017,-154.19 178.017,-154.19 178.017,-154.19 176.458,-157.323 180.838,-155.593 174.899,-160.457 174.899,-160.457\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"208\" y=\"-140.8\">a &amp; !b &amp; c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223\" y=\"-126.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239\" y=\"-126.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
+        "<path d=\"M297.849,-141.167C294.772,-151.664 298.156,-162 308,-162 315.537,-162 319.287,-155.941 319.25,-148.39\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"318.151,-141.167 322.318,-147.614 318.678,-144.627 319.204,-148.087 319.204,-148.087 319.204,-148.087 318.678,-144.627 316.09,-148.561 318.151,-141.167 318.151,-141.167\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"275\" y=\"-180.8\">a &amp; !b &amp; !c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"300\" y=\"-165.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>2-&gt;3</title>\n",
+        "<path d=\"M324.94,-132.618C361.385,-146.743 453.12,-176.549 524,-151 530.542,-148.642 536.728,-144.471 542.027,-140.014\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"547.404,-135.139 544.334,-142.174 544.811,-137.49 542.218,-139.841 542.218,-139.841 542.218,-139.841 544.811,-137.49 540.102,-137.507 547.404,-135.139 547.404,-135.139\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"417\" y=\"-177.8\">b &amp; c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"410\" y=\"-163.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"426\" y=\"-163.8\">\u2776</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"442\" y=\"-163.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"434\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"434\" y=\"-14.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>2-&gt;4</title>\n",
+        "<path d=\"M322.27,-114.442C344.459,-95.1167 389.141,-56.1998 414.437,-34.1681\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"419.825,-29.4748 416.616,-36.4477 417.186,-31.7735 414.547,-34.0723 414.547,-34.0723 414.547,-34.0723 417.186,-31.7735 412.478,-31.6969 419.825,-29.4748 419.825,-29.4748\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"349.5\" y=\"-111.8\">b &amp; !c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"352\" y=\"-97.8\">\u24ff</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368\" y=\"-97.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
+        "<path d=\"M554.644,-139.41C553.644,-149.088 555.43,-158 560,-158 563.356,-158 565.211,-153.194 565.563,-146.807\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"565.356,-139.41 568.701,-146.319 565.454,-142.909 565.552,-146.407 565.552,-146.407 565.552,-146.407 565.454,-142.909 562.403,-146.495 565.356,-139.41 565.356,-139.41\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"541.5\" y=\"-175.8\">!b &amp; c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"544\" y=\"-161.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"560\" y=\"-161.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge13\"><title>3-&gt;3</title>\n",
+        "<path d=\"M551.925,-138.318C545.824,-159.036 548.516,-186 560,-186 570.228,-186 573.482,-164.612 569.761,-145.297\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"568.075,-138.318 572.781,-144.382 568.897,-141.72 569.719,-145.122 569.719,-145.122 569.719,-145.122 568.897,-141.72 566.657,-145.862 568.075,-138.318 568.075,-138.318\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"555.5\" y=\"-203.8\">b</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"536\" y=\"-189.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"552\" y=\"-189.8\">\u2776</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"568\" y=\"-189.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge14\"><title>3-&gt;4</title>\n",
+        "<path d=\"M558.767,-103.826C557.363,-79.8765 550.913,-38.5086 524,-19 505.251,-5.40945 477.956,-7.38732 458.544,-11.3639\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"451.524,-12.9575 457.653,-8.33586 454.938,-12.1826 458.351,-11.4077 458.351,-11.4077 458.351,-11.4077 454.938,-12.1826 459.048,-14.4795 451.524,-12.9575 451.524,-12.9575\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"479.5\" y=\"-37.8\">!b &amp; !c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"492\" y=\"-22.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge15\"><title>4-&gt;3</title>\n",
+        "<path d=\"M439.138,-35.4338C444.487,-54.1502 455.631,-83.4228 476,-100 492.592,-113.503 516.662,-118.781 534.614,-120.811\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"541.893,-121.497 534.628,-123.977 538.408,-121.169 534.924,-120.841 534.924,-120.841 534.924,-120.841 538.408,-121.169 535.22,-117.704 541.893,-121.497 541.893,-121.497\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"481.5\" y=\"-136.8\">!b &amp; c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"484\" y=\"-122.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"500\" y=\"-122.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge16\"><title>4-&gt;3</title>\n",
+        "<path d=\"M448.032,-29.3018C455.793,-35.6525 466.043,-43.4025 476,-49 496,-60.2437 506.251,-53.4607 524,-68 534.306,-76.4424 542.605,-88.7369 548.531,-99.4628\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"551.91,-105.89 545.864,-101.16 550.281,-102.792 548.653,-99.6944 548.653,-99.6944 548.653,-99.6944 550.281,-102.792 551.441,-98.2283 551.91,-105.89 551.91,-105.89\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"483\" y=\"-85.8\">b &amp; c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"476\" y=\"-71.8\">\u24ff</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"492\" y=\"-71.8\">\u2776</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"508\" y=\"-71.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge17\"><title>4-&gt;4</title>\n",
+        "<path d=\"M428.152,-35.0373C426.959,-44.8579 428.908,-54 434,-54 437.819,-54 439.87,-48.8576 440.153,-42.1433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"439.848,-35.0373 443.296,-41.8954 439.998,-38.5341 440.149,-42.0308 440.149,-42.0308 440.149,-42.0308 439.998,-38.5341 437.002,-42.1663 439.848,-35.0373 439.848,-35.0373\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"413.5\" y=\"-72.8\">!b &amp; !c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"426\" y=\"-57.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge18\"><title>4-&gt;4</title>\n",
+        "<path d=\"M425.326,-33.947C418.347,-55.2861 421.238,-84 434,-84 445.416,-84 448.933,-61.0236 444.553,-40.9026\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"442.674,-33.947 447.54,-39.8834 443.587,-37.3259 444.499,-40.7048 444.499,-40.7048 444.499,-40.7048 443.587,-37.3259 441.458,-41.5263 442.674,-33.947 442.674,-33.947\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"415.5\" y=\"-101.8\">b &amp; !c</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"418\" y=\"-87.8\">\u24ff</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"434\" y=\"-87.8\">\u2777</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      },
+      {
+       "output_type": "stream",
+       "stream": "stdout",
+       "text": [
+        "0: (1, 0)\n",
+        "1: (0, 0)\n",
+        "2: (0, 1)\n",
+        "3: (2, 0)\n",
+        "4: (2, 1)\n"
+       ]
+      }
+     ],
+     "prompt_number": 10
+    },
     {
      "cell_type": "markdown",
      "metadata": {},
@@ -2060,11 +2271,11 @@
        "output_type": "stream",
        "stream": "stdout",
        "text": [
-        "1000 loops, best of 3: 216 \u00b5s per loop\n"
+        "1000 loops, best of 3: 231 \u00b5s per loop\n"
        ]
       }
      ],
-     "prompt_number": 10
+     "prompt_number": 11
     },
     {
      "cell_type": "code",
@@ -2079,12 +2290,12 @@
        "output_type": "stream",
        "stream": "stdout",
        "text": [
-        "The slowest run took 4.86 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
+        "The slowest run took 5.96 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
-        "100000 loops, best of 3: 10.3 \u00b5s per loop\n"
+        "100000 loops, best of 3: 4.6 \u00b5s per loop\n"
        ]
       }
      ],
-     "prompt_number": 11
+     "prompt_number": 12
     },
     {
      "cell_type": "markdown",