Quantifier Elimination

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:

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=Formula)#: A type variable denoting a formula with upper bound logic1.firstorder.formula.Formula.

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='Options')#: A type variable denoting a options for QuantifierElimination.__call__() with upper bound Options.

Assumptions#

class logic1.abc.qe.Assumptions[source]#

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

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.

Nodes#

class logic1.abc.qe.Node[source]#

Bases: Generic[φ, χ, λ]

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: φ#: A quantifier-free formula.

abstract copy() → Self[source]#: Create a copy of this node.

abstract process(assumptions: λ) → list[Self][source]#

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:

variable is not in successor.variables for successor in S;
variable does not occur in successor.formula for successor in S;
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[source]#

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 = 0#: The log_level of the logger used by QuantifierElimination.

log_rate: float = 0.5#: The minimal timespan (in s) between to log outputs in certain loops.

Quantifier Elimination#

class logic1.abc.qe.QuantifierElimination[source]#

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

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[Formula[α, τ, χ, σ], ν] | 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[Formula[α, τ, χ, σ], ν] | None = None#: Finished subproblems of the current block. For each node in success_nodes we have node.variables == [].

failure_nodes: NodeList[Formula[α, τ, χ, σ], ν] | 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__():

workers: int = 0#: The number of worker processes used. For more information see the documentation of the parameter workers 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[α] = [], workers: int = 0, **options) → Formula[α, τ, χ, σ] | None[source]#

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.
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 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.

abstract create_options(**kwargs) → ω[source]#: Create an instance of ω that holds **kwargs. The **kwargs arriving here are the **options that have been passed to __call__().

abstract create_root_nodes(variables: Iterable[χ], matrix: Formula[α, τ, χ, σ]) → list[ν][source]#: 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.

abstract create_assumptions(assume: Iterable[α]) → λ[source]#: Create in instance of λ that holds assume. Those assumptions assume are the corresponding parameter of __call__().

abstract create_true_node() → ν[source]#: Create an instance node of ν with node.variables == [] and node.formula == _T().

abstract final_simplify(formula: Formula[α, τ, χ, σ], assume: Iterable[α] = []) → Formula[α, τ, χ, σ][source]#: Used for simplifying the disjunction of all success_nodes. The return value yields result, which is then used as the return value of __call__().

abstract classmethod init_env(arg: ι) → None[source]#: 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.

abstract init_env_arg() → ι[source]#: Create an instance of ι to be used as an argument for a subsequent call of init_env().

Quantifier Elimination

Contents

Quantifier Elimination#

Generic Types#

Assumptions#

Nodes#

Options#

Quantifier Elimination#