"""
Lattice
=======
Interface of a lattice. Lattice elements support lattice operations.
:Author: Caterina Urban
"""
from abc import ABCMeta, abstractmethod
from enum import Enum
from functools import reduce
from typing import List
from lyra.core.utils import copy_docstring
[docs]class Lattice(metaclass=ABCMeta):
"""Mutable lattice element.
.. warning::
Lattice operations modify the current lattice element.
Subclasses are expected to provide consistent method implementations for
``bottom()``, ``is_bottom()``, ``top()`` and ``is_top()``.
"""
def __eq__(self, other: 'Lattice'):
return isinstance(other, self.__class__) and repr(self) == repr(other)
def __ne__(self, other: 'Lattice'):
return not (self == other)
def __hash__(self):
return hash(repr(self))
@abstractmethod
def __repr__(self):
"""Unambiguous string representation of the current lattice element.
:return: unambiguous string representation
"""
[docs] @abstractmethod
def bottom(self):
"""Bottom lattice element.
:return: current lattice element modified to be the bottom lattice element
"""
[docs] @abstractmethod
def top(self):
"""Top lattice element.
:return: current lattice element modified to be the top lattice element
"""
[docs] @abstractmethod
def is_bottom(self) -> bool:
"""Test whether the lattice element is bottom.
:return: whether the lattice element is bottom
"""
[docs] @abstractmethod
def is_top(self) -> bool:
"""Test whether the lattice element is top.
:return: whether the lattice element is top
"""
@abstractmethod
def _less_equal(self, other: 'Lattice') -> bool:
"""Partial order between default lattice elements.
:param other: other lattice element
:return: whether the current lattice element is less than or equal to the other element
"""
[docs] def less_equal(self, other: 'Lattice') -> bool:
"""Partial order between lattice elements.
:param other: other lattice element
:return: whether the current lattice element is less than or equal to the other element
"""
if self.is_bottom() or other.is_top():
return True
elif other.is_bottom() or self.is_top():
return False
else:
return self._less_equal(other)
@abstractmethod
def _join(self, other: 'Lattice') -> 'Lattice':
"""Least upper bound between default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the least upper bound
"""
[docs] def join(self, other: 'Lattice') -> 'Lattice':
"""Least upper bound between lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the least upper bound
"""
if self.is_bottom() or other.is_top():
return self._replace(other)
elif other.is_bottom() or self.is_top():
return self
else:
return self._join(other)
[docs] def big_join(self, elements: List['Lattice']) -> 'Lattice':
"""Least upper bound between multiple lattice elements.
:param elements: lattice elements to compute the least upper bound of
:return: current lattice element modified to be the least upper bound
"""
return reduce(lambda s1, s2: s1.join(s2), elements, self.bottom())
@abstractmethod
def _meet(self, other: 'Lattice'):
"""Greatest lower bound between default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the greatest lower bound
"""
[docs] def meet(self, other: 'Lattice'):
"""Greatest lower bound between lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the greatest lower bound
"""
if self.is_top() or other.is_bottom():
return self._replace(other)
elif other.is_top() or self.is_bottom():
return self
else:
return self._meet(other)
[docs] def big_meet(self, elements: List['Lattice']) -> 'Lattice':
"""Greatest lower bound between multiple lattice elements.
:param elements: lattice elements to compute the greatest lower bound of
:return: current lattice element modified to be the least upper bound
"""
return reduce(lambda s1, s2: s1.meet(s2), elements, self.top())
@abstractmethod
def _widening(self, other: 'Lattice'):
"""Widening between default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the widening
"""
[docs] def widening(self, other: 'Lattice'):
"""Widening between lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the widening
"""
if self.is_bottom() or other.is_top():
return self._replace(other)
elif other.is_bottom() or self.is_top():
return self
else:
return self._widening(other)
def _replace(self, other: 'Lattice') -> 'Lattice':
"""Replace this instance with another lattice element.
:param other: other lattice element
:return: current lattice element updated to be equal to other
"""
self.__dict__.update(other.__dict__)
return self
[docs]class KindMixin(Lattice, metaclass=ABCMeta):
"""Mixin to add an explicit distinction between bottom, default, and top lattice elements."""
[docs] class Kind(Enum):
"""Kind of a lattice element."""
TOP = 3
DEFAULT = 2
BOTTOM = 1
def __init__(self):
"""Create a default lattice element."""
self._kind = KindMixin.Kind.DEFAULT
@property
def kind(self):
"""The kind of the current lattice element."""
return self._kind
@kind.setter
def kind(self, kind: 'KindMixin.Kind'):
self._kind = kind
[docs]class BottomMixin(KindMixin, metaclass=ABCMeta):
"""Mixin to add a predefined bottom element to a lattice.
.. warning::
Subclasses are expected to provide consistent method implementations
that check for the eventuality of ``is_bottom()`` being true.
"""
[docs] @copy_docstring(Lattice.bottom)
def bottom(self):
self._kind = KindMixin.Kind.BOTTOM
return self
[docs] @copy_docstring(Lattice.is_bottom)
def is_bottom(self) -> bool:
return self._kind == KindMixin.Kind.BOTTOM
[docs]class TopMixin(KindMixin, metaclass=ABCMeta):
"""Mixin to add a predefined top element to another lattice.
.. warning::
Subclasses are expected to provide consistent method implementations
that check for the eventuality of ``is_top()`` being true.
"""
[docs] @copy_docstring(Lattice.top)
def top(self):
self._kind = KindMixin.Kind.TOP
return self
[docs] @copy_docstring(Lattice.is_top)
def is_top(self) -> bool:
return self._kind == KindMixin.Kind.TOP
[docs]class BoundedLattice(TopMixin, BottomMixin, metaclass=ABCMeta):
"""Mutable lattice element, with predefined bottom and top elements.
.. warning::
Lattice operations modify the current lattice element.
"""
[docs] @copy_docstring(Lattice.bottom)
def bottom(self) -> 'BoundedLattice':
self.kind = KindMixin.Kind.BOTTOM
return self
[docs] @copy_docstring(Lattice.top)
def top(self) -> 'BoundedLattice':
self.kind = KindMixin.Kind.TOP
return self
[docs] @copy_docstring(Lattice.is_bottom)
def is_bottom(self) -> bool:
return self.kind == KindMixin.Kind.BOTTOM
[docs] @copy_docstring(Lattice.is_top)
def is_top(self) -> bool:
return self.kind == KindMixin.Kind.TOP
[docs]class ArithmeticMixin(Lattice, metaclass=ABCMeta):
"""Mixin to add arithmetic operations to a lattice."""
@abstractmethod
def _neg(self) -> 'ArithmeticMixin':
"""Negation of a default lattice elements.
:return: current lattice element modified to be its negation
"""
[docs] def neg(self) -> 'ArithmeticMixin':
"""Negation of a lattice elements.
:return: current lattice element modified to be its negation
"""
if self.is_bottom():
return self
else:
return self._neg()
@abstractmethod
def _add(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Addition between two default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the sum
"""
[docs] def add(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Addition between two lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the sum
"""
if self.is_bottom():
return self
elif other.is_bottom():
return self._replace(other)
else:
return self._add(other)
@abstractmethod
def _sub(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Subtraction between two default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the difference
"""
[docs] def sub(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Subtraction between two lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the difference
"""
if self.is_bottom():
return self
elif other.is_bottom():
return self._replace(other)
else:
return self._sub(other)
@abstractmethod
def _mult(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Multiplication between two default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the product
"""
[docs] def mult(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Multiplication between two lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the product
"""
if self.is_bottom():
return self
elif other.is_bottom():
return self._replace(other)
else:
return self._mult(other)
@abstractmethod
def _div(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Division between two default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the division
"""
[docs] def div(self, other: 'ArithmeticMixin') -> 'ArithmeticMixin':
"""Multiplication between two lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the product
"""
if self.is_bottom():
return self
elif other.is_bottom():
return self._replace(other)
else:
return self._div(other)
[docs]class BooleanMixin(Lattice, metaclass=ABCMeta):
"""Mixin to add boolean operations to a lattice."""
[docs] @abstractmethod
def false(self) -> 'BooleanMixin':
"""False lattice element.
:return: current lattice element modified to be the false lattice element
"""
[docs] @abstractmethod
def true(self) -> 'BooleanMixin':
"""True lattice element.
:return: current lattice element modified to be the true lattice element
"""
[docs] @abstractmethod
def maybe(self) -> 'BooleanMixin':
"""Maybe lattice element.
:return: current lattice element modified to be the maybe lattice element
"""
[docs] @abstractmethod
def is_false(self) -> bool:
"""Test whether the lattice element is false.
:return: whether the lattice element is false
"""
[docs] @abstractmethod
def is_true(self) -> bool:
"""Test whether the lattice element is true.
:return: whether the lattice element is true
"""
[docs] @abstractmethod
def is_maybe(self) -> bool:
"""Test whether the lattice element is maybe.
:return: whether the lattice element is maybe
"""
def _compl(self) -> 'BooleanMixin':
"""Complement of a default lattice elements.
:return: current lattice element modified to be its complement
"""
if self.is_false():
return self.true()
elif self.is_true():
return self.false()
return self
[docs] def compl(self) -> 'BooleanMixin':
"""Complement of a lattice elements.
:return: current lattice element modified to be its complement
"""
if self.is_bottom():
return self
else:
return self._compl()
def _conj(self, other: 'BooleanMixin') -> 'BooleanMixin':
"""Conjunction between two default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the conjunction
"""
if self.is_false() or other.is_false():
return self.false()
elif self.is_maybe() or other.is_maybe():
return self.maybe()
return self.true()
[docs] def conj(self, other: 'BooleanMixin') -> 'BooleanMixin':
"""Conjunction between two lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the conjunction
"""
if self.is_bottom():
return self
elif other.is_bottom():
return self._replace(other)
else:
return self._conj(other)
def _disj(self, other: 'BooleanMixin') -> 'BooleanMixin':
"""Disjunction between two default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the disjunction
"""
if self.is_true() or other.is_true():
return self.true()
elif self.is_maybe() or other.is_maybe():
return self.maybe()
return self.false()
[docs] def disj(self, other: 'BooleanMixin') -> 'BooleanMixin':
"""Disjunction between two lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the disjunction
"""
if self.is_bottom():
return self
elif other.is_bottom():
return self._replace(other)
else:
return self._disj(other)
[docs]class SequenceMixin(Lattice, metaclass=ABCMeta):
"""Mixin to add sequence operations to a lattice."""
@abstractmethod
def _concat(self, other: 'SequenceMixin') -> 'SequenceMixin':
"""Concatenation between two default lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the concatenation
"""
[docs] def concat(self, other: 'SequenceMixin') -> 'SequenceMixin':
"""Concatenation between two lattice elements.
:param other: other lattice element
:return: current lattice element modified to be the concatenation
"""
if self.is_bottom(): # self is the empty sequence
return self._replace(other)
elif other.is_bottom(): # other is the empty sequence
return self
else:
return self._concat(other)