Sets

Quantifier Elimination

Assumptions

class logic1.theories.Sets.qe.Assumptions

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

Implements the abstract method simplify() of its super class abc.qe.Assumptions. Required by Node and QuantifierElimination for instantiating the type variable abc.qe.λ of abc.qe.Node and abc.qe.QuantifierElimination, respectively.

Nodes

class logic1.theories.Sets.qe.Node

Bases: Node[Formula[AtomicFormula, Variable, Variable, Never], Variable, Assumptions]

Implements the abstract methods copy() and process() of its super class abc.qe.Node. Required by QuantifierElimination for instantiating the type variable abc.qe.ν of abc.qe.QuantifierElimination.

Quantifier Elimination

class logic1.theories.Sets.qe.QuantifierElimination

Bases: QuantifierElimination[Node, Assumptions, None, Options, AtomicFormula, Variable, Variable, Never]

Quantifier elimination for the theory of sets with cardinality constraints.

Implements the abstract methods create_options(), create_root_nodes(), create_assumptions(), create_true_node(), final_simplify(), init_env(), init_env_arg() of its super class abc.qe.QuantifierElimination.

User Interface

logic1.theories.Sets.qe.qe(f: Formula[α, τ, χ, σ], assume: Iterable[α] = [], workers: int = 0, **options) → Formula[α, τ, χ, σ] | None

Quantifier elimination for the theory of sets with cardinanity constraints. Technically, qe() is an instance of the callable class QuantifierElimination.

Parameters:

• f – The input formula to which quantifier elimination will be applied.

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

• workers –

  Specifies the number of processes to be used in parallel:

  • The default value workers=0 uses a sequential implementation, which avoids overhead when input problems are small. For all other values, there are additional processes started.

  • A positive value workers=n > 0 uses n + 2 processes: the master process, n worker processes, and a proxy processes that manages shared data.

    Note

    workers=1 uses the parallel implementation with only one worker. Algorithmically this is similar to the sequential version with workers=0 but comes at the cost of 2 additional processes.

  • A negative value workers=-n < 0 specifies os.num_cpu() - n many workers. It follows that workers=-2 exactly allocates all of CPUs of the machine, and workers=-3 is an interesting choice, which leaves one CPU free for smooth interaction with the machine.

• **options – Keyword arguments with keywords corresponding to attributes of abc.qe.Options. Those are log_level, log_rate.

Returns:

A quantifier-free equivalent of f modulo the assumptions that are passed as the assume parameter.

Some examples

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> a, u, v, w, x, y, z = VV.get('a', 'u', 'v', 'w', 'x', 'y', 'z')

For the following input formula to hold, there must be at least two different elements in the universe. We derive this information via quantifier elimination:

>>> qe(Ex([x, y], x != y))
C(2)

See also

The documentation of C and C_.

In the next example, we learn that there must be at most one element in the universe:

>>> qe(All(u, Ex(w, All(x, Ex([y, v],
...   And(Or(u == v, v != w), ~ Equivalent(u == x, u != w), y == a))))))
C_(2)

In the next example, the cardinality of the universe must be exactly three:

>>> qe(Ex([x, y, z],
...   And(x != y, x != z, y != z, All(u, Or(u == x, u == y, u == z)))))
And(C(3), C_(4))

In our final example, the cardinality of the universe must be exactly one or at least 4:

>>> qe(Implies(Ex([w, x], w != x),
...            Ex([w, x, y, z],
...              And(w != x, w != y, w != z, x != y, x != z, y != z))))
Or(C_(2), C(4))