Synasc2019.ipynb

{
  "cells": [
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "# Spacer Tutorial\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 `Synasc2019.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": [
          3,
          16,
          22,
          31,
          38
        ],
        "trusted": true
      },
      "cell_type": "code",
      "source": "import 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": 1,
      "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  \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,
          6,
          11,
          14
        ],
        "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    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": 163,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(itp)",
      "execution_count": 164,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(a + -1&middot;b &ge; -1)",
            "text/plain": "'&not;(a + -1&middot;b &ge; -1)'"
          },
          "execution_count": 164,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "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,
          35,
          36,
          48,
          72,
          76,
          82,
          85,
          91,
          96,
          98,
          100,
          102,
          104,
          106,
          108,
          120,
          125,
          127,
          135,
          137,
          140,
          145
        ],
        "trusted": true
      },
      "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    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    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    def get_var_name(self, idx):\n        if idx < len(self._var_names):\n            return self._var_names[idx]\n        return None\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    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    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    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    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 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    def _mk_input_name(self, idx):\n        return 'i_' + str(idx)\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    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    def __str__(self):\n        return repr(self)",
      "execution_count": 53,
      "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": true
      },
      "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": 165,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=True)\nHtmlStr(ts0)",
      "execution_count": 166,
      "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": 166,
          "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": true
      },
      "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": 167,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts0)",
      "execution_count": 168,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "chc_to_str(vc)",
      "execution_count": 169,
      "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": 169,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(inv)",
      "execution_count": 170,
      "outputs": [
        {
          "data": {
            "text/html": "Inv(x)",
            "text/plain": "'Inv(x)'"
          },
          "execution_count": 170,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)",
      "execution_count": 171,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(res)",
      "execution_count": 172,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "'<b>sat</b>'"
          },
          "execution_count": 172,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer)",
      "execution_count": 173,
      "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": 173,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(inv))",
      "execution_count": 174,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &ge; 6)",
            "text/plain": "'&not;(x &ge; 6)'"
          },
          "execution_count": 174,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=False)\nHtmlStr(ts0)",
      "execution_count": 175,
      "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": 175,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts0)\nres, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": 176,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unsat</b>",
            "text/plain": "'<b>unsat</b>'"
          },
          "execution_count": 176,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer)",
      "execution_count": 177,
      "outputs": [
        {
          "data": {
            "text/html": "hyper-res(asserted(&forall;A : Inv(A) &and; A &ge; 4 &rArr; query!2600(A)),<br/>          hyper-res(asserted(&forall;A, B :<br/>                              Inv(A) &and; &not;(5 &le; A) &and; B = 1 + A &rArr;<br/>                              Inv(B)),<br/>                    hyper-res(asserted(&forall;A, B :<br/>                                        Inv(A) &and;<br/>                                        &not;(5 &le; A) &and;<br/>                                        B = 1 + A &rArr;<br/>                                        Inv(B)),<br/>                              hyper-res(asserted(&forall;A, B :<br/>                                        Inv(A) &and;<br/>                                        &not;(5 &le; A) &and;<br/>                                        B = 1 + A &rArr;<br/>                                        Inv(B)),<br/>                                        hyper-res(asserted(&forall;A,<br/>                                        B :<br/>                                        Inv(A) &and;<br/>                                        &not;(5 &le; A) &and;<br/>                                        B = 1 + A &rArr;<br/>                                        Inv(B)),<br/>                                        hyper-res(asserted(&forall;A :<br/>                                        A &le; 0 &rArr; Inv(A)),<br/>                                        Inv(0)),<br/>                                        Inv(1)),<br/>                                        Inv(2)),<br/>                              Inv(3)),<br/>                    Inv(4)),<br/>          query!2600(4))",
            "text/plain": "'hyper-res(asserted(&forall;A : Inv(A) &and; A &ge; 4 &rArr; query!2600(A)),<br/>          hyper-res(asserted(&forall;A, B :<br/>                              Inv(A) &and; &not;(5 &le; A) &and; B = 1 + A &rArr;<br/>                              Inv(B)),<br/>                    hyper-res(asserted(&forall;A, B :<br/>                                        Inv(A) &and;<br/>                                        &not;(5 &le; A) &and;<br/>                                        B = 1 + A &rArr;<br/>                                        Inv(B)),<br/>                              hyper-res(asserted(&forall;A, B :<br/>                                        Inv(A) &and;<br/>                                        &not;(5 &le; A) &and;<br/>                                        B = 1 + A &rArr;<br/>                                        Inv(B)),<br/>                                        hyper-res(asserted(&forall;A,<br/>                                        B :<br/>                                        Inv(A) &and;<br/>                                        &not;(5 &le; A) &and;<br/>                                        B = 1 + A &rArr;<br/>                                        Inv(B)),<br/>                                        hyper-res(asserted(&forall;A :<br/>                                        A &le; 0 &rArr; Inv(A)),<br/>                                        Inv(0)),<br/>                                        Inv(1)),<br/>                                        Inv(2)),<br/>                              Inv(3)),<br/>                    Inv(4)),<br/>          query!2600(4))'"
          },
          "execution_count": 177,
          "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": true
      },
      "cell_type": "code",
      "source": "SpacerProof(answer)",
      "execution_count": 67,
      "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=\"404pt\"\n viewBox=\"0.00 0.00 124.99 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 120.9896,-400 120.9896,4 -4,4\"/>\n<!-- 2746 -->\n<g id=\"node1\" class=\"node\">\n<title>2746</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!201(4)</text>\n</g>\n<!-- 2123 -->\n<g id=\"node2\" class=\"node\">\n<title>2123</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-90\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(4)</text>\n</g>\n<!-- 2123&#45;&gt;2746 -->\n<g id=\"edge5\" class=\"edge\">\n<title>2123&#45;&gt;2746</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<!-- 2249 -->\n<g id=\"node3\" class=\"node\">\n<title>2249</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-162\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(3)</text>\n</g>\n<!-- 2249&#45;&gt;2123 -->\n<g id=\"edge4\" class=\"edge\">\n<title>2249&#45;&gt;2123</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<!-- 2231 -->\n<g id=\"node4\" class=\"node\">\n<title>2231</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-234\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(2)</text>\n</g>\n<!-- 2231&#45;&gt;2249 -->\n<g id=\"edge3\" class=\"edge\">\n<title>2231&#45;&gt;2249</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<!-- 2185 -->\n<g id=\"node5\" class=\"node\">\n<title>2185</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-306\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(1)</text>\n</g>\n<!-- 2185&#45;&gt;2231 -->\n<g id=\"edge2\" class=\"edge\">\n<title>2185&#45;&gt;2231</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<!-- 2169 -->\n<g id=\"node6\" class=\"node\">\n<title>2169</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"58.4948\" cy=\"-378\" rx=\"33.2948\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"58.4948\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">Inv(0)</text>\n</g>\n<!-- 2169&#45;&gt;2185 -->\n<g id=\"edge1\" class=\"edge\">\n<title>2169&#45;&gt;2185</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</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x104e16350>"
          },
          "execution_count": 67,
          "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": true
      },
      "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": 178,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=True)\nvc, inv = vc_gen_bwd(ts0)\nchc_to_str(vc)",
      "execution_count": 179,
      "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": 179,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)\nHtmlStr(answer.eval(inv))",
      "execution_count": 180,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &le; 9)",
            "text/plain": "'&not;(x &le; 9)'"
          },
          "execution_count": 180,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=False)\nvc, inv = vc_gen_bwd(ts0)\nres, answer = solve_horn(vc)\nSpacerProof(answer)",
      "execution_count": 181,
      "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=\"134pt\" height=\"404pt\"\n viewBox=\"0.00 0.00 134.09 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 130.0888,-400 130.0888,4 -4,4\"/>\n<!-- 71163 -->\n<g id=\"node1\" class=\"node\">\n<title>71163</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-18\" rx=\"63.0888\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">query!2648(0)</text>\n</g>\n<!-- 430 -->\n<g id=\"node2\" class=\"node\">\n<title>430</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-90\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(0)</text>\n</g>\n<!-- 430&#45;&gt;71163 -->\n<g id=\"edge5\" class=\"edge\">\n<title>430&#45;&gt;71163</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-71.8314C63.0444,-64.131 63.0444,-54.9743 63.0444,-46.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-46.4132 63.0444,-36.4133 59.5445,-46.4133 66.5445,-46.4132\"/>\n</g>\n<!-- 1183 -->\n<g id=\"node3\" class=\"node\">\n<title>1183</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-162\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(1)</text>\n</g>\n<!-- 1183&#45;&gt;430 -->\n<g id=\"edge4\" class=\"edge\">\n<title>1183&#45;&gt;430</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-143.8314C63.0444,-136.131 63.0444,-126.9743 63.0444,-118.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-118.4132 63.0444,-108.4133 59.5445,-118.4133 66.5445,-118.4132\"/>\n</g>\n<!-- 1198 -->\n<g id=\"node4\" class=\"node\">\n<title>1198</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-234\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(2)</text>\n</g>\n<!-- 1198&#45;&gt;1183 -->\n<g id=\"edge3\" class=\"edge\">\n<title>1198&#45;&gt;1183</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-215.8314C63.0444,-208.131 63.0444,-198.9743 63.0444,-190.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-190.4132 63.0444,-180.4133 59.5445,-190.4133 66.5445,-190.4132\"/>\n</g>\n<!-- 1115 -->\n<g id=\"node5\" class=\"node\">\n<title>1115</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-306\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(3)</text>\n</g>\n<!-- 1115&#45;&gt;1198 -->\n<g id=\"edge2\" class=\"edge\">\n<title>1115&#45;&gt;1198</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-287.8314C63.0444,-280.131 63.0444,-270.9743 63.0444,-262.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-262.4132 63.0444,-252.4133 59.5445,-262.4133 66.5445,-262.4132\"/>\n</g>\n<!-- 255 -->\n<g id=\"node6\" class=\"node\">\n<title>255</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-378\" rx=\"50.8918\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">BwdInv(4)</text>\n</g>\n<!-- 255&#45;&gt;1115 -->\n<g id=\"edge1\" class=\"edge\">\n<title>255&#45;&gt;1115</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-359.8314C63.0444,-352.131 63.0444,-342.9743 63.0444,-334.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-334.4132 63.0444,-324.4133 59.5445,-334.4133 66.5445,-334.4132\"/>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x10515a550>"
          },
          "execution_count": 181,
          "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": true
      },
      "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": 71,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=True)\nvc, inv = vc_gen_2ind(ts0)\nchc_to_str(vc)",
      "execution_count": 182,
      "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": 182,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)\nHtmlStr(answer.eval(inv))",
      "execution_count": 183,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &ge; 6)",
            "text/plain": "'&not;(x &ge; 6)'"
          },
          "execution_count": 183,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "ts0 = mk_ts0(safe=False)\nvc, inv = vc_gen_2ind(ts0)\nres, answer = solve_horn(vc)\nSpacerProof(answer)",
      "execution_count": 184,
      "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=\"548pt\"\n viewBox=\"0.00 0.00 189.89 548.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 544)\">\n<title>%3</title>\n<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-544 185.8927,-544 185.8927,4 -4,4\"/>\n<!-- 37561 -->\n<g id=\"node1\" class=\"node\">\n<title>37561</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"76.9464\" cy=\"-18\" rx=\"63.0888\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"76.9464\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">query!2678(4)</text>\n</g>\n<!-- 3423 -->\n<g id=\"node2\" class=\"node\">\n<title>3423</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"76.9464\" cy=\"-90\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"76.9464\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(4)</text>\n</g>\n<!-- 3423&#45;&gt;37561 -->\n<g id=\"edge13\" class=\"edge\">\n<title>3423&#45;&gt;37561</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M76.9464,-71.8314C76.9464,-64.131 76.9464,-54.9743 76.9464,-46.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"80.4465,-46.4132 76.9464,-36.4133 73.4465,-46.4133 80.4465,-46.4132\"/>\n</g>\n<!-- 3711 -->\n<g id=\"node3\" class=\"node\">\n<title>3711</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"109.9464\" cy=\"-162\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"109.9464\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(3)</text>\n</g>\n<!-- 3711&#45;&gt;3423 -->\n<g id=\"edge11\" class=\"edge\">\n<title>3711&#45;&gt;3423</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M101.7891,-144.2022C97.9927,-135.9192 93.3966,-125.8915 89.1952,-116.7248\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"92.3582,-115.2254 85.0098,-107.593 85.9947,-118.142 92.3582,-115.2254\"/>\n</g>\n<!-- 3713 -->\n<g id=\"node4\" class=\"node\">\n<title>3713</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"43.9464\" cy=\"-234\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"43.9464\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(2)</text>\n</g>\n<!-- 3713&#45;&gt;3423 -->\n<g id=\"edge12\" class=\"edge\">\n<title>3713&#45;&gt;3423</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M47.4916,-216.0168C51.1396,-197.8111 57.0998,-168.8731 62.9464,-144 64.963,-135.4205 67.315,-126.1172 69.509,-117.6887\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"72.9118,-118.5108 72.0738,-107.9491 66.1426,-116.7281 72.9118,-118.5108\"/>\n</g>\n<!-- 3713&#45;&gt;3711 -->\n<g id=\"edge9\" class=\"edge\">\n<title>3713&#45;&gt;3711</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M59.254,-217.3008C67.7506,-208.0317 78.4689,-196.339 87.8589,-186.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"90.5445,-188.3453 94.7218,-178.6087 85.3844,-183.6152 90.5445,-188.3453\"/>\n</g>\n<!-- 3655 -->\n<g id=\"node5\" class=\"node\">\n<title>3655</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"109.9464\" cy=\"-306\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"109.9464\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(1)</text>\n</g>\n<!-- 3655&#45;&gt;3711 -->\n<g id=\"edge10\" class=\"edge\">\n<title>3655&#45;&gt;3711</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M109.9464,-287.7623C109.9464,-263.201 109.9464,-219.2474 109.9464,-190.3541\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"113.4465,-190.0896 109.9464,-180.0896 106.4465,-190.0897 113.4465,-190.0896\"/>\n</g>\n<!-- 3655&#45;&gt;3713 -->\n<g id=\"edge7\" class=\"edge\">\n<title>3655&#45;&gt;3713</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M94.6387,-289.3008C86.1421,-280.0317 75.4238,-268.339 66.0338,-258.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"68.5083,-255.6152 59.171,-250.6087 63.3482,-260.3453 68.5083,-255.6152\"/>\n</g>\n<!-- 3708 -->\n<g id=\"node6\" class=\"node\">\n<title>3708</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"43.9464\" cy=\"-378\" rx=\"37.8943\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"43.9464\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(0)</text>\n</g>\n<!-- 3708&#45;&gt;3713 -->\n<g id=\"edge8\" class=\"edge\">\n<title>3708&#45;&gt;3713</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M43.9464,-359.7623C43.9464,-335.201 43.9464,-291.2474 43.9464,-262.3541\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"47.4465,-262.0896 43.9464,-252.0896 40.4465,-262.0897 47.4465,-262.0896\"/>\n</g>\n<!-- 3708&#45;&gt;3655 -->\n<g id=\"edge5\" class=\"edge\">\n<title>3708&#45;&gt;3655</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M59.254,-361.3008C67.7506,-352.0317 78.4689,-340.339 87.8589,-330.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"90.5445,-332.3453 94.7218,-322.6087 85.3844,-327.6152 90.5445,-332.3453\"/>\n</g>\n<!-- 3491 -->\n<g id=\"node7\" class=\"node\">\n<title>3491</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"109.9464\" cy=\"-450\" rx=\"40.8928\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"109.9464\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(&#45;1)</text>\n</g>\n<!-- 3491&#45;&gt;3655 -->\n<g id=\"edge6\" class=\"edge\">\n<title>3491&#45;&gt;3655</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M109.9464,-431.7623C109.9464,-407.201 109.9464,-363.2474 109.9464,-334.3541\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"113.4465,-334.0896 109.9464,-324.0896 106.4465,-334.0897 113.4465,-334.0896\"/>\n</g>\n<!-- 3491&#45;&gt;3708 -->\n<g id=\"edge3\" class=\"edge\">\n<title>3491&#45;&gt;3708</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M94.6387,-433.3008C86.1421,-424.0317 75.4238,-412.339 66.0338,-402.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"68.5083,-399.6152 59.171,-394.6087 63.3482,-404.3453 68.5083,-399.6152\"/>\n</g>\n<!-- 3502 -->\n<g id=\"node8\" class=\"node\">\n<title>3502</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"40.9464\" cy=\"-522\" rx=\"40.8928\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"40.9464\" y=\"-518.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(&#45;2)</text>\n</g>\n<!-- 3502&#45;&gt;3708 -->\n<g id=\"edge4\" class=\"edge\">\n<title>3502&#45;&gt;3708</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M41.3263,-503.7623C41.838,-479.201 42.7537,-435.2474 43.3557,-406.3541\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"46.8604,-406.1604 43.5695,-396.0896 39.8619,-406.0145 46.8604,-406.1604\"/>\n</g>\n<!-- 3502&#45;&gt;3491 -->\n<g id=\"edge1\" class=\"edge\">\n<title>3502&#45;&gt;3491</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M56.9498,-505.3008C65.8326,-496.0317 77.0381,-484.339 86.8549,-474.0954\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"89.6376,-476.2502 94.0297,-466.6087 84.5837,-471.4069 89.6376,-476.2502\"/>\n</g>\n<!-- 3492 -->\n<g id=\"node9\" class=\"node\">\n<title>3492</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"140.9464\" cy=\"-522\" rx=\"40.8928\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"140.9464\" y=\"-518.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2Inv(&#45;3)</text>\n</g>\n<!-- 3492&#45;&gt;3491 -->\n<g id=\"edge2\" class=\"edge\">\n<title>3492&#45;&gt;3491</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M133.2834,-504.2022C129.781,-496.0675 125.5541,-486.2501 121.6653,-477.2181\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"124.7979,-475.6433 117.6286,-467.8425 118.3685,-478.4115 124.7979,-475.6433\"/>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x10516f550>"
          },
          "execution_count": 184,
          "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,
          32,
          35,
          38,
          40,
          43
        ],
        "trusted": true
      },
      "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 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 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": 75,
      "outputs": []
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "Then, convert our running example to a CFA:"
    },
    {
      "metadata": {
        "trusted": true
      },
      "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": 197,
      "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 0x101315b10>"
          },
          "execution_count": 197,
          "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": true
      },
      "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": 198,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "chc, invs = cfa_vc_gen(cfa0)\nHtmlStr('<br/>'.join([str(c) for c in chc]))",
      "execution_count": 199,
      "outputs": [
        {
          "data": {
            "text/html": "&forall;x, x' : L0(x)<br/>&forall;x, x' : L0(x) &and; x' = 0 &rArr; L1(x')<br/>&forall;x, x' : L1(x) &and; x &le; 5 &and; x' = x + 1 &rArr; L1(x')<br/>&forall;x, x' : L1(x) &and; x &ge; 10 &rArr; L2(x')<br/>&forall;x, x' : L2(x) &rArr; False",
            "text/plain": "\"&forall;x, x' : L0(x)<br/>&forall;x, x' : L0(x) &and; x' = 0 &rArr; L1(x')<br/>&forall;x, x' : L1(x) &and; x &le; 5 &and; x' = x + 1 &rArr; L1(x')<br/>&forall;x, x' : L1(x) &and; x &ge; 10 &rArr; L2(x')<br/>&forall;x, x' : L2(x) &rArr; False\""
          },
          "execution_count": 199,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(chc)\nHtmlStr(res)",
      "execution_count": 200,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "'<b>sat</b>'"
          },
          "execution_count": 200,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "invs",
      "execution_count": 201,
      "outputs": [
        {
          "data": {
            "text/plain": "{'L0': L0(x), 'L2': L2(x), 'L1': L1(x)}"
          },
          "execution_count": 201,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "answer.eval(invs['L0'])",
      "execution_count": 202,
      "outputs": [
        {
          "data": {
            "text/plain": "True"
          },
          "execution_count": 202,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(invs['L1']))",
      "execution_count": 203,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(x &ge; 7)",
            "text/plain": "'&not;(x &ge; 7)'"
          },
          "execution_count": 203,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "answer.eval(invs['L2'])",
      "execution_count": 204,
      "outputs": [
        {
          "data": {
            "text/plain": "False"
          },
          "execution_count": 204,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "cfa0 = mk_cfa0(safe=False)\nvc, invs = cfa_vc_gen(cfa0)\nres, answer = solve_horn(vc)\nSpacerProof(answer)",
      "execution_count": 206,
      "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=\"134pt\" height=\"476pt\"\n viewBox=\"0.00 0.00 134.09 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 130.0888,-472 130.0888,4 -4,4\"/>\n<!-- 85160 -->\n<g id=\"node1\" class=\"node\">\n<title>85160</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-18\" rx=\"63.0888\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">query!2805(0)</text>\n</g>\n<!-- 2590 -->\n<g id=\"node2\" class=\"node\">\n<title>2590</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-90\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L2(0)</text>\n</g>\n<!-- 2590&#45;&gt;85160 -->\n<g id=\"edge6\" class=\"edge\">\n<title>2590&#45;&gt;85160</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-71.8314C63.0444,-64.131 63.0444,-54.9743 63.0444,-46.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-46.4132 63.0444,-36.4133 59.5445,-46.4133 66.5445,-46.4132\"/>\n</g>\n<!-- 2160 -->\n<g id=\"node3\" class=\"node\">\n<title>2160</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-162\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(4)</text>\n</g>\n<!-- 2160&#45;&gt;2590 -->\n<g id=\"edge5\" class=\"edge\">\n<title>2160&#45;&gt;2590</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-143.8314C63.0444,-136.131 63.0444,-126.9743 63.0444,-118.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-118.4132 63.0444,-108.4133 59.5445,-118.4133 66.5445,-118.4132\"/>\n</g>\n<!-- 2159 -->\n<g id=\"node4\" class=\"node\">\n<title>2159</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-234\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(3)</text>\n</g>\n<!-- 2159&#45;&gt;2160 -->\n<g id=\"edge4\" class=\"edge\">\n<title>2159&#45;&gt;2160</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-215.8314C63.0444,-208.131 63.0444,-198.9743 63.0444,-190.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-190.4132 63.0444,-180.4133 59.5445,-190.4133 66.5445,-190.4132\"/>\n</g>\n<!-- 1917 -->\n<g id=\"node5\" class=\"node\">\n<title>1917</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-306\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(2)</text>\n</g>\n<!-- 1917&#45;&gt;2159 -->\n<g id=\"edge3\" class=\"edge\">\n<title>1917&#45;&gt;2159</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-287.8314C63.0444,-280.131 63.0444,-270.9743 63.0444,-262.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-262.4132 63.0444,-252.4133 59.5445,-262.4133 66.5445,-262.4132\"/>\n</g>\n<!-- 456 -->\n<g id=\"node6\" class=\"node\">\n<title>456</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-378\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(1)</text>\n</g>\n<!-- 456&#45;&gt;1917 -->\n<g id=\"edge2\" class=\"edge\">\n<title>456&#45;&gt;1917</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-359.8314C63.0444,-352.131 63.0444,-342.9743 63.0444,-334.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-334.4132 63.0444,-324.4133 59.5445,-334.4133 66.5445,-334.4132\"/>\n</g>\n<!-- 1493 -->\n<g id=\"node7\" class=\"node\">\n<title>1493</title>\n<ellipse fill=\"none\" stroke=\"#000000\" cx=\"63.0444\" cy=\"-450\" rx=\"31.3957\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"63.0444\" y=\"-446.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">L1(0)</text>\n</g>\n<!-- 1493&#45;&gt;456 -->\n<g id=\"edge1\" class=\"edge\">\n<title>1493&#45;&gt;456</title>\n<path fill=\"none\" stroke=\"#000000\" d=\"M63.0444,-431.8314C63.0444,-424.131 63.0444,-414.9743 63.0444,-406.4166\"/>\n<polygon fill=\"#000000\" stroke=\"#000000\" points=\"66.5445,-406.4132 63.0444,-396.4133 59.5445,-406.4133 66.5445,-406.4132\"/>\n</g>\n</g>\n</svg>\n",
            "text/plain": "<__main__.SpacerProof at 0x1051607d0>"
          },
          "execution_count": 206,
          "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": true
      },
      "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": 208,
      "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=\"node3\" 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<!-- exit -->\n<g id=\"node2\" 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<!-- 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</g>\n</svg>\n",
            "text/plain": "<graphviz.dot.Digraph at 0x105054690>"
          },
          "execution_count": 208,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "vc, invs = cfa_vc_gen(cfa1)\nres, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": 209,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unknown</b>",
            "text/plain": "'<b>unknown</b>'"
          },
          "execution_count": 209,
          "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": true
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc, q3=True)\nHtmlStr(res)",
      "execution_count": 210,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "'<b>sat</b>'"
          },
          "execution_count": 210,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(invs['L0']))",
      "execution_count": 211,
      "outputs": [
        {
          "data": {
            "text/html": "(&forall;sk!0 : cnt + -1&middot;sk!0 &le; 0 &or; MEM[sk!0] &ge; 0 &or; &not;(sk!0 &ge; 0)) &and;<br/>(&forall;sk!0 : MEM[sk!0] &le; 0 &or; cnt + -1&middot;sk!0 &le; 0 &or; &not;(sk!0 &ge; 0))",
            "text/plain": "'(&forall;sk!0 : cnt + -1&middot;sk!0 &le; 0 &or; MEM[sk!0] &ge; 0 &or; &not;(sk!0 &ge; 0)) &and;<br/>(&forall;sk!0 : MEM[sk!0] &le; 0 &or; cnt + -1&middot;sk!0 &le; 0 &or; &not;(sk!0 &ge; 0))'"
          },
          "execution_count": 211,
          "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": true
      },
      "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": 100,
      "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": 100,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts1)\nres, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": 101,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unknown</b>",
            "text/plain": "'<b>unknown</b>'"
          },
          "execution_count": 101,
          "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": true
      },
      "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": 102,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "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": 158,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "chc_to_str(vc)",
      "execution_count": 160,
      "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": 160,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "res, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": null,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(inv))",
      "execution_count": 108,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(b &ge; 213) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &le; 2) &and; a &ge; 0",
            "text/plain": "'&not;(b &ge; 213) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &le; 2) &and; a &ge; 0'"
          },
          "execution_count": 108,
          "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": true
      },
      "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": 112,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "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)\nHtmlStr(res)",
      "execution_count": 122,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "'<b>sat</b>'"
          },
          "execution_count": 122,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(inv))",
      "execution_count": 123,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(b &le; 2) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &ge; 213) &and; a &ge; 0",
            "text/plain": "'&not;(b &le; 2) &and; &not;(b + -1&middot;a &ge; 13) &and; &not;(b &ge; 213) &and; a &ge; 0'"
          },
          "execution_count": 123,
          "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": {
        "trusted": true
      },
      "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": 124,
      "outputs": []
    },
    {
      "metadata": {
        "trusted": true
      },
      "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": 132,
      "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": 132,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen(ts2)\nres, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": 133,
      "outputs": [
        {
          "data": {
            "text/html": "<b>unknown</b>",
            "text/plain": "'<b>unknown</b>'"
          },
          "execution_count": 133,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "code_folding": [
          0
        ],
        "trusted": true
      },
      "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=4)\nvc, inv = vc_gen(ts2_bnd)\nres, answer = solve_horn(vc)\nHtmlStr(res)",
      "execution_count": 136,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "'<b>sat</b>'"
          },
          "execution_count": 136,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(inv))",
      "execution_count": 137,
      "outputs": [
        {
          "data": {
            "text/html": "&not;(bnd &ge; 5) &and;<br/>(&not;(bnd &ge; 4) &or; &not;(20&middot;a + 10&middot;b + 4&middot;c + d &le; -26)) &and;<br/>(&not;(bnd &ge; 2) &or; &not;(4&middot;a + 3&middot;b + 2&middot;c + d &le; -4)) &and;<br/>(bnd &le; 0 &or; a + b + c + d &ge; 0) &and;<br/>(&not;(bnd &ge; 3) &or; &not;(10&middot;a + 6&middot;b + 3&middot;c + d &le; -6)) &and;<br/>d &ge; 0",
            "text/plain": "'&not;(bnd &ge; 5) &and;<br/>(&not;(bnd &ge; 4) &or; &not;(20&middot;a + 10&middot;b + 4&middot;c + d &le; -26)) &and;<br/>(&not;(bnd &ge; 2) &or; &not;(4&middot;a + 3&middot;b + 2&middot;c + d &le; -4)) &and;<br/>(bnd &le; 0 &or; a + b + c + d &ge; 0) &and;<br/>(&not;(bnd &ge; 3) &or; &not;(10&middot;a + 6&middot;b + 3&middot;c + d &le; -6)) &and;<br/>d &ge; 0'"
          },
          "execution_count": 137,
          "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": true
      },
      "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)\nHtmlStr(res)",
      "execution_count": 145,
      "outputs": [
        {
          "data": {
            "text/html": "<b>sat</b>",
            "text/plain": "'<b>sat</b>'"
          },
          "execution_count": 145,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(inv)",
      "execution_count": 146,
      "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": 146,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "HtmlStr(answer.eval(inv))",
      "execution_count": 147,
      "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": 147,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "vc, inv = vc_gen_part(ts2, { \"ac\":[a, c], \"bc\":[b, c], \"d\":[d] })\nres, answer = solve_horn(vc)\nHtmlStr(answer.eval(inv))",
      "execution_count": 149,
      "outputs": [
        {
          "data": {
            "text/html": "a &ge; 0 &and; b &ge; 0 &and; &not;(b + c &le; -2) &and; d &ge; 0",
            "text/plain": "'a &ge; 0 &and; b &ge; 0 &and; &not;(b + c &le; -2) &and; d &ge; 0'"
          },
          "execution_count": 149,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "chc_to_str(vc)",
      "execution_count": 150,
      "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": 150,
          "metadata": {},
          "output_type": "execute_result"
        }
      ]
    },
    {
      "metadata": {},
      "cell_type": "markdown",
      "source": "## Conclusion\n\nThis is the end of the interactive portion of the tutorial"
    },
    {
      "metadata": {
        "trusted": true
      },
      "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
}