Simplification

Abstract Base Classes

Simplification#

Attention

This documentation page addresses implementers rather than users. Concrete implemtations of the abstract classes described here are documented in the corresponding sections of the various domains:

This module logic1.abc.simplify provides a generic abstract implementation of deep simplifcication based on generating and propagating internal representations during recursion. This is essentially the standard simplifier, which has been proposed for Ordered Fields in [DolzmannSturm-1997].

Generic Types#

We use type variables simplify.α, simplify.τ, simplify.χ, simplify.σ in anology to their counterparts in formula.

logic1.abc.simplify.α = TypeVar('α', bound='AtomicFormula')#
logic1.abc.simplify.τ = TypeVar('τ', bound='Term')#
logic1.abc.simplify.χ = TypeVar('χ', bound='Variable')#
logic1.abc.simplify.σ = TypeVar('σ')#

Additionally, we introduce a type variable ρ for internal representations and a type variable ω for options used by the simplifier.

logic1.abc.simplify.ρ = TypeVar('ρ', bound='InternalRepresentation')#

A type variable denoting a type of variables with upper bound logic1.abc.simplify.InternalRepresentation.

logic1.abc.simplify.ω = TypeVar('ω', bound='Options')#

A type variable denoting a options for Simplify.simplify() with upper bound Options.

Internal Representations#

class logic1.abc.simplify.RESTART[source]#

Bases: Enum

Used for the return value of InternalRepresentation.add().

NONE = 1#

No formulas of the current level require resimplification.

OTHERS = 2#

Non-atoms of the current level require resimplification.

ALL = 3#

All formulas of the current level require resimplification.

class logic1.abc.simplify.InternalRepresentation[source]#

Bases: Generic[α, τ, χ, σ]

This abstract class serves as an upper bound for the type variable ρ in abc.simplify.Simplify. It specifies an interface comprising methods required there.

The principal idea is that a InternalRepresentation should holds information that corresponds to a conjunction of atomic formulas. In the course of recursive simplification in abc.simplify.Simplify, instances of this class are inherited from higher levels and are enriched with information from all atomic formulas on the toplevel of the subformula currently under consideration.

exception Inconsistent[source]#

Bases: Exception

Indicates that an instance of InternalRepresentation contains inconsistent information. This exception is typically handled in abc.simplify.Simplify and its derived classes, where appropriate values are returned.

abstractmethod add(gand: type[And[α, τ, χ, σ] | Or[α, τ, χ, σ]], atoms: Iterable[α]) → RESTART[source]#

Add information originating from atoms. If gand is And, consider atoms. If gand is Or, consider (Not(at) for at in atoms). Simplification among atoms is supposed to take place here.

abstractmethod extract(gand: type[And[α, τ, χ, σ] | Or[α, τ, χ, σ]], ref: Self) → Iterable[α][source]#

Comapare self and ref to identify and extract information that must be represented on the toplevel of the subformula currently under consideration. If gand is And, the result represents a conjunction. If gand is Or, it represents a disjunction.

abstractmethod next_(remove: χ | None = None) → Self[source]#

Create a copy of self, optionally removing all information involving the variable remove.

restart(ir: Self) → Self[source]#

Return a new internal representation for the current level during simplifiation after RESTART.ALL has been returned by InternalRepresentation.add(). In this case, ir is the internal representation of the current level, and self is the internal representation of the previous level.

Raise a NotImplementedError by default.

transform_atom(atom: α) → α[source]#

Return an atomic formula that is equivalent to atom modulo the information contained in self.

Return atom by default.

Simplification and Validity#

class logic1.abc.simplify.Options[source]#

Bases: ABC

This class holds options that can be provided to Simplify.simplify(). Theories subclassing Simplify can add further options by subclassing Options.

This is an upper bound for the type variable ω.

class logic1.abc.simplify.Simplify[source]#

Bases: Generic[α, τ, χ, σ, ρ, ω]

Deep simplification following [DolzmannSturm-1997].

See also

Derived classes in various theories: RCF.simplify.Simplify, Sets.simplify.Simplify, Complex.simplify.Simplify

abstractmethod create_initial_representation(assume: Iterable[α]) → ρ[source]#

Create a fresh instance of ρ.

is_valid(f: Formula[α, τ, χ, σ], assume: Iterable[α] = []) → bool | None[source]#

Simplification-based heuristic test for vailidity of a formula.

Mathematical definition

A first-order formula is valid if it holds for all values all free variables.

Parameters:

  • f – The formula to be tested for validity

  • assume – A list of atomic formulas that are assumed to hold. The result of the validity test is correct modulo these assumptions.

Returns:

Returns True or False if abc.simplify.Simplify.simplify() succeeds in heuristically simplifying f to T or F, respectively. Returns None in the sense of “don’t know” otherwise.

abstractmethod simpl_at(atom: α, context: type[And[α, τ, χ, σ]] | type[Or[α, τ, χ, σ]] | None) → Formula[α, τ, χ, σ][source]#

Simplify the atomic formula atom. The context tells whether atom occurs within a conjunction or a disjunction. This can be taken into consideration for the inclusion of certain simplification strategies. For instance, simplification of xy == 0 to Or(x == 0, y == 0) over the reals could be desirable within a disjunction but not otherwise.

simplify(f: Formula[α, τ, χ, σ], assume: Iterable[α] = []) → Formula[α, τ, χ, σ][source]#

Simplify f modulo assume.

Parameters:

  • f – The formula to be simplified

  • assume – A list of atomic formulas that are assumed to hold. The simplification result is equivalent modulo those assumptions.

Returns:

A simplified equivalent of f modulo assume.