Sets with Cardinality Constraints

Simplification

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.

logic1.theories.Sets.simplify.simplify(f: Formula, assume: Iterable[AtomicFormula] = []) → Formula

This is the primary simplification function for f modulo assume.

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> a, b, c, d = VV.get('a', 'b', 'c', 'd')
>>> simplify(And(a == b, b == c, c == d,  d == c), assume=[a == b])
And(a == c, a == d)

Assumptions do not affect bound variables.

>>> simplify(And(a == c, Ex(a, a == b)), assume=[a == b])
And(a == c, Ex(a, a == b))

See also

Simplify

Its inherited method Simplify.simplify() is wrapped by this function.

logic1.theories.Sets.simplify.is_valid(f: Formula, assume: Iterable[AtomicFormula] = []) → bool | None

Simplification-based heuristic test for validity and unsatisfiability of a formula.

Mathematical definition

A formula is valid if it is true for all values of its free variables. A formula is unsatisfiable if it is false for all values of its free variables.

This function provides an efficient heuristic test whether f is valid or unsatisfiable modulo assume:

• If the simplifier yields T, then f is valid and True is returned.

• If the simplifier yields F, then f is unsatisfiable and False is returned.

Otherwise, None is returned, which means “don’t know”.

Some examples

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> a, b, c, d = VV.get('a', 'b', 'c', 'd')

Valid:

>>> is_valid(a == d, assume=[a == b, b == c, c == d])
True

Unsatisfiable:

>>> is_valid(a == d, assume=[a == b, b != c, c == d])
False

Neither valid nor unsatisfiable:

>>> is_valid(a == d, assume=[a != b, b != c, c != d])

See also

Simplify

Its inherited method Simplify.is_valid() is wrapped by this function.

Details

Attention

The material below addresses implementers rather than users.

class logic1.theories.Sets.simplify.Simplify

Bases: Simplify[AtomicFormula, Variable, Variable, Never, InternalRepresentation, Options]

Deep simplification in the style of [DolzmannSturm-1997]. Implements the abstract methods create_initial_representation and simpl_at of its super class abc.simplify.Simplify.

The simplifier should be called via simplify(), as described below. In addition, this class inherits abc.simplify.Simplify.is_valid(), which should be called via is_valid(), as described below.

class logic1.theories.Sets.simplify.InternalRepresentation

Bases: InternalRepresentation[AtomicFormula, Variable, Variable, Never]

Implements the abstract methods add(), extract(), and next_() of it super class abc.simplify.InternalRepresentation. Required by Sets.simplify.Simplify for instantiating the type variable abc.simplify.ρ of abc.simplify.Simplify.