from __future__ import annotations
import logging
import string
from typing import Any, ClassVar, Final, Iterator, Never, Optional, Self, TypeAlias
from logic1 import firstorder
from logic1.firstorder import _F, _T
logging.basicConfig(
format='%(levelname)s[%(relativeCreated)0.0f ms]: %(message)s',
level=logging.CRITICAL)
oo = float('Inf')
"""A symbolic name for the ``float('inf')`` as an :data:`.Index`.
"""
Index: TypeAlias = int | float
"""An index, which is either a positive integer or the ``float('inf')``, which
is represented by :data:`oo`.
"""
[docs]
class VariableSet(firstorder.VariableSet['Variable']):
"""The infinite set of all variables belonging to the theory of Sets.
Variables are uniquely identified by their name, which is a
:external:class:`.str`. This class is a singleton, whose single instance is
assigned to :data:`.VV`.
.. seealso::
Final methods inherited from the parent class:
* :meth:`.firstorder.term.VariableSet.get`
-- obtain several variables simultaneously
* :meth:`.firstorder.term.VariableSet.imp`
-- import variables into global namespace
"""
_instance: ClassVar[Optional[VariableSet]] = None
@property
def stack(self) -> list[set[str]]:
return self._stack
[docs]
def __getitem__(self, index: str) -> Variable:
"""Return the variable with the name ``index``. Implements abstract
method :meth:`.firstorder.term.VariableSet.__getitem__`.
>>> from logic1.theories.Sets import VV
>>> VV['x']
x
"""
match index:
case str():
self._used.update((index,))
return Variable(index)
case _:
raise ValueError(f'expecting string as index; {index} is {type(index)}')
def __init__(self) -> None:
self._stack: list[set[str]] = []
self._used: set[str] = set()
def __new__(cls) -> VariableSet:
if cls._instance is None:
cls._instance = super().__new__(cls)
return cls._instance
def __repr__(self) -> str:
s = ', '.join(str(g) for g in (*self._used, '...'))
return f'{{{s}}}'
[docs]
def fresh(self, suffix: str = '') -> Variable:
"""Return a fresh variable, by default from the sequence ``G0001``,
``G0002``, ..., ``G9999``, ``G10000``, ... This naming convention is
inspired by Lisp's ``gensym()``. If the optional argument ``suffix``
is specified, the sequence ``G0001<suffix>``, ``G0002<suffix>``, ...
is used instead.
"""
i = 1
v_as_str = f'G{i:04d}{suffix}'
while v_as_str in self._used:
i += 1
v_as_str = f'G{i:04d}{suffix}'
return self[v_as_str]
[docs]
def pop(self) -> None:
self._used = self._stack.pop()
[docs]
def push(self) -> None:
self._stack.append(self._used)
self._used = set()
VV = VariableSet()
"""The unique instance of :class:`.VariableSet`. This is a singleton.
"""
[docs]
class Variable(firstorder.Variable['Variable', Never, str]):
wrapped_variable_set: VariableSet = VV
string: str
[docs]
def __eq__(self, other: Variable) -> Eq: # type: ignore[override]
if isinstance(other, Variable):
return Eq(self, other)
raise ValueError(f'arguments must be terms - {other} is {type(other)}')
def __hash__(self) -> int:
return hash((tuple(str(cls) for cls in self.__class__.mro()), self.string))
def __init__(self, arg: str) -> None:
if not isinstance(arg, str):
raise ValueError(f'argument must be a string; {arg} is {type(arg)}')
self.string = arg
[docs]
def __ne__(self, other: Variable) -> Ne: # type: ignore[override]
if isinstance(other, Variable):
return Ne(self, other)
raise ValueError(f'arguments must be terms; {other} is {type(other)}')
def __repr__(self) -> str:
return self.string
[docs]
def as_latex(self) -> str:
"""LaTeX representation as a string. Implements the abstract method
:meth:`.firstorder.term.Term.as_latex`.
"""
base = self.string.rstrip(string.digits)
index = self.string[len(base):]
if index:
return f'{base}_{{{index}}}'
return base
[docs]
def fresh(self) -> Variable:
"""Returns a variable that has not been used so far. Implements
abstract method :meth:`.firstorder.term.Variable.fresh`.
"""
return self.wrapped_variable_set.fresh(suffix=f'_{str(self)}')
[docs]
def sort_key(self) -> str:
"""A sort key suitable for ordering instances of this class. Implements
the abstract method :meth:`.firstorder.term.Term.sort_key`.
"""
return self.string
[docs]
def subs(self, d: dict[Variable, Variable]) -> Variable:
"""Simultaneous substitution of variables for variables.
>>> from logic1.theories.Sets import VV
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = x
>>> f.subs({x: y, y: z})
y
"""
return d.get(self, self)
[docs]
def vars(self) -> Iterator[Variable]:
"""An iterator that yields this variable. Implements the abstract
method :meth:`.firstorder.term.Term.vars`.
"""
yield self
[docs]
class Eq(AtomicFormula):
@property
def lhs(self) -> Variable:
return self.args[0]
@property
def rhs(self) -> Variable:
return self.args[1]
def __bool__(self) -> bool:
return self.lhs.string == self.rhs.string
def __init__(self, lhs: Variable, rhs: Variable) -> None:
super().__init__()
for arg in (lhs, rhs):
if not isinstance(arg, Variable):
raise ValueError(
f'arguments must be variables; {arg} is {type(arg)}')
self.args = (lhs, rhs)
[docs]
class Ne(AtomicFormula):
@property
def lhs(self) -> Variable:
return self.args[0]
@property
def rhs(self) -> Variable:
return self.args[1]
def __bool__(self) -> bool:
return self.lhs.string != self.rhs.string
def __init__(self, lhs: Variable, rhs: Variable) -> None:
super().__init__()
for arg in (lhs, rhs):
if not isinstance(arg, Variable):
raise ValueError(
f'arguments must be variables - {arg} is {type(arg)}')
self.args = (lhs, rhs)
[docs]
class C(AtomicFormula):
"""Cardinality constraints. From a mathematical perspective, the instances
are constant relation symbols with an index, which is either a positive
integer or ``float('inf')``, represented as ``oo``. ``C(n)`` holds iff there
are at least ``n`` different elements in the universe. This is not a
statement about the index ``n`` but about a range of models where this
constant relation holds.
In the following example, ``f`` states that there should be at least 2
elements but not 3 elements or more:
>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = Ex([x, y], x != y) & All([x, y, z], Or(x == y, y == z, z == x))
>>> qe(f) # quantifier elimination:
And(C(2), C_(3))
The class constructor takes care that instances with equal indices are
identical:
>>> C(1) is C(1)
True
>>> C(1) == C(2)
False
"""
_instances: ClassVar[dict[Index, C]] = dict()
@property
def index(self) -> Index:
"""The index of the constant relation symbol
"""
return self.args[0]
def __init__(self, index: Index) -> None:
"""Implements abstract method
:meth:`firstorder.formula.Formula.__init__`.
"""
super().__init__()
self.args = (index,)
def __new__(cls, index: Index):
if not (isinstance(index, int) and index > 0 or index == oo):
raise ValueError(f'argument must be positive int or oo; '
f'{index} is {type(index)}')
if index not in cls._instances:
cls._instances[index] = super().__new__(cls)
return cls._instances[index]
[docs]
class C_(AtomicFormula):
"""Cardinality constraints. The class :class:`C_` is dual to :class:`C`;
more precisely, for every index ``n``, we have that ``C_(n)`` is the dual
relation of ``C(n)``, and vice versa.
"""
_instances: ClassVar[dict[Index, C_]] = dict()
@property
def index(self) -> Index:
"""The index of the constant relation symbol
"""
return self.args[0]
def __init__(self, index: Index) -> None:
"""Implements abstract method
:meth:`firstorder.formula.Formula.__init__`.
"""
super().__init__()
self.args = (index,)
def __new__(cls, index: Index):
if not (isinstance(index, int) and index > 0 or index == oo):
raise ValueError(f'argument must be positive int or oo; '
f'{index} is {type(index)}')
if index not in cls._instances:
cls._instances[index] = super().__new__(cls)
return cls._instances[index]
from logic1.theories.Sets.types import Formula