Package logic1.abc

Package `logic1.abc`#

Module `qe`#

exception logic1.abc.qe.FoundT#: Bases: Exception

class logic1.abc.qe.QuantifierElimination(blocks=None, matrix=None, negated=None, pool=None, finished=None)#

Bases: ABC

class Pool(vars_: list[Any], f: Formula)#

Bases: list

push(vars_: list[Any], f: Formula) → None#

Quantifier#: alias of type[QuantifiedFormula]

QuantifierBlock#: alias of tuple[type[QuantifiedFormula], list[Any]]

Job#: alias of tuple[list[Any], Formula]

blocks: list[QuantifierBlock] | None#

matrix: Formula | None#

negated: bool | None#

pool: Pool | None#

finished: list[Formula] | None#

collect_finished() → None#

pop_block() → None#

process_pool() → None#

qe(f: Formula) → Formula#

abstract qe1p(v: Any, f: Formula) → Formula#

setup(f: Formula) → None#

abstract static is_valid_atom(f: Formula) → bool#