Merge pull request #28 from rindPHI/dev

dev

CHANGELOG.md

@@ -5,6 +5,23 @@ This file contains the notable changes in the ISLa project since version 0.2a1
 
 ## [unreleased]
 
+## [1.9.3] - 2022-11-10
+
+### Changed
+
+- Further improvements in input repair: Better ordering of abstracted trees. Now, all
+  abstractions are generated at once (not lazily in a generator), which *might* impact
+  performance; however, the results are ordered by tree size, i.e., less abstract trees
+  come first, which is the expected behavior. Code is simplified.
+
+## [1.9.2] - 2022-11-10
+
+### Changed
+
+- Improved input repair:
+  + Results are more local now, performance improvement for more complicated repairs
+  + Fixed tree abstraction for the top (empty) path
+
 ## [1.9.1] - 2022-11-08
 
 ### Changed

pyproject.toml

@@ -8,7 +8,7 @@ build-backend = "setuptools.build_meta"
 
 [project]
 name = "isla-solver"
-version = "1.9.1"
+version = "1.9.3"
 authors = [
     { name = "Dominic Steinhoefel", email = "dominic.steinhoefel@cispa.de" },
 ]

src/isla/__init__.py

@@ -16,4 +16,4 @@
 # You should have received a copy of the GNU General Public License
 # along with ISLa.  If not, see <http://www.gnu.org/licenses/>.
 
-__version__ = "1.9.1"
+__version__ = "1.9.3"

src/isla/solver.py

@@ -39,7 +39,6 @@
     cast,
     Callable,
     Iterable,
-    Generator,
 )
 
 import pkg_resources
@@ -497,6 +496,8 @@ def __init__(
         self.step_cnt: int = 0
         self.last_cost_recomputation: int = 0
 
+        self.regex_cache = {}
+
         self.solutions: List[DerivationTree] = []
 
         # Debugging stuff
@@ -536,7 +537,7 @@ def copy_without_queue(
         grammar_unwinding_threshold: Maybe[int] = Maybe.nothing(),
         initial_tree: Maybe[DerivationTree] = Maybe.nothing(),
     ):
-        return ISLaSolver(
+        result = ISLaSolver(
             grammar=grammar.orelse(lambda: self.grammar).get(),
             formula=formula.orelse(lambda: self.formula).get(),
             max_number_free_instantiations=max_number_free_instantiations.orelse(
@@ -571,6 +572,10 @@ def copy_without_queue(
             initial_tree=initial_tree,
         )
 
+        result.regex_cache = self.regex_cache
+
+        return result
+
     def check(self, inp: DerivationTree | str) -> bool:
         """
         Evaluates whether the given derivation tree satisfies the constraint passed to
@@ -651,8 +656,11 @@ def repair(
 
         inp = self.parse(inp, skip_check=True) if isinstance(inp, str) else inp
 
-        if self.check(inp) or not self.top_constant.is_present():
-            return Maybe(inp)
+        try:
+            if self.check(inp) or not self.top_constant.is_present():
+                return Maybe(inp)
+        except UnknownResultError:
+            pass
 
         formula = self.top_constant.map(
             lambda c: self.formula.substitute_expressions({c: inp})
@@ -727,7 +735,7 @@ def do_complete(tree: DerivationTree) -> Maybe[DerivationTree]:
                 if maybe_completed.is_present():
                     return maybe_completed
 
-        raise Maybe.nothing()
+        return Maybe.nothing()
 
     def mutate(
         self,
@@ -2871,8 +2879,10 @@ def quantified_formula_might_match(
             self.graph.reachable,
         )
 
-    @lru_cache(maxsize=None)
     def extract_regular_expression(self, nonterminal: str) -> z3.ReRef:
+        if nonterminal in self.regex_cache:
+            return self.regex_cache[nonterminal]
+
         regex_conv = RegexConverter(
             self.grammar,
             compress_unions=True,
@@ -2933,6 +2943,8 @@ def extract_regular_expression(self, nonterminal: str) -> z3.ReRef:
                     ), f"Input '{new_inp}' from regex language is not in grammar language."
                 prev.add(new_inp)
 
+        self.regex_cache[nonterminal] = z3_regex
+
         return z3_regex
 
 
@@ -3329,7 +3341,7 @@ def equivalent(
 
 def generate_abstracted_trees(
     inp: DerivationTree, participating_paths: Set[Path]
-) -> Generator[DerivationTree, None, None]:
+) -> List[DerivationTree]:
     """
     Yields trees that are more and more "abstracted," i.e., pruned, at prefixes of the
     paths specified in `participating_paths`.
@@ -3339,44 +3351,35 @@ def generate_abstracted_trees(
     :return: A generator of more and more abstract trees, beginning with the most
     concrete and ending with the most abstract ones.
     """
-    sub_paths = {
+    parent_paths: Set[ImmutableList[Path]] = {
         tuple(
-            [
-                (len(path) - i, tuple(path[:i]))
-                for i in reversed(range(1, len(path) + 1))
-            ]
+            [tuple(path[:i]) for i in reversed(range(1, len(path) + 1))]
+            if path
+            else [()]
         )
         for path in participating_paths
     }
 
-    already_seen: Set[frozenset[Path]] = set()
-    for l_diffs_and_paths in itertools.islice(
-        sorted(
-            itertools.product(*sub_paths),
-            key=lambda l_diffs_and_paths_: (
-                max(map(lambda t: t[0], l_diffs_and_paths_))
-            ),
-        ),
-        1,
-        None,
-    ):
-        for chosen_paths in [
-            tuple(eliminate_suffixes([c[1] for c in combination]))
-            for k in range(1, len(participating_paths) + 1)
-            for combination in itertools.combinations(l_diffs_and_paths, k)
-        ]:
-            if frozenset(chosen_paths) in already_seen:
-                continue
-            already_seen.add(frozenset(chosen_paths))
+    abstraction_candidate_combinations: Set[ImmutableList[Path]] = {
+        tuple(eliminate_suffixes(combination))
+        for k in range(1, len(participating_paths) + 1)
+        for paths in itertools.product(*parent_paths)
+        for combination in itertools.combinations(paths, k)
+    }
 
-            yield inp.substitute(
-                {
-                    inp.get_subtree(chosen_path): DerivationTree(
-                        inp.get_subtree(chosen_path).value
-                    )
-                    for chosen_path in chosen_paths
-                }
-            )
+    result: Dict[int, DerivationTree] = {}
+    for paths_to_abstract in abstraction_candidate_combinations:
+        abstracted_tree = inp.substitute(
+            {
+                inp.get_subtree(path_to_abstract): DerivationTree(
+                    inp.get_subtree(path_to_abstract).value
+                )
+                for path_to_abstract in paths_to_abstract
+            }
+        )
+        result[abstracted_tree.structural_hash()] = abstracted_tree
+
+    return sorted(result.values(), key=lambda tree: -len(tree))
 
 
 class EvaluatePredicateFormulasTransformer(NoopFormulaTransformer):