diff --git a/logic_programming/4_DPLL.ipynb b/logic_programming/4_DPLL.ipynb
index 0e698531f720d8fbb46cacb54d3b65a028b846c0..484cfc0f6bae6d4e2b2ed17ecb93a7c0fe6d71e7 100644
--- a/logic_programming/4_DPLL.ipynb
+++ b/logic_programming/4_DPLL.ipynb
@@ -37,7 +37,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 1,
"id": "964ebd52",
"metadata": {
"vscode": {
@@ -68,7 +68,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 2,
"id": "26e0221b",
"metadata": {
"vscode": {
@@ -106,7 +106,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 3,
"id": "152289b6",
"metadata": {
"vscode": {
@@ -141,7 +141,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 4,
"id": "2c3dd1bf",
"metadata": {
"vscode": {
@@ -180,7 +180,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 5,
"id": "33fc6271",
"metadata": {
"vscode": {
@@ -238,7 +238,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 7,
"id": "06aa608c",
"metadata": {
"vscode": {
@@ -262,7 +262,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 8,
"id": "a76d8b5d",
"metadata": {
"vscode": {
@@ -286,7 +286,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 9,
"id": "d7a0cc62",
"metadata": {
"vscode": {
@@ -318,7 +318,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 10,
"id": "78163b60",
"metadata": {
"vscode": {
@@ -355,7 +355,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 11,
"id": "9d3fbd1a",
"metadata": {
"vscode": {
@@ -415,7 +415,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 12,
"id": "26924712",
"metadata": {
"vscode": {
@@ -438,7 +438,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 13,
"id": "7d90c4ad",
"metadata": {
"vscode": {
@@ -462,7 +462,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 14,
"id": "d4b4e71f",
"metadata": {
"vscode": {
@@ -495,7 +495,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 15,
"id": "3b9c87e4",
"metadata": {
"vscode": {
@@ -519,7 +519,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 16,
"id": "0abd90f6",
"metadata": {
"vscode": {
@@ -543,7 +543,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 17,
"id": "cc81b404",
"metadata": {
"vscode": {
@@ -575,7 +575,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 18,
"id": "57df05f0",
"metadata": {
"vscode": {
@@ -607,7 +607,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 19,
"id": "a36a54a4",
"metadata": {
"vscode": {
@@ -641,7 +641,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 20,
"id": "95fcf64b",
"metadata": {
"vscode": {
@@ -665,7 +665,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 21,
"id": "9c35b0b3",
"metadata": {
"vscode": {
@@ -697,7 +697,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 22,
"id": "56175b0d",
"metadata": {
"vscode": {
@@ -739,7 +739,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 23,
"id": "8259d2d7",
"metadata": {
"vscode": {
@@ -771,7 +771,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 24,
"id": "9e0d83d0",
"metadata": {
"vscode": {
@@ -805,7 +805,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 25,
"id": "25b19d82",
"metadata": {
"vscode": {
@@ -829,7 +829,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 26,
"id": "75a52c4f",
"metadata": {
"vscode": {
@@ -862,7 +862,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 27,
"id": "d8876a92",
"metadata": {
"vscode": {
@@ -894,7 +894,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 28,
"id": "5535384f",
"metadata": {
"vscode": {
@@ -920,7 +920,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 29,
"id": "592fcdd9",
"metadata": {
"vscode": {
@@ -958,7 +958,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 30,
"id": "b8cabba2",
"metadata": {
"vscode": {
@@ -985,7 +985,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 31,
"id": "e369355c",
"metadata": {
"vscode": {
@@ -1010,7 +1010,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 32,
"id": "78764141",
"metadata": {
"vscode": {
@@ -1029,7 +1029,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 33,
"id": "c51455cf",
"metadata": {
"vscode": {
@@ -1063,7 +1063,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 34,
"id": "b0466a5d",
"metadata": {
"vscode": {
@@ -1094,7 +1094,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 35,
"id": "2df16148",
"metadata": {
"vscode": {
@@ -1128,7 +1128,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 36,
"id": "8d8cf76a",
"metadata": {
"vscode": {
@@ -1162,7 +1162,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 37,
"id": "31d1b945",
"metadata": {
"vscode": {
@@ -1339,7 +1339,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 38,
"id": "c51f1ce6",
"metadata": {
"vscode": {
@@ -1373,7 +1373,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 39,
"id": "39bb01e4",
"metadata": {
"vscode": {
@@ -1409,22 +1409,83 @@
"cell_type": "markdown",
"id": "d3ec741b",
"metadata": {},
- "source": []
+ "source": [
+ "Below we show another version of the DPLL algorithm which returns the full decision tree.\n",
+ "It is for education purposes, e.g., to visualise the choices made by the algorithm:"
+ ]
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 40,
"id": "062d6089",
"metadata": {
"vscode": {
"languageId": "prolog"
}
},
+ "outputs": [],
+ "source": [
+ "dpll_tree(Clauses,unit(Lit,Tree),Res) :-\n",
+ " select([Lit],Clauses,Clauses2), % unit clause found\n",
+ " !,\n",
+ " set_literal(Lit,Clauses2,Clauses3),\n",
+ " dpll_tree(Clauses3,Tree,Res).\n",
+ "dpll_tree([],Tree,Res) :- !, Tree=[], Res=sat. % SAT\n",
+ "dpll_tree(Clauses,Tree,Res) :- member([],Clauses),!, Tree=unsat,Res=unsat.\n",
+ "dpll_tree(Clauses,branch(Lit,TreePos,TreeNeg),Res) :-\n",
+ " choose_literal(Clauses,Lit),\n",
+ " !,\n",
+ " set_literal(Lit,Clauses,Clauses1),\n",
+ " dpll_tree(Clauses1,TreePos,Res1),\n",
+ " (Res1=sat\n",
+ " -> TreeNeg=unexplored, Res=sat\n",
+ " ; negate(Lit,NegLit),\n",
+ " set_literal(NegLit,Clauses,Clauses2),\n",
+ " dpll_tree(Clauses2,TreeNeg,Res)\n",
+ " )."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 41,
+ "id": "03d3fe70",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mStr = Knights & Knaves,\n",
+ "Clauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "Tree = branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[]))),\n",
+ "Res = sat"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,Str,Clauses), dpll_tree(Clauses,Tree,Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "id": "5c82bfa1",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
"outputs": [
{
"data": {
"text/plain": [
- "Version 0.8.0-nightly of Jupyter-Prolog-Kernel"
+ "branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))"
]
},
"metadata": {},
@@ -1433,7 +1494,7 @@
{
"data": {
"text/plain": [
- "\u001b[1mtrue"
+ "\u001b[1mTree = branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))"
]
},
"metadata": {},
@@ -1441,26 +1502,63 @@
}
],
"source": [
- "jupyter:version."
+ "?- print($Tree),nl."
]
},
{
"cell_type": "code",
- "execution_count": 2,
- "id": "03d3fe70",
+ "execution_count": 43,
+ "id": "d614588e",
"metadata": {
"vscode": {
"languageId": "prolog"
}
},
"outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 7.0.0 (20221023.0053)\n -->\n<!-- Pages: 1 -->\n<svg width=\"366pt\" height=\"392pt\"\n viewBox=\"0.00 0.00 365.89 392.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 388)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-388 361.89,-388 361.89,4 -4,4\"/>\n<!-- [] -->\n<g id=\"node1\" class=\"node\">\n<title>[]</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"57.74,-123 3.74,-123 3.74,-87 57.74,-87 57.74,-123\"/>\n<text text-anchor=\"middle\" x=\"30.74\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n</g>\n<!-- a -->\n<g id=\"node2\" class=\"node\">\n<title>a</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"31.43,-174.05 33.2,-174.15 34.96,-174.3 36.69,-174.49 38.39,-174.74 40.05,-175.03 41.67,-175.36 43.23,-175.75 44.73,-176.18 46.17,-176.65 47.54,-177.16 48.84,-177.71 50.06,-178.31 51.2,-178.94 52.25,-179.61 53.22,-180.31 54.09,-181.04 54.87,-181.8 55.56,-182.59 56.15,-183.41 56.65,-184.25 57.05,-185.11 57.36,-185.99 57.58,-186.89 57.7,-187.8 57.73,-188.72 57.68,-189.65 57.54,-190.59 57.31,-191.53 57.01,-192.47 56.63,-193.41 56.18,-194.35 55.66,-195.28 55.08,-196.2 54.43,-197.11 53.72,-198.01 52.97,-198.89 52.16,-199.75 51.3,-200.59 50.41,-201.41 49.48,-202.2 48.51,-202.96 47.51,-203.69 46.48,-204.39 45.43,-205.06 44.35,-205.69 43.26,-206.29 42.15,-206.84 41.02,-207.35 39.89,-207.82 38.74,-208.25 37.58,-208.64 36.42,-208.97 35.24,-209.26 34.07,-209.51 32.89,-209.7 31.71,-209.85 30.52,-209.95 29.34,-210 28.15,-210 26.96,-209.95 25.78,-209.85 24.6,-209.7 23.42,-209.51 22.24,-209.26 21.07,-208.97 19.91,-208.64 18.75,-208.25 17.6,-207.82 16.46,-207.35 15.34,-206.84 14.23,-206.29 13.13,-205.69 12.06,-205.06 11.01,-204.39 9.98,-203.69 8.98,-202.96 8.01,-202.2 7.08,-201.41 6.18,-200.59 5.33,-199.75 4.52,-198.89 3.76,-198.01 3.06,-197.11 2.41,-196.2 1.83,-195.28 1.3,-194.35 0.85,-193.41 0.47,-192.47 0.17,-191.53 -0.05,-190.59 -0.19,-189.65 -0.25,-188.72 -0.21,-187.8 -0.09,-186.89 0.13,-185.99 0.43,-185.11 0.84,-184.25 1.34,-183.41 1.93,-182.59 2.62,-181.8 3.4,-181.04 4.27,-180.31 5.24,-179.61 6.29,-178.94 7.43,-178.31 8.65,-177.71 9.94,-177.16 11.31,-176.65 12.75,-176.18 14.26,-175.75 15.82,-175.36 17.44,-175.03 19.1,-174.74 20.79,-174.49 22.53,-174.3 24.28,-174.15 26.06,-174.05 27.85,-174 29.64,-174 31.43,-174.05\"/>\n<text text-anchor=\"middle\" x=\"28.74\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n</g>\n<!-- b -->\n<g id=\"node3\" class=\"node\">\n<title>b</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"179.43,-87.05 181.2,-87.15 182.96,-87.3 184.69,-87.49 186.39,-87.74 188.05,-88.03 189.67,-88.36 191.23,-88.75 192.73,-89.18 194.17,-89.65 195.54,-90.16 196.84,-90.71 198.06,-91.31 199.2,-91.94 200.25,-92.61 201.22,-93.31 202.09,-94.04 202.87,-94.8 203.56,-95.59 204.15,-96.41 204.65,-97.25 205.05,-98.11 205.36,-98.99 205.58,-99.89 205.7,-100.8 205.73,-101.72 205.68,-102.65 205.54,-103.59 205.31,-104.53 205.01,-105.47 204.63,-106.41 204.18,-107.35 203.66,-108.28 203.08,-109.2 202.43,-110.11 201.72,-111.01 200.97,-111.89 200.16,-112.75 199.3,-113.59 198.41,-114.41 197.48,-115.2 196.51,-115.96 195.51,-116.69 194.48,-117.39 193.43,-118.06 192.35,-118.69 191.26,-119.29 190.15,-119.84 189.02,-120.35 187.89,-120.82 186.74,-121.25 185.58,-121.64 184.42,-121.97 183.24,-122.26 182.07,-122.51 180.89,-122.7 179.71,-122.85 178.52,-122.95 177.34,-123 176.15,-123 174.96,-122.95 173.78,-122.85 172.6,-122.7 171.42,-122.51 170.24,-122.26 169.07,-121.97 167.91,-121.64 166.75,-121.25 165.6,-120.82 164.46,-120.35 163.34,-119.84 162.23,-119.29 161.13,-118.69 160.06,-118.06 159.01,-117.39 157.98,-116.69 156.98,-115.96 156.01,-115.2 155.08,-114.41 154.18,-113.59 153.33,-112.75 152.52,-111.89 151.76,-111.01 151.06,-110.11 150.41,-109.2 149.83,-108.28 149.3,-107.35 148.85,-106.41 148.47,-105.47 148.17,-104.53 147.95,-103.59 147.81,-102.65 147.75,-101.72 147.79,-100.8 147.91,-99.89 148.13,-98.99 148.43,-98.11 148.84,-97.25 149.34,-96.41 149.93,-95.59 150.62,-94.8 151.4,-94.04 152.27,-93.31 153.24,-92.61 154.29,-91.94 155.43,-91.31 156.65,-90.71 157.94,-90.16 159.31,-89.65 160.75,-89.18 162.26,-88.75 163.82,-88.36 165.44,-88.03 167.1,-87.74 168.79,-87.49 170.53,-87.3 172.28,-87.15 174.06,-87.05 175.85,-87 177.64,-87 179.43,-87.05\"/>\n<text text-anchor=\"middle\" x=\"176.74\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n</g>\n<!-- c -->\n<g id=\"node4\" class=\"node\">\n<title>c</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"179.43,-0.05 181.2,-0.15 182.96,-0.3 184.69,-0.49 186.39,-0.74 188.05,-1.03 189.67,-1.36 191.23,-1.75 192.73,-2.18 194.17,-2.65 195.54,-3.16 196.84,-3.71 198.06,-4.31 199.2,-4.94 200.25,-5.61 201.22,-6.31 202.09,-7.04 202.87,-7.8 203.56,-8.59 204.15,-9.41 204.65,-10.25 205.05,-11.11 205.36,-11.99 205.58,-12.89 205.7,-13.8 205.73,-14.72 205.68,-15.65 205.54,-16.59 205.31,-17.53 205.01,-18.47 204.63,-19.41 204.18,-20.35 203.66,-21.28 203.08,-22.2 202.43,-23.11 201.72,-24.01 200.97,-24.89 200.16,-25.75 199.3,-26.59 198.41,-27.41 197.48,-28.2 196.51,-28.96 195.51,-29.69 194.48,-30.39 193.43,-31.06 192.35,-31.69 191.26,-32.29 190.15,-32.84 189.02,-33.35 187.89,-33.82 186.74,-34.25 185.58,-34.64 184.42,-34.97 183.24,-35.26 182.07,-35.51 180.89,-35.7 179.71,-35.85 178.52,-35.95 177.34,-36 176.15,-36 174.96,-35.95 173.78,-35.85 172.6,-35.7 171.42,-35.51 170.24,-35.26 169.07,-34.97 167.91,-34.64 166.75,-34.25 165.6,-33.82 164.46,-33.35 163.34,-32.84 162.23,-32.29 161.13,-31.69 160.06,-31.06 159.01,-30.39 157.98,-29.69 156.98,-28.96 156.01,-28.2 155.08,-27.41 154.18,-26.59 153.33,-25.75 152.52,-24.89 151.76,-24.01 151.06,-23.11 150.41,-22.2 149.83,-21.28 149.3,-20.35 148.85,-19.41 148.47,-18.47 148.17,-17.53 147.95,-16.59 147.81,-15.65 147.75,-14.72 147.79,-13.8 147.91,-12.89 148.13,-11.99 148.43,-11.11 148.84,-10.25 149.34,-9.41 149.93,-8.59 150.62,-7.8 151.4,-7.04 152.27,-6.31 153.24,-5.61 154.29,-4.94 155.43,-4.31 156.65,-3.71 157.94,-3.16 159.31,-2.65 160.75,-2.18 162.26,-1.75 163.82,-1.36 165.44,-1.03 167.1,-0.74 168.79,-0.49 170.53,-0.3 172.28,-0.15 174.06,-0.05 175.85,0 177.64,0 179.43,-0.05\"/>\n<text text-anchor=\"middle\" x=\"176.74\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n</g>\n<!-- unsat -->\n<g id=\"node5\" class=\"node\">\n<title>unsat</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"329.64,-87.05 331.56,-87.15 333.45,-87.3 335.32,-87.49 337.16,-87.74 338.95,-88.03 340.69,-88.36 342.38,-88.75 344,-89.18 345.56,-89.65 347.04,-90.16 348.44,-90.71 349.76,-91.31 350.98,-91.94 352.12,-92.61 353.16,-93.31 354.1,-94.04 354.95,-94.8 355.69,-95.59 356.33,-96.41 356.87,-97.25 357.3,-98.11 357.64,-98.99 357.87,-99.89 358,-100.8 358.04,-101.72 357.98,-102.65 357.83,-103.59 357.59,-104.53 357.26,-105.47 356.85,-106.41 356.36,-107.35 355.8,-108.28 355.17,-109.2 354.47,-110.11 353.71,-111.01 352.89,-111.89 352.02,-112.75 351.1,-113.59 350.13,-114.41 349.12,-115.2 348.08,-115.96 347,-116.69 345.89,-117.39 344.75,-118.06 343.59,-118.69 342.41,-119.29 341.21,-119.84 340,-120.35 338.77,-120.82 337.53,-121.25 336.28,-121.64 335.03,-121.97 333.76,-122.26 332.49,-122.51 331.22,-122.7 329.94,-122.85 328.66,-122.95 327.38,-123 326.1,-123 324.82,-122.95 323.54,-122.85 322.27,-122.7 320.99,-122.51 319.73,-122.26 318.46,-121.97 317.2,-121.64 315.95,-121.25 314.72,-120.82 313.49,-120.35 312.27,-119.84 311.07,-119.29 309.89,-118.69 308.73,-118.06 307.6,-117.39 306.49,-116.69 305.41,-115.96 304.36,-115.2 303.35,-114.41 302.39,-113.59 301.47,-112.75 300.59,-111.89 299.78,-111.01 299.02,-110.11 298.32,-109.2 297.68,-108.28 297.12,-107.35 296.64,-106.41 296.23,-105.47 295.9,-104.53 295.66,-103.59 295.51,-102.65 295.45,-101.72 295.49,-100.8 295.62,-99.89 295.85,-98.99 296.18,-98.11 296.62,-97.25 297.16,-96.41 297.8,-95.59 298.54,-94.8 299.38,-94.04 300.33,-93.31 301.37,-92.61 302.5,-91.94 303.73,-91.31 305.05,-90.71 306.45,-90.16 307.93,-89.65 309.48,-89.18 311.11,-88.75 312.79,-88.36 314.54,-88.03 316.33,-87.74 318.16,-87.49 320.03,-87.3 321.93,-87.15 323.85,-87.05 325.78,-87 327.71,-87 329.64,-87.05\"/>\n<text text-anchor=\"middle\" x=\"326.74\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">unsat</text>\n</g>\n<!-- neg(a) -->\n<g id=\"node6\" class=\"node\">\n<title>neg(a)</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"56.74,-297 2.74,-297 2.74,-261 56.74,-261 56.74,-297\"/>\n<text text-anchor=\"middle\" x=\"29.74\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">neg</text>\n</g>\n<!-- neg(a)->a -->\n<g id=\"edge1\" class=\"edge\">\n<title>neg(a)->a</title>\n<path fill=\"none\" stroke=\"black\" d=\"M29.54,-260.8C29.41,-249.58 29.23,-234.67 29.08,-221.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"32.58,-221.94 28.97,-211.98 25.58,-222.02 32.58,-221.94\"/>\n<text text-anchor=\"middle\" x=\"33.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- neg(c) -->\n<g id=\"node7\" class=\"node\">\n<title>neg(c)</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"129.74,-123 75.74,-123 75.74,-87 129.74,-87 129.74,-123\"/>\n<text text-anchor=\"middle\" x=\"102.74\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">neg</text>\n</g>\n<!-- neg(c)->c -->\n<g id=\"edge2\" class=\"edge\">\n<title>neg(c)->c</title>\n<path fill=\"none\" stroke=\"black\" d=\"M117.72,-86.8C128.87,-73.99 144.23,-56.35 156.48,-42.27\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"159.09,-44.61 163.02,-34.77 153.81,-40.01 159.09,-44.61\"/>\n<text text-anchor=\"middle\" x=\"147.24\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- pos(b) -->\n<g id=\"node8\" class=\"node\">\n<title>pos(b)</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"202.74,-210 148.74,-210 148.74,-174 202.74,-174 202.74,-210\"/>\n<text text-anchor=\"middle\" x=\"175.74\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">pos</text>\n</g>\n<!-- pos(b)->b -->\n<g id=\"edge3\" class=\"edge\">\n<title>pos(b)->b</title>\n<path fill=\"none\" stroke=\"black\" d=\"M175.95,-173.8C176.08,-162.58 176.25,-147.67 176.41,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"179.9,-135.02 176.52,-124.98 172.9,-134.94 179.9,-135.02\"/>\n<text text-anchor=\"middle\" x=\"179.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- pos(c) -->\n<g id=\"node9\" class=\"node\">\n<title>pos(c)</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"277.74,-123 223.74,-123 223.74,-87 277.74,-87 277.74,-123\"/>\n<text text-anchor=\"middle\" x=\"250.74\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">pos</text>\n</g>\n<!-- pos(c)->c -->\n<g id=\"edge4\" class=\"edge\">\n<title>pos(c)->c</title>\n<path fill=\"none\" stroke=\"black\" d=\"M235.77,-86.8C224.61,-73.99 209.26,-56.35 197.01,-42.27\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"199.68,-40.01 190.47,-34.77 194.4,-44.61 199.68,-40.01\"/>\n<text text-anchor=\"middle\" x=\"221.24\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- unit(neg(c),[]) -->\n<g id=\"node10\" class=\"node\">\n<title>unit(neg(c),[])</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"129.74,-210 75.74,-210 75.74,-174 129.74,-174 129.74,-210\"/>\n<text text-anchor=\"middle\" x=\"102.74\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">unit</text>\n</g>\n<!-- unit(neg(c),[])->[] -->\n<g id=\"edge6\" class=\"edge\">\n<title>unit(neg(c),[])->[]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M88.17,-173.8C77.99,-161.78 64.22,-145.52 52.71,-131.94\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"55.65,-129.99 46.52,-124.62 50.31,-134.51 55.65,-129.99\"/>\n<text text-anchor=\"middle\" x=\"75.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n<!-- unit(neg(c),[])->neg(c) -->\n<g id=\"edge5\" class=\"edge\">\n<title>unit(neg(c),[])->neg(c)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M102.74,-173.8C102.74,-162.58 102.74,-147.67 102.74,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"106.24,-134.98 102.74,-124.98 99.24,-134.98 106.24,-134.98\"/>\n<text text-anchor=\"middle\" x=\"106.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- unit(pos(b),unit(neg(c),[])) -->\n<g id=\"node11\" class=\"node\">\n<title>unit(pos(b),unit(neg(c),[]))</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"129.74,-297 75.74,-297 75.74,-261 129.74,-261 129.74,-297\"/>\n<text text-anchor=\"middle\" x=\"102.74\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">unit</text>\n</g>\n<!-- unit(pos(b),unit(neg(c),[]))->pos(b) -->\n<g id=\"edge7\" class=\"edge\">\n<title>unit(pos(b),unit(neg(c),[]))->pos(b)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M117.52,-260.8C127.84,-248.78 141.8,-232.52 153.47,-218.94\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"155.9,-221.48 159.76,-211.62 150.59,-216.92 155.9,-221.48\"/>\n<text text-anchor=\"middle\" x=\"146.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- unit(pos(b),unit(neg(c),[]))->unit(neg(c),[]) -->\n<g id=\"edge8\" class=\"edge\">\n<title>unit(pos(b),unit(neg(c),[]))->unit(neg(c),[])</title>\n<path fill=\"none\" stroke=\"black\" d=\"M102.74,-260.8C102.74,-249.58 102.74,-234.67 102.74,-221.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"106.24,-221.98 102.74,-211.98 99.24,-221.98 106.24,-221.98\"/>\n<text text-anchor=\"middle\" x=\"106.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n<!-- unit(pos(b),unit(pos(c),unsat)) -->\n<g id=\"node12\" class=\"node\">\n<title>unit(pos(b),unit(pos(c),unsat))</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"202.74,-297 148.74,-297 148.74,-261 202.74,-261 202.74,-297\"/>\n<text text-anchor=\"middle\" x=\"175.74\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">unit</text>\n</g>\n<!-- unit(pos(b),unit(pos(c),unsat))->pos(b) -->\n<g id=\"edge9\" class=\"edge\">\n<title>unit(pos(b),unit(pos(c),unsat))->pos(b)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M175.74,-260.8C175.74,-249.58 175.74,-234.67 175.74,-221.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"179.24,-221.98 175.74,-211.98 172.24,-221.98 179.24,-221.98\"/>\n<text text-anchor=\"middle\" x=\"179.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- unit(pos(c),unsat) -->\n<g id=\"node13\" class=\"node\">\n<title>unit(pos(c),unsat)</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"277.74,-210 223.74,-210 223.74,-174 277.74,-174 277.74,-210\"/>\n<text text-anchor=\"middle\" x=\"250.74\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">unit</text>\n</g>\n<!-- unit(pos(b),unit(pos(c),unsat))->unit(pos(c),unsat) -->\n<g id=\"edge10\" class=\"edge\">\n<title>unit(pos(b),unit(pos(c),unsat))->unit(pos(c),unsat)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M190.92,-260.8C201.52,-248.78 215.87,-232.52 227.86,-218.94\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"230.34,-221.42 234.33,-211.6 225.09,-216.78 230.34,-221.42\"/>\n<text text-anchor=\"middle\" x=\"220.24\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n<!-- unit(pos(c),unsat)->unsat -->\n<g id=\"edge12\" class=\"edge\">\n<title>unit(pos(c),unsat)->unsat</title>\n<path fill=\"none\" stroke=\"black\" d=\"M266.12,-173.8C277.69,-160.86 293.65,-143.01 306.29,-128.87\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"308.6,-131.54 312.66,-121.76 303.38,-126.88 308.6,-131.54\"/>\n<text text-anchor=\"middle\" x=\"296.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n<!-- unit(pos(c),unsat)->pos(c) -->\n<g id=\"edge11\" class=\"edge\">\n<title>unit(pos(c),unsat)->pos(c)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M250.74,-173.8C250.74,-162.58 250.74,-147.67 250.74,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"254.24,-134.98 250.74,-124.98 247.24,-134.98 254.24,-134.98\"/>\n<text text-anchor=\"middle\" x=\"254.24\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[]))) -->\n<g id=\"node14\" class=\"node\">\n<title>branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))</title>\n<polygon fill=\"none\" stroke=\"black\" points=\"129.74,-384 75.74,-384 75.74,-348 129.74,-348 129.74,-384\"/>\n<text text-anchor=\"middle\" x=\"102.74\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">branch</text>\n</g>\n<!-- branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))->neg(a) -->\n<g id=\"edge13\" class=\"edge\">\n<title>branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))->neg(a)</title>\n<path fill=\"none\" stroke=\"black\" d=\"M87.97,-347.8C77.65,-335.78 63.68,-319.52 52.02,-305.94\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"54.9,-303.92 45.73,-298.62 49.59,-308.48 54.9,-303.92\"/>\n<text text-anchor=\"middle\" x=\"74.24\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n</g>\n<!-- branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))->unit(pos(b),unit(neg(c),[])) -->\n<g id=\"edge15\" class=\"edge\">\n<title>branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))->unit(pos(b),unit(neg(c),[]))</title>\n<path fill=\"none\" stroke=\"black\" d=\"M102.74,-347.8C102.74,-336.58 102.74,-321.67 102.74,-308.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"106.24,-308.98 102.74,-298.98 99.24,-308.98 106.24,-308.98\"/>\n<text text-anchor=\"middle\" x=\"106.24\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n</g>\n<!-- branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))->unit(pos(b),unit(pos(c),unsat)) -->\n<g id=\"edge14\" class=\"edge\">\n<title>branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))->unit(pos(b),unit(pos(c),unsat))</title>\n<path fill=\"none\" stroke=\"black\" d=\"M117.52,-347.8C127.84,-335.78 141.8,-319.52 153.47,-305.94\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"155.9,-308.48 159.76,-298.62 150.59,-303.92 155.9,-308.48\"/>\n<text text-anchor=\"middle\" x=\"146.24\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "digraph {\n",
+ "\"[]\" [shape=\"rect\", label=\"[]\"]\n",
+ "\"a\" [shape=\"egg\", label=\"a\"]\n",
+ "\"b\" [shape=\"egg\", label=\"b\"]\n",
+ "\"c\" [shape=\"egg\", label=\"c\"]\n",
+ "\"unsat\" [shape=\"egg\", label=\"unsat\"]\n",
+ "\"neg(a)\" [shape=\"rect\", label=\"neg\"]\n",
+ "\"neg(c)\" [shape=\"rect\", label=\"neg\"]\n",
+ "\"pos(b)\" [shape=\"rect\", label=\"pos\"]\n",
+ "\"pos(c)\" [shape=\"rect\", label=\"pos\"]\n",
+ "\"unit(neg(c),[])\" [shape=\"rect\", label=\"unit\"]\n",
+ "\"unit(pos(b),unit(neg(c),[]))\" [shape=\"rect\", label=\"unit\"]\n",
+ "\"unit(pos(b),unit(pos(c),unsat))\" [shape=\"rect\", label=\"unit\"]\n",
+ "\"unit(pos(c),unsat)\" [shape=\"rect\", label=\"unit\"]\n",
+ "\"branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))\" [shape=\"rect\", label=\"branch\"]\n",
+ " \"neg(a)\" -> \"a\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"neg(c)\" -> \"c\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"pos(b)\" -> \"b\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"pos(c)\" -> \"c\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(neg(c),[])\" -> \"neg(c)\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(neg(c),[])\" -> \"[]\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(pos(b),unit(neg(c),[]))\" -> \"pos(b)\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(pos(b),unit(neg(c),[]))\" -> \"unit(neg(c),[])\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(pos(b),unit(pos(c),unsat))\" -> \"pos(b)\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(pos(b),unit(pos(c),unsat))\" -> \"unit(pos(c),unsat)\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(pos(c),unsat)\" -> \"pos(c)\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"unit(pos(c),unsat)\" -> \"unsat\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))\" -> \"neg(a)\" [label=\"1\", color=\"black\", style=\"solid\"]\n",
+ " \"branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))\" -> \"unit(pos(b),unit(pos(c),unsat))\" [label=\"2\", color=\"black\", style=\"solid\"]\n",
+ " \"branch(neg(a),unit(pos(b),unit(pos(c),unsat)),unit(pos(b),unit(neg(c),[])))\" -> \"unit(pos(b),unit(neg(c),[]))\" [label=\"3\", color=\"black\", style=\"solid\"]\n",
+ "}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
{
"data": {
"text/plain": [
- "\u001b[1mA = 0,\n",
- "B = 8,\n",
- "C = 0,\n",
- "D = nightly"
+ "\u001b[1mtrue"
]
},
"metadata": {},
@@ -1468,7 +1566,7 @@
}
],
"source": [
- "jupyter:version(A,B,C,D)"
+ "show_term($Tree)"
]
}
],