old_z3_noodler_eval.ipynb

{
  "cells": [
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "cellView": "form",
        "id": "E6qy0q5XoFWn"
      },
      "outputs": [],
      "source": [
        "#@title Import stuff, helper functions...\n",
        "import datetime\n",
        "import pandas as pd\n",
        "import numpy as np\n",
        "import re as re\n",
        "import tabulate as tab\n",
        "import plotnine as p9\n",
        "import math\n",
        "import mizani.formatters as mizani\n",
        "import pylab\n",
        "# import warnings\n",
        "\n",
        "# warnings.filterwarnings('ignore')\n",
        "\n",
        "\n",
        "from plotnine.themes.themeable import legend_key_width\n",
        "# in seconds\n",
        "TIMEOUT = 120\n",
        "TIMEOUT_VAL = TIMEOUT * 1.1\n",
        "TIME_MIN = 0.01\n",
        "\n",
        "# For reading in files\n",
        "def read_file(filename):\n",
        "    \"\"\"Reads a CSV file into Panda's data frame\"\"\"\n",
        "    df_loc = pd.read_csv(\n",
        "        filename,\n",
        "        sep=\";\",\n",
        "        # comment=\"#\",\n",
        "        na_values=['ERR', 'TO', 'MISSING'],\n",
        "        # na_values=['TO', 'MISSING'],\n",
        "        # na_values=['TO'],\n",
        "        )\n",
        "    return df_loc\n",
        "\n",
        "# For reading in files\n",
        "def read_file_no_nan(filename):\n",
        "    \"\"\"Reads a CSV file into Panda's data frame\"\"\"\n",
        "    df_loc = pd.read_csv(\n",
        "        filename,\n",
        "        sep=\";\",\n",
        "        # comment=\"#\",\n",
        "        # na_values=['ERR', 'TO', 'MISSING'],\n",
        "        # na_values=['TO', 'MISSING'],\n",
        "        # na_values=['TO'],\n",
        "        )\n",
        "    return df_loc\n",
        "\n",
        "\n",
        "# For printing scatter plots\n",
        "def scatter_plot(df, xcol, ycol, domain, xname=None, yname=None, log=False, width=6, height=6, clamp=True, tickCount=5, show_legend=True):\n",
        "    assert len(domain) == 2\n",
        "\n",
        "    POINT_SIZE = 1.0\n",
        "    DASH_PATTERN = (0, (6, 2))\n",
        "\n",
        "    if xname is None:\n",
        "        xname = xcol\n",
        "    if yname is None:\n",
        "        yname = ycol\n",
        "\n",
        "    # formatter for axes' labels\n",
        "    ax_formatter = mizani.custom_format('{:n}')\n",
        "\n",
        "    if clamp:  # clamp overflowing values if required\n",
        "        df = df.copy(deep=True)\n",
        "        df.loc[df[xcol] > domain[1], xcol] = domain[1]\n",
        "        df.loc[df[ycol] > domain[1], ycol] = domain[1]\n",
        "\n",
        "    # generate scatter plot\n",
        "    scatter = p9.ggplot(df)\n",
        "    scatter += p9.aes(x=xcol, y=ycol, color=\"benchmark\")\n",
        "    scatter += p9.geom_point(size=POINT_SIZE, na_rm=True, show_legend=show_legend, raster=True)\n",
        "    scatter += p9.labs(x=xname, y=yname)\n",
        "    scatter += p9.theme(legend_key_width=2)\n",
        "    scatter += p9.scale_color_hue(l=0.4, s=0.9, h=0.1)\n",
        "\n",
        "    # rug plots\n",
        "    scatter += p9.geom_rug(na_rm=True, sides=\"tr\", alpha=0.05, raster=True)\n",
        "\n",
        "    if log:  # log scale\n",
        "        scatter += p9.scale_x_log10(limits=domain, labels=ax_formatter)\n",
        "        scatter += p9.scale_y_log10(limits=domain, labels=ax_formatter)\n",
        "    else:\n",
        "        scatter += p9.scale_x_continuous(limits=domain, labels=ax_formatter)\n",
        "        scatter += p9.scale_y_continuous(limits=domain, labels=ax_formatter)\n",
        "\n",
        "    # scatter += p9.theme_xkcd()\n",
        "    scatter += p9.theme_bw()\n",
        "    scatter += p9.theme(panel_grid_major=p9.element_line(color='#666666', alpha=0.5))\n",
        "    scatter += p9.theme(panel_grid_minor=p9.element_blank())\n",
        "    scatter += p9.theme(figure_size=(width, height))\n",
        "    scatter += p9.theme(axis_text=p9.element_text(size=24, color=\"black\"))\n",
        "    scatter += p9.theme(axis_title=p9.element_text(size=24, color=\"black\"))\n",
        "    scatter += p9.theme(legend_text=p9.element_text(size=12))\n",
        "\n",
        "    if not show_legend:\n",
        "        scatter += p9.theme(legend_position='none')\n",
        "\n",
        "    # generate additional lines\n",
        "    scatter += p9.geom_abline(intercept=0, slope=1, linetype=DASH_PATTERN)  # diagonal\n",
        "    scatter += p9.geom_vline(xintercept=domain[1], linetype=DASH_PATTERN)  # vertical rule\n",
        "    scatter += p9.geom_hline(yintercept=domain[1], linetype=DASH_PATTERN)  # horizontal rule\n",
        "\n",
        "    res = scatter\n",
        "\n",
        "    return res\n",
        "\n",
        "# Print a matrix of plots\n",
        "def matrix_plot(list_of_plots, cols):\n",
        "    assert len(list_of_plots) > 0\n",
        "    assert cols >= 0\n",
        "\n",
        "    matrix_plot = None\n",
        "    row = None\n",
        "    for i in range(0, len(list_of_plots)):\n",
        "        if i % cols == 0:  # starting a new row\n",
        "            row = list_of_plots[i]\n",
        "        else:\n",
        "            row |= list_of_plots[i]\n",
        "\n",
        "        if (i + 1) % cols == 0 or i + 1 == len(list_of_plots):  # last chart in a row\n",
        "            if not matrix_plot:  # first row finished\n",
        "                matrix_plot = row\n",
        "            else:\n",
        "                matrix_plot &= row\n",
        "\n",
        "    return matrix_plot\n",
        "\n",
        "\n",
        "# table to LaTeX file\n",
        "def table_to_file(table, headers, out_file):\n",
        "    with open(f\"plots/{out_file}.tex\", mode='w') as fl:\n",
        "        print(tab.tabulate(table, headers=headers, tablefmt=\"latex\"), file=fl)\n",
        "\n",
        "# generate evaluation\n",
        "def gen_evaluation(df, main_tool, all_tools):\n",
        "\n",
        "    print(f\"time:  {datetime.datetime.now()}\")\n",
        "    print(f\"# of formulae: {len(df)}\")\n",
        "\n",
        "    summary_times = dict()\n",
        "    for col in df.columns:\n",
        "        if re.search('-result$', col):\n",
        "            summary_times[col] = dict()\n",
        "            summary_times[col]['timeouts'] = df[col].isna().sum()\n",
        "            df[col] = df[col].str.strip()\n",
        "            summary_times[col]['unknowns'] = df[df[col] == \"unknown\"].shape[0] #[df[col] == \"unknown\"].shape[0]\n",
        "\n",
        "    # Remove unknowns\n",
        "    # df = df.drop(df[df[main_tool + \"-result\"] == \"unknown\"].index)\n",
        "    for tool in all_tools:\n",
        "      df.loc[df[tool + \"-result\"] == \"unknown\", tool + '-runtime'] = np.NaN\n",
        "\n",
        "    for col in df.columns:\n",
        "        if re.search('-runtime$', col):\n",
        "            summary_times[col] = dict()\n",
        "            summary_times[col]['max'] = df[col].max()\n",
        "            summary_times[col]['min'] = df[col].min()\n",
        "            summary_times[col]['mean'] = df[col].mean()\n",
        "            summary_times[col]['median'] = df[col].median()\n",
        "            summary_times[col]['std'] = df[col].std()\n",
        "\n",
        "    df_summary_times = pd.DataFrame(summary_times).transpose()\n",
        "\n",
        "\n",
        "\n",
        "    tab_interesting = []\n",
        "    for i in all_tools:\n",
        "        row = df_summary_times.loc[i + '-runtime']\n",
        "        unknown_row = dict(df_summary_times.loc[i + '-result'])\n",
        "        row_dict = dict(row)\n",
        "        row_dict.update({'name': i})\n",
        "        tab_interesting.append([row_dict['name'],\n",
        "                                # row_dict['min'],\n",
        "                                row_dict['max'],\n",
        "                                row_dict['mean'],\n",
        "                                row_dict['median'],\n",
        "                                row_dict['std'],\n",
        "                                unknown_row['timeouts'],\n",
        "                                unknown_row[\"unknowns\"]])\n",
        "\n",
        "    headers = [\"method\", \"max\", \"mean\", \"median\", \"std. dev\", \"TO+MO+ERR\", \"unknowns\"]\n",
        "    print(\"###################################################################################\")\n",
        "    print(\"####                                   Table 1                                 ####\")\n",
        "    print(\"###################################################################################\")\n",
        "    print(tab.tabulate(tab_interesting, headers=headers, tablefmt=\"github\"))\n",
        "    print(\"\\n\\n\")\n",
        "\n",
        "    # sanitizing NAs\n",
        "    for col in df.columns:\n",
        "        if re.search('-runtime$', col):\n",
        "            df[col].fillna(TIMEOUT_VAL, inplace=True)\n",
        "            df.loc[df[col] < TIME_MIN, col] = TIME_MIN  # to remove 0 (in case of log graph)\n",
        "\n",
        "\n",
        "    # comparing wins/loses\n",
        "    compare_methods = []\n",
        "    for t in all_tools:\n",
        "      if t == main_tool:\n",
        "        continue\n",
        "      compare_methods.append((main_tool + \"-runtime\", t + \"-runtime\"))\n",
        "\n",
        "\n",
        "    # compare_methods = [(\"noodler-runtime\", \"z3-runtime\"),\n",
        "    #                    (\"noodler-runtime\", \"cvc4-runtime\")\n",
        "    #                   ]\n",
        "\n",
        "    tab_wins = []\n",
        "    for left, right in compare_methods:\n",
        "        left_over_right = df[df[left] < df[right]]\n",
        "        right_timeouts = left_over_right[left_over_right[right] == TIMEOUT_VAL]\n",
        "\n",
        "        right_over_left = df[df[left] > df[right]]\n",
        "        left_timeouts = right_over_left[right_over_left[left] == TIMEOUT_VAL]\n",
        "\n",
        "        tab_wins.append([right, len(left_over_right), len(right_timeouts), len(right_over_left), len(left_timeouts)])\n",
        "\n",
        "    headers_wins = [\"method\", \"wins\", \"wins-timeouts\", \"loses\", \"loses-timeouts\"]\n",
        "    print(\"######################################################################\")\n",
        "    print(\"####                             Table 2                          ####\")\n",
        "    print(\"######################################################################\")\n",
        "    print(tab.tabulate(tab_wins, headers=headers_wins, tablefmt=\"github\"))\n",
        "    #table_to_file(tab_wins, headers_wins, out_prefix + \"_table1right\")\n",
        "    print(\"\\n\\n\")\n",
        "\n",
        "    print(\"##############    other claimed results    ###############\")\n",
        "\n",
        "    ############# the best solution ##########\n",
        "    # df['other_min-runtime'] = df[\n",
        "    #     ['cvc4-runtime',]].min(axis=1)\n",
        "\n",
        "\n",
        "    to_cmp2 = []\n",
        "    for t in all_tools:\n",
        "      if t == main_tool:\n",
        "        continue\n",
        "      to_cmp2.append({'x': main_tool, 'y': t,\n",
        "                'xname': NOODLER, 'yname': t,\n",
        "                'max': TIMEOUT_VAL, 'tickCount': 3})\n",
        "\n",
        "    # to_cmp2 = [{'x': \"noodler\", 'y': \"cvc4\",\n",
        "    #             'xname': 'Noodler', 'yname': 'CVC4',\n",
        "    #             'max': TIMEOUT_VAL, 'tickCount': 3},\n",
        "    #            {'x': \"noodler\", 'y': \"z3\",\n",
        "    #             'xname': 'Noodler', 'yname': 'Z3',\n",
        "    #             'max': TIMEOUT_VAL, 'tickCount': 3}\n",
        "    #           ]\n",
        "\n",
        "    # add fields where not present\n",
        "    for params in to_cmp2:\n",
        "        if 'xname' not in params:\n",
        "            params['xname'] = None\n",
        "        if 'yname' not in params:\n",
        "            params['yname'] = None\n",
        "        if 'max' not in params:\n",
        "            params['max'] = TIMEOUT_VAL\n",
        "        if 'tickCount' not in params:\n",
        "            params['tickCount'] = 5\n",
        "        if 'filename' not in params:\n",
        "            params['filename'] = \"/home/fig_\" + params['x'] + \"_vs_\" + params['y'] + \".pdf\"\n",
        "\n",
        "    size = 7\n",
        "    plot_list = [(params['x'],\n",
        "                  params['y'],\n",
        "                  params['filename'],\n",
        "                  scatter_plot(df,\n",
        "                               xcol=params['x'] + '-runtime',\n",
        "                               ycol=params['y'] + '-runtime',\n",
        "                               xname=params['xname'], yname=params['yname'],\n",
        "                               domain=[TIME_MIN, params['max']],\n",
        "                               tickCount=params['tickCount'],\n",
        "                               log=True, width=size+2, height=size)) for params\n",
        "                 in to_cmp2]\n",
        "\n",
        "    print(\"\\n\\n\")\n",
        "    print(\"Generating plots...\")\n",
        "    for x, y, filename, plot in plot_list:\n",
        "        #filename = f\"plots/{out_prefix}_{filename}.pdf\"\n",
        "        print(f\"plotting x: {x}, y: {y}... saving to {filename}\")\n",
        "        # plot.save(filename, scale_factor=2)\n",
        "        # plot.save(filename=filename, dpi=1000)\n",
        "        print(plot)\n",
        "\n",
        "    # return benchmarks solvable only by 'engine'\n",
        "    # def only_solves(df, engine):\n",
        "    #     # select those where engine finishes\n",
        "    #     res = df[df[engine + '-runtime'] != TIMEOUT_VAL]\n",
        "    #     for col in res.columns:\n",
        "    #         if re.search('-runtime$', col) and not re.search(engine, col):\n",
        "    #             res = res[res[col] == TIMEOUT_VAL]\n",
        "\n",
        "    #     return res\n",
        "\n",
        "\n",
        "    # engines = [\"z3\",\n",
        "    #            \"cvc4\",\n",
        "    #            \"noodler\"\n",
        "    #           ]\n",
        "\n",
        "    # for i in all_tools:\n",
        "    #     i_only_solves = only_solves(df, i)\n",
        "    #     print(f\"only {i} = \" + str(len(i_only_solves)))\n",
        "    #     if len(i_only_solves) > 0:\n",
        "    #         print()\n",
        "    #         print(tab.tabulate(i_only_solves, headers='keys'))\n",
        "    #         print()\n",
        "\n",
        "    def none_solves(df):\n",
        "        # select those where engine finishes\n",
        "        res = df\n",
        "        for col in res.columns:\n",
        "            if re.search('-runtime$', col):\n",
        "                res = res[res[col] == TIMEOUT_VAL]\n",
        "\n",
        "        return res\n",
        "\n",
        "    unsolvable = none_solves(df)\n",
        "    #print(\"unsolvable: \" + str(len(unsolvable)))\n",
        "    #print(tab.tabulate(unsolvable, headers='keys'))\n",
        "    #print(\"\\n\\n\\n\\n\\n\")\n",
        "\n",
        "def get_unknowns(df, tool):\n",
        "  pt = df#[[\"name\", NOODLER+\"-result\"]]\n",
        "  pt = pt[(pt[tool+\"-result\"].str.strip() == 'unknown')]\n",
        "  return pt\n",
        "def sanity_check(df, tool, compare_with):\n",
        "  pt = df#[[\"name\", compare_with+\"-result\", NOODLER+\"-result\"]]\n",
        "  pt = pt[((pt[tool+\"-result\"].str.strip() == 'sat') & (pt[compare_with+\"-result\"].str.strip() == 'unsat') | (pt[tool+\"-result\"].str.strip() == 'unsat') & (pt[compare_with+\"-result\"].str.strip() == 'sat'))]\n",
        "  return pt\n",
        "def check_for_errors(df, tool):\n",
        "  pt = df#[[\"name\", NOODLER+\"-result\"]]\n",
        "  pt = pt[((pt[tool+\"-result\"].str.strip() != 'sat') & (pt[tool+\"-result\"].str.strip() != 'unsat') & (pt[tool+\"-result\"].str.strip() != 'unknown') & (pt[tool+\"-result\"].str.strip() != 'TO'))]\n",
        "  return pt\n",
        "def get_timeouts(df, tool):\n",
        "  pt = df#[[\"name\", NOODLER+\"-result\"]]\n",
        "  pt = pt[(pt[tool+\"-result\"].str.strip() == 'TO')]\n",
        "  return pt\n",
        "def get_solved(df, tool):\n",
        "  pt = df#[[\"name\", NOODLER+\"-result\"]]\n",
        "  pt = pt[(pt[tool+\"-result\"].str.strip() == 'sat')|(pt[tool+\"-result\"].str.strip() == 'unsat')]\n",
        "  return pt"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "\n",
        "# make tables interactive\n",
        "from itables import init_notebook_mode\n",
        "import itables.options as opt\n",
        "init_notebook_mode(all_interactive=True, connected=True)\n",
        "opt.maxBytes=0"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "id": "z2uuCCJutPm3"
      },
      "outputs": [],
      "source": [
        "restrict_to_int_conversion = False\n",
        "\n",
        "if not restrict_to_int_conversion:\n",
        "  FILES = [\n",
        "      \"sygus_qgen/to120.csv\",\n",
        "      \"denghang/to120.csv\",\n",
        "      \"automatark/to120.csv\",\n",
        "      \"stringfuzz/to120.csv\",\n",
        "\n",
        "      \"norn/to120.csv\",\n",
        "      \"slog/to120.csv\",\n",
        "      \"slent/to120.csv\",\n",
        "      \"transducer_plus/to120.csv\",\n",
        "      \"kepler/to120.csv\",\n",
        "      \"woorpje/to120.csv\",\n",
        "      \"webapp/to120.csv\",\n",
        "      \"kaluza/to120.csv\",\n",
        "      # \"redos/to120.csv\",\n",
        "\n",
        "      \"leetcode/to120.csv\",\n",
        "      \"str_small_rw/to120.csv\",\n",
        "      \"pyex/to120.csv\",\n",
        "      \"full_str_int/to120.csv\",\n",
        "      ]\n",
        "else:\n",
        "  # Only benchmarks with to_int/from_int\n",
        "  FILES = [\n",
        "      \"stringfuzz/to120.csv\",\n",
        "      \"str_small_rw/to120.csv\",\n",
        "      \"full_str_int/to120.csv\",\n",
        "  ]\n",
        "  with open(\"int_convs_not-full_str_int.txt\") as file:\n",
        "    fsi_not_conv = file.read().splitlines()\n",
        "  with open(\"int_convs-str_small_rw.txt\") as file:\n",
        "    ssr_conv = file.read().splitlines()\n",
        "  with open(\"int_convs-stringfuzz.txt\") as file:\n",
        "    sf_conv = file.read().splitlines()\n",
        "\n",
        "NOODLER = \"\"\n",
        "\n",
        "TOOLS = [\n",
        "    NOODLER,\n",
        "\n",
        "    ### OTHER TOOLS ###\n",
        "\n",
        "    # NOT run with 8GB limit (and some of them are not complete + at some point pycobench got broken and set 60s TO always)\n",
        "    # \"cvc5-1.0.5\",\n",
        "    # \"z3-4.12.1\",\n",
        "    # \"z3-4.12.2-nomem\",\n",
        "    # \"z3-trau\",\n",
        "    # \"z3strRE-nomem\",\n",
        "    # \"z3str4-nomem\",\n",
        "    # \"ostrich-1.2\", # run with ol\n",
        "    # \"ostrich-1.3\",\n",
        "\n",
        "    # run with 8GB limit (they should be also complete, and pycobench works probably correctly)\n",
        "    # \"cvc5-1.0.8\",\n",
        "    # \"z3-4.12.2\",\n",
        "    # \"z3str4\",\n",
        "    # \"ostrich-70d01e2d2\", # 1.3 with some extra commits that seems to fix some bugs + run with '-portfolio=strings'\n",
        "    # \"ostrich-70d01e2d2-parikh\", # same as previous but also run with +parikh (not run on pyex)\n",
        "    # \"z3strRE\",\n",
        "    # \"z3-trau-1.1\",\n",
        "\n",
        "    # run on pikachu with 6 processes in parallel (not 8 like previously)\n",
        "    # \"cvc5-1.1.1\",\n",
        "    \"cvc5-1.1.2\",\n",
        "    # \"z3-4.12.5\",\n",
        "    # \"z3-4.12.6\",\n",
        "    \"z3-4.13.0\",\n",
        "    \"ostrich-5dd2e10ca\", # 1.3 with even more commits than 70d01e2d2 (run without any arguments)\n",
        "    # \"z3-noodler-fb447e3-2cddb2f\", # v1.0.0\n",
        "    # \"z3-noodler-0751e1e-2cddb2f\", # v1.1.0\n",
        "\n",
        "\n",
        "    ### PREVIOUS NOODLER VERSIONS ###\n",
        "\n",
        "    # noodler from OOPSLA paper\n",
        "    # \"z3-noodler-9f5e602\",\n",
        "    # \"z3-noodler-9f5e602-underapprox\", # for kaluza\n",
        "\n",
        "    # # noodler that was run on everything except pyex (but there was some problem with stringfuzz and leetcode)\n",
        "    # \"z3-noodler-6e14cda\",\n",
        "    # # noodler that was run on everything except pyex (with infinite loop thingy)\n",
        "    # \"z3-noodler-59658f7\",\n",
        "    # # noodler that was run on everything except pyex (without infinite loop thingy)\n",
        "    # \"z3-noodler-e8a4269\",\n",
        "\n",
        "    # noodler that was run on everything (with wrong results on pyex)\n",
        "    # \"z3-noodler-daa40de\",\n",
        "    # noodler that was run on everything (with wrong results on pyex)\n",
        "    # \"z3-noodler-5f32279\",\n",
        "\n",
        "    # noodler after merging PR64: Regex construction optimization (right before refactoring, with bug in mata for removing unused states - 3 norn and 190 pyex bad)\n",
        "    #\"z3-noodler-49295a5-8781b7d\",\n",
        "\n",
        "    # noodler after refactoring that was run on everything (with bug in mata for removing unused states - 3 wrong results on norn)\n",
        "    # \"z3-noodler-d1676a5-8781b7d\",\n",
        "    # \"z3-noodler-d1676a5-8781b7d-underapprox\",\n",
        "    # \"z3-noodler-d1676a5-8781b7d-nielsen\",\n",
        "\n",
        "    # noodler after refactoring, with fixed bug in mata\n",
        "    # \"z3-noodler-loop-13af422-5fa5ea0\",\n",
        "    # \"z3-noodler-13af422-5fa5ea0\",\n",
        "\n",
        "    # just before merging branch opt-pred-inst\n",
        "    # \"z3-noodler-d83b1b9-2f0ef53\",\n",
        "\n",
        "    # just before merging loop-protection-fix\n",
        "    # \"z3-noodler-loop-1a1ac35-2f0ef53\",\n",
        "    # \"z3-noodler-loop-mem\", # 1a1ac35-2f0ef53 but with 8GB memory limit\n",
        "\n",
        "    ### Everything after this has loop protection by default + is run with 8GB memory limit\n",
        "\n",
        "    # just before merging regex-info\n",
        "    # \"z3-noodler-381ffd1-2f0ef53\",\n",
        "\n",
        "    # from dec-proc-default, both run only with either nielsen or underapproximation allowed\n",
        "    # \"z3-noodler-nielsen-0746e08-8ba88ce\",\n",
        "    # \"z3-noodler-underapprox-ab28d76-2f0ef53\",\n",
        "\n",
        "    # str_int where dec-proc-default was not yet in\n",
        "    # \"z3-noodler-63aa361-8ba88ce\",\n",
        "\n",
        "    ### Everything after this has also nielsen and underapproximation on by default\n",
        "    \n",
        "    # devel after merging nielsen_first\n",
        "    # \"z3-noodler-a0e3745-8ba88ce\",\n",
        "\n",
        "    # just before merging new_mata\n",
        "    # \"z3-noodler-0ae38ae-40ca1cd\",\n",
        "\n",
        "    # after updating to z3 v4.12.2\n",
        "    # \"z3-noodler-1ba1904-40ca1cd\"\n",
        "\n",
        "    # noodler stays the same, but we update mata\n",
        "    # \"z3-noodler-f211b89-7831cdc\",\n",
        "    #\"z3-noodler-f211b89-bb85433\",\n",
        "    #\"z3-noodler-1482571-a57f582\"\n",
        "\n",
        "    # branch noodle_reduce\n",
        "    # \"z3-noodler-feada45-a57f582\",\n",
        "\n",
        "    # branch underapprox-opt\n",
        "    #z3-noodler-482f3c0-387babd,\n",
        "\n",
        "    # branch pyex-opt-it2\n",
        "    # \"z3-noodler-8de5f2c-387babd\",\n",
        "\n",
        "    # branch to-from-int\n",
        "    # \"z3-noodler-147a0e0-fb6e2b1\",\n",
        "    # \"z3-noodler-34ea542-2cddb2f\", # for errors, instead of unknown, it shows the error message in the result\n",
        "\n",
        "    # branch tp-from-int-2\n",
        "    # \"z3-noodler-7421e81-2cddb2f\",\n",
        "\n",
        "    # branch to-from-int-3\n",
        "    # \"z3-noodler-c69c980-2cddb2f\",\n",
        "\n",
        "    # branch asserts-fixing\n",
        "    # \"z3-noodler-1174fd1-2cddb2f\",\n",
        "\n",
        "    # branch full-int-opt\n",
        "    # \"z3-noodler-bdb7f83-2cddb2f\",\n",
        "\n",
        "    # branch to-int-eq\n",
        "    # \"z3-noodler-a0d4232-2cddb2f\",\n",
        "\n",
        "    # branch to-from-int-length-based,\n",
        "    # \"z3-noodler-bee36a1-2cddb2f\",\n",
        "\n",
        "    # branch to-from-int-more-precise\n",
        "    # \"z3-noodler-005708c-2cddb2f\",\n",
        "\n",
        "    # branch rewrite-inre\n",
        "    # \"z3-noodler-789525b-2cddb2f\",\n",
        "\n",
        "    # branch underapprox-unsound\n",
        "    # \"z3-noodler-77f7c04-2cddb2f\",\n",
        "\n",
        "    # branch new-new-z3 (both are basically the same, but the first one is older mata)\n",
        "    # \"z3-noodler-3233733-2cddb2f\",\n",
        "    # \"z3-noodler-ec4ce36-d95fe13\",\n",
        "\n",
        "    ]\n",
        "\n",
        "dfs = dict()\n",
        "dfs_no_nan = dict()\n",
        "for file in FILES:\n",
        "  df = read_file(file)\n",
        "  df[\"benchmark\"] = file\n",
        "  dfs[file] = df\n",
        "  df = read_file_no_nan(file)\n",
        "  df[\"benchmark\"] = file\n",
        "  dfs_no_nan[file] = df\n",
        "# df_all is used for generating results, we select only columns with used tools\n",
        "df_all = pd.concat(dfs)[[\"name\"] + [f(tool) for tool in TOOLS for f in (lambda x: x+\"-result\", lambda x: x+\"-runtime\")] + [\"benchmark\"]]\n",
        "\n",
        "# df_all_no_nan is used for checking if noodler gives correct results, we select only columns with used tools + only result columns are needed\n",
        "df_all_no_nan = pd.concat(dfs_no_nan)[[\"name\"] + [f(tool) for tool in TOOLS for f in (lambda x: x+\"-result\", lambda x: x+\"-runtime\")] + [\"benchmark\"]]\n",
        "for tool in TOOLS:\n",
        "  df_all_no_nan.loc[(df_all_no_nan[f\"{tool}-result\"] != \" sat\")&(df_all_no_nan[f\"{tool}-result\"] != \" unsat\")&(df_all_no_nan[f\"{tool}-result\"] != \" unknown\"), f\"{tool}-runtime\"] = 120\n",
        "  df_all_no_nan[f\"{tool}-runtime\"] = df_all_no_nan[f\"{tool}-runtime\"].astype(float)\n",
        "\n",
        "if restrict_to_int_conversion:\n",
        "  df_all_no_nan = df_all_no_nan[(df_all_no_nan.benchmark != \"full_str_int/to120.csv\")|(~(df_all_no_nan.name.isin(fsi_not_conv)))]\n",
        "  df_all = df_all[(df_all.benchmark != \"full_str_int/to120.csv\")|(~(df_all.name.isin(fsi_not_conv)))]\n",
        "\n",
        "  df_all_no_nan = df_all_no_nan[((df_all_no_nan.benchmark != \"str_small_rw/to120.csv\")&(df_all_no_nan.benchmark != \"stringfuzz/to120.csv\"))|((df_all_no_nan.name.isin(ssr_conv))|(df_all_no_nan.name.isin(sf_conv)))]\n",
        "  df_all = df_all[((df_all.benchmark != \"str_small_rw/to120.csv\")&(df_all.benchmark != \"stringfuzz/to120.csv\"))|((df_all.name.isin(ssr_conv))|(df_all.name.isin(sf_conv)))]"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "58kc36300GyL"
      },
      "source": [
        "Sanity check"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 53
        },
        "id": "299saL3rt1Dc",
        "outputId": "a2e252df-6307-4984-e90b-6407d4bb3d8e"
      },
      "outputs": [],
      "source": [
        "# check if noodler does not return different result than other solvers (i.e. wrong sat/unsat)\n",
        "all_bad = [sanity_check(df_all_no_nan, NOODLER, tool) for tool in TOOLS if tool != NOODLER]\n",
        "# merged = all_bad[0]\n",
        "# for bad in all_bad[1:]:\n",
        "#   merged = pd.merge(merged, bad, on='name', how='outer')\n",
        "# merged\n",
        "pd.concat(all_bad).drop_duplicates()"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Print ERR/TO/unknowns"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 615
        },
        "id": "NRnpSINTl0jX",
        "outputId": "21cdaa9e-c227-4f6f-e57f-25b62b553847"
      },
      "outputs": [],
      "source": [
        "# get all formulae where noodler gives different result than sat/unsat/unknown/TO\n",
        "res = check_for_errors(df_all_no_nan, NOODLER)\n",
        "\n",
        "# filter memouts (just kinda heuristics, we assume all ERR for last run (assumed to be last in TOOLS) were memout, so we assume they are still memouts)\n",
        "# res = res[(res[TOOLS[-1] + \"-result\"] != \"ERR\")]\n",
        "\n",
        "# filter out \"ERR\", usually those are MEMOUTs\n",
        "# res = res[(res[NOODLER + '-result'] != \"ERR\")]\n",
        "\n",
        "# some common errors you might want to filter out\n",
        "# res = res[(res[NOODLER + '-result'] != \" cannot process to_int/from_int for automaton with infinite language\")]\n",
        "# res = res[(res[NOODLER + '-result'] != \" str.replace_all is not supported\")]\n",
        "# res = res[(res[NOODLER + '-result'] != \" str.replace_re_all is not supported\")]\n",
        "\n",
        "# show everything\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 1000
        },
        "id": "iZM3O3y7gNXL",
        "outputId": "c8e7b8d0-0406-41ef-d9b9-874a645f4a68"
      },
      "outputs": [],
      "source": [
        "res = get_timeouts(df_all_no_nan, NOODLER)\n",
        "\n",
        "# filter those that in previous version of noodler had TO\n",
        "# res = res[(res[TOOLS[-1] + \"-result\"] != \"TO\")]\n",
        "\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 217
        },
        "id": "-BOelXU1qeol",
        "outputId": "ddd88e9a-fb9f-445d-9fc5-8f6304f7444f"
      },
      "outputs": [],
      "source": [
        "res = get_unknowns(df_all_no_nan, NOODLER)\n",
        "\n",
        "# filter those that in previous version of noodler had unknown\n",
        "# res = res[(res[TOOLS[-1] + \"-result\"] != \" unknown\")]\n",
        "\n",
        "# filter those that in previous version of noodler had TO/ERR\n",
        "# res = res[(res[TOOLS[-1] + \"-result\"] != \"ERR\") & (res[TOOLS[-1] + \"-result\"] != \"TO\")]\n",
        "\n",
        "res"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "res = get_solved(df_all_no_nan, NOODLER)\n",
        "\n",
        "res"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "Show graphs/tables"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 1000
        },
        "id": "1XvGImTWpID4",
        "outputId": "aa9d49f9-e150-494d-b000-b5ae64d087c6"
      },
      "outputs": [],
      "source": [
        "gen_evaluation(df_all, NOODLER, TOOLS)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "header = [\"tool\", \"✅\", \"❌\", \"avg\", \"med\", \"time\", \"sat\", \"unsat\", \"unknown\", \"TO\", \"MO+ERR\", \"other\"]\n",
        "\n",
        "if restrict_to_int_conversion:\n",
        "    with open(\"int_convs_not-full_str_int.txt\") as file:\n",
        "        fsi_not_conv = file.read().splitlines()\n",
        "    with open(\"int_convs-str_small_rw.txt\") as file:\n",
        "        ssr_conv = file.read().splitlines()\n",
        "    with open(\"int_convs-stringfuzz.txt\") as file:\n",
        "        sf_conv = file.read().splitlines()\n",
        "\n",
        "for bench in FILES:\n",
        "    df = read_file_no_nan(bench)\n",
        "    if restrict_to_int_conversion:\n",
        "        if bench.startswith(\"full_str_int\"):\n",
        "            df = df[(~(df.name.isin(fsi_not_conv)))]\n",
        "        if bench.startswith(\"str_small_rw\"):\n",
        "            df = df[(df.name.isin(ssr_conv))]\n",
        "        if bench.startswith(\"stringfuzz\"):\n",
        "            df = df[(df.name.isin(sf_conv))]\n",
        "    print(f\"Benchmark {bench}\")\n",
        "    print(f\"# of formulae: {len(df)}\")\n",
        "    print(\"--------------------------------------------------\")\n",
        "    table = [header]\n",
        "    for tool in TOOLS:\n",
        "        if tool == \"z3-trau-1.1\" and bench.startswith(\"transducer_plus\"): # trau gives only errors, so \"z3-trau-1.1\" does not exist in df\n",
        "            table.append([tool, 0, len(df), \"-\", \"-\", 0,0,0,0,len(df),0])\n",
        "            continue\n",
        "        sat = len(df[df[tool + \"-result\"] == \" sat\"])\n",
        "        unsat = len(df[df[tool + \"-result\"] == \" unsat\"])\n",
        "        solved = df[(df[tool + \"-result\"] == \" sat\") | (df[tool + '-result'] == \" unsat\")][f\"{tool}-runtime\"].astype(float)\n",
        "        avg_solved = solved.mean()\n",
        "        median_solved = solved.median()\n",
        "        total_solved = solved.sum()\n",
        "        unknown = len(df[df[tool + \"-result\"] == \" unknown\"])\n",
        "        to = len(df[df[tool + \"-result\"] == \"TO\"])\n",
        "        err = len(df[df[tool + \"-result\"] == \"ERR\"])\n",
        "        other = len(df[(df[tool + \"-result\"] != \"ERR\") & (df[tool + \"-result\"] != \"TO\") & (df[tool + \"-result\"] != \" unknown\") & (df[tool + \"-result\"] != \" unsat\") & (df[tool + \"-result\"] != \" sat\")])\n",
        "        table.append([tool, sat+unsat, unknown+to+err+other, avg_solved, median_solved, total_solved, sat, unsat, unknown, to, err, other])\n",
        "    print(tab.tabulate(table, headers='firstrow', floatfmt=\".2f\"))\n",
        "    print(\"--------------------------------------------------\")\n",
        "    print()"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "### Stuff to generate tables/graphs for SAT'24 paper:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "\n",
        "import warnings\n",
        "warnings.filterwarnings('ignore')\n",
        "\n",
        "NOODLER_FOR_BENCHMARK = \"z3-noodler-0751e1e-2cddb2f\"\n",
        "CVC5 = \"cvc5-1.1.2\"\n",
        "Z3 = \"z3-4.13.0\"\n",
        "OSTRICH = \"ostrich-5dd2e10ca\"\n",
        "Z3STR4 = \"z3str4\"\n",
        "Z3TRAU = \"z3-trau-1.1\"\n",
        "OLD_NOODLER = \"z3-noodler-fb447e3-2cddb2f\"\n",
        "tools_for_comparison = [\n",
        "    NOODLER_FOR_BENCHMARK,\n",
        "    CVC5,\n",
        "    Z3,\n",
        "    # Z3STR4,\n",
        "    OSTRICH,\n",
        "    # Z3STR3RE,\n",
        "    # Z3TRAU,\n",
        "    OLD_NOODLER,\n",
        "]\n",
        "tool_names_mapping = {\n",
        "    NOODLER_FOR_BENCHMARK : \"Z3-Noodler\",\n",
        "    CVC5 : \"cvc5\",\n",
        "    Z3 : \"Z3\",\n",
        "    Z3STR4 : \"Z3stsr4\",\n",
        "    OSTRICH : \"OSTRICH\",\n",
        "    # Z3STR3RE : \"Z3str3RE\",\n",
        "    # Z3TRAU : \"Z3-Trau\",\n",
        "    OLD_NOODLER : \"Z3-Noodler*\",\n",
        "}\n",
        "\n",
        "tool_latex_mapping = {\n",
        "    NOODLER_FOR_BENCHMARK : \"\\\\ziiinoodler\",\n",
        "    CVC5 : \"\\\\cvcv\",\n",
        "    Z3 : \"\\\\ziii\",\n",
        "    Z3STR4 : \"\\\\ziiistriv\",\n",
        "    OSTRICH : \"\\\\ostrich\",\n",
        "    # Z3STR3RE : \"\\\\ziiistriiire\",\n",
        "    Z3TRAU : \"\\\\ziiitrau\",\n",
        "    OLD_NOODLER : \"\\\\ziiinoodlerold\",\n",
        "}\n",
        "\n",
        "def clean_runtimes(df):\n",
        "    for tool in tools_for_comparison:\n",
        "        # set \"-runtime\" column to 120 if it does not contain number (ERR/MO) + work with is as a float\n",
        "        df.loc[(df[f\"{tool}-result\"] != \" sat\")&(df[f\"{tool}-result\"] != \" unsat\"), f\"{tool}-runtime\"] = 120\n",
        "        df[f\"{tool}-runtime\"] = df[f\"{tool}-runtime\"].astype(float)\n",
        "    return df\n",
        "\n",
        "def print_num(num):\n",
        "    if isinstance(num, int):\n",
        "        return f\"{num:_}\".replace('_', '\\\\,')\n",
        "    else:\n",
        "        return f\"{num:.2f}\"\n",
        "\n",
        "benches = []\n",
        "with open(\"int_convs_not-full_str_int.txt\") as file:\n",
        "    fsi_not_conv = file.read().splitlines()\n",
        "    df = clean_runtimes(read_file_no_nan(\"full_str_int/to120.csv\"))\n",
        "    df[\"benchmark\"] = \"StrInt\"\n",
        "    benches.append([\"StrInt\", R\"\\fullstrint\", df, df[(~(df.name.isin(fsi_not_conv)))]])\n",
        "with open(\"int_convs-stringfuzz.txt\") as file:\n",
        "    sf_conv = file.read().splitlines()\n",
        "    df = clean_runtimes(read_file_no_nan(\"stringfuzz/to120.csv\"))\n",
        "    df[\"benchmark\"] = \"StrFuzz\"\n",
        "    benches.append([\"StrFuzz\", R\"\\stringfuzz\", df, df[(df.name.isin(sf_conv))]])\n",
        "with open(\"int_convs-str_small_rw.txt\") as file:\n",
        "    ssr_conv = file.read().splitlines()\n",
        "    df = clean_runtimes(read_file_no_nan(\"str_small_rw/to120.csv\"))\n",
        "    df[\"benchmark\"] = \"StrSm\"\n",
        "    benches.append([\"StrSm\", R\"\\strsmall\", df, df[(df.name.isin(ssr_conv))]])"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "print(R\"\"\"\\newcolumntype{g}{>{\\columncolor{gray!30}}r}\n",
        "\\newcolumntype{h}{>{\\columncolor{gray!30}}c}\"\"\")\n",
        "# print(R\"\"\"\\newcolumntype{g}{r}\n",
        "# \\newcolumntype{h}{c}\"\"\")\n",
        "\n",
        "# for printing best\n",
        "print(R\"\\newcommand{\\ping}[0]{\\bf}\")\n",
        "\n",
        "COLUMNS = [\n",
        "    \"solved\",\n",
        "    \"unknown\", # unknowns\n",
        "    \"OOR\", # out of resources\n",
        "    # \"TOs\",\n",
        "    # \"MOs\",\n",
        "    # \"Total\",\n",
        "    # \"Med\",\n",
        "    # \"Avg/Std\",\n",
        "    # \"Std\"\n",
        "    ]\n",
        "print(R\"\\begin{tabular}{l\" + \"g\"*len(COLUMNS)*2 + \"r\"*len(COLUMNS)*2 + \"g\"*len(COLUMNS)*2 + R\"\"\"rr}\n",
        "\\toprule\"\"\")\n",
        "\n",
        "bench_name_line = \"\"\n",
        "top_line = \"\"\n",
        "top_line_2 = \"\"\n",
        "\n",
        "col_type = \"h\"\n",
        "for bench in benches:\n",
        "    bench_name_line += f\" & \\\\multicolumn{{{len(COLUMNS)*2}}}{{{col_type}}}{{{bench[1]} ({print_num(len(bench[2]))}\\,|\\,{print_num(len(bench[3]))})}}\"\n",
        "    top_line += \" & \" + \" & \".join([f\"\\\\multicolumn{{2}}{{{col_type}}}{{\\\\textbf{{\\\\emph{{{s}}}}}}}\" for s in COLUMNS])\n",
        "    top_line_2 += f\" & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\emph{{all}}}} & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\emph{{conv}}}}\"*len(COLUMNS)\n",
        "    if (col_type == \"h\"):\n",
        "        col_type = \"c\"\n",
        "    else:\n",
        "        col_type = \"h\"\n",
        "\n",
        "# bench_name_line += f\" & \\\\multicolumn{{2}}{{{col_type}}}{{$\\\\Sigma$}} ({print_num(sum([len(bench[2]) for bench in benches]))}|{print_num(sum([len(bench[3]) for bench in benches]))})\\\\\\\\\"\n",
        "bench_name_line += f\" & \\\\multicolumn{{2}}{{{col_type}}}{{$\\\\Sigma$}}\\\\\\\\\"\n",
        "top_line += f\" & \\\\multicolumn{{2}}{{{col_type}}}{{\\\\textbf{{\\\\emph{{solved}}}}}}\\\\\\\\\"\n",
        "top_line_2 += f\" & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\emph{{all}}}} & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\emph{{conv}}}}\\\\\\\\\"\n",
        "\n",
        "for i in range(len(benches)):\n",
        "    cur_start = len(COLUMNS)*2*i+2\n",
        "    bench_name_line += f\"\\\\cmidrule(lr){{{cur_start}-{cur_start + len(COLUMNS)*2 - 1}}}\"\n",
        "    for j in range(len(COLUMNS)):\n",
        "        top_line += f\"\\\\cmidrule(lr){{{cur_start+2*j}-{cur_start+2*j+1}}}\"\n",
        "\n",
        "bench_name_line += f\"\\\\cmidrule(lr){{{len(benches)*len(COLUMNS)*2+2}-{len(benches)*len(COLUMNS)*2+3}}}\"\n",
        "top_line += f\"\\\\cmidrule(lr){{{len(benches)*len(COLUMNS)*2+2}-{len(benches)*len(COLUMNS)*2+3}}}\"\n",
        "\n",
        "print(bench_name_line)\n",
        "print(top_line)\n",
        "print(top_line_2)\n",
        "print(R\"\\midrule\")\n",
        "\n",
        "tool_lines = {}\n",
        "solved_total_all = {tool: 0 for tool in tools_for_comparison}\n",
        "solved_total_int = {tool: 0 for tool in tools_for_comparison}\n",
        "avg_and_std_line = {tool: f\"{tool_latex_mapping[tool]}\" for tool in tools_for_comparison}\n",
        "for bench in benches:\n",
        "    bench_name = bench[0]\n",
        "    tool_lines[bench_name] = {}\n",
        "    df_all = bench[2]\n",
        "    df_int = bench[3]\n",
        "    total_all = len(df_all)\n",
        "    total_int = len(df_int)\n",
        "    for tool in tools_for_comparison:\n",
        "        solved_df_all = df_all[(df_all[tool + \"-result\"] == \" sat\") | (df_all[tool + '-result'] == \" unsat\")]\n",
        "        solved_df_int = df_int[(df_int[tool + \"-result\"] == \" sat\") | (df_int[tool + '-result'] == \" unsat\")]\n",
        "        # num_of_unsolved[tool] = total - len(solved_df)\n",
        "        # TOs[tool] = len(df[(df[tool + \"-result\"] == \"TO\")])\n",
        "        # MOs[tool] = len(df[(df[tool + \"-result\"] == \"ERR\")])\n",
        "        # unknowns[tool] = len(df[(df[tool + \"-result\"] == \" unknown\")])\n",
        "\n",
        "\n",
        "        solved_runtime_all = solved_df_all[f\"{tool}-runtime\"]\n",
        "        solved_runtime_int = solved_df_int[f\"{tool}-runtime\"]\n",
        "        # avg_time[tool] = solved_runtime.mean()\n",
        "        # std_time[tool] = solved_runtime.std()\n",
        "        # total_time[tool] = solved_runtime.sum()\n",
        "        solved_total_all[tool] += len(solved_df_all)\n",
        "        solved_total_int[tool] += len(solved_df_int)\n",
        "\n",
        "        avg_and_std_line[tool] += f\" & {print_num(solved_runtime_all.mean())} & {print_num(solved_runtime_all.std())}\"\n",
        "        # avg_and_std_line[tool] += f\" & {print_num(solved_runtime_all.mean())} & {print_num(solved_runtime_int.mean())} & {print_num(solved_runtime_all.std())} & {print_num(solved_runtime_int.std())}\"\n",
        "\n",
        "        tool_lines[bench_name][tool] = [\n",
        "            len(solved_df_all),\n",
        "            len(solved_df_int),\n",
        "            len(df_all[(df_all[tool + \"-result\"] == \" unknown\")]),\n",
        "            len(df_int[(df_int[tool + \"-result\"] == \" unknown\")]),\n",
        "            len(df_all[(df_all[tool + \"-result\"] == \"ERR\")|(df_all[tool + \"-result\"] == \"TO\")]),\n",
        "            len(df_int[(df_int[tool + \"-result\"] == \"ERR\")|(df_int[tool + \"-result\"] == \"TO\")]),\n",
        "                # f\"{num_of_unsolved[tool]}\",\n",
        "                # f\"{unknowns[tool]}\",\n",
        "                # f\"{TOs[tool]}\",\n",
        "                # f\"{MOs[tool]}\",\n",
        "                # f\"{total_time[tool]:.2f}\",\n",
        "                # f\"{solved_runtime.median()}\",\n",
        "                # f\"{avg_time[tool]:.2f}\",\n",
        "                # f\"{std_time[tool]:.2f}\",\n",
        "            ]\n",
        "\n",
        "for tool in tools_for_comparison:\n",
        "    if tool == NOODLER_FOR_BENCHMARK:\n",
        "        print(R\"\\rowcolor{yellow}\")\n",
        "    line = tool_latex_mapping[tool]\n",
        "    for bench in benches:\n",
        "        def is_min_in_col(col_num, num):\n",
        "            return (num == min([val[col_num] for val in tool_lines[bench[0]].values()]))\n",
        "        def is_max_in_col(col_num, num):\n",
        "            return (num == max([val[col_num] for val in tool_lines[bench[0]].values()]))\n",
        "        for idx, tl in enumerate(tool_lines[bench[0]][tool]):\n",
        "            line += \" & \"\n",
        "            if (idx < 2 and is_max_in_col(idx, tl)) or (idx >= 2 and is_min_in_col(idx,tl)):\n",
        "                line += R\"\\ping \"\n",
        "            line += print_num(tl)\n",
        "    line += \" & \"\n",
        "    tl = solved_total_all[tool]\n",
        "    if tl == max(solved_total_all.values()):\n",
        "        line += R\"\\ping \"\n",
        "    line += print_num(tl)\n",
        "    line += \" & \"\n",
        "    tl = solved_total_int[tool]\n",
        "    if tl == max(solved_total_int.values()):\n",
        "        line += R\"\\ping \"\n",
        "    line += print_num(tl)\n",
        "    print(f\"{line}\\\\\\\\\")\n",
        "print(R\"\"\"\\bottomrule\n",
        "\\end{tabular}\"\"\")"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "print(R\"\"\"\\newcolumntype{g}{>{\\columncolor{gray!30}}r}\n",
        "\\newcolumntype{h}{>{\\columncolor{gray!30}}c}\"\"\")\n",
        "print(R\"\"\"\\begin{tabular}{lggrrgg}\"\"\")\n",
        "# print(R\"\"\"\\begin{tabular}{lggggrrrrgggg}\"\"\")\n",
        "print(R\"\"\"\\toprule\"\"\")\n",
        "bench_name_line = \"\"\n",
        "top_line = \"\"\n",
        "# top_line2 = \"\"\n",
        "col_type = \"h\"\n",
        "for bench in benches:\n",
        "    bench_name_line += f\" & \\\\multicolumn{{2}}{{{col_type}}}{{{bench[1]}}}\"\n",
        "    top_line += f\" & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\textbf{{\\\\emph{{avg}}}}}} & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\textbf{{\\\\emph{{std}}}}}}\"\n",
        "    # bench_name_line += f\" & \\\\multicolumn{{4}}{{{col_type}}}{{{bench[1]}}}\"\n",
        "    # top_line += f\" & \\\\multicolumn{{2}}{{{col_type}}}{{\\\\textbf{{\\\\emph{{avg}}}}}} & \\\\multicolumn{{2}}{{{col_type}}}{{\\\\textbf{{\\\\emph{{std}}}}}}\"\n",
        "    # top_line2 += f\" & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\textbf{{\\\\emph{{all}}}}}} & \\\\multicolumn{{1}}{{{col_type}}}{{\\\\emph{{conv}}}}\"*2\n",
        "    if (col_type == \"h\"):\n",
        "        col_type = \"c\"\n",
        "    else:\n",
        "        col_type = \"h\"\n",
        "print(bench_name_line + R\"\\\\\")\n",
        "print(top_line + R\"\\\\\")\n",
        "# print(top_line2 + R\"\\\\\")\n",
        "print(R\"\\midrule\")\n",
        "for tool in tools_for_comparison:\n",
        "    if tool == NOODLER_FOR_BENCHMARK:\n",
        "        print(R\"\\rowcolor{yellow}\")\n",
        "    print(avg_and_std_line[tool] + R\"\\\\\")\n",
        "print(R\"\"\"\\bottomrule\n",
        "\\end{tabular}\"\"\")"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "for tool in tools_for_comparison:\n",
        "    if tool != NOODLER_FOR_BENCHMARK:\n",
        "        dfff = pd.concat([bench[2] for bench in benches])\n",
        "        scat = scatter_plot(dfff, xcol=f'{NOODLER_FOR_BENCHMARK}-runtime', ycol= f'{tool}-runtime',\n",
        "                            xname=\"Z3-Noodler\",        yname=f\"{tool_names_mapping[tool]}\",\n",
        "                            domain=[TIME_MIN, 120], tickCount=3, log=True, width=6, height=6, show_legend=False)\n",
        "        print(scat)\n",
        "        scat.save(filename=f\"all_noodler_vs_{tool_names_mapping[tool]}.pdf\", dpi=500, verbose = False)\n",
        "        dfff = pd.concat([bench[3] for bench in benches])\n",
        "        scat = scatter_plot(dfff, xcol=f'{NOODLER_FOR_BENCHMARK}-runtime', ycol= f'{tool}-runtime',\n",
        "                            xname=\"Z3-Noodler\",        yname=f\"{tool_names_mapping[tool]}\",\n",
        "                            domain=[TIME_MIN, 120], tickCount=3, log=True, width=6, height=6, show_legend=False)\n",
        "        print(scat)\n",
        "        scat.save(filename=f\"int_noodler_vs_{tool_names_mapping[tool]}.pdf\", dpi=500, verbose = False)"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "### Stuff to generate tables and graphs for TACAS'24 paper:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "NOODLER_FOR_BENCHMARK = \"z3-noodler-f211b89-bb85433\"\n",
        "CVC5 = \"cvc5-1.0.8\"\n",
        "Z3 = \"z3-4.12.2\"\n",
        "Z3STR4 = \"z3str4\"\n",
        "OSTRICH = \"ostrich-70d01e2d2\"\n",
        "Z3STR3RE = \"z3strRE\"\n",
        "Z3TRAU = \"z3-trau-1.1\"\n",
        "OLD_NOODLER = \"z3-noodler-9f5e602-199b36d\"\n",
        "\n",
        "BENCHES_IGNORE_UNKNOWN = [\"stringfuzz\", \"webapp\", \"full_str_int\", \"str_small_rw\"]\n",
        "\n",
        "# for poster\n",
        "NOODLER_FOR_BENCHMARK = \"z3-noodler-0751e1e-2cddb2f\" # noodler 1.1\n",
        "CVC5 = \"cvc5-1.1.2\"\n",
        "Z3 = \"z3-4.13.0\"\n",
        "OSTRICH = \"ostrich-5dd2e10ca\"\n",
        "OLD_NOODLER = \"z3-noodler-fb447e3-2cddb2f\" # noodler 1.0 (only for presentation scatter plot)\n",
        "\n",
        "BENCHES_IGNORE_UNKNOWN = [\"webapp\"]\n",
        "\n",
        "tools_for_comparison = [\n",
        "    NOODLER_FOR_BENCHMARK,\n",
        "    CVC5,\n",
        "    Z3,\n",
        "    Z3STR4,\n",
        "    OSTRICH,\n",
        "    Z3STR3RE,\n",
        "    # Z3TRAU,\n",
        "    OLD_NOODLER,\n",
        "]\n",
        "\n",
        "#\n",
        "tool_latex_mapping = {\n",
        "    NOODLER_FOR_BENCHMARK : \"\\\\ziiinoodler\",\n",
        "    CVC5 : \"\\\\cvcv\",\n",
        "    Z3 : \"\\\\ziii\",\n",
        "    Z3STR4 : \"\\\\ziiistriv\",\n",
        "    OSTRICH : \"\\\\ostrich\",\n",
        "    Z3STR3RE : \"\\\\ziiistriiire\",\n",
        "    Z3TRAU : \"\\\\ziiitrau\",\n",
        "    OLD_NOODLER : \"\\\\ziiinoodleroopsla\",\n",
        "}\n",
        "tool_names_mapping = {\n",
        "    NOODLER_FOR_BENCHMARK : \"Z3-Noodler 1.1\",\n",
        "    CVC5 : \"cvc5\",\n",
        "    Z3 : \"Z3\",\n",
        "    Z3STR4 : \"Z3stsr4\",\n",
        "    OSTRICH : \"OSTRICH\",\n",
        "    Z3STR3RE : \"Z3str3RE\",\n",
        "    Z3TRAU : \"Z3-Trau\",\n",
        "    OLD_NOODLER : \"Z3-Noodler 1.0\",\n",
        "}\n",
        "tool_file_names_mapping = {\n",
        "    NOODLER_FOR_BENCHMARK : \"noodler\",\n",
        "    CVC5 : \"cvc5\",\n",
        "    Z3 : \"z3\",\n",
        "    Z3STR4 : \"z3str4\",\n",
        "    OSTRICH : \"ostrich\",\n",
        "    Z3STR3RE : \"z3str3re\",\n",
        "    Z3TRAU : \"z3trau\",\n",
        "    OLD_NOODLER : \"old_noodler\",\n",
        "}\n",
        "bench_mapping = {\n",
        "    \"automatark\" : \"\\\\automatark\",\n",
        "    \"denghang\" : \"\\\\denghang\",\n",
        "    \"stringfuzz\" : \"\\\\stringfuzz\",\n",
        "    \"sygus_qgen\" : \"\\sygusqgen\",\n",
        "    \"kaluza\" : \"\\\\kaluza\",\n",
        "    \"kepler\" : \"\\\\keplerbench\",\n",
        "    \"norn\" : \"\\\\nornbench\",\n",
        "    \"slent\" : \"\\\\slent\",\n",
        "    \"slog\" : \"\\\\slog\",\n",
        "    \"webapp\" : \"\\\\webapp\",\n",
        "    \"woorpje\" : \"\\\\woorpje\",\n",
        "    \"full_str_int\" : \"\\\\fullstrint\",\n",
        "    \"leetcode\" : \"\\\\leetcode\",\n",
        "    \"str_small_rw\" : \"\\\\strsmall\",\n",
        "    \"pyex\" : \"\\\\pyex\",\n",
        "    \"transducer_plus\" : \"\\\\transducerplus\",\n",
        "}\n",
        "bench_div = {\n",
        "    \"Regex\" : [\"automatark\", \"denghang\", \"stringfuzz\", \"sygus_qgen\"],\n",
        "    \"Equations\" : [\"kaluza\", \"kepler\", \"norn\", \"slent\", \"slog\", \"webapp\", \"woorpje\"],\n",
        "    \"Predicates\" : [\"full_str_int\", \"leetcode\", \"str_small_rw\"],# \"pyex\", \"transducer_plus\"],\n",
        "    \"\" : [\"pyex\"]\n",
        "}\n",
        "bench_div_mapping = {\n",
        "    \"Regex\" : \"\\\\regexbench\",\n",
        "    \"Equations\" : \"\\\\eqbench\",\n",
        "    \"Predicates\" : \"\\\\predbench\",\n",
        "    \"\" : \"\",\n",
        "}"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "\n",
        "# bench_div = { n : [n] for n in [\"automatark\", \"denghang\", \"stringfuzz\", \"sygus_qgen\", \"kaluza\", \"kepler\", \"norn\", \"slent\", \"slog\", \"webapp\", \"woorpje\", \"full_str_int\", \"leetcode\", \"str_small_rw\", \"pyex\"] }\n",
        "table = dict()\n",
        "dfs_here = []\n",
        "for benchset, benchmarks in bench_div.items():\n",
        "    dfs = []\n",
        "    for bench in benchmarks:\n",
        "        df = read_file_no_nan(bench + \"/to120.csv\")\n",
        "        if bench in BENCHES_IGNORE_UNKNOWN:\n",
        "            df = df[df[f\"{NOODLER_FOR_BENCHMARK}-result\"] != \" unknown\"]\n",
        "        dfs.append(df)\n",
        "    df = pd.concat(dfs)\n",
        "    df = df[[\"name\"] + [f\"{tool}-result\" for tool in tools_for_comparison] + [f\"{tool}-runtime\" for tool in tools_for_comparison]]\n",
        "    total = len(df)\n",
        "\n",
        "    # we can help ostrich by substracting some value pretending it is the time for java to start\n",
        "    # ostrich_solved = df[(df[\"{OSTRICH}-result\"] == \" sat\")|(df[\"{OSTRICH}-result\"] == \" unsat\")]\n",
        "    # df.loc[(df[\"{OSTRICH}-result\"] == \" sat\")|(df[\"{OSTRICH}-result\"] == \" unsat\"), \"{OSTRICH}-runtime\"] = (ostrich_solved['{OSTRICH}-runtime'].astype(float)- 1.3).astype(str)\n",
        "\n",
        "    total_time_for_tools = 0\n",
        "\n",
        "    for tool in tools_for_comparison:\n",
        "        df.loc[(df[f\"{tool}-result\"] != \" sat\")&(df[f\"{tool}-result\"] != \" unsat\"), f\"{tool}-runtime\"] = 120\n",
        "        df[f\"{tool}-runtime\"] = df[f\"{tool}-runtime\"].astype(float)\n",
        "\n",
        "        solved = df[(df[tool + \"-result\"] == \" sat\") | (df[tool + '-result'] == \" unsat\")]\n",
        "        unknown_sum = len(df[df[tool + \"-result\"] == \" unknown\"])\n",
        "        solved_num = len(solved)\n",
        "        solved_runtime = solved[f\"{tool}-runtime\"].astype(float)\n",
        "        # solved_runtime = df[f\"{tool}-runtime\"].astype(float)\n",
        "        solved_avg = solved_runtime.mean()\n",
        "        solved_median = solved_runtime.median()\n",
        "        solved_total = solved_runtime.sum()\n",
        "        total_time_for_tools += solved_total\n",
        "        solved_std_deviation = solved_runtime.std()\n",
        "        table.setdefault(tool_latex_mapping[tool], []).extend(\n",
        "            [\n",
        "                # total - solved_num,\n",
        "                solved_total,\n",
        "                # solved_avg,\n",
        "                # solved_median,\n",
        "                # solved_std_deviation,\n",
        "            ])\n",
        "    \n",
        "    # table.setdefault(\"sum\", []).extend([(total_time_for_tools/60)/60])\n",
        "\n",
        "\n",
        "    # virtual best\n",
        "    def add_vbs_from_tools(tools_list, name_for_vbs, latex_name_for_vbs):\n",
        "        df[name_for_vbs] = df[[f\"{tool}-runtime\" for tool in tools_list]].min(axis=1)\n",
        "        solved_vbs = df[df[name_for_vbs] != 120][name_for_vbs]\n",
        "        table.setdefault(latex_name_for_vbs, []).extend(\n",
        "            [\n",
        "                # total - len(solved_vbs),\n",
        "                solved_vbs.sum(),\n",
        "                # solved_vbs.mean(),\n",
        "                # solved_vbs.median(),\n",
        "                # solved_vbs.std(),\n",
        "            ])\n",
        "    tools_without_old_noodler = [tool for tool in tools_for_comparison if tool != OLD_NOODLER]\n",
        "    add_vbs_from_tools(tools_without_old_noodler, \"vbs\", \"\\\\vbs\")\n",
        "    for tool in tools_without_old_noodler:\n",
        "        add_vbs_from_tools([tool1 for tool1 in tools_without_old_noodler if tool1 != tool], f\"vbs-{tool}\", f\"\\\\vbs - {tool_latex_mapping[tool]}\")\n",
        "    # add_vbs_from_tools([CVC5, Z3, NOODLER_FOR_BENCHMARK], \"cvc5-z3-noodler\", f\"{tool_latex_mapping[CVC5]} + {tool_latex_mapping[Z3]} + {tool_latex_mapping[NOODLER_FOR_BENCHMARK]}\")\n",
        "    # add_vbs_from_tools([CVC5, Z3], \"cvc5-z3\", f\"{tool_latex_mapping[CVC5]} + {tool_latex_mapping[Z3]}\")\n",
        "\n",
        "    df[\"benchmark\"] = benchset\n",
        "    dfs_here.append(df)\n",
        "dfff = pd.concat(dfs_here)\n",
        "\n",
        "header = pd.MultiIndex.from_product(\n",
        "    [\n",
        "        # ['Reg','Eq','Pred','Pyex'],\n",
        "        list(bench_div.keys()),\n",
        "        # ['Unsolved','Total time','Avg','Med','Std']\n",
        "        ['Total time']\n",
        "    ], names=['',''])\n",
        "# table_df = pd.DataFrame.from_dict(table, 'index', columns=header)\n",
        "# table_df = table_df.style.format(precision=2)#, decimal=',', thousands='.')\n",
        "# print(table_df.to_latex())\n",
        "with pd.option_context('display.float_format', '{:0.2f}'.format):\n",
        "    print(pd.DataFrame.from_dict(table, 'index', columns=header).to_string())\n",
        "\n",
        "for tool in [CVC5, Z3]:\n",
        "    if tool != NOODLER_FOR_BENCHMARK:\n",
        "        scat = scatter_plot(dfff, xcol=f'{NOODLER_FOR_BENCHMARK}-runtime', ycol= f'{tool}-runtime',\n",
        "                            xname=tool_names_mapping[NOODLER_FOR_BENCHMARK],        yname=tool_names_mapping[tool],\n",
        "                            domain=[TIME_MIN, 120], tickCount=3, log=True, width=6, height=6, show_legend=False)\n",
        "        print(scat)\n",
        "        scat.save(filename=f\"{tool_file_names_mapping[NOODLER_FOR_BENCHMARK]}_vs_{tool_file_names_mapping[tool]}.pdf\", dpi=500, verbose = False)\n",
        "\n",
        "# scat_vbs = scatter_plot(dfff, xcol=f'{NOODLER_FOR_BENCHMARK}-runtime', ycol= f'vbs-{NOODLER_FOR_BENCHMARK}',\n",
        "#                     xname=tool_names_mapping[NOODLER_FOR_BENCHMARK],        yname=\"Virtual Best Solver\",\n",
        "#                     domain=[TIME_MIN, 120], tickCount=3, log=True, width=6, height=6, show_legend=False)\n",
        "# print(scat_vbs)\n",
        "# scat_vbs.save(filename=f\"{tool_file_names_mapping[NOODLER_FOR_BENCHMARK]}_vs_vbs.pdf\", dpi=500, verbose = False)\n",
        "\n",
        "# scat_vbs = scatter_plot(dfff, xcol=f'{NOODLER_FOR_BENCHMARK}-runtime', ycol= f'cvc5-z3',\n",
        "#                     xname=\"Noodler\",        yname=\"cvc5 + Z3\",\n",
        "#                     domain=[TIME_MIN, 120], tickCount=3, log=True, width=6, height=6, show_legend=False)\n",
        "# print(scat_vbs)\n",
        "# scat_vbs.save(filename=f\"{tool_file_names_mapping[NOODLER_FOR_BENCHMARK]}_vs_{tool_file_names_mapping[CVC5]}_and_{tool_file_names_mapping[Z3]}.pdf\", dpi=500, verbose = False)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "print(R\"\"\"\\newcolumntype{g}{>{\\columncolor{gray!30}}r}\n",
        "\\newcolumntype{f}{>{\\columncolor{gray!30}}l}\n",
        "\\newcolumntype{h}{>{\\columncolor{gray!30}}c}\"\"\")\n",
        "\n",
        "# for printing best\n",
        "print(R\"\\newcommand{\\ping}[0]{\\bf}\")\n",
        "\n",
        "# for printing those that have wrong results\n",
        "print(R\"\"\"\\newcommand{\\wrongres}[2]{${}^*${#1}}\n",
        "% if you want wrong results to be shown in parentheses, uncomment this\n",
        "% \\newcommand{\\wrongres}[2]{${}^*${#1}({#2})}\"\"\")\n",
        "\n",
        "tabular_begin = R\"\\begin{tabular}{l\"\n",
        "col_type = \"g\"\n",
        "for benches in bench_div.values():\n",
        "    tabular_begin += (len(benches)+1)*col_type\n",
        "    if col_type == \"g\":\n",
        "        col_type = \"r\"\n",
        "    else:\n",
        "        col_type = \"g\"\n",
        "print(tabular_begin + R\"\"\"}\n",
        "\\toprule\"\"\")\n",
        "\n",
        "header_line1 = \"\"\n",
        "header_line2 = \"\"\n",
        "usedbenchmarks = 2\n",
        "cmidrules = \"\"\n",
        "col_type = \"h\"\n",
        "for bench_cat, bench_set in bench_div.items():\n",
        "    num_of_bench = len(bench_set) + 1\n",
        "    header_line1 += f\" & \\\\multicolumn{{{num_of_bench}}}{{{col_type}}}{{{bench_div_mapping[bench_cat]}}}\"\n",
        "    cmidrules += f\"\\\\cmidrule(lr){{{usedbenchmarks}-{usedbenchmarks+num_of_bench-1}}}\"\n",
        "    usedbenchmarks += num_of_bench\n",
        "    header_line2 += \" & \" + \" & \".join(f\"\\\\multicolumn{{1}}{{{col_type}}}{{{bench_mapping[bench]}short}}\" for bench in bench_set)\n",
        "    if len(bench_set) != 1:\n",
        "        header_line2 += f\" & \\\\multicolumn{{1}}{{{col_type}}}{{$\\\\Sigma$}}\"\n",
        "    if col_type == \"h\":\n",
        "        col_type = \"c\"\n",
        "    else:\n",
        "        col_type = \"h\"\n",
        "print(header_line1 + \"\\\\\\\\\" + cmidrules)\n",
        "print(header_line2 + \"\\\\\\\\\")\n",
        "\n",
        "def printNum(num):\n",
        "    # return f\"\\\\num{{{num}}}\"\n",
        "    return str(num)\n",
        "def getRealSolved(solved, total, incorrect_num):\n",
        "    return total-solved+incorrect_num\n",
        "def printSolved(solved, total, incorrect_num):\n",
        "    return printNum(getRealSolved(solved, total, incorrect_num))\n",
        "    # return printNum(num+incorrect_num)\n",
        "\n",
        "totals = []\n",
        "throwaways = []\n",
        "solved_for_tools = dict()\n",
        "for bench_set in bench_div.values():\n",
        "    solved_for_tools_nums = dict()\n",
        "    tools_with_incorrect_results = []\n",
        "    totals_here = []\n",
        "    throwaways_here = []\n",
        "    for bench in bench_set:\n",
        "        df = read_file_no_nan(bench + \"/to120.csv\")\n",
        "\n",
        "        realtotal = len(df)\n",
        "        if bench in BENCHES_IGNORE_UNKNOWN:\n",
        "            df = df[df[f\"{NOODLER_FOR_BENCHMARK}-result\"] != \" unknown\"]\n",
        "        throwaw = realtotal - len(df)\n",
        "        throwaways_here.append(throwaw)\n",
        "        throwaways.append(str(throwaw))\n",
        "        total = len(df)\n",
        "        totals_here.append(total)\n",
        "        totals.append(str(total))\n",
        "\n",
        "        best = 0\n",
        "        for tool in tools_for_comparison:\n",
        "            solved_num = len(df[(df[tool + \"-result\"] == \" sat\") | (df[tool + '-result'] == \" unsat\")])\n",
        "            # get the number of incorrect results for tool for given bench (by checking if cvc5 or z3 (or z3-noodler) gives different result)\n",
        "            incorrect_num = len(df[\n",
        "                ((df[tool + \"-result\"] == \" sat\") & \n",
        "                    (\n",
        "                        (df[f\"{CVC5}-result\"] == \" unsat\")\n",
        "                        | (df[f\"{Z3}-result\"] == \" unsat\")\n",
        "                        #| (df[f\"{NOODLER_FOR_BENCHMARK}-result\"] == \" unsat\")\n",
        "                    )) |\n",
        "                ((df[tool + \"-result\"] == \" unsat\") &\n",
        "                    (\n",
        "                        (df[f\"{CVC5}-result\"] == \" sat\")\n",
        "                        | (df[f\"{Z3}-result\"] == \" sat\")\n",
        "                        #| (df[f\"{NOODLER_FOR_BENCHMARK}-result\"] == \" sat\")\n",
        "                    ))\n",
        "                ])\n",
        "\n",
        "            tool_latex = tool_latex_mapping[tool]\n",
        "            solved_for_tools_nums.setdefault(tool_latex, []).append(getRealSolved(solved_num, total, incorrect_num))\n",
        "            if incorrect_num == 0:\n",
        "                # no incorrect results, we use the solved_num to compute the best\n",
        "                solved_for_tools.setdefault(tool_latex, []).extend([printSolved(solved_num, total, incorrect_num)])\n",
        "                best = max(best, solved_num)\n",
        "            else:\n",
        "                # if there are different results, we print * before the number...\n",
        "                solved_for_tools.setdefault(tool_latex, []).extend([f\"\\\\wrongres{{{printSolved(solved_num, total, incorrect_num)}}}{{{incorrect_num}}}\"])\n",
        "                tools_with_incorrect_results.append(tool_latex)\n",
        "        \n",
        "        # best tool should be marked\n",
        "        for tool in solved_for_tools.keys():\n",
        "            if solved_for_tools[tool][-1] == printSolved(best, total, 0):\n",
        "                solved_for_tools[tool][-1] = f\"\\\\ping {printSolved(best, total, 0)}\"\n",
        "\n",
        "\n",
        "    if len(bench_set) != 1:\n",
        "        num_of_bench = len(bench_set)\n",
        "        totals.append(sum(totals_here))\n",
        "        throwaways.append(sum(throwaways_here))\n",
        "        solved_for_tools_nums = { tool : sum(solved) for tool,solved in solved_for_tools_nums.items()}\n",
        "        best = min(solved for tool,solved in solved_for_tools_nums.items() if tool not in tools_with_incorrect_results)\n",
        "        for tool,num in solved_for_tools_nums.items():\n",
        "            if tool in tools_with_incorrect_results:\n",
        "                solved_for_tools[tool].append(f\"\\\\wrongres{{{printNum(num)}}}{{0}}\")\n",
        "            else:\n",
        "                if num == best:\n",
        "                    solved_for_tools[tool].append(f\"\\\\ping {printNum(num)}\")\n",
        "                else:\n",
        "                    solved_for_tools[tool].append(f\"{printNum(num)}\")\n",
        "\n",
        "\n",
        "        \n",
        "print(R\"\\emph{Included} & \" + \" & \".join(printNum(tot) for tot in totals) + \"\\\\\\\\\")\n",
        "print(R\"\\emph{Unsupported} & \" + \" & \".join(printNum(thr) for thr in throwaways) + \"\\\\\\\\\")\n",
        "print(R\"\\midrule\")\n",
        "for tool, results in solved_for_tools.items():\n",
        "    if tool == tool_latex_mapping[NOODLER_FOR_BENCHMARK]:\n",
        "        print(R\"\\rowcolor{yellow}\")\n",
        "    print(f\"{tool} & {' & '.join(results)}\\\\\\\\\")\n",
        "print(R\"\\bottomrule\")\n",
        "print(R\"\\end{tabular}\")"
      ]
    }
  ],
  "metadata": {
    "colab": {
      "provenance": []
    },
    "kernelspec": {
      "display_name": "Python 3.11.8 64-bit",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "file_extension": ".py",
      "mimetype": "text/x-python",
      "name": "python",
      "nbconvert_exporter": "python",
      "pygments_lexer": "ipython3",
      "version": "3.11.7"
    },
    "vscode": {
      "interpreter": {
        "hash": "5c7b89af1651d0b8571dde13640ecdccf7d5a6204171d6ab33e7c296e100e08a"
      }
    }
  },
  "nbformat": 4,
  "nbformat_minor": 0
}