Source code for logic1.theories.Sets.simplify

"""
This module implements *deep simplification* through the generation and
propagation of internal representations during recursion. It is an adaptation
of the *standard simplifier* from [DolzmannSturm-1997]_ tailored to the
specific requirements of Sets.
"""
from __future__ import annotations

from typing import Iterable, Iterator, Never, Optional, Self

from ... import abc
from dataclasses import dataclass, field

from ...firstorder import And, _F, Or, _T
from .atomic import AtomicFormula, C, C_, Eq, Index, Ne, oo, Variable
from .typing import Formula

from ...support.tracing import trace  # noqa


@dataclass(frozen=True)
class UnionFind:
    _parents: dict[Variable, Variable] = field(default_factory=dict)

    def copy(self) -> UnionFind:
        return UnionFind(self._parents.copy())

    def find(self, v: Variable) -> Variable:
        try:
            root = self.find(self._parents[v])
        except KeyError:
            return v
        self._parents[v] = root
        return root

    def union(self, v1: Variable, v2: Variable) -> None:
        root1 = self.find(v1)
        root2 = self.find(v2)
        if root1 == root2:
            return
        if Variable.sort_key(root1) <= Variable.sort_key(root2):
            self._parents[root2] = root1
        else:
            self._parents[root1] = root2

    def equations(self) -> Iterator[Eq]:
        for y in self._parents:
            yield Eq(self.find(y), y)


[docs] class InternalRepresentation( abc.simplify.InternalRepresentation[AtomicFormula, Variable, Variable, Never]): """Implements the abstract methods :meth:`add() <.abc.simplify.InternalRepresentation.add>`, :meth:`extract() <.abc.simplify.InternalRepresentation.extract>`, and :meth:`next_() <.abc.simplify.InternalRepresentation.next_>` of it super class :class:`.abc.simplify.InternalRepresentation`. Required by :class:`.Sets.simplify.Simplify` for instantiating the type variable :data:`.abc.simplify.ρ` of :class:`.abc.simplify.Simplify`. """ _ref_min_card: Index _ref_max_card: Index _ref_equations: UnionFind _ref_inequations: set[Ne] _cur_min_card: Index _cur_max_card: Index _cur_equations: UnionFind _cur_inequations: set[Ne] def __init__(self) -> None: self._ref_min_card = 1 self._ref_max_card = oo self._ref_equations = UnionFind() self._ref_inequations = set() self._cur_min_card = 1 self._cur_max_card = oo self._cur_equations = UnionFind() self._cur_inequations = set() def __repr__(self) -> str: return (f'InternalRepresentation([{self._ref_min_card}..{self._ref_max_card}], ' f'{self._ref_equations}, {self._ref_inequations} | ' f'[{self._cur_min_card}..{self._cur_max_card}], ' f'{self._cur_equations}, {self._cur_inequations})') def add(self, gand: type[And | Or], atoms: Iterable[AtomicFormula]) -> abc.simplify.Restart: """Implements the abstract method :meth:`.abc.simplify.InternalRepresentation.add`. """ for atom in atoms: if gand is Or: atom = atom.to_complement() # Collect information match atom: case C(index=n): if n > self._cur_min_card: self._cur_min_card = n if self._cur_min_card > self._cur_max_card: raise InternalRepresentation.Inconsistent() case C_(index=n): if n - 1 < self._cur_max_card: self._cur_max_card = n - 1 if self._cur_min_card > self._cur_max_card: raise InternalRepresentation.Inconsistent() case Eq(lhs=lhs, rhs=rhs): self._cur_equations.union(lhs, rhs) case Ne(lhs=lhs, rhs=rhs): self._cur_inequations.add(atom) case _: assert False for ne in self._cur_inequations: if self._cur_equations.find(ne.lhs) == self._cur_equations.find(ne.rhs): raise InternalRepresentation.Inconsistent() for ne in self._cur_inequations: if self._cur_equations.find(ne.lhs) == self._cur_equations.find(ne.rhs): raise InternalRepresentation.Inconsistent() return abc.simplify.Restart.OTHERS def extract(self, gand: type[And | Or]) -> list[AtomicFormula]: """Implements the abstract method :meth:`.abc.simplify.InternalRepresentation.extract`. """ def canonicalize(ne: Ne) -> Ne: ne_subs = ne.subs({ne.lhs: self._cur_equations.find(ne.lhs), ne.rhs: self._cur_equations.find(ne.rhs)}) if Variable.sort_key(ne_subs.lhs) <= Variable.sort_key(ne_subs.rhs): return ne_subs else: return Ne(ne_subs.rhs, ne_subs.lhs) L: list[AtomicFormula] = [] if self._cur_min_card > self._ref_min_card: L.append(C(self._cur_min_card)) if self._cur_max_card < self._ref_max_card: L.append(C_(self._cur_max_card + 1)) for eq in self._cur_equations.equations(): if self._ref_equations.find(eq.lhs) != self._ref_equations.find(eq.rhs): L.append(eq) canonical_ref_inequations = {canonicalize(ne) for ne in self._ref_inequations} for ne in self._cur_inequations: ne = canonicalize(ne) if ne not in canonical_ref_inequations: L.append(ne) if gand is Or: L = [atom.to_complement() for atom in L] return L def next_(self, remove: Optional[Variable] = None) -> Self: """Implements the abstract method :meth:`.abc.simplify.next_`. """ result = self.__class__() result._ref_min_card = self._cur_min_card result._ref_max_card = self._cur_max_card if remove is None: result._ref_equations = self._cur_equations.copy() result._ref_inequations = self._cur_inequations.copy() else: result._ref_equations = UnionFind() for eq in self._cur_equations.equations(): if remove not in eq.fvars(): result._ref_equations.union(eq.lhs, eq.rhs) result._ref_inequations = {ne for ne in self._cur_inequations if remove not in ne.fvars()} result._cur_min_card = result._ref_min_card result._cur_max_card = result._ref_max_card result._cur_equations = result._ref_equations.copy() result._cur_inequations = result._ref_inequations.copy() return result
[docs] class Simplify( abc.simplify.Simplify[AtomicFormula, Variable, Variable, Never, InternalRepresentation]): """Deep simplification in the style of [DolzmannSturm-1997]_. Implements the abstract methods :meth:`create_initial_representation <.abc.simplify.Simplify.create_initial_representation>` and :meth:`simpl_at <.abc.simplify.Simplify.simpl_at>` of its super class :class:`.abc.simplify.Simplify`. The simplifier should be called via :func:`.simplify`, as described below. In addition, this class inherits :meth:`.abc.simplify.Simplify.is_valid`, which should be called via :func:`.is_valid`, as described below. """ def create_initial_representation(self, assume=Iterable[AtomicFormula]) \ -> InternalRepresentation: """Implements the abstract method :meth:`.abc.simplify.Simplify.create_initial_representation`. """ ir = InternalRepresentation() for atom in assume: simplified_atom = self.simpl_at(atom, And) match simplified_atom: case AtomicFormula(): ir.add(And, [simplified_atom]) case _T(): continue case _F(): raise ir.Inconsistent() case _: assert False, simplified_atom return ir def simpl_at(self, atom: AtomicFormula, context: Optional[type[And] | type[Or]]) -> Formula: """Implements the abstract method :meth:`.abc.simplify.Simplify.simpl_at`. """ return atom.simplify()
simplify = Simplify().simplify is_valid = Simplify().is_valid