{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Experiments in SMTLib Translation #\n",
"\n",
"Let us look at a simple example that poses problems for the Z3/CVC4 backend:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
]
}
],
"source": [
":solve z3 f = {1|->3, 2|->6} & r = f~[{6}]"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
]
}
],
"source": [
":solve z3 f = {1|->3, 2|->6} & r = f~[{6}] & not(r={2})"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To understand why this simple constraint cannot be solved, we have to know how the translation works:\n",
"The relational inverse gets translated into two universal quantifications for SMTLib:\n",
"```\n",
" x = y~\n",
"<=>\n",
" !(st11,st12).(st11 |-> st12 : x => st12 |-> st11 : y) & \n",
" !(st11,st12).(st12 |-> st11 : y => st11 |-> st12 : x))\n",
"```\n",
"Similarly, r = f[s] is translated as follows:\n",
"```\n",
" r = f[s]\n",
"<=>\n",
" !st27.(st27 : r => #st26.(st26 |-> st27 : f & st26 : s) & \n",
" !st27.(#st26.(st26 |-> st27 : f & st26 : s) => st27 : r)\n",
"```\n",
"The resulting predicate (without the inverse and image operators) is the following, which Z3 cannot solve (but ProB can)."
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\} \\wedge \\exists \\mathit{st13}\\cdot (\\mathit{r} = \\mathit{st13} \\wedge (\\forall \\mathit{st15}\\cdot (\\mathit{st15} \\in \\mathit{st13} \\mathbin\\Rightarrow \\exists \\mathit{st14}\\cdot (\\exists \\mathit{st16}\\cdot (\\mathit{st14} \\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 \\mathit{st14} \\in \\{6\\})) \\wedge \\forall \\mathit{st15}\\cdot (\\exists \\mathit{st14}\\cdot (\\exists \\mathit{st19}\\cdot (\\mathit{st14} \\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}))) \\wedge \\mathit{st14} \\in \\{6\\}) \\mathbin\\Rightarrow \\mathit{st15} \\in \\mathit{st13})))$"
],
"text/plain": [
"f = {(1↦3),(2↦6)} ∧ ∃st13·(r = st13 ∧ (∀st15·(st15 ∈ st13 ⇒ ∃st14·(∃st16·(st14 ↦ st15 ∈ st16 ∧ (∀(st17,st18)·(st17 ↦ st18 ∈ st16 ⇒ st18 ↦ st17 ∈ f) ∧ ∀(st17,st18)·(st18 ↦ st17 ∈ f ⇒ st17 ↦ st18 ∈ st16))) ∧ st14 ∈ {6})) ∧ ∀st15·(∃st14·(∃st19·(st14 ↦ st15 ∈ st19 ∧ (∀(st20,st21)·(st20 ↦ st21 ∈ st19 ⇒ st21 ↦ st20 ∈ f) ∧ ∀(st20,st21)·(st21 ↦ st20 ∈ f ⇒ st20 ↦ st21 ∈ st19))) ∧ st14 ∈ {6}) ⇒ st15 ∈ st13)))"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":prettyprint f = {(1|->3),(2|->6)} &\n",
"#st13.(r = st13 & (\n",
" !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
" (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
" !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
" !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
" !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"Execution time: 0.359755436 seconds"
],
"text/plain": [
"Execution time: 0.359755436 seconds"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/markdown": [
"$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{r} = \\{2\\}$\n",
"* $\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\}$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tr = {2}\n",
"\tf = {(1↦3),(2↦6)}"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":time :solve prob f = {(1|->3),(2|->6)} &\n",
"#st13.(r = st13 & (\n",
" !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
" (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
" !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
" !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
" !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))\n",
"\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Experiment in Rodin: adding r={2} as theorem and use SMT Plugin using the technique suggested by Laurent:\n",
"\n",
"pour voir la traduction d’Event-B vers SMT, créer un fichier texte contenant\n",
"```\n",
" org.eventb.smt.core/debug = true\n",
" org.eventb.smt.core/debug/translator = true\n",
" org.eventb.smt.core/debug/translator_details = true\n",
"```\n",
"et lancer Rodin avec les paramètres `-debug <text-file>`.\n",
"\n",
"À chaque fois qu’un solveur SMT est lancé, le contenu du fichier SMT sera affiché dans la console.\n",
"\n",
"```\n",
"; translated from Event-B with the PP approach of Rodin SMT Plugin\n",
"\n",
"(set-info :status unsat)\n",
"(set-logic AUFLIA)\n",
"(declare-fun f (Int Int) Bool)\n",
"(declare-fun r (Int) Bool)\n",
"\n",
"(assert (and \n",
" (forall ((x Int) (x0 Int)) \n",
" (= \n",
" (f x x0) \n",
" (or \n",
" (and \n",
" (= x 1) \n",
" (= x0 3)) \n",
" (and \n",
" (= x 2) \n",
" (= x0 6))))) \n",
" (forall ((x1 Int)) \n",
" (= \n",
" (r x1) \n",
" (exists ((x2 Int)) \n",
" (and \n",
" (= x2 6) \n",
" (f x1 x2)))))))\n",
"(assert (not \n",
" (forall ((x3 Int)) \n",
" (= \n",
" (r x3) \n",
" (= x3 2)))))\n",
"(check-sat)\n",
"```"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This is not using the set datatype but functions to bool."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\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": 6,
"metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\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)"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "ProB 2",
"language": "prob",
"name": "prob2"
},
"language_info": {
"codemirror_mode": "prob2_jupyter_repl",
"file_extension": ".prob",
"mimetype": "text/x-prob2-jupyter-repl",
"name": "prob"
}
},
"nbformat": 4,
"nbformat_minor": 2
}