Source code for logic1.theories.RCF.simplify

"""This module provides an implementation of *deep simplifcication* based on
generating and propagating internal representations during recursion in Real
Closed fields. This is essentially the *standard simplifier*, which has been
proposed for Ordered Fields in [DolzmannSturm-1997]_.
"""

from dataclasses import dataclass, field
from functools import lru_cache
from operator import xor
from sage.all import oo, product, Rational  # type: ignore
from sage.rings.infinity import MinusInfinity, PlusInfinity  # type: ignore
from typing import Final, Iterable, Optional, Self, TypeAlias

from ... import abc

from ...firstorder import And, _F, Not, Or, _T
from .atomic import AtomicFormula, Eq, Ge, Le, Gt, Lt, Ne, Term, TSQ, Variable
from .typing import Formula

from ...support.tracing import trace  # noqa


CACHE_SIZE: Final[Optional[int]] = 2**16


@dataclass
class _Interval:
    # Non-empty real intervals. Raises Inconsistent when an empty interval
    # is created.

    lopen: bool = True
    start: Rational | MinusInfinity = -oo
    end: Rational | PlusInfinity = oo
    ropen: bool = True

    def __contains__(self, q: Rational) -> bool:
        if q < self.start or (self.lopen and q == self.start):
            return False
        if self.end < q or (self.ropen and q == self.end):
            return False
        return True

    def __init__(self, lopen: bool, start: Rational | MinusInfinity,
                 end: Rational | PlusInfinity, ropen: bool) -> None:
        assert lopen or start is not -oo, (lopen, start, end, ropen)
        assert ropen or end is not oo
        if start > end:
            raise InternalRepresentation.Inconsistent()
        if (lopen or ropen) and start == end:
            raise InternalRepresentation.Inconsistent()
        self.lopen = lopen
        self.start = start
        self.end = end
        self.ropen = ropen

    def intersection(self, other: Self) -> Self:
        if self.start < other.start:
            lopen = other.lopen
            start = other.start
        elif other.start < self.start:
            lopen = self.lopen
            start = self.start
        else:
            assert self.start == other.start
            start = self.start
            lopen = self.lopen or other.lopen
        if self.end < other.end:
            end = self.end
            ropen = self.ropen
        elif other.end < self.end:
            end = other.end
            ropen = other.ropen
        else:
            assert self.end == other.end
            end = self.end
            ropen = self.ropen or other.ropen
        return self.__class__(lopen, start, end, ropen)

    def is_point(self) -> bool:
        # It is assumed and has been asserted that the interval is not empty.
        return self.start == self.end

    def __repr__(self):
        left = '(' if self.lopen else '['
        right = ')' if self.ropen else ']'
        return f'{left}{self.start}, {self.end}{right}'


Knowledge: TypeAlias = dict[Term, tuple[_Interval, set[Rational]]]
Substitution: TypeAlias = dict[Variable, Rational]


[docs] @dataclass class InternalRepresentation( abc.simplify.InternalRepresentation[AtomicFormula, Term, Variable, int]): """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`. """ prefer_weak: bool prefer_order: bool _ref_knowl: Knowledge = field(default_factory=dict) _ref_subst: Substitution = field(default_factory=dict) _cur_knowl: Knowledge = field(default_factory=dict) _cur_subst: Substitution = field(default_factory=dict) def add(self, gand: type[And | Or], atoms: Iterable[AtomicFormula]) -> abc.simplify.Restart: """Implements the abstract method :meth:`.abc.simplify.InternalRepresentation.add`. """ if gand is Or: atoms = (atom.to_complement() for atom in atoms) restart = abc.simplify.Restart.NONE for atom in atoms: # print(f'{atom=}') # print(f'{self=}') # print() atom = atom.subsq(self._cur_subst) if atom.lhs.is_constant(): if bool(atom): continue else: raise InternalRepresentation.Inconsistent() # rel is the relation of atom, p is the parametric part, and q is # the negative of the Rational absolute summand. rel, t, q = self._decompose_atom(atom) if t.lc() < 0: rel = rel.converse() t = -t q = -q # We model t in ivl \ exc. if rel is Eq: ivl = _Interval(False, q, q, False) exc = set() elif rel is Ne: ivl = _Interval(True, -oo, oo, True) exc = {q} elif rel is Ge: ivl = _Interval(False, q, oo, True) exc = set() elif rel is Le: ivl = _Interval(True, -oo, q, False) exc = set() elif rel is Gt: ivl = _Interval(True, q, oo, True) exc = set() elif rel is Lt: ivl = _Interval(True, -oo, q, True) exc = set() else: assert False, rel t, ivl, exc = self.prune_item(self._cur_knowl, t, ivl, exc) if self._cur_knowl.get(t) != (ivl, exc): subst_value = self.as_subst_value(gand, t, ivl, exc) if subst_value is not None: self._add_point(gand, t, subst_value) restart = abc.simplify.Restart.ALL else: self._cur_knowl[t] = (ivl, exc) if restart is not abc.simplify.Restart.ALL: restart = abc.simplify.Restart.OTHERS # print(f'{self=}') return restart def _add_point(self, gand: type[And | Or], t: Term, q: Rational) -> None: stack = [(t, q)] while stack: t, q = stack.pop() v = t.as_variable() if v in self._cur_subst: if self._cur_subst[v] != q: raise InternalRepresentation.Inconsistent() else: continue else: self._cur_subst[v] = q cur_knowl: Knowledge = dict() for t, (ivl, exc) in self._cur_knowl.items(): t, ivl, exc = self.fancy_subs(t, ivl, exc, {v: q}) if t.is_constant(): t_as_rational = Rational(t.as_int()) if t_as_rational in ivl and t_as_rational not in exc: continue else: raise InternalRepresentation.Inconsistent() t, ivl, exc = self.prune_item(cur_knowl, t, ivl, exc) subst_value = self.as_subst_value(gand, t, ivl, exc) if subst_value is not None: stack.append((t, subst_value)) else: cur_knowl[t] = (ivl, exc) self._cur_knowl = cur_knowl @staticmethod def as_subst_value(gand, t, ivl, exc) -> Optional[Rational]: if not t.is_variable(): return None if ivl.is_point() and not exc: return ivl.start return None @staticmethod @lru_cache(maxsize=CACHE_SIZE) def _compose_atom(rel: type[AtomicFormula], t: Term, q: Rational) -> AtomicFormula: num = q.numer() den = q.denom() return rel(den * t - num, 0) @staticmethod @lru_cache(maxsize=CACHE_SIZE) def _decompose_atom(f: AtomicFormula)\ -> tuple[type[AtomicFormula], Term, Rational]: r"""Decompose into relation :math:`\rho`, term :math:`p` without absolute summand, and rational :math:`q` such that :data:`f` is equivalent to :math:`p \rho q`. We assume that :data:`f` has gone through :meth:`_simpl_at` so that its right hand side is zero. >>> from .atomic import VV >>> a, b = VV.get('a', 'b') >>> f = 6*a**2 + 12*a*b + 6*b**2 + 3 <= 0 >>> rel, p, q = InternalRepresentation._decompose_atom(f); rel, p, q (<class 'logic1.theories.RCF.atomic.Le'>, a^2 + 2*a*b + b^2, -1/2) >>> g = InternalRepresentation._compose_atom(rel, p, q); g 2*a^2 + 4*a*b + 2*b^2 + 1 <= 0 >>> (f.lhs.poly / g.lhs.poly) 3 """ lhs = f.lhs q = -lhs.constant_coefficient() p = lhs + q c = p.content() p /= c # Given that _simpl_at has produced a primitive polynomial, q != 0 # will not be divisible by c. This is relevant for the reconstruction # in _compose_atom to work. assert c == 1 or not q % c == 0, # f'{c} divides {q}' return f.op, p, Rational((q, c)) def extract(self, gand: type[And | Or]) -> list[AtomicFormula]: """Implements the abstract method :meth:`.abc.simplify.InternalRepresentation.extract`. """ ref_knowl: Knowledge = dict() for t, (ivl, exc) in self._ref_knowl.items(): t, ivl, exc = self.fancy_subs(t, ivl, exc, self._cur_subst) t, ivl, exc = self.prune_item(ref_knowl, t, ivl, exc) ref_knowl[t] = (ivl, exc) # print(f'extract: {self._ref_knowl=}\n' # f' {self._cur_knowl=}\n' # f' {self._cur_subst=}\n' # f' {ref_knowl=}') L: list[AtomicFormula] = [] for t in self._cur_knowl: if t in ref_knowl: ref_ivl, ref_exc = ref_knowl[t] else: ref_ivl, ref_exc = _Interval(True, -oo, oo, True), set() ivl, exc = self._cur_knowl[t] # ivl cannot be empty because the construction of an empty interval # raises an Exception during `add`. if ivl.is_point(): if ref_ivl.is_point(): assert ref_ivl.start == ivl.start # throw away the point ivl \ exc, which is equal to ref_ivl \ ref_exc else: assert ivl.start in ref_ivl and ivl.start not in ref_exc # Pick the one point of ivl. q = ivl.start # When gand is And, the equation q = 0 is generally # preferable. Otherwise, q = 0 would become q != 0 # via subsequent negation, and we want to take # self.prefer_order into consideration. if self.prefer_order and gand is Or: if q == ref_ivl.start: assert not ref_ivl.lopen L.append(self._compose_atom(Le, t, q)) elif q == ref_ivl.end: assert not ref_ivl.ropen L.append(self._compose_atom(Ge, t, q)) else: L.append(self._compose_atom(Eq, t, q)) else: L.append(self._compose_atom(Eq, t, q)) else: # We know that ref_ivl is a proper interval, too, because ivl # is a subset of ref_ivl. # print(f'{t=}, {ref_ivl=}, {ivl=}') assert not ref_ivl.is_point() if ref_ivl.start < ivl.start: if ivl.start in ref_exc: # When gand is Or, weak and strong are dualized via # subsequent negation. if xor(self.prefer_weak, gand is Or): L.append(self._compose_atom(Ge, t, ivl.start)) else: L.append(self._compose_atom(Gt, t, ivl.start)) else: if ivl.lopen: L.append(self._compose_atom(Gt, t, ivl.start)) else: L.append(self._compose_atom(Ge, t, ivl.start)) elif ref_ivl.start == ivl.start: if not ref_ivl.lopen and ivl.lopen: # When gand is Or, Ne will become Eq via subsequent # nagation. This is generally preferable. if self.prefer_order and gand is And: L.append(self._compose_atom(Gt, t, ivl.start)) else: L.append(self._compose_atom(Ne, t, ivl.start)) else: assert False, (self, (t, ivl, exc)) if ivl.end < ref_ivl.end: if ivl.end in ref_exc: # When gand is Or, weak and strong are dualized via # subsequent negation. if xor(self.prefer_weak, gand is Or): L.append(self._compose_atom(Le, t, ivl.end)) else: L.append(self._compose_atom(Lt, t, ivl.end)) else: if ivl.ropen: L.append(self._compose_atom(Lt, t, ivl.end)) else: L.append(self._compose_atom(Le, t, ivl.end)) elif ref_ivl.end == ivl.end: if not ref_ivl.ropen and ivl.ropen: # When gand is Or, Ne will become Eq via subsequent # nagation. This is generally preferable. if self.prefer_order and gand is And: L.append(self._compose_atom(Lt, t, ivl.end)) else: L.append(self._compose_atom(Ne, t, ivl.end)) else: assert False for q in exc: if q not in ref_exc: L.append(self._compose_atom(Ne, t, q)) for v, q in self._cur_subst.items(): if v in self._ref_subst: continue cur_subst = {vv: qq for vv, qq in self._cur_subst.items() if vv != v} ref_knowl = dict() for t, (ivl, exc) in self._ref_knowl.items(): t, ivl, exc = self.fancy_subs(t, ivl, exc, cur_subst) t, ivl, exc = self.prune_item(ref_knowl, t, ivl, exc) ref_knowl[t] = (ivl, exc) if self.prefer_order and gand is Or and v in ref_knowl: ref_ivl, ref_exc = ref_knowl[v] if q == ref_ivl.start: assert not ref_ivl.lopen L.append(self._compose_atom(Le, v, q)) elif q == ref_ivl.end: assert not ref_ivl.ropen L.append(self._compose_atom(Ge, v, q)) else: L.append(self._compose_atom(Eq, v, q)) else: L.append(self._compose_atom(Eq, v, q)) if gand is Or: L = [atom.to_complement() for atom in L] return L @staticmethod def fancy_subs(t: Term, ivl: _Interval, exc: set[Rational], subst: Substitution) \ -> tuple[Term, _Interval, set[Rational]]: c, t = t._subsq_rat(subst) if t.is_constant(): return t, ivl, exc assert c > 0, (c, t) constant_coefficient = t.constant_coefficient() t -= constant_coefficient content = t.content() t /= content c *= content shift = Rational((constant_coefficient, content)) if t.lc() >= 0: ivl = _Interval(ivl.lopen, ivl.start / c - shift, ivl.end / c - shift, ivl.ropen) else: t = -t c = -c shift = -shift ivl = _Interval(ivl.ropen, ivl.end / c - shift, ivl.start / c - shift, ivl.lopen) exc = {point / c - shift for point in exc} return t, ivl, exc def next_(self, remove: Optional[Variable] = None) -> Self: """Implements the abstract method :meth:`.abc.simplify.InternalRepresentation.next_`. """ result = self.__class__(self.prefer_weak, self.prefer_order) if remove is None: result._ref_knowl = self._cur_knowl.copy() result._ref_subst = self._cur_subst.copy() else: result._ref_knowl = {p: q for p, q in self._cur_knowl.items() if remove not in p.vars()} result._ref_subst = {p: q for p, q in self._cur_subst.items() if p != remove} result._cur_knowl = result._ref_knowl.copy() result._cur_subst = result._ref_subst.copy() return result @staticmethod def prune_item(knowl: Knowledge, t: Term, ivl: _Interval, exc: set[Rational]) \ -> tuple[Term, _Interval, set[Rational]]: if t in knowl: cur_ivl, cur_exc = knowl[t] ivl = ivl.intersection(cur_ivl) exc = exc.union(cur_exc) # Restrict exc to the new ivl. exc = {x for x in exc if x in ivl} # Note that exc is a subset of ivl now. Fix the case that ivl # is closed on either side and the corresponding endpoint is in # exc. We are going to use inf and sup in contrast to start and # end, because ivl can be a FiniteSet. if ivl.start in exc: # It follows that ivl is left-closed. _Interval # raises Inconsistent if ivl gets empty. ivl = _Interval(True, ivl.start, ivl.end, ivl.ropen) exc.remove(ivl.start) if ivl.end in exc: # It follows that ivl is right-closed. ivl cannot get emty # here. ivl = _Interval(ivl.lopen, ivl.start, ivl.end, True) exc.remove(ivl.end) return t, ivl, exc
[docs] class Simplify(abc.simplify.Simplify[ AtomicFormula, Term, Variable, int, InternalRepresentation]): """Deep simplification following [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. """ explode_always: bool = True prefer_order: bool = True prefer_weak: bool = False def create_initial_representation(self, assume=Iterable[AtomicFormula]) \ -> InternalRepresentation: """Implements the abstract method :meth:`.abc.simplify.Simplify.create_initial_representation`. """ ir = InternalRepresentation(prefer_weak=self.prefer_weak, prefer_order=self.prefer_order) for atom in assume: simplified_atom = self._simpl_at(atom, And, explode_always=False) match simplified_atom: case AtomicFormula(): ir.add(And, [simplified_atom]) case And(args=args): assert all(isinstance(arg, AtomicFormula) for arg in args) ir.add(And, args) case _T(): continue case _F(): raise InternalRepresentation.Inconsistent() case _: assert False, simplified_atom return ir def simplify(self, f: Formula, assume: Iterable[AtomicFormula] = [], explode_always: bool = True, prefer_order: bool = True, prefer_weak: bool = False) -> Formula: r"""Simplify `f` modulo `assume`. :param f: The formula to be simplified :param assume: A list of atomic formulas that are assumed to hold. The simplification result is equivalent modulo those assumptions. Note that assumptions do not affect bound variables. >>> from logic1.firstorder import * >>> from logic1.theories.RCF import * >>> a, b = VV.get('a', 'b') >>> simplify(Ex(a, And(a > 5, b > 10)), assume=[a > 10, b > 20]) Ex(a, a - 5 > 0) :param explode_always: Simplification can split certain atomic formulas built from products or square sums: .. admonition:: Example 1. 1. :math:`ab = 0` is equivalent to :math:`a = 0 \lor b = 0` 2. :math:`a^2 + b^2 \neq 0` is equivalent to :math:`a \neq 0 \lor b \neq 0`; 2. 1. :math:`ab \neq 0` is equivalent to :math:`a \neq 0 \land b \neq 0` 2. :math:`a^2 + b^2 = 0` is equivalent to :math:`a = 0 \land b = 0`. If `explode_always` is :data:`False`, the splittings in "1." are only applied within disjunctions and the ones in "2." are only applied within conjunctions. This keeps terms more complex but the boolean structure simpler. >>> from logic1.firstorder import * >>> from logic1.theories.RCF import * >>> a, b, c = VV.get('a', 'b', 'c') >>> simplify(And(a * b == 0, c == 0)) And(c == 0, Or(b == 0, a == 0)) >>> simplify(And(a * b == 0, c == 0), explode_always=False) And(c == 0, a*b == 0) >>> simplify(Or(a * b == 0, c == 0), explode_always=False) Or(c == 0, b == 0, a == 0) :param prefer_order: One can sometimes equivalently choose between order inequalities and (in)equations. .. admonition:: Example 1. :math:`a > 0 \lor (b = 0 \land a < 0)` is equivalent to :math:`a > 0 \lor (b = 0 \land a \neq 0)` 2. :math:`a \geq 0 \land (b = 0 \lor a > 0)` is equivalent to :math:`a \geq 0 \land (b = 0 \lor a \neq 0)` By default, the left hand sides in the Example are preferred. If `prefer_order` is :data:`False`, then the right hand sides are preferred. >>> from logic1.firstorder import * >>> from logic1.theories.RCF import * >>> a, b = VV.get('a', 'b') >>> simplify(And(a >= 0, Or(b == 0, a > 0))) And(a >= 0, Or(b == 0, a > 0)) >>> simplify(And(a >= 0, Or(b == 0, a != 0))) And(a >= 0, Or(b == 0, a > 0)) >>> simplify(And(a >= 0, Or(b == 0, a > 0)), prefer_order=False) And(a >= 0, Or(b == 0, a != 0)) >>> simplify(And(a >= 0, Or(b == 0, a != 0)), prefer_order=False) And(a >= 0, Or(b == 0, a != 0)) :param prefer_weak: One can sometimes equivalently choose between strict and weak inequalities. .. admonition:: Example 1. :math:`a = 0 \lor (b = 0 \land a \geq 0)` is equivalent to :math:`a = 0 \lor (b = 0 \land a > 0)` 2. :math:`a \neq 0 \land (b = 0 \lor a \geq 0)` is equivalent to :math:`a \neq 0 \land (b = 0 \lor a > 0)` By default, the right hand sides in the Example are preferred. If `prefer_weak` is :data:`True`, then the left hand sides are preferred. >>> from logic1.firstorder import * >>> from logic1.theories.RCF import * >>> a, b = VV.get('a', 'b') >>> simplify(And(a != 0, Or(b == 0, a >= 0))) And(a != 0, Or(b == 0, a > 0)) >>> simplify(And(a != 0, Or(b == 0, a > 0))) And(a != 0, Or(b == 0, a > 0)) >>> simplify(And(a != 0, Or(b == 0, a >= 0)), prefer_weak=True) And(a != 0, Or(b == 0, a >= 0)) >>> simplify(And(a != 0, Or(b == 0, a > 0)), prefer_weak=True) And(a != 0, Or(b == 0, a >= 0)) :returns: A simplified equivalent of `f` modulo `assume`. """ self.explode_always = explode_always self.prefer_order = prefer_order self.prefer_weak = prefer_weak return super().simplify(f, assume) def simpl_at(self, atom: AtomicFormula, context: Optional[type[And] | type[Or]]) -> Formula: """Implements the abstract method :meth:`.abc.simplify.Simplify.simpl_at`. """ # MyPy does not recognize that And[Any, Any, Any] is an instance of # Hashable. https://github.com/python/mypy/issues/11470 return self._simpl_at(atom, context, self.explode_always) # type: ignore[arg-type] @lru_cache(maxsize=CACHE_SIZE) def _simpl_at(self, atom: AtomicFormula, context: Optional[type[And] | type[Or]], explode_always: bool) -> Formula: """Simplify atomic formula. >>> from .atomic import VV >>> a, b = VV.get('a', 'b') >>> simplify(-6 * (a+b)**2 + 3 <= 0) 2*a^2 + 4*a*b + 2*b^2 - 1 >= 0 """ def _simpl_at_eq_ne(rel, lhs, context): def split_tsq(term): args = [] for _, power_product in term: if explode_always: args.append(fac_junctor(*(rel(v, 0) for v in power_product.vars()))) else: args.append(rel(product(power_product.vars()), 0)) return tsq_junctor(*args) if rel is Eq: tsq_junctor = And fac_junctor = Or else: assert rel is Ne tsq_junctor = Or fac_junctor = And tsq = lhs.is_definite() if tsq == TSQ.STRICT: return tsq_junctor.definite_element() unit, _, factors = lhs.factor() primitive_lhs = Term(1) for factor in factors: # Square-free part primitive_lhs *= factor primitive_tsq = primitive_lhs.is_definite() if primitive_tsq == TSQ.STRICT: return tsq_junctor.definite_element() if primitive_tsq == TSQ.WEAK and (explode_always or context == tsq_junctor): return split_tsq(primitive_lhs) if tsq == TSQ.WEAK and (explode_always or context == tsq_junctor): return split_tsq(lhs) if explode_always or context == fac_junctor: args = (rel(factor, 0) for factor in factors if not factor.is_constant()) return fac_junctor(*args) return rel(primitive_lhs, 0) def tsq_test_ge(f: Term, context: Optional[type[And | Or]]) -> Optional[Formula]: if f.is_definite() in (TSQ.STRICT, TSQ.WEAK): return _T() neg_tsq = (-f).is_definite() if neg_tsq == TSQ.STRICT: return _F() if neg_tsq == TSQ.WEAK: return _simpl_at_eq_ne(Eq, f, context) return None def _simpl_at_ge(lhs, context): # TSQ tests on original left hand side hit = tsq_test_ge(lhs, context) if hit is not None: return hit # Factorize unit, _, factors = lhs.factor() even_factors = [] odd_factor = unit for factor, multiplicity in factors.items(): if factor.is_definite() is TSQ.STRICT: continue if multiplicity % 2 == 0: even_factors.append(factor) else: odd_factor *= factor even_factor = product(even_factors) signed_remaining_squarefree_part = odd_factor * even_factor # TSQ tests on factorization if odd_factor.is_definite() in (TSQ.STRICT, TSQ.WEAK): return _T() neg_tsq = (-odd_factor).is_definite() if neg_tsq == TSQ.STRICT: return _simpl_at_eq_ne(Eq, even_factor, context) if neg_tsq == TSQ.WEAK: return _simpl_at_eq_ne(Eq, signed_remaining_squarefree_part, context) hit = tsq_test_ge(signed_remaining_squarefree_part, context) if hit is not None: return hit # TSQ tests have failed if unit < 0: rel = Le odd_factor = - odd_factor else: rel = Ge if context is Or or explode_always: odd_part = rel(odd_factor, 0) even_part = (Eq(f, 0) for f in even_factors) return Or(odd_part, *even_part) return rel(odd_factor * even_factor ** 2, 0) lhs = atom.lhs - atom.rhs if lhs.is_constant(): # In the following if-condition, the __bool__ method of atom.op # will be called. return _T() if atom.op(lhs, 0) else _F() lhs /= lhs.content() match atom: case Eq(): return _simpl_at_eq_ne(Eq, lhs, context) case Ne(): return _simpl_at_eq_ne(Ne, lhs, context) case Ge(): return _simpl_at_ge(lhs, context) case Le(): return _simpl_at_ge(-lhs, context) case Gt(): if context is not None: context = context.dual() return Not(_simpl_at_ge(-lhs, context)).to_nnf() case Lt(): if context is not None: context = context.dual() return Not(_simpl_at_ge(lhs, context)).to_nnf() case _: assert False def transform_atom(self, atom: AtomicFormula, ir: InternalRepresentation) -> AtomicFormula: substitution = ir._cur_subst atom = atom.subsq(substitution) assert atom.rhs == 0 if atom.lhs.is_constant(): return Eq(0, 0) if bool(atom) else Eq(1, 0) if atom.lhs.lc() < 0: atom = atom.op.converse()(-atom.lhs, 0) return atom
simplify = Simplify().simplify is_valid = Simplify().is_valid