from __future__ import annotations
from dataclasses import dataclass
from enum import auto, Enum
from fractions import Fraction
from functools import lru_cache
from typing import (
Any, ClassVar, Final, Generic, Iterable, Iterator, Mapping, Optional, Self,
TypeVar)
from gmpy2 import mpq, sign
from sage.all import QQ
# Importing QQ from sage.rings.rational_fields causes problems. Notably, a
# fresh instance of RationalField is assigned to QQ in sage.all.
from sage.misc.latex import latex as sage_latex
from sage.rings.integer import Integer
from sage.rings.polynomial.multi_polynomial_libsingular import (
MPolynomial_libsingular as MPolynomial,
MPolynomialRing_libsingular as MPolynomialRing)
from sage.rings.polynomial.polynomial_ring_constructor import (
PolynomialRing as sage_PolynomialRing)
from sage.rings.polynomial.polynomial_element import (
Polynomial_generic_dense as UPolynomial)
from sage.rings.polynomial.term_order import TermOrder
from sage.rings.rational import Rational
from ... import firstorder
from ...firstorder import _T, _F
from ...support.excepthook import NoTraceException
from ...support.tracing import trace # noqa
τ = TypeVar('τ', bound='Term')
"""A type variable denoting a type of terms with upper bound
:class:`logic1.theories.RCF.Term`.
"""
CACHE_SIZE: Final[Optional[int]] = 2**16
def _caches():
from .simplify import Simplify
from .substitution import _SubstValue
return [Term.factor, _SubstValue.as_term, Simplify._simpl_at]
def cache_clear():
for cache in _caches():
cache.cache_clear()
def cache_info():
return {cache.__wrapped__: cache.cache_info() for cache in _caches()}
class _PolynomialRing:
sage_ring: MPolynomialRing
stack: list[MPolynomialRing]
def __call__(self, obj):
return self.sage_ring(obj)
def __init__(self, term_order='deglex'):
self.sage_ring = self.MPolynomialRing_factory('unused_', order=term_order)
self.stack = []
def __repr__(self):
return str(self.sage_ring)
def add_var(self, var: str) -> None:
new_vars = [str(g) for g in self.sage_ring.gens()]
assert var not in new_vars
new_vars.append(var)
new_vars.sort()
self.sage_ring = self.MPolynomialRing_factory(new_vars, order=self.sage_ring.term_order())
def add_vars(self, vars_: Iterable[str]) -> None:
def sort_key(s: str) -> tuple[str, int]:
base = s.rstrip('0123456789')
index = s[len(base):]
n = int(index) if index else -1
return base, n
new_vars = []
for g in self.sage_ring.gens():
new_vars.append(str(g))
have_appended = False
for v in vars_:
if v not in new_vars:
new_vars.append(v)
have_appended = True
if have_appended:
new_vars.sort(key=sort_key)
self.sage_ring = self.MPolynomialRing_factory(
new_vars, order=self.sage_ring.term_order())
def get_vars(self) -> tuple[MPolynomial[Integer], ...]:
gens = (g for g in self.sage_ring.gens() if str(g) != 'unused_')
return tuple(gens)
@staticmethod
def MPolynomialRing_factory(names: str | Iterable[str], order: TermOrder) -> MPolynomialRing:
return sage_PolynomialRing(QQ, names, order=order, implementation='singular')
def pop(self) -> None:
self.sage_ring = self.stack.pop()
def push(self) -> None:
self.stack.append(self.sage_ring)
self.sage_ring = self.MPolynomialRing_factory('unused_', order=self.sage_ring.term_order())
polynomial_ring = _PolynomialRing()
[docs]
class VariableSet(firstorder.atomic.VariableSet['Variable']):
"""The infinite set of all variables belonging to the theory of Real Closed
Fields. 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 parent class:
* :meth:`.firstorder.atomic.VariableSet.get`
-- obtain several variables simultaneously
* :meth:`.firstorder.atomic.VariableSet.imp`
-- import variables into global namespace
"""
polynomial_ring: ClassVar[_PolynomialRing] = polynomial_ring
@property
def stack(self) -> list[MPolynomialRing]:
"""Implements abstract property
:attr:`.firstorder.atomic.VariableSet.stack`.
"""
return self.polynomial_ring.stack
[docs]
def __getitem__(self, index: str) -> Variable:
"""Implements abstract method
:meth:`.firstorder.atomic.VariableSet.__getitem__`.
"""
match index:
case str():
self.polynomial_ring.add_vars((index,))
return Variable(self.polynomial_ring(index))
case _:
raise ValueError(f'expecting string as index; {index} is {type(index)}')
def __repr__(self) -> str:
vars_ = self.polynomial_ring.get_vars()
s = ', '.join(str(g) for g in (*vars_, '...'))
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 :data:`suffix` is specified, the
sequence G0001<suffix>, G0002<suffix>, ... is used instead.
"""
vars_ = set(str(g) for g in self.polynomial_ring.get_vars())
i = 1
v = f'G{i:04d}{suffix}'
while v in vars_:
i += 1
v = f'G{i:04d}{suffix}'
self.polynomial_ring.add_var(v)
return Variable(self.polynomial_ring(v))
[docs]
def pop(self) -> None:
from . import cache_clear
self.polynomial_ring.pop()
cache_clear()
[docs]
def push(self) -> None:
from . import cache_clear
self.polynomial_ring.push()
cache_clear()
VV = VariableSet()
"""
The unique instance of :class:`.VariableSet`.
"""
[docs]
class DEFINITE(Enum):
"""Information whether a certain term has positive or negative definiteness
properties; typically as a result of a heuristic test as in
:meth:`.Term.is_definite`.
"""
NEGATIVE = auto()
"""The polynomial negative definite, i.e., negative for all real choices of
variables.
"""
NEGATIVE_SEMI = auto()
"""The polynomial negative semi-definite, i.e., non-positive for all real
choices of variables.
"""
NONE = auto()
"""None of the other cases holds..
"""
POSITIVE = auto()
"""The polynomial positive definite, i.e., positive for all real choices of
variables.
"""
POSITIVE_SEMI = auto()
"""The polynomial positive semi-definite, i.e., non-negative for all real
choices of variables.
"""
ZERO = auto()
"""The polynomial is the zero polynomial.
"""
@dataclass
class SortKey(Generic[τ]):
term: τ
def __eq__(self, other: Self) -> bool: # type: ignore[override]
if hash(self.term) != hash(other.term):
return False
return self.term._poly == other.term._poly
def __ge__(self, other: Self) -> bool:
return self.term._poly >= other.term._poly
def __gt__(self, other: Self) -> bool:
return self.term._poly > other.term._poly
def __hash__(self) -> int:
return hash(self.term)
def __le__(self, other: Self) -> bool:
return self.term._poly <= other.term._poly
def __lt__(self, other: Self) -> bool:
return self.term._poly < other.term._poly
def __ne__(self, other: Self) -> bool: # type: ignore[override]
if hash(self.term) != hash(other.term):
return True
return self.term._poly != other.term._poly
[docs]
class Term(firstorder.Term['Term', 'Variable', int, SortKey['Term']]):
polynomial_ring: ClassVar[_PolynomialRing] = polynomial_ring
_hash: Optional[int] = None
_poly: MPolynomial[Rational]
# The property should be private. We might want a method to_sage()
@property
def poly(self) -> MPolynomial[Rational]:
"""
An instance of :class:`MPolynomial_libsingular
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular>`,
which is wrapped by ``self``.
"""
parent = self._poly.parent()
if parent is not self.polynomial_ring.sage_ring:
poly_gens = parent.gens()
# Make sure that the manager process in parallel qe knows all
# variables. Otherwise the following line could be replaced with an
# assertion.
self.polynomial_ring.add_vars(map(str, poly_gens))
# We currently coerce manually in: reduce, subs, derivative,
# pseudo_quo_rem. The following line might cleaner:
#
# self._poly = self.polynomial_ring(self._poly)
return self._poly
[docs]
def __add__(self, other: object) -> Term:
if isinstance(other, Term):
return Term(self.poly + other.poly)
if isinstance(other, mpq):
return Term(self.poly + Rational(other))
return Term(self.poly + other)
[docs]
def __eq__(self, other: Term | int) -> Eq: # type: ignore[override]
# MyPy requires "other: object". However, with our use a a constructor,
# it makes no sense to compare terms with general objects. We have
# Eq.__bool__, which supports some comparisons in boolean contexts.
# Same for __ne__.
lhs = self - other
if lhs.lc() < 0:
lhs = -lhs
return Eq(lhs, 0)
[docs]
def __ge__(self, other: Term | int) -> Ge | Le:
lhs = self - other
if lhs.lc() < 0:
return Le(-lhs, 0)
return Ge(lhs, 0)
[docs]
def __gt__(self, other: Term | int) -> Gt | Lt:
lhs = self - other
if lhs.lc() < 0:
return Lt(-lhs, 0)
return Gt(lhs, 0)
def __hash__(self) -> int:
if self._hash is None:
self._hash = hash(self.poly)
return self._hash
def __init__(self, arg: Fraction | int | Integer | MPolynomial[Rational]
| mpq | Rational | UPolynomial) -> None:
if isinstance(arg, MPolynomial):
self._poly = arg
elif isinstance(arg, (Fraction, int, Integer, mpq, Rational, UPolynomial)):
self._poly = self.polynomial_ring(arg)
else:
raise ValueError(f'expected polynomial, integer, or rational; {arg} is {type(arg)}')
[docs]
def __iter__(self) -> Iterator[tuple[mpq, Term]]:
"""Iterate over the polynomial representation of the term, yielding
pairs of coefficients and power products.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> [(abs(coef), power_product) for coef, power_product in t]
[(mpq(1,1), x^2), (mpq(2,1), x*y), (mpq(1,1), y^2), (mpq(4,1), x),
(mpq(4,1), y), (mpq(4,1), 1)]
"""
for coefficient, power_product in self.poly:
yield mpq(coefficient), Term(power_product)
[docs]
def __le__(self, other: Term | int | mpq) -> Ge | Le:
lhs = self - other
if lhs.lc() < 0:
return Ge(-lhs, 0)
return Le(lhs, 0)
[docs]
def __lt__(self, other: Term | int | mpq) -> Gt | Lt:
lhs = self - other
if lhs.lc() < 0:
return Gt(-lhs, 0)
return Lt(lhs, 0)
[docs]
def __mul__(self, other: object) -> Term:
if isinstance(other, Term):
return Term(self.poly * other.poly)
if isinstance(other, mpq):
return Term(self.poly * Rational(other))
return Term(self.poly * other)
[docs]
def __ne__( # type: ignore[override]
self, other: Term | int | mpq) -> Ne:
lhs = self - other
if lhs.lc() < 0:
lhs = -lhs
return Ne(lhs, Term(0))
[docs]
def __neg__(self) -> Term:
return Term(-self.poly)
[docs]
def __pow__(self, other: object) -> Term:
return Term(self.poly ** other)
def __repr__(self) -> str:
return str(self.poly)
[docs]
def __radd__(self, other: object) -> Term:
assert not isinstance(object, Term)
if isinstance(other, mpq):
return Term(Rational(other) + self.poly)
return Term(other + self.poly)
[docs]
def __rmul__(self, other: object) -> Term:
assert not isinstance(object, Term)
if isinstance(other, mpq):
return Term(Rational(other) * self.poly)
return Term(other * self.poly)
[docs]
def __rsub__(self, other: object) -> Term:
assert not isinstance(object, Term)
if isinstance(other, mpq):
return Term(Rational(other) - self.poly)
return Term(other - self.poly)
[docs]
def __sub__(self, other: object) -> Term:
if isinstance(other, Term):
return Term(self.poly - other.poly)
if isinstance(other, mpq):
return Term(self.poly - Rational(other))
return Term(self.poly - other)
[docs]
def __truediv__(self, other: object) -> Term:
if isinstance(other, mpq):
return Term(self.poly / Rational(other))
if isinstance(other, Term):
return Term(self.poly / other.poly)
# x*y / x would yield y as a Sage rational function and raise and
# exception.
return Term(self.poly / other)
def __xor__(self, other: object) -> Term:
raise NotImplementedError(
"Use ** for exponentiation, not '^', which means xor "
"in Python, and has the wrong precedence")
def as_fraction(self) -> mpq:
if not self.is_constant():
raise ValueError(f'{self} is not constant')
return self.constant_coefficient()
[docs]
def as_latex(self) -> str:
"""LaTeX representation as a string. Implements the abstract method
:meth:`.firstorder.atomic.Term.as_latex`.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.as_latex()
'x^{2} - 2 x y + y^{2} + 4 x - 4 y + 4'
"""
return str(sage_latex(self.poly))
def as_variable(self) -> Variable:
if not self.is_variable():
raise ValueError(f'{self} is not a variable')
return Variable(self.poly)
[docs]
def coefficient(self, degrees: dict[Variable, int]) -> Term:
"""Return the coefficient of the variables with the degrees specified
in the python dictionary `degrees`.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.coefficient({x: 1, y: 1})
-2
>>> t.coefficient({x: 1})
-2*y + 4
.. seealso::
:external:meth:`MPolynomial_libsingular.coefficient()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.coefficient>`
"""
d_poly = {key.poly: value for key, value in degrees.items()}
return Term(self.poly.coefficient(d_poly))
[docs]
def constant_coefficient(self) -> mpq:
"""Return the constant coefficient of this term.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.constant_coefficient()
mpq(4,1)
.. seealso::
:external:meth:`MPolynomial_libsingular.constant_coefficient()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.constant_coefficient>`
"""
return mpq(self.poly.constant_coefficient())
[docs]
def content(self) -> mpq:
"""Return the content of this term, which is defined as the gcd of its
integer coefficients.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2 - (x**2 + y**2)
>>> t.content()
mpq(2,1)
.. seealso::
:external:meth:`MPolynomial.content()
<sage.rings.polynomial.multi_polynomial.MPolynomial.content>`
"""
content = self.poly.content()
assert content > 0 or (content == 0 and self == 0)
return mpq(content)
[docs]
def degree(self, x: Variable) -> int:
"""Return the degree in `x` of this term.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.degree(y)
2
.. seealso::
:external:meth:`MPolynomial_libsingular.degree()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.degree>`
"""
return self.poly.degree(x.poly)
[docs]
def derivative(self, x: Variable, n: int = 1) -> Term:
"""The `n`-th derivative of this term, with respect to `x`.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.derivative(x)
2*x - 2*y + 4
.. seealso::
:external:meth:`MPolynomial.derivative()
<sage.rings.polynomial.multi_polynomial.MPolynomial.derivative>`
"""
return Term(self.poly.derivative(self.polynomial_ring(x.poly), n))
[docs]
@lru_cache(maxsize=CACHE_SIZE)
def factor(self) -> tuple[mpq, dict[Term, int]]:
"""A polynomial factorization of this term.
:returns: A pair `(unit, D)`, where `unit` is a rational number, the
keys of `D` are irreducible factors, and the corresponding values are
their multiplicities. All irreducible factors are monic. Note that
the return value is uniquely determined by this specification.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = -x**2 + y**2
>>> t.factor()
(mpq(-1,1), {x - y: 1, x + y: 1})
.. seealso::
:external:meth:`MPolynomial_libsingular.factor()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.factor>`
"""
F = self.poly.factor()
assert F.unit().is_constant()
unit = mpq(F.unit().constant_coefficient())
D = dict()
for poly, multiplicity in F:
assert not poly.is_constant()
lc = poly.lc()
poly /= lc
unit *= mpq(lc)
D[Term(poly)] = multiplicity
return unit, D
[docs]
def is_constant(self) -> bool:
"""Return :obj:`True` if this term is constant.
.. seealso::
:external:meth:`MPolynomial_libsingular.is_constant()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.is_constant>`
"""
return self.poly.is_constant()
[docs]
def is_definite(self) -> DEFINITE:
"""A fast heuristic test for definitetess properties of this term. This
is based on *trivial square sum* properties of coefficient signs and
exponents.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> Term(0).is_definite()
<DEFINITE.ZERO: 6>
>>> f = x**2 + y**2
>>> f.is_definite()
<DEFINITE.POSITIVE_SEMI: 5>
>>> g = -x**2 - y**2 - 1
>>> g.is_definite()
<DEFINITE.NEGATIVE: 1>
>>> h = (x + y) ** 2
>>> h.is_definite()
<DEFINITE.NONE: 3>
"""
if self.is_zero():
return DEFINITE.ZERO
ls = sign(self.lc())
for exponent, coefficient in self.poly.dict().items():
if coefficient.sign() != ls:
return DEFINITE.NONE
for e in exponent:
if e % 2 == 1:
return DEFINITE.NONE
if self.poly.constant_coefficient() == 0:
return DEFINITE.POSITIVE_SEMI if ls == 1 else DEFINITE.NEGATIVE_SEMI
return DEFINITE.POSITIVE if ls == 1 else DEFINITE.NEGATIVE
def is_monomial(self) -> bool:
"""Return :obj:`True` if this term is a monomial.
"""
return self.poly.is_monomial()
def is_variable(self) -> bool:
"""Return :obj:`True` if this term is a variable.
"""
return self.poly.is_generator()
[docs]
def is_zero(self) -> bool:
"""Return :obj:`True` if this term is a zero.
.. seealso::
:external:meth:`MPolynomial_libsingular.is_zero()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.is_zero>`
"""
return self.poly.is_zero()
[docs]
def lc(self) -> mpq:
"""Leading coefficient of this term with respect to the degree
lexicographical term order :mod:`deglex
<sage.rings.polynomial.term_order>`.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> f = 2*x*y**2 + 3*x**2 + 1
>>> f.lc()
mpq(2,1)
.. seealso::
:external:meth:`MPolynomial_libsingular.lc()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.lc>`
"""
return mpq(self.poly.lc())
def monomial_coefficient(self, mon: Term) -> mpq:
"""Return the coefficient in the base ring of the monomial mon in self,
where mon must have the same parent as self.
.. seealso::
:external:meth:`MPolynomial_libsingular.monomial_coefficient()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.monomial_coefficient>`
"""
if not mon.is_monomial():
raise ValueError(f'{mon} is not a monomial')
return mpq(self.poly.monomial_coefficient(mon.poly))
[docs]
def monomials(self) -> list[Term]:
"""List of monomials of this term. A monomial is defined here as a
summand of a polynomial *without* the coefficient.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> t = (x - y + 2) ** 2
>>> t.monomials()
[x^2, x*y, y^2, x, y, 1]
.. seealso::
:external:meth:`MPolynomial_libsingular.monomials()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.monomials>`
"""
return [Term(monomial) for monomial in self.poly.monomials()]
def normalize(self) -> Term:
return Term(self.poly / self.poly.lc())
[docs]
def pseudo_quo_rem(self, other: Term, x: Variable) -> tuple[Term, Term]:
"""Pseudo quotient and remainder of this term and other, both as
univariate polynomials in `x` with polynomial coefficients in all other
variables.
>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> f = a * x**2 + b*x + c
>>> g = c * x + b
>>> q, r = f.pseudo_quo_rem(g, x); q, r
(a*c*x - a*b + b*c, a*b^2 - b^2*c + c^3)
>>> assert c**(2 - 1 + 1) * f == q * g + r
.. seealso::
:meth:`Polynomial.pseudo_quo_rem()
<sage.rings.polynomial.polynomial_element.Polynomial.pseudo_quo_rem>`
"""
self1 = self.poly.polynomial(self.polynomial_ring(x.poly))
other1 = other.poly.polynomial(self.polynomial_ring(x.poly))
quotient, remainder = self1.pseudo_quo_rem(other1)
return Term(quotient), Term(remainder)
def reduce(self, G: Iterable[Term]) -> Term:
"""Reduce self modulo G.
"""
# Sage requires that g.poly can be coerced to self.poly.parent().
poly = self.polynomial_ring(self.poly).reduce([g.poly for g in G])
return Term(poly)
[docs]
def quo_rem(self, other: Term) -> tuple[Term, Term]:
"""Quotient and remainder of this term and `other`.
>>> from logic1.theories.RCF import VV
>>> x, y = VV.get('x', 'y')
>>> f = 2*y*x**2 + x + 1
>>> f.quo_rem(x)
(2*x*y + 1, 1)
>>> f.quo_rem(y)
(2*x^2, x + 1)
>>> f.quo_rem(3*x) # would yield (0, 2*x^2*y + x + 1) over ZZ
(2/3*x*y + 1/3, 1)
.. seealso::
:external:meth:`MPolynomial_libsingular.quo_rem()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.quo_rem>`
"""
quo, rem = self.poly.quo_rem(other.poly)
return Term(quo), Term(rem)
[docs]
def sort_key(self) -> SortKey[Self]:
"""A sort key suitable for ordering instances of this class. ImplementTerm(remainder)s
the abstract method :meth:`.firstorder.atomic.Term.sort_key`.
"""
return SortKey(self)
[docs]
def subs(self, d: Mapping[Variable, Term | int | mpq]) -> Term:
"""Simultaneous substitution of terms for variables.
>>> from logic1.theories.RCF import VV
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = 2*y*x**2 + x + 1
>>> f.subs({x: y, y: 2*z})
4*y^2*z + y + 1
.. seealso::
:external:meth:`MPolynomial_libsingular.subs()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.subs>`
"""
sage_keywords: dict[str, MPolynomial[Rational] | int | mpq] = dict()
for variable, substitute in d.items():
match substitute:
case Term():
sage_keywords[str(variable.poly)] = substitute.poly
case int() | mpq():
sage_keywords[str(variable.poly)] = substitute
case _:
assert False, (self, d)
return Term(self.polynomial_ring(self.poly).subs(**sage_keywords))
[docs]
def vars(self) -> Iterator[Variable]:
"""An iterator that yields each variable of this term once. Implements
the abstract method :meth:`.firstorder.atomic.Term.vars`.
.. seealso::
:external:meth:`MPolynomial_libsingular.variables()
<sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.variables>`
"""
for g in self.poly.variables():
yield Variable(g)
# discuss: Variable inherits __init__, and we can create Variable(3), Variable(term.poly), etc.
[docs]
class Variable(Term, firstorder.Variable['Variable', int, SortKey['Variable']]):
VV: ClassVar[VariableSet] = VV
[docs]
def fresh(self) -> Variable:
"""Returns a variable that has not been used so far. Implements
abstract method :meth:`.firstorder.atomic.Variable.fresh`.
"""
return self.VV.fresh(suffix=f'_{str(self)}')
[docs]
class Eq(AtomicFormula):
pass
[docs]
class Ne(AtomicFormula):
pass
[docs]
class Ge(AtomicFormula):
pass
[docs]
class Le(AtomicFormula):
pass
[docs]
class Gt(AtomicFormula):
pass
[docs]
class Lt(AtomicFormula):
pass
from .typing import Formula