From 337b6f3f9ca34f23c5d5623dda17c09f18f95019 Mon Sep 17 00:00:00 2001 From: Marco Biasion Date: Fri, 13 Sep 2024 09:44:00 +0200 Subject: [PATCH] #81: added utils.function. utils cleanup. removed unused files --- sxpat/distance_function.py | 253 ------------------------------------- sxpat/utils/collections.py | 9 +- sxpat/utils/functions.py | 27 ++++ sxpat/utils/inheritance.py | 5 +- sxpat/utils/utils.py | 44 ------- 5 files changed, 38 insertions(+), 300 deletions(-) delete mode 100644 sxpat/distance_function.py create mode 100644 sxpat/utils/functions.py delete mode 100644 sxpat/utils/utils.py diff --git a/sxpat/distance_function.py b/sxpat/distance_function.py deleted file mode 100644 index 4de72ab7b..000000000 --- a/sxpat/distance_function.py +++ /dev/null @@ -1,253 +0,0 @@ -from __future__ import annotations -from typing import List, Optional, Sequence, Tuple -from abc import abstractmethod - -from sxpat.utils.utils import call_z3_function, declare_z3_function, declare_z3_gate - - -class DistanceFunction: - def __init__(self) -> None: - raise NotImplementedError(f"Class `{self.__class__.__name__}` is an abstract class.") - - @property - @abstractmethod - def name(self): - raise NotImplementedError(f"Property `{self.__class__.__name__}.name` is an abstract property.") - - @property - @abstractmethod - def abbreviation(self): - raise NotImplementedError(f"Property `{self.__class__.__name__}.abbreviation` is an abstract property.") - - @property - @abstractmethod - def min_distance(self) -> int: - """The minimum value above 0 this function can be.""" - raise NotImplementedError(f"Property `{self.__class__.__name__}.min_distance` is an abstract property.") - - @abstractmethod - def with_no_input(self): - raise NotImplementedError(f"Method `{self.__class__.__name__}.with_no_input` is an abstract method.") - - @abstractmethod - def declare(self, prefix: str = None) -> List[str]: - raise NotImplementedError(f"Method `{self.__class__.__name__}.declare` is an abstract method.") - - @abstractmethod - def assign(self, vars_1: Sequence[str], vars_2: Sequence[str], prefix: str = None) -> List[str]: - raise NotImplementedError(f"Method `{self.__class__.__name__}.assign` is an abstract method.") - - @staticmethod - def _prefix(prefix: Optional[str]) -> str: - return f"{prefix}_" if prefix else "" - - -class HammingDistance(DistanceFunction): - def __init__(self, inputs: Sequence[str]) -> None: - self._inputs: Tuple[str] = tuple(inputs) - - name = property(lambda s: "Hamming Distance") - abbreviation = property(lambda s: "HamD") - - min_distance = property(lambda s: 1) - - def with_no_input(self): - return type(self)([]) - - @classmethod - def _declare(cls, inputs: Sequence[str], prefix: str) -> List[str]: - return [ - declare_z3_function( - f"{prefix}val", len(inputs), - "z3.BoolSort()", "z3.IntSort()" - ), - ( - f"{prefix}out_dist = " - + call_z3_function(f"{prefix}val", inputs) - ) - ] - - @classmethod - def _assign(cls, - inputs: Sequence[str], - vars_1: Sequence[str], vars_2: Sequence[str], - prefix: str): - parts = [ - f"{call_z3_function(v1, inputs)} != {call_z3_function(v2, inputs)}" - for v1, v2 in zip(vars_1, vars_2) - ] - return [ - "# Function: hamming distance", - call_z3_function(f"{prefix}val", inputs) + f" == z3.Sum({', '.join(parts)})," - ] - - def declare(self, prefix: str = None) -> List[str]: - return self._declare(self._inputs, self._prefix(prefix)) - - def assign(self, - vars_1: Sequence[str], vars_2: Sequence[str], - prefix: str = None) -> List[str]: - return self._assign( - self._inputs, - vars_1, vars_2, - self._prefix(prefix), - ) - - -class WeightedHammingDistance(DistanceFunction): - def __init__(self, inputs: Sequence[str], weights: Sequence[int]) -> None: - self._inputs: Tuple[str] = tuple(inputs) - self._weights: Tuple[int] = tuple(weights) - - name = property(lambda s: "Weighted Hamming Distance") - abbreviation = property(lambda s: "WHamD") - - min_distance = property(lambda s: min(s._weights)) - - def with_no_input(self): - return type(self)([], self._weights) - - @classmethod - def _declare(cls, inputs: Sequence[str], prefix: str) -> List[str]: - return [ - declare_z3_function( - f"{prefix}val", len(inputs), - "z3.BoolSort()", "z3.IntSort()" - ), - ( - f"{prefix}out_dist = " - + call_z3_function(f"{prefix}val", inputs) - ) - ] - - @classmethod - def _assign(cls, - inputs: Sequence[str], - vars_1: Sequence[str], vars_2: Sequence[str], - weights: Sequence[int], prefix: str): - parts = [ - f"z3.If({call_z3_function(v1, inputs)} != {call_z3_function(v2, inputs)}, {w}, 0)" - for v1, v2, w in zip(vars_1, vars_2, weights) - ] - return [ - "# Function: weighted hamming distance", - call_z3_function(f"{prefix}val", inputs) + f" == z3.Sum({', '.join(parts)})," - ] - - def declare(self, prefix: str = None) -> List[str]: - return self._declare(self._inputs, self._prefix(prefix)) - - def assign(self, - vars_1: Sequence[str], vars_2: Sequence[str], - prefix: str = None) -> List[str]: - return self._assign( - self._inputs, - vars_1, vars_2, - self._weights, - self._prefix(prefix), - ) - - -class WeightedAbsoluteDifference(DistanceFunction): - def __init__(self, - inputs: Sequence[str], weights: Sequence[int] - ) -> None: - self._inputs: Tuple[str] = tuple(inputs) - self._weights: Tuple[int] = tuple(weights) - - name = property(lambda s: "Absolute Difference of Weighted Sums") - abbreviation = property(lambda s: "WAD") - - min_distance = property(lambda s: min(s._weights)) - - def with_no_input(self): - return type(self)([], self._weights) - - @classmethod - def _declare(cls, - inputs: Sequence[str], prefix: str - ) -> List[str]: - return [ - *[ - declare_z3_function( - f"{prefix}val1", len(inputs), - "z3.BoolSort()", "z3.IntSort()" - ), - declare_z3_function( - f"{prefix}val2", len(inputs), - "z3.BoolSort()", "z3.IntSort()" - ), - ], - ( - f"{prefix}out_dist = z3.Abs(" - + call_z3_function(f"{prefix}val1", inputs) - + " - " - + call_z3_function(f"{prefix}val2", inputs) - + ")" - ) - ] - - @classmethod - def _assign_one(cls, - val_name: str, inputs: Sequence[str], - vars: Sequence[str], weights: Sequence[int] - ) -> str: - vars = [ - call_z3_function(v, inputs) + f'*{w}' - for v, w in zip(vars, weights) - ] - return ( - f"{call_z3_function(val_name, inputs)} == " - + f"z3.Sum({', '.join(vars)})" - ) - - @classmethod - def _assign(cls, - inputs: Sequence[str], - vars_1: Sequence[str], vars_2: Sequence[str], - weights: Sequence[int], prefix: str - ) -> List[str]: - return [ - "# Function: weighted sum absolute difference", - cls._assign_one(f"{prefix}val1", inputs, vars_1, weights) + ",", - cls._assign_one(f"{prefix}val2", inputs, vars_2, weights) + ",", - ] - - def declare(self, prefix: str = None) -> List[str]: - return self._declare(self._inputs, self._prefix(prefix)) - - def assign(self, - vars_1: Sequence[str], vars_2: Sequence[str], - prefix: str = None) -> List[str]: - return self._assign( - self._inputs, - vars_1, vars_2, - self._weights, - self._prefix(prefix), - ) - -# class IntegerAbsoluteDifference(WeightedAbsoluteDifference): -# def __init__(self) -> None: -# super().__init__([]) - -# name = property(lambda s: "Integer Absolute Difference") -# abbreviation = property(lambda s: "IAD") - -# @classmethod -# def _declare(cls, -# vars_1: Iterable[str], vars_2: Iterable[str], -# prefix: str) -> List[str]: -# lines = super()._declare( -# vars_1, vars_2, prefix, -# [2**i for i in range(len(vars_1))] -# ) -# lines[0] = "# Function: integer sum absolute difference" -# return lines - -# def declare(self, -# vars_1: Iterable[str], vars_2: Iterable[str], -# prefix: str = None) -> List[str]: -# return self._declare( -# vars_1, vars_2, -# self._prefix(prefix) -# ) diff --git a/sxpat/utils/collections.py b/sxpat/utils/collections.py index 526f64a91..98f625bb9 100644 --- a/sxpat/utils/collections.py +++ b/sxpat/utils/collections.py @@ -1,8 +1,9 @@ from __future__ import annotations from collections import UserDict -from typing import Iterable, Iterator, Mapping, Sequence, Tuple, Type, TypeVar, Union +from typing import Iterable, Iterator, Mapping, Tuple, Type, TypeVar -import itertools + +__all__ = ['mapping_inv', 'flat', 'pairwise', 'MultiDict', 'InheritanceMapping'] NOTHING = object() @@ -39,6 +40,10 @@ def pairwise(iterable: Iterable[T]) -> Iterator[Tuple[T, T]]: a = b +def unzip(iterable: Iterable) -> Iterable: + return zip(*iterable) + + class MultiDict(UserDict, Mapping[K, V]): def __init__(self, mapping: Mapping[Iterable[K], V] = None) -> None: super().__init__() diff --git a/sxpat/utils/functions.py b/sxpat/utils/functions.py new file mode 100644 index 000000000..139f344e6 --- /dev/null +++ b/sxpat/utils/functions.py @@ -0,0 +1,27 @@ +from typing import Callable, TypeVar + + +__all__ = ['get_producer', 'identity', 'str_to_bool'] + + +T = TypeVar('T') + + +def get_producer(value: T) -> Callable[[], T]: + return lambda: value + + +def identity(value: T) -> T: + return value + + +STR_TO_BOOL = { + 'true': True, + 't': True, + 'false': False, + 'f': False, +} + + +def str_to_bool(string: str) -> bool: + return STR_TO_BOOL[string.lower()] diff --git a/sxpat/utils/inheritance.py b/sxpat/utils/inheritance.py index d6ab241a1..11559b506 100644 --- a/sxpat/utils/inheritance.py +++ b/sxpat/utils/inheritance.py @@ -1,4 +1,7 @@ -from typing import List, Set, Type +from typing import Set, Type + + +__all__ = ['get_all_subclasses', 'get_all_leaves_subclasses'] def get_all_subclasses(cls: Type) -> Set[Type]: diff --git a/sxpat/utils/utils.py b/sxpat/utils/utils.py deleted file mode 100644 index 99f89e700..000000000 --- a/sxpat/utils/utils.py +++ /dev/null @@ -1,44 +0,0 @@ -# typing -from __future__ import annotations -from typing import Iterable - - -# Z3Log libs -from Z3Log.config.config import TAB - - -def indent_lines(lines: Iterable[str], indent_amount: int = 1) -> Iterable[str]: - """Indent the lines by the wanted amound.""" - return (TAB * indent_amount + line for line in lines) - - -def format_lines(lines: Iterable[str], indent_amount: int = 0, extra_newlines: int = 0) -> str: - """Join lines into a single string, indenting each line by the wanted amount and adding extra newlines at the end if needed.""" - return "\n".join(indent_lines(lines, indent_amount)) + "\n" * (1 + extra_newlines) - - -def unzip(it: Iterable) -> Iterable: - return zip(*it) - - -# > Z3 functions -def declare_z3_function(name: str, input_count: int, input_type: str, output_type: str) -> str: - """NOTE: If the input count is 0, then the result will be a variable and not a function""" - if input_count == 0: - # remove the sort-ref part, keep the pure type - output_type = output_type.replace("Sort()", "") - return f"{name} = {output_type}('{name}')" - else: - return f"{name} = z3.Function('{name}', {', '.join([input_type]*input_count)}, {output_type})" - - -def declare_z3_gate(name: str) -> str: - return f"{name} = z3.Bool('{name}')" - - -def call_z3_function(name: str, arguments: Iterable[str]) -> str: - """NOTE: If the arguments count is 0, then the result will be a variable use and not a function call""" - if len(arguments) == 0: - return name - else: - return f"{name}({', '.join(arguments)})"