from __future__ import annotations
from collections import Counter
from dataclasses import dataclass
from itertools import combinations
import logging
from typing import Iterable, Never
from logic1 import abc
from logic1.firstorder import And, Or, _T
from logic1.support.tracing import trace # noqa
from logic1.theories.Sets.atomic import AtomicFormula, C, Eq, Ne, Variable
from logic1.theories.Sets.bnf import dnf
from logic1.theories.Sets.simplify import simplify
from logic1.theories.Sets.types import Formula
[docs]
class Assumptions(abc.qe.Assumptions[AtomicFormula, Variable, Variable, Never]):
"""Implements the abstract method :meth:`simplify()
<.abc.qe.Assumptions.simplify>` of its super class :class:`.abc.qe.Assumptions`.
Required by :class:`.Node` and :class:`.QuantifierElimination` for
instantiating the type variable :data:`.abc.qe.λ` of :class:`.abc.qe.Node`
and :class:`.abc.qe.QuantifierElimination`, respectively.
"""
def simplify(self, f: Formula) -> Formula:
"""Implements the abstract method :meth:`.abc.qe.Assumptions.simplify`.
"""
return simplify(f)
[docs]
@dataclass
class Node(abc.qe.Node[AtomicFormula, Variable, Variable, Never, Assumptions, Formula]):
"""Implements the abstract methods :meth:`copy() <.abc.qe.Node.copy>`,
:meth:`memorize() <.abc.qe.Node.memorize>` and
:meth:`process() <.abc.qe.Node.process>` of its super class
:class:`.abc.qe.Node`. Required by :class:`.QuantifierElimination` for
instantiating the type variable :data:`.abc.qe.ν` of
:class:`.abc.qe.QuantifierElimination`.
"""
options: abc.qe.Options
def copy(self) -> Node:
"""Implements the abstract method :meth:`.abc.qe.Node.copy`.
"""
return Node(variables=self.variables, formula=self.formula, options=self.options)
def memorize(self) -> Formula:
"""Implements the abstract method :meth:`.abc.qe.Node.memoize`.
"""
return self.formula
def process(self, assumptions: Assumptions) -> list[Node]:
"""Implements the abstract method :meth:`.abc.qe.Node.process`.
"""
# We assume that that atoms of the form v == v or v != v have been
# removed by simplification. This is similar to the assumption in RCF
# that right hand sides are zero. Both are not asserted anywhere at the
# moment.
counter = Counter(self.formula.bvars(frozenset(self.variables)))
if not counter:
return [Node(variables=[], formula=self.formula, options=self.options)]
best_variable, _ = counter.most_common()[-1]
self.variables.remove(best_variable)
phi_prime = self.qe1(best_variable, self.formula)
phi_prime = simplify(phi_prime, assume=assumptions.atoms)
phi_prime = dnf(phi_prime)
match phi_prime:
case Or():
nodes = []
for arg in phi_prime.args:
formula = simplify(arg, assume=assumptions.atoms)
if formula is _T():
raise abc.qe.FoundT()
nodes.append(Node(variables=self.variables.copy(),
formula=formula,
options=self.options))
return nodes
case _:
formula = simplify(phi_prime, assume=assumptions.atoms)
if formula is _T():
raise abc.qe.FoundT()
return [Node(variables=self.variables.copy(),
formula=formula,
options=self.options)]
def qe1(self, v: Variable, f: Formula) -> Formula:
def eta(Z: set[Variable], k: int) -> Formula:
args = []
for k_choice in combinations(Z, k):
args1: list[Formula] = []
for z in Z:
args_inner = (Eq(z, chosen_z) for chosen_z in k_choice)
args1.append(Or(*args_inner))
for i in range(k):
for j in range(i + 1, k):
args1.append(Ne(k_choice[i], k_choice[j]))
args.append(And(*args1))
return Or(*args)
def split(v: Variable, f: Formula) -> tuple[list[Eq], list[Ne], list[AtomicFormula]]:
eqs = []
nes = []
others = []
args = f.args if isinstance(f, And) else (f,)
for atom in args:
match atom:
case Eq() if v in atom.fvars():
eqs.append(atom)
case Ne() if v in atom.fvars():
nes.append(atom)
case AtomicFormula():
others.append(atom)
case _:
assert False, (v, f)
return eqs, nes, others
logging.info(f'{self.qe1.__qualname__}: eliminating Ex {v} ({f})')
eqs, nes, others = split(v, f)
if eqs:
if eqs[0].lhs == v:
return And(f.subs({v: eqs[0].rhs}), *others)
else:
assert eqs[0].rhs == v
return And(f.subs({v: eqs[0].lhs}), *others)
Z = {z for ne in nes for z in ne.fvars(frozenset({v}))}
m = len(Z)
args = (And(eta(Z, k), C(k + 1)) for k in range(1, m + 1))
phi_prime = Or(*args)
result = And(phi_prime, *others)
logging.info(f'{self.qe1.__qualname__}: result is {phi_prime}')
return result
[docs]
@dataclass
class QuantifierElimination(abc.qe.QuantifierElimination[Node, Formula,
Assumptions, None, abc.qe.Options, AtomicFormula, Variable, Variable, Never]):
"""
Quantifier elimination for the theory of sets with cardinality constraints.
Implements the abstract methods
:meth:`create_options() <.abc.qe.QuantifierElimination.create_options>`,
:meth:`create_root_nodes() <.abc.qe.QuantifierElimination.create_root_nodes>`,
:meth:`create_assumptions() <.abc.qe.QuantifierElimination.create_assumptions>`,
:meth:`create_true_node() <.abc.qe.QuantifierElimination.create_true_node>`,
:meth:`final_simplify() <.abc.qe.QuantifierElimination.final_simplify>`,
:meth:`init_env() <.abc.qe.QuantifierElimination.init_env>`,
:meth:`init_env_arg() <.abc.qe.QuantifierElimination.init_env_arg>` of its
super class :class:`.abc.qe.QuantifierElimination`.
"""
def create_options(self, **kwargs) -> abc.qe.Options:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.create_options`.
"""
return abc.qe.Options(**kwargs)
def create_root_nodes(self, variables: Iterable[Variable], matrix: Formula) -> list[Node]:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.create_root_nodes`.
"""
assert self.options is not None
assert self._assumptions is not None
formula = simplify(matrix, assume=self._assumptions.atoms)
formula = dnf(formula)
match formula:
case Or():
root_nodes = []
for arg in formula.args:
node = Node(variables=list(variables),
formula=simplify(arg, assume=self._assumptions.atoms),
options=self.options)
if node.formula is _T():
raise abc.qe.FoundT()
root_nodes.append(node)
return root_nodes
case _:
node = Node(variables=list(variables),
formula=simplify(formula, assume=self._assumptions.atoms),
options=self.options)
if node.formula is _T():
raise abc.qe.FoundT()
return [node]
def create_assumptions(self, assume: Iterable[AtomicFormula]) -> Assumptions:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.create_assumptions`.
"""
return Assumptions(assume)
def create_true_node(self) -> Node:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.create_true_node`.
"""
assert self.options is not None
return Node(variables=[], formula=_T(), options=self.options)
def final_simplify(self, formula: Formula, assume: Iterable[AtomicFormula] = []) -> Formula:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.final_simplify`.
"""
return simplify(formula, assume)
@classmethod
def init_env(cls, none: None) -> None:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.init_env`.
"""
pass
def init_env_arg(self) -> None:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.init_env_arg`.
"""
return None
qe = quantifier_elimination = QuantifierElimination()
r"""
Quantifier elimination for the theory of sets with cardinanity constraints.
Returns a quantifier-free equivalent ``f'`` of ``f`` modulo the assumptions
passed in the `assume` parameter.
.. math::
\textsf{Sets} \models \bigwedge \mathtt{assume} \longrightarrow
(\mathtt{f} \longleftrightarrow \mathtt{f'}).
.. seealso::
:class:`logic1.abc.qe.Options`
for the options that can be passed to this function.
:attr:`logic1.abc.qe.Options.workers`
explains how to specify parallel computation of subproblems.
:class:`logic1.theories.Sets.qe.Node`
The subproblems referred to above correspond to instances of this class.
:class:`logic1.theories.Sets.qe.QuantifierElimination`
:obj:`qe` is an instance of this callable class.
"""