add experiment notebook

notebooks/experiments/SMT_Translation_Experiments.ipynb

+{
+ "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)",
+     "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}]"
+   ]
+  },
+  {
+   "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": 2,
+   "metadata": {},
+   "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": 2,
+     "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": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "Execution time: 0.194111316 seconds"
+      ],
+      "text/plain": [
+       "Execution time: 0.194111316 seconds"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr = {2}\n",
+       "\tf = {(1↦3),(2↦6)}"
+      ]
+     },
+     "execution_count": 3,
+     "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": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "ProB 2",
+   "language": "prob",
+   "name": "prob2"
+  },
+  "language_info": {
+   "file_extension": ".prob",
+   "mimetype": "text/x-prob",
+   "name": "prob"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}