ECE750T29_Fall2019.ipynb

{
  "cells": [
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "# Spacer on Jupyter\n\nThis is an interactive document. You can follow along on the cloud, change, play, go deeper into the code.\n\nTo 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 `ECE750T29_Fall2019.ipynb` notebook\n \nIf 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."
    },
    {
      "metadata": {
        "code_folding": [
          4,
          17,
          23,
          32,
          39
        ],
        "trusted": true
      },
      "cell_type": "code",
      "source": "from IPython.core.display import display, HTML\nimport sys\nimport z3\n\nclass 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\ndef 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\ndef 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\ndef 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\nclass SpacerProof(object):\n    def __init__(self, pf_ast):\n        self._ast = pf_ast\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 in visited:\n            return\n\n        visited.add(ast)\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 not in visited:\n                graph.node(str(k_fact.get_id()), str(k_fact))\n                visited.add(k_fact)\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_svg_(self):\n        return self.to_dot()._repr_svg_()\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\nz3.set_param(proof=True)\nz3.set_param(model=True)\n# print expressions with HTML\nz3.set_html_mode(True)",
      "execution_count": 7,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Craig Interpolation\n\nLet $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  \n**Example 1**: let $A$ be $a < x < b$ and $B$ be $a > b$. Then, $A \\wedge B$ is unsat, and $a < b$ is (the unique) interpolant.\n\nCraig Interpolation is at a core of many SMT- and SAT-based verification algorithms. \nComputing 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 \nwhere uninterpreted constants $c$ are shared between $A$ and $B$, and uninterpreted constants $a$ and $b$ are  local to $A$ and $B$, respectively."
    },
    {
      "metadata": {
        "code_folding": [
          1
        ],
        "trusted": true
      },
      "cell_type": "code",
      "source": "# compute uninterpreted constants in a formula\ndef 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",
      "execution_count": 2,
      "outputs": []
    },
    {
      "metadata": {
        "code_folding": [
          1,
          7,
          15
        ],
        "trusted": true
      },
      "cell_type": "code",
      "source": "# wrapper to solve CHC constraints and extract result\ndef 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",
      "execution_count": 3,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "# Binary Craig Interpolation by reduction to CHC\ndef 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",
      "execution_count": 4,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "a, b, x, y = z3.Ints('a b x y')\nitp = interpolate(z3.And(a < x, x < b), z3.And(b < a))",
      "execution_count": 5,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "itp",
      "execution_count": 6,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 6,
          "data": {
            "text/html": "&not;(a + -1&middot;b &ge; -1)",
            "text/plain": "&not;(a + -1&middot;b &ge; -1)"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Principle of Induction\n\nSymbolic 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   \nThe 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."
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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"
    },
    {
      "metadata": {
        "code_folding": [
          0,
          15,
          36,
          50,
          75,
          80,
          87,
          91,
          98,
          118,
          130,
          136,
          139,
          148,
          150,
          153,
          159
        ],
        "trusted": false
      },
      "cell_type": "code",
      "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)",
      "execution_count": 7,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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:"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 8,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=True)\nHtmlStr(ts0)",
      "execution_count": 9,
      "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": 9,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "We define a function `vc_gen` that generates **verification conditions** using the principle of induction:"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 10,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts0)",
      "execution_count": 11,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "chc_to_str(vc)",
      "execution_count": 12,
      "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": 12,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "HtmlStr(inv)",
      "execution_count": 13,
      "outputs": [
        {
          "data": {
            "text/html": "Inv(x)",
            "text/plain": "'Inv(x)'"
          },
          "execution_count": 13,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)",
      "execution_count": 14,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res",
      "execution_count": 15,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 15,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer",
      "execution_count": 16,
      "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": 16,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(inv)",
      "execution_count": 17,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &ge; 6)",
            "text/plain": "&not;(x &ge; 6)"
          },
          "execution_count": 17,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=False)\nHtmlStr(ts0)",
      "execution_count": 18,
      "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": 18,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts0)\nres, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": 19,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unsat</b>",
            "text/plain": "'<b>unsat</b>'"
          },
          "execution_count": 19,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer",
      "execution_count": 20,
      "outputs": [
        {
          "data": {
            "text/html": "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; &not;(5 &le; A) &and; 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))",
            "text/plain": "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; &not;(5 &le; A) &and; 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))"
          },
          "execution_count": 20,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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:"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "SpacerProof(answer)",
      "execution_count": 21,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"116pt\" height=\"404pt\"\n viewBox=\"0.00 0.00 115.89 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-400 111.8904,-400 111.8904,4 -4,4\"/>\n<!-- 2204 -->\n<g id=\"node1\" class=\"node\">\n<title>2204</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-18\" rx=\"53.8905\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">query!19(4)</text>\n</g>\n<!-- 2214 -->\n<g id=\"node2\" class=\"node\">\n<title>2214</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-90\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(4)</text>\n</g>\n<!-- 2214&#45;&gt;2204 -->\n<g id=\"edge5\" class=\"edge\">\n<title>2214&#45;&gt;2204</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-71.8314C53.9452,-64.131 53.9452,-54.9743 53.9452,-46.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-46.4132 53.9452,-36.4133 50.4453,-46.4133 57.4453,-46.4132\"/>\n</g>\n<!-- 2336 -->\n<g id=\"node3\" class=\"node\">\n<title>2336</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-162\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(3)</text>\n</g>\n<!-- 2336&#45;&gt;2214 -->\n<g id=\"edge4\" class=\"edge\">\n<title>2336&#45;&gt;2214</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-143.8314C53.9452,-136.131 53.9452,-126.9743 53.9452,-118.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-118.4132 53.9452,-108.4133 50.4453,-118.4133 57.4453,-118.4132\"/>\n</g>\n<!-- 2318 -->\n<g id=\"node4\" class=\"node\">\n<title>2318</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-234\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(2)</text>\n</g>\n<!-- 2318&#45;&gt;2336 -->\n<g id=\"edge3\" class=\"edge\">\n<title>2318&#45;&gt;2336</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-215.8314C53.9452,-208.131 53.9452,-198.9743 53.9452,-190.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-190.4132 53.9452,-180.4133 50.4453,-190.4133 57.4453,-190.4132\"/>\n</g>\n<!-- 2272 -->\n<g id=\"node5\" class=\"node\">\n<title>2272</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-306\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(1)</text>\n</g>\n<!-- 2272&#45;&gt;2318 -->\n<g id=\"edge2\" class=\"edge\">\n<title>2272&#45;&gt;2318</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-287.8314C53.9452,-280.131 53.9452,-270.9743 53.9452,-262.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-262.4132 53.9452,-252.4133 50.4453,-262.4133 57.4453,-262.4132\"/>\n</g>\n<!-- 2256 -->\n<g id=\"node6\" class=\"node\">\n<title>2256</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-378\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(0)</text>\n</g>\n<!-- 2256&#45;&gt;2272 -->\n<g id=\"edge1\" class=\"edge\">\n<title>2256&#45;&gt;2272</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-359.8314C53.9452,-352.131 53.9452,-342.9743 53.9452,-334.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-334.4132 53.9452,-324.4133 50.4453,-334.4133 57.4453,-334.4132\"/>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x1106d0350>"
          },
          "execution_count": 21,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "The shortest counter-example is to start the counter at `0` and count until `4`, at which point the bad state is reached."
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Principle of Backward Induction\n\nSometimes forward induction is not effective. One alternative is to run the analysis backwards.\nA counter-example starts from a bad state and goes towards initial state. There is no need to change the\nunderlying sat algorithm for that. We simply change the encoding!\n\nA **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$."
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 22,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=True)\nvc, inv = vc_gen_bwd(ts0)\nchc_to_str(vc)",
      "execution_count": 23,
      "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": 23,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)\nanswer.eval(inv)",
      "execution_count": 24,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &le; 9)",
            "text/plain": "&not;(x &le; 9)"
          },
          "execution_count": 24,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=False)\nvc, inv = vc_gen_bwd(ts0)\nres, answer = solve_horn(vc)\nSpacerProof(answer)",
      "execution_count": 25,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"116pt\" height=\"404pt\"\n viewBox=\"0.00 0.00 115.89 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-400 111.8904,-400 111.8904,4 -4,4\"/>\n<!-- 794 -->\n<g id=\"node1\" class=\"node\">\n<title>794</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-18\" rx=\"53.8905\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">query!67(0)</text>\n</g>\n<!-- 499 -->\n<g id=\"node2\" class=\"node\">\n<title>499</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-90\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(0)</text>\n</g>\n<!-- 499&#45;&gt;794 -->\n<g id=\"edge5\" class=\"edge\">\n<title>499&#45;&gt;794</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-71.8314C53.9452,-64.131 53.9452,-54.9743 53.9452,-46.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-46.4132 53.9452,-36.4133 50.4453,-46.4133 57.4453,-46.4132\"/>\n</g>\n<!-- 1912 -->\n<g id=\"node3\" class=\"node\">\n<title>1912</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-162\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(1)</text>\n</g>\n<!-- 1912&#45;&gt;499 -->\n<g id=\"edge4\" class=\"edge\">\n<title>1912&#45;&gt;499</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-143.8314C53.9452,-136.131 53.9452,-126.9743 53.9452,-118.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-118.4132 53.9452,-108.4133 50.4453,-118.4133 57.4453,-118.4132\"/>\n</g>\n<!-- 1578 -->\n<g id=\"node4\" class=\"node\">\n<title>1578</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-234\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(2)</text>\n</g>\n<!-- 1578&#45;&gt;1912 -->\n<g id=\"edge3\" class=\"edge\">\n<title>1578&#45;&gt;1912</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-215.8314C53.9452,-208.131 53.9452,-198.9743 53.9452,-190.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-190.4132 53.9452,-180.4133 50.4453,-190.4133 57.4453,-190.4132\"/>\n</g>\n<!-- 1483 -->\n<g id=\"node5\" class=\"node\">\n<title>1483</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-306\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(3)</text>\n</g>\n<!-- 1483&#45;&gt;1578 -->\n<g id=\"edge2\" class=\"edge\">\n<title>1483&#45;&gt;1578</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-287.8314C53.9452,-280.131 53.9452,-270.9743 53.9452,-262.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-262.4132 53.9452,-252.4133 50.4453,-262.4133 57.4453,-262.4132\"/>\n</g>\n<!-- 204 -->\n<g id=\"node6\" class=\"node\">\n<title>204</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"53.9452\" cy=\"-378\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"53.9452\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(4)</text>\n</g>\n<!-- 204&#45;&gt;1483 -->\n<g id=\"edge1\" class=\"edge\">\n<title>204&#45;&gt;1483</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M53.9452,-359.8314C53.9452,-352.131 53.9452,-342.9743 53.9452,-334.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"57.4453,-334.4132 53.9452,-324.4133 50.4453,-334.4133 57.4453,-334.4132\"/>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x1106eb450>"
          },
          "execution_count": 25,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "As expected, the counter-example runs backward. Starting fromt the bad state and evolving to the initial state."
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## The principle of 2-induction\n\n2-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\nA **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   \nFromt the above definition, it is obvious that discovering a 2-inductive hypothesis is reducible to satisfiablity of *non-linear* CHC."
    },
    {
      "metadata": {
        "code_folding": [
          1
        ],
        "trusted": false
      },
      "cell_type": "code",
      "source": "# helper function to compute sequential composition by connecting output of T1 to input of T2\ndef 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\ndef 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",
      "execution_count": 26,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=True)\nvc, inv = vc_gen_2ind(ts0)\nchc_to_str(vc)",
      "execution_count": 27,
      "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": 27,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)\nanswer.eval(inv)",
      "execution_count": 28,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &ge; 6)",
            "text/plain": "&not;(x &ge; 6)"
          },
          "execution_count": 28,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=False)\nvc, inv = vc_gen_2ind(ts0)\nres, answer = solve_horn(vc)\nSpacerProof(answer)",
      "execution_count": 29,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"190pt\" height=\"476pt\"\n viewBox=\"0.00 0.00 189.89 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-472 185.8927,-472 185.8927,4 -4,4\"/>\n<!-- 3000 -->\n<g id=\"node1\" class=\"node\">\n<title>3000</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"73.9464\" cy=\"-18\" rx=\"53.8905\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"73.9464\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">query!97(4)</text>\n</g>\n<!-- 3014 -->\n<g id=\"node2\" class=\"node\">\n<title>3014</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"73.9464\" cy=\"-90\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"73.9464\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(4)</text>\n</g>\n<!-- 3014&#45;&gt;3000 -->\n<g id=\"edge11\" class=\"edge\">\n<title>3014&#45;&gt;3000</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M73.9464,-71.8314C73.9464,-64.131 73.9464,-54.9743 73.9464,-46.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"77.4465,-46.4132 73.9464,-36.4133 70.4465,-46.4133 77.4465,-46.4132\"/>\n</g>\n<!-- 3274 -->\n<g id=\"node3\" class=\"node\">\n<title>3274</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"40.9464\" cy=\"-162\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"40.9464\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(3)</text>\n</g>\n<!-- 3274&#45;&gt;3014 -->\n<g id=\"edge9\" class=\"edge\">\n<title>3274&#45;&gt;3014</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M49.1037,-144.2022C52.9001,-135.9192 57.4961,-125.8915 61.6975,-116.7248\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"64.898,-118.142 65.8829,-107.593 58.5346,-115.2254 64.898,-118.142\"/>\n</g>\n<!-- 3276 -->\n<g id=\"node4\" class=\"node\">\n<title>3276</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"106.9464\" cy=\"-234\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"106.9464\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(2)</text>\n</g>\n<!-- 3276&#45;&gt;3014 -->\n<g id=\"edge10\" class=\"edge\">\n<title>3276&#45;&gt;3014</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M103.4012,-216.0168C99.7532,-197.8111 93.7929,-168.8731 87.9464,-144 85.9297,-135.4205 83.5778,-126.1172 81.3837,-117.6887\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"84.7502,-116.7281 78.8189,-107.9491 77.9809,-118.5108 84.7502,-116.7281\"/>\n</g>\n<!-- 3276&#45;&gt;3274 -->\n<g id=\"edge7\" class=\"edge\">\n<title>3276&#45;&gt;3274</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M91.6387,-217.3008C83.1421,-208.0317 72.4238,-196.339 63.0338,-186.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"65.5083,-183.6152 56.171,-178.6087 60.3482,-188.3453 65.5083,-183.6152\"/>\n</g>\n<!-- 3222 -->\n<g id=\"node5\" class=\"node\">\n<title>3222</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"40.9464\" cy=\"-306\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"40.9464\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(1)</text>\n</g>\n<!-- 3222&#45;&gt;3274 -->\n<g id=\"edge8\" class=\"edge\">\n<title>3222&#45;&gt;3274</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M40.9464,-287.7623C40.9464,-263.201 40.9464,-219.2474 40.9464,-190.3541\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"44.4465,-190.0896 40.9464,-180.0896 37.4465,-190.0897 44.4465,-190.0896\"/>\n</g>\n<!-- 3222&#45;&gt;3276 -->\n<g id=\"edge5\" class=\"edge\">\n<title>3222&#45;&gt;3276</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M56.254,-289.3008C64.7506,-280.0317 75.4689,-268.339 84.8589,-258.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"87.5445,-260.3453 91.7218,-250.6087 82.3844,-255.6152 87.5445,-260.3453\"/>\n</g>\n<!-- 3271 -->\n<g id=\"node6\" class=\"node\">\n<title>3271</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"106.9464\" cy=\"-378\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"106.9464\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(0)</text>\n</g>\n<!-- 3271&#45;&gt;3276 -->\n<g id=\"edge6\" class=\"edge\">\n<title>3271&#45;&gt;3276</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M106.9464,-359.7623C106.9464,-335.201 106.9464,-291.2474 106.9464,-262.3541\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"110.4465,-262.0896 106.9464,-252.0896 103.4465,-262.0897 110.4465,-262.0896\"/>\n</g>\n<!-- 3271&#45;&gt;3222 -->\n<g id=\"edge3\" class=\"edge\">\n<title>3271&#45;&gt;3222</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M91.6387,-361.3008C83.1421,-352.0317 72.4238,-340.339 63.0338,-330.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"65.5083,-327.6152 56.171,-322.6087 60.3482,-332.3453 65.5083,-327.6152\"/>\n</g>\n<!-- 3057 -->\n<g id=\"node7\" class=\"node\">\n<title>3057</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"40.9464\" cy=\"-450\" rx=\"40.8928\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"40.9464\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(&#45;1)</text>\n</g>\n<!-- 3057&#45;&gt;3222 -->\n<g id=\"edge4\" class=\"edge\">\n<title>3057&#45;&gt;3222</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M40.9464,-431.7623C40.9464,-407.201 40.9464,-363.2474 40.9464,-334.3541\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"44.4465,-334.0896 40.9464,-324.0896 37.4465,-334.0897 44.4465,-334.0896\"/>\n</g>\n<!-- 3057&#45;&gt;3271 -->\n<g id=\"edge1\" class=\"edge\">\n<title>3057&#45;&gt;3271</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M56.254,-433.3008C64.7506,-424.0317 75.4689,-412.339 84.8589,-402.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"87.5445,-404.3453 91.7218,-394.6087 82.3844,-399.6152 87.5445,-404.3453\"/>\n</g>\n<!-- 3190 -->\n<g id=\"node8\" class=\"node\">\n<title>3190</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"140.9464\" cy=\"-450\" rx=\"40.8928\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"140.9464\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(&#45;2)</text>\n</g>\n<!-- 3190&#45;&gt;3271 -->\n<g id=\"edge2\" class=\"edge\">\n<title>3190&#45;&gt;3271</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M132.5419,-432.2022C128.6304,-423.9192 123.8951,-413.8915 119.5664,-404.7248\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"122.6892,-403.141 115.2542,-395.593 116.3594,-406.1301 122.6892,-403.141\"/>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x1106ebb10>"
          },
          "execution_count": 29,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "Spacer often finds the shortest counterexample. The counterexample above is short (4 transitions), but maybe not the most obvious one."
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Control Flow Automaton (CFA)\n\nIt is often desired to extend a transition system with control locations. \nA **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  \nA 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\nA 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)'$"
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "We begin by defining a python class to represent a CFA:"
    },
    {
      "metadata": {
        "code_folding": [
          5,
          12,
          14,
          16,
          18,
          20,
          22,
          24,
          26,
          28,
          30,
          32,
          36,
          39,
          42,
          44,
          47
        ],
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 30,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "Then, convert our running example to a CFA:"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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\ncfa0 = mk_cfa0(safe=True)\ncfa0.to_dot()",
      "execution_count": 31,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"178pt\" height=\"218pt\"\n viewBox=\"0.00 0.00 178.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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-214 174,-214 174,4 -4,4\"/>\n<!-- L0 -->\n<g id=\"node1\" class=\"node\">\n<title>L0</title>\n<ellipse fill=\"none\" stroke=\"#000000\" 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\" fill=\"#000000\">L0</text>\n</g>\n<!-- L1 -->\n<g id=\"node3\" class=\"node\">\n<title>L1</title>\n<ellipse fill=\"none\" stroke=\"#000000\" 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\" fill=\"#000000\">L1</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=\"#000000\" d=\"M27,-173.9735C27,-162.1918 27,-146.5607 27,-133.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"30.5001,-133.0033 27,-123.0034 23.5001,-133.0034 30.5001,-133.0033\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x&#39; = 0</text>\n</g>\n<!-- L2 -->\n<g id=\"node2\" class=\"node\">\n<title>L2</title>\n<ellipse fill=\"none\" stroke=\"#000000\" 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\" fill=\"#000000\">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=\"#000000\" d=\"M27,-86.9735C27,-75.1918 27,-59.5607 27,-46.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"30.5001,-46.0033 27,-36.0034 23.5001,-46.0034 30.5001,-46.0033\"/>\n<text text-anchor=\"middle\" x=\"45\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x ≥ 10</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=\"#000000\" d=\"M51.5325,-112.752C62.5078,-113.4902 72,-110.9063 72,-105 72,-101.0317 67.7151,-98.5632 61.5743,-97.5944\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.6472,-94.0949 51.5325,-97.248 61.4059,-101.0908 61.6472,-94.0949\"/>\n<text text-anchor=\"middle\" x=\"121\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x ≤ 5 ∧ x&#39; = x + 1</text>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<graphviz.dot.Digraph at 0x1149678d0>"
          },
          "execution_count": 31,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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:"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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}",
      "execution_count": 32,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "chc, invs = cfa_vc_gen(cfa0)\nchc_to_str(chc)",
      "execution_count": 33,
      "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": 33,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(chc)\nres",
      "execution_count": 34,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 34,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "invs",
      "execution_count": 35,
      "outputs": [
        {
          "data": {
            "text/plain": "{'L0': L0(x), 'L2': L2(x), 'L1': L1(x)}"
          },
          "execution_count": 35,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(invs['L0'])",
      "execution_count": 36,
      "outputs": [
        {
          "data": {
            "text/html": "True",
            "text/plain": "True"
          },
          "execution_count": 36,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(invs['L1'])",
      "execution_count": 37,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &ge; 7)",
            "text/plain": "&not;(x &ge; 7)"
          },
          "execution_count": 37,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(invs['L2'])",
      "execution_count": 38,
      "outputs": [
        {
          "data": {
            "text/html": "False",
            "text/plain": "False"
          },
          "execution_count": 38,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "cfa0 = mk_cfa0(safe=False)\nvc, invs = cfa_vc_gen(cfa0)\nres, answer = solve_horn(vc)\nSpacerProof(answer)",
      "execution_count": 39,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"125pt\" height=\"476pt\"\n viewBox=\"0.00 0.00 124.99 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-472 120.9896,-472 120.9896,4 -4,4\"/>\n<!-- 1911 -->\n<g id=\"node1\" class=\"node\">\n<title>1911</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-18\" rx=\"58.4896\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">query!136(0)</text>\n</g>\n<!-- 1538 -->\n<g id=\"node2\" class=\"node\">\n<title>1538</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-90\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L2(0)</text>\n</g>\n<!-- 1538&#45;&gt;1911 -->\n<g id=\"edge6\" class=\"edge\">\n<title>1538&#45;&gt;1911</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M58.4948,-71.8314C58.4948,-64.131 58.4948,-54.9743 58.4948,-46.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.9949,-46.4132 58.4948,-36.4133 54.9949,-46.4133 61.9949,-46.4132\"/>\n</g>\n<!-- 1523 -->\n<g id=\"node3\" class=\"node\">\n<title>1523</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-162\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(4)</text>\n</g>\n<!-- 1523&#45;&gt;1538 -->\n<g id=\"edge5\" class=\"edge\">\n<title>1523&#45;&gt;1538</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M58.4948,-143.8314C58.4948,-136.131 58.4948,-126.9743 58.4948,-118.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.9949,-118.4132 58.4948,-108.4133 54.9949,-118.4133 61.9949,-118.4132\"/>\n</g>\n<!-- 677 -->\n<g id=\"node4\" class=\"node\">\n<title>677</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-234\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(3)</text>\n</g>\n<!-- 677&#45;&gt;1523 -->\n<g id=\"edge4\" class=\"edge\">\n<title>677&#45;&gt;1523</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M58.4948,-215.8314C58.4948,-208.131 58.4948,-198.9743 58.4948,-190.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.9949,-190.4132 58.4948,-180.4133 54.9949,-190.4133 61.9949,-190.4132\"/>\n</g>\n<!-- 966 -->\n<g id=\"node5\" class=\"node\">\n<title>966</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-306\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(2)</text>\n</g>\n<!-- 966&#45;&gt;677 -->\n<g id=\"edge3\" class=\"edge\">\n<title>966&#45;&gt;677</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M58.4948,-287.8314C58.4948,-280.131 58.4948,-270.9743 58.4948,-262.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.9949,-262.4132 58.4948,-252.4133 54.9949,-262.4133 61.9949,-262.4132\"/>\n</g>\n<!-- 437 -->\n<g id=\"node6\" class=\"node\">\n<title>437</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-378\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(1)</text>\n</g>\n<!-- 437&#45;&gt;966 -->\n<g id=\"edge2\" class=\"edge\">\n<title>437&#45;&gt;966</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M58.4948,-359.8314C58.4948,-352.131 58.4948,-342.9743 58.4948,-334.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.9949,-334.4132 58.4948,-324.4133 54.9949,-334.4133 61.9949,-334.4132\"/>\n</g>\n<!-- 463 -->\n<g id=\"node7\" class=\"node\">\n<title>463</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-450\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(0)</text>\n</g>\n<!-- 463&#45;&gt;437 -->\n<g id=\"edge1\" class=\"edge\">\n<title>463&#45;&gt;437</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M58.4948,-431.8314C58.4948,-424.131 58.4948,-414.9743 58.4948,-406.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"61.9949,-406.4132 58.4948,-396.4133 54.9949,-406.4133 61.9949,-406.4132\"/>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x114969bd0>"
          },
          "execution_count": 39,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Arrays and Quantifiers\n\nSo 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:"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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\ncfa1 = mk_cfa1()\ncfa1.to_dot()",
      "execution_count": 40,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"390pt\" height=\"218pt\"\n viewBox=\"0.00 0.00 390.25 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-214 386.2474,-214 386.2474,4 -4,4\"/>\n<!-- entry -->\n<g id=\"node1\" class=\"node\">\n<title>entry</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-192\" rx=\"29.4969\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">entry</text>\n</g>\n<!-- L0 -->\n<g id=\"node2\" class=\"node\">\n<title>L0</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-173.9735C29.2474,-162.1918 29.2474,-146.5607 29.2474,-133.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-133.0033 29.2474,-123.0034 25.7475,-133.0034 32.7475,-133.0033\"/>\n<text text-anchor=\"middle\" x=\"75.2474\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">cnt&#39; = 0 ∧ N&#39; &gt; 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=\"#000000\" d=\"M53.7799,-112.752C64.7552,-113.4902 74.2474,-110.9063 74.2474,-105 74.2474,-101.0317 69.9625,-98.5632 63.8217,-97.5944\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"63.8946,-94.0949 53.7799,-97.248 63.6533,-101.0908 63.8946,-94.0949\"/>\n<text text-anchor=\"middle\" x=\"228.2474\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">cnt &lt; N ∧ cnt&#39; = cnt + 1 ∧ MEM&#39; = Store(MEM, cnt, 0)</text>\n</g>\n<!-- exit -->\n<g id=\"node3\" class=\"node\">\n<title>exit</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">exit</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=\"#000000\" d=\"M29.2474,-86.9735C29.2474,-75.1918 29.2474,-59.5607 29.2474,-46.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-46.0033 29.2474,-36.0034 25.7475,-46.0034 32.7475,-46.0033\"/>\n<text text-anchor=\"middle\" x=\"109.7474\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">j ≥ 0 ∧ j &lt; cnt ∧ MEM[j] ≠ 0</text>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<graphviz.dot.Digraph at 0x110ca3e10>"
          },
          "execution_count": 40,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, invs = cfa_vc_gen(cfa1)\nres, answer = solve_horn(vc)\nres",
      "execution_count": 41,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unknown</b>",
            "text/plain": "<b>unknown</b>"
          },
          "execution_count": 41,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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."
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc, q3=True)\nres",
      "execution_count": 42,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 42,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(invs['L0'])",
      "execution_count": 43,
      "outputs": [
        {
          "data": {
            "text/html": "(&forall;sk!0 : cnt + -1&middot;sk!0 &le; 0 &or; MEM[sk!0] &le; 0 &or; &not;(sk!0 &ge; 0)) &and;\n(&forall;sk!0 : &not;(sk!0 &ge; 0) &or; MEM[sk!0] &ge; 0 &or; cnt + -1&middot;sk!0 &le; 0)",
            "text/plain": "(&forall;sk!0 : cnt + -1&middot;sk!0 &le; 0 &or; MEM[sk!0] &le; 0 &or; &not;(sk!0 &ge; 0)) &and;\n(&forall;sk!0 : &not;(sk!0 &ge; 0) &or; MEM[sk!0] &ge; 0 &or; cnt + -1&middot;sk!0 &le; 0)"
          },
          "execution_count": 43,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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$"
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Back to basics\n\nCHC 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."
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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\nGiven 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  \nNote 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"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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\nts1 = mk_ts1(safe=True)\nHtmlStr(ts1)",
      "execution_count": 44,
      "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": 44,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts1)\nres, answer = solve_horn(vc)\nres",
      "execution_count": 45,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unknown</b>",
            "text/plain": "<b>unknown</b>"
          },
          "execution_count": 45,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "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`."
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 46,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "a = ts1.get_pre_var('a')\nb = ts1.get_pre_var('b')\nvc, inv = vc_gen_pa(ts1, [b - a >= 13, a >= 0, b <= 2, b >= 213])",
      "execution_count": 47,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "chc_to_str(vc)",
      "execution_count": 48,
      "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": 48,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)\nres",
      "execution_count": 49,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 49,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(inv)",
      "execution_count": 50,
      "outputs": [
        {
          "data": {
            "text/html": "a &ge; 0 &and; &not;(b &le; 2) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &ge; 213)",
            "text/plain": "a &ge; 0 &and; &not;(b &le; 2) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &ge; 213)"
          },
          "execution_count": 50,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Term Abstraction\n\nPredicate abstraction requires the user to specify the exact predicates to be used in the solution.\nWe can relax this by requiring the user to only specify the terms that are allowed in the solution.\n\nPredicate 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"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 51,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "a, b, c = ts1.get_pre_vars('a b c')\nvc, inv = vc_gen_ta(ts1, [b-a, b])\nres, answer = solve_horn(vc, max_unfold=400)\nres",
      "execution_count": 52,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 52,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(inv)",
      "execution_count": 53,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(b + -1&middot;a &ge; 13) &and; &not;(b &le; 2) &and; a &ge; 0 &and; &not;(b &ge; 213)",
            "text/plain": "&not;(b + -1&middot;a &ge; 13) &and; &not;(b &le; 2) &and; a &ge; 0 &and; &not;(b &ge; 213)"
          },
          "execution_count": 53,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Invariant Partitioning\n\nAnother 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."
    },
    {
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 54,
      "outputs": []
    },
    {
      "metadata": {
        "scrolled": true,
        "trusted": false
      },
      "cell_type": "code",
      "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\nts2 = mk_ts2()\nHtmlStr(ts2)",
      "execution_count": 55,
      "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": 55,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts2)\nchc_to_str(vc)",
      "execution_count": 56,
      "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; Inv(a, b, c, d) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> Inv(a, b, c, 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/> Inv(a', b', c', d') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> Inv(a, b, c, d) &and; &not;(d &ge; 0) &rArr; 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; Inv(a, b, c, d) <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> Inv(a, b, c, 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/> Inv(a', b', c', d') <br/><br/>&forall;a, b, c, d, a', b', c', d' :<br/> Inv(a, b, c, d) &and; &not;(d &ge; 0) &rArr; False <br/><br/>\""
          },
          "execution_count": 56,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": 57,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unknown</b>",
            "text/plain": "'<b>unknown</b>'"
          },
          "execution_count": 57,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": false
      },
      "cell_type": "code",
      "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\nts2_bnd = mk_bnd(ts2, N=12)\nvc, inv = vc_gen(ts2_bnd)\nchc_to_str(vc)",
      "execution_count": 58,
      "outputs": [
        {
          "data": {
            "text/html": "&forall;a, b, c, d, bnd, a', b', c', d', bnd' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &and; bnd = 12 &rArr;<br/> Inv(a, b, c, d, bnd) <br/><br/>&forall;a, b, c, d, bnd, a', b', c', d', bnd' :<br/> Inv(a, b, c, d, bnd) &and;<br/> a' = 1 + a &and;<br/> b' = 1 + b + a &and;<br/> c' = 1 + c + b + a &and;<br/> d' = 1 + d + c + b + a &and;<br/> &not;(bnd &le; bnd') &and;<br/> bnd' &ge; 0 &rArr;<br/> Inv(a', b', c', d', bnd') <br/><br/>&forall;a, b, c, d, bnd, a', b', c', d', bnd' :<br/> Inv(a, b, c, d, bnd) &and; &not;(d &ge; 0) &rArr; False <br/><br/>",
            "text/plain": "\"&forall;a, b, c, d, bnd, a', b', c', d', bnd' :<br/> a = 0 &and; b = 0 &and; c = 0 &and; d = 0 &and; bnd = 12 &rArr;<br/> Inv(a, b, c, d, bnd) <br/><br/>&forall;a, b, c, d, bnd, a', b', c', d', bnd' :<br/> Inv(a, b, c, d, bnd) &and;<br/> a' = 1 + a &and;<br/> b' = 1 + b + a &and;<br/> c' = 1 + c + b + a &and;<br/> d' = 1 + d + c + b + a &and;<br/> &not;(bnd &le; bnd') &and;<br/> bnd' &ge; 0 &rArr;<br/> Inv(a', b', c', d', bnd') <br/><br/>&forall;a, b, c, d, bnd, a', b', c', d', bnd' :<br/> Inv(a, b, c, d, bnd) &and; &not;(d &ge; 0) &rArr; False <br/><br/>\""
          },
          "execution_count": 58,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc, max_unfold=20)\nres",
      "execution_count": 59,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 59,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(inv))",
      "execution_count": 60,
      "outputs": [
        {
          "data": {
            "text/html": "(&not;(bnd &ge; 2) &or; &not;(4&middot;a + 3&middot;b + 2&middot;c + d &le; -2)) &and;<br/>(&not;(bnd &ge; 5) &or; &not;(35&middot;a + 15&middot;b + 5&middot;c + d &le; -44)) &and;<br/>d &ge; 0 &and;<br/>(&not;(bnd &ge; 9) &or; &not;(165&middot;a + 45&middot;b + 9&middot;c + d &le; -466)) &and;<br/>(&not;(bnd &ge; 8) &or; &not;(120&middot;a + 36&middot;b + 8&middot;c + d &le; -301)) &and;<br/>(&not;(bnd &ge; 3) &or; &not;(10&middot;a + 6&middot;b + 3&middot;c + d &le; -6)) &and;<br/>(&not;(bnd &ge; 12) &or; &not;(364&middot;a + 78&middot;b + 12&middot;c + d &le; -1116)) &and;<br/>(&not;(bnd &ge; 4) &or; &not;(20&middot;a + 10&middot;b + 4&middot;c + d &le; -21)) &and;<br/>(&not;(bnd &ge; 11) &or; &not;(286&middot;a + 66&middot;b + 11&middot;c + d &le; -817)) &and;<br/>(bnd &le; 0 &or; a + b + c + d &ge; 0) &and;<br/>(&not;(bnd &ge; 6) &or; &not;(56&middot;a + 21&middot;b + 6&middot;c + d &le; -97)) &and;<br/>(&not;(bnd &ge; 10) &or; &not;(220&middot;a + 55&middot;b + 10&middot;c + d &le; -631)) &and;<br/>(&not;(bnd &ge; 7) &or; &not;(84&middot;a + 28&middot;b + 7&middot;c + d &le; -181)) &and;<br/>&not;(bnd &ge; 13)",
            "text/plain": "'(&not;(bnd &ge; 2) &or; &not;(4&middot;a + 3&middot;b + 2&middot;c + d &le; -2)) &and;<br/>(&not;(bnd &ge; 5) &or; &not;(35&middot;a + 15&middot;b + 5&middot;c + d &le; -44)) &and;<br/>d &ge; 0 &and;<br/>(&not;(bnd &ge; 9) &or; &not;(165&middot;a + 45&middot;b + 9&middot;c + d &le; -466)) &and;<br/>(&not;(bnd &ge; 8) &or; &not;(120&middot;a + 36&middot;b + 8&middot;c + d &le; -301)) &and;<br/>(&not;(bnd &ge; 3) &or; &not;(10&middot;a + 6&middot;b + 3&middot;c + d &le; -6)) &and;<br/>(&not;(bnd &ge; 12) &or; &not;(364&middot;a + 78&middot;b + 12&middot;c + d &le; -1116)) &and;<br/>(&not;(bnd &ge; 4) &or; &not;(20&middot;a + 10&middot;b + 4&middot;c + d &le; -21)) &and;<br/>(&not;(bnd &ge; 11) &or; &not;(286&middot;a + 66&middot;b + 11&middot;c + d &le; -817)) &and;<br/>(bnd &le; 0 &or; a + b + c + d &ge; 0) &and;<br/>(&not;(bnd &ge; 6) &or; &not;(56&middot;a + 21&middot;b + 6&middot;c + d &le; -97)) &and;<br/>(&not;(bnd &ge; 10) &or; &not;(220&middot;a + 55&middot;b + 10&middot;c + d &le; -631)) &and;<br/>(&not;(bnd &ge; 7) &or; &not;(84&middot;a + 28&middot;b + 7&middot;c + d &le; -181)) &and;<br/>&not;(bnd &ge; 13)'"
          },
          "execution_count": 60,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "The solver is stuck trying to find a monolithic solution that converges to an invariant in non-linear arithmetic!\nWe can guide it by partitioning the invariants to individual state variables:"
    },
    {
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": false
      },
      "cell_type": "code",
      "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\na, b, c, d = ts2.get_pre_vars('a b c d')\nvc, inv = vc_gen_part(ts2, { \"a\":[a], \"b\":[b], \"c\":[c], \"d\":[d] })\nres, answer = solve_horn(vc)\nres",
      "execution_count": 61,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 61,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "inv",
      "execution_count": 62,
      "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": 62,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(inv)",
      "execution_count": 63,
      "outputs": [
        {
          "data": {
            "text/html": "a &ge; 0 &and; b &ge; 0 &and; c &ge; 0 &and; d &ge; 0",
            "text/plain": "a &ge; 0 &and; b &ge; 0 &and; c &ge; 0 &and; d &ge; 0"
          },
          "execution_count": 63,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen_part(ts2, { \"ac\":[a, c], \"bc\":[b, c], \"d\":[d] })\nres, answer = solve_horn(vc)\nanswer.eval(inv)",
      "execution_count": 64,
      "outputs": [
        {
          "data": {
            "text/html": "a &ge; 0 &and; &not;(a + c &le; -2) &and; b &ge; 0 &and; d &ge; 0",
            "text/plain": "a &ge; 0 &and; &not;(a + c &le; -2) &and; b &ge; 0 &and; d &ge; 0"
          },
          "execution_count": 64,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "chc_to_str(vc)",
      "execution_count": 65,
      "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": 65,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Combining Data Flow and Control Flow\n\nOur examples so far modeled the control flow of the transition system. Alternatively,\nwe can model the data flow, and even combine the two together.\n\nTo 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  \nUsing $pack$ and $unpack$ we can model data flow (or, even weak memory updates)"
    },
    {
      "metadata": {
        "code_folding": [
          0,
          43,
          51
        ],
        "trusted": false
      },
      "cell_type": "code",
      "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        \nclass 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\nclass 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 + ')'",
      "execution_count": 66,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 67,
      "outputs": []
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "In `dcfa0`, the loop at `L1` hides the dataflow of variable `x` from `L0` to `L2`"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "dcfa0 = mk_dcfa0()\ndcfa0.to_dot()",
      "execution_count": 68,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"248pt\" height=\"392pt\"\n viewBox=\"0.00 0.00 248.25 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-388 244.2474,-388 244.2474,4 -4,4\"/>\n<!-- entry -->\n<g id=\"node1\" class=\"node\">\n<title>entry</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-366\" rx=\"29.4969\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">entry</text>\n</g>\n<!-- L0 -->\n<g id=\"node4\" class=\"node\">\n<title>L0</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-279\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-347.9735C29.2474,-336.1918 29.2474,-320.5607 29.2474,-307.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-307.0033 29.2474,-297.0034 25.7475,-307.0034 32.7475,-307.0033\"/>\n<text text-anchor=\"middle\" x=\"48.7474\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x&#39; = 10</text>\n</g>\n<!-- L2 -->\n<g id=\"node2\" class=\"node\">\n<title>L2</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L2</text>\n</g>\n<!-- exit -->\n<g id=\"node5\" class=\"node\">\n<title>exit</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-86.9735C29.2474,-75.1918 29.2474,-59.5607 29.2474,-46.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-46.0033 29.2474,-36.0034 25.7475,-46.0034 32.7475,-46.0033\"/>\n<text text-anchor=\"middle\" x=\"47.2474\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x &gt; 10</text>\n</g>\n<!-- L1 -->\n<g id=\"node3\" class=\"node\">\n<title>L1</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-192\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-173.9735C29.2474,-162.1918 29.2474,-146.5607 29.2474,-133.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-133.0033 29.2474,-123.0034 25.7475,-133.0034 32.7475,-133.0033\"/>\n<text text-anchor=\"middle\" x=\"77.7474\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M53.7799,-199.752C64.7552,-200.4902 74.2474,-197.9063 74.2474,-192 74.2474,-188.0317 69.9625,-185.5632 63.8217,-184.5944\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"63.8946,-181.0949 53.7799,-184.248 63.6533,-188.0908 63.8946,-181.0949\"/>\n<text text-anchor=\"middle\" x=\"157.2474\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-260.9735C29.2474,-249.1918 29.2474,-233.5607 29.2474,-220.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-220.0033 29.2474,-210.0034 25.7475,-220.0034 32.7475,-220.0033\"/>\n<text text-anchor=\"middle\" x=\"68.7474\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">y&#39; = 0 ∧ x&#39; = x</text>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<graphviz.dot.Digraph at 0x114941d10>"
          },
          "execution_count": 68,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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\ndcfa1 = mk_dcfa1()\ndcfa1.to_dot()",
      "execution_count": 69,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"248pt\" height=\"566pt\"\n viewBox=\"0.00 0.00 248.25 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-562 244.2474,-562 244.2474,4 -4,4\"/>\n<!-- UP -->\n<g id=\"node1\" class=\"node\">\n<title>UP</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">UP</text>\n</g>\n<!-- exit -->\n<g id=\"node6\" class=\"node\">\n<title>exit</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-86.9735C29.2474,-75.1918 29.2474,-59.5607 29.2474,-46.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-46.0033 29.2474,-36.0034 25.7475,-46.0034 32.7475,-46.0033\"/>\n<text text-anchor=\"middle\" x=\"47.2474\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x &gt; 10</text>\n</g>\n<!-- entry -->\n<g id=\"node2\" class=\"node\">\n<title>entry</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-540\" rx=\"29.4969\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">entry</text>\n</g>\n<!-- L0 -->\n<g id=\"node5\" class=\"node\">\n<title>L0</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-453\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-521.9735C29.2474,-510.1918 29.2474,-494.5607 29.2474,-481.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-481.0033 29.2474,-471.0034 25.7475,-481.0034 32.7475,-481.0033\"/>\n<text text-anchor=\"middle\" x=\"48.7474\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x&#39; = 10</text>\n</g>\n<!-- L2 -->\n<g id=\"node3\" class=\"node\">\n<title>L2</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-192\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-173.9735C29.2474,-162.1918 29.2474,-146.5607 29.2474,-133.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-133.0033 29.2474,-123.0034 25.7475,-133.0034 32.7475,-133.0033\"/>\n<text text-anchor=\"middle\" x=\"67.2474\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">unpack(x:=p)</text>\n</g>\n<!-- L1 -->\n<g id=\"node4\" class=\"node\">\n<title>L1</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-279\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-260.9735C29.2474,-249.1918 29.2474,-233.5607 29.2474,-220.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-220.0033 29.2474,-210.0034 25.7475,-220.0034 32.7475,-220.0033\"/>\n<text text-anchor=\"middle\" x=\"77.7474\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M53.7799,-286.752C64.7552,-287.4902 74.2474,-284.9063 74.2474,-279 74.2474,-275.0317 69.9625,-272.5632 63.8217,-271.5944\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"63.8946,-268.0949 53.7799,-271.248 63.6533,-275.0908 63.8946,-268.0949\"/>\n<text text-anchor=\"middle\" x=\"157.2474\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">y &lt; 2019 ∧ y&#39; = y + 1 ∧ x&#39; = x</text>\n</g>\n<!-- P -->\n<g id=\"node7\" class=\"node\">\n<title>P</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-366\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-434.9735C29.2474,-423.1918 29.2474,-407.5607 29.2474,-394.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-394.0033 29.2474,-384.0034 25.7475,-394.0034 32.7475,-394.0033\"/>\n<text text-anchor=\"middle\" x=\"60.2474\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">pack(p:=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=\"#000000\" d=\"M29.2474,-347.9735C29.2474,-336.1918 29.2474,-320.5607 29.2474,-307.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-307.0033 29.2474,-297.0034 25.7475,-307.0034 32.7475,-307.0033\"/>\n<text text-anchor=\"middle\" x=\"68.7474\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">y&#39; = 0 ∧ x&#39; = x</text>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<graphviz.dot.Digraph at 0x11490e450>"
          },
          "execution_count": 69,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": false
      },
      "cell_type": "code",
      "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",
      "execution_count": 70,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "",
      "execution_count": null,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, invs, pack = dcfa_vc_gen(dcfa1)\nres, answer = solve_horn(vc, max_unfold=40)\nres",
      "execution_count": 71,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 71,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "chc_to_str(vc)",
      "execution_count": 72,
      "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": 72,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer.eval(pack)",
      "execution_count": 73,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(p &ge; 11)",
            "text/plain": "&not;(p &ge; 11)"
          },
          "execution_count": 73,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer",
      "execution_count": 74,
      "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": 74,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "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\ndcfa2 = mk_dcfa2()\ndcfa2.to_dot()",
      "execution_count": 75,
      "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 2.40.1 (20161225.0304)\n -->\n<!-- Title: %3 Pages: 1 -->\n<svg width=\"225pt\" height=\"566pt\"\n viewBox=\"0.00 0.00 225.25 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<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-562 221.2474,-562 221.2474,4 -4,4\"/>\n<!-- UP -->\n<g id=\"node1\" class=\"node\">\n<title>UP</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-105\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">UP</text>\n</g>\n<!-- exit -->\n<g id=\"node6\" class=\"node\">\n<title>exit</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-18\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-86.9735C29.2474,-75.1918 29.2474,-59.5607 29.2474,-46.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-46.0033 29.2474,-36.0034 25.7475,-46.0034 32.7475,-46.0033\"/>\n<text text-anchor=\"middle\" x=\"47.2474\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x &gt; 10</text>\n</g>\n<!-- entry -->\n<g id=\"node2\" class=\"node\">\n<title>entry</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-540\" rx=\"29.4969\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">entry</text>\n</g>\n<!-- L0 -->\n<g id=\"node5\" class=\"node\">\n<title>L0</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-453\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-521.9735C29.2474,-510.1918 29.2474,-494.5607 29.2474,-481.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-481.0033 29.2474,-471.0034 25.7475,-481.0034 32.7475,-481.0033\"/>\n<text text-anchor=\"middle\" x=\"48.7474\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">x&#39; = 11</text>\n</g>\n<!-- L2 -->\n<g id=\"node3\" class=\"node\">\n<title>L2</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-192\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-173.9735C29.2474,-162.1918 29.2474,-146.5607 29.2474,-133.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-133.0033 29.2474,-123.0034 25.7475,-133.0034 32.7475,-133.0033\"/>\n<text text-anchor=\"middle\" x=\"67.2474\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">unpack(x:=p)</text>\n</g>\n<!-- L1 -->\n<g id=\"node4\" class=\"node\">\n<title>L1</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-279\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-260.9735C29.2474,-249.1918 29.2474,-233.5607 29.2474,-220.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-220.0033 29.2474,-210.0034 25.7475,-220.0034 32.7475,-220.0033\"/>\n<text text-anchor=\"middle\" x=\"67.7474\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M53.7799,-286.752C64.7552,-287.4902 74.2474,-284.9063 74.2474,-279 74.2474,-275.0317 69.9625,-272.5632 63.8217,-271.5944\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"63.8946,-268.0949 53.7799,-271.248 63.6533,-275.0908 63.8946,-268.0949\"/>\n<text text-anchor=\"middle\" x=\"145.7474\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">True ∧ y&#39; = y + 1 ∧ x&#39; = x</text>\n</g>\n<!-- P -->\n<g id=\"node7\" class=\"node\">\n<title>P</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"29.2474\" cy=\"-366\" rx=\"27\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"29.2474\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">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=\"#000000\" d=\"M29.2474,-434.9735C29.2474,-423.1918 29.2474,-407.5607 29.2474,-394.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-394.0033 29.2474,-384.0034 25.7475,-394.0034 32.7475,-394.0033\"/>\n<text text-anchor=\"middle\" x=\"60.2474\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">pack(p:=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=\"#000000\" d=\"M29.2474,-347.9735C29.2474,-336.1918 29.2474,-320.5607 29.2474,-307.1581\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"32.7475,-307.0033 29.2474,-297.0034 25.7475,-307.0034 32.7475,-307.0033\"/>\n<text text-anchor=\"middle\" x=\"68.7474\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">y&#39; = 0 ∧ x&#39; = x</text>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<graphviz.dot.Digraph at 0x114924050>"
          },
          "execution_count": 75,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, invs, pack = dcfa_vc_gen(dcfa2)\nres, answer = solve_horn(vc, max_unfold=40)\nres",
      "execution_count": 76,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 76,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "answer",
      "execution_count": 77,
      "outputs": [
        {
          "data": {
            "text/html": "[Pack = [else &rarr; True],\n L0 = [else &rarr; &#957;<sub>0</sub> = 11],\n entry = [else &rarr; True],\n exit = [else &rarr; False],\n L2 = [else &rarr; False],\n UP = [else &rarr; False],\n L1 = [else &rarr; True],\n P = [else &rarr; True]]",
            "text/plain": "[Pack = [else &rarr; True],\n L0 = [else &rarr; &#957;<sub>0</sub> = 11],\n entry = [else &rarr; True],\n exit = [else &rarr; False],\n L2 = [else &rarr; False],\n UP = [else &rarr; False],\n L1 = [else &rarr; True],\n P = [else &rarr; True]]"
          },
          "execution_count": 77,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Conclusion\n\nThis is the end of the interactive portion of the tutorial"
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "# Additional Examples"
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "def mk_ts_add():\n    T = Ts('Add')\n    x, x_out = T.add_var(z3.IntSort(), name='x')\n    y, y_out = T.add_var(z3.IntSort(), name='y')\n    z, z_out = T.add_var(z3.IntSort(), name='z')\n    i, i_out = T.add_var(z3.IntSort(), name='i')\n    T.Init = z3.And(z == x, i == 0, y > 0)\n    T.Tr = z3.And(i < y, z_out == z + 1, i_out == i + 1, x == x_out, y == y_out)\n    T.Bad = z3.And(i >= y, z3.Not(z == x + y))\n    return T\nts_add = mk_ts_add()\nHtmlStr(ts_add)",
      "execution_count": 78,
      "outputs": [
        {
          "data": {
            "text/html": "Transition System: Add<br/>\tInit: z = x &and; i = 0 &and; y &gt; 0<br/>\tBad: i &ge; y &and; &not;(z = x + y)<br/>\tTr: i &lt; y &and; z' = z + 1 &and; i' = i + 1 &and; x = x' &and; y = y'",
            "text/plain": "\"Transition System: Add<br/>\\tInit: z = x &and; i = 0 &and; y &gt; 0<br/>\\tBad: i &ge; y &and; &not;(z = x + y)<br/>\\tTr: i &lt; y &and; z' = z + 1 &and; i' = i + 1 &and; x = x' &and; y = y'\""
          },
          "execution_count": 78,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts_add)\nchc_to_str(vc)",
      "execution_count": 79,
      "outputs": [
        {
          "data": {
            "text/html": "&forall;x, y, z, i, x', y', z', i' :<br/> z = x &and; i = 0 &and; y &gt; 0 &rArr; Inv(x, y, z, i) <br/><br/>&forall;x, y, z, i, x', y', z', i' :<br/> Inv(x, y, z, i) &and;<br/> i &lt; y &and;<br/> z' = z + 1 &and;<br/> i' = i + 1 &and;<br/> x = x' &and;<br/> y = y' &rArr;<br/> Inv(x', y', z', i') <br/><br/>&forall;x, y, z, i, x', y', z', i' :<br/> Inv(x, y, z, i) &and; i &ge; y &and; &not;(z = x + y) &rArr; False <br/><br/>",
            "text/plain": "\"&forall;x, y, z, i, x', y', z', i' :<br/> z = x &and; i = 0 &and; y &gt; 0 &rArr; Inv(x, y, z, i) <br/><br/>&forall;x, y, z, i, x', y', z', i' :<br/> Inv(x, y, z, i) &and;<br/> i &lt; y &and;<br/> z' = z + 1 &and;<br/> i' = i + 1 &and;<br/> x = x' &and;<br/> y = y' &rArr;<br/> Inv(x', y', z', i') <br/><br/>&forall;x, y, z, i, x', y', z', i' :<br/> Inv(x, y, z, i) &and; i &ge; y &and; &not;(z = x + y) &rArr; False <br/><br/>\""
          },
          "execution_count": 79,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)",
      "execution_count": 80,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "res",
      "execution_count": 81,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "<b>sat</b>"
          },
          "execution_count": 81,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "horn_inv = answer.eval(inv)\nhorn_inv",
      "execution_count": 82,
      "outputs": [
        {
          "data": {
            "text/html": "z + -1&middot;x + -1&middot;i &le; 0 &and; x + i + -1&middot;z &le; 0 &and; z + -1&middot;x + -1&middot;y &le; 0",
            "text/plain": "z + -1&middot;x + -1&middot;i &le; 0 &and; x + i + -1&middot;z &le; 0 &and; z + -1&middot;x + -1&middot;y &le; 0"
          },
          "execution_count": 82,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "x, y, z, i = ts_add.get_pre_vars('x y z i')",
      "execution_count": 83,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "human = z3.And(z == x + i, i <= y  )\ndef Iff(a, b):\n    return z3.And(z3.Implies(a, b), z3.Implies(b, a))\ns = z3.Solver()\ns.add(z3.Not(Iff(horn_inv, human)))\nres = s.check()\nif res == z3.sat:\n    print('Not equal')\n    print(s.model())\nelif res == z3.unsat:\n    display(HTML('<h2>Human readable</h2>'))\n    display(human)",
      "execution_count": 84,
      "outputs": [
        {
          "data": {
            "text/html": "<h2>Human readable</h2>",
            "text/plain": "<IPython.core.display.HTML object>"
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "data": {
            "text/html": "z = x + i &and; i &le; y",
            "text/plain": "z = x + i &and; i &le; y"
          },
          "metadata": {},
          "output_type": "display_data"
        }
      ]
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "",
      "execution_count": null,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": false
      },
      "cell_type": "code",
      "source": "",
      "execution_count": null,
      "outputs": []
    }
  ],
  "metadata": {
    "kernelspec": {
      "name": "python36",
      "display_name": "Python 3.6",
      "language": "python"
    },
    "language_info": {
      "mimetype": "text/x-python",
      "nbconvert_exporter": "python",
      "name": "python",
      "pygments_lexer": "ipython3",
      "version": "3.6.6",
      "file_extension": ".py",
      "codemirror_mode": {
        "version": 3,
        "name": "ipython"
      }
    }
  },
  "nbformat": 4,
  "nbformat_minor": 2
}