diff --git a/notebooks/presentations/LPOP18.ipynb b/notebooks/presentations/LPOP18.ipynb
index 87f6ef68ef1f3bc9062ac2eadfedd6fa78bfa35c..6d2b2fcd648223cb15c4858f30a14ac0a9ab1170 100644
--- a/notebooks/presentations/LPOP18.ipynb
+++ b/notebooks/presentations/LPOP18.ipynb
@@ -499,7 +499,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 30,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -507,21 +507,16 @@
},
"outputs": [
{
- "data": {
- "text/markdown": [
- "$\\{(\\mathit{thomas}\\mapsto \\mathit{thomas}),(\\mathit{thomas}\\mapsto \\mathit{gordon}),(\\mathit{gordon}\\mapsto \\mathit{gordon})\\}$"
- ],
- "text/plain": [
- "{(thomas↦thomas),(thomas↦gordon),(gordon↦gordon)}"
- ]
- },
- "execution_count": 15,
- "metadata": {},
- "output_type": "execute_result"
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: Computation not completed: Unknown identifier \"thomas\",Unknown identifier \"gordon\",Unknown identifier \"gordon\",Unknown identifier \"gordon\",Unknown identifier \"thomas\",Unknown identifier \"thomas\"",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"thomas\",Unknown identifier \"gordon\",Unknown identifier \"gordon\",Unknown identifier \"gordon\",Unknown identifier \"thomas\",Unknown identifier \"thomas\"\u001b[0m"
+ ]
}
],
"source": [
- "{ thomas|->gordon, gordon|->gordon, thomas|->thomas}"
+ "{ thomas↦gordon, gordon↦gordon, thomas↦thomas}"
]
},
{
@@ -603,6 +598,146 @@
"The above relation is a subset of ```Trains * Trains```."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: DOT_ENGINE = circo\n"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref DOT_ENGINE=circo"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "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 2.28.0 (20110509.1545)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"243pt\" height=\"235pt\"\n",
+ " viewBox=\"0.00 0.00 243.39 234.72\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 230.72)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-230.72 240.386,-230.72 240.386,5 -4,5\"/>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>5</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.103,-36 112.103,-36 112.103,-0 166.103,-0 166.103,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.103\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"235.386,-131.36 181.386,-131.36 181.386,-95.3602 235.386,-95.3602 235.386,-131.36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"208.386\" y=\"-109.16\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 5->4 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>5->4</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M152.461,-36.3864C162.879,-50.7254 177.49,-70.8353 189.165,-86.9044\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"186.594,-89.3207 195.303,-95.3536 192.257,-85.2062 186.594,-89.3207\"/>\n",
+ "<text text-anchor=\"middle\" x=\"179.813\" y=\"-50.4454\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-190.296 1.42109e-14,-190.296 1.42109e-14,-154.296 54,-154.296 54,-190.296\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-168.096\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 5->3 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>5->3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M126.024,-36.0017C106.385,-63.0326 69.1556,-114.274 46.3626,-145.646\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"43.3895,-143.783 40.3432,-153.931 49.0526,-147.898 43.3895,-143.783\"/>\n",
+ "<text text-anchor=\"middle\" x=\"95.1931\" y=\"-93.6237\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node7\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.103,-226.72 112.103,-226.72 112.103,-190.72 166.103,-190.72 166.103,-226.72\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.103\" y=\"-204.52\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 5->2 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>5->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M139.103,-36.2871C139.103,-69.6799 139.103,-140.734 139.103,-180.418\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"135.603,-180.489 139.103,-190.489 142.603,-180.489 135.603,-180.489\"/>\n",
+ "<text text-anchor=\"middle\" x=\"131.103\" y=\"-104.152\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node9\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-72.4243 0,-72.4243 0,-36.4243 54,-36.4243 54,-72.4243\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-50.2243\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 5->1 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>5->1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M111.966,-26.8173C97.6137,-31.4806 79.779,-37.2754 64.1603,-42.3502\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"62.7045,-39.143 54.2756,-45.562 64.8677,-45.8004 62.7045,-39.143\"/>\n",
+ "<text text-anchor=\"middle\" x=\"91.063\" y=\"-40.3838\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 4->3 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>4->3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.231,-122.183C150.018,-132.325 98.6277,-149.023 63.8291,-160.33\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"62.4733,-157.09 54.0443,-163.509 64.6364,-163.747 62.4733,-157.09\"/>\n",
+ "<text text-anchor=\"middle\" x=\"125.53\" y=\"-147.056\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 4->2 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>4->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M195.027,-131.747C184.609,-146.086 169.999,-166.196 158.324,-182.265\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"155.231,-180.566 152.185,-190.714 160.895,-184.681 155.231,-180.566\"/>\n",
+ "<text text-anchor=\"middle\" x=\"185.676\" y=\"-159.806\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 4->1 -->\n",
+ "<g id=\"edge14\" class=\"edge\"><title>4->1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.231,-104.537C150.018,-94.3953 98.6277,-77.6976 63.8291,-66.3908\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"64.6364,-62.9731 54.0443,-63.2116 62.4733,-69.6305 64.6364,-62.9731\"/>\n",
+ "<text text-anchor=\"middle\" x=\"119.53\" y=\"-91.2639\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 3->2 -->\n",
+ "<g id=\"edge16\" class=\"edge\"><title>3->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.1369,-181.113C68.4889,-185.777 86.3236,-191.571 101.942,-196.646\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"101.235,-200.096 111.827,-199.858 103.398,-193.439 101.235,-200.096\"/>\n",
+ "<text text-anchor=\"middle\" x=\"81.0396\" y=\"-174.68\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 3->1 -->\n",
+ "<g id=\"edge18\" class=\"edge\"><title>3->1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M27,-154.137C27,-135.157 27,-105.11 27,-82.9567\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"30.5001,-82.7983 27,-72.7983 23.5001,-82.7983 30.5001,-82.7983\"/>\n",
+ "<text text-anchor=\"middle\" x=\"35\" y=\"-114.347\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge20\" class=\"edge\"><title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M126.024,-190.719C106.385,-163.688 69.1556,-112.447 46.3626,-81.0746\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"49.0526,-78.8226 40.3432,-72.7896 43.3895,-82.9371 49.0526,-78.8226\"/>\n",
+ "<text text-anchor=\"middle\" x=\"77.1931\" y=\"-138.697\" font-family=\"Times,serif\" font-size=\"14.00\">k5</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"k5\",{x,y|x:1..5 & y:1..5 & x>y})]>"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"k5\",{x,y|x:1..5 & y:1..5 & x>y})"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -634,7 +769,7 @@
}
],
"source": [
- "{ thomas|->1, gordon|->2}"
+ "{ thomas↦1, gordon↦2}"
]
},
{
@@ -664,7 +799,7 @@
}
],
"source": [
- "[4,5,6] = {1|->4, 2|->5, 3|->6}"
+ "[4,5,6] = {1↦4, 2↦5, 3↦6}"
]
},
{
@@ -1255,7 +1390,7 @@
],
"source": [
" {S,E,N,D, M,O,R, Y |\n",
- " {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n",
+ " {S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 & \n",
" card({S,E,N,D, M,O,R, Y}) = 8 & \n",
" S*1000 + E*100 + N*10 + D +\n",
" M*1000 + O*100 + R*10 + E =\n",
@@ -1286,7 +1421,7 @@
],
"source": [
":table {S,E,N,D, M,O,R, Y |\n",
- " {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n",
+ " {S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 & \n",
" card({S,E,N,D, M,O,R, Y}) = 8 & \n",
" S*1000 + E*100 + N*10 + D +\n",
" M*1000 + O*100 + R*10 + E =\n",
@@ -1343,13 +1478,43 @@
}
],
"source": [
- " {K,P} <: 1..9 &\n",
- " {I,S,A,O,N} <: 0..9 &\n",
+ " {K,P} ⊆ 1..9 &\n",
+ " {I,S,A,O,N} ⊆ 0..9 &\n",
" (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) \n",
" = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &\n",
" card({K, I, S, P, A, O, N}) = 7"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|K|I|S|P|A|O|N|\n",
+ "|---|---|---|---|---|---|---|\n",
+ "|$2$|$0$|$3$|$4$|$1$|$8$|$9$|\n"
+ ],
+ "text/plain": [
+ "K\tI\tS\tP\tA\tO\tN\n",
+ "2\t0\t3\t4\t1\t8\t9\n"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {K,I,S,P,A,O,N | {K,P} ⊆ 1..9 &\n",
+ " {I,S,A,O,N} ⊆ 0..9 &\n",
+ " (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) \n",
+ " = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &\n",
+ " card({K, I, S, P, A, O, N}) = 7}"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -1399,16 +1564,16 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "Execution time: 0.020736936 seconds"
+ "Execution time: 0.113811662 seconds"
],
"text/plain": [
- "Execution time: 0.020736936 seconds"
+ "Execution time: 0.113811662 seconds"
]
},
"metadata": {},
@@ -1431,15 +1596,15 @@
"\tn = 8"
]
},
- "execution_count": 5,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":time :solve prob n=8 &\n",
- " queens : perm(1..n) &\n",
- " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
+ " queens ∈ perm(1..n) &\n",
+ " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
]
},
{
@@ -1601,7 +1766,7 @@
"source": [
":time :solve prob n=20 &\n",
" queens : perm(1..n) &\n",
- " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
+ " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
]
},
{
@@ -1646,7 +1811,7 @@
"source": [
":time :solve kodkod n=13 &\n",
" queens : 1..n >-> 1..n &\n",
- " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
+ " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
]
},
{
@@ -1666,7 +1831,7 @@
"source": [
":time :solve z3 n=8 &\n",
" queens : perm(1..n) &\n",
- " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
+ " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))"
]
},
{
@@ -1956,17 +2121,17 @@
},
{
"cell_type": "code",
- "execution_count": 63,
+ "execution_count": 39,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$TRUE$\n",
+ "$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $x = \\{1\\}$\n",
- "* $y = \\{1,2\\}$"
+ "* $\\mathit{x} = \\{1\\}$\n",
+ "* $\\mathit{y} = \\{1,2\\}$"
],
"text/plain": [
"TRUE\n",
@@ -1976,13 +2141,13 @@
"\ty = {1,2}"
]
},
- "execution_count": 63,
+ "execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":solve kodkod x <: 1..2 & y<: 1..2 & x \\/ y = 1..2 & 1:x & x <<: y"
+ ":solve kodkod x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y"
]
},
{
@@ -2032,16 +2197,16 @@
},
{
"cell_type": "code",
- "execution_count": 65,
+ "execution_count": 36,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$TRUE$\n",
+ "$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $x = \\{\\{100\\},\\{1\\}\\}$"
+ "* $\\mathit{x} = \\{\\{100\\},\\{1\\}\\}$"
],
"text/plain": [
"TRUE\n",
@@ -2050,13 +2215,13 @@
"\tx = {{100},{1}}"
]
},
- "execution_count": 65,
+ "execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x)"
+ "x ⊆ POW(1..100) & {100}∈x & ∀y.(y∈x ⇒ {card(y)}:x)"
]
},
{
@@ -2072,16 +2237,16 @@
},
{
"cell_type": "code",
- "execution_count": 66,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$TRUE$\n",
+ "$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $x = \\{\\{100\\},\\{50,100\\},\\{25,50,100\\},\\{12,25,50,100\\},\\{6,12,25,50,100\\},\\{3,6,12,25,50,100\\},\\{1,3,6,12,25,50,100\\},\\{0,1,3,6,12,25,50,100\\}\\}$"
+ "* $\\mathit{x} = \\{\\{100\\},\\{50,100\\},\\{25,50,100\\},\\{12,25,50,100\\},\\{6,12,25,50,100\\},\\{3,6,12,25,50,100\\},\\{1,3,6,12,25,50,100\\},\\{0,1,3,6,12,25,50,100\\}\\}$"
],
"text/plain": [
"TRUE\n",
@@ -2090,13 +2255,13 @@
"\tx = {{100},{50,100},{25,50,100},{12,25,50,100},{6,12,25,50,100},{3,6,12,25,50,100},{1,3,6,12,25,50,100},{0,1,3,6,12,25,50,100}}"
]
},
- "execution_count": 66,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "{100}:x & !y.(y:x => (!z.(z:y => y \\/ {z / 2}:x)))"
+ "{100}∈x & ∀y.(y∈x ⇒ (∀z.(z∈y ⇒ y ∪ {z / 2}∈x)))"
]
},
{