diff --git a/notebooks/experiments/SMT_Translation_Experiments.ipynb b/notebooks/experiments/SMT_Translation_Experiments.ipynb
index 40c0aa6bc85c32ec9b846c521aa07f0a027d0c4a..b200fa719ec5f6dad3e10ccc958bc718008a9158 100644
--- a/notebooks/experiments/SMT_Translation_Experiments.ipynb
+++ b/notebooks/experiments/SMT_Translation_Experiments.ipynb
@@ -27,6 +27,24 @@
":solve z3 f = {1|->3, 2|->6} & r = f~[{6}]"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":solve z3 f = {1|->3, 2|->6} & r = f~[{6}] & not(r={2})"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -172,6 +190,61 @@
"```"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "This is not using the set datatype but functions to bool."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":solve z3 f:(INTEGER*INTEGER)-->BOOL & \n",
+ "f = ((INTEGER*INTEGER)*{FALSE}) <+ {(1,3,TRUE),(2,6,TRUE)} &\n",
+ "r:INTEGER-->BOOL & !x1.(x1:INTEGER => (x1|->TRUE:r <=> (x|->6)|->TRUE:f))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "What we get in probcli REPL:\n",
+ "unsupported_type_or_expression(comprehension_set([b(identifier(_smt_tmp30),couple(integer,integer),[]),b(identifier(_smt_tmp31),boolean,[])],b(conjunct(b(member(b(couple(b(identifier(_smt_tmp30),couple(integer,integer),[]),b(identifier(_smt_tmp31),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier(_smt_tmp33),couple(integer,integer),[]),b(identifier(_smt_tmp32),boolean,[])],b(conjunct(b(exists([b(identifier(_smt_tmp36)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":solve z3 f:(INTEGER*INTEGER)-->BOOL & \n",
+ "f = ((INTEGER*INTEGER)*{FALSE}) <+ {(1,3,TRUE),(2,6,TRUE)} &\n",
+ "r:INTEGER-->BOOL & !x1.(x1:INTEGER => (x1|->TRUE:r <=> (x|->6)|->TRUE:f)) & not(2|->TRUE:r)"
+ ]
+ },
{
"cell_type": "code",
"execution_count": null,
diff --git a/notebooks/presentations/SETS_RODIN18.ipynb b/notebooks/presentations/SETS_RODIN18.ipynb
index dba64d2a14c959093ccb6128c719098cae601456..f9479ae876cd0068e3cc72b8e2f6d6cb7cfa0b92 100644
--- a/notebooks/presentations/SETS_RODIN18.ipynb
+++ b/notebooks/presentations/SETS_RODIN18.ipynb
@@ -9,6 +9,8 @@
},
"source": [
"# Solving (Set) Constraints in B and Event-B #\n",
+ "Michael Leuschel,\n",
+ "David Geleßus (Jupyter Interface)\n",
"\n",
"## A quick Introduction to B ##"
]
@@ -37,7 +39,7 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 3,
"metadata": {
"slideshow": {
"slide_type": "subslide"
@@ -50,7 +52,7 @@
"{FALSE,TRUE}"
]
},
- "execution_count": 1,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -61,7 +63,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 4,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -74,7 +76,7 @@
"\"this is a string\""
]
},
- "execution_count": 2,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -85,7 +87,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 5,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -98,7 +100,7 @@
"1024"
]
},
- "execution_count": 3,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -121,7 +123,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 74,
"metadata": {
"slideshow": {
"slide_type": "-"
@@ -132,11 +134,11 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 17:10:21,614, T+7877565] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 17:10:22,773, T+7878724] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57165\n",
- "[2018-06-04 17:10:22,774, T+7878725] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52908\n",
- "[2018-06-04 17:10:22,782, T+7878733] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 17:10:22,792, T+7878743] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
+ "[2018-06-05 11:26:25,674, T+11556688] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
+ "[2018-06-05 11:26:26,811, T+11557825] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54552\n",
+ "[2018-06-05 11:26:26,812, T+11557826] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 61500\n",
+ "[2018-06-05 11:26:26,814, T+11557828] \"ProB Output Logger for instance 78644ca9\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-06-05 11:26:26,833, T+11557847] \"ProB Output Logger for instance 78644ca9\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
]
},
{
@@ -145,7 +147,7 @@
"Loaded machine: MyBasicSets : []\n"
]
},
- "execution_count": 14,
+ "execution_count": 74,
"metadata": {},
"output_type": "execute_result"
}
@@ -159,7 +161,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -168,7 +170,7 @@
"{thomas,gordon}"
]
},
- "execution_count": 5,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -190,7 +192,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 8,
"metadata": {
"slideshow": {
"slide_type": "-"
@@ -203,7 +205,7 @@
"{Points1,Points2}"
]
},
- "execution_count": 6,
+ "execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@@ -226,7 +228,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 9,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -239,7 +241,7 @@
"(thomas↦10)"
]
},
- "execution_count": 7,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -250,7 +252,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 10,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -263,7 +265,7 @@
"(thomas↦10)"
]
},
- "execution_count": 8,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -285,7 +287,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 11,
"metadata": {},
"outputs": [
{
@@ -294,7 +296,7 @@
"((thomas↦gordon)↦20)"
]
},
- "execution_count": 9,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -312,20 +314,9 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "rec(length∈20,position∈10302,train∈thomas)"
- ]
- },
- "execution_count": 15,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"rec(train:thomas,length:20,position:10302)"
]
@@ -345,7 +336,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 12,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -358,7 +349,7 @@
"{1,2,3}"
]
},
- "execution_count": 10,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -380,7 +371,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 13,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -393,7 +384,7 @@
"{1,2,3}"
]
},
- "execution_count": 11,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -411,20 +402,9 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(((({FALSE,TRUE}↦INTEGER)↦STRING)↦{thomas,gordon})↦{Points1,Points2})"
- ]
- },
- "execution_count": 12,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"(BOOL,INTEGER,STRING,Trains,Points)"
]
@@ -442,7 +422,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 14,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -455,7 +435,7 @@
"{1,2,3}"
]
},
- "execution_count": 13,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -484,7 +464,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 15,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -497,7 +477,7 @@
"{{0,1},{1,2,3}}"
]
},
- "execution_count": 14,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -555,20 +535,9 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "{(thomas↦thomas),(thomas↦gordon),(gordon↦thomas),(gordon↦gordon)}"
- ]
- },
- "execution_count": 17,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"Trains * Trains"
]
@@ -586,7 +555,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 17,
"metadata": {},
"outputs": [
{
@@ -595,7 +564,7 @@
"{(thomas↦1),(gordon↦2)}"
]
},
- "execution_count": 18,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -630,7 +599,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 18,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -643,7 +612,7 @@
"10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376"
]
},
- "execution_count": 19,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -666,7 +635,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 19,
"metadata": {},
"outputs": [
{
@@ -675,7 +644,7 @@
"{1,7,8,9,10}"
]
},
- "execution_count": 20,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -686,7 +655,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 20,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -699,7 +668,7 @@
"{1,7,8,9,10}"
]
},
- "execution_count": 21,
+ "execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@@ -727,7 +696,7 @@
{
"data": {
"text/plain": [
- "{1,2}"
+ "{thomas,gordon}"
]
},
"execution_count": 22,
@@ -736,7 +705,7 @@
}
],
"source": [
- "ran({(thomas↦1),(gordon↦2)})"
+ "dom({(thomas↦1),(gordon↦2)})"
]
},
{
@@ -752,15 +721,26 @@
},
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 77,
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
- "outputs": [],
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: NOT-WELL-DEFINED: \nFunction applied outside of domain (#8): Function argument: thomas, function value: {}\n ### Line: 1, Column: 0 until 21\n\n",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
+ "\u001b[1m\u001b[31mFunction applied outside of domain (#8): Function argument: thomas, function value: {}\u001b[0m",
+ "\u001b[1m\u001b[31m ### Line: 1, Column: 0 until 21\u001b[0m"
+ ]
+ }
+ ],
"source": [
- "{(thomas↦1),(gordon↦2)} (thomas)"
+ "{(gordon↦2)} (thomas)"
]
},
{
@@ -776,13 +756,24 @@
},
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 24,
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
- "outputs": [],
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{gordon}"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
"source": [
"{(thomas↦1),(gordon↦2)}~[2..3]"
]
@@ -801,7 +792,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 26,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -814,7 +805,7 @@
"FALSE"
]
},
- "execution_count": 23,
+ "execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
@@ -825,7 +816,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 27,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -838,7 +829,7 @@
"TRUE"
]
},
- "execution_count": 24,
+ "execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
@@ -861,7 +852,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 28,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -877,7 +868,7 @@
"\tx = −10"
]
},
- "execution_count": 25,
+ "execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
@@ -900,7 +891,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 29,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -913,7 +904,7 @@
"{−10,10}"
]
},
- "execution_count": 26,
+ "execution_count": 29,
"metadata": {},
"output_type": "execute_result"
}
@@ -954,7 +945,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 32,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -963,17 +954,20 @@
"outputs": [
{
"data": {
+ "text/latex": [
+ "$\\exists \\mathit{x}\\cdot (\\mathit{x} \\in \\mathbb N \\wedge \\mathit{x} * \\mathit{x} = 1000)$"
+ ],
"text/plain": [
- "FALSE"
+ "∃x·(x ∈ ℕ ∧ x * x = 1000)"
]
},
- "execution_count": 27,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "x*x=1000"
+ ":prettyprint #x.(x:NATURAL & x*x=1000)"
]
},
{
@@ -1018,7 +1012,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -1033,7 +1027,7 @@
"\tt2 = gordon"
]
},
- "execution_count": 28,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -1046,20 +1040,9 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 29,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"train_position = {thomas|->2019, gordon|->2020} &\n",
"t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &\n",
@@ -1080,7 +1063,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -1095,7 +1078,7 @@
"\tt2 = gordon"
]
},
- "execution_count": 30,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
@@ -1106,6 +1089,36 @@
"x:1..(train_position(t2)-train_position(t1)-1)"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Nr|x|y|\n",
+ "|---|---|---|\n",
+ "|1|TRUE|1|\n",
+ "|2|TRUE|2|\n",
+ "|3|TRUE|3|\n"
+ ],
+ "text/plain": [
+ "Nr\tx\ty\n",
+ "1\tTRUE\t1\n",
+ "2\tTRUE\t2\n",
+ "3\tTRUE\t3\n"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {x,y|x=TRUE & y:1..3}"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -1125,7 +1138,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 36,
"metadata": {},
"outputs": [
{
@@ -1134,13 +1147,15 @@
"FALSE"
]
},
- "execution_count": 31,
+ "execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "train_position:Trains-->1..10000 & train_position(t1) < train_position(t2) & not( t1 /= t2 )"
+ "train_position:Trains-->1..10000 &\n",
+ "train_position(t1) < train_position(t2) & \n",
+ "not( t1 /= t2 )"
]
},
{
@@ -1167,7 +1182,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 37,
"metadata": {
"slideshow": {
"slide_type": "skip"
@@ -1183,7 +1198,7 @@
"{S,E,N,D,M,O,R,Y} ⊆ 0 ‥ 9 ∧ S > 0 ∧ M > 0 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧ S * 1000 + E * 100 + N * 10 + D + M * 1000 + O * 100 + R * 10 + E = M * 10000 + O * 1000 + N * 100 + E * 10 + Y"
]
},
- "execution_count": 32,
+ "execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
@@ -1195,7 +1210,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 38,
"metadata": {},
"outputs": [
{
@@ -1214,7 +1229,7 @@
"\tO = 0"
]
},
- "execution_count": 16,
+ "execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
@@ -1240,7 +1255,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 39,
"metadata": {},
"outputs": [
{
@@ -1249,7 +1264,7 @@
"{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}"
]
},
- "execution_count": 34,
+ "execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
@@ -1265,7 +1280,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 40,
"metadata": {},
"outputs": [
{
@@ -1280,7 +1295,7 @@
"1\t9\t5\t6\t7\t1\t0\t8\t2\n"
]
},
- "execution_count": 15,
+ "execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
@@ -1308,29 +1323,9 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tP = 4\n",
- "\tA = 1\n",
- "\tS = 3\n",
- "\tI = 0\n",
- "\tK = 2\n",
- "\tN = 9\n",
- "\tO = 8"
- ]
- },
- "execution_count": 35,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
" {K,P} <: 1..9 &\n",
" {I,S,A,O,N} <: 0..9 &\n",
@@ -1352,7 +1347,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 41,
"metadata": {},
"outputs": [
{
@@ -1364,7 +1359,7 @@
"\tx = {2,3,4,5}"
]
},
- "execution_count": 36,
+ "execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
@@ -1426,7 +1421,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 42,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -1444,7 +1439,7 @@
"\tC = FALSE"
]
},
- "execution_count": 37,
+ "execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
@@ -1483,7 +1478,7 @@
},
{
"cell_type": "code",
- "execution_count": 39,
+ "execution_count": 43,
"metadata": {},
"outputs": [
{
@@ -1492,7 +1487,7 @@
"{(0↦2),(1↦1),(2↦0)}"
]
},
- "execution_count": 39,
+ "execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@@ -1533,7 +1528,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 44,
"metadata": {},
"outputs": [
{
@@ -1551,7 +1546,7 @@
"\tCARRY0 = TRUE"
]
},
- "execution_count": 40,
+ "execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
@@ -1566,7 +1561,7 @@
},
{
"cell_type": "code",
- "execution_count": 41,
+ "execution_count": 46,
"metadata": {
"slideshow": {
"slide_type": "subslide"
@@ -1576,20 +1571,20 @@
{
"data": {
"text/plain": [
- "{((((((FALSE↦FALSE)↦FALSE)↦TRUE)↦FALSE)↦TRUE)↦FALSE),((((((FALSE↦TRUE)↦FALSE)↦FALSE)↦FALSE)↦TRUE)↦FALSE),((((((TRUE↦FALSE)↦TRUE)↦FALSE)↦FALSE)↦TRUE)↦TRUE),((((((TRUE↦TRUE)↦TRUE)↦TRUE)↦FALSE)↦TRUE)↦TRUE)}"
+ "4"
]
},
- "execution_count": 41,
+ "execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "{X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n",
+ "card({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n",
" ((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) & \n",
" (CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) & \n",
" (CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &\n",
- " Z0=FALSE & Z1=TRUE}"
+ " Z0=FALSE & Z1=TRUE})"
]
},
{
@@ -1602,7 +1597,7 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 91,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -1611,23 +1606,33 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "|Nr|X0|X1|Y0|Y1|Z0|Z1|CARRY0|\n",
+ "|---|---|---|---|---|---|---|---|\n",
+ "|1|FALSE|FALSE|FALSE|TRUE|FALSE|TRUE|FALSE|\n",
+ "|2|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE|FALSE|\n",
+ "|3|TRUE|FALSE|TRUE|FALSE|FALSE|TRUE|TRUE|\n"
+ ],
"text/plain": [
- "{((((((FALSE↦FALSE)↦FALSE)↦TRUE)↦FALSE)↦TRUE)↦FALSE),((((((FALSE↦TRUE)↦FALSE)↦FALSE)↦FALSE)↦TRUE)↦FALSE),((((((TRUE↦FALSE)↦TRUE)↦FALSE)↦FALSE)↦TRUE)↦TRUE)}"
+ "Nr\tX0\tX1\tY0\tY1\tZ0\tZ1\tCARRY0\n",
+ "1\tFALSE\tFALSE\tFALSE\tTRUE\tFALSE\tTRUE\tFALSE\n",
+ "2\tFALSE\tTRUE\tFALSE\tFALSE\tFALSE\tTRUE\tFALSE\n",
+ "3\tTRUE\tFALSE\tTRUE\tFALSE\tFALSE\tTRUE\tTRUE\n"
]
},
- "execution_count": 42,
+ "execution_count": 91,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "{X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n",
+ ":table ({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n",
" ((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) & \n",
" (CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) & \n",
" (CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &\n",
" (CARRY0=TRUE => (X1=FALSE & Y1=FALSE)) & // no overflow\n",
" (CARRY0=FALSE => (X1=FALSE or Y1=FALSE)) & // no overflow\n",
- " Z0=FALSE & Z1=TRUE}"
+ " Z0=FALSE & Z1=TRUE})"
]
},
{
@@ -1651,7 +1656,7 @@
},
{
"cell_type": "code",
- "execution_count": 43,
+ "execution_count": 49,
"metadata": {
"slideshow": {
"slide_type": "subslide"
@@ -1662,9 +1667,9 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:01:28,941, T+458790] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x : 0 .. 2 & y : 0 .. 2 & x + y = 2 ints: irange(0,4), intatoms: none\u001b[0m\n",
- "[2018-06-04 14:01:28,941, T+458790] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
- "[2018-06-04 14:01:28,942, T+458791] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,5,2]\u001b[0m\n"
+ "[2018-06-05 10:10:18,465, T+6989479] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mkodkod ok: x : 0 .. 2 & y : 0 .. 2 & x + y = 2 ints: irange(0,4), intatoms: none\u001b[0m\n",
+ "[2018-06-05 10:10:18,465, T+6989479] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
+ "[2018-06-05 10:10:18,466, T+6989480] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1,2,0]\u001b[0m\n"
]
},
{
@@ -1677,7 +1682,7 @@
"\ty = 0"
]
},
- "execution_count": 43,
+ "execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
@@ -1695,7 +1700,7 @@
},
{
"cell_type": "code",
- "execution_count": 44,
+ "execution_count": 50,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -1706,8 +1711,8 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:01:31,052, T+460901] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: {x,y|x : 0 .. 2 & y : 0 .. 2 & x + y = 2} = res ints: irange(0,4), intatoms: irange(0,2)\u001b[0m\n",
- "[2018-06-04 14:01:31,054, T+460903] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n"
+ "[2018-06-05 10:10:35,717, T+7006731] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: {x,y|x : 0 .. 2 & y : 0 .. 2 & x + y = 2} = res ints: irange(0,4), intatoms: irange(0,2)\u001b[0m\n",
+ "[2018-06-05 10:10:35,718, T+7006732] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n"
]
},
{
@@ -1719,7 +1724,7 @@
"\tres = {(0↦2),(1↦1),(2↦0)}"
]
},
- "execution_count": 44,
+ "execution_count": 50,
"metadata": {},
"output_type": "execute_result"
}
@@ -1770,7 +1775,7 @@
},
{
"cell_type": "code",
- "execution_count": 45,
+ "execution_count": 51,
"metadata": {},
"outputs": [
{
@@ -1783,7 +1788,7 @@
"\ty = 2"
]
},
- "execution_count": 45,
+ "execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
@@ -1832,16 +1837,16 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 52,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "Execution time: 0.050491290 seconds"
+ "Execution time: 0.009508264 seconds"
],
"text/plain": [
- "Execution time: 0.050491290 seconds"
+ "Execution time: 0.009508264 seconds"
]
},
"metadata": {},
@@ -1862,18 +1867,20 @@
"\tO = 8"
]
},
- "execution_count": 17,
+ "execution_count": 52,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":time :solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
+ ":time :solve prob {K,P} <: 1..9 & {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 & card({K, I, S, P, A, O, N}) = 7"
]
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 53,
"metadata": {
"slideshow": {
"slide_type": "subslide"
@@ -1895,25 +1902,24 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 54,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 21:43:31,067, T+24267018] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n",
- "[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
- "[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [636]\u001b[0m\n"
+ "[2018-06-05 10:18:05,165, T+7456179] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n",
+ "[2018-06-05 10:18:05,165, T+7456179] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [395]\u001b[0m\n"
]
},
{
"data": {
"text/markdown": [
- "Execution time: 2.287290784 seconds"
+ "Execution time: 0.918848527 seconds"
],
"text/plain": [
- "Execution time: 2.287290784 seconds"
+ "Execution time: 0.918848527 seconds"
]
},
"metadata": {},
@@ -1934,7 +1940,7 @@
"\tO = 8"
]
},
- "execution_count": 19,
+ "execution_count": 54,
"metadata": {},
"output_type": "execute_result"
}
@@ -1982,7 +1988,7 @@
},
{
"cell_type": "code",
- "execution_count": 49,
+ "execution_count": 55,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -1998,7 +2004,7 @@
"\tx = −10"
]
},
- "execution_count": 49,
+ "execution_count": 55,
"metadata": {},
"output_type": "execute_result"
}
@@ -2020,14 +2026,14 @@
},
{
"cell_type": "code",
- "execution_count": 50,
+ "execution_count": 56,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:01:46,410, T+476259] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n"
+ "[2018-06-05 10:19:13,740, T+7524754] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n"
]
},
{
@@ -2039,7 +2045,7 @@
"\tx = 6001"
]
},
- "execution_count": 50,
+ "execution_count": 56,
"metadata": {},
"output_type": "execute_result"
}
@@ -2050,7 +2056,7 @@
},
{
"cell_type": "code",
- "execution_count": 51,
+ "execution_count": 57,
"metadata": {},
"outputs": [
{
@@ -2062,7 +2068,7 @@
"\tx = 6001"
]
},
- "execution_count": 51,
+ "execution_count": 57,
"metadata": {},
"output_type": "execute_result"
}
@@ -2084,14 +2090,14 @@
},
{
"cell_type": "code",
- "execution_count": 52,
+ "execution_count": 59,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:01:48,945, T+478794] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n"
+ "[2018-06-05 10:19:51,805, T+7562819] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : 6001:sup ---> 6001:6001\u001b[0m\n"
]
},
{
@@ -2109,7 +2115,7 @@
},
{
"cell_type": "code",
- "execution_count": 53,
+ "execution_count": 58,
"metadata": {},
"outputs": [
{
@@ -2121,7 +2127,7 @@
"\tx = 6756001"
]
},
- "execution_count": 53,
+ "execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
@@ -2144,47 +2150,18 @@
},
{
"cell_type": "code",
- "execution_count": 54,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 54,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve z3 x>y & y>x"
]
},
{
"cell_type": "code",
- "execution_count": 55,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:01:54,055, T+483904] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Timeout when posting constraint:\u001b[0m\n",
- "[2018-06-04 14:01:54,055, T+483904] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % kernel_objects:(_2222183#>0)\u001b[0m\n",
- "[2018-06-04 14:01:54,056, T+483905] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating x : INTEGER : inf:sup ---> -1:3\u001b[0m\n"
- ]
- },
- {
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":solve prob x>y &y>x"
]
@@ -2223,24 +2200,9 @@
},
{
"cell_type": "code",
- "execution_count": 56,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = thomas\n",
- "\ty = gordon"
- ]
- },
- "execution_count": 56,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"x:Trains & y:Trains & x/=y"
]
@@ -2265,7 +2227,7 @@
},
{
"cell_type": "code",
- "execution_count": 57,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -2278,18 +2240,28 @@
"\ty = {1,2}"
]
},
- "execution_count": 57,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "x <: 1..2 & y <: 1..2 & x \\/ y = 1..2 & 1:x & x <<: y"
+ "x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1:x & x ⊂ y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "| Element | x | y | x ∪ y |\n",
+ "| ------------- |-------------| -----| -----|\n",
+ "| 1 | x1 | y1 | x1 or y1\n",
+ "| 2 | x2 | y2 | x2 or y2 |"
]
},
{
"cell_type": "code",
- "execution_count": 58,
+ "execution_count": 88,
"metadata": {},
"outputs": [
{
@@ -2304,7 +2276,7 @@
"\tx2 = FALSE"
]
},
- "execution_count": 58,
+ "execution_count": 88,
"metadata": {},
"output_type": "execute_result"
}
@@ -2316,6 +2288,35 @@
" (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) // x <<: y"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 90,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Nr|x1|x2|y1|y2|\n",
+ "|---|---|---|---|---|\n",
+ "|1|TRUE|FALSE|TRUE|TRUE|\n"
+ ],
+ "text/plain": [
+ "Nr\tx1\tx2\ty1\ty2\n",
+ "1\tTRUE\tFALSE\tTRUE\tTRUE\n"
+ ]
+ },
+ "execution_count": 90,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {x1,x2,y1,y2 | {x1,x2,y1,y2} <: BOOL &\n",
+ " x1=TRUE or y1=TRUE & x2=TRUE or y2=TRUE & \n",
+ " x1=TRUE & // 1:x \n",
+ " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) }"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -2329,15 +2330,15 @@
},
{
"cell_type": "code",
- "execution_count": 59,
+ "execution_count": 61,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:02:32,427, T+522276] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x <: 1 .. 2 & y <: 1 .. 2 & x \\/ y = 1 .. 2 & 1 : ... ints: irange(1,2), intatoms: irange(1,2)\u001b[0m\n",
- "[2018-06-04 14:02:32,428, T+522277] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n"
+ "[2018-06-05 10:22:52,620, T+7743634] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x <: 1 .. 2 & y <: 1 .. 2 & x \\/ y = 1 .. 2 & 1 : ... ints: irange(1,2), intatoms: irange(1,2)\u001b[0m\n",
+ "[2018-06-05 10:22:52,620, T+7743634] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1]\u001b[0m\n"
]
},
{
@@ -2350,7 +2351,7 @@
"\ty = {1,2}"
]
},
- "execution_count": 59,
+ "execution_count": 61,
"metadata": {},
"output_type": "execute_result"
}
@@ -2376,7 +2377,7 @@
},
{
"cell_type": "code",
- "execution_count": 60,
+ "execution_count": 62,
"metadata": {},
"outputs": [
{
@@ -2385,7 +2386,7 @@
"1267650600228229401496703205376"
]
},
- "execution_count": 60,
+ "execution_count": 62,
"metadata": {},
"output_type": "execute_result"
}
@@ -2403,23 +2404,9 @@
},
{
"cell_type": "code",
- "execution_count": 61,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = {{100},{1}}"
- ]
- },
- "execution_count": 61,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x)"
]
@@ -2437,23 +2424,9 @@
},
{
"cell_type": "code",
- "execution_count": 62,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\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": 62,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"{100}:x & !y.(y:x => (!z.(z:y => y \\/ {z / 2}:x)))"
]
@@ -2472,24 +2445,24 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 63,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 21:54:17,800, T+24913751] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: r : 1 .. 5 <-> 1 .. 5 & (r ; r) = r & r /= {} & do... ints: irange(0,5), intatoms: irange(0,5)\u001b[0m\n",
- "[2018-06-04 21:54:17,801, T+24913752] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,2,1,1,3,2,1,2,1,1,5,1,1,2,1,2,1,2,1,1,1,1]\u001b[0m\n"
+ "[2018-06-05 10:23:40,430, T+7791444] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: r : 1 .. 5 <-> 1 .. 5 & (r ; r) = r & r /= {} & do... ints: irange(0,5), intatoms: irange(0,5)\u001b[0m\n",
+ "[2018-06-05 10:23:40,431, T+7791445] \"ProB Output Logger for instance 67d0d036\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,2,2,2,4,4,7,2,2,4,6,2,1,4,1,3,2,1,2,3,1,1]\u001b[0m\n"
]
},
{
"data": {
"text/markdown": [
- "Execution time: 0.153314218 seconds"
+ "Execution time: 0.103495089 seconds"
],
"text/plain": [
- "Execution time: 0.153314218 seconds"
+ "Execution time: 0.103495089 seconds"
]
},
"metadata": {},
@@ -2504,7 +2477,7 @@
"\tr = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)}"
]
},
- "execution_count": 20,
+ "execution_count": 63,
"metadata": {},
"output_type": "execute_result"
}
@@ -2529,24 +2502,9 @@
},
{
"cell_type": "code",
- "execution_count": 63,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = ∅\n",
- "\ty = {1,2}"
- ]
- },
- "execution_count": 63,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2"
]
@@ -2560,28 +2518,13 @@
},
{
"cell_type": "code",
- "execution_count": 64,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = ∅\n",
- "\ty = {1,2}"
- ]
- },
- "execution_count": 64,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"∀ smt_tmp28.(smt_tmp28 ∈ x ⇒ smt_tmp28 ≥ 1 & 2 ≥ smt_tmp28) & \n",
"∀ smt_tmp29.(smt_tmp29 ∈ y ⇒ smt_tmp29 ≥ 1 & 2 ≥ smt_tmp29) &\n",
@@ -2638,25 +2581,9 @@
},
{
"cell_type": "code",
- "execution_count": 65,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:02:49,960, T+539809] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n"
- ]
- },
- {
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: time out",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: time out\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y"
]
@@ -2718,27 +2645,13 @@
},
{
"cell_type": "code",
- "execution_count": 67,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
- "outputs": [
- {
- "data": {
- "text/latex": [
- "$\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\} \\wedge (\\exists /* LET */ (\\mathit{st13}).( (\\mathit{st13})=\\mathit{r} \\wedge \\forall \\mathit{st15}\\cdot (\\mathit{st15} \\in \\mathit{st13} \\mathbin\\Rightarrow \\exists \\mathit{st16}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st16} \\wedge (\\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16} \\mathbin\\Rightarrow \\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16})))) \\wedge \\forall \\mathit{st15}\\cdot (\\exists \\mathit{st19}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st19} \\wedge (\\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19} \\mathbin\\Rightarrow \\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19}))) \\mathbin\\Rightarrow \\mathit{st15} \\in \\mathit{st13})))$"
- ],
- "text/plain": [
- "f = {(1↦3),(2↦6)} ∧ (∃ /* LET */ (st13).( (st13)=r ∧ ∀st15·(st15 ∈ st13 ⇒ ∃st16·(6 ↦ st15 ∈ st16 ∧ (∀(st17,st18)·(st17 ↦ st18 ∈ st16 ⇒ st18 ↦ st17 ∈ f) ∧ ∀(st17,st18)·(st18 ↦ st17 ∈ f ⇒ st17 ↦ st18 ∈ st16)))) ∧ ∀st15·(∃st19·(6 ↦ st15 ∈ st19 ∧ (∀(st20,st21)·(st20 ↦ st21 ∈ st19 ⇒ st21 ↦ st20 ∈ f) ∧ ∀(st20,st21)·(st21 ↦ st20 ∈ f ⇒ st20 ↦ st21 ∈ st19))) ⇒ st15 ∈ st13)))"
- ]
- },
- "execution_count": 67,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":prettyprint f = {(1|->3),(2|->6)} &\n",
"#st13.(r = st13 & (\n",
@@ -2751,35 +2664,13 @@
},
{
"cell_type": "code",
- "execution_count": 68,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.038201131 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {2}\n",
- "\tf = {(1↦3),(2↦6)}"
- ]
- },
- "execution_count": 68,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob f = {(1|->3),(2|->6)} &\n",
"#st13.(r = st13 & (\n",
@@ -2792,18 +2683,9 @@
},
{
"cell_type": "code",
- "execution_count": 69,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve cvc4 f = {(1|->3),(2|->6)} &\n",
"#st13.(r = st13 & (\n",
@@ -2829,20 +2711,9 @@
},
{
"cell_type": "code",
- "execution_count": 70,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 70,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve prob x:s1 & x:s2 & x /: (s1 /\\ s2) & s1 <: INTEGER"
]
@@ -2856,20 +2727,9 @@
},
{
"cell_type": "code",
- "execution_count": 71,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 71,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve z3 x:s1 & x/:s2 & x /: (s1 \\/s2) & s1 <: INTEGER"
]
@@ -2902,24 +2762,13 @@
},
{
"cell_type": "code",
- "execution_count": 72,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "{0,100,200,300,400,500,600,700,800,900,1000}"
- ]
- },
- "execution_count": 72,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"{x|x∈0..2**10 & x mod 100 = 0}"
]
@@ -2937,25 +2786,9 @@
},
{
"cell_type": "code",
- "execution_count": 73,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tmn = 0\n",
- "\ts = {0,100,200,300,400,500,600,700,800,900,1000}\n",
- "\tmx = 1000"
- ]
- },
- "execution_count": 73,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"s = {x|x∈0..2**10 & x mod 100 = 0} &\n",
"mx = max(s) &\n",
@@ -2977,20 +2810,9 @@
},
{
"cell_type": "code",
- "execution_count": 74,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "{x∣x > 1000}"
- ]
- },
- "execution_count": 74,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"{x|x>1000}"
]
@@ -3004,24 +2826,9 @@
},
{
"cell_type": "code",
- "execution_count": 75,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tinf = {x∣x > 1000}\n",
- "\tres = (1001 ‥ 1100)"
- ]
- },
- "execution_count": 75,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"inf = {x|x>1000} & 1024 : inf & not(1000:inf) & res = (900..1100) ∩ inf"
]
@@ -3040,31 +2847,9 @@
},
{
"cell_type": "code",
- "execution_count": 76,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:03:14,350, T+564199] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] VIRTUAL TIME-OUT caused by: ### Warning: enumerating x : (all_solutions) : INTEGER : 1025:sup ---> 1025:1025\u001b[0m\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tinf = {x∣x > 1000 ∧ x mod 25 = 0}\n",
- "\tres = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})"
- ]
- },
- "execution_count": 76,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"inf = {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf"
]
@@ -3082,24 +2867,9 @@
},
{
"cell_type": "code",
- "execution_count": 77,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tinf = {x∣x > 1000 ∧ x mod 25 = 0}\n",
- "\tres = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})"
- ]
- },
- "execution_count": 77,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"inf = /*@symbolic*/ {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf"
]
@@ -3132,27 +2902,13 @@
},
{
"cell_type": "code",
- "execution_count": 78,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tvec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128),(9↦256),(10↦512)}"
- ]
- },
- "execution_count": 78,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"vec: 1..10 --> 0..9999 &\n",
"vec(1) : {1,10} &\n",
@@ -3173,87 +2929,27 @@
},
{
"cell_type": "code",
- "execution_count": 79,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:03:20,699, T+570548] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mkodkod ok: vec : 1 .. 8 --> 0 .. 199 & vec(1) : {1,10} & !x.(... ints: irange(0,398), intatoms: irange(0,199)\u001b[0m\n",
- "[2018-06-04 14:03:20,699, T+570548] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [204]\u001b[0m\n",
- "Execution time: 2.184422799 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tvec = {(3↦4),(5↦16),(6↦32),(7↦64),(1↦1),(2↦2),(4↦8),(8↦128)}"
- ]
- },
- "execution_count": 79,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)"
]
},
{
"cell_type": "code",
- "execution_count": 80,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.014949467 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tvec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128)}"
- ]
- },
- "execution_count": 80,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)"
]
},
{
"cell_type": "code",
- "execution_count": 81,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:03:24,797, T+574646] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n"
- ]
- },
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: time out",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)"
]
@@ -3278,33 +2974,9 @@
},
{
"cell_type": "code",
- "execution_count": 89,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.305008223 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\ts3 = ∃500∈{20,40,…,9980,10000}\n",
- "\tn = 4\n",
- "\ts1 = ∃2500∈{4,8,…,9996,10000}\n",
- "\ts2 = ∃2000∈{5,10,…,9995,10000}"
- ]
- },
- "execution_count": 89,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob s1 = {x|x:1..10**n & x mod n = 0} & s2 = {y|y:1..10**n & y mod (n+1) = 0} & s3 = s1 /\\ s2 & n=4"
]
@@ -3322,90 +2994,31 @@
},
{
"cell_type": "code",
- "execution_count": 90,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.013053703 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\txy = ∃201∈{1,2,…,299,300}\n",
- "\tx = (1 ‥ 100)\n",
- "\ty = (200 ‥ 300)\n",
- "\tn = 100"
- ]
- },
- "execution_count": 90,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y"
]
},
{
"cell_type": "code",
- "execution_count": 91,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: time out",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: time out\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":solve z3 x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y"
]
},
{
"cell_type": "code",
- "execution_count": 92,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:05:05,176, T+675025] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x = 1 .. n & y = 2 * n .. 3 * n & n = 100 & xy = x... ints: irange(1,300), intatoms: irange(1,300)\u001b[0m\n",
- "[2018-06-04 14:05:05,176, T+675025] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2]\u001b[0m\n",
- "Execution time: 0.336676466 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\txy = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,…}\n",
- "\tx = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64}\n",
- "\ty = {200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256}\n",
- "\tn = 100"
- ]
- },
- "execution_count": 92,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y"
]
@@ -3476,28 +3089,9 @@
},
{
"cell_type": "code",
- "execution_count": 93,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr2 = {1,4,9,16,25,36,49,64,81,100}\n",
- "\tr3 = [4,9,25,49,121]\n",
- "\tr4 = 256\n",
- "\tsqrt = 10\n",
- "\tf = λx·(x ∈ INTEGER∣x ∗ x)\n",
- "\tr1 = 10000000000"
- ]
- },
- "execution_count": 93,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"f = %x.(x:INTEGER|x*x) &\n",
"r1 = f(100000) &\n",
@@ -3509,39 +3103,9 @@
},
{
"cell_type": "code",
- "execution_count": 94,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:08:39,826, T+889675] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! source(b_compute_comprehension_set)\u001b[0m\n",
- "[2018-06-04 14:08:39,826, T+889675] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Keeping comprehension-set symbolic (you may want to use the /*@symbolic*/ pragma to prevent this message, unless it was due to a WD-Error), identifiers: [x,y]\u001b[0m\n",
- "[2018-06-04 14:08:39,827, T+889676] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Line: 1 Column: 9 until 44\u001b[0m\n",
- "[2018-06-04 14:08:39,837, T+889686] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mVIRTUAL TIME-OUT caused by: ### Warning: enumerating NATURAL(1) : NATURAL(1) : 1:sup ---> 1:3\u001b[0m\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr2 = {1,2,3,4}\n",
- "\tr3 = [2,2,3,3,4]\n",
- "\tr4 = 2\n",
- "\tr5 = {2,4,10,100}\n",
- "\tsqr = 9802\n",
- "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
- "\tr1 = 317"
- ]
- },
- "execution_count": 94,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n",
"r1 = f(100000) &\n",
@@ -3570,24 +3134,9 @@
},
{
"cell_type": "code",
- "execution_count": 95,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = 125\n",
- "\tReifVar = TRUE"
- ]
- },
- "execution_count": 95,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"(x>100 <=> (ReifVar=TRUE)) & (x<125 <=> (ReifVar=FALSE)) & x<200"
]
@@ -3625,26 +3174,9 @@
},
{
"cell_type": "code",
- "execution_count": 96,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tR = {1,0}\n",
- "\tS = {0}\n",
- "\tT = {0}\n",
- "\tX = 0"
- ]
- },
- "execution_count": 96,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"1:R & 1/:S & R/\\S=T & T={X}"
]
@@ -3670,20 +3202,9 @@
},
{
"cell_type": "code",
- "execution_count": 97,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "{((4↦4)↦{4}),((5↦4)↦∅),((5↦5)↦{5})}"
- ]
- },
- "execution_count": 97,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"{X,Y,R|X: 1..5 & Y: 4..10 & {X}/\\{Y}=R & X>=Y}"
]
@@ -3705,26 +3226,9 @@
},
{
"cell_type": "code",
- "execution_count": 98,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:08:47,442, T+897291] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating A : STRING : inf ---> \"STRING1\",\"STRING2\",...\u001b[0m\n",
- "[2018-06-04 14:08:47,443, T+897292] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ### Warning: enumerating B : STRING : inf ---> \"STRING1\",\"STRING2\",...\u001b[0m\n"
- ]
- },
- {
- "ename": "CommandExecutionException",
- "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
"A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(STRING)"
]
@@ -3743,68 +3247,27 @@
},
{
"cell_type": "code",
- "execution_count": 99,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 99,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)"
]
},
{
"cell_type": "code",
- "execution_count": 100,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:08:48,854, T+898703] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: A \\/ B = D & A /\\ C = {} & D = C & A /= {} ints: none, intatoms: none\u001b[0m\n",
- "[2018-06-04 14:08:48,854, T+898703] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: []\u001b[0m\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 100,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve kodkod A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)"
]
},
{
"cell_type": "code",
- "execution_count": 101,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 101,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve z3 A \\/ B = D & A /\\ C = {} & D=C & A /= {} & A:POW(BOOL)"
]
@@ -3830,19 +3293,40 @@
},
{
"cell_type": "code",
- "execution_count": 102,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
+ "outputs": [],
+ "source": [
+ ":time R= (1..200) \\ {50}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Another example, for minimum of set from SETS'18 paper:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 86,
+ "metadata": {},
"outputs": [
{
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.005074849 seconds\n"
- ]
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.005957963 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.005957963 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
},
{
"data": {
@@ -3850,16 +3334,41 @@
"TRUE\n",
"\n",
"Solution:\n",
- "\tR = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200}"
+ "\tS = {2,4,5,6,8,10}\n",
+ "\ty = 2"
]
},
- "execution_count": 102,
+ "execution_count": 86,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":time R= (1..200) \\ {50}"
+ ":time :solve prob S = {8,4,6,2,10,5} & y:S & S = {x|x:S & y<=x}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 80,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tS = {2,4,5,6,8,10}\n",
+ "\ty = 2"
+ ]
+ },
+ "execution_count": 80,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "S= {8,4,6,2,10,5} & y:S & !x.(x:S => y<=x)"
]
},
{
@@ -3936,138 +3445,45 @@
},
{
"cell_type": "code",
- "execution_count": 103,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":solve z3 x = 1..1000 /\\ (200..300)"
]
},
{
"cell_type": "code",
- "execution_count": 104,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.175097068 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = {6,7,8,9,10,11,12,13,14,15}"
- ]
- },
- "execution_count": 104,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 x = 1..40 /\\ (6..15)"
]
},
{
"cell_type": "code",
- "execution_count": 105,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.754973438 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = {6,7,8,9,10,11,12,13,14,15}"
- ]
- },
- "execution_count": 105,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 x = 1..60 /\\ (6..15)"
]
},
{
"cell_type": "code",
- "execution_count": 106,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 2.369086566 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = {6,7,8,9,10,11,12,13,14,15}"
- ]
- },
- "execution_count": 106,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 x = 1..80 /\\ (6..15)"
]
},
{
"cell_type": "code",
- "execution_count": 107,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.004883079 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tx = (6 ‥ 15)"
- ]
- },
- "execution_count": 107,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob x = 1..80 /\\ (6..15)"
]
@@ -4085,44 +3501,18 @@
},
{
"cell_type": "code",
- "execution_count": 108,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":solve z3 s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]"
]
},
{
"cell_type": "code",
- "execution_count": 109,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {2,3,5,7,11}\n",
- "\tc = ({2,3,5,7,11} ∗ {4,8,16,32})\n",
- "\ts1 = {2,3,5,7,11}\n",
- "\ts2 = {4,8,16,32}"
- ]
- },
- "execution_count": 109,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve prob s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]"
]
@@ -4141,89 +3531,27 @@
},
{
"cell_type": "code",
- "execution_count": 110,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.012805716 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tf = {(1↦1),(2↦2),(3↦3),(4↦4),(5↦5),(6↦6),(7↦7),(8↦8),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(16↦16),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(32↦32),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50)}\n",
- "\tn = 50"
- ]
- },
- "execution_count": 110,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob f: 1..n --> 1..n & !x.(x:2..n => f(x)=f(x-1)+1) & n=50"
]
},
{
"cell_type": "code",
- "execution_count": 111,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:10,559, T+920408] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: f : 1 .. n --> 1 .. n & !x.(x : 2 .. n => f(x) = f... ints: irange(1,50), intatoms: irange(1,50)\u001b[0m\n",
- "[2018-06-04 14:09:10,560, T+920409] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1185]\u001b[0m\n",
- "Execution time: 3.657044854 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tf = {(3↦3),(5↦5),(6↦6),(7↦7),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50),(1↦1),(2↦2),(4↦4),(8↦8),(16↦16),(32↦32)}\n",
- "\tn = 50"
- ]
- },
- "execution_count": 111,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod f: 1..n --> 1..n & !x.(x:2..n => f(x)=f(x-1)+1) & n=50"
]
},
{
"cell_type": "code",
- "execution_count": 112,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:13,146, T+922995] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n"
- ]
- },
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: time out",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 f: 1..n --> 1..n & !x.(x:2..n => f(x)=f(x-1)+1) & n=50"
]
@@ -4243,110 +3571,36 @@
},
{
"cell_type": "code",
- "execution_count": 113,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 2.087463022 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(2↦3),(2↦4),(3↦3),(3↦4),(4↦3),(4↦4),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5)}"
- ]
- },
- "execution_count": 113,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4"
]
},
{
"cell_type": "code",
- "execution_count": 114,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:15,382, T+925231] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: r : 1 .. 5 <-> 1 .. 5 & (r ; r) = r & r /= {} & do... ints: irange(0,5), intatoms: irange(0,5)\u001b[0m\n",
- "[2018-06-04 14:09:15,383, T+925232] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1,1,1,0,1,0,1,0,1,1,0,1,0,1,1,0,1,0,1,0,1,1]\u001b[0m\n",
- "Execution time: 0.037624591 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {(3↦3),(3↦4),(5↦4),(1↦4),(2↦4),(4↦4)}"
- ]
- },
- "execution_count": 114,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4"
]
},
{
"cell_type": "code",
- "execution_count": 115,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4"
]
},
{
"cell_type": "code",
- "execution_count": 116,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 1.971222669 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(2↦3),(2↦4),(3↦3),(3↦4),(4↦3),(4↦4),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5)}"
- ]
- },
- "execution_count": 116,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=3..4"
]
@@ -4366,31 +3620,9 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 16:46:59,166, T+6475117] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 16:47:00,347, T+6476298] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 55595\n",
- "[2018-06-04 16:47:00,348, T+6476299] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52301\n",
- "[2018-06-04 16:47:00,350, T+6476301] \"ProB Output Logger for instance ecdd0f\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 16:47:00,364, T+6476315] \"ProB Output Logger for instance ecdd0f\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "Loaded machine: GraphTheorem : []\n"
- ]
- },
- "execution_count": 10,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"::load\n",
"MACHINE GraphTheorem\n",
@@ -4401,23 +3633,9 @@
},
{
"cell_type": "code",
- "execution_count": 118,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/latex": [
- "$\\mathit{edges} \\in \\mathit{NODES5} \\mathbin\\leftrightarrow \\mathit{NODES5} \\wedge \\mathit{edges}^{-1} = \\mathit{edges} \\wedge \\neg (\\exists (\\mathit{n1},\\mathit{n2})\\cdot (\\mathit{n1} \\in \\mathit{NODES5} \\wedge \\mathit{n2} \\in \\mathit{NODES5} \\wedge \\mathit{n2} \\neq \\mathit{n1} \\wedge \\mathit{card}(\\mathit{edges}[\\{\\mathit{n1}\\}]) = \\mathit{card}(\\mathit{edges}[\\{\\mathit{n2}\\}]))) \\wedge \\mathit{dom}(\\mathit{edges}) = \\mathit{NODES5} \\wedge id(\\mathit{NODES5}) \\cap \\mathit{edges} = \\emptyset $"
- ],
- "text/plain": [
- "edges ∈ NODES5 ↔ NODES5 ∧ edges⁻¹ = edges ∧ ¬(∃(n1,n2)·(n1 ∈ NODES5 ∧ n2 ∈ NODES5 ∧ n2 ≠ n1 ∧ card(edges[{n1}]) = card(edges[{n2}]))) ∧ dom(edges) = NODES5 ∧ id(NODES5) ∩ edges = ∅"
- ]
- },
- "execution_count": 118,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":prettyprint edges : NODES5 <-> NODES5 & \n",
" edges~=edges &\n",
@@ -4428,18 +3646,9 @@
},
{
"cell_type": "code",
- "execution_count": 119,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: time out",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob edges : NODES5 <-> NODES5 & \n",
" edges~=edges &\n",
@@ -4450,34 +3659,13 @@
},
{
"cell_type": "code",
- "execution_count": 120,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:25,781, T+935630] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: edges~ = edges & not(#(n1,n2).(n2 /= n1 & card(edg... ints: irange(0,5), intatoms: none\u001b[0m\n",
- "[2018-06-04 14:09:25,781, T+935630] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
- "[2018-06-04 14:09:25,782, T+935631] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: []\u001b[0m\n",
- "Execution time: 0.837816834 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 120,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod edges : NODES5 <-> NODES5 & \n",
" edges~=edges &\n",
@@ -4488,18 +3676,9 @@
},
{
"cell_type": "code",
- "execution_count": 121,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 edges : NODES5 <-> NODES5 & \n",
" edges~=edges &\n",
@@ -4522,32 +3701,9 @@
},
{
"cell_type": "code",
- "execution_count": 122,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:26,058, T+935907] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: edges~ = edges & not(#(n1,n2).(n2 /= n1 & card(edg... ints: irange(0,5), intatoms: none\u001b[0m\n",
- "[2018-06-04 14:09:26,059, T+935908] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [5,4,3,1,2,2,2,2,2,1,7,1,2,2,2,1,3,2,2,2,1,2]\u001b[0m\n",
- "Execution time: 0.107056638 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tedges = {(NODES51↦NODES54),(NODES52↦NODES52),(NODES52↦NODES53),(NODES52↦NODES54),(NODES53↦NODES52),(NODES53↦NODES53),(NODES53↦NODES54),(NODES53↦NODES55),(NODES54↦NODES51),(NODES54↦NODES52),(NODES54↦NODES53),(NODES54↦NODES54),(NODES54↦NODES55),(NODES55↦NODES53),(NODES55↦NODES54)}"
- ]
- },
- "execution_count": 122,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod edges : NODES5 <-> NODES5 & \n",
" edges~=edges &\n",
@@ -4558,28 +3714,9 @@
},
{
"cell_type": "code",
- "execution_count": 123,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:26,173, T+936022] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: edges~ = edges & not(#(n1,n2).(n1 : dom(edges) & n... ints: irange(0,5), intatoms: none\u001b[0m\n",
- "Execution time: 0.056822248 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "FALSE"
- ]
- },
- "execution_count": 123,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod edges : NODES5 <-> NODES5 & \n",
" edges~=edges &\n",
@@ -4603,31 +3740,9 @@
},
{
"cell_type": "code",
- "execution_count": 124,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.053214873 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tqueens = {(1↦4),(2↦2),(3↦7),(4↦3),(5↦6),(6↦8),(7↦5),(8↦1)}\n",
- "\tn = 8"
- ]
- },
- "execution_count": 124,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob n=8 &\n",
" queens : 1..n >-> 1..n &\n",
@@ -4636,31 +3751,9 @@
},
{
"cell_type": "code",
- "execution_count": 125,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.370806337 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tqueens = {(1↦4),(2↦7),(3↦5),(4↦2),(5↦6),(6↦1),(7↦3),(8↦8)}\n",
- "\tn = 8"
- ]
- },
- "execution_count": 125,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 n=8 &\n",
" queens : 1..n >-> 1..n &\n",
@@ -4669,33 +3762,9 @@
},
{
"cell_type": "code",
- "execution_count": 126,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:27,167, T+937016] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: n = 8 & queens : 1 .. n >-> 1 .. n & !(q1,q2).(q1 ... ints: irange(-7,15), intatoms: irange(1,8)\u001b[0m\n",
- "[2018-06-04 14:09:27,168, T+937017] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [27,19,44,9,6,6,11,5,5,10,4,9,22,2,6,8,4,3,3,14,3,3]\u001b[0m\n",
- "Execution time: 0.405027874 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tqueens = {(3↦2),(5↦5),(6↦1),(7↦8),(1↦3),(2↦6),(4↦7),(8↦4)}\n",
- "\tn = 8"
- ]
- },
- "execution_count": 126,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod n=8 &\n",
" queens : 1..n >-> 1..n &\n",
@@ -4715,31 +3784,9 @@
},
{
"cell_type": "code",
- "execution_count": 127,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.054922769 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tbshp = {(1↦1),(1↦2),(1↦3)}\n",
- "\tn = 3"
- ]
- },
- "execution_count": 127,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob n=3 & bshp <: (1..n)*(1..n) & \n",
" !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n",
@@ -4748,25 +3795,9 @@
},
{
"cell_type": "code",
- "execution_count": 128,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:29,856, T+939705] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n"
- ]
- },
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: time out",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 n=3 & bshp <: (1..n)*(1..n) & \n",
" !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n",
@@ -4782,23 +3813,9 @@
},
{
"cell_type": "code",
- "execution_count": 129,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/latex": [
- "$\\mathit{n} = 3 \\wedge \\mathit{bshp} \\subseteq (1 .. \\mathit{n}) \\times (1 .. \\mathit{n}) \\wedge \\forall (\\mathit{i},\\mathit{j})\\cdot (\\{\\mathit{i},\\mathit{j}\\} \\subseteq 1 .. \\mathit{n} \\mathbin\\Rightarrow (\\mathit{i} \\mapsto \\mathit{j} \\in \\mathit{bshp} \\mathbin\\Rightarrow \\forall \\mathit{k}\\cdot (\\mathit{k} \\in \\mathit{i} + 1 .. \\mathit{n} \\mathbin\\Rightarrow (\\mathit{k} \\mapsto (\\mathit{j} + \\mathit{k}) - \\mathit{i}) \\not\\in \\mathit{bshp} \\wedge (\\mathit{k} \\mapsto (\\mathit{j} - \\mathit{k}) + \\mathit{i}) \\not\\in \\mathit{bshp}))) \\wedge \\mathit{card}(\\mathit{bshp}) = 3$"
- ],
- "text/plain": [
- "n = 3 ∧ bshp ⊆ (1 ‥ n) × (1 ‥ n) ∧ ∀(i,j)·({i,j} ⊆ 1 ‥ n ⇒ (i ↦ j ∈ bshp ⇒ ∀k·(k ∈ i + 1 ‥ n ⇒ (k ↦ (j + k) - i) ∉ bshp ∧ (k ↦ (j - k) + i) ∉ bshp))) ∧ card(bshp) = 3"
- ]
- },
- "execution_count": 129,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":prettyprint n=3 & bshp <: (1..n)*(1..n) & \n",
" !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n",
@@ -4818,46 +3835,18 @@
},
{
"cell_type": "code",
- "execution_count": 130,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3)}"
- ]
- },
- "execution_count": 130,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"!x.(x:1..2 => !y.(y:1..3 => (x,y):r)) "
]
},
{
"cell_type": "code",
- "execution_count": 131,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {z_∣z_ ∈ INTEGER ∗ INTEGER}"
- ]
- },
- "execution_count": 131,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":solve z3 !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) "
]
@@ -4871,80 +3860,27 @@
},
{
"cell_type": "code",
- "execution_count": 132,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":solve z3 !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)"
]
- },
- {
- "cell_type": "code",
- "execution_count": 133,
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:32,837, T+942686] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: !x.(x : 1 .. 2 => !y.(y : 1 .. 3 => x |-> y : r)) ... ints: irange(1,10), intatoms: irange(1,10)\u001b[0m\n",
- "[2018-06-04 14:09:32,839, T+942688] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,2,0,2,3,6,0,4,2,0,1,1,2,1,2,0,1,2,4,2,0,1]\u001b[0m\n",
- "Execution time: 0.112904757 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {(1↦3),(1↦1),(1↦2),(2↦3),(2↦1),(2↦2)}"
- ]
- },
- "execution_count": 133,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- ":time :solve kodkod !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 134,
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.019540215 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tr = {(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3)}"
- ]
- },
- "execution_count": 134,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ ":time :solve kodkod !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
"source": [
":time :solve prob !x.(x:1..2 => !y.(y:1..3 => (x,y):r)) & r<: (1..10)*(1..10)"
]
@@ -4962,31 +3898,9 @@
},
{
"cell_type": "code",
- "execution_count": 135,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:33,012, T+942861] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 14:09:34,585, T+944434] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63565\n",
- "[2018-06-04 14:09:34,585, T+944434] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47984\n",
- "[2018-06-04 14:09:34,589, T+944438] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 14:09:34,613, T+944462] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "Loaded machine: signals : []\n"
- ]
- },
- "execution_count": 135,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"::load\n",
"MACHINE\n",
@@ -5021,31 +3935,9 @@
},
{
"cell_type": "code",
- "execution_count": 136,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.201494972 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tres = {PL01,PL12}\n",
- "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL11),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20)}"
- ]
- },
- "execution_count": 136,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob nxt = \n",
" {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
@@ -5058,18 +3950,9 @@
},
{
"cell_type": "code",
- "execution_count": 137,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "ename": "CommandExecutionException",
- "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
- ]
- }
- ],
+ "outputs": [],
"source": [
":time :solve z3 nxt = \n",
" {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
@@ -5082,34 +3965,9 @@
},
{
"cell_type": "code",
- "execution_count": 138,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:38,479, T+948328] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: nxt = {PL01 |-> PL02,PL02 |-> PL03,PL03 |-> PL04,P... ints: none, intatoms: none\u001b[0m\n",
- "[2018-06-04 14:09:38,480, T+948329] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
- "[2018-06-04 14:09:38,480, T+948329] \"ProB Output Logger for instance 79d26131\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2]\u001b[0m\n",
- "Execution time: 0.686312764 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tres = {PL01,PL12}\n",
- "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL11),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20)}"
- ]
- },
- "execution_count": 138,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod nxt = \n",
" {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
@@ -5122,31 +3980,9 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 15:03:05,856, T+241807] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 15:03:07,015, T+242966] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51091\n",
- "[2018-06-04 15:03:07,018, T+242969] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 50312\n",
- "[2018-06-04 15:03:07,021, T+242972] \"ProB Output Logger for instance 5f836b9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 15:03:07,034, T+242985] \"ProB Output Logger for instance 5f836b9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "Loaded machine: signals : []\n"
- ]
- },
- "execution_count": 4,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"::load\n",
"MACHINE\n",
@@ -5201,35 +4037,9 @@
},
{
"cell_type": "code",
- "execution_count": 140,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:40,326, T+950175] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] empty_kodkod_union_constraint\u001b[0m\n",
- "[2018-06-04 14:09:40,326, T+950175] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod fail: nxt = {PL01 |-> PL02,PL02 |-> PL03,PL03 |-> PL04,P... , reason: integer without upper and lower bound in: {max(ran(nrs))} while extracting used types\u001b[0m\n",
- "Execution time: 0.318373176 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tcl1 = ∃197∈{(PL01↦PL02),(PL01↦PL03),…,(PL33↦PL35),(PL34↦PL35)}\n",
- "\tmx = {PL01}\n",
- "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL12),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20),(PL30↦PL31),(PL31↦PL32),(PL33↦PL34),(PL34↦PL35)}\n",
- "\tnrs = {(PL01↦19),(PL02↦18),(PL03↦17),(PL04↦16),(PL05↦15),(PL06↦14),(PL07↦13),(PL08↦12),(PL09↦11),(PL10↦10),(PL11↦9),(PL12↦8),(PL13↦7),(PL14↦6),(PL15↦5),(PL16↦4),(PL17↦3),(PL18↦2),(PL19↦1),(PL20↦1),(PL21↦0),(PL22↦0),(PL23↦0),(PL24↦0),(PL25↦0),(PL26↦0),(PL27↦0),(PL28↦0),(PL29↦0),(PL30↦2),(PL31↦1),(PL32↦0),(PL33↦2),(PL34↦1),(PL35↦0),(PL36↦0),(PL37↦0),(PL38↦0),(PL39↦0),(PL40↦0)}"
- ]
- },
- "execution_count": 140,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve kodkod nxt = \n",
" {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
@@ -5245,33 +4055,9 @@
},
{
"cell_type": "code",
- "execution_count": 141,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.046631537 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tcl1 = ∃197∈{(PL01↦PL02),(PL01↦PL03),…,(PL33↦PL35),(PL34↦PL35)}\n",
- "\tmx = {PL01}\n",
- "\tnxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL12),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20),(PL30↦PL31),(PL31↦PL32),(PL33↦PL34),(PL34↦PL35)}\n",
- "\tnrs = {(PL01↦19),(PL02↦18),(PL03↦17),(PL04↦16),(PL05↦15),(PL06↦14),(PL07↦13),(PL08↦12),(PL09↦11),(PL10↦10),(PL11↦9),(PL12↦8),(PL13↦7),(PL14↦6),(PL15↦5),(PL16↦4),(PL17↦3),(PL18↦2),(PL19↦1),(PL20↦1),(PL21↦0),(PL22↦0),(PL23↦0),(PL24↦0),(PL25↦0),(PL26↦0),(PL27↦0),(PL28↦0),(PL29↦0),(PL30↦2),(PL31↦1),(PL32↦0),(PL33↦2),(PL34↦1),(PL35↦0),(PL36↦0),(PL37↦0),(PL38↦0),(PL39↦0),(PL40↦0)}"
- ]
- },
- "execution_count": 141,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob nxt = \n",
" {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
@@ -5287,72 +4073,9 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "|Nr|prj1|prj2|\n",
- "|---|---|---|\n",
- "|1|PL01|PL02|\n",
- "|2|PL02|PL03|\n",
- "|3|PL03|PL04|\n",
- "|4|PL04|PL05|\n",
- "|5|PL05|PL06|\n",
- "|6|PL06|PL07|\n",
- "|7|PL07|PL08|\n",
- "|8|PL08|PL09|\n",
- "|9|PL09|PL10|\n",
- "|10|PL10|PL11|\n",
- "|11|PL11|PL12|\n",
- "|12|PL12|PL13|\n",
- "|13|PL13|PL14|\n",
- "|14|PL14|PL15|\n",
- "|15|PL15|PL16|\n",
- "|16|PL16|PL17|\n",
- "|17|PL17|PL18|\n",
- "|18|PL18|PL19|\n",
- "|19|PL19|PL20|\n",
- "|20|PL20|PL20|\n",
- "|21|PL30|PL31|\n",
- "|22|PL31|PL32|\n",
- "|23|PL33|PL34|\n",
- "|24|PL34|PL35|\n"
- ],
- "text/plain": [
- "Nr\tprj1\tprj2\n",
- "1\tPL01\tPL02\n",
- "2\tPL02\tPL03\n",
- "3\tPL03\tPL04\n",
- "4\tPL04\tPL05\n",
- "5\tPL05\tPL06\n",
- "6\tPL06\tPL07\n",
- "7\tPL07\tPL08\n",
- "8\tPL08\tPL09\n",
- "9\tPL09\tPL10\n",
- "10\tPL10\tPL11\n",
- "11\tPL11\tPL12\n",
- "12\tPL12\tPL13\n",
- "13\tPL13\tPL14\n",
- "14\tPL14\tPL15\n",
- "15\tPL15\tPL16\n",
- "16\tPL16\tPL17\n",
- "17\tPL17\tPL18\n",
- "18\tPL18\tPL19\n",
- "19\tPL19\tPL20\n",
- "20\tPL20\tPL20\n",
- "21\tPL30\tPL31\n",
- "22\tPL31\tPL32\n",
- "23\tPL33\tPL34\n",
- "24\tPL34\tPL35\n"
- ]
- },
- "execution_count": 5,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":table {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
" PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,\n",
@@ -5364,35 +4087,13 @@
},
{
"cell_type": "code",
- "execution_count": 142,
+ "execution_count": null,
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-06-04 14:09:40,536, T+950385] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 14:09:41,873, T+951722] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63578\n",
- "[2018-06-04 14:09:41,874, T+951723] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47994\n",
- "[2018-06-04 14:09:41,875, T+951724] \"ProB Output Logger for instance 1145e2a2\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 14:09:41,890, T+951739] \"ProB Output Logger for instance 1145e2a2\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "Loaded machine: SlotSolver_KodkodTest : []\n"
- ]
- },
- "execution_count": 142,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
"::load\n",
"MACHINE SlotSolver_KodkodTest\n",
@@ -5406,31 +4107,9 @@
},
{
"cell_type": "code",
- "execution_count": 143,
+ "execution_count": null,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Execution time: 0.353512947 seconds\n"
- ]
- },
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tcs = {kom,lin,pol,rom}\n",
- "\tmapping = ∃235∈{(((ang↦1)↦T_KF)↦1),(((ang↦1)↦T_KF)↦5),…,(((soz↦2)↦T_EF)↦156),(((soz↦2)↦T_EF)↦158)}"
- ]
- },
- "execution_count": 143,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
+ "outputs": [],
"source": [
":time :solve prob mapping = {\n",
" (lin, 1, T_EF, 102),\n",
@@ -5672,6 +4351,87 @@
" cs = {c|#(sem,typ,nr).( (c,sem,typ,nr):mapping & nr:100..150)}"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 100,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CliError",
+ "evalue": "Error during communication with Prolog core.",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[1m\u001b[31mde.prob.exception.CliError: Error during communication with Prolog core.\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.cli.ProBInstance.send(ProBInstance.java:78)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:48)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:68)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.execute(StateSpace.java:549)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:76)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:109)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:124)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.TimeCommand.run(TimeCommand.java:32)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:109)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:124)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\u001b[0m",
+ "\u001b[1m\u001b[31mCaused by: java.io.IOException: ProB binary returned nothing - it might have crashed\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.cli.ProBConnection.getAnswer(ProBConnection.java:75)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.cli.ProBConnection.send(ProBConnection.java:62)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.cli.ProBInstance.send(ProBInstance.java:76)\u001b[0m",
+ "\u001b[1m\u001b[31m\t... 13 more\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":time :solve kodkod f = %x.(x:1..1000 & x mod 2 = 1|x+1) & f[800..802] = res"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "For 2000: this takes 55 seconds already and generates Java out of heap error."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 99,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.053545046 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.053545046 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tres = {802}\n",
+ "\tf = ∃1000∈{(1↦2),(3↦4),…,(1997↦1998),(1999↦2000)}"
+ ]
+ },
+ "execution_count": 99,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve prob f = %x.(x:1..2000 & x mod 2 = 1|x+1) & f[800..802] = res"
+ ]
+ },
{
"cell_type": "code",
"execution_count": null,
diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 7752c948b6dbd66ec2ade48f4151e9e433038f12..b8acdd1b7af62a631371705781ac1a903b57964a 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -338,6 +338,46 @@
" => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Nr|prj1|prj2|\n",
+ "|---|---|---|\n",
+ "|1|1|1|\n",
+ "|2|2|5|\n",
+ "|3|3|8|\n",
+ "|4|4|6|\n",
+ "|5|5|3|\n",
+ "|6|6|7|\n",
+ "|7|7|2|\n",
+ "|8|8|4|\n"
+ ],
+ "text/plain": [
+ "Nr\tprj1\tprj2\n",
+ "1\t1\t1\n",
+ "2\t2\t5\n",
+ "3\t3\t8\n",
+ "4\t4\t6\n",
+ "5\t5\t3\n",
+ "6\t6\t7\n",
+ "7\t7\t2\n",
+ "8\t8\t4\n"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)}"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 11,