Abstract Base Classes

Quantifier Elimination

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:

• Quantifier elimination in Real Closed Fields

• Quantifier elimination in Complex

• Quantifier elimination in Sets

This module logic1.abc.qe provides generic classes for effective quantifier elimination, which can used by various theories via subclassing.

Generic Types

We use type variables qe.α, qe.τ, qe.χ, qe.σ in anology to their counterparts in the module logic1.firstorder.formula.

logic1.abc.qe.α = TypeVar('α', bound='AtomicFormula')

logic1.abc.qe.τ = TypeVar('τ', bound='Term')

logic1.abc.qe.χ = TypeVar('χ', bound='Variable')

logic1.abc.qe.σ = TypeVar('σ')

We introduce the following additional type variables.

logic1.abc.qe.ν = TypeVar('ν', bound='Node')

A type variable denoting a node with upper bound Node.

logic1.abc.qe.ι = TypeVar('ι')

A type variable denoting the type of the principal argument of the abstract method QuantifierElimination.init_env().

logic1.abc.qe.λ = TypeVar('λ', bound='Assumptions')

A type variable denoting a assumptions with upper bound Assumptions.

logic1.abc.qe.μ = TypeVar('μ', bound='Hashable')

A type variable denoting the information stored in the Memory attribute of NodeList and its subclasses.

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

A type variable denoting a options for QuantifierElimination.__call__() with upper bound Options.

Assumptions

class logic1.abc.qe.Assumptions

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

Holds the currently valid assumptions. This starts with user assumptions explicitly provided by the user. Certain variants of quantified elimination may add further assumptions in the course of the elimination.

See also

• The argument assume of QuantifierElimination.__call__().

• Generic quantifier elimination in RCF.qe.

This is an upper bound for the type variable λ.

exception Inconsistent

Bases: Exception

Raised when the assumptions made become inconsistent.

atoms: list[α]

A list of atoms holding the current set of assumptions.

append(new_atom: α) → None

Add new_atom as another assumption and simplify.

extend(new_atoms: Iterable[α]) → None

Add new_atoms as further assumptions and simplify.

abstractmethod simplify(f: Formula[α, τ, χ, σ]) → Formula[α, τ, χ, σ]

f is a (possibly unary or trivial) conjunction of atoms. Simplifes f in such a way that the result is again a (possibly unary or trivial) conjunction of atoms. Raises Inconsistent if f is simplified to F.

Nodes

class logic1.abc.qe.Node

Bases: Generic[α, τ, χ, σ, λ, μ], ABC

Holds a subproblem for existential quantifier elimination. Theories implementing the interface can put restrictions on the existing fields and add further fields.

variables: list[χ]

A list of variables.

formula: Formula[α, τ, χ, σ]

A quantifier-free formula.

abstractmethod copy() → Self

Create a copy of this node.

abstractmethod memorize() → μ

Return a hashable object that identifies this node. This is used to avoid processing the same node twice.

abstractmethod process(assumptions: λ) → Sequence[Self]

This node describes a formula Ex(node.variables, node.formula). Select a variable from node.variables and compute a list S of successor nodes such that:

1. variable is not in successor.variables for successor in S;

2. variable does not occur in successor.formula for successor in S;

3. Or(*(Ex(successor.variables, successor.formula) for s in S)) is logically equivalent to Ex(node.variables, node.formula).

Options

class logic1.abc.qe.Options

Bases: object

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

This is an upper bound for the type variable ω.

log_level: int

The logging level of the logger used

log_rate: float

The minimal timespan (in s) between log outputs when reporting progress

workers: int

Controls the number of CPUs used for processing subproblems:

• With the default value workers=0, the implementation runs sequentially. For all other values, additional processes are started.

• A positive value workers=n uses n + 2 CPUs: n for worker processes that process subproblems, one for the master process, and another one for a proxy process that manages shared data.

• A negative value workers=-n uses os.cpu_count() - n CPUs for workers, plus two additional CPUs for the master and proxy processes. It follows that workers=-2 uses all available CPUs, while workers=-3 leaves one CPU free.

Attention

• workers=1 uses the parallel implementation with only one worker. Algorithmically, this is similar to the sequential implementation with workers=0, but introduces overhead.

• workers=-1 uses os.cpu_count() + 1 CPUs, which is not a natural choice.

See also

logic1.abc.qe.Node

The subproblems referred to above correspond to instances of this class.

Quantifier Elimination

class logic1.abc.qe.QuantifierElimination

Bases: Generic[ν, μ, λ, ι, ω, α, τ, χ, σ], ABC

A generic callable class that implements quantifier elimination.

A first group of attributes holds the state of the computation:

property assumptions: list[α]

A list of atoms, which serve as external assumptions. This includes the assumptions passed via the assume parameter of __call__(). Some theories have an option for generic quantifier elimination, which adds additional assumptions on parameters in the course of the elimination.

blocks: Prefix[χ] | None = None

Remaining quantifier blocks, to be processed after the current block.

matrix: Formula[α, τ, χ, σ] | None = None

The quantifier-free formula associated with blocks. This is None while there is a block being processed.

negated: bool | None = None

Indicates whether or not the block currently processed has been logically negated in order to equivalently transform universal quantifiers into existential quanitifers.

root_nodes: list[ν] | None = None

The root nodes of the next block to be processed. Logically, the list describes a disjunction, and each node in root_nodes describes a quantifier elimination subproblem Ex(node.variables, node.formula). This is an intermediate object for moving the innermost block with and the matrix into the working_nodes.

working_nodes: WorkingNodeList[ν, μ] | None = None

Subproblems left for the current block. Element nodes of working_nodes have the same shape as element nodes of root_nodes

success_nodes: NodeList[ν, μ] | None = None

Finished subproblems of the current block. For each node in success_nodes we have node.variables == [].

failure_nodes: NodeList[ν, μ] | None = None

Failed subproblems of the current block, which can occur with incomplete quantifier elimination procedures. An element nodes of failure_nodes have the same shape as an element node of working_nodes, but quantifier elimination procedure could not eliminate any variable from the node.

result: Formula[α, τ, χ, σ] | None = None

The final result as returned by __call__().

Note that the parameter f of __call__() inizializes blocks and matrix, and the parameter assume inizializes assumptions. The next group of attributes corresponds to read-only input parameters of __call__():

options: ω | None = None

The options that have been passed to __call__().

The third and last group of attributes holds comprehensive timing information on the last computation. All times are wall times in seconds:

time_syncmanager_enter: float | None = None

The time spent for starting the SyncManager, which is a proxy process that manages shared data in multiprocessing.

time_start_first_worker: float | None = None

The time spent for starting the first worker process in multiprocessing.

time_start_all_workers: float | None = None

The time spent for starting all worker processes in multiprocessing.

time_multiprocessing: float | None = None

The time spent in multiprocessing after the first worker process has been started and until the last worker process has terminated.

time_import_failure_nodes: float | None = None

The time spent for importing all failure_nodes from the SyncManager into the master process after all workers have terminated.

time_import_success_nodes: float | None = None

The time spent for importing all success_nodes from the SyncManager into the master process after all workers have terminated.

time_import_working_nodes: float | None = None

The time spent for importing all working_nodes from the SyncManager into the master process after all workers have terminated.

time_syncmanager_exit: float | None = None

The time spent for exiting the SyncManager.

time_final_simplification: float | None = None

The time spent for finally simplifying the disjunction over all success_nodes imported from the workers. This yields the final result, which is also the return value of __call__().

time_total: float | None = None

The total time spent in __call__().

__call__(f: Formula[α, τ, χ, σ], assume: Iterable[α] = [], **options) → Formula[α, τ, χ, σ] | None

The entry point 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.

• **options – Keyword arguments with keywords corresponding to attributes of the generic type ω, which extends Options.

Returns:

A quantifier-free equivalent of f modulo certain assumptions. A simplified equivalent of all relevant assumptions are available as assumptions.

• Regularly, the assumptions are exactly those passed as the assume parameter.

• Some theories have an option for generic quantifier elimination, which adds additional assumptions in the course of the elimination.

abstractmethod create_options(**kwargs) → ω

Create an instance of ω that holds **kwargs. The **kwargs arriving here are the **options that have been passed to __call__().

abstractmethod create_root_nodes(variables: Iterable[χ], matrix: Formula[α, τ, χ, σ]) → list[ν]

If matrix is not a disjunction, create a list containing one instance node of ν with node.variables == variables and node.formula == matrix. If matrix is a disjunction Or(*args), create a list containing one such node for each arg in args.

abstractmethod create_assumptions(assume: Iterable[α]) → λ

Create in instance of λ that holds assume. Those assumptions assume are the corresponding parameter of __call__().

abstractmethod create_true_node() → ν

Create an instance node of ν with node.variables == [] and node.formula == _T().

abstractmethod final_simplify(formula: Formula[α, τ, χ, σ], assume: Iterable[α] = []) → Formula[α, τ, χ, σ]

Used for simplifying the disjunction of all success_nodes. The return value yields result, which is then used as the return value of __call__().

abstractmethod classmethod init_env(arg: ι) → None

A hook for initialization of worker process. This is used, e.g., in Real Closed Fields for reconstructing within the worker the Sage polynomial ring of the master.

abstractmethod init_env_arg() → ι

Create an instance of ι to be used as an argument for a subsequent call of init_env().

Node Lists

class logic1.abc.qe.NodeList

Bases: Collection[ν], Generic[ν, μ]

A list of nodes with a memory to avoid duplicates and statistics about the number of nodes added and dropped.

class logic1.abc.qe.WorkingNodeList

Bases: NodeList[ν, μ]

A subclass of NodeList that is used for the list of nodes that are currently being processed during quantifier elimination. Additionally, it keeps track of the current number of nodes with a given number of variables.