Skip to content

Instantly share code, notes, and snippets.

@rindPHI

rindPHI/Issue39.ipynb

Created January 3, 2023 10:16
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save rindPHI/551087dd4ff3a26f2d36b916333ecba1 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save rindPHI/551087dd4ff3a26f2d36b916333ecba1 to your computer and use it in GitHub Desktop.
Download ZIP
Display the source blob
Display the rendered blob
Raw
Issue39.ipynb
{
"cells": [
{
"cell_type": "markdown",
"id": "a02a8355-53c1-4bda-80e0-8baa507c43a3",
"metadata": {},
"source": [
"This notebook refers to [ISLa Issue 39](https://github.com/rindPHI/isla/issues/39)."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "fda3a93c-69e9-4b05-b1d8-4bc356b2ca8c",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Collecting isla-solver\n",
" Using cached isla_solver-1.9.9-py3-none-any.whl (198 kB)\n",
"Requirement already satisfied: wheel>=0.37.1 in ./venv/lib/python3.10/site-packages (from isla-solver) (0.38.4)\n",
"Requirement already satisfied: pathos>=0.2.9 in ./venv/lib/python3.10/site-packages (from isla-solver) (0.3.0)\n",
"Requirement already satisfied: toml>=0.10.2 in ./venv/lib/python3.10/site-packages (from isla-solver) (0.10.2)\n",
"Requirement already satisfied: grammar-to-regex>=0.0.4 in ./venv/lib/python3.10/site-packages (from isla-solver) (0.0.4)\n",
"Requirement already satisfied: proxyorderedset>=0.3.0 in ./venv/lib/python3.10/site-packages (from isla-solver) (0.3.1)\n",
"Requirement already satisfied: ijson>=3.1.4 in ./venv/lib/python3.10/site-packages (from isla-solver) (3.1.4)\n",
"Requirement already satisfied: datrie>=0.8.2 in ./venv/lib/python3.10/site-packages (from isla-solver) (0.8.2)\n",
"Requirement already satisfied: grammar-graph>=0.1.14 in ./venv/lib/python3.10/site-packages (from isla-solver) (0.1.14)\n",
"Requirement already satisfied: packaging>=21.3 in ./venv/lib/python3.10/site-packages (from isla-solver) (22.0)\n",
"Requirement already satisfied: z3-solver>=4.8.17.0 in ./venv/lib/python3.10/site-packages (from isla-solver) (4.11.2.0)\n",
"Requirement already satisfied: antlr4-python3-runtime>=4.11 in ./venv/lib/python3.10/site-packages (from isla-solver) (4.11.1)\n",
"Requirement already satisfied: fibheap>=0.2.1 in ./venv/lib/python3.10/site-packages (from grammar-graph>=0.1.14->isla-solver) (0.2.1)\n",
"Requirement already satisfied: graphviz>=0.20 in ./venv/lib/python3.10/site-packages (from grammar-graph>=0.1.14->isla-solver) (0.20.1)\n",
"Requirement already satisfied: pydot>=1.4.2 in ./venv/lib/python3.10/site-packages (from grammar-to-regex>=0.0.4->isla-solver) (1.4.2)\n",
"Requirement already satisfied: multiprocess>=0.70.14 in ./venv/lib/python3.10/site-packages (from pathos>=0.2.9->isla-solver) (0.70.14)\n",
"Requirement already satisfied: ppft>=1.7.6.6 in ./venv/lib/python3.10/site-packages (from pathos>=0.2.9->isla-solver) (1.7.6.6)\n",
"Requirement already satisfied: dill>=0.3.6 in ./venv/lib/python3.10/site-packages (from pathos>=0.2.9->isla-solver) (0.3.6)\n",
"Requirement already satisfied: pox>=0.3.2 in ./venv/lib/python3.10/site-packages (from pathos>=0.2.9->isla-solver) (0.3.2)\n",
"Requirement already satisfied: frozendict>=2.3.2 in ./venv/lib/python3.10/site-packages (from proxyorderedset>=0.3.0->isla-solver) (2.3.4)\n",
"Requirement already satisfied: pyparsing>=2.1.4 in ./venv/lib/python3.10/site-packages (from pydot>=1.4.2->grammar-to-regex>=0.0.4->isla-solver) (3.0.9)\n",
"Installing collected packages: isla-solver\n",
"Successfully installed isla-solver-1.9.9\n"
]
}
],
"source": [
"!python -m pip install isla-solver"
]
},
{
"cell_type": "markdown",
"id": "97a4dd46-5c82-42b9-8a83-9473ec3fc835",
"metadata": {},
"source": [
"The described behavior is that no solutions are found for a formula with the `count` predicate. This behavior can be reproduced using the following grammar with an epsilon production for `<sequence>`:"
]
},
{
"cell_type": "code",
"execution_count": 34,
"id": "c35b5cab-263a-4354-a3e0-b7e792f5badc",
"metadata": {},
"outputs": [],
"source": [
"grammar = \"\"\"\n",
"<start> ::= <sequences>\n",
"<sequences> ::= <sequence> <sequences> | \"\"\n",
"<sequence> ::= \"X\"\n",
"\"\"\""
]
},
{
"cell_type": "code",
"execution_count": 35,
"id": "6d87f326-d061-454b-8407-8e2eab01242c",
"metadata": {},
"outputs": [],
"source": [
"constraint = \"\"\"\n",
"exists int seqs: (\n",
" count(<start>, \"<sequence>\", seqs) and\n",
" str.to.int(seqs) >= 3\n",
" )\n",
"\"\"\""
]
},
{
"cell_type": "code",
"execution_count": 36,
"id": "dbef2e7b-6c21-432e-88a8-bf7a86d748d0",
"metadata": {},
"outputs": [],
"source": [
"from isla.solver import ISLaSolver"
]
},
{
"cell_type": "code",
"execution_count": 37,
"id": "3f5da431-7cb4-4671-829f-addb1e0f5c39",
"metadata": {},
"outputs": [],
"source": [
"solver = ISLaSolver(grammar, constraint)"
]
},
{
"cell_type": "code",
"execution_count": 39,
"id": "4a5fbc8c-2a7a-4704-bd6f-d549816e53f1",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"No solutions found.\n"
]
}
],
"source": [
"try:\n",
" print(solver.solve())\n",
"except StopIteration:\n",
" print(\"No solutions found.\")"
]
},
{
"cell_type": "markdown",
"id": "d1dcfd63-2562-4be3-af34-854038caac0d",
"metadata": {},
"source": [
"However, it does not occur with this equivalent grammar:"
]
},
{
"cell_type": "code",
"execution_count": 40,
"id": "b00a4d4d-db46-4804-8c60-d7c4a67f2582",
"metadata": {},
"outputs": [],
"source": [
"grammar = \"\"\"\n",
"<start> ::= <maybe-sequences>\n",
"<maybe-sequences> ::= \"\" | <sequences>\n",
"<sequences> ::= <sequence> <sequences> | <sequence>\n",
"<sequence> ::= \"X\"\n",
"\"\"\""
]
},
{
"cell_type": "code",
"execution_count": 41,
"id": "9452e44c-32ed-4e79-9da9-f9f4bedb0cb4",
"metadata": {},
"outputs": [],
"source": [
"solver = ISLaSolver(grammar, constraint)"
]
},
{
"cell_type": "code",
"execution_count": 43,
"id": "87a0f376-6117-465f-9bf9-75f509955742",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"XXXX\n"
]
}
],
"source": [
"print(solver.solve())"
]
},
{
"cell_type": "markdown",
"id": "32b96334-ed02-4147-ae6e-e05ad8394a2c",
"metadata": {},
"source": [
"Note that to obtain multiple solutions, you need to enable multiple SMT solver queries and *dis*able the restriction to unique trees in the queue. To get more diverse solutions, we additionally restrict the number of free instantiations to 1."
]
},
{
"cell_type": "code",
"execution_count": 56,
"id": "c7e7c2b1-9529-44a2-84df-712f5edca1bd",
"metadata": {},
"outputs": [],
"source": [
"num_solutions = 10\n",
"solver = ISLaSolver(\n",
" grammar,\n",
" constraint,\n",
" max_number_smt_instantiations=num_solutions,\n",
" max_number_free_instantiations=1,\n",
" enforce_unique_trees_in_queue=False)"
]
},
{
"cell_type": "code",
"execution_count": 57,
"id": "60b06086-ec1a-497d-a436-4f018404b6a1",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"XXXXXXXXX\n",
"XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n",
"XXXXX\n",
"XXXXXXX\n",
"XXXXXX\n",
"XXXXXXXXXXXXXXXXXXXXXX\n",
"XXX\n",
"XXXX\n",
"XXXXXXXXXXXXXXXXXXXXXXX\n",
"XXXXXXXX\n"
]
}
],
"source": [
"for _ in range(num_solutions):\n",
" print(solver.solve())"
]
},
{
"cell_type": "markdown",
"id": "535f7419-9839-411c-b952-6c3867f86e61",
"metadata": {},
"source": [
"Concluding, there *is* a bug related to epsilon productions and the count predicate, but it can be worked around by eliminating the epsilon production in the quantified nonterminal."
]
},
{
"cell_type": "markdown",
"id": "a8bc03a6-33e5-400d-af31-3f417e0fbbae",
"metadata": {},
"source": [
"The problem is in lines 337ff. in `isla_predicates.py`:\n",
"\n",
"```python\n",
"if (\n",
" not candidate_more_needles_possible\n",
" and candidate_needle_occurrences == target_num_needle_occurrences\n",
"):\n",
" return SemPredEvalResult({in_tree: candidate})\n",
"```\n",
"\n",
"Here, we should additionally be able to replace additional `<sequences>` occurrences by empty expansions if the desired number of `<sequence>` nonterminals is reached. We will address this bug. "
]
}
],
"metadata": {
"kernelspec": {
"display_name": "tmpenv",
"language": "python",
"name": "tmpenv"
},
"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.10.9"
}
},
"nbformat": 4,
"nbformat_minor": 5
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment