{
"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.394252508 seconds"
],
"text/plain": [
"Execution time: 0.394252508 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: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp50'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[nodeid(pos(16,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp55'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp56'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp56'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp57'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp58'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp58'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp54'])]),b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp59'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp60'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp60'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp61'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp62'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp62'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp51'])]),b(member(b(identifier('_smt_tmp50'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(20,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(19,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(15,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])]),b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp63'])]),b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp48'])])),pred,[])),pred,[])))",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp50'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[nodeid(pos(16,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp55'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp56'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp56'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp57'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp58'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp58'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp54'])]),b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp59'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp60'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp60'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp61'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp62'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp62'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp51'])]),b(member(b(identifier('_smt_tmp50'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(20,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(19,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(15,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])]),b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp63'])]),b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp48'])])),pred,[])),pred,[])))\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: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp108'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[nodeid(pos(17,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp113'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp114'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp114'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp115'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp116'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp116'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp112'])]),b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp117'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp118'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp118'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp119'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp120'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp120'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp109'])]),b(member(b(identifier('_smt_tmp108'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(21,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(20,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(16,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])]),b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp121'])]),b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp106'])])),pred,[])),pred,[])))",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp108'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[nodeid(pos(17,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp113'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp114'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp114'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp115'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp116'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp116'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp112'])]),b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp117'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp118'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp118'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp119'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp120'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp120'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp109'])]),b(member(b(identifier('_smt_tmp108'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(21,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(20,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(16,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])]),b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp121'])]),b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp106'])])),pred,[])),pred,[])))\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
}