Adding some minor changes in playground

mojtaba-eshghie · Jul 10, 2024 · 09da074 · 09da074
1 parent 3a80516
commit 09da074
Showing 1 changed file with 26 additions and 27 deletions.
diff --git a/playground.ipynb b/playground.ipynb
@@ -41,22 +41,22 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 46,
+   "execution_count": 51,
    "metadata": {},
    "outputs": [
     {
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "Parsed AST1: ASTNode(value='<=', children=[ASTNode(value='balanceOf()', children=[ASTNode(value='to', children=[])]), ASTNode(value='-', children=[ASTNode(value='holdLimitAmount', children=[]), ASTNode(value='amount', children=[])])])\n",
-      "Parsed AST2: ASTNode(value='<=', children=[ASTNode(value='+', children=[ASTNode(value='balanceOf()', children=[ASTNode(value='to', children=[])]), ASTNode(value='amount', children=[])]), ASTNode(value='holdLimitAmount', children=[])])\n",
-      "SymPy Expression 1: balanceOf(to) <= -amount + holdLimitAmount\n",
-      "Simplified SymPy Expression 1: balanceOf(to) <= -amount + holdLimitAmount\n",
-      "SymPy Expression 2: amount + balanceOf(to) <= holdLimitAmount\n",
-      "Simplified SymPy Expression 2: holdLimitAmount >= amount + balanceOf(to)\n",
-      "we are here!... expr1: balanceOf(to) <= -amount + holdLimitAmount, expr2: amount + balanceOf(to) <= holdLimitAmount\n",
+      "Parsed AST1: ASTNode(value='<', children=[ASTNode(value='a', children=[]), ASTNode(value='12', children=[])])\n",
+      "Parsed AST2: ASTNode(value='==', children=[ASTNode(value='a', children=[]), ASTNode(value='12', children=[])])\n",
+      "SymPy Expression 1: a < 12\n",
+      "Simplified SymPy Expression 1: a < 12\n",
+      "SymPy Expression 2: Eq(a, 12)\n",
+      "Simplified SymPy Expression 2: Eq(a, 12)\n",
+      "we are here!... expr1: a < 12, expr2: Eq(a, 12)\n",
       "> Implies expr1 to expr2: False\n",
-      "we are here!... expr1: amount + balanceOf(to) <= holdLimitAmount, expr2: balanceOf(to) <= -amount + holdLimitAmount\n",
+      "we are here!... expr1: Eq(a, 12), expr2: a < 12\n",
       "> Implies expr2 to expr1: False\n",
       "The predicates are not equivalent and neither is stronger.\n"
      ]
@@ -105,9 +105,9 @@
     "       print(f\"Simplified SymPy Expression 2: {simplified_expr2}\")\n",
     "\n",
     "       # Manually check implications\n",
-    "       implies1_to_2 = self._implies(expr1, expr2)\n",
+    "       implies1_to_2 = self._implies(simplified_expr1, simplified_expr2)\n",
     "       print(f\"> Implies expr1 to expr2: {implies1_to_2}\")\n",
-    "       implies2_to_1 = self._implies(expr2, expr1)\n",
+    "       implies2_to_1 = self._implies(simplified_expr2, simplified_expr1)\n",
     "       print(f\"> Implies expr2 to expr1: {implies2_to_1}\")\n",
     "\n",
     "       if implies1_to_2 and not implies2_to_1:\n",
@@ -220,16 +220,15 @@
     "               result = not satisfiable(negation, use_lra_theory=True)\n",
     "               print(f\"Implication {expr1} -> {expr2} using satisfiable: {result}\")\n",
     "               return result\n",
-    "       \n",
-    "       #    print('We got to the buttom of the function!')\n",
-    "       #    # Check if the negation of the implication is not satisfiable for general expressions\n",
-    "       #    print(f'Expression 1 is: {expr1}, and its type is {type(expr1)}')\n",
-    "       #    print(f'Expression 2 is: {expr2}, and its type is {type(expr2)}')\n",
-    "       #    negation = sp.And(expr1, Not(expr2))\n",
-    "       #    result = not satisfiable(negation)\n",
-    "       #    print(f\"Implication {expr1} -> {expr2} using satisfiable: {result}\")\n",
-    "       #    return result\n",
-    "       return False\n",
+    "\n",
+    "       # Check if the negation of the implication is not satisfiable for general expressions\n",
+    "       print(f'Expression 1 is: {expr1}, and its type is {type(expr1)}')\n",
+    "       print(f'Expression 2 is: {expr2}, and its type is {type(expr2)}')\n",
+    "       negation = sp.And(expr1, Not(expr2))\n",
+    "       result = not satisfiable(negation, use_lra_theory=True)\n",
+    "       print(f\"Implication {expr1} -> {expr2} using satisfiable: {result}\")\n",
+    "       return result\n",
+    "\n",
     "\n",
     "# Example usage\n",
     "# predicate1 = \"_getIdentifierWhitelist().isIdentifierSupported(_priceIdentifier)\"\n",
@@ -242,20 +241,20 @@
     "# predicate1 = \"(_tTotalpercentBuy)/divisorBuy>=(10000/5000)\" \n",
     "# predicate2 = \"(_tTotalpercentBuy)/divisorBuy>=(10000/1000)\"\n",
     "\n",
-    "# predicate1 = \"12 < a\"\n",
-    "# predicate2 = \"a < 12\"\n",
+    "predicate1 = \"12 < a\"\n",
+    "predicate2 = \"a < 12\"\n",
     "\n",
     "\n",
     "\n",
-    "# predicate1 = \"a < 12\"\n",
-    "# predicate2 = \"a < 13\"\n",
+    "predicate1 = \"a < 12\"\n",
+    "predicate2 = \"a < 13\"\n",
     "\n",
     "# predicate1 = \"a < 12\"\n",
     "# predicate2 = \"a == 12\"\n",
     "\n",
-    "predicate1 = \"balanceOf(to)<=holdLimitAmount-amount\" \n",
-    "predicate2 = \"balanceOf(to)+amount<=holdLimitAmount\" \n",
     "\n",
+    "# predicate1 = \"balanceOf(to)<=holdLimitAmount-amount\" \n",
+    "# predicate2 = \"balanceOf(to)+amount<=holdLimitAmount\" \n",
     "\n",
     "comparator = Comparator()\n",
     "result = comparator.compare(predicate1, predicate2)\n",