Dagstuhl2019.ipynb

{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "# Spacer on Jupyter\n",
        "\n",
        "This is an interactive document. You can follow along on the cloud, change, play, go deeper into the code.\n",
        "\n",
        "Slides accompanying this notebook are available [here](https://arieg.bitbucket.io/pdf/synasc2019.pdf).\n",
        "\n",
        "To create your own copy:\n",
        " \n",
        " 1. Go to https://notebooks.azure.com/arie-gurfinkel/projects/spacerexamples\n",
        " 2. Create an Azure Notebooks account\n",
        " 3. **Clone** `spacerexamples` project into your space\n",
        " 4. Start `Dagstuhl2019.ipynb` notebook\n",
        " \n",
        "If you get an error about `z3` package not being found, wait a little and try again. It takes some time for the underlying virtual machine to get provisioned with all the necessary pacakges."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 1,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "name": "stdout",
          "output_type": "stream",
          "text": [
            "Requirement already satisfied: z3-solver in ./venv/lib/python3.9/site-packages (4.12.1.0)\n",
            "\u001b[33mWARNING: You are using pip version 22.0.4; however, version 23.0.1 is available.\n",
            "You should consider upgrading via the '/Users/arie/ag/git/spacer-on-jupyter/venv/bin/python -m pip install --upgrade pip' command.\u001b[0m\u001b[33m\n",
            "\u001b[0m"
          ]
        }
      ],
      "source": [
        "import sys\n",
        "!{sys.executable} -m pip install z3-solver"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 26,
      "metadata": {
        "code_folding": [
          3,
          16,
          22,
          31
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "import sys\n",
        "import z3\n",
        "\n",
        "class HtmlStr(object):\n",
        "    def __init__(self, s):\n",
        "        self._s = str(s)\n",
        "        self._s = self._s.replace('\\n', '<br/>')\n",
        "\n",
        "    def _repr_html_(self):\n",
        "        return self._s\n",
        "\n",
        "    def __repr__(self):\n",
        "        return repr(self._s)\n",
        "    def __str__(self):\n",
        "        return str(self._s)\n",
        "\n",
        "def chc_to_str(chc):\n",
        "    if z3.in_html_mode():\n",
        "        return chc_to_html(chc)\n",
        "    else:\n",
        "        return chc_to_txt(chc)\n",
        "\n",
        "def chc_to_html(chc):\n",
        "    import io\n",
        "    out = io.StringIO()\n",
        "\n",
        "    for cls in chc:\n",
        "        print(cls, '<br/>', file=out)\n",
        "\n",
        "    return HtmlStr(out.getvalue())\n",
        "\n",
        "def chc_to_txt(chc):\n",
        "    import io\n",
        "    out = io.StringIO()\n",
        "    for cls in chc:\n",
        "        print(cls, file=out)\n",
        "    return out.getvalue()\n",
        "\n",
        "class SpacerProof(object):\n",
        "    def __init__(self, pf_ast):\n",
        "        # strip off last mp to false\n",
        "        self._ast = pf_ast.children()[0]\n",
        "\n",
        "    def _get_fact(self, ast):\n",
        "        return ast.children()[-1]\n",
        "\n",
        "    def _to_dot_rec(self, ast, graph, visited):\n",
        "        if ast.get_id() in visited:\n",
        "            return\n",
        "\n",
        "        visited.add(ast.get_id())\n",
        "\n",
        "        dst = str(self._get_fact(ast).get_id())\n",
        "        kids = ast.children()\n",
        "        for k in kids[1:-1]:\n",
        "            k_fact = self._get_fact(k)\n",
        "            if k_fact.get_id() not in visited:\n",
        "                graph.node(str(k_fact.get_id()), str(k_fact))\n",
        "                visited.add(k_fact.get_id())\n",
        "                self._to_dot_rec(k, graph, visited)\n",
        "            graph.edge(str(k_fact.get_id()), dst)\n",
        "\n",
        "    def to_dot(self):\n",
        "        import graphviz\n",
        "        g = graphviz.Digraph()\n",
        "\n",
        "        visited = set()\n",
        "\n",
        "        fact = self._get_fact(self._ast)\n",
        "        id = fact.get_id()\n",
        "        g.node(str(id), str(fact))\n",
        "        visited.add(id)\n",
        "        self._to_dot_rec(self._ast, g, visited)\n",
        "        return g\n",
        "\n",
        "    def _repr_mimebundle_(self, include, exclude, **kwargs):\n",
        "        return self.to_dot()._repr_mimebundle_(include, exclude, **kwargs)\n",
        "\n",
        "    def __str__(self):\n",
        "        return str(self.to_dot())\n",
        "    def raw(self):\n",
        "        return self._ast\n",
        "\n",
        "\n",
        "# proof mode must be enabled before any expressions are created\n",
        "z3.set_param(proof=True)\n",
        "z3.set_param(model=True)\n",
        "# print expressions with HTML\n",
        "z3.set_html_mode(True)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Craig Interpolation\n",
        "\n",
        "Let $A$ and $B$ be two formulas such that $A \\wedge B$ is unsat. A __Craig Interpolant__ of $A$ and $B$ is a formula $Itp$ such that:\n",
        "\n",
        "  1. $A \\implies Itp$\n",
        "  2. $Itp \\wedge B \\implies False$\n",
        "  3. uninterpreted symbols of $Itp$ are those that are shared between $A$ and $B$\n",
        "  \n",
        "Craig Interpolation is at a core of many SMT- and SAT-based verification algorithms. \n",
        "Computing Craig Interpolants is one of the most requested (missing) features of Z3.\n",
        "__But__, Craig Interpolation is reducible to CHC satisfiability!\n",
        "\n",
        "$Itp$ is an interpolant of $A \\wedge B$ if and only if, $Itp$ is a satisfying assignment to the following CHC:\n",
        "\n",
        "  1. $\\forall a, c \\cdot A(a, c) \\implies Itp(c)$\n",
        "  2. $\\forall b, c \\cdot Itp(c) \\wedge B(b, c) \\implies False$\n",
        " \n",
        "where uninterpreted constants $c$ are shared between $A$ and $B$, and uninterpreted constants $a$ and $b$ are  local to $A$ and $B$, respectively."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 3,
      "metadata": {
        "code_folding": [
          1
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "# compute uninterpreted constants in a formula\n",
        "def free_arith_vars(fml):\n",
        "    '''Returns the set of all integer uninterpreted constants in a formula'''\n",
        "    seen = set([])\n",
        "    vars = set([])\n",
        "\n",
        "    int_sort = z3.IntSort()\n",
        "    def fv(seen, vars, f):\n",
        "        if f in seen:\n",
        "            return\n",
        "        seen |= { f }\n",
        "        if f.sort().eq(int_sort) and f.decl().kind() == z3.Z3_OP_UNINTERPRETED:\n",
        "            vars |= { f }\n",
        "        for ch in f.children():\n",
        "            fv(seen, vars, ch)\n",
        "    fv(seen, vars, fml)\n",
        "    return vars"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 4,
      "metadata": {
        "code_folding": [
          1,
          7,
          12,
          15
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "# wrapper to solve CHC constraints and extract result\n",
        "def solve_horn(chc, pp=False, q3=False, max_unfold=10, verbosity=0):\n",
        "    z3.set_param(verbose=verbosity)\n",
        "\n",
        "    s = z3.SolverFor('HORN')\n",
        "    s.set('engine', 'spacer')\n",
        "    s.set('spacer.order_children', 2)\n",
        "    if not pp:\n",
        "        s.set('xform.inline_eager', False)\n",
        "        s.set('xform.inline_linear', False)\n",
        "        s.set('xform.slice', False)\n",
        "\n",
        "    if max_unfold > 0:\n",
        "        s.set('spacer.max_level', max_unfold)\n",
        "\n",
        "    if q3:\n",
        "        # allow quantified variables in pobs\n",
        "        s.set('spacer.ground_pobs', False)\n",
        "        # enable quantified generalization\n",
        "        s.set('spacer.q3.use_qgen', True)\n",
        "\n",
        "    # add constraints to solver\n",
        "    s.add(chc)\n",
        "    if verbosity > 0:\n",
        "        print(s.sexpr())\n",
        "    # run solver\n",
        "    res = s.check()\n",
        "    # extract model or proof\n",
        "    answer = None\n",
        "    if res == z3.sat:\n",
        "        answer = s.model()\n",
        "    elif res == z3.unsat:\n",
        "        answer = s.proof()\n",
        "    return res, answer"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 5,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "# Binary Craig Interpolation by reduction to CHC\n",
        "def interpolate(A, B, verbosity=0):\n",
        "    '''Computes a Craig interpolant between A and B'''\n",
        "    As = free_arith_vars(A)\n",
        "    Bs = free_arith_vars(B)\n",
        "\n",
        "    shared = [s for s in As & Bs ]\n",
        "\n",
        "    Itp = z3.Function('Itp', [s.sort() for s in shared] + [z3.BoolSort()])\n",
        "    left = z3.ForAll([a for a in As], z3.Implies(A, Itp(shared)))\n",
        "    right = z3.ForAll([b for b in Bs], z3.Implies(Itp(shared), z3.Not(B)))\n",
        "\n",
        "    res, answer = solve_horn([left, right])\n",
        "\n",
        "    if res == z3.sat:\n",
        "        return answer.eval(Itp(shared))\n",
        "    return None"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 6,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "a, b, x, y = z3.Ints('a b x y')\n",
        "itp = interpolate(z3.And(a < x, x < b), z3.And(b < a))"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 7,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(b + -1&middot;a &le; 1)"
            ],
            "text/plain": [
              "&not;(b + -1&middot;a &le; 1)"
            ]
          },
          "execution_count": 7,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "itp"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Principle of Induction\n",
        "\n",
        "Symbolic reachability problem $P$ is a tuple $(v, Init, Tr, Bad)$, where \n",
        "   1. $V$ is a set of state variables\n",
        "   2. $Init$ is a formula over $v$ describing the set of initial states\n",
        "   3. $Tr$ is a formula $v$ and $v'$ describing the transition relation\n",
        "   4. $Bad$ is a formula over $v$ describing the set of bad (or error) states\n",
        "   \n",
        "**Principle of Induction**: $P$ is **SAFE** if and only if there exists a formula $Inv(v)$ such that\n",
        "   1. (Initiation) $Init \\implies Inv$\n",
        "   2. (Induction) $Inv \\wedge Tr \\implies Inv'$\n",
        "   3. (Safety) $Inv \\wedge Bad \\implies False$\n",
        "   \n",
        "The formula $Inv$ is called an **inductive hypothesis**. Finding the right inductive hypothesis is reducible to deciding satifiability of the CHC that follow directly from the definition of principle of induction."
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "We begin by definition a class `Ts` to represent a transition system. It has three fields, `Init`, `Tr`, and `Bad` to represent the three corresponding components, and lots of additional code to manage state and input variables"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 8,
      "metadata": {
        "code_folding": [
          0,
          15,
          36,
          50,
          75,
          80,
          87,
          91,
          98,
          118,
          130,
          136,
          139,
          148,
          150,
          153,
          159
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "class Ts(object):\n",
        "    \"\"\"A transition system\n",
        "\n",
        "    Example usage\n",
        "    >>> T = Ts('Ts0')\n",
        "    >>> x, x_out = T.add_var(z3.IntSort(), name='x')\n",
        "    >>> T.Init = x <= 0\n",
        "    >>> T.Tr = z3.And(x < 5, x_out == x + 1)\n",
        "    >>> T.Bad = x >= 10\n",
        "    >>> T                                   #doctest: +NORMALIZE_WHITESPACE\n",
        "    Transition System: Ts0\n",
        "        Init: v_0 <= 0\n",
        "        Bad: v_0 >= 10\n",
        "        Tr: And(v_0 < 5, v_out_0 == v_0 + 1)\n",
        "    \"\"\"\n",
        "    def __init__(self, name='Ts'):\n",
        "        # string name\n",
        "        self.name = name\n",
        "        # state variables (pair of input and output)\n",
        "        self._vars = []\n",
        "        # inputs\n",
        "        self._inputs = []\n",
        "        # a map from optional names to state variables\n",
        "        self._named_vars = dict()\n",
        "\n",
        "        # maps state variable index to optional name\n",
        "        self._var_names = list()\n",
        "\n",
        "        # Transition relation\n",
        "        self.Tr = z3.BoolVal(True)\n",
        "        # Initial condition\n",
        "        self.Init = z3.BoolVal(True)\n",
        "        # Bad states\n",
        "        self.Bad = z3.BoolVal(False)\n",
        "\n",
        "\n",
        "    def add_var(self, sort, name=None):\n",
        "        '''Add a state variable of a given sort. Returns a pair (pre, post)\n",
        "           of a pre- and post- state versions of the variable\n",
        "        '''\n",
        "        pre, post = self._new_var_name(name=name)\n",
        "        v_in = z3.Const(pre, sort)\n",
        "        v_out = z3.Const(post, sort)\n",
        "        self._vars.append((v_in, v_out))\n",
        "        self._var_names.append(name)\n",
        "        if name is not None:\n",
        "            self._named_vars[name] = (v_in, v_out) \n",
        "\n",
        "        return (v_in, v_out)\n",
        "\n",
        "    def get_var(self, idx):\n",
        "        \"\"\"Returns a pair of pre- and post-variables with a given index or name\n",
        "\n",
        "        If idx is not an int it is interpreted as a name.\n",
        "        Otherwise, it is interpreted as a variable index.\n",
        "\n",
        "        >>> T = Ts('Ts0')\n",
        "        >>> x, x_out = T.add_var(z3.IntSort(), name='x')\n",
        "        >>> y, y_out = T.add_var(z3.IntSort(), name='y')\n",
        "        >>> x\n",
        "        v_0\n",
        "\n",
        "        >>> T.get_var(1)\n",
        "        (v_1, v_out_1)\n",
        "\n",
        "        >>> T.get_var('x')\n",
        "        (v_0, v_out_0)\n",
        "\n",
        "        \"\"\"\n",
        "        if isinstance(idx, int):\n",
        "            return self._vars[idx]\n",
        "        elif idx in self._named_vars:\n",
        "            return self._named_vars[idx]\n",
        "        return None\n",
        "\n",
        "    def get_var_name(self, idx):\n",
        "        if idx < len(self._var_names):\n",
        "            return self._var_names[idx]\n",
        "        return None\n",
        "\n",
        "    def get_pre_var(self, idx):\n",
        "        \"\"\"Returns a pre-state variable with a given name/index\"\"\"\n",
        "        res = self.get_var(idx)\n",
        "        if res is not None:\n",
        "            return res[0]\n",
        "        return None\n",
        "\n",
        "    def get_pre_vars(self, vars):\n",
        "        \"\"\"Returns a tuple of pre-state variables with given names\"\"\"\n",
        "        return (self.get_pre_var(v) for v in vars.split())\n",
        "\n",
        "    def get_post_var(self, idx):\n",
        "        \"\"\"Returns a post-state variable with a given name\"\"\"\n",
        "        res = self.get_var(idx)\n",
        "        if res is not None:\n",
        "            return res[1]\n",
        "        return None\n",
        "\n",
        "    def add_input(self, sort, name=None):\n",
        "        '''Add an input of a given sort'''\n",
        "        v = z3.Const(self._new_input_name(name=name), sort)\n",
        "        self._inputs.append(v)\n",
        "        return v\n",
        "\n",
        "    def inputs(self):\n",
        "        return self._inputs\n",
        "    def pre_vars(self):\n",
        "        return [u for (u, v) in self._vars]\n",
        "    def post_vars(self):\n",
        "        return [v for (u, v) in self._vars]\n",
        "    def vars(self):\n",
        "        return self.pre_vars() + self.post_vars()\n",
        "    def pre_post_vars(self):\n",
        "        return self._vars\n",
        "    def all(self):\n",
        "        return self.vars() + self.inputs()\n",
        "    def sig(self):\n",
        "        return [v.sort() for (u, v) in self._vars]\n",
        "    def to_post(self, e):\n",
        "        '''Rename expression over pre-state variables to post-state variables\n",
        "\n",
        "        >>> T = Ts('Ts0')\n",
        "        >>> x, x_out = T.add_var(z3.IntSort(), 'x')\n",
        "        >>> y, y_out = T.add_var(z3.IntSort(), 'y')\n",
        "        >>> e = x > y\n",
        "        >>> T.to_post(x > y)\n",
        "        v_out_0 > v_out_1\n",
        "        '''\n",
        "        return z3.substitute(e, *self._vars)\n",
        "\n",
        "    def _new_input_name(self, name=None):\n",
        "        if name is not None:\n",
        "            return str(name)\n",
        "        else:\n",
        "            return self._mk_input_name(len(self._inputs))\n",
        "\n",
        "    def _mk_input_name(self, idx):\n",
        "        return 'i_' + str(idx)\n",
        "\n",
        "    def _new_var_name(self, name=None):\n",
        "        if name is not None:\n",
        "            assert name not in self._named_vars\n",
        "            assert str(name) not in self._named_vars\n",
        "            return str(name), str(name) + \"'\" \n",
        "        else:\n",
        "            idx = len(self._vars)\n",
        "            return self._mk_var_name(idx), self._mk_post_var_name(idx)\n",
        "\n",
        "    def _mk_var_name(self, idx):\n",
        "        return 'v_' + str(idx)\n",
        "    def _mk_post_var_name(self, idx):\n",
        "        return 'v_out_' + str(idx)\n",
        "\n",
        "    def __repr__(self):\n",
        "        return 'Transition System: ' + self.name + '\\n' + \\\n",
        "            '\\tInit: ' + str(self.Init) + '\\n' + \\\n",
        "            '\\tBad: ' + str(self.Bad) + '\\n' + \\\n",
        "            '\\tTr: ' + str(self.Tr)\n",
        "\n",
        "    def __str__(self):\n",
        "        return repr(self)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "We now define a transition system that counts. The definition is wrapped in a method since we will use it multiple times. We create two versions, one safe and one unsafe:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 9,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def mk_ts0(safe=True):\n",
        "    T = Ts('Ts0')\n",
        "    x, x_out = T.add_var(z3.IntSort(), name='x')\n",
        "    T.Init = x <= 0\n",
        "    T.Tr = z3.And(x < 5, x_out == x + 1)\n",
        "    if safe:\n",
        "        T.Bad = x >= 10\n",
        "    else:\n",
        "        T.Bad = x >= 4\n",
        "    return T"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 10,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "Transition System: Ts0<br/>\tInit: x &le; 0<br/>\tBad: x &ge; 10<br/>\tTr: x &lt; 5 &and; x' = x + 1"
            ],
            "text/plain": [
              "\"Transition System: Ts0<br/>\\tInit: x &le; 0<br/>\\tBad: x &ge; 10<br/>\\tTr: x &lt; 5 &and; x' = x + 1\""
            ]
          },
          "execution_count": 10,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "ts0 = mk_ts0(safe=True)\n",
        "HtmlStr(ts0)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "We define a function `vc_gen` that generates **verification conditions** using the principle of induction:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 11,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def vc_gen(T):\n",
        "    '''Verification Condition (VC) for an Inductive Invariant'''\n",
        "    Inv = z3.Function('Inv', *(T.sig() + [z3.BoolSort()]))\n",
        "\n",
        "    InvPre = Inv(*T.pre_vars())\n",
        "    InvPost = Inv(*T.post_vars())\n",
        "\n",
        "    all_vars = T.all()\n",
        "    vc_init = z3.ForAll(all_vars, z3.Implies(T.Init, InvPre))\n",
        "    vc_ind = z3.ForAll(all_vars, z3.Implies(z3.And(InvPre, T.Tr), InvPost))\n",
        "    vc_bad = z3.ForAll(all_vars, z3.Implies(z3.And(InvPre, T.Bad), z3.BoolVal(False)))\n",
        "    return [vc_init, vc_ind, vc_bad], InvPre"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 12,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "vc, inv = vc_gen(ts0)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 13,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;x, x' : x &le; 0 &rArr; Inv(x) <br/><br/>&forall;x, x' : Inv(x) &and; x &lt; 5 &and; x' = x + 1 &rArr; Inv(x') <br/><br/>&forall;x, x' : Inv(x) &and; x &ge; 10 &rArr; False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;x, x' : x &le; 0 &rArr; Inv(x) <br/><br/>&forall;x, x' : Inv(x) &and; x &lt; 5 &and; x' = x + 1 &rArr; Inv(x') <br/><br/>&forall;x, x' : Inv(x) &and; x &ge; 10 &rArr; False <br/><br/>\""
            ]
          },
          "execution_count": 13,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "chc_to_str(vc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 14,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "Inv(x)"
            ],
            "text/plain": [
              "'Inv(x)'"
            ]
          },
          "execution_count": 14,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "HtmlStr(inv)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 15,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "res, answer = solve_horn(vc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 16,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 16,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 17,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "[Inv = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 6)]]"
            ],
            "text/plain": [
              "[Inv = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 6)]]"
            ]
          },
          "execution_count": 17,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 18,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(x &ge; 6)"
            ],
            "text/plain": [
              "&not;(x &ge; 6)"
            ]
          },
          "execution_count": 18,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(inv)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 19,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "Transition System: Ts0<br/>\tInit: x &le; 0<br/>\tBad: x &ge; 4<br/>\tTr: x &lt; 5 &and; x' = x + 1"
            ],
            "text/plain": [
              "\"Transition System: Ts0<br/>\\tInit: x &le; 0<br/>\\tBad: x &ge; 4<br/>\\tTr: x &lt; 5 &and; x' = x + 1\""
            ]
          },
          "execution_count": 19,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "ts0 = mk_ts0(safe=False)\n",
        "HtmlStr(ts0)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 20,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>unsat</b>"
            ],
            "text/plain": [
              "'<b>unsat</b>'"
            ]
          },
          "execution_count": 20,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, inv = vc_gen(ts0)\n",
        "res, answer = solve_horn(vc)\n",
        "HtmlStr(res)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 21,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "mp(hyper-res(asserted(&forall;A : Inv(A) &and; A &ge; 4 &rArr; query!19(A)),\n",
              "             hyper-res(asserted(&forall;A, B :\n",
              "                                 Inv(A) &and;\n",
              "                                 &not;(5 &le; A) &and;\n",
              "                                 B = 1 + A &rArr;\n",
              "                                 Inv(B)),\n",
              "                       hyper-res(asserted(&forall;A, B :\n",
              "                                        Inv(A) &and;\n",
              "                                        &not;(5 &le; A) &and;\n",
              "                                        B = 1 + A &rArr;\n",
              "                                        Inv(B)),\n",
              "                                 hyper-res(asserted(&forall;A, B :\n",
              "                                        Inv(A) &and;\n",
              "                                        &not;(5 &le; A) &and;\n",
              "                                        B = 1 + A &rArr;\n",
              "                                        Inv(B)),\n",
              "                                        hyper-res(asserted(&forall;A,\n",
              "                                        B :\n",
              "                                        Inv(A) &and;\n",
              "                                        &not;(5 &le; A) &and;\n",
              "                                        B = 1 + A &rArr;\n",
              "                                        Inv(B)),\n",
              "                                        hyper-res(asserted(&forall;A :\n",
              "                                        A &le; 0 &rArr; Inv(A)),\n",
              "                                        Inv(0)),\n",
              "                                        Inv(1)),\n",
              "                                        Inv(2)),\n",
              "                                 Inv(3)),\n",
              "                       Inv(4)),\n",
              "             query!19(4)),\n",
              "   asserted(query!19(4) &rArr; False),\n",
              "   False)"
            ],
            "text/plain": [
              "mp(hyper-res(asserted(&forall;A : Inv(A) &and; A &ge; 4 &rArr; query!19(A)),\n",
              "             hyper-res(asserted(&forall;A, B :\n",
              "                                 Inv(A) &and;\n",
              "                                 &not;(5 &le; A) &and;\n",
              "                                 B = 1 + A &rArr;\n",
              "                                 Inv(B)),\n",
              "                       hyper-res(asserted(&forall;A, B :\n",
              "                                        Inv(A) &and;\n",
              "                                        &not;(5 &le; A) &and;\n",
              "                                        B = 1 + A &rArr;\n",
              "                                        Inv(B)),\n",
              "                                 hyper-res(asserted(&forall;A, B :\n",
              "                                        Inv(A) &and;\n",
              "                                        &not;(5 &le; A) &and;\n",
              "                                        B = 1 + A &rArr;\n",
              "                                        Inv(B)),\n",
              "                                        hyper-res(asserted(&forall;A,\n",
              "                                        B :\n",
              "                                        Inv(A) &and;\n",
              "                                        &not;(5 &le; A) &and;\n",
              "                                        B = 1 + A &rArr;\n",
              "                                        Inv(B)),\n",
              "                                        hyper-res(asserted(&forall;A :\n",
              "                                        A &le; 0 &rArr; Inv(A)),\n",
              "                                        Inv(0)),\n",
              "                                        Inv(1)),\n",
              "                                        Inv(2)),\n",
              "                                 Inv(3)),\n",
              "                       Inv(4)),\n",
              "             query!19(4)),\n",
              "   asserted(query!19(4) &rArr; False),\n",
              "   False)"
            ]
          },
          "execution_count": 21,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "The result is **unsat** and the certificate is a resolution proof. Since the proof is not easy to read, we abstract it by a graph, preserving only the instances of CHC predicates that are used in resolution steps:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 27,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"113pt\" height=\"404pt\"\n",
              " viewBox=\"0.00 0.00 113.29 404.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 400)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-400 109.29,-400 109.29,4 -4,4\"/>\n",
              "<!-- 1567 -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>1567</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-18\" rx=\"52.79\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">query!19(4)</text>\n",
              "</g>\n",
              "<!-- 1614 -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>1614</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-90\" rx=\"32.49\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">Inv(4)</text>\n",
              "</g>\n",
              "<!-- 1614&#45;&gt;1567 -->\n",
              "<g id=\"edge5\" class=\"edge\">\n",
              "<title>1614&#45;&gt;1567</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-71.7C52.65,-64.41 52.65,-55.73 52.65,-47.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-47.62 52.65,-37.62 49.15,-47.62 56.15,-47.62\"/>\n",
              "</g>\n",
              "<!-- 1621 -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>1621</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-162\" rx=\"32.49\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">Inv(3)</text>\n",
              "</g>\n",
              "<!-- 1621&#45;&gt;1614 -->\n",
              "<g id=\"edge4\" class=\"edge\">\n",
              "<title>1621&#45;&gt;1614</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-143.7C52.65,-136.41 52.65,-127.73 52.65,-119.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-119.62 52.65,-109.62 49.15,-119.62 56.15,-119.62\"/>\n",
              "</g>\n",
              "<!-- 1592 -->\n",
              "<g id=\"node4\" class=\"node\">\n",
              "<title>1592</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-234\" rx=\"32.49\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">Inv(2)</text>\n",
              "</g>\n",
              "<!-- 1592&#45;&gt;1621 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>1592&#45;&gt;1621</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-215.7C52.65,-208.41 52.65,-199.73 52.65,-191.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-191.62 52.65,-181.62 49.15,-191.62 56.15,-191.62\"/>\n",
              "</g>\n",
              "<!-- 1574 -->\n",
              "<g id=\"node5\" class=\"node\">\n",
              "<title>1574</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-306\" rx=\"32.49\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\">Inv(1)</text>\n",
              "</g>\n",
              "<!-- 1574&#45;&gt;1592 -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>1574&#45;&gt;1592</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-287.7C52.65,-280.41 52.65,-271.73 52.65,-263.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-263.62 52.65,-253.62 49.15,-263.62 56.15,-263.62\"/>\n",
              "</g>\n",
              "<!-- 1617 -->\n",
              "<g id=\"node6\" class=\"node\">\n",
              "<title>1617</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-378\" rx=\"32.49\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\">Inv(0)</text>\n",
              "</g>\n",
              "<!-- 1617&#45;&gt;1574 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>1617&#45;&gt;1574</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-359.7C52.65,-352.41 52.65,-343.73 52.65,-335.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-335.62 52.65,-325.62 49.15,-335.62 56.15,-335.62\"/>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<__main__.SpacerProof at 0x112dce640>"
            ]
          },
          "execution_count": 27,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "sp = SpacerProof(answer)\n",
        "sp"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "The shortest counter-example is to start the counter at `0` and count until `4`, at which point the bad state is reached."
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Principle of Backward Induction\n",
        "\n",
        "Sometimes forward induction is not effective. One alternative is to run the analysis backwards.\n",
        "A counter-example starts from a bad state and goes towards initial state. There is no need to change the\n",
        "underlying sat algorithm for that. We simply change the encoding!\n",
        "\n",
        "A **backward inductive invariant** for $P = (V, Init, Tr, Bad)$ is a formula $BInv$ such that \n",
        "   \n",
        "  1. $Bad \\implies BInv$\n",
        "  2. $BInv' \\wedge Tr \\implies Binv$\n",
        "  3. $BInv \\wedge Init \\implies False$\n",
        "    \n",
        "**Fact**: If $BInv$ is a backward inductive invariant for $P$, then $\\neg BInv$ is an inductive invariant for $P$."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 28,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def vc_gen_bwd(T):\n",
        "    '''Verification Condition (VC) for Backward Inductive Invariant'''\n",
        "\n",
        "    Inv = z3.Function('BwdInv', *(T.sig() + [z3.BoolSort()]))\n",
        "\n",
        "    InvPre = Inv(*T.pre_vars())\n",
        "    InvPost = Inv(*T.post_vars())\n",
        "\n",
        "    all_vars = T.all()\n",
        "    vc_init = z3.ForAll(all_vars, z3.Implies(T.Bad, InvPre))\n",
        "    vc_ind = z3.ForAll(all_vars, z3.Implies(z3.And(InvPost, T.Tr), InvPre))\n",
        "    vc_bad = z3.ForAll(all_vars, z3.Implies(z3.And(InvPre, T.Init), z3.BoolVal(False)))\n",
        "\n",
        "    return [vc_init, vc_ind, vc_bad], InvPre"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 29,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;x, x' : x &ge; 10 &rArr; BwdInv(x) <br/><br/>&forall;x, x' : BwdInv(x') &and; x &lt; 5 &and; x' = x + 1 &rArr; BwdInv(x) <br/><br/>&forall;x, x' : BwdInv(x) &and; x &le; 0 &rArr; False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;x, x' : x &ge; 10 &rArr; BwdInv(x) <br/><br/>&forall;x, x' : BwdInv(x') &and; x &lt; 5 &and; x' = x + 1 &rArr; BwdInv(x) <br/><br/>&forall;x, x' : BwdInv(x) &and; x &le; 0 &rArr; False <br/><br/>\""
            ]
          },
          "execution_count": 29,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "ts0 = mk_ts0(safe=True)\n",
        "vc, inv = vc_gen_bwd(ts0)\n",
        "chc_to_str(vc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 30,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(x &le; 9)"
            ],
            "text/plain": [
              "&not;(x &le; 9)"
            ]
          },
          "execution_count": 30,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "res, answer = solve_horn(vc)\n",
        "answer.eval(inv)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 31,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"113pt\" height=\"404pt\"\n",
              " viewBox=\"0.00 0.00 113.29 404.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 400)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-400 109.29,-400 109.29,4 -4,4\"/>\n",
              "<!-- 916 -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>916</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-18\" rx=\"52.79\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">query!67(0)</text>\n",
              "</g>\n",
              "<!-- 1051 -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>1051</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-90\" rx=\"49.29\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">BwdInv(0)</text>\n",
              "</g>\n",
              "<!-- 1051&#45;&gt;916 -->\n",
              "<g id=\"edge5\" class=\"edge\">\n",
              "<title>1051&#45;&gt;916</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-71.7C52.65,-64.41 52.65,-55.73 52.65,-47.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-47.62 52.65,-37.62 49.15,-47.62 56.15,-47.62\"/>\n",
              "</g>\n",
              "<!-- 1854 -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>1854</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-162\" rx=\"49.29\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">BwdInv(1)</text>\n",
              "</g>\n",
              "<!-- 1854&#45;&gt;1051 -->\n",
              "<g id=\"edge4\" class=\"edge\">\n",
              "<title>1854&#45;&gt;1051</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-143.7C52.65,-136.41 52.65,-127.73 52.65,-119.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-119.62 52.65,-109.62 49.15,-119.62 56.15,-119.62\"/>\n",
              "</g>\n",
              "<!-- 1339 -->\n",
              "<g id=\"node4\" class=\"node\">\n",
              "<title>1339</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-234\" rx=\"49.29\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">BwdInv(2)</text>\n",
              "</g>\n",
              "<!-- 1339&#45;&gt;1854 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>1339&#45;&gt;1854</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-215.7C52.65,-208.41 52.65,-199.73 52.65,-191.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-191.62 52.65,-181.62 49.15,-191.62 56.15,-191.62\"/>\n",
              "</g>\n",
              "<!-- 407 -->\n",
              "<g id=\"node5\" class=\"node\">\n",
              "<title>407</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-306\" rx=\"49.29\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\">BwdInv(3)</text>\n",
              "</g>\n",
              "<!-- 407&#45;&gt;1339 -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>407&#45;&gt;1339</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-287.7C52.65,-280.41 52.65,-271.73 52.65,-263.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-263.62 52.65,-253.62 49.15,-263.62 56.15,-263.62\"/>\n",
              "</g>\n",
              "<!-- 1809 -->\n",
              "<g id=\"node6\" class=\"node\">\n",
              "<title>1809</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"52.65\" cy=\"-378\" rx=\"49.29\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"52.65\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\">BwdInv(4)</text>\n",
              "</g>\n",
              "<!-- 1809&#45;&gt;407 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>1809&#45;&gt;407</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M52.65,-359.7C52.65,-352.41 52.65,-343.73 52.65,-335.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"56.15,-335.62 52.65,-325.62 49.15,-335.62 56.15,-335.62\"/>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<__main__.SpacerProof at 0x112858670>"
            ]
          },
          "execution_count": 31,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "ts0 = mk_ts0(safe=False)\n",
        "vc, inv = vc_gen_bwd(ts0)\n",
        "res, answer = solve_horn(vc)\n",
        "SpacerProof(answer)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "As expected, the counter-example runs backward. Starting fromt the bad state and evolving to the initial state."
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## The principle of 2-induction\n",
        "\n",
        "2-induction, or more generally, $k$-induction is a strengthening of the principle of induction. It allows assuming inductive hypothesis for multiple steps of the transtion relation.\n",
        "\n",
        "A **2-inductive invariant** for a system $P = (V, Init, Tr, Bad)$ is a formula $2Inv$ such that\n",
        "\n",
        "   1. (initiataion 1) $Init \\implies 2Inv$\n",
        "   2. (initiation 2)  $Init \\wedge Tr \\implies 2Inv'$\n",
        "   3. (2-induction)   $2Inv \\wedge Tr \\wedge 2Inv' \\wedge Tr' \\implies 2Inv''$\n",
        "   4. (safety)        $2Inv \\wedge Bad \\implies False$\n",
        "   \n",
        "Fromt the above definition, it is obvious that discovering a 2-inductive hypothesis is reducible to satisfiablity of *non-linear* CHC."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 32,
      "metadata": {
        "code_folding": [
          1
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "# helper function to compute sequential composition by connecting output of T1 to input of T2\n",
        "def mk_seq(T1, T2, constraint = None):\n",
        "    \"\"\"\n",
        "    Constructs a sequential composition of two transition systems.\n",
        "\n",
        "    An optional constraint is added on the glue variables of the composition.\n",
        "    The constraint must be specified over pre-state variables of T1\n",
        "    \"\"\"\n",
        "    assert len(T1.post_vars()) == len(T2.post_vars())\n",
        "    assert len(T1.inputs()) == 0, \"Not supported yet\"\n",
        "    assert len(T2.inputs()) == 0, \"Not supported yet\"\n",
        "\n",
        "    for v1, v2 in zip(T1.post_vars(), T2.pre_vars()):\n",
        "        assert(v1.sort() == v2.sort())\n",
        "\n",
        "    TSeq = Ts(T1.name + ';' + T2.name)\n",
        "    for idx, v in enumerate(T1.pre_vars()):\n",
        "        TSeq.add_var(v.sort(), T1.get_var_name(idx))\n",
        "\n",
        "    glue = [TSeq.add_input(v.sort()) for v in T1.post_vars()]\n",
        "    Tr1 = z3.substitute(T1.Tr, *list(zip(T1.post_vars(), glue)))\n",
        "    Tr2 = z3.substitute(T2.Tr, *list(zip(T2.pre_vars(), glue)))\n",
        "\n",
        "    # if there is an optional constraint, shift it to the glue variables\n",
        "    C = z3.BoolVal(True)\n",
        "    if constraint is not None:\n",
        "       C = z3.substitute(constraint, *list(zip(T1.pre_vars(), glue)))\n",
        "\n",
        "    TSeq.Tr = z3.simplify(z3.And(Tr1, Tr2, C))\n",
        "\n",
        "    TSeq.Init = T1.Init\n",
        "    TSeq.Bad = T2.Bad\n",
        "\n",
        "    return TSeq\n",
        "\n",
        "def vc_gen_2ind(T):\n",
        "    \"\"\"Verification condition for 2-inductive invariant\"\"\"\n",
        "    Inv = z3.Function('2Inv', *(T.sig() + [z3.BoolSort()]))\n",
        "\n",
        "    InvPre = Inv(*T.pre_vars())\n",
        "    InvPost = Inv(*T.post_vars())\n",
        "\n",
        "    all_vars = T.all()\n",
        "    # Inv contains initial states\n",
        "    vc_init1 = z3.ForAll(all_vars, z3.Implies(T.Init, InvPre))\n",
        "    # Inv contains states reachable in one step\n",
        "    vc_init2 = z3.ForAll(all_vars, z3.Implies(z3.And(T.Init, T.Tr), InvPost))\n",
        "\n",
        "    # Inv is stable under two steps of Tr , assuming Inv holds after first step\n",
        "    TSeq = mk_seq(T, T, constraint = InvPre)\n",
        "    InvPost = Inv(*TSeq.post_vars())\n",
        "    all_vars = TSeq.all()\n",
        "    vc_ind = z3.ForAll(all_vars, z3.Implies(z3.And(InvPre, TSeq.Tr), InvPost))\n",
        "\n",
        "    # Inv does not satisfy Bad\n",
        "    vc_bad = z3.ForAll(all_vars, z3.Implies(z3.And(InvPre, T.Bad), z3.BoolVal(False)))\n",
        "\n",
        "    return [vc_init1, vc_init2, vc_ind, vc_bad], InvPre"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 33,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;x, x' : x &le; 0 &rArr; 2Inv(x) <br/><br/>&forall;x, x' : x &le; 0 &and; x &lt; 5 &and; x' = x + 1 &rArr; 2Inv(x') <br/><br/>&forall;x, x', i_0 :<br/> 2Inv(x) &and;<br/> &not;(5 &le; x) &and;<br/> i_0 = 1 + x &and;<br/> &not;(5 &le; i_0) &and;<br/> x' = 1 + i_0 &and;<br/> 2Inv(i_0) &rArr;<br/> 2Inv(x') <br/><br/>&forall;x, x', i_0 : 2Inv(x) &and; x &ge; 10 &rArr; False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;x, x' : x &le; 0 &rArr; 2Inv(x) <br/><br/>&forall;x, x' : x &le; 0 &and; x &lt; 5 &and; x' = x + 1 &rArr; 2Inv(x') <br/><br/>&forall;x, x', i_0 :<br/> 2Inv(x) &and;<br/> &not;(5 &le; x) &and;<br/> i_0 = 1 + x &and;<br/> &not;(5 &le; i_0) &and;<br/> x' = 1 + i_0 &and;<br/> 2Inv(i_0) &rArr;<br/> 2Inv(x') <br/><br/>&forall;x, x', i_0 : 2Inv(x) &and; x &ge; 10 &rArr; False <br/><br/>\""
            ]
          },
          "execution_count": 33,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "ts0 = mk_ts0(safe=True)\n",
        "vc, inv = vc_gen_2ind(ts0)\n",
        "chc_to_str(vc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 34,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(x &ge; 6)"
            ],
            "text/plain": [
              "&not;(x &ge; 6)"
            ]
          },
          "execution_count": 34,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "res, answer = solve_horn(vc)\n",
        "answer.eval(inv)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 35,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"188pt\" height=\"476pt\"\n",
              " viewBox=\"0.00 0.00 187.59 476.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 472)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-472 183.59,-472 183.59,4 -4,4\"/>\n",
              "<!-- 2246 -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>2246</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"72.3\" cy=\"-18\" rx=\"52.79\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"72.3\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">query!97(4)</text>\n",
              "</g>\n",
              "<!-- 2302 -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>2302</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"72.3\" cy=\"-90\" rx=\"37.09\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"72.3\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">2Inv(4)</text>\n",
              "</g>\n",
              "<!-- 2302&#45;&gt;2246 -->\n",
              "<g id=\"edge11\" class=\"edge\">\n",
              "<title>2302&#45;&gt;2246</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M72.3,-71.7C72.3,-64.41 72.3,-55.73 72.3,-47.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"75.8,-47.62 72.3,-37.62 68.8,-47.62 75.8,-47.62\"/>\n",
              "</g>\n",
              "<!-- 2386 -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>2386</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"40.3\" cy=\"-162\" rx=\"37.09\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"40.3\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">2Inv(3)</text>\n",
              "</g>\n",
              "<!-- 2386&#45;&gt;2302 -->\n",
              "<g id=\"edge9\" class=\"edge\">\n",
              "<title>2386&#45;&gt;2302</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M48.04,-144.05C51.62,-136.23 55.95,-126.75 59.96,-117.98\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"63.02,-119.72 63.99,-109.17 56.65,-116.81 63.02,-119.72\"/>\n",
              "</g>\n",
              "<!-- 2388 -->\n",
              "<g id=\"node4\" class=\"node\">\n",
              "<title>2388</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"105.3\" cy=\"-234\" rx=\"37.09\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"105.3\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">2Inv(2)</text>\n",
              "</g>\n",
              "<!-- 2388&#45;&gt;2302 -->\n",
              "<g id=\"edge10\" class=\"edge\">\n",
              "<title>2388&#45;&gt;2302</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M101.9,-215.88C98.27,-197.92 92.24,-168.9 86.3,-144 84.37,-135.91 82.12,-127.18 80.01,-119.17\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"83.41,-118.35 77.44,-109.6 76.65,-120.16 83.41,-118.35\"/>\n",
              "</g>\n",
              "<!-- 2388&#45;&gt;2386 -->\n",
              "<g id=\"edge7\" class=\"edge\">\n",
              "<title>2388&#45;&gt;2386</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M90.55,-217.12C82.32,-208.26 71.9,-197.04 62.69,-187.12\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"65.39,-184.88 56.02,-179.93 60.26,-189.64 65.39,-184.88\"/>\n",
              "</g>\n",
              "<!-- 2378 -->\n",
              "<g id=\"node5\" class=\"node\">\n",
              "<title>2378</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"40.3\" cy=\"-306\" rx=\"37.09\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"40.3\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\">2Inv(1)</text>\n",
              "</g>\n",
              "<!-- 2378&#45;&gt;2386 -->\n",
              "<g id=\"edge8\" class=\"edge\">\n",
              "<title>2378&#45;&gt;2386</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M40.3,-287.59C40.3,-263.61 40.3,-220.14 40.3,-191.42\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"43.8,-191.62 40.3,-181.62 36.8,-191.62 43.8,-191.62\"/>\n",
              "</g>\n",
              "<!-- 2378&#45;&gt;2388 -->\n",
              "<g id=\"edge5\" class=\"edge\">\n",
              "<title>2378&#45;&gt;2388</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M55.05,-289.12C63.27,-280.26 73.69,-269.04 82.9,-259.12\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"85.34,-261.64 89.58,-251.93 80.21,-256.88 85.34,-261.64\"/>\n",
              "</g>\n",
              "<!-- 2366 -->\n",
              "<g id=\"node6\" class=\"node\">\n",
              "<title>2366</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"105.3\" cy=\"-378\" rx=\"37.09\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"105.3\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\">2Inv(0)</text>\n",
              "</g>\n",
              "<!-- 2366&#45;&gt;2388 -->\n",
              "<g id=\"edge6\" class=\"edge\">\n",
              "<title>2366&#45;&gt;2388</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M105.3,-359.59C105.3,-335.61 105.3,-292.14 105.3,-263.42\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"108.8,-263.62 105.3,-253.62 101.8,-263.62 108.8,-263.62\"/>\n",
              "</g>\n",
              "<!-- 2366&#45;&gt;2378 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>2366&#45;&gt;2378</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M90.55,-361.12C82.32,-352.26 71.9,-341.04 62.69,-331.12\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"65.39,-328.88 56.02,-323.93 60.26,-333.64 65.39,-328.88\"/>\n",
              "</g>\n",
              "<!-- 2277 -->\n",
              "<g id=\"node7\" class=\"node\">\n",
              "<title>2277</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"40.3\" cy=\"-450\" rx=\"40.09\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"40.3\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\">2Inv(&#45;1)</text>\n",
              "</g>\n",
              "<!-- 2277&#45;&gt;2378 -->\n",
              "<g id=\"edge4\" class=\"edge\">\n",
              "<title>2277&#45;&gt;2378</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M40.3,-431.59C40.3,-407.61 40.3,-364.14 40.3,-335.42\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"43.8,-335.62 40.3,-325.62 36.8,-335.62 43.8,-335.62\"/>\n",
              "</g>\n",
              "<!-- 2277&#45;&gt;2366 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>2277&#45;&gt;2366</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M55.05,-433.12C63.27,-424.26 73.69,-413.04 82.9,-403.12\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"85.34,-405.64 89.58,-395.93 80.21,-400.88 85.34,-405.64\"/>\n",
              "</g>\n",
              "<!-- 2307 -->\n",
              "<g id=\"node8\" class=\"node\">\n",
              "<title>2307</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"139.3\" cy=\"-450\" rx=\"40.09\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"139.3\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\">2Inv(&#45;2)</text>\n",
              "</g>\n",
              "<!-- 2307&#45;&gt;2366 -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>2307&#45;&gt;2366</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M131.07,-432.05C127.27,-424.23 122.66,-414.75 118.4,-405.98\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"121.63,-404.62 114.11,-397.15 115.33,-407.67 121.63,-404.62\"/>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<__main__.SpacerProof at 0x112ba2970>"
            ]
          },
          "execution_count": 35,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "ts0 = mk_ts0(safe=False)\n",
        "vc, inv = vc_gen_2ind(ts0)\n",
        "res, answer = solve_horn(vc)\n",
        "SpacerProof(answer)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Spacer often finds the shortest counterexample. The counterexample above is short (4 transitions), but maybe not the most obvious one."
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Control Flow Automaton (CFA)\n",
        "\n",
        "It is often desired to extend a transition system with control locations. \n",
        "A **Control Flow Automaton (CFA)** is a graph \n",
        "$G = (V, E, entry, exit, \\tau)$, where\n",
        "\n",
        "  1. $V$ is a set of control locations\n",
        "  2. $E \\subseteq V \\times V$ is a set of control flow edges\n",
        "  3. $entry \\in V$, $exit \\in V$ are designated *entry* and *exit* locations\n",
        "  4. $\\tau : E \\to Tr$ maps each edge in $E$ to a transition relation\n",
        "  \n",
        "A CFA $A$ is **SAFE** if there is no path $\\pi$ from $entry$ to $exit$ that each edge on $\\pi$ satisfies the corresponding transition relation.\n",
        "\n",
        "A CFA $A$ is **SAFE** if and only iff there exists an **inductive invariant map** $\\sigma : V \\to Fml$ such that \n",
        "\n",
        "   1. (initiation) $\\sigma(entry) = True$\n",
        "   2. (safety) $\\sigma(exit) = False$\n",
        "   3. (induction) for every edge $(u, v) \\in E$, $\\sigma(u) \\wedge \\tau(u, v) \\implies \\sigma(v)'$"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "We begin by defining a python class to represent a CFA:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 36,
      "metadata": {
        "code_folding": [
          5,
          12,
          14,
          16,
          18,
          20,
          22,
          24,
          26,
          28,
          30,
          32,
          36,
          39,
          42,
          44,
          47
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "class CFA(object):\n",
        "    '''Control Flow Automaton\n",
        "\n",
        "    An automation whose nodes are annotated with transition relations\n",
        "    '''\n",
        "    def __init__(self, name):\n",
        "        self._base = Ts(name)\n",
        "\n",
        "        self.entry = None\n",
        "        self.exit = None\n",
        "        self.edges = dict()\n",
        "        self.nodes = set()\n",
        "    def sig(self):\n",
        "        return self._base.sig()\n",
        "    def inputs(self):\n",
        "        return self._base.inputs()\n",
        "    def pre_vars(self):\n",
        "        return self._base.pre_vars()\n",
        "    def post_vars(self):\n",
        "        return self._base.post_vars()\n",
        "    def vars(self):\n",
        "        return self._base.vars()\n",
        "    def pre_post_vars(self):\n",
        "        return self._base.pre_post_vars()\n",
        "    def all(self):\n",
        "        return self._base.all()\n",
        "    def add_var(self, sort, name=None):\n",
        "        return self._base.add_var(sort, name)\n",
        "    def add_input(self, sort, name=None):\n",
        "        return self._base.add_input(sort, name)\n",
        "    def to_post(self, e):\n",
        "        return self._base.to_post(e)\n",
        "    def add_edge(self, src, dst, tr):\n",
        "        self.nodes.add(src)\n",
        "        self.nodes.add(dst)\n",
        "        self.edges[(src, dst)] = tr\n",
        "    def set_entry_node(self, n):\n",
        "        self.nodes.add(n)\n",
        "        self.entry = n\n",
        "    def set_exit_node(self, n):\n",
        "        self.nodes.add(n)\n",
        "        self.exit = n\n",
        "    def is_entry_node(self, n):\n",
        "        return n == self.entry\n",
        "    def is_exit_node(self, n):\n",
        "        return n == self.exit\n",
        "\n",
        "    def to_dot(self):\n",
        "        import graphviz\n",
        "        g = graphviz.Digraph()\n",
        "\n",
        "        for n in self.nodes:\n",
        "            g.node(str(n), str(n))\n",
        "\n",
        "        for (k, v) in self.edges.items():\n",
        "            src, dst = k\n",
        "            g.edge(str(src), str(dst), label=str(v))\n",
        "\n",
        "        return g"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Then, convert our running example to a CFA:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 37,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"179pt\" height=\"218pt\"\n",
              " viewBox=\"0.00 0.00 179.00 218.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 214)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-214 175,-214 175,4 -4,4\"/>\n",
              "<!-- L1 -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>L1</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"27\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L1 -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M51.53,-113.03C62.51,-113.79 72,-111.12 72,-105 72,-101.18 68.29,-98.7 62.83,-97.56\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"63.21,-94.08 53.04,-97.05 62.85,-101.07 63.21,-94.08\"/>\n",
              "<text text-anchor=\"middle\" x=\"121.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">x ≤ 5 ∧ x&#39; = x + 1</text>\n",
              "</g>\n",
              "<!-- L2 -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>L2</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"27\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"27\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">L2</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L2 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L2</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M27,-86.8C27,-75.58 27,-60.67 27,-47.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"30.5,-47.98 27,-37.98 23.5,-47.98 30.5,-47.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"45\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">x ≥ 10</text>\n",
              "</g>\n",
              "<!-- L0 -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>L0</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"27\" cy=\"-192\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"27\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
              "</g>\n",
              "<!-- L0&#45;&gt;L1 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>L0&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M27,-173.8C27,-162.58 27,-147.67 27,-134.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"30.5,-134.98 27,-124.98 23.5,-134.98 30.5,-134.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"43\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">x&#39; = 0</text>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<graphviz.graphs.Digraph at 0x112d7cd30>"
            ]
          },
          "execution_count": 37,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_cfa0(safe=True):\n",
        "    A = CFA('prog')\n",
        "    x, x_out = A.add_var(z3.IntSort(), name='x')\n",
        "\n",
        "    A.add_edge('L0', 'L1', x_out == 0)\n",
        "    A.add_edge('L1', 'L1', z3.And(x <= 5, x_out == x + 1))\n",
        "    if safe:\n",
        "        A.add_edge('L1', 'L2', x >= 10)\n",
        "    else:\n",
        "        A.add_edge('L1', 'L2', x >= 4)\n",
        "\n",
        "    A.set_entry_node('L0')\n",
        "    A.set_exit_node('L2')\n",
        "    return A\n",
        "cfa0 = mk_cfa0(safe=True)\n",
        "cfa0.to_dot()"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "To compute an inductive map, we define a CHC system with one uninterpreted predicate per control location. In our running example above, we will have 3 predicates representing invariants at location $L_0$, $L_1$, and $L_2$, respectively:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 38,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def cfa_vc_gen(A):\n",
        "    '''Verification Condition (VC) for a Control Flow Automaton'''\n",
        "    all_vars = A.all()\n",
        "    sig = A.sig() + [z3.BoolSort()]\n",
        "\n",
        "    Invs = dict()\n",
        "    for n in A.nodes:\n",
        "        inv = z3.Function(str(n), *sig)\n",
        "        Invs[n] = inv\n",
        "\n",
        "    Entry = Invs[A.entry]\n",
        "    Exit = Invs[A.exit]\n",
        "\n",
        "    vc = list()\n",
        "    vc.append(z3.ForAll(all_vars, Entry(*A.pre_vars())))\n",
        "\n",
        "    for (k, v) in A.edges.items():\n",
        "        src, dst = k\n",
        "        srcP, dstP = Invs[src], Invs[dst]\n",
        "\n",
        "        head = dstP(*A.post_vars())\n",
        "        sPred = srcP(*A.pre_vars())\n",
        "        vc.append(z3.ForAll(all_vars, z3.Implies(z3.And(sPred, v), head)))\n",
        "    vc.append(z3.ForAll(all_vars,\n",
        "                        z3.Implies(Exit(*A.pre_vars()), z3.BoolVal(False))))\n",
        "    return vc, {n : Invs[n](A.pre_vars()) for n in A.nodes}"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 39,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;x, x' : L0(x) <br/><br/>&forall;x, x' : L0(x) &and; x' = 0 &rArr; L1(x') <br/><br/>&forall;x, x' : L1(x) &and; x &le; 5 &and; x' = x + 1 &rArr; L1(x') <br/><br/>&forall;x, x' : L1(x) &and; x &ge; 10 &rArr; L2(x') <br/><br/>&forall;x, x' : L2(x) &rArr; False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;x, x' : L0(x) <br/><br/>&forall;x, x' : L0(x) &and; x' = 0 &rArr; L1(x') <br/><br/>&forall;x, x' : L1(x) &and; x &le; 5 &and; x' = x + 1 &rArr; L1(x') <br/><br/>&forall;x, x' : L1(x) &and; x &ge; 10 &rArr; L2(x') <br/><br/>&forall;x, x' : L2(x) &rArr; False <br/><br/>\""
            ]
          },
          "execution_count": 39,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "chc, invs = cfa_vc_gen(cfa0)\n",
        "chc_to_str(chc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 40,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 40,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "res, answer = solve_horn(chc)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 41,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/plain": [
              "{'L1': L1(x), 'L2': L2(x), 'L0': L0(x)}"
            ]
          },
          "execution_count": 41,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "invs"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 42,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "True"
            ],
            "text/plain": [
              "True"
            ]
          },
          "execution_count": 42,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(invs['L0'])"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 43,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(x &ge; 7)"
            ],
            "text/plain": [
              "&not;(x &ge; 7)"
            ]
          },
          "execution_count": 43,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(invs['L1'])"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 44,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "False"
            ],
            "text/plain": [
              "False"
            ]
          },
          "execution_count": 44,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(invs['L2'])"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 45,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"122pt\" height=\"476pt\"\n",
              " viewBox=\"0.00 0.00 122.39 476.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 472)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-472 118.39,-472 118.39,4 -4,4\"/>\n",
              "<!-- 232 -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>232</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"57.19\" cy=\"-18\" rx=\"57.39\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"57.19\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">query!136(0)</text>\n",
              "</g>\n",
              "<!-- 227 -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>227</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"57.19\" cy=\"-90\" rx=\"30.59\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"57.19\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">L2(0)</text>\n",
              "</g>\n",
              "<!-- 227&#45;&gt;232 -->\n",
              "<g id=\"edge6\" class=\"edge\">\n",
              "<title>227&#45;&gt;232</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M57.19,-71.7C57.19,-64.41 57.19,-55.73 57.19,-47.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"60.7,-47.62 57.19,-37.62 53.7,-47.62 60.7,-47.62\"/>\n",
              "</g>\n",
              "<!-- 593 -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>593</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"57.19\" cy=\"-162\" rx=\"30.59\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"57.19\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1(4)</text>\n",
              "</g>\n",
              "<!-- 593&#45;&gt;227 -->\n",
              "<g id=\"edge5\" class=\"edge\">\n",
              "<title>593&#45;&gt;227</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M57.19,-143.7C57.19,-136.41 57.19,-127.73 57.19,-119.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"60.7,-119.62 57.19,-109.62 53.7,-119.62 60.7,-119.62\"/>\n",
              "</g>\n",
              "<!-- 631 -->\n",
              "<g id=\"node4\" class=\"node\">\n",
              "<title>631</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"57.19\" cy=\"-234\" rx=\"30.59\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"57.19\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1(3)</text>\n",
              "</g>\n",
              "<!-- 631&#45;&gt;593 -->\n",
              "<g id=\"edge4\" class=\"edge\">\n",
              "<title>631&#45;&gt;593</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M57.19,-215.7C57.19,-208.41 57.19,-199.73 57.19,-191.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"60.7,-191.62 57.19,-181.62 53.7,-191.62 60.7,-191.62\"/>\n",
              "</g>\n",
              "<!-- 336 -->\n",
              "<g id=\"node5\" class=\"node\">\n",
              "<title>336</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"57.19\" cy=\"-306\" rx=\"30.59\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"57.19\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1(2)</text>\n",
              "</g>\n",
              "<!-- 336&#45;&gt;631 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>336&#45;&gt;631</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M57.19,-287.7C57.19,-280.41 57.19,-271.73 57.19,-263.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"60.7,-263.62 57.19,-253.62 53.7,-263.62 60.7,-263.62\"/>\n",
              "</g>\n",
              "<!-- 1429 -->\n",
              "<g id=\"node6\" class=\"node\">\n",
              "<title>1429</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"57.19\" cy=\"-378\" rx=\"30.59\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"57.19\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1(1)</text>\n",
              "</g>\n",
              "<!-- 1429&#45;&gt;336 -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>1429&#45;&gt;336</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M57.19,-359.7C57.19,-352.41 57.19,-343.73 57.19,-335.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"60.7,-335.62 57.19,-325.62 53.7,-335.62 60.7,-335.62\"/>\n",
              "</g>\n",
              "<!-- 1776 -->\n",
              "<g id=\"node7\" class=\"node\">\n",
              "<title>1776</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"57.19\" cy=\"-450\" rx=\"30.59\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"57.19\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1(0)</text>\n",
              "</g>\n",
              "<!-- 1776&#45;&gt;1429 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>1776&#45;&gt;1429</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M57.19,-431.7C57.19,-424.41 57.19,-415.73 57.19,-407.54\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"60.7,-407.62 57.19,-397.62 53.7,-407.62 60.7,-407.62\"/>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<__main__.SpacerProof at 0x112858ca0>"
            ]
          },
          "execution_count": 45,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "cfa0 = mk_cfa0(safe=False)\n",
        "vc, invs = cfa_vc_gen(cfa0)\n",
        "res, answer = solve_horn(vc)\n",
        "SpacerProof(answer)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Arrays and Quantifiers\n",
        "\n",
        "So far, we have only used integer valued state variables. Other sorts and theories are supported as well. For example, we can use array-valued state variables to represent a state of computer memory:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 46,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"391pt\" height=\"218pt\"\n",
              " viewBox=\"0.00 0.00 390.60 218.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 214)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-214 386.6,-214 386.6,4 -4,4\"/>\n",
              "<!-- exit -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>exit</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">exit</text>\n",
              "</g>\n",
              "<!-- L0 -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>L0</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
              "</g>\n",
              "<!-- L0&#45;&gt;exit -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>L0&#45;&gt;exit</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-86.8C28.6,-75.58 28.6,-60.67 28.6,-47.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-47.98 28.6,-37.98 25.1,-47.98 32.1,-47.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"109.6\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">j ≥ 0 ∧ j &lt; cnt ∧ MEM[j] ≠ 0</text>\n",
              "</g>\n",
              "<!-- L0&#45;&gt;L0 -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>L0&#45;&gt;L0</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M53.13,-113.03C64.11,-113.79 73.6,-111.12 73.6,-105 73.6,-101.18 69.89,-98.7 64.43,-97.56\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"64.81,-94.08 54.64,-97.05 64.44,-101.07 64.81,-94.08\"/>\n",
              "<text text-anchor=\"middle\" x=\"228.1\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">cnt &lt; N ∧ cnt&#39; = cnt + 1 ∧ MEM&#39; = Store(MEM, cnt, 0)</text>\n",
              "</g>\n",
              "<!-- entry -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>entry</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-192\" rx=\"28.7\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">entry</text>\n",
              "</g>\n",
              "<!-- entry&#45;&gt;L0 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>entry&#45;&gt;L0</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-173.8C28.6,-162.58 28.6,-147.67 28.6,-134.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-134.98 28.6,-124.98 25.1,-134.98 32.1,-134.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"74.6\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">cnt&#39; = 0 ∧ N&#39; &gt; 0</text>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<graphviz.graphs.Digraph at 0x112d7cb80>"
            ]
          },
          "execution_count": 46,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_cfa1():\n",
        "    A = CFA('prog2')\n",
        "    ZZ = z3.IntSort()\n",
        "    Mem, Mem_out = A.add_var(z3.ArraySort(ZZ, ZZ), name='MEM')\n",
        "    N, N_out = A.add_var(ZZ, name='N')\n",
        "    cnt, cnt_out = A.add_var(ZZ, name='cnt')\n",
        "    # local variable\n",
        "    j = A.add_input(ZZ, name='j')\n",
        "\n",
        "    # initially counter is 0, N is positive\n",
        "    init_tr = z3.And(cnt_out == 0, N_out > 0)\n",
        "    A.add_edge('entry', 'L0', init_tr)\n",
        "\n",
        "    # if cnt < N then Mem[cnt++] := 0\n",
        "    loop_tr = z3.And(cnt < N,\n",
        "                     cnt_out == cnt + 1,\n",
        "                     Mem_out == z3.Update(Mem, cnt,  0))\n",
        "    A.add_edge('L0', 'L0', loop_tr)\n",
        "\n",
        "    # if 0 <= j < cnt then assert(Mem[j] == 0)\n",
        "    bad_tr = z3.And(0 <= j, j < cnt, Mem[j] != 0)\n",
        "    A.add_edge('L0', 'exit', bad_tr)\n",
        "\n",
        "    A.set_entry_node('entry')\n",
        "    A.set_exit_node('exit')\n",
        "    return A\n",
        "cfa1 = mk_cfa1()\n",
        "cfa1.to_dot()"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 47,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>unknown</b>"
            ],
            "text/plain": [
              "<b>unknown</b>"
            ]
          },
          "execution_count": 47,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, invs = cfa_vc_gen(cfa1)\n",
        "res, answer = solve_horn(vc)\n",
        "res"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "No solution is found (with out search limit). The underlying reason is that so far we have been restricted to quantifier free solutions. Yet, no QF solution exists for this problem."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 48,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 48,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "res, answer = solve_horn(vc, q3=True)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 49,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "(&forall;sk!0 :\n",
              "  &not;(MEM[sk!0] &le; -1) &or; &not;(sk!0 + -1&middot;cnt &le; -1) &or; &not;(sk!0 &ge; 0)) &and;\n",
              "(&forall;sk!0 :\n",
              "  &not;(sk!0 &ge; 0) &or; &not;(MEM[sk!0] &ge; 1) &or; &not;(sk!0 + -1&middot;cnt &le; -1))"
            ],
            "text/plain": [
              "(&forall;sk!0 :\n",
              "  &not;(MEM[sk!0] &le; -1) &or; &not;(sk!0 + -1&middot;cnt &le; -1) &or; &not;(sk!0 &ge; 0)) &and;\n",
              "(&forall;sk!0 :\n",
              "  &not;(sk!0 &ge; 0) &or; &not;(MEM[sk!0] &ge; 1) &or; &not;(sk!0 + -1&middot;cnt &le; -1))"
            ]
          },
          "execution_count": 49,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(invs['L0'])"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "The solution above is a little hard to read, but it is equivalent to the expected result:\n",
        "\n",
        "$\\forall sk \\cdot 0 \\leq sk < cnt \\implies MEM[sk] \\leq 0$ <br/>\n",
        "$\\forall sk \\cdot 0 \\leq sk < cnt \\implies MEM[sk] \\geq 0$"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Lamport's Bakery Algorithm\n",
        "\n",
        "It is common for multiple processes to share the same resources in concurrent systems. Lamport's Bakery Algorithm facilitates this sharing and seeks to prevent multiple processes from accessing the critical sections of code at the same time.\n",
        "\n",
        "We can encode a transition system for Bakery, where\n",
        "\n",
        "1. *Issue* is the next priority to be issued\n",
        "2. *Serve* is the process currently being served\n",
        "3. *State* is an array of the state for each process, where *0* is idle, *1* is waiting to be served, and *2* is being served\n",
        "4. *Num* is an array of the priority for each process\n",
        "\n",
        "Here we have restricted the implementation to 3 processes: 1, 2, and 3."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 50,
      "metadata": {},
      "outputs": [
        {
          "data": {
            "text/html": [
              "Transition System: Bakery<br/>\tInit: Issue = 0 &and;<br/>Serve = 0 &and;<br/>State[1] = 0 &and;<br/>State[2] = 0 &and;<br/>State[3] = 0 &and;<br/>Num[1] = -1 &and;<br/>Num[2] = -1 &and;<br/>Num[3] = -1<br/>\tBad: State[i] = 2 &and;<br/>State[j] = 2 &and;<br/>i &ne; j &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>j &le; 3 &and;<br/>j &ge; 1<br/>\tTr: State[i] = 0 &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>Serve' = Serve &and;<br/>Issue' = Issue + 1 &and;<br/>State' = Store(State, i, 1) &and;<br/>Num' = Store(Num, i, Issue) &or;<br/>State[i] = 1 &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>Num[i] = Serve &and;<br/>Serve' = Serve &and;<br/>Issue' = Issue &and;<br/>Num' = Num &and;<br/>State' = Store(State, i, 2) &or;<br/>State[i] = 2 &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>Issue' = Issue &and;<br/>Serve' = Serve + 1 &and;<br/>Num' = Store(Num, i, -1) &and;<br/>State' = Store(State, i, 0)"
            ],
            "text/plain": [
              "\"Transition System: Bakery<br/>\\tInit: Issue = 0 &and;<br/>Serve = 0 &and;<br/>State[1] = 0 &and;<br/>State[2] = 0 &and;<br/>State[3] = 0 &and;<br/>Num[1] = -1 &and;<br/>Num[2] = -1 &and;<br/>Num[3] = -1<br/>\\tBad: State[i] = 2 &and;<br/>State[j] = 2 &and;<br/>i &ne; j &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>j &le; 3 &and;<br/>j &ge; 1<br/>\\tTr: State[i] = 0 &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>Serve' = Serve &and;<br/>Issue' = Issue + 1 &and;<br/>State' = Store(State, i, 1) &and;<br/>Num' = Store(Num, i, Issue) &or;<br/>State[i] = 1 &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>Num[i] = Serve &and;<br/>Serve' = Serve &and;<br/>Issue' = Issue &and;<br/>Num' = Num &and;<br/>State' = Store(State, i, 2) &or;<br/>State[i] = 2 &and;<br/>i &le; 3 &and;<br/>i &ge; 1 &and;<br/>Issue' = Issue &and;<br/>Serve' = Serve + 1 &and;<br/>Num' = Store(Num, i, -1) &and;<br/>State' = Store(State, i, 0)\""
            ]
          },
          "execution_count": 50,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_bakery():\n",
        "    T = Ts('Bakery')\n",
        "    ZZ = z3.IntSort()\n",
        "    State, State_out = T.add_var(z3.ArraySort(ZZ,ZZ), name='State')\n",
        "    Num, Num_out = T.add_var(z3.ArraySort(ZZ,ZZ), name='Num')\n",
        "    Issue, Issue_out = T.add_var(ZZ, name='Issue')\n",
        "    Serve, Serve_out = T.add_var(ZZ, name='Serve')\n",
        "    i = T.add_input(ZZ, name='i')\n",
        "    j = T.add_input(ZZ, name='j')\n",
        "    \n",
        "    T.Init = z3.And(Issue == 0, Serve == 0, State[1] == 0, State[2] == 0, State[3] == 0, Num[1] == -1, Num[2] == -1, Num[3] == -1)\n",
        "    T.Tr = z3.Or(\n",
        "                    z3.And(\n",
        "                        State[i] == 0,\n",
        "                        i <= 3,\n",
        "                        i >= 1,\n",
        "                        Serve_out == Serve,\n",
        "                        Issue_out == Issue + 1,\n",
        "                        State_out == z3.Update(State, i,  1),\n",
        "                        Num_out == z3.Update(Num, i, Issue)),\n",
        "                    z3.And(\n",
        "                        State[i] == 1,\n",
        "                        i <= 3, \n",
        "                        i >= 1,\n",
        "                        Num[i] == Serve,\n",
        "                        Serve_out == Serve,\n",
        "                        Issue_out == Issue,\n",
        "                        Num_out == Num,\n",
        "                        State_out == z3.Update(State, i,  2)),\n",
        "                    z3.And(\n",
        "                        State[i] == 2,\n",
        "                        i <= 3,\n",
        "                        i >= 1,\n",
        "                        Issue_out == Issue,\n",
        "                        Serve_out == Serve + 1,\n",
        "                        Num_out == z3.Update(Num, i, -1),\n",
        "                        State_out == z3.Update(State, i,  0))\n",
        "    )\n",
        "    T.Bad = z3.And(State[i] == 2, State[j] == 2, i != j, i <= 3, i >= 1, j <= 3, j >= 1)\n",
        "    return T\n",
        "bakery = mk_bakery()\n",
        "HtmlStr(bakery)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 51,
      "metadata": {},
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;State,<br/> Num,<br/> Issue,<br/> Serve,<br/> State',<br/> Num',<br/> Issue',<br/> Serve',<br/> i,<br/> j :<br/> Issue = 0 &and;<br/> Serve = 0 &and;<br/> State[1] = 0 &and;<br/> State[2] = 0 &and;<br/> State[3] = 0 &and;<br/> Num[1] = -1 &and;<br/> Num[2] = -1 &and;<br/> Num[3] = -1 &rArr;<br/> Inv(State, Num, Issue, Serve) <br/><br/>&forall;State,<br/> Num,<br/> Issue,<br/> Serve,<br/> State',<br/> Num',<br/> Issue',<br/> Serve',<br/> i,<br/> j :<br/> Inv(State, Num, Issue, Serve) &and;<br/> (State[i] = 0 &and;<br/>  i &le; 3 &and;<br/>  i &ge; 1 &and;<br/>  Serve' = Serve &and;<br/>  Issue' = Issue + 1 &and;<br/>  State' = Store(State, i, 1) &and;<br/>  Num' = Store(Num, i, Issue) &or;<br/>  State[i] = 1 &and;<br/>  i &le; 3 &and;<br/>  i &ge; 1 &and;<br/>  Num[i] = Serve &and;<br/>  Serve' = Serve &and;<br/>  Issue' = Issue &and;<br/>  Num' = Num &and;<br/>  State' = Store(State, i, 2) &or;<br/>  State[i] = 2 &and;<br/>  i &le; 3 &and;<br/>  i &ge; 1 &and;<br/>  Issue' = Issue &and;<br/>  Serve' = Serve + 1 &and;<br/>  Num' = Store(Num, i, -1) &and;<br/>  State' = Store(State, i, 0)) &rArr;<br/> Inv(State', Num', Issue', Serve') <br/><br/>&forall;State,<br/> Num,<br/> Issue,<br/> Serve,<br/> State',<br/> Num',<br/> Issue',<br/> Serve',<br/> i,<br/> j :<br/> Inv(State, Num, Issue, Serve) &and;<br/> State[i] = 2 &and;<br/> State[j] = 2 &and;<br/> i &ne; j &and;<br/> i &le; 3 &and;<br/> i &ge; 1 &and;<br/> j &le; 3 &and;<br/> j &ge; 1 &rArr;<br/> False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;State,<br/> Num,<br/> Issue,<br/> Serve,<br/> State',<br/> Num',<br/> Issue',<br/> Serve',<br/> i,<br/> j :<br/> Issue = 0 &and;<br/> Serve = 0 &and;<br/> State[1] = 0 &and;<br/> State[2] = 0 &and;<br/> State[3] = 0 &and;<br/> Num[1] = -1 &and;<br/> Num[2] = -1 &and;<br/> Num[3] = -1 &rArr;<br/> Inv(State, Num, Issue, Serve) <br/><br/>&forall;State,<br/> Num,<br/> Issue,<br/> Serve,<br/> State',<br/> Num',<br/> Issue',<br/> Serve',<br/> i,<br/> j :<br/> Inv(State, Num, Issue, Serve) &and;<br/> (State[i] = 0 &and;<br/>  i &le; 3 &and;<br/>  i &ge; 1 &and;<br/>  Serve' = Serve &and;<br/>  Issue' = Issue + 1 &and;<br/>  State' = Store(State, i, 1) &and;<br/>  Num' = Store(Num, i, Issue) &or;<br/>  State[i] = 1 &and;<br/>  i &le; 3 &and;<br/>  i &ge; 1 &and;<br/>  Num[i] = Serve &and;<br/>  Serve' = Serve &and;<br/>  Issue' = Issue &and;<br/>  Num' = Num &and;<br/>  State' = Store(State, i, 2) &or;<br/>  State[i] = 2 &and;<br/>  i &le; 3 &and;<br/>  i &ge; 1 &and;<br/>  Issue' = Issue &and;<br/>  Serve' = Serve + 1 &and;<br/>  Num' = Store(Num, i, -1) &and;<br/>  State' = Store(State, i, 0)) &rArr;<br/> Inv(State', Num', Issue', Serve') <br/><br/>&forall;State,<br/> Num,<br/> Issue,<br/> Serve,<br/> State',<br/> Num',<br/> Issue',<br/> Serve',<br/> i,<br/> j :<br/> Inv(State, Num, Issue, Serve) &and;<br/> State[i] = 2 &and;<br/> State[j] = 2 &and;<br/> i &ne; j &and;<br/> i &le; 3 &and;<br/> i &ge; 1 &and;<br/> j &le; 3 &and;<br/> j &ge; 1 &rArr;<br/> False <br/><br/>\""
            ]
          },
          "execution_count": 51,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, inv = vc_gen(bakery)\n",
        "chc_to_str(vc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 52,
      "metadata": {},
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "'<b>sat</b>'"
            ]
          },
          "execution_count": 52,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "res, answer = solve_horn(vc, q3=False, max_unfold=100)\n",
        "HtmlStr(res)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 53,
      "metadata": {},
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &le; -2) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -2)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &le; -2) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[2] &ge; 2) &or; &not;(State[3] &ge; 2)"
            ],
            "text/plain": [
              "&not;(State[2] &ge; 2) &or; &not;(State[3] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Issue &ge; 0) &or; &not;(State[3] &ge; 2)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Issue &ge; 0) &or; &not;(State[3] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 2) &or; &not;(State[2] &ge; 2)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 2) &or; &not;(State[2] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 2) &or; &not;(State[3] &ge; 2)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 2) &or; &not;(State[3] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[2] &ge; 2) &or; &not;(Serve + -1&middot;Issue &ge; 0)"
            ],
            "text/plain": [
              "&not;(State[2] &ge; 2) &or; &not;(Serve + -1&middot;Issue &ge; 0)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 2) &or; &not;(Serve + -1&middot;Issue &ge; 0)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 2) &or; &not;(Serve + -1&middot;Issue &ge; 0)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[2] &ge; 1) &or; &not;(State[3] &ge; 2) &or; &not;(Num[2] = Serve)"
            ],
            "text/plain": [
              "&not;(State[2] &ge; 1) &or; &not;(State[3] &ge; 2) &or; &not;(Num[2] = Serve)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[3] &ge; 1) &or; &not;(State[1] &ge; 2) &or; &not;(Num[3] = Serve)"
            ],
            "text/plain": [
              "&not;(State[3] &ge; 1) &or; &not;(State[1] &ge; 2) &or; &not;(Num[3] = Serve)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; 0) &or;\n",
              "&not;(Serve + -1&middot;Num[3] &le; 0)"
            ],
            "text/plain": [
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; 0) &or;\n",
              "&not;(Serve + -1&middot;Num[3] &le; 0)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; 0) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; 0)"
            ],
            "text/plain": [
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; 0) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; 0)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Num[2] = Serve) &or;\n",
              "&not;(Num[3] = Serve)"
            ],
            "text/plain": [
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Num[2] = Serve) &or;\n",
              "&not;(Num[3] = Serve)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[3] &ge; 1) &or; &not;(State[2] &ge; 2) &or; &not;(Num[3] = Serve)"
            ],
            "text/plain": [
              "&not;(State[3] &ge; 1) &or; &not;(State[2] &ge; 2) &or; &not;(Num[3] = Serve)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[1] &le; 0) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; 0)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[1] &le; 0) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; 0)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Num[1] = Serve) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Num[2] = Serve)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Num[1] = Serve) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Num[2] = Serve)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[2] &ge; 1) &or; &not;(State[1] &ge; 2) &or; &not;(Num[2] = Serve)"
            ],
            "text/plain": [
              "&not;(State[2] &ge; 1) &or; &not;(State[1] &ge; 2) &or; &not;(Num[2] = Serve)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] &le; -1)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] &le; -1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(State[1] &ge; 2)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(State[1] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Num[1] = Serve) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Num[3] = Serve)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Num[1] = Serve) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Num[3] = Serve)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &ge; 0) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(State[3] &ge; 1)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &ge; 0) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(State[3] &ge; 1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 2)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Num[1] = Serve) &or; &not;(State[1] &ge; 1) &or; &not;(State[2] &ge; 2)"
            ],
            "text/plain": [
              "&not;(Num[1] = Serve) &or; &not;(State[1] &ge; 1) &or; &not;(State[2] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; -1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; -1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; -1) &or;\n",
              "&not;(State[2] &ge; 1)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; -1) &or;\n",
              "&not;(State[2] &ge; 1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] &le; -1)"
            ],
            "text/plain": [
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] &le; -1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &le; -1)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &le; -1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &le; -1)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Issue &ge; -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] &le; -1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &ge; 0) &or;\n",
              "&not;(State[3] &ge; 1)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &ge; 0) &or;\n",
              "&not;(State[3] &ge; 1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 2)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[3] = -1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[3] &le; -2) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -2)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[3] &le; -2) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 1) &or; &not;(State[3] &ge; 2) &or; &not;(Serve + -1&middot;Num[1] = 0)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 1) &or; &not;(State[3] &ge; 2) &or; &not;(Serve + -1&middot;Num[1] = 0)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(Serve + -1&middot;Num[3] &ge; 0) &or;\n",
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1)"
            ],
            "text/plain": [
              "&not;(Serve + -1&middot;Num[3] &ge; 0) &or;\n",
              "&not;(Serve + -1&middot;Num[2] = -1) &or;\n",
              "&not;(Serve + -1&middot;Num[1] = -1) &or;\n",
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; -2) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -2)"
            ],
            "text/plain": [
              "&not;(State[1] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Num[2] &le; -2) &or;\n",
              "&not;(State[2] &ge; 1) &or;\n",
              "&not;(State[3] &ge; 1) &or;\n",
              "&not;(Serve + -1&middot;Issue &ge; -2)"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        }
      ],
      "source": [
        "horn_inv = answer.eval(inv)\n",
        "for f in horn_inv.children():\n",
        "    display(f)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "We can condense and display this in SMT-LIB format."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 54,
      "metadata": {},
      "outputs": [
        {
          "name": "stdout",
          "output_type": "stream",
          "text": [
            "(set-logic HORN)\n",
            "(declare-fun Inv ((Array Int Int) (Array Int Int) Int Int) Bool)\n",
            "(assert (forall ((State (Array Int Int))\n",
            "         (Num (Array Int Int))\n",
            "         (Issue Int)\n",
            "         (Serve Int)\n",
            "         (|State'| (Array Int Int))\n",
            "         (|Num'| (Array Int Int))\n",
            "         (|Issue'| Int)\n",
            "         (|Serve'| Int)\n",
            "         (i Int)\n",
            "         (j Int))\n",
            "  (=> (and (= Issue 0)\n",
            "           (= Serve 0)\n",
            "           (= (select State 1) 0)\n",
            "           (= (select State 2) 0)\n",
            "           (= (select State 3) 0)\n",
            "           (= (select Num 1) (- 1))\n",
            "           (= (select Num 2) (- 1))\n",
            "           (= (select Num 3) (- 1)))\n",
            "      (Inv State Num Issue Serve))))\n",
            "(assert (forall ((State (Array Int Int))\n",
            "         (Num (Array Int Int))\n",
            "         (Issue Int)\n",
            "         (Serve Int)\n",
            "         (|State'| (Array Int Int))\n",
            "         (|Num'| (Array Int Int))\n",
            "         (|Issue'| Int)\n",
            "         (|Serve'| Int)\n",
            "         (i Int)\n",
            "         (j Int))\n",
            "  (let ((a!1 (or (and (= (select State i) 0)\n",
            "                      (<= i 3)\n",
            "                      (>= i 1)\n",
            "                      (= |Serve'| Serve)\n",
            "                      (= |Issue'| (+ Issue 1))\n",
            "                      (= |State'| (store State i 1))\n",
            "                      (= |Num'| (store Num i Issue)))\n",
            "                 (and (= (select State i) 1)\n",
            "                      (<= i 3)\n",
            "                      (>= i 1)\n",
            "                      (= (select Num i) Serve)\n",
            "                      (= |Serve'| Serve)\n",
            "                      (= |Issue'| Issue)\n",
            "                      (= |Num'| Num)\n",
            "                      (= |State'| (store State i 2)))\n",
            "                 (and (= (select State i) 2)\n",
            "                      (<= i 3)\n",
            "                      (>= i 1)\n",
            "                      (= |Issue'| Issue)\n",
            "                      (= |Serve'| (+ Serve 1))\n",
            "                      (= |Num'| (store Num i (- 1)))\n",
            "                      (= |State'| (store State i 0))))))\n",
            "    (=> (and (Inv State Num Issue Serve) a!1)\n",
            "        (Inv |State'| |Num'| |Issue'| |Serve'|)))))\n",
            "(assert (forall ((State (Array Int Int))\n",
            "         (Num (Array Int Int))\n",
            "         (Issue Int)\n",
            "         (Serve Int)\n",
            "         (|State'| (Array Int Int))\n",
            "         (|Num'| (Array Int Int))\n",
            "         (|Issue'| Int)\n",
            "         (|Serve'| Int)\n",
            "         (i Int)\n",
            "         (j Int))\n",
            "  (=> (and (Inv State Num Issue Serve)\n",
            "           (= (select State i) 2)\n",
            "           (= (select State j) 2)\n",
            "           (distinct i j)\n",
            "           (<= i 3)\n",
            "           (>= i 1)\n",
            "           (<= j 3)\n",
            "           (>= j 1))\n",
            "      false)))\n",
            "\n",
            "(check-sat)\n"
          ]
        }
      ],
      "source": [
        "s = z3.SolverFor('HORN')\n",
        "s.add(vc)\n",
        "print('(set-logic HORN)')\n",
        "print(s.sexpr())\n",
        "print('(check-sat)')"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Back to basics\n",
        "\n",
        "CHC Satisfiability over Linear Integer Arithmetic is undecidable. Thus, there are always \"simple looking\" instances that are difficult to solve with any current algorithm. In this part of the tutorial, we will look at how different encoding techniques are used to guide the search."
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Predicate Abstraction\n",
        "\n",
        "(Implicit) Predicate Abstraction is an abstraction (or search guidance) technique that restricts the search to a solution that is expressed by a Boolean combination of a user-defined set of predicates.\n",
        "\n",
        "Given a set of predicates $Pred$ (i.e., formulas in the underlying theory), a predicate abstraction of an inductive invariant for a transition system $P$ is a formula $InvPred$ such that\n",
        "  1. $InvPred$ is a Boolean combination of predicates from $Pred$\n",
        "  2. $InvPred$ is an inductive invariant of $P$\n",
        "  \n",
        "Note that deciding whether there exists an $InvPred$ is **decidable**! There are finitely many distinct Boolean combinations of a given finite set of predicates.\n",
        "\n",
        "[CGMT14] A. Cimatti, A. Griggio, S. Mover, S. Tonetta:\n",
        "_IC3 Modulo Theories via Implicit Predicate Abstraction_. TACAS 2014: 46-61\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 55,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "Transition System: Ts1<br/>\tInit: a = 0 &and; c &gt; 0 &and; c &lt; 5 &and; b = 3&middot;c<br/>\tBad: &not;(b &ge; 3 &and; b &le; 212)<br/>\tTr: a &lt; 200 &and; a' = a + 1 &and; b' = b + 1"
            ],
            "text/plain": [
              "\"Transition System: Ts1<br/>\\tInit: a = 0 &and; c &gt; 0 &and; c &lt; 5 &and; b = 3&middot;c<br/>\\tBad: &not;(b &ge; 3 &and; b &le; 212)<br/>\\tTr: a &lt; 200 &and; a' = a + 1 &and; b' = b + 1\""
            ]
          },
          "execution_count": 55,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_ts1(safe=True):\n",
        "    T = Ts('Ts1')\n",
        "    a, a_out = T.add_var(z3.IntSort(), name='a')\n",
        "    b, b_out = T.add_var(z3.IntSort(), name='b')\n",
        "    c, c_out = T.add_var(z3.IntSort(), name='c')\n",
        "    T.Init = z3.And(a == 0, 0 < c, c < 5, b == 3 * c)\n",
        "    T.Tr = z3.And(a < 200, a_out == a + 1, b_out == b + 1)\n",
        "    if safe:\n",
        "        T.Bad = z3.Not(z3.And(3 <= b, b <= 200 + 12))\n",
        "    else:\n",
        "        T.Bad = z3.Not(z3.And(3 <= b, b <= 200 + 2))\n",
        "    return T\n",
        "ts1 = mk_ts1(safe=True)\n",
        "HtmlStr(ts1)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 52,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>unknown</b>"
            ],
            "text/plain": [
              "<b>unknown</b>"
            ]
          },
          "execution_count": 52,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, inv = vc_gen(ts1)\n",
        "res, answer = solve_horn(vc)\n",
        "res"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "We define `vc_gen_pa` that generates verification condition for predicate abstraction given a set of predicates. The basic structure is the same as `vc_gen`, except, the uninterpreted predicate `InvPredAbs` only takes Boolean arguments. The predicates are evaluated in the pre-state and post-state of the transition relation, and are then passed to `InvPredAbs`."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 56,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def vc_gen_pa(T, preds):\n",
        "    '''Verification Condition for Predicate Abstraction'''\n",
        "\n",
        "    post_preds = [T.to_post(p) for p in preds]\n",
        "\n",
        "    # create predicate Inv\n",
        "    sig = [z3.BoolSort()] * (len(preds) + 1)\n",
        "    Inv = z3.Function('InvPredAbs', *sig)\n",
        "\n",
        "    all_vars = T.all()\n",
        "\n",
        "    InvPre = Inv(*preds)\n",
        "    InvPost = Inv(*post_preds)\n",
        "    vc_init = z3.ForAll(all_vars, z3.Implies(T.Init, InvPre))\n",
        "    vc_ind = z3.ForAll(all_vars, z3.Implies(z3.And(InvPre, T.Tr), InvPost))\n",
        "    vc_bad = z3.ForAll(all_vars,\n",
        "                       z3.Implies(z3.And(InvPre, T.Bad), z3.BoolVal(False)))\n",
        "\n",
        "    return [vc_init, vc_ind, vc_bad], InvPre"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 57,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "a = ts1.get_pre_var('a')\n",
        "b = ts1.get_pre_var('b')\n",
        "vc, inv = vc_gen_pa(ts1, [b - a >= 13, a >= 0, b <= 2, b >= 213])"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 58,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;a, b, c, a', b', c' :<br/> a = 0 &and; c &gt; 0 &and; c &lt; 5 &and; b = 3&middot;c &rArr;<br/> InvPredAbs(b - a &ge; 13, a &ge; 0, b &le; 2, b &ge; 213) <br/><br/>&forall;a, b, c, a', b', c' :<br/> InvPredAbs(b - a &ge; 13, a &ge; 0, b &le; 2, b &ge; 213) &and;<br/> a &lt; 200 &and;<br/> a' = a + 1 &and;<br/> b' = b + 1 &rArr;<br/> InvPredAbs(b' - a' &ge; 13, a' &ge; 0, b' &le; 2, b' &ge; 213) <br/><br/>&forall;a, b, c, a', b', c' :<br/> InvPredAbs(b - a &ge; 13, a &ge; 0, b &le; 2, b &ge; 213) &and;<br/> &not;(b &ge; 3 &and; b &le; 212) &rArr;<br/> False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;a, b, c, a', b', c' :<br/> a = 0 &and; c &gt; 0 &and; c &lt; 5 &and; b = 3&middot;c &rArr;<br/> InvPredAbs(b - a &ge; 13, a &ge; 0, b &le; 2, b &ge; 213) <br/><br/>&forall;a, b, c, a', b', c' :<br/> InvPredAbs(b - a &ge; 13, a &ge; 0, b &le; 2, b &ge; 213) &and;<br/> a &lt; 200 &and;<br/> a' = a + 1 &and;<br/> b' = b + 1 &rArr;<br/> InvPredAbs(b' - a' &ge; 13, a' &ge; 0, b' &le; 2, b' &ge; 213) <br/><br/>&forall;a, b, c, a', b', c' :<br/> InvPredAbs(b - a &ge; 13, a &ge; 0, b &le; 2, b &ge; 213) &and;<br/> &not;(b &ge; 3 &and; b &le; 212) &rArr;<br/> False <br/><br/>\""
            ]
          },
          "execution_count": 58,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "chc_to_str(vc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 59,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 59,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "res, answer = solve_horn(vc)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 60,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(b &ge; 213) &and; &not;(b &le; 2) &and; a &ge; 0 &and; &not;(b + -1&middot;a &ge; 13)"
            ],
            "text/plain": [
              "&not;(b &ge; 213) &and; &not;(b &le; 2) &and; a &ge; 0 &and; &not;(b + -1&middot;a &ge; 13)"
            ]
          },
          "execution_count": 60,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(inv)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Term Abstraction\n",
        "\n",
        "Predicate abstraction requires the user to specify the exact predicates to be used in the solution.\n",
        "We can relax this by requiring the user to only specify the terms that are allowed in the solution.\n",
        "\n",
        "Predicate Abstraction is a special case of Term Abstraction where user provided terms are Boolean.\n",
        "\n",
        "[LRS16] J. Leroux, P. Rümmer, P. Subotic:\n",
        "_Guiding Craig interpolation with domain-specific abstractions_. Acta Inf. 53(4): 387-424 (2016)\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 61,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def vc_gen_ta(T, terms):\n",
        "    '''Verification Condition for Term Abstraction'''\n",
        "\n",
        "    post_terms = [T.to_post(p) for p in terms]\n",
        "\n",
        "    # create term Inv\n",
        "    sig = [t.sort() for t in terms] + [z3.BoolSort()]\n",
        "    Inv = z3.Function('InvTermAbs', *sig)\n",
        "    all_vars = T.all()\n",
        "\n",
        "    InvPre = Inv(*terms)\n",
        "    InvPost = Inv(*post_terms)\n",
        "\n",
        "    vc_init = z3.ForAll(all_vars, z3.Implies(T.Init, InvPre))\n",
        "    vc_ind = z3.ForAll(all_vars, z3.Implies(z3.And(InvPre, T.Tr), InvPost))\n",
        "    vc_bad = z3.ForAll(all_vars,\n",
        "                       z3.Implies(z3.And(InvPre, T.Bad), z3.BoolVal(False)))\n",
        "\n",
        "    return [vc_init, vc_ind, vc_bad], InvPre"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 62,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 62,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "a, b, c = ts1.get_pre_vars('a b c')\n",
        "vc, inv = vc_gen_ta(ts1, [b-a, b])\n",
        "res, answer = solve_horn(vc, max_unfold=400)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 63,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(a &le; -1) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &ge; 213) &and; &not;(b &le; 2)"
            ],
            "text/plain": [
              "&not;(a &le; -1) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &ge; 213) &and; &not;(b &le; 2)"
            ]
          },
          "execution_count": 63,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(inv)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Invariant Partitioning\n",
        "\n",
        "Another way to guide the search is to look for modular invariants. The state variables are partitioned into groups $G_1$, $G_2$, ..., The invariant is partitioned into a conjunction of formulas $Inv_1$, $Inv_2$, ... such that $Inv_i$ is a formula over state variables in group $G_i$. Note that the groups $G_i$ do not have to be disjoint."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 64,
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def vc_gen_part(T, partitions):\n",
        "    '''Partitioned abstraction'''\n",
        "\n",
        "    def _mk_inv_pred(name, vars):\n",
        "        sig = [v.sort() for v in vars] + [z3.BoolSort()]\n",
        "        inv = z3.Function(name, *sig)\n",
        "        return inv(vars)\n",
        "\n",
        "    part_inv = [_mk_inv_pred('PartInv_' + str(pname), vars)\n",
        "                for pname, vars in partitions.items()]\n",
        "\n",
        "\n",
        "    vc = list()\n",
        "    all_vars = T.all()\n",
        "    for inv in part_inv:\n",
        "        vc.append(z3.ForAll(all_vars, z3.Implies(T.Init, inv)))\n",
        "\n",
        "    preInvs = z3.And(part_inv)\n",
        "    for inv in part_inv:\n",
        "        postInv = T.to_post(inv)\n",
        "        vc.append(z3.ForAll(all_vars,\n",
        "                            z3.Implies(z3.And(preInvs, T.Tr),\n",
        "                                       postInv)))\n",
        "    vc.append(z3.ForAll(all_vars,\n",
        "                        z3.Implies(z3.And(preInvs, T.Bad),\n",
        "                                   z3.BoolVal(False))))\n",
        "    return vc, preInvs"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 65,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "Transition System: Ts2<br/>\tInit: a = 0 &and; b = 0 &and; c = 0 &and; d = 0<br/>\tBad: &not;(d &ge; 0)<br/>\tTr: a' = a + 1 &and;<br/>b' = b + a + 1 &and;<br/>c' = c + b + a + 1 &and;<br/>d' = d + c + b + a + 1"
            ],
            "text/plain": [
              "\"Transition System: Ts2<br/>\\tInit: a = 0 &and; b = 0 &and; c = 0 &and; d = 0<br/>\\tBad: &not;(d &ge; 0)<br/>\\tTr: a' = a + 1 &and;<br/>b' = b + a + 1 &and;<br/>c' = c + b + a + 1 &and;<br/>d' = d + c + b + a + 1\""
            ]
          },
          "execution_count": 65,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_ts2():\n",
        "    T = Ts('Ts2')\n",
        "    a, a_out = T.add_var(z3.IntSort(), name='a')\n",
        "    b, b_out = T.add_var(z3.IntSort(), name='b')\n",
        "    c, c_out = T.add_var(z3.IntSort(), name='c')\n",
        "    d, d_out = T.add_var(z3.IntSort(), name='d')\n",
        "    T.Init = z3.And(a == 0, b == 0, c == 0, d == 0)\n",
        "    T.Tr = z3.And(a_out == a + 1,\n",
        "                  b_out == b + a + 1,\n",
        "                  c_out == c + b + a + 1,\n",
        "                  d_out == d + c + b + a + 1)\n",
        "    T.Bad = z3.Not(d >= 0)\n",
        "    return T\n",
        "ts2 = mk_ts2()\n",
        "HtmlStr(ts2)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 66,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>unknown</b>"
            ],
            "text/plain": [
              "'<b>unknown</b>'"
            ]
          },
          "execution_count": 66,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, inv = vc_gen(ts2)\n",
        "res, answer = solve_horn(vc)\n",
        "HtmlStr(res)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 67,
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 67,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_bnd(T, N):\n",
        "    \"\"\"\n",
        "    Bound a given transition system by to at most N iterations\n",
        "\n",
        "    Transforms a given transition system T into a transition system T_N\n",
        "    that executes for at most N steps\n",
        "    \"\"\"\n",
        "\n",
        "    import copy\n",
        "    TN = copy.deepcopy(T)\n",
        "    TN.name += '_bnd_' + str(N)\n",
        "    bnd, bnd_out = TN.add_var(z3.IntSort(), \"bnd\")\n",
        "    TN.Init = z3.simplify(z3.And(T.Init, bnd == N))\n",
        "    TN.Tr = z3.simplify(z3.And(T.Tr, bnd_out < bnd, bnd_out >= 0))\n",
        "    TN.Bad = T.Bad\n",
        "\n",
        "    return TN\n",
        "ts2_bnd = mk_bnd(ts2, N=4)\n",
        "vc, inv = vc_gen(ts2_bnd)\n",
        "res, answer = solve_horn(vc)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 68,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(bnd &ge; 5) &and;<br/>(&not;(bnd &ge; 2) &or; &not;(4&middot;a + 3&middot;b + d + 2&middot;c &le; -3)) &and;<br/>&not;(d &le; -1) &and;<br/>(&not;(bnd &ge; 1) &or; &not;(a + b + d + c &le; -1)) &and;<br/>(&not;(bnd &ge; 3) &or; &not;(10&middot;a + 6&middot;b + d + 3&middot;c &le; -11)) &and;<br/>(&not;(20&middot;a + 10&middot;b + d + 4&middot;c &le; -31) &or; &not;(bnd &ge; 4))"
            ],
            "text/plain": [
              "'&not;(bnd &ge; 5) &and;<br/>(&not;(bnd &ge; 2) &or; &not;(4&middot;a + 3&middot;b + d + 2&middot;c &le; -3)) &and;<br/>&not;(d &le; -1) &and;<br/>(&not;(bnd &ge; 1) &or; &not;(a + b + d + c &le; -1)) &and;<br/>(&not;(bnd &ge; 3) &or; &not;(10&middot;a + 6&middot;b + d + 3&middot;c &le; -11)) &and;<br/>(&not;(20&middot;a + 10&middot;b + d + 4&middot;c &le; -31) &or; &not;(bnd &ge; 4))'"
            ]
          },
          "execution_count": 68,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "HtmlStr(answer.eval(inv))"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "The solver is stuck trying to find a monolithic solution that converges to an invariant in non-linear arithmetic!\n",
        "We can guide it by partitioning the invariants to individual state variables:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 69,
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 69,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def vc_gen_part(T, partitions):\n",
        "    '''Partitioned abstraction'''\n",
        "\n",
        "    def _mk_inv_pred(name, vars):\n",
        "        sig = [v.sort() for v in vars] + [z3.BoolSort()]\n",
        "        inv = z3.Function(name, *sig)\n",
        "        return inv(vars)\n",
        "\n",
        "    part_inv = [_mk_inv_pred('PartInv_' + str(pname), vars)\n",
        "                for pname, vars in partitions.items()]\n",
        "\n",
        "\n",
        "    vc = list()\n",
        "    all_vars = T.all()\n",
        "    for inv in part_inv:\n",
        "        vc.append(z3.ForAll(all_vars, z3.Implies(T.Init, inv)))\n",
        "\n",
        "    preInvs = z3.And(part_inv)\n",
        "    for inv in part_inv:\n",
        "        postInv = T.to_post(inv)\n",
        "        vc.append(z3.ForAll(all_vars,\n",
        "                            z3.Implies(z3.And(preInvs, T.Tr),\n",
        "                                       postInv)))\n",
        "    vc.append(z3.ForAll(all_vars,\n",
        "                        z3.Implies(z3.And(preInvs, T.Bad),\n",
        "                                   z3.BoolVal(False))))\n",
        "    return vc, preInvs\n",
        "\n",
        "a, b, c, d = ts2.get_pre_vars('a b c d')\n",
        "vc, inv = vc_gen_part(ts2, { \"a\":[a], \"b\":[b], \"c\":[c], \"d\":[d] })\n",
        "res, answer = solve_horn(vc)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 70,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "PartInv_a(a) &and; PartInv_b(b) &and; PartInv_c(c) &and; PartInv_d(d)"
            ],
            "text/plain": [
              "PartInv_a(a) &and; PartInv_b(b) &and; PartInv_c(c) &and; PartInv_d(d)"
            ]
          },
          "execution_count": 70,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "inv"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 71,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(a &le; -1) &and; &not;(b &le; -1) &and; &not;(c &le; -1) &and; &not;(d &le; -1)"
            ],
            "text/plain": [
              "&not;(a &le; -1) &and; &not;(b &le; -1) &and; &not;(c &le; -1) &and; &not;(d &le; -1)"
            ]
          },
          "execution_count": 71,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(inv)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 72,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(c + a &le; -2) &and; &not;(a &le; -1) &and; &not;(b &le; -1) &and; &not;(d &le; -1)"
            ],
            "text/plain": [
              "&not;(c + a &le; -2) &and; &not;(a &le; -1) &and; &not;(b &le; -1) &and; &not;(d &le; -1)"
            ]
          },
          "execution_count": 72,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, inv = vc_gen_part(ts2, { \"ac\":[a, c], \"bc\":[b, c], \"d\":[d] })\n",
        "res, answer = solve_horn(vc)\n",
        "answer.eval(inv)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 73,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;a, b, c, d, a', b', c', d' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &rArr; PartInv_ac(a, c) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &rArr; PartInv_bc(b, c) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &rArr; PartInv_d(d) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> a' = a + 1 &and;<br/> b' = b + a + 1 &and;<br/> c' = c + b + a + 1 &and;<br/> d' = d + c + b + a + 1 &rArr;<br/> PartInv_ac(a', c') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> a' = a + 1 &and;<br/> b' = b + a + 1 &and;<br/> c' = c + b + a + 1 &and;<br/> d' = d + c + b + a + 1 &rArr;<br/> PartInv_bc(b', c') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> a' = a + 1 &and;<br/> b' = b + a + 1 &and;<br/> c' = c + b + a + 1 &and;<br/> d' = d + c + b + a + 1 &rArr;<br/> PartInv_d(d') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> &not;(d &ge; 0) &rArr;<br/> False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;a, b, c, d, a', b', c', d' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &rArr; PartInv_ac(a, c) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &rArr; PartInv_bc(b, c) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &rArr; PartInv_d(d) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> a' = a + 1 &and;<br/> b' = b + a + 1 &and;<br/> c' = c + b + a + 1 &and;<br/> d' = d + c + b + a + 1 &rArr;<br/> PartInv_ac(a', c') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> a' = a + 1 &and;<br/> b' = b + a + 1 &and;<br/> c' = c + b + a + 1 &and;<br/> d' = d + c + b + a + 1 &rArr;<br/> PartInv_bc(b', c') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> a' = a + 1 &and;<br/> b' = b + a + 1 &and;<br/> c' = c + b + a + 1 &and;<br/> d' = d + c + b + a + 1 &rArr;<br/> PartInv_d(d') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> PartInv_ac(a, c) &and;<br/> PartInv_bc(b, c) &and;<br/> PartInv_d(d) &and;<br/> &not;(d &ge; 0) &rArr;<br/> False <br/><br/>\""
            ]
          },
          "execution_count": 73,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "chc_to_str(vc)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Combining Data Flow and Control Flow\n",
        "\n",
        "Our examples so far modeled the control flow of the transition system. Alternatively,\n",
        "we can model the data flow, and even combine the two together.\n",
        "\n",
        "To model data flow, we extend our CFA with a block of _packed_ registers $p$ and two instructions:\n",
        "\n",
        "  1. $pack (p := v)$ that stores the values of registers $v$ into the pack\n",
        "  2. $unpack (v := p)$ that unpackes the values stored in $p$ into state registers $v$\n",
        "  \n",
        "Using $pack$ and $unpack$ we can model data flow (or, even weak memory updates)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 74,
      "metadata": {
        "code_folding": [
          0,
          43,
          51
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "class DCFA(CFA):\n",
        "    def __init__(self, name):\n",
        "        super().__init__(name)\n",
        "        self._named_pack_vars = dict()\n",
        "        self._pack_vars = list()\n",
        "        self._pack_var_names = list()\n",
        "\n",
        "    def all(self):\n",
        "        return super().all() + self.pack_vars()\n",
        "    def packed_sig(self):\n",
        "        return [v.sort() for v in self._pack_vars]\n",
        "\n",
        "    def add_pack_var(self, sort, name = None):\n",
        "        vname = self._new_pack_var_name(name=name)\n",
        "        v = z3.Const(vname, sort)\n",
        "        self._pack_vars.append(v)\n",
        "        self._pack_var_names.append(name)\n",
        "        if name is not None:\n",
        "            self._named_pack_vars[name] = v\n",
        "        return v\n",
        "\n",
        "    def get_pack_var(self, idx):\n",
        "        if isinstance(idx, int):\n",
        "            return self._pack_vars[idx]\n",
        "        elif idx in self._named_pack_vars:\n",
        "            return self._named_pack_vars[idx]\n",
        "        return None\n",
        "\n",
        "    def pack_vars(self):\n",
        "        return self._pack_vars\n",
        "\n",
        "    def get_pack_var_name(self, idx):\n",
        "        if idx < len(self._pack_var_names):\n",
        "            return self._pack_var_names[idx]\n",
        "        return None\n",
        "\n",
        "    def _new_pack_var_name(self, name):\n",
        "        if name is not None:\n",
        "            return str(name)\n",
        "        else:\n",
        "            idx = len(self._pack_vars)\n",
        "            return 'p_' + str(idx)\n",
        "        \n",
        "class PackTr(object):\n",
        "    \"assignment of state/input expressions into packed variables\"\n",
        "    def __init__(self, *sub):\n",
        "        self.sub = sub\n",
        "    def __repr__(self):\n",
        "        body = ' '.join([str(lhs) + ':=' + str(rhs) for (lhs, rhs) in self.sub])\n",
        "        return 'pack(' + body + ')'\n",
        "\n",
        "class UnpackTr(object):\n",
        "    \"assignment from packed variables to state/input variables\"\n",
        "    def __init__(self, *sub):\n",
        "        self.sub = sub\n",
        "    def __repr__(self):\n",
        "        body = ' '.join([str(lhs) + ':=' + str(rhs) for (lhs, rhs) in self.sub])\n",
        "        return 'unpack(' + body + ')'"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 75,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def mk_dcfa0():\n",
        "    A = DCFA('prog3')\n",
        "    ZZ = z3.IntSort()\n",
        "    x, x_out = A.add_var(ZZ, 'x')\n",
        "    y, y_out = A.add_var(ZZ, 'y')\n",
        "    p = A.add_pack_var(ZZ, 'p')\n",
        "\n",
        "    A.add_edge('entry', 'L0', x_out == 10)\n",
        "    A.add_edge('L0', 'L1', z3.And( y_out == 0, x_out == x ))\n",
        "    A.add_edge('L1', 'L1', z3.And( y < 2019, y_out == y + 1, x_out == x ) )\n",
        "    A.add_edge('L1', 'L2', z3.And(y >= 2019, x_out == x))\n",
        "    A.add_edge('L2', 'exit', x > 10)\n",
        "    A.set_entry_node('entry')\n",
        "    A.set_exit_node('exit')\n",
        "    return A"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "source": [
        "In `dcfa0`, the loop at `L1` hides the dataflow of variable `x` from `L0` to `L2`"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 76,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"249pt\" height=\"392pt\"\n",
              " viewBox=\"0.00 0.00 248.60 392.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 388)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-388 244.6,-388 244.6,4 -4,4\"/>\n",
              "<!-- entry -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>entry</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-366\" rx=\"28.7\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">entry</text>\n",
              "</g>\n",
              "<!-- L0 -->\n",
              "<g id=\"node5\" class=\"node\">\n",
              "<title>L0</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-279\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
              "</g>\n",
              "<!-- entry&#45;&gt;L0 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>entry&#45;&gt;L0</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-347.8C28.6,-336.58 28.6,-321.67 28.6,-308.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-308.98 28.6,-298.98 25.1,-308.98 32.1,-308.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"48.1\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">x&#39; = 10</text>\n",
              "</g>\n",
              "<!-- L2 -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>L2</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">L2</text>\n",
              "</g>\n",
              "<!-- exit -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>exit</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">exit</text>\n",
              "</g>\n",
              "<!-- L2&#45;&gt;exit -->\n",
              "<g id=\"edge5\" class=\"edge\">\n",
              "<title>L2&#45;&gt;exit</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-86.8C28.6,-75.58 28.6,-60.67 28.6,-47.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-47.98 28.6,-37.98 25.1,-47.98 32.1,-47.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"47.1\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">x &gt; 10</text>\n",
              "</g>\n",
              "<!-- L1 -->\n",
              "<g id=\"node4\" class=\"node\">\n",
              "<title>L1</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-192\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L2 -->\n",
              "<g id=\"edge4\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L2</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-173.8C28.6,-162.58 28.6,-147.67 28.6,-134.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-134.98 28.6,-124.98 25.1,-134.98 32.1,-134.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"77.1\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">y ≥ 2019 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L1 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M53.13,-200.03C64.11,-200.79 73.6,-198.12 73.6,-192 73.6,-188.18 69.89,-185.7 64.43,-184.56\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"64.81,-181.08 54.64,-184.05 64.44,-188.07 64.81,-181.08\"/>\n",
              "<text text-anchor=\"middle\" x=\"157.1\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">y &lt; 2019 ∧ y&#39; = y + 1 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "<!-- L0&#45;&gt;L1 -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>L0&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-260.8C28.6,-249.58 28.6,-234.67 28.6,-221.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-221.98 28.6,-211.98 25.1,-221.98 32.1,-221.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"68.1\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">y&#39; = 0 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<graphviz.graphs.Digraph at 0x112d77e20>"
            ]
          },
          "execution_count": 76,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "dcfa0 = mk_dcfa0()\n",
        "dcfa0.to_dot()"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 77,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"249pt\" height=\"566pt\"\n",
              " viewBox=\"0.00 0.00 248.60 566.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 562)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-562 244.6,-562 244.6,4 -4,4\"/>\n",
              "<!-- L0 -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>L0</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-453\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
              "</g>\n",
              "<!-- P -->\n",
              "<g id=\"node7\" class=\"node\">\n",
              "<title>P</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-366\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">P</text>\n",
              "</g>\n",
              "<!-- L0&#45;&gt;P -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>L0&#45;&gt;P</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-434.8C28.6,-423.58 28.6,-408.67 28.6,-395.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-395.98 28.6,-385.98 25.1,-395.98 32.1,-395.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"59.1\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">pack(p:=x)</text>\n",
              "</g>\n",
              "<!-- entry -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>entry</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-540\" rx=\"28.7\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">entry</text>\n",
              "</g>\n",
              "<!-- entry&#45;&gt;L0 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>entry&#45;&gt;L0</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-521.8C28.6,-510.58 28.6,-495.67 28.6,-482.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-482.98 28.6,-472.98 25.1,-482.98 32.1,-482.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"48.1\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">x&#39; = 10</text>\n",
              "</g>\n",
              "<!-- UP -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>UP</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">UP</text>\n",
              "</g>\n",
              "<!-- exit -->\n",
              "<g id=\"node5\" class=\"node\">\n",
              "<title>exit</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">exit</text>\n",
              "</g>\n",
              "<!-- UP&#45;&gt;exit -->\n",
              "<g id=\"edge7\" class=\"edge\">\n",
              "<title>UP&#45;&gt;exit</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-86.8C28.6,-75.58 28.6,-60.67 28.6,-47.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-47.98 28.6,-37.98 25.1,-47.98 32.1,-47.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"47.1\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">x &gt; 10</text>\n",
              "</g>\n",
              "<!-- L2 -->\n",
              "<g id=\"node4\" class=\"node\">\n",
              "<title>L2</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-192\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">L2</text>\n",
              "</g>\n",
              "<!-- L2&#45;&gt;UP -->\n",
              "<g id=\"edge6\" class=\"edge\">\n",
              "<title>L2&#45;&gt;UP</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-173.8C28.6,-162.58 28.6,-147.67 28.6,-134.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-134.98 28.6,-124.98 25.1,-134.98 32.1,-134.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"65.6\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">unpack(x:=p)</text>\n",
              "</g>\n",
              "<!-- L1 -->\n",
              "<g id=\"node6\" class=\"node\">\n",
              "<title>L1</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-279\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L2 -->\n",
              "<g id=\"edge5\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L2</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-260.8C28.6,-249.58 28.6,-234.67 28.6,-221.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-221.98 28.6,-211.98 25.1,-221.98 32.1,-221.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"77.1\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">y ≥ 2019 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L1 -->\n",
              "<g id=\"edge4\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M53.13,-287.03C64.11,-287.79 73.6,-285.12 73.6,-279 73.6,-275.18 69.89,-272.7 64.43,-271.56\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"64.81,-268.08 54.64,-271.05 64.44,-275.07 64.81,-268.08\"/>\n",
              "<text text-anchor=\"middle\" x=\"157.1\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">y &lt; 2019 ∧ y&#39; = y + 1 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "<!-- P&#45;&gt;L1 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>P&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-347.8C28.6,-336.58 28.6,-321.67 28.6,-308.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-308.98 28.6,-298.98 25.1,-308.98 32.1,-308.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"68.1\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">y&#39; = 0 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<graphviz.graphs.Digraph at 0x112dfc370>"
            ]
          },
          "execution_count": 77,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_dcfa1():\n",
        "    A = DCFA('prog4')\n",
        "    ZZ = z3.IntSort()\n",
        "    x, x_out = A.add_var(ZZ, 'x')\n",
        "    y, y_out = A.add_var(ZZ, 'y')\n",
        "    p = A.add_pack_var(ZZ, 'p')\n",
        "\n",
        "    A.add_edge('entry', 'L0', x_out == 10)\n",
        "    A.add_edge('L0', 'P', PackTr((p, x)))\n",
        "    A.add_edge('P', 'L1', z3.And( y_out == 0, x_out == x ))\n",
        "    A.add_edge('L1', 'L1', z3.And( y < 2019, y_out == y + 1, x_out == x ) )\n",
        "    A.add_edge('L1', 'L2', z3.And(y >= 2019, x_out == x))\n",
        "    A.add_edge('L2', 'UP', UnpackTr((x, p)))\n",
        "    A.add_edge('UP', 'exit', x > 10)\n",
        "    A.set_entry_node('entry')\n",
        "    A.set_exit_node('exit')\n",
        "    return A\n",
        "\n",
        "dcfa1 = mk_dcfa1()\n",
        "dcfa1.to_dot()"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 78,
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": true
      },
      "outputs": [],
      "source": [
        "def dcfa_vc_gen(A):\n",
        "    '''Verification Condition (VC) for a Data-Flow and Control Flow Automaton'''\n",
        "    all_vars = A.all()\n",
        "    sig = A.sig() + [z3.BoolSort()]\n",
        "\n",
        "    Invs = dict()\n",
        "    for n in A.nodes:\n",
        "        inv = z3.Function(str(n), *sig)\n",
        "        Invs[n] = inv\n",
        "\n",
        "    Entry = Invs[A.entry]\n",
        "    Exit = Invs[A.exit]\n",
        "\n",
        "    # predicate for packed variables\n",
        "    Pack = z3.Function('Pack', *(A.packed_sig() + [z3.BoolSort()]))\n",
        "    # applied predicate\n",
        "    Packed = Pack(A.pack_vars())\n",
        "\n",
        "\n",
        "    vc = list()\n",
        "    vc.append(z3.ForAll(all_vars, Entry(*A.pre_vars())))\n",
        "\n",
        "    for (k, tr) in A.edges.items():\n",
        "        src, dst = k\n",
        "        srcP, dstP = Invs[src], Invs[dst]\n",
        "\n",
        "        sPred = z3.BoolVal(True)\n",
        "        if isinstance(tr, PackTr):\n",
        "            # add clause defining Packed\n",
        "            body = [srcP(*A.pre_vars())] + [p == x for (p, x) in tr.sub]\n",
        "            vc.append(z3.ForAll(all_vars, z3.Implies(z3.And(*body), Packed)))\n",
        "\n",
        "            # no-op for control-flow transition\n",
        "            tr = z3.And(*[v == v_out for (v, v_out) in A.pre_post_vars()]) \n",
        "        elif isinstance(tr, UnpackTr):\n",
        "            # body depends on the packed predicate\n",
        "            body = [Packed]\n",
        "            unpacked = set()\n",
        "            # generate equalities for unpacked variables\n",
        "            for x, p in tr.sub:\n",
        "                unpacked.add(id(x))\n",
        "                x_out = A.to_post(x)\n",
        "                body.append(x_out == p)\n",
        "            # all other variables are preserved over the transition\n",
        "            for v, v_out in A.pre_post_vars():\n",
        "                if id(v) not in unpacked:\n",
        "                    body.append(v_out == v)\n",
        "            tr = z3.And(*body)\n",
        "\n",
        "        head = dstP(*A.post_vars())\n",
        "        loc = srcP(*A.pre_vars())\n",
        "        vc.append(z3.ForAll(all_vars, z3.Implies(z3.And(loc, tr), head)))\n",
        "\n",
        "\n",
        "    vc.append(z3.ForAll(all_vars,\n",
        "                        z3.Implies(Exit(*A.pre_vars()), z3.BoolVal(False))))\n",
        "    return vc, {n : Invs[n](A.pre_vars()) for n in A.nodes}, Packed"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": []
    },
    {
      "cell_type": "code",
      "execution_count": 79,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 79,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, invs, pack = dcfa_vc_gen(dcfa1)\n",
        "res, answer = solve_horn(vc, max_unfold=40)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 80,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;x, y, x', y', p : entry(x, y) <br/><br/>&forall;x, y, x', y', p : entry(x, y) &and; x' = 10 &rArr; L0(x', y') <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; p = x &rArr; Pack(p) <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; x = x' &and; y = y' &rArr; P(x', y') <br/><br/>&forall;x, y, x', y', p : P(x, y) &and; y' = 0 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L1(x, y) &and; y &lt; 2019 &and; y' = y + 1 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p : L1(x, y) &and; y &ge; 2019 &and; x' = x &rArr; L2(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L2(x, y) &and; Pack(p) &and; x' = p &and; y' = y &rArr; UP(x', y') <br/><br/>&forall;x, y, x', y', p : UP(x, y) &and; x &gt; 10 &rArr; exit(x', y') <br/><br/>&forall;x, y, x', y', p : exit(x, y) &rArr; False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;x, y, x', y', p : entry(x, y) <br/><br/>&forall;x, y, x', y', p : entry(x, y) &and; x' = 10 &rArr; L0(x', y') <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; p = x &rArr; Pack(p) <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; x = x' &and; y = y' &rArr; P(x', y') <br/><br/>&forall;x, y, x', y', p : P(x, y) &and; y' = 0 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L1(x, y) &and; y &lt; 2019 &and; y' = y + 1 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p : L1(x, y) &and; y &ge; 2019 &and; x' = x &rArr; L2(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L2(x, y) &and; Pack(p) &and; x' = p &and; y' = y &rArr; UP(x', y') <br/><br/>&forall;x, y, x', y', p : UP(x, y) &and; x &gt; 10 &rArr; exit(x', y') <br/><br/>&forall;x, y, x', y', p : exit(x, y) &rArr; False <br/><br/>\""
            ]
          },
          "execution_count": 80,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "chc_to_str(vc)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 81,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&not;(p &ge; 11)"
            ],
            "text/plain": [
              "&not;(p &ge; 11)"
            ]
          },
          "execution_count": 81,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer.eval(pack)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 82,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "[L0 = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 11)],\n",
              " UP = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 11)],\n",
              " L2 = [else &rarr; True],\n",
              " exit = [else &rarr; False],\n",
              " P = [else &rarr; True],\n",
              " Pack = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 11)],\n",
              " L1 = [else &rarr; True],\n",
              " entry = [else &rarr; True]]"
            ],
            "text/plain": [
              "[L0 = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 11)],\n",
              " UP = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 11)],\n",
              " L2 = [else &rarr; True],\n",
              " exit = [else &rarr; False],\n",
              " P = [else &rarr; True],\n",
              " Pack = [else &rarr; &not;(&#957;<sub>0</sub> &ge; 11)],\n",
              " L1 = [else &rarr; True],\n",
              " entry = [else &rarr; True]]"
            ]
          },
          "execution_count": 82,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 83,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "image/svg+xml": [
              "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
              "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
              " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
              "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
              " -->\n",
              "<!-- Pages: 1 -->\n",
              "<svg width=\"225pt\" height=\"566pt\"\n",
              " viewBox=\"0.00 0.00 224.60 566.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
              "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 562)\">\n",
              "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-562 220.6,-562 220.6,4 -4,4\"/>\n",
              "<!-- L0 -->\n",
              "<g id=\"node1\" class=\"node\">\n",
              "<title>L0</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-453\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
              "</g>\n",
              "<!-- P -->\n",
              "<g id=\"node7\" class=\"node\">\n",
              "<title>P</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-366\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">P</text>\n",
              "</g>\n",
              "<!-- L0&#45;&gt;P -->\n",
              "<g id=\"edge2\" class=\"edge\">\n",
              "<title>L0&#45;&gt;P</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-434.8C28.6,-423.58 28.6,-408.67 28.6,-395.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-395.98 28.6,-385.98 25.1,-395.98 32.1,-395.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"59.1\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">pack(p:=x)</text>\n",
              "</g>\n",
              "<!-- entry -->\n",
              "<g id=\"node2\" class=\"node\">\n",
              "<title>entry</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-540\" rx=\"28.7\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">entry</text>\n",
              "</g>\n",
              "<!-- entry&#45;&gt;L0 -->\n",
              "<g id=\"edge1\" class=\"edge\">\n",
              "<title>entry&#45;&gt;L0</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-521.8C28.6,-510.58 28.6,-495.67 28.6,-482.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-482.98 28.6,-472.98 25.1,-482.98 32.1,-482.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"48.1\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">x&#39; = 11</text>\n",
              "</g>\n",
              "<!-- UP -->\n",
              "<g id=\"node3\" class=\"node\">\n",
              "<title>UP</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">UP</text>\n",
              "</g>\n",
              "<!-- exit -->\n",
              "<g id=\"node5\" class=\"node\">\n",
              "<title>exit</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">exit</text>\n",
              "</g>\n",
              "<!-- UP&#45;&gt;exit -->\n",
              "<g id=\"edge7\" class=\"edge\">\n",
              "<title>UP&#45;&gt;exit</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-86.8C28.6,-75.58 28.6,-60.67 28.6,-47.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-47.98 28.6,-37.98 25.1,-47.98 32.1,-47.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"47.1\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">x &gt; 10</text>\n",
              "</g>\n",
              "<!-- L2 -->\n",
              "<g id=\"node4\" class=\"node\">\n",
              "<title>L2</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-192\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">L2</text>\n",
              "</g>\n",
              "<!-- L2&#45;&gt;UP -->\n",
              "<g id=\"edge6\" class=\"edge\">\n",
              "<title>L2&#45;&gt;UP</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-173.8C28.6,-162.58 28.6,-147.67 28.6,-134.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-134.98 28.6,-124.98 25.1,-134.98 32.1,-134.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"65.6\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">unpack(x:=p)</text>\n",
              "</g>\n",
              "<!-- L1 -->\n",
              "<g id=\"node6\" class=\"node\">\n",
              "<title>L1</title>\n",
              "<ellipse fill=\"none\" stroke=\"black\" cx=\"28.6\" cy=\"-279\" rx=\"27\" ry=\"18\"/>\n",
              "<text text-anchor=\"middle\" x=\"28.6\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">L1</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L2 -->\n",
              "<g id=\"edge5\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L2</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-260.8C28.6,-249.58 28.6,-234.67 28.6,-221.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-221.98 28.6,-211.98 25.1,-221.98 32.1,-221.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"66.6\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">False ∧ x&#39; = x</text>\n",
              "</g>\n",
              "<!-- L1&#45;&gt;L1 -->\n",
              "<g id=\"edge4\" class=\"edge\">\n",
              "<title>L1&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M53.13,-287.03C64.11,-287.79 73.6,-285.12 73.6,-279 73.6,-275.18 69.89,-272.7 64.43,-271.56\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"64.81,-268.08 54.64,-271.05 64.44,-275.07 64.81,-268.08\"/>\n",
              "<text text-anchor=\"middle\" x=\"145.1\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">True ∧ y&#39; = y + 1 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "<!-- P&#45;&gt;L1 -->\n",
              "<g id=\"edge3\" class=\"edge\">\n",
              "<title>P&#45;&gt;L1</title>\n",
              "<path fill=\"none\" stroke=\"black\" d=\"M28.6,-347.8C28.6,-336.58 28.6,-321.67 28.6,-308.69\"/>\n",
              "<polygon fill=\"black\" stroke=\"black\" points=\"32.1,-308.98 28.6,-298.98 25.1,-308.98 32.1,-308.98\"/>\n",
              "<text text-anchor=\"middle\" x=\"68.1\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">y&#39; = 0 ∧ x&#39; = x</text>\n",
              "</g>\n",
              "</g>\n",
              "</svg>\n"
            ],
            "text/plain": [
              "<graphviz.graphs.Digraph at 0x112dfca30>"
            ]
          },
          "execution_count": 83,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "def mk_dcfa2():\n",
        "    A = DCFA('dcfa2')\n",
        "    ZZ = z3.IntSort()\n",
        "    x, x_out = A.add_var(ZZ, 'x')\n",
        "    y, y_out = A.add_var(ZZ, 'y')\n",
        "    p = A.add_pack_var(ZZ, 'p')\n",
        "\n",
        "    A.add_edge('entry', 'L0', x_out == 11)\n",
        "    A.add_edge('L0', 'P', PackTr((p, x)))\n",
        "    A.add_edge('P', 'L1', z3.And( y_out == 0, x_out == x ))\n",
        "    A.add_edge('L1', 'L1', z3.And( z3.BoolVal(True), y_out == y + 1, x_out == x ) )\n",
        "    A.add_edge('L1', 'L2', z3.And(z3.BoolVal(False), x_out == x))\n",
        "    A.add_edge('L2', 'UP', UnpackTr((x, p)))\n",
        "    A.add_edge('UP', 'exit', x > 10)\n",
        "    A.set_entry_node('entry')\n",
        "    A.set_exit_node('exit')\n",
        "    return A\n",
        "\n",
        "dcfa2 = mk_dcfa2()\n",
        "dcfa2.to_dot()"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 84,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<b>sat</b>"
            ],
            "text/plain": [
              "<b>sat</b>"
            ]
          },
          "execution_count": 84,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "vc, invs, pack = dcfa_vc_gen(dcfa2)\n",
        "res, answer = solve_horn(vc, max_unfold=40)\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 85,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "[L0 = [else &rarr; True],\n",
              " UP = [else &rarr; False],\n",
              " exit = [else &rarr; False],\n",
              " L2 = [else &rarr; False],\n",
              " P = [else &rarr; True],\n",
              " Pack = [else &rarr; True],\n",
              " L1 = [else &rarr; True],\n",
              " entry = [else &rarr; True]]"
            ],
            "text/plain": [
              "[L0 = [else &rarr; True],\n",
              " UP = [else &rarr; False],\n",
              " exit = [else &rarr; False],\n",
              " L2 = [else &rarr; False],\n",
              " P = [else &rarr; True],\n",
              " Pack = [else &rarr; True],\n",
              " L1 = [else &rarr; True],\n",
              " entry = [else &rarr; True]]"
            ]
          },
          "execution_count": 85,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "answer"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Conclusion\n",
        "\n",
        "This is the end of the interactive portion of the tutorial"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 86,
      "metadata": {
        "trusted": true
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "&forall;x, y, x', y', p : entry(x, y) <br/><br/>&forall;x, y, x', y', p : entry(x, y) &and; x' = 11 &rArr; L0(x', y') <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; p = x &rArr; Pack(p) <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; x = x' &and; y = y' &rArr; P(x', y') <br/><br/>&forall;x, y, x', y', p : P(x, y) &and; y' = 0 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L1(x, y) &and; True &and; y' = y + 1 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p : L1(x, y) &and; False &and; x' = x &rArr; L2(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L2(x, y) &and; Pack(p) &and; x' = p &and; y' = y &rArr; UP(x', y') <br/><br/>&forall;x, y, x', y', p : UP(x, y) &and; x &gt; 10 &rArr; exit(x', y') <br/><br/>&forall;x, y, x', y', p : exit(x, y) &rArr; False <br/><br/>"
            ],
            "text/plain": [
              "\"&forall;x, y, x', y', p : entry(x, y) <br/><br/>&forall;x, y, x', y', p : entry(x, y) &and; x' = 11 &rArr; L0(x', y') <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; p = x &rArr; Pack(p) <br/><br/>&forall;x, y, x', y', p : L0(x, y) &and; x = x' &and; y = y' &rArr; P(x', y') <br/><br/>&forall;x, y, x', y', p : P(x, y) &and; y' = 0 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L1(x, y) &and; True &and; y' = y + 1 &and; x' = x &rArr; L1(x', y') <br/><br/>&forall;x, y, x', y', p : L1(x, y) &and; False &and; x' = x &rArr; L2(x', y') <br/><br/>&forall;x, y, x', y', p :<br/> L2(x, y) &and; Pack(p) &and; x' = p &and; y' = y &rArr; UP(x', y') <br/><br/>&forall;x, y, x', y', p : UP(x, y) &and; x &gt; 10 &rArr; exit(x', y') <br/><br/>&forall;x, y, x', y', p : exit(x, y) &rArr; False <br/><br/>\""
            ]
          },
          "execution_count": 86,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "chc_to_str(vc)\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": []
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "trusted": true
      },
      "outputs": [],
      "source": []
    }
  ],
  "metadata": {
    "kernelspec": {
      "display_name": "venv",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "file_extension": ".py",
      "mimetype": "text/x-python",
      "name": "python",
      "nbconvert_exporter": "python",
      "pygments_lexer": "ipython3",
      "version": "3.9.16"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 2
}