playground.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "! pip install sympy==1.13.0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "! pip install predi"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def debug_print(message):\n",
    "    #print(f\"{message}\")\n",
    "    pass"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [],
   "source": [
    "import sympy as sp\n",
    "from typing import Union\n",
    "from src.predi.parser import ASTNode\n",
    "from src.predi.config import debug_print\n",
    "\n",
    "class Simplifier:\n",
    "    def __init__(self):\n",
    "        self.symbols = {\n",
    "            'msg.sender': sp.Symbol('msg_sender'),\n",
    "            'msg.origin': sp.Symbol('msg_origin'),\n",
    "            '==': sp.Eq,\n",
    "            '!=': sp.Ne,\n",
    "            '>=': sp.Ge,\n",
    "            '<=': sp.Le,\n",
    "            '>': sp.Gt,\n",
    "            '<': sp.Lt,\n",
    "            '&&': sp.And,\n",
    "            '||': sp.Or,\n",
    "            '!': sp.Not\n",
    "        }\n",
    "\n",
    "    def simplify(self, ast: ASTNode) -> Union[str, ASTNode]:\n",
    "        #debug_print(f\"Simplifying AST: {ast}\")\n",
    "        sympy_expr = self._to_sympy(ast)\n",
    "        #debug_print(f\"Converted to sympy expression: {sympy_expr}\")\n",
    "        simplified_expr = sp.simplify(sympy_expr)\n",
    "        #debug_print(f\"Simplified sympy expression: {simplified_expr}\")\n",
    "        simplified_ast = self._to_ast(simplified_expr)\n",
    "        #debug_print(f\"Converted back to AST: {simplified_ast}\")\n",
    "        return simplified_ast\n",
    "\n",
    "    def _to_sympy(self, node: ASTNode):\n",
    "        if node.value in self.symbols and not node.children:\n",
    "            return self.symbols[node.value]\n",
    "        elif node.value in self.symbols:\n",
    "            if node.value in ('&&', '||'):\n",
    "                return self.symbols[node.value](*[self._to_sympy(child) for child in node.children])\n",
    "            elif node.value == '!':\n",
    "                return self.symbols[node.value](self._to_sympy(node.children[0]))\n",
    "            elif len(node.children) == 2:\n",
    "                return self.symbols[node.value](self._to_sympy(node.children[0]), self._to_sympy(node.children[1]))\n",
    "            else:\n",
    "                raise ValueError(f\"Invalid number of children for operator {node.value}\")\n",
    "        elif isinstance(node.value, (int, float)):\n",
    "            return sp.Number(node.value)\n",
    "        else:\n",
    "            # Preserve function calls and other identifiers as-is\n",
    "            if '(' in node.value and ')' in node.value:\n",
    "                func_name = node.value  # Ensure the function name is preserved entirely\n",
    "                args = node.children\n",
    "                return sp.Function(func_name)(*map(self._to_sympy, args))\n",
    "            else:\n",
    "                return sp.Symbol(node.value.replace('.', '_'))\n",
    "\n",
    "    def _to_ast(self, expr):\n",
    "        if isinstance(expr, sp.Equality):\n",
    "            return ASTNode('==', [self._to_ast(expr.lhs), self._to_ast(expr.rhs)])\n",
    "        elif isinstance(expr, sp.Rel):\n",
    "            op_map = {'>': '>', '<': '<', '>=': '>=', '<=': '<=', '!=': '!='}\n",
    "            return ASTNode(op_map[expr.rel_op], [self._to_ast(expr.lhs), self._to_ast(expr.rhs)])\n",
    "        elif isinstance(expr, sp.And):\n",
    "            return ASTNode('&&', [self._to_ast(arg) for arg in expr.args])\n",
    "        elif isinstance(expr, sp.Or):\n",
    "            return ASTNode('||', [self._to_ast(arg) for arg in expr.args])\n",
    "        elif isinstance(expr, sp.Not):\n",
    "            return ASTNode('!', [self._to_ast(expr.args[0])])\n",
    "        elif isinstance(expr, sp.Function):\n",
    "            func_name = str(expr.func)\n",
    "            return ASTNode(func_name, [self._to_ast(arg) for arg in expr.args])\n",
    "        else:\n",
    "            return ASTNode(str(expr))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "predicate1: !(a > 5 && b < 3)\n",
      "AST1 is: ASTNode(value='!', children=[ASTNode(value='&&', children=[ASTNode(value='>', children=[ASTNode(value='a', children=[]), ASTNode(value='5', children=[])]), ASTNode(value='<', children=[ASTNode(value='b', children=[]), ASTNode(value='3', children=[])])])])\n",
      "Simplified AST1: ASTNode(value='||', children=[ASTNode(value='>=', children=[ASTNode(value='5', children=[]), ASTNode(value='a', children=[])]), ASTNode(value='<=', children=[ASTNode(value='3', children=[]), ASTNode(value='b', children=[])])])\n",
      "--------------------------------------------------------------------------------------------\n",
      "predicate1: a <= 5 || b >= 3\n",
      "AST2 is: ASTNode(value='||', children=[ASTNode(value='<=', children=[ASTNode(value='a', children=[]), ASTNode(value='5', children=[])]), ASTNode(value='>=', children=[ASTNode(value='b', children=[]), ASTNode(value='3', children=[])])])\n",
      "Simplified AST1: ASTNode(value='||', children=[ASTNode(value='>=', children=[ASTNode(value='5', children=[]), ASTNode(value='a', children=[])]), ASTNode(value='<=', children=[ASTNode(value='3', children=[]), ASTNode(value='b', children=[])])])\n"
     ]
    }
   ],
   "source": [
    "\n",
    "tokenizer = Tokenizer()\n",
    "simplifier = Simplifier()\n",
    "\n",
    "tokens1 = tokenizer.tokenize(predicate1)\n",
    "parser1 = Parser(tokens1)\n",
    "ast1 = parser1.parse()\n",
    "simplified_ast1 = simplifier.simplify(ast1)\n",
    "\n",
    "print(f\"predicate1: {predicate1}\")\n",
    "print(f\"AST1 is: {ast1}\")\n",
    "print(f\"Simplified AST1: {simplified_ast1}\")\n",
    "\n",
    "\n",
    "print('--------------------------------------------------------------------------------------------')\n",
    "\n",
    "tokens2 = tokenizer.tokenize(predicate2)\n",
    "parser2 = Parser(tokens2)\n",
    "ast2 = parser2.parse()\n",
    "simplified_ast2 = simplifier.simplify(ast2)\n",
    "\n",
    "print(f\"predicate1: {predicate2}\")\n",
    "print(f\"AST2 is: {ast2}\")\n",
    "print(f\"Simplified AST1: {simplified_ast2}\")\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "predicate1, predicate2 = \"(_tTotalpercentBuy)/divisorBuy>=(_tTotal/5000)\", \"(percentBuy_decimals)/divisorBuy>=(_tTotal/10000)\"\n",
    "comparator = Comparator()\n",
    "result = comparator.compare(predicate1, predicate2)\n",
    "print(result)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from datasets import load_dataset\n",
    "\n",
    "ds = load_dataset(\"GGmorello/FLAMES_results\", \"100k\", token='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')\n",
    "\n",
    "#ds = load_dataset('GGmorello/FLAMES', 'infilled', split='train[:10000]', token='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', cache_dir='/Users/mojtabaeshghie/.cache/hf')#, num_proc=8)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "df_100k = ds['train'].to_pandas()\n",
    "df_100k.head()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from predi.comparator import Comparator\n",
    "comparator = Comparator()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from tqdm import tqdm\n",
    "\n",
    "df_100k = ds['train'].to_pandas()\n",
    "head_100 = df_100k.head(100000)\n",
    "predi_failures = []\n",
    "comparison_results = []\n",
    "for i, row in tqdm(df_100k.iterrows(), total=len(df_100k)):\n",
    "    ground_truth = row['predicate']\n",
    "    synthesized = row['results']\n",
    "\n",
    "    # test for exact string match between two predicates (first strip them out of any leading/trailing whitespaces)\n",
    "    if ground_truth.strip() == synthesized.strip():\n",
    "        comparison_results.append({'original_index': i, 'ground_truth': ground_truth, 'synthesized': synthesized, 'result': 'Exact Match'}) \n",
    "        continue\n",
    "    \n",
    "    # if not exact match, we will use predi to compare the two predicates\n",
    "    try:\n",
    "        result = comparator.compare(ground_truth, synthesized)\n",
    "        comparison_results.append({'original_index': i, 'ground_truth': ground_truth, 'synthesized': synthesized, 'result': result})        \n",
    "        #print(f\"({i}) For predicates {pred1} ************* {pred2} ############## {result}\")\n",
    "    except Exception as e:\n",
    "        comparison_results.append({'original_index': i, 'ground_truth': ground_truth, 'synthesized': synthesized, 'result': 'The predicates are not equivalent and neither is stronger.'})\n",
    "        predi_failures.append(({'index': i, 'ground_truth': ground_truth, 'synthesized': synthesized, 'exception': e}))\n",
    "        continue\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "len(comparison_results)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "len(predi_failures)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "comparison_results[0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import csv\n",
    "\n",
    "filename = 'comparison_results.csv'\n",
    "\n",
    "header = comparison_results[0].keys()\n",
    "\n",
    "with open(filename, 'w', newline='') as csvfile:\n",
    "    writer = csv.DictWriter(csvfile, fieldnames=header)\n",
    "    writer.writeheader()\n",
    "    writer.writerows(comparison_results[0:5000])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# retrieve 100 random rows from comparison_results with the result 'Exact Match'\n",
    "import random\n",
    "\n",
    "equivalences = [row for row in comparison_results if row['result'] == 'The predicates are equivalent.']\n",
    "\n",
    "# store the results in a csv file\n",
    "filename = 'equivalences.csv'\n",
    "\n",
    "header = equivalences[0].keys()\n",
    "\n",
    "with open(filename, 'w', newline='') as csvfile:\n",
    "    writer = csv.DictWriter(csvfile, fieldnames=header)\n",
    "    writer.writeheader()\n",
    "    writer.writerows(equivalences)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# retrieve 100 random rows from comparison_results with the result 'The second predicate is stronger'\n",
    "import random\n",
    "\n",
    "equivalences = [row for row in comparison_results if row['result'] == 'The second predicate is stronger.']\n",
    "\n",
    "# store the results in a csv file\n",
    "filename = 'synthesized_stronger.csv'\n",
    "\n",
    "header = equivalences[0].keys()\n",
    "\n",
    "with open(filename, 'w', newline='') as csvfile:\n",
    "    writer = csv.DictWriter(csvfile, fieldnames=header)\n",
    "    writer.writeheader()\n",
    "    writer.writerows(equivalences)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# retrieve 100 random rows from comparison_results with the result 'The second predicate is stronger'\n",
    "import random\n",
    "\n",
    "equivalences = [row for row in comparison_results if row['result'] == 'The first predicate is stronger.']\n",
    "\n",
    "# store the results in a csv file\n",
    "filename = 'ground_truth_stronger.csv'\n",
    "\n",
    "header = equivalences[0].keys()\n",
    "\n",
    "with open(filename, 'w', newline='') as csvfile:\n",
    "    writer = csv.DictWriter(csvfile, fieldnames=header)\n",
    "    writer.writeheader()\n",
    "    writer.writerows(equivalences)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from matplotlib import pyplot as plt\n",
    "import matplotlib.patches as mpatches\n",
    "import pandas as pd\n",
    "\n",
    "# Assuming 'comparison_results' is already defined and is a DataFrame\n",
    "data = pd.DataFrame.from_dict(comparison_results[0:5000])\n",
    "\n",
    "# Calculate the result distribution\n",
    "result_distribution = data['result'].value_counts()\n",
    "\n",
    "# Define the updated color palette and use a pattern for the \"Exact Match\" bar\n",
    "color_map_updated = {\n",
    "    \"The predicates are not equivalent and neither is stronger.\": \"#8c8c8c\",\n",
    "    \"Exact Match\": \"#66c2a5\",\n",
    "    \"The predicates are equivalent.\": \"#2ca25f\",\n",
    "    \"The second predicate is stronger.\": \"#fc8d62\",\n",
    "    \"The first predicate is stronger.\": \"#8da0cb\"\n",
    "}\n",
    "\n",
    "# Create the bar plot with the previous color scheme and add pattern for \"Exact Match\"\n",
    "plt.figure(figsize=(7, 5))\n",
    "bars = plt.bar(result_distribution.index, result_distribution.values, color=[color_map_updated.get(result, 'gray') for result in result_distribution.index])\n",
    "\n",
    "# Add patterns to the \"Exact Match\" bar\n",
    "for bar, label in zip(bars, result_distribution.index):\n",
    "    if label == \"Exact Match\":\n",
    "        bar.set_hatch('//')\n",
    "    elif label == \"The predicates are equivalent.\":\n",
    "        bar.set_hatch('xx')\n",
    "\n",
    "# Add numbers on top of the bars with larger font size\n",
    "for bar in bars:\n",
    "    yval = bar.get_height()\n",
    "    plt.text(bar.get_x() + bar.get_width()/2, yval + 30, int(yval), ha='center', va='bottom', fontsize=13)\n",
    "\n",
    "# Set the labels with specified font sizes\n",
    "plt.xlabel('Result', fontsize=13)\n",
    "plt.ylabel('Count', fontsize=13)\n",
    "\n",
    "# Remove x labels and add a legend below the plot with specified font size and updated labels\n",
    "plt.xticks([])\n",
    "legend_labels = [\n",
    "    mpatches.Patch(color=\"#8c8c8c\", label=\"The predicates are not equivalent and neither is stronger.\"),\n",
    "    mpatches.Patch(facecolor=\"#66c2a5\", hatch='//', label=\"Exact match\"),\n",
    "    mpatches.Patch(facecolor=\"#2ca25f\", hatch='xx', label=\"The predicates are equivalent.\"),\n",
    "    mpatches.Patch(color=\"#fc8d62\", label=\"The synthesized is stronger.\"),\n",
    "    mpatches.Patch(color=\"#8da0cb\", label=\"Ground truth is stronger.\")\n",
    "]\n",
    "plt.legend(handles=legend_labels, loc='upper center', bbox_to_anchor=(0.5, -0.15), ncol=1, fontsize=13)\n",
    "\n",
    "# Adjust layout and save the plot as PDF with a suitable size for ACM papers\n",
    "plt.tight_layout()\n",
    "plt.savefig('match_results_distribution_acm_v5.pdf')\n",
    "plt.show()\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from matplotlib import pyplot as plt\n",
    "import matplotlib.patches as mpatches\n",
    "import pandas as pd\n",
    "\n",
    "# Assuming 'comparison_results' is already defined and is a DataFrame\n",
    "data = pd.DataFrame.from_dict(comparison_results[0:5000])\n",
    "\n",
    "# Calculate the result distribution\n",
    "result_distribution = data['result'].value_counts()\n",
    "\n",
    "# Define the updated color palette and use a pattern for the \"Exact Match\" bar\n",
    "color_map_updated = {\n",
    "    \"The predicates are not equivalent and neither is stronger.\": \"#8c8c8c\",\n",
    "    \"Exact Match\": \"#66c2a5\",\n",
    "    \"The predicates are equivalent.\": \"#2ca25f\",\n",
    "    \"The second predicate is stronger.\": \"#fc8d62\",\n",
    "    \"The first predicate is stronger.\": \"#8da0cb\"\n",
    "}\n",
    "\n",
    "# Create the bar plot with the updated color scheme and add patterns for specified bars\n",
    "plt.figure(figsize=(6, 4))\n",
    "bars = plt.bar(result_distribution.index, result_distribution.values, color=[color_map_updated.get(result, 'gray') for result in result_distribution.index])\n",
    "\n",
    "# Add patterns to the \"Exact Match\" and \"The predicates are equivalent.\" bars\n",
    "for bar, label in zip(bars, result_distribution.index):\n",
    "    if label == \"Exact Match\":\n",
    "        bar.set_hatch('//')\n",
    "    elif label == \"The predicates are equivalent.\":\n",
    "        bar.set_hatch('xx')\n",
    "\n",
    "# Adjust the y-axis limits to add space above the bars\n",
    "plt.ylim(0, max(result_distribution.values) * 1.1)\n",
    "\n",
    "# Add numbers on top of the bars with a smaller font size\n",
    "for bar in bars:\n",
    "    yval = bar.get_height()\n",
    "    plt.text(bar.get_x() + bar.get_width()/2, yval + (max(result_distribution.values) * 0.02), int(yval), ha='center', va='bottom', fontsize=10)\n",
    "\n",
    "# Set the labels with specified font sizes\n",
    "plt.xlabel('Result', fontsize=11)\n",
    "plt.ylabel('Count', fontsize=11)\n",
    "\n",
    "# Remove x labels and add a legend below the plot with specified font size and updated labels\n",
    "plt.xticks([])\n",
    "legend_labels = [\n",
    "    mpatches.Patch(color=\"#8c8c8c\", label=\"The predicates are not equivalent and neither is stronger.\"),\n",
    "    mpatches.Patch(facecolor=\"#66c2a5\", hatch='//', label=\"Exact match\"),\n",
    "    mpatches.Patch(facecolor=\"#2ca25f\", hatch='xx', label=\"The predicates are equivalent.\"),\n",
    "    mpatches.Patch(color=\"#fc8d62\", label=\"The synthesized is stronger.\"),\n",
    "    mpatches.Patch(color=\"#8da0cb\", label=\"Ground truth is stronger.\")\n",
    "]\n",
    "plt.legend(handles=legend_labels, loc='upper center', bbox_to_anchor=(0.5, -0.1), ncol=1, fontsize=10)\n",
    "\n",
    "# Adjust layout and save the plot as PDF with a suitable size for ACM papers\n",
    "plt.tight_layout()\n",
    "plt.savefig('match_results_distribution_acm.pdf')\n",
    "plt.show()\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Counting the label and predicates that have `+=` in them"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Convert the Dataset to a pandas DataFrame\n",
    "df_100k = ds['train'].to_pandas()\n",
    "\n",
    "# Filter the rows where 'label' or 'predicate' columns contain \"+=\"\n",
    "filtered_rows = df_100k[(df_100k['label'].str.contains('\\+=', regex=True)) | (df_100k['predicate'].str.contains('\\+=', regex=True))]\n",
    "\n",
    "# Add the original indices to the filtered DataFrame\n",
    "filtered_rows = filtered_rows.reset_index(drop=False).rename(columns={'index': 'original_index'})\n",
    "\n",
    "# Display the count of such rows\n",
    "count = len(filtered_rows)\n",
    "print(f\"Number of rows containing '+=': {count}\")\n",
    "\n",
    "# Display the DataFrame with original index and both 'label' and 'predicate' columns\n",
    "#print(filtered_rows[['original_index', 'label', 'predicate']])\n",
    "\n",
    "# If you want to store it for further viewing, you can save it to a new DataFrame\n",
    "#filtered_rows_for_viewing = filtered_rows[['original_index', 'label', 'predicate']]\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Counting the number of rows having `days`, `minutes`, and `hours` in them"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Convert the Dataset to a pandas DataFrame\n",
    "df_100k = ds['train'].to_pandas()\n",
    "\n",
    "# Define the search strings\n",
    "search_strings = ['days', 'minutes', 'hours']\n",
    "\n",
    "# Filter the rows where 'label' or 'predicate' columns contain any of the search strings\n",
    "filtered_rows = df_100k[\n",
    "    df_100k['label'].str.contains('|'.join(search_strings), regex=True) |\n",
    "    df_100k['predicate'].str.contains('|'.join(search_strings), regex=True)\n",
    "]\n",
    "\n",
    "# Add the original indices to the filtered DataFrame\n",
    "filtered_rows = filtered_rows.reset_index(drop=False).rename(columns={'index': 'original_index'})\n",
    "\n",
    "# Display the count of such rows\n",
    "count = len(filtered_rows)\n",
    "print(f\"Number of rows containing 'days', 'minutes', or 'hours': {count}\")\n",
    "\n",
    "# Display the DataFrame with original index and both 'label' and 'predicate' columns\n",
    "#print(filtered_rows[['original_index', 'label', 'predicate']])\n",
    "\n",
    "# If you want to store it for further viewing, you can save it to a new DataFrame\n",
    "#filtered_rows_for_viewing = filtered_rows[['original_index', 'label', 'predicate']]\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Counting the ones that contain Ethereum currency units"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Convert the Dataset to a pandas DataFrame\n",
    "df_100k = ds['train'].to_pandas()\n",
    "\n",
    "# Define the Ethereum-related search strings\n",
    "ethereum_keywords = ['wei', 'gwei', 'eth']\n",
    "\n",
    "# Filter the rows where 'label' or 'predicate' columns contain any of the Ethereum-related keywords\n",
    "filtered_rows = df_100k[\n",
    "    df_100k['label'].str.contains('|'.join(ethereum_keywords), case=False, regex=True) |\n",
    "    df_100k['predicate'].str.contains('|'.join(ethereum_keywords), case=False, regex=True)\n",
    "]\n",
    "\n",
    "# Add the original indices to the filtered DataFrame\n",
    "filtered_rows = filtered_rows.reset_index(drop=False).rename(columns={'index': 'original_index'})\n",
    "\n",
    "# Display the count of such rows\n",
    "count = len(filtered_rows)\n",
    "print(f\"Number of rows containing Ethereum-related keywords: {count}\")\n",
    "\n",
    "# Display the DataFrame with original index and both 'label' and 'predicate' columns\n",
    "#print(filtered_rows[['original_index', 'label', 'predicate']])\n",
    "\n",
    "# If you want to store it for further viewing, you can save it to a new DataFrame\n",
    "#filtered_rows_for_viewing = filtered_rows[['original_index', 'label', 'predicate']]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Convert the Dataset to a pandas DataFrame\n",
    "df_100k = ds['train'].to_pandas()\n",
    "\n",
    "msg_sender_keywords = ['_msgSender()']\n",
    "\n",
    "# Filter the rows where 'label' or 'predicate' columns contain any of the Ethereum-related keywords\n",
    "filtered_rows = df_100k[\n",
    "    df_100k['predicate'].str.contains(\"_msgSender()\") |\n",
    "    df_100k['results'].str.contains(\"_msgSender()\")\n",
    "]\n",
    "\n",
    "# Add the original indices to the filtered DataFrame\n",
    "filtered_rows = filtered_rows.reset_index(drop=False).rename(columns={'index': 'original_index'})\n",
    "\n",
    "# Display the count of such rows\n",
    "count = len(filtered_rows)\n",
    "print(f\"Number of rows containing _msgSender() keywords: {count}\")\n",
    "\n",
    "filtered_rows.head()\n",
    "# Display the DataFrame with original index and both 'label' and 'predicate' columns\n",
    "#print(filtered_rows[['original_index', 'label', 'predicate']])\n",
    "\n",
    "# If you want to store it for further viewing, you can save it to a new DataFrame\n",
    "#filtered_rows_for_viewing = filtered_rows[['original_index', 'label', 'predicate']]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Convert the Dataset to a pandas DataFrame\n",
    "df_100k = ds['train'].to_pandas()\n",
    "\n",
    "\n",
    "# Filter the rows where 'label' or 'predicate' columns contain any of the Ethereum-related keywords\n",
    "filtered_rows = df_100k[\n",
    "    df_100k['predicate'].str.contains(\"_owner()\") |\n",
    "    df_100k['results'].str.contains(\"_owner()\")\n",
    "]\n",
    "\n",
    "# Add the original indices to the filtered DataFrame\n",
    "filtered_rows = filtered_rows.reset_index(drop=False).rename(columns={'index': 'original_index'})\n",
    "\n",
    "# Display the count of such rows\n",
    "count = len(filtered_rows)\n",
    "print(f\"Number of rows containing _msgSender() keywords: {count}\")\n",
    "\n",
    "filtered_rows.head()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Handling time constructs"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [],
   "source": [
    "import re\n",
    "from typing import List, Tuple\n",
    "\n",
    "class Tokenizer:\n",
    "    def __init__(self):\n",
    "        self.token_patterns = [\n",
    "            (r'\\bmsg\\.sender\\b', 'MSG_SENDER'),\n",
    "            (r'\\bmsg\\.origin\\b', 'MSG_ORIGIN'),\n",
    "            (r'\\brequire\\b', 'REQUIRE'),\n",
    "            (r'==', 'EQUAL'),\n",
    "            (r'!=', 'NOT_EQUAL'),\n",
    "            (r'>=', 'GREATER_EQUAL'),\n",
    "            (r'<=', 'LESS_EQUAL'),\n",
    "            (r'>', 'GREATER'),\n",
    "            (r'<', 'LESS'),\n",
    "            (r'&&', 'AND'),\n",
    "            (r'\\|\\|', 'OR'),\n",
    "            (r'\\!', 'NOT'),\n",
    "            (r'&', 'BITWISE_AND'),\n",
    "            (r'\\?', 'QUESTION'),\n",
    "            (r':', 'COLON'),\n",
    "            (r'\\(', 'LPAREN'),\n",
    "            (r'\\)', 'RPAREN'),\n",
    "            (r'\\+', 'PLUS'),\n",
    "            (r'\\-', 'MINUS'),\n",
    "            (r'\\*', 'MULTIPLY'),\n",
    "            (r'\\/', 'DIVIDE'),\n",
    "            (r'\\%', 'MODULUS'),\n",
    "            (r'\\.', 'DOT'),\n",
    "            (r',', 'COMMA'),\n",
    "            (r'=', 'ASSIGN'),\n",
    "            (r'\\[', 'LBRACKET'),\n",
    "            (r'\\]', 'RBRACKET'),\n",
    "            (r'\\\"[^\\\"]*\\\"', 'STRING_LITERAL'),\n",
    "            (r'\\b\\d+\\.\\d+\\b', 'FLOAT'),\n",
    "            (r'\\b\\d+\\b', 'INTEGER'),\n",
    "            (r'\\btrue\\b', 'TRUE'),\n",
    "            (r'\\bfalse\\b', 'FALSE'),\n",
    "            (r'0x[0-9a-fA-F]{40}', 'ADDRESS_LITERAL'),\n",
    "            (r'0x[0-9a-fA-F]+', 'BYTES_LITERAL'),\n",
    "            (r'\\b\\d+\\s*(seconds|minutes|hours|days|weeks)\\b', 'TIME_UNIT'),  # Handle time units\n",
    "            (r'[a-zA-Z_]\\w*', 'IDENTIFIER'),\n",
    "            (r'\\d+e\\d+', 'SCIENTIFIC'),  # Handle scientific notation\n",
    "            (r'\\s+', None),  # Let's ignore whitespace(s)\n",
    "        ]\n",
    "        self.time_units = {\n",
    "            'seconds': 1,\n",
    "            'minutes': 60,\n",
    "            'hours': 3600,\n",
    "            'days': 86400,\n",
    "            'weeks': 604800,\n",
    "        }\n",
    "\n",
    "    def normalize(self, predicate: str) -> str:\n",
    "        predicate = re.sub(r'\\s+', '', predicate)\n",
    "        predicate = re.sub(r'([!=<>]=?)', r' \\1 ', predicate)\n",
    "        predicate = re.sub(r'(\\&\\&|\\|\\|)', r' \\1 ', predicate)\n",
    "        predicate = re.sub(r'\\(', r' ( ', predicate)\n",
    "        predicate = re.sub(r'\\)', r' ) ', predicate)\n",
    "        predicate = re.sub(r'\\s+', ' ', predicate)\n",
    "        return predicate.strip()\n",
    "\n",
    "    def tokenize(self, predicate: str) -> List[Tuple[str, str]]:\n",
    "        tokens = []\n",
    "        position = 0\n",
    "        length = len(predicate)\n",
    "\n",
    "        while position < length:\n",
    "            match = None\n",
    "            for pattern, tag in self.token_patterns:\n",
    "                regex = re.compile(pattern)\n",
    "                match = regex.match(predicate, position)\n",
    "                if match:\n",
    "                    if tag:\n",
    "                        value = match.group(0)\n",
    "                        if tag == 'TIME_UNIT':\n",
    "                            number, unit = re.match(r'(\\d+)\\s*(\\w+)', value).groups()\n",
    "                            value = str(int(number) * self.time_units[unit])\n",
    "                            tag = 'INTEGER'\n",
    "                        elif tag == 'SCIENTIFIC':\n",
    "                            value = str(int(float(value)))\n",
    "                            tag = 'INTEGER'\n",
    "                        tokens.append((value, tag))\n",
    "                    position = match.end()\n",
    "                    break\n",
    "            if not match:\n",
    "                if predicate[position] == '(':\n",
    "                    tokens.append(('(', 'LPAREN'))\n",
    "                    position += 1\n",
    "                elif predicate[position] == ')':\n",
    "                    tokens.append((')', 'RPAREN'))\n",
    "                    position += 1\n",
    "                elif predicate[position] == ',':\n",
    "                    tokens.append((',', 'COMMA'))\n",
    "                    position += 1\n",
    "                else:\n",
    "                    raise ValueError(f\"Unexpected character: {predicate[position]} at position {position}\")\n",
    "\n",
    "        return tokens\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [],
   "source": [
    "from typing import List, Tuple\n",
    "\n",
    "class ASTNode:\n",
    "    def __init__(self, value: str, children: List['ASTNode'] = None):\n",
    "        self.value = value\n",
    "        self.children = children if children is not None else []\n",
    "\n",
    "    def __repr__(self):\n",
    "        return f\"ASTNode(value='{self.value}', children={self.children})\"\n",
    "\n",
    "class Parser:\n",
    "    def __init__(self, tokens: List[Tuple[str, str]]):\n",
    "        self.tokens = tokens\n",
    "        self.position = 0\n",
    "\n",
    "    def parse(self) -> ASTNode:\n",
    "        self.position = 0  # Reset the position for each new parse\n",
    "        return self.expression()\n",
    "\n",
    "    def consume(self, expected_tag: str) -> Tuple[str, str]:\n",
    "        if self.position >= len(self.tokens):\n",
    "            raise ValueError(f\"Unexpected end of input, expected {expected_tag}\")\n",
    "        token = self.tokens[self.position]\n",
    "        if token[1] != expected_tag:\n",
    "            raise ValueError(f\"Expected token {expected_tag} but got {token[1]} at position {self.position}\")\n",
    "        self.position += 1\n",
    "        return token\n",
    "\n",
    "    def expression(self) -> ASTNode:\n",
    "        node = self.logical_term()\n",
    "        #debug_print(f\"Parsed term: {node}\")\n",
    "\n",
    "        while self.position < len(self.tokens) and self.tokens[self.position][1] in ('AND', 'OR'):\n",
    "            operator = self.tokens[self.position]\n",
    "            #debug_print(f\"Parsing operator in expression: {operator}\")\n",
    "            self.position += 1\n",
    "            right = self.logical_term()\n",
    "            node = ASTNode(operator[0], [node, right])\n",
    "            #debug_print(f\"Parsed expression with operator: {node}\")\n",
    "\n",
    "        return node\n",
    "\n",
    "    def logical_term(self) -> ASTNode:\n",
    "        node = self.equality()\n",
    "        #debug_print(f\"Parsed equality: {node}\")\n",
    "\n",
    "        while self.position < len(self.tokens) and self.tokens[self.position][1] in ('EQUAL', 'NOT_EQUAL'):\n",
    "            operator = self.tokens[self.position]\n",
    "            #debug_print(f\"Parsing operator in logical term: {operator}\")\n",
    "            self.position += 1\n",
    "            right = self.equality()\n",
    "            node = ASTNode(operator[0], [node, right])\n",
    "            #debug_print(f\"Parsed logical term with operator: {node}\")\n",
    "\n",
    "        return node\n",
    "\n",
    "    def equality(self) -> ASTNode:\n",
    "        node = self.relational()\n",
    "        #debug_print(f\"Parsed relational: {node}\")\n",
    "\n",
    "        while self.position < len(self.tokens) and self.tokens[self.position][1] in ('GREATER', 'LESS', 'GREATER_EQUAL', 'LESS_EQUAL'):\n",
    "            operator = self.tokens[self.position]\n",
    "            #debug_print(f\"Parsing operator in equality: {operator}\")\n",
    "            self.position += 1\n",
    "            right = self.relational()\n",
    "            node = ASTNode(operator[0], [node, right])\n",
    "            #debug_print(f\"Parsed equality with operator: {node}\")\n",
    "\n",
    "        return node\n",
    "\n",
    "    def relational(self) -> ASTNode:\n",
    "        node = self.term()\n",
    "        #debug_print(f\"Parsed term in relational: {node}\")\n",
    "\n",
    "        while self.position < len(self.tokens) and self.tokens[self.position][1] in ('PLUS', 'MINUS'):\n",
    "            operator = self.tokens[self.position]\n",
    "            #debug_print(f\"Parsing operator in relational: {operator}\")\n",
    "            self.position += 1\n",
    "            right = self.term()\n",
    "            node = ASTNode(operator[0], [node, right])\n",
    "            #debug_print(f\"Parsed relational with operator: {node}\")\n",
    "\n",
    "        return node\n",
    "\n",
    "    def term(self) -> ASTNode:\n",
    "        node = self.factor()\n",
    "        #debug_print(f\"Parsed factor in term: {node}\")\n",
    "\n",
    "        while self.position < len(self.tokens) and self.tokens[self.position][1] in ('MULTIPLY', 'DIVIDE', 'MODULUS'):\n",
    "            operator = self.tokens[self.position]\n",
    "            #debug_print(f\"Parsing operator in term: {operator}\")\n",
    "            self.position += 1\n",
    "            right = self.factor()\n",
    "            node = ASTNode(operator[0], [node, right])\n",
    "            #debug_print(f\"Parsed term with operator: {node}\")\n",
    "\n",
    "        return node\n",
    "\n",
    "    def factor(self) -> ASTNode:\n",
    "        if self.position >= len(self.tokens):\n",
    "            raise ValueError(\"Unexpected end of input\")\n",
    "        token = self.tokens[self.position]\n",
    "        if token[1] in ('TRUE', 'FALSE'):\n",
    "            self.position += 1\n",
    "            return ASTNode(token[0])\n",
    "        if token[1] == 'ADDRESS_LITERAL':\n",
    "            self.position += 1\n",
    "            return ASTNode(token[0])\n",
    "        if token[1] == 'BYTES_LITERAL':\n",
    "            self.position += 1\n",
    "            return ASTNode(token[0])\n",
    "        if token[1] == 'LPAREN':\n",
    "            self.position += 1\n",
    "            node = self.expression()\n",
    "            self.consume('RPAREN')\n",
    "            return node\n",
    "        elif token[1] in ('IDENTIFIER', 'MSG_SENDER', 'MSG_ORIGIN', 'INTEGER', 'FLOAT', 'SCIENTIFIC'):\n",
    "            self.position += 1\n",
    "            node = ASTNode(token[0])\n",
    "            return self.postfix(node)\n",
    "        elif token[1] == 'NOT':\n",
    "            self.position += 1\n",
    "            node = self.factor()\n",
    "            node = ASTNode('!', [node])\n",
    "            return node\n",
    "        elif token[1] in ('PLUS', 'MINUS'):\n",
    "            self.position += 1\n",
    "            node = self.factor()\n",
    "            node = ASTNode(token[0], [node])\n",
    "            return node\n",
    "        raise ValueError(f\"Unexpected token {token[1]} at position {self.position}\")\n",
    "\n",
    "    def postfix(self, node: ASTNode) -> ASTNode:\n",
    "        while self.position < len(self.tokens) and self.tokens[self.position][1] in ('DOT', 'LBRACKET', 'LPAREN'):\n",
    "            token = self.tokens[self.position]\n",
    "            #debug_print(f\"Parsing postfix at position {self.position}: {token}\")\n",
    "\n",
    "            if token[1] == 'DOT':\n",
    "                self.position += 1\n",
    "                member_token = self.consume('IDENTIFIER')\n",
    "                node = ASTNode(f\"{node.value}.{member_token[0]}\")\n",
    "            elif token[1] == 'LBRACKET':\n",
    "                self.position += 1\n",
    "                index_node = self.expression()\n",
    "                self.consume('RBRACKET')\n",
    "                node = ASTNode(f\"{node.value}[]\", [index_node])\n",
    "            elif token[1] == 'LPAREN':\n",
    "                self.position += 1\n",
    "                args = []\n",
    "                while self.position < len(self.tokens) and self.tokens[self.position][1] != 'RPAREN':\n",
    "                    args.append(self.expression())\n",
    "                    if self.position < len(self.tokens) and self.tokens[self.position][1] == 'COMMA':\n",
    "                        #debug_print(f\"Consuming COMMA at position {self.position}\")\n",
    "                        self.position += 1\n",
    "                self.consume('RPAREN')\n",
    "                node = ASTNode(f\"{node.value}()\", args)\n",
    "            #debug_print(f\"Parsed postfix: {node}\")\n",
    "        return node\n",
    "\n",
    "    def function_call(self, token: Tuple[str, str]) -> ASTNode:\n",
    "        function_name = token[0]\n",
    "        self.position += 1  # Consume FUNCTION_CALL token\n",
    "        self.consume('LPAREN')\n",
    "        args = []\n",
    "        while self.position < len(self.tokens) and self.tokens[self.position][1] != 'RPAREN':\n",
    "            args.append(self.expression())\n",
    "            if self.position < len(self.tokens) and self.tokens[self.position][1] == 'COMMA':\n",
    "                self.position += 1\n",
    "        self.consume('RPAREN')\n",
    "        node = ASTNode(function_name, args)\n",
    "        #debug_print(f\"Parsed function call: {node}\")\n",
    "        return node\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The predicates are equivalent.\n"
     ]
    }
   ],
   "source": [
    "import sympy as sp\n",
    "from sympy.logic.boolalg import And, Or, Not\n",
    "from sympy.logic.inference import satisfiable\n",
    "\n",
    "\n",
    "\n",
    "class Comparator:\n",
    "    def __init__(self):\n",
    "        self.tokenizer = Tokenizer()\n",
    "        self.simplifier = Simplifier()\n",
    "\n",
    "    def compare(self, predicate1: str, predicate2: str) -> str:\n",
    "        # Tokenize, parse, and simplify the first predicate\n",
    "        tokens1 = self.tokenizer.tokenize(predicate1)\n",
    "        #debug_print(f\"Tokens1: {tokens1}\")\n",
    "        parser1 = Parser(tokens1)\n",
    "        ast1 = parser1.parse()\n",
    "        #debug_print(f\"Parsed AST1: {ast1}\")\n",
    "\n",
    "        # Tokenize, parse, and simplify the second predicate\n",
    "        tokens2 = self.tokenizer.tokenize(predicate2)\n",
    "        #debug_print(f\"Tokens2: {tokens2}\")\n",
    "        parser2 = Parser(tokens2)\n",
    "        ast2 = parser2.parse()\n",
    "        #debug_print(f\"Parsed AST2: {ast2}\")\n",
    "\n",
    "        # Convert ASTs to SymPy expressions\n",
    "        expr1 = self._to_sympy_expr(ast1)\n",
    "        expr2 = self._to_sympy_expr(ast2)\n",
    "\n",
    "        #debug_print(f'> expr1: {expr1}')\n",
    "        #debug_print(f'> expr2: {expr2}')\n",
    "\n",
    "        # Simplify expressions\n",
    "        simplified_expr1 = sp.simplify(expr1)\n",
    "        #debug_print(f\"Simplified SymPy Expression 1: {simplified_expr1}\")\n",
    "\n",
    "        simplified_expr2 = sp.simplify(expr2)\n",
    "        #debug_print(f\"Simplified SymPy Expression 2: {simplified_expr2}\")\n",
    "\n",
    "        # Manually check implications\n",
    "        implies1_to_2 = self._implies(simplified_expr1, simplified_expr2)\n",
    "        #debug_print(f\"> Implies expr1 to expr2: {implies1_to_2}\")\n",
    "        implies2_to_1 = self._implies(simplified_expr2, simplified_expr1)\n",
    "        #debug_print(f\"> Implies expr2 to expr1: {implies2_to_1}\")\n",
    "\n",
    "        if implies1_to_2 and not implies2_to_1:\n",
    "            return \"The first predicate is stronger.\"\n",
    "        elif implies2_to_1 and not implies1_to_2:\n",
    "            return \"The second predicate is stronger.\"\n",
    "        elif implies1_to_2 and implies2_to_1:\n",
    "            return \"The predicates are equivalent.\"\n",
    "        else:\n",
    "            return \"The predicates are not equivalent and neither is stronger.\"\n",
    "\n",
    "    def _to_sympy_expr(self, ast):\n",
    "        if not ast.children:\n",
    "            try:\n",
    "                # Try converting to int or float if the value is a numeric string\n",
    "                value = float(ast.value) if '.' in ast.value else int(ast.value)\n",
    "                return sp.Number(value)\n",
    "            except ValueError:\n",
    "                # If conversion fails, treat it as a symbol\n",
    "                return sp.Symbol(ast.value.replace('.', '_'))\n",
    "        args = [self._to_sympy_expr(child) for child in ast.children]\n",
    "        if ast.value in ('&&', '||', '!', '==', '!=', '>', '<', '>=', '<='):\n",
    "            return getattr(sp, self._sympy_operator(ast.value))(*args)\n",
    "        elif ast.value == '/':\n",
    "            return sp.Mul(sp.Pow(args[1], -1), args[0])\n",
    "        elif ast.value == '+':\n",
    "            return sp.Add(*args)\n",
    "        elif ast.value == '-':\n",
    "            return sp.Add(args[0], sp.Mul(-1, args[1]))\n",
    "        elif ast.value == '*':\n",
    "            return sp.Mul(*args)\n",
    "        elif '()' in ast.value:\n",
    "            func_name = ast.value.replace('()', '')\n",
    "            return sp.Function(func_name)(*args)\n",
    "        return sp.Symbol(ast.value.replace('.', '_'))\n",
    "\n",
    "    def _sympy_operator(self, op):\n",
    "        return {\n",
    "            '&&': 'And',\n",
    "            '||': 'Or',\n",
    "            '!': 'Not',\n",
    "            '==': 'Eq',\n",
    "            '!=': 'Ne',\n",
    "            '>': 'Gt',\n",
    "            '<': 'Lt',\n",
    "            '>=': 'Ge',\n",
    "            '<=': 'Le'\n",
    "        }[op]\n",
    "\n",
    "    def _implies(self, expr1, expr2):\n",
    "        \"\"\"\n",
    "        Check if expr1 implies expr2 by manually comparing the expressions.\n",
    "        \"\"\"\n",
    "        #debug_print(f\"Checking implication: {expr1} -> {expr2}\")\n",
    "        if expr1 == expr2:\n",
    "            #debug_print(\"Expressions are identical.\")\n",
    "            return True\n",
    "\n",
    "        # Handle equivalences through algebraic manipulation\n",
    "        try:\n",
    "            if sp.simplify(expr1 - expr2) == 0:\n",
    "                #debug_print(\"Expressions are equivalent through algebraic manipulation.\")\n",
    "                return True\n",
    "        except Exception as e: \n",
    "            #debug_print(f\"Error: {e}\")\n",
    "            pass\n",
    "\n",
    "\n",
    "        # Handle negation equivalence (e.g., !used[salt] == used[salt] == false)\n",
    "        if isinstance(expr1, Not) and isinstance(expr2, sp.Equality):\n",
    "            #debug_print('>>>>>>>>>>>> here1')\n",
    "            #debug_print(f'expr2: {expr2}')\n",
    "            #debug_print(f'expr2.rhs: {expr2.rhs}')\n",
    "            #debug_print(f'expr2.lhs: {expr2.lhs}')\n",
    "            if expr2.rhs == sp.false or expr2.rhs == False or expr2.rhs == sp.Symbol('false'):\n",
    "                #debug_print('>>>>>>>>>>>> here1.1')\n",
    "                return self._implies(expr1.args[0], expr2.lhs)\n",
    "            if expr2.lhs == sp.false or expr2.lhs == False or expr2.lhs == sp.Symbol('false'):\n",
    "                #debug_print('>>>>>>>>>>>> here1.2')\n",
    "                return self._implies(expr1.args[0], expr2.rhs)\n",
    "\n",
    "        if isinstance(expr2, Not) and isinstance(expr1, sp.Equality):\n",
    "            #debug_print('>>>>>>>>>>>> here2')\n",
    "            #debug_print(f'expr1: {expr1}')\n",
    "            #debug_print(f'expr1.rhs: {expr1.rhs}')\n",
    "            #debug_print(f'expr1.lhs: {expr1.lhs}')\n",
    "            if expr1.rhs == sp.false or expr1.rhs == False or expr1.rhs == sp.Symbol('false'):\n",
    "                #debug_print('>>>>>>>>>>>> here2.1')\n",
    "                return self._implies(expr2.args[0], expr1.lhs)\n",
    "            if expr1.lhs == sp.false or expr1.lhs == False or expr1.lhs == sp.Symbol('false'):\n",
    "                #debug_print('>>>>>>>>>>>> here2.2')\n",
    "                return self._implies(expr2.args[0], expr1.rhs)\n",
    "\n",
    "        # Handle equivalence involving `true`\n",
    "        if isinstance(expr1, sp.Symbol) and isinstance(expr2, sp.Equality):\n",
    "            if expr2.rhs == sp.true or expr2.rhs == True or expr2.rhs == sp.Symbol('true'):\n",
    "                return self._implies(expr1, expr2.lhs)\n",
    "            if expr2.lhs == sp.true or expr2.lhs == True or expr2.lhs == sp.Symbol('true'):\n",
    "                return self._implies(expr1, expr2.rhs)\n",
    "        \n",
    "        if isinstance(expr2, sp.Symbol) and isinstance(expr1, sp.Equality):\n",
    "            if expr1.rhs == sp.true or expr1.rhs == True or expr1.rhs == sp.Symbol('true'):\n",
    "                return self._implies(expr2, expr1.lhs)\n",
    "            if expr1.lhs == sp.true or expr1.lhs == True or expr1.lhs == sp.Symbol('true'):\n",
    "                return self._implies(expr2, expr1.rhs)\n",
    "        \n",
    "\n",
    "        # Handle logical equivalence for AND, OR, NOT operations\n",
    "        if isinstance(expr1, Not) and isinstance(expr2, Or):\n",
    "            if len(expr2.args) == 2:\n",
    "                left, right = expr2.args\n",
    "                if isinstance(left, sp.Equality) and left.rhs == sp.false:\n",
    "                    return self._implies(expr1.args[0], left.lhs) and self._implies(right, sp.true)\n",
    "                if isinstance(right, sp.Equality) and right.rhs == sp.false:\n",
    "                    return self._implies(expr1.args[0], right.lhs) and self._implies(left, sp.true)\n",
    "\n",
    "        if isinstance(expr2, Not) and isinstance(expr1, Or):\n",
    "            if len(expr1.args) == 2:\n",
    "                left, right = expr1.args\n",
    "                if isinstance(left, sp.Equality) and left.rhs == sp.false:\n",
    "                    return self._implies(expr2.args[0], left.lhs) and self._implies(right, sp.true)\n",
    "                if isinstance(right, sp.Equality) and right.rhs == sp.false:\n",
    "                    return self._implies(expr2.args[0], right.lhs) and self._implies(left, sp.true)\n",
    "\n",
    "        if isinstance(expr1, And) and isinstance(expr2, And):\n",
    "            if len(expr1.args) == len(expr2.args):\n",
    "                return all(self._implies(arg1, arg2) for arg1, arg2 in zip(expr1.args, expr2.args))\n",
    "\n",
    "        if isinstance(expr1, Or) and isinstance(expr2, Or):\n",
    "            if len(expr1.args) == len(expr2.args):\n",
    "                return all(self._implies(arg1, arg2) for arg1, arg2 in zip(expr1.args, expr2.args))\n",
    "\n",
    "\n",
    "\n",
    "        # Handle AND expression for expr2\n",
    "        if isinstance(expr2, And):\n",
    "            # expr1 should imply all parts of expr2 if expr2 is an AND expression\n",
    "            results = [self._implies(expr1, arg) for arg in expr2.args]\n",
    "            #debug_print(f\"Implication results for And expr2 which was `{expr1} => {expr2}`: {results}\")\n",
    "            return all(results)\n",
    "\n",
    "        # Handle AND expression for expr1\n",
    "        if isinstance(expr1, And):\n",
    "            # All parts of expr1 should imply expr2 if expr1 is an AND expression\n",
    "            results = [self._implies(arg, expr2) for arg in expr1.args]\n",
    "            #debug_print(f\"Implication results for And expr1 which was `{expr1} => {expr2}`: {results}\")\n",
    "            return any(results)\n",
    "\n",
    "        # Handle OR expression for expr2\n",
    "        if isinstance(expr2, Or):\n",
    "            # expr1 should imply at least one part of expr2 if expr2 is an OR expression\n",
    "            results = [self._implies(expr1, arg) for arg in expr2.args]\n",
    "            #debug_print(f\"Implication results for Or expr2 which was `{expr1} => {expr2}`: {results}\")\n",
    "            return any(results)\n",
    "\n",
    "        # Handle OR expression for expr1\n",
    "        if isinstance(expr1, Or):\n",
    "            # All parts of expr1 should imply expr2 if expr1 is an OR expression\n",
    "            results = [self._implies(arg, expr2) for arg in expr1.args]\n",
    "            #debug_print(f\"Implication results for Or expr1 which was `{expr1} => {expr2}`: {results}\")\n",
    "            return all(results)\n",
    "\n",
    "        # Handle function calls\n",
    "        if isinstance(expr1, sp.Function) and isinstance(expr2, sp.Function):\n",
    "            # Ensure the function names and the number of arguments match\n",
    "            if expr1.func == expr2.func and len(expr1.args) == len(expr2.args):\n",
    "                return all(self._implies(arg1, arg2) for arg1, arg2 in zip(expr1.args, expr2.args))\n",
    "            return False\n",
    "\n",
    "        if isinstance(expr1, sp.Symbol) and isinstance(expr2, sp.Symbol):\n",
    "            return expr1 == expr2\n",
    "\n",
    "        # Specific relational operator checks for numerical comparisons\n",
    "        relational_operators = (sp.Gt, sp.Ge, sp.Lt, sp.Le, sp.Eq, sp.Ne)\n",
    "        if isinstance(expr1, relational_operators) and isinstance(expr2, relational_operators):\n",
    "            #debug_print(f'we are here!... expr1: {expr1}, expr2: {expr2}')\n",
    "            # Check for Eq vs non-Eq comparisons; we don't handle this well, let's return False\n",
    "            if (isinstance(expr1, sp.Eq) and not isinstance(expr2, sp.Eq)) or (not isinstance(expr1, sp.Eq) and isinstance(expr2, sp.Eq)):\n",
    "                return False  # Handle Eq vs non-Eq cases explicitly\n",
    "\n",
    "            if all(isinstance(arg, (sp.Float, sp.Integer, sp.Symbol)) for arg in [expr1.lhs, expr1.rhs, expr2.lhs, expr2.rhs]):\n",
    "                #debug_print(f'Inside!... expr1: {expr1}, expr2: {expr2}')\n",
    "                # Check if the negation of the implication is not satisfiable\n",
    "                try:\n",
    "                    negation = sp.And(expr1, Not(expr2))\n",
    "                    #debug_print(f\"Negation of the implication {expr1} -> {expr2}: {satisfiable(negation)}; type of {type(satisfiable(negation))}\")\n",
    "                    result = not satisfiable(negation, use_lra_theory=True)\n",
    "                    #debug_print(f\"Implication {expr1} -> {expr2} using satisfiable: {result}\")\n",
    "                    return result\n",
    "                except Exception as e:\n",
    "                    #debug_print(f\"Error: {e}\")\n",
    "                    return False\n",
    "        return False\n",
    "\n",
    "\n",
    "# Example usage\n",
    "# predicate1 = \"msg.sender != msg.origin\" \n",
    "# predicate2 = \"a >= b\" \n",
    "\n",
    "# predicate1 = \"_addresses.length>0\"\n",
    "# predicate2 = \"_addresses.length<=200\"\n",
    "\n",
    "# predicate1 = \"ethBalances[_msgSender()]<=9e18\"\n",
    "# predicate2 = \"ethBalances[_msgSender()]<=9e10\"\n",
    "\n",
    "# predicate1 = \"a < 10\"\n",
    "# predicate2 = \"a < 9\"\n",
    "\n",
    "# predicate1 = \"a + b < 10\"\n",
    "# predicate2 = \"a < 10 - b\"\n",
    "\n",
    "# predicate1 = \"msg.sender==governance||msg.sender==controller||msg.sender==address(this)\"\n",
    "# predicate2 = \"msg.sender==governance||msg.sender==controller\"\n",
    "\n",
    "# predicate1 = 'msg.sender==_mintRequest.to'\n",
    "# predicate2 = 'requiredPrice==msg.value'\n",
    "\n",
    "\n",
    "# predicate1 = 'a==12'\n",
    "# predicate2 = '12==b'\n",
    "\n",
    "\n",
    "# predicate1 = \"a == b\"\n",
    "# #predicate2 = \"b == a\"\n",
    "\n",
    "predicate1 = \"!used[salt]\"\n",
    "predicate2 = \"used[salt]==false\"\n",
    "\n",
    "predicate1 = \"!condition\"\n",
    "predicate2 = \"condition==false\"\n",
    "\n",
    "\n",
    "\n",
    "comparator = Comparator()\n",
    "result = comparator.compare(predicate1, predicate2)\n",
    "print(result)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "if __name__ == \"__main__\":\n",
    "    comparator = Comparator()\n",
    "\n",
    "    predicates = [\n",
    "        (\"!condition\", \"condition == false\"),\n",
    "        (\"!used[salt]\", \"used[salt] == false\"),\n",
    "        (\"!(a && b)\", \"a == false || b == false\"),\n",
    "        (\"!!a\", \"a == true\"),\n",
    "        (\"!a || b\", \"a == false || b == true\"),\n",
    "        (\"!isActive(user)\", \"isActive(user) == false\"),\n",
    "        (\"!(x > 10)\", \"x <= 10\"),\n",
    "        (\"!((a && b) || c)\", \"(a == false || b == false) && c == false\"),\n",
    "        (\"!(a + b > 10)\", \"a + b <= 10\"),\n",
    "        (\"!(a > 5 && b < 3)\", \"a <= 5 || b >= 3\")\n",
    "    ]\n",
    "\n",
    "    for predicate1, predicate2 in predicates:\n",
    "        result = comparator.compare(predicate1, predicate2)\n",
    "        print(f\"Comparing:\\n  {predicate1}\\n  {predicate2}\\nResult: {result}\\n\")\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "predicate1 = \"ethBalances[_msgSender()]<=9e18\"\n",
    "predicate2 = \"ethBalances[_msgSender()]<=9e10\"\n",
    "\n",
    "tokens1 = Tokenizer().tokenize(predicate1)\n",
    "tokens2 = Tokenizer().tokenize(predicate2)\n",
    "print(f\"Tokens1: {tokens1}\")\n",
    "parser1 = Parser(tokens1)\n",
    "ast1 = parser1.parse()\n",
    "print(f\"Parsed AST1: {ast1}\")\n",
    "\n",
    "print(f\"Tokens2: {tokens2}\")\n",
    "parser2 = Parser(tokens2)\n",
    "ast2 = parser2.parse()\n",
    "print(f\"Parsed AST2: {ast2}\")\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[('msg.sender', 'MSG_SENDER'), ('!=', 'NOT_EQUAL'), ('msg.origin', 'MSG_ORIGIN')]\n"
     ]
    }
   ],
   "source": [
    "import re\n",
    "from typing import List, Tuple\n",
    "\n",
    "class Tokenizer:\n",
    "    def __init__(self):\n",
    "        self.token_patterns = [\n",
    "            (r'\\b\\d+\\s*(seconds|minutes|hours|days|weeks)\\b', 'TIME_UNIT'),  # Handle time units first\n",
    "            (r'\\bmsg\\.sender\\b', 'MSG_SENDER'),\n",
    "            (r'\\bmsg\\.origin\\b', 'MSG_ORIGIN'),\n",
    "            (r'\\brequire\\b', 'REQUIRE'),\n",
    "            (r'==', 'EQUAL'),\n",
    "            (r'!=', 'NOT_EQUAL'),\n",
    "            (r'>=', 'GREATER_EQUAL'),\n",
    "            (r'<=', 'LESS_EQUAL'),\n",
    "            (r'>', 'GREATER'),\n",
    "            (r'<', 'LESS'),\n",
    "            (r'&&', 'AND'),\n",
    "            (r'\\|\\|', 'OR'),\n",
    "            (r'\\!', 'NOT'),\n",
    "            (r'&', 'BITWISE_AND'),\n",
    "            (r'\\?', 'QUESTION'),\n",
    "            (r':', 'COLON'),\n",
    "            (r'\\(', 'LPAREN'),\n",
    "            (r'\\)', 'RPAREN'),\n",
    "            (r'\\+', 'PLUS'),\n",
    "            (r'\\-', 'MINUS'),\n",
    "            (r'\\*', 'MULTIPLY'),\n",
    "            (r'\\/', 'DIVIDE'),\n",
    "            (r'\\%', 'MODULUS'),\n",
    "            (r'\\.', 'DOT'),\n",
    "            (r',', 'COMMA'),\n",
    "            (r'=', 'ASSIGN'),\n",
    "            (r'\\[', 'LBRACKET'),\n",
    "            (r'\\]', 'RBRACKET'),\n",
    "            (r'\\\"[^\\\"]*\\\"', 'STRING_LITERAL'),\n",
    "            (r'\\b\\d+\\.\\d+\\b', 'FLOAT'),\n",
    "            (r'\\b\\d+\\b', 'INTEGER'),\n",
    "            (r'\\btrue\\b', 'TRUE'),\n",
    "            (r'\\bfalse\\b', 'FALSE'),\n",
    "            (r'0x[0-9a-fA-F]{40}', 'ADDRESS_LITERAL'),\n",
    "            (r'0x[0-9a-fA-F]+', 'BYTES_LITERAL'),\n",
    "            (r'[a-zA-Z_]\\w*', 'IDENTIFIER'),\n",
    "            (r'\\s+', None),  # Let's ignore whitespace(s)\n",
    "        ]\n",
    "        self.time_units = {\n",
    "            'seconds': 1,\n",
    "            'minutes': 60,\n",
    "            'hours': 3600,\n",
    "            'days': 86400,\n",
    "            'weeks': 604800,\n",
    "        }\n",
    "\n",
    "    def normalize(self, predicate: str) -> str:\n",
    "        predicate = re.sub(r'\\s+', '', predicate)\n",
    "        predicate = re.sub(r'([!=<>]=?)', r' \\1 ', predicate)\n",
    "        predicate = re.sub(r'(\\&\\&|\\|\\|)', r' \\1 ', predicate)\n",
    "        predicate = re.sub(r'\\(', r' ( ', predicate)\n",
    "        predicate = re.sub(r'\\)', r' ) ', predicate)\n",
    "        predicate = re.sub(r'\\s+', ' ', predicate)\n",
    "        return predicate.strip()\n",
    "\n",
    "    def tokenize(self, predicate: str) -> List[Tuple[str, str]]:\n",
    "        tokens = []\n",
    "        position = 0\n",
    "        length = len(predicate)\n",
    "\n",
    "        while position < length:\n",
    "            match = None\n",
    "            for pattern, tag in self.token_patterns:\n",
    "                regex = re.compile(pattern)\n",
    "                match = regex.match(predicate, position)\n",
    "                if match:\n",
    "                    if tag:\n",
    "                        value = match.group(0)\n",
    "                        if tag == 'TIME_UNIT':\n",
    "                            number, unit = re.match(r'(\\d+)\\s*(\\w+)', value).groups()\n",
    "                            value = str(int(number) * self.time_units[unit])\n",
    "                            tag = 'INTEGER'\n",
    "                        tokens.append((value, tag))\n",
    "                    position = match.end()\n",
    "                    break\n",
    "            if not match:\n",
    "                if predicate[position] == '(':\n",
    "                    tokens.append(('(', 'LPAREN'))\n",
    "                    position += 1\n",
    "                elif predicate[position] == ')':\n",
    "                    tokens.append((')', 'RPAREN'))\n",
    "                    position += 1\n",
    "                elif predicate[position] == ',':\n",
    "                    tokens.append((',', 'COMMA'))\n",
    "                    position += 1\n",
    "                else:\n",
    "                    raise ValueError(f\"Unexpected character: {predicate[position]} at position {position}\")\n",
    "\n",
    "        return tokens\n",
    "\n",
    "# Test the tokenizer\n",
    "tokenizer = Tokenizer()\n",
    "tokens = tokenizer.tokenize(\"NS < (1 days)\")\n",
    "tokens = tokenizer.tokenize(\"msg.sender != msg.origin\")\n",
    "print(tokens)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from datasets import load_dataset\n",
    "ds_llama = load_dataset(\"GGmorello/FLAMES_results\", \"CodeLLaMa\", token='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')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "df_llama = ds_llama['train'].to_pandas()\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "df_llama['results CodeLLama'][0:2000]\n",
    "\n",
    "# put the extracted column in a json file\n",
    "df_llama['results CodeLLama'].to_json('results.json', orient='records', lines=True) \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import pandas as pd\n",
    "import re\n",
    "\n",
    "# Example data\n",
    "data = {\n",
    "    'results': [\n",
    "        \"blockLoanAmount[block.number] <= blockLoanLimit, \\\"BLOCK_LOAN_LIMIT_EXCEEDED\\\"\",\n",
    "        \"s.isLosslessOn, \\\"LTO\\\"); require(s.isLosslessTurnOffProposed, \\\"LTP\\\"); require(s.losslessTurnOffTimestamp > block.timestamp, \\\"LTL\\\"); s.isLosslessOn = false; s.isLosslessTurnOffProposed = false; emit LosslessTurnedOff(); } function proposeLosslessTurnOn() external onlyRecoveryAdmin { } function executeLosslessTurnOn() external onlyRecoveryAdmin { } } // SPDX-License-Identifier: MIT // UNLICENSED // ALL RIGHTS RESERVED // Unicrypt by SDDTech reserves all rights on this code. You may NOT copy these contracts. pragma solidity 0.8.17; contract LosslessFacet is Ownable { Storage internal s; event Admin\",\n",
    "        \"toSend > 0); require(receiver1.send(toSend)); toSend = msg.value.mul(denominator).div(numerator); require(toSend > 0\",\n",
    "        \"payable(sara).send(_each)\",\n",
    "        \"_app != address(0)); require(_app != apps[_namespace][_appId]); _setApp(_namespace, _appId, _app\",\n",
    "        \"clearUserScore(msg.sender), \\\"Not claimable\\\"); require(userInfo[msg.sender].amount >= value_, \\\"Not enough balance\\\"); if (block.number > poolInfo.lastUpdateBlk\",\n",
    "        \"getCurrentStatus() == Status.REDEEMING, \\\"redeeming is not started\\\" ); require( block.timestamp - redeemingStartedAt <= durationOfRedeeming, \\\"redeeming is over\\\" ); require( amount <= maxAmount, \\\"exceed maxAmount granted by the proof\\\" ); require( amount <= _addressToMinted[msg.sender] + _reservedSupply, \\\"exceed maxAmount granted by the proof\\\" ); require( amount <= maxSupply - totalMinted(), \\\"exceed maxSupply\\\" ); require( amount <= mintingCapPerAddress - _addressToMinted[msg.sender], \\\"exceed mintingCapPerAddress\\\" ); require( amount <= maxAmount - _addressToMinted[msg.sender], \\\"exceed maxAmount granted by the proof\\\" ); require( amount <= maxAmount - _addressToMinted\"\n",
    "    ]\n",
    "}\n",
    "\n",
    "df = pd.DataFrame(data)\n",
    "\n",
    "# Define the regex pattern\n",
    "pattern = r\"(require\\()?([^;,\\\"']+?)\\s*(,|\\);|;|$)\"\n",
    "\n",
    "def extract_predicate(text):\n",
    "    # Simplify text to handle edge cases like new lines and comments\n",
    "    text = re.sub(r\"//.*\", \"\", text)  # Remove inline comments\n",
    "    matches = re.search(pattern, text.replace('\\n', ' '))\n",
    "    if matches:\n",
    "        return matches.group(2).strip()\n",
    "    return None\n",
    "\n",
    "# Apply regex on DataFrame\n",
    "df['predicate'] = df['results'].apply(extract_predicate)\n",
    "\n",
    "print(df['predicate'][6])\n",
    "#print(df[['results', 'predicate']])\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "WARNING: Ignoring invalid distribution -th-utils (/Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages)\n",
      "Requirement already satisfied: pandas in /Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages (1.3.3)\n",
      "Collecting pandas\n",
      "  Using cached pandas-2.0.3-cp38-cp38-macosx_10_9_x86_64.whl.metadata (18 kB)\n",
      "Requirement already satisfied: python-dateutil>=2.8.2 in /Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages (from pandas) (2.9.0.post0)\n",
      "Requirement already satisfied: pytz>=2020.1 in /Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages (from pandas) (2024.1)\n",
      "Requirement already satisfied: tzdata>=2022.1 in /Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages (from pandas) (2024.1)\n",
      "Requirement already satisfied: numpy>=1.20.3 in /Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages (from pandas) (1.24.4)\n",
      "Requirement already satisfied: six>=1.5 in /Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages (from python-dateutil>=2.8.2->pandas) (1.16.0)\n",
      "Using cached pandas-2.0.3-cp38-cp38-macosx_10_9_x86_64.whl (11.7 MB)\n",
      "WARNING: Ignoring invalid distribution -th-utils (/Users/mojtabaeshghie/opt/anaconda3/lib/python3.8/site-packages)\n",
      "Installing collected packages: pandas\n",
      "  Attempting uninstall: pandas\n",
      "    Found existing installation: pandas 1.3.3\n",
      "    Uninstalling pandas-1.3.3:\n",
      "      Successfully uninstalled pandas-1.3.3\n",
      "Successfully installed pandas-2.0.3\n",
      "Note: you may need to restart the kernel to use updated packages.\n"
     ]
    }
   ],
   "source": [
    "pip install --upgrade pandas"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [],
   "source": [
    "import csv\n",
    "import time\n",
    "\n",
    "# Instantiate the Comparator class\n",
    "comparator = Comparator()\n",
    "\n",
    "# Read the CSV file\n",
    "filename = 'comparison-results-200.csv'\n",
    "data = []\n",
    "\n",
    "with open(filename, newline='') as csvfile:\n",
    "    reader = csv.reader(csvfile)\n",
    "    header = next(reader)  # Skip the header\n",
    "    for row in reader:\n",
    "        data.append((row[1], row[2]))  # Assuming the second and third columns are p1 and p2\n",
    "\n",
    "# Compare the predicates (keep track of time to see how long it takes)\n",
    "start_time = time.time()\n",
    "results = []\n",
    "for p1, p2 in data:\n",
    "    try:\n",
    "        result = comparator.compare(p1, p2)\n",
    "    except Exception as e:\n",
    "        result = None  # Or handle the error as needed\n",
    "    results.append((p1, p2, result))\n",
    "end_time = time.time()\n",
    "\n",
    "print(f\"Time taken: {end_time - start_time:.2f} seconds\")\n",
    "\n",
    "# Display the first few results\n",
    "for result in results[:5]:\n",
    "    print(result)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "base",
   "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.8.17"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}