"""Real quantifier elimination by virtual substitution [Sturm-2018]_.
"""
from __future__ import annotations
from dataclasses import dataclass, field
from enum import auto, Enum
from typing import ClassVar, Iterable, Iterator, Literal, Optional, TypeAlias
from typing import reveal_type # noqa
from logic1 import abc
from logic1.firstorder import And, _F, Not, Or, _T
from logic1.support.tracing import trace # noqa
from logic1.theories.RCF.atomic import (
AtomicFormula, Eq, Ne, Ge, Le, Gt, Lt, polynomial_ring, Term, Variable)
from logic1.theories.RCF.simplify import is_valid, simplify
from logic1.theories.RCF.typing import Formula
class DegreeViolation(abc.qe.NodeProcessFailure):
pass
class Failed(Exception):
pass
[docs]
class Assumptions(abc.qe.Assumptions[AtomicFormula, Term, Variable, int]):
"""Implements the abstract method :meth:`simplify()
<.abc.qe.Assumptions.simplify>` of its super class
:class:`.abc.qe.Assumptions`. Required by :class:`.Node` and
:class:`.VirtualSubstitution` 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, explode_always=False, prefer_order=False, prefer_weak=True)
[docs]
class CLUSTERING(Enum):
"""Available clustering strategies. Required by :class:`.Options`.
"""
NONE = auto()
"""No clustering at all.
"""
FULL = auto()
"""Full clustering.
"""
[docs]
class GENERIC(Enum):
"""Available degrees of genericity. For details on generic quantifier
elimination see
Required by :class:`.Options`.
"""
NONE = auto()
"""Regular quantifier elimination, not making any assumptions.
"""
MONOMIAL = auto()
"""Admit assumptions on parameters by adding atomic formulas to
:attr:`.abc.qe.QuantifierElimination.assumptions`, where the left hand side of those
atomic formulas is a monomial (and the right hand side is zero).
"""
FULL = auto()
"""Admit assumptions on parameters by adding atomic formulas to
:attr:`.abc.qe.QuantifierElimination.assumptions`.
"""
class NSP(Enum):
NONE = auto()
PLUS_EPSILON = auto()
MINUS_EPSILON = auto()
PLUS_INFINITY = auto()
MINUS_INFINITY = auto()
class TAG(Enum):
XLB = auto()
XUB = auto()
ANY = auto()
SignSequence: TypeAlias = tuple[Literal[-1, 0, 1], ...]
@dataclass(frozen=True)
class RootSpec:
signs: SignSequence
index: int
def __neg__(self) -> RootSpec:
return RootSpec(signs=tuple(-i for i in self.signs), index=self.index)
def bound_type(self, atom: AtomicFormula) -> tuple[bool, Optional[TAG]]:
"""Return value None means that atom has a constant truth value
"""
zero_index = 2 * self.index - 1
assert self.signs[zero_index] == 0, (self, atom)
left = self.signs[zero_index - 1]
right = self.signs[zero_index + 1]
assert left != 0 and right != 0, (self, atom)
match (atom, left, right):
case (Eq(), _, _):
return (False, TAG.ANY)
case (Ne(), _, _):
return (True, TAG.ANY)
case (Lt(), -1, -1) | (Gt(), 1, 1):
return (True, TAG.ANY)
case (Lt(), -1, 1) | (Gt(), 1, -1):
return (True, TAG.XUB)
case (Lt(), 1, -1) | (Gt(), -1, 1):
return (True, TAG.XLB)
case (Lt(), 1, 1) | (Gt(), -1, -1):
return (True, None)
case (Le(), -1, -1) | (Ge(), 1, 1):
return (False, None)
case (Le(), -1, 1) | (Ge(), 1, -1):
return (False, TAG.XUB)
case (Le(), 1, -1) | (Ge(), -1, 1):
return (False, TAG.XLB)
case (Le(), 1, 1) | (Ge(), -1, -1):
return (False, TAG.ANY)
case _:
assert False, (atom, left, right)
def guard(self, term: Term, x: Variable) -> Formula:
match term.degree(x):
case -1 | 0:
assert False, (self, term, x)
case 1:
a = term.coefficient({x: 1})
match self.signs:
case (-1, 0, 1):
return a > 0
case (1, 0, -1):
return a < 0
case _:
assert False, (self, term, x)
case 2:
a = term.coefficient({x: 2})
b = term.coefficient({x: 1})
c = term.coefficient({x: 0})
d2 = b**2 - 4 * a * c
match self.signs:
case (1, 0, -1, 0, 1):
return And(a > 0, d2 > 0)
case (-1, 0, 1, 0, -1):
return And(a < 0, d2 > 0)
case (1, 0, 1):
return And(a > 0, d2 == 0)
case (-1, 0, -1):
return And(a < 0, d2 == 0)
case _:
assert False, (self, term, x)
case _:
raise DegreeViolation(self, term, x)
def kosta_code(self, d: int) -> int:
D: dict[tuple[int, SignSequence], int] = {
(1, (-1, 0, 1)): 1,
(1, (1, 0, -1)): -1,
(2, (1, 0, -1, 0, 1)): 1,
(2, (1, 0, 1)): 2,
(2, (1,)): 3,
(2, (-1, 0, 1, 0, -1)): -1,
(2, (-1, 0, -1)): -2,
(2, (-1,)): -3,
(3, (-1, 0, 1)): 1,
(3, (-1, 0, -1, 0, 1)): 2,
(3, (-1, 0, 1, 0, 1)): 3,
(3, (-1, 0, 1, 0, -1, 0, 1)): 4,
(3, (1, 0, -1)): -1,
(3, (1, 0, 1, 0, -1)): -2,
(3, (1, 0, -1, 0, -1)): -3,
(3, (1, 0, -1, 0, 1, 0, -1)): -4}
return D[d, self.signs]
@dataclass(frozen=True)
class Cluster:
root_specs: tuple[RootSpec, ...]
def __neg__(self) -> Cluster:
return Cluster(tuple(- root_spec for root_spec in self.root_specs))
def __iter__(self) -> Iterator[RootSpec]:
return iter(self.root_specs)
def bound_type(self, atom: AtomicFormula, x: Variable, assumptions: Assumptions)\
-> tuple[bool, Optional[TAG]]:
epsilons = set()
tags = set()
for root_spec in self.root_specs:
if simplify(root_spec.guard(atom.lhs, x), assume=assumptions.atoms) is _F():
continue
with_epsilon, tag = root_spec.bound_type(atom)
if tag is not None:
epsilons.add(with_epsilon)
tags.add(tag)
assert len(epsilons) <= 1, (self, atom, x)
try:
epsilon = next(iter(epsilons))
except StopIteration:
epsilon = False
if len(tags) == 0:
tag = None
elif tags == {TAG.XLB} or tags == {TAG.XLB, TAG.ANY}:
tag = TAG.XLB
elif tags == {TAG.XUB} or tags == {TAG.XUB, TAG.ANY}:
tag = TAG.XUB
else:
tag = TAG.ANY
return (epsilon, tag)
def guard(self, term: Term, x: Variable) -> Formula:
d = term.degree(x)
match d, self:
case 1, Cluster((RootSpec(signs=(-1, 0, 1), index=1),
RootSpec(signs=(1, 0, -1), index=1))):
a = term.coefficient({x: 1})
return a != 0
case 2, Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),
RootSpec(signs=(-1, 0, 1, 0, -1), index=2),
RootSpec(signs=(1, 0, 1), index=1),
RootSpec(signs=(-1, 0, -1), index=1))):
a = term.coefficient({x: 2})
b = term.coefficient({x: 1})
c = term.coefficient({x: 0})
d2 = b**2 - 4 * a * c
return And(a != 0, d2 >= 0)
case _:
return Or(*(root_spec.guard(term, x) for root_spec in self.root_specs))
@dataclass(frozen=True)
class PRD:
"""Parametric Root Description"""
term: Term
variable: Variable
cluster: Cluster
xguard: Formula = field(default_factory=_T)
def guard(self, assumptions: Assumptions) -> Formula:
guard = self.cluster.guard(self.term, self.variable)
return simplify(And(self.xguard, guard), assume=assumptions.atoms)
def vsubs(self, atom: AtomicFormula) -> Formula:
"""Virtually substitute self into atom yielding a quantifier-free
formula
"""
match atom:
case Ne() | Gt() | Ge():
return Not(self._vsubs(atom.to_complement())).to_nnf()
case Eq() | Lt() | Le():
return self._vsubs(atom)
case _:
assert False, (self, atom)
def _vsubs(self, atom: AtomicFormula) -> Formula:
"""Virtual substitution of PRD into atom.
"""
x = self.variable
deg_g = atom.lhs.degree(x)
match deg_g:
case -1 | 0:
return atom
case 1:
aa = atom.lhs.coefficient({x: 1})
bb = atom.lhs.coefficient({x: 0})
case _:
raise NotImplementedError(deg_g)
deg_f = self.term.degree(x)
assert deg_g < deg_f, f'{self=}, {atom=}' # Pseudo-division has been applied
# f into g
match deg_f:
case -1 | 0 | 1:
assert False
case 2:
a = self.term.coefficient({x: 2})
b = self.term.coefficient({x: 1})
c = self.term.coefficient({x: 0})
A = 2 * a * aa * bb - aa**2 * b
B = a * bb**2 + aa**2 * c - aa * b * bb
C = 2 * a * bb - aa * b
match (deg_g, atom, self.cluster):
# Kosta Appendix A.1: Without clustering
case (1, Eq(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),))):
return And(A >= 0, B == 0)
case (1, Eq(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=2),))):
return And(A <= 0, B == 0)
case (1, Eq(), Cluster((RootSpec(signs=(1, 0, 1), index=1),))):
return C == 0
case (1, Lt(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),))):
return Or(And(C < 0, B > 0), And(aa >= 0, Or(C < 0, B < 0)))
case (1, Lt(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=2),))):
return Or(And(C < 0, B > 0), And(aa <= 0, Or(C < 0, B < 0)))
case (1, Lt(), Cluster((RootSpec(signs=(1, 0, 1), index=1),))):
return C < 0
case (1, Le(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),))):
return Or(And(C <= 0, B >= 0), And(aa >= 0, B <= 0))
case (1, Le(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=2),))):
return Or(And(C <= 0, B >= 0), And(aa <= 0, B <= 0))
case (1, Le(), Cluster((RootSpec(signs=(1, 0, 1), index=1),))):
return C <= 0
# Kosta Appendix A.3: With clustering
case (1, Eq(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),
RootSpec(signs=(-1, 0, 1, 0, -1), index=2),
RootSpec(signs=(1, 0, 1), index=1),
RootSpec(signs=(-1, 0, -1), index=1)))):
return And(A >= 0, B == 0)
case (1, Lt(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),
RootSpec(signs=(-1, 0, 1, 0, -1), index=2),
RootSpec(signs=(1, 0, 1), index=1),
RootSpec(signs=(-1, 0, -1), index=1)))):
return Or(And(a * C < 0, a * B > 0),
And(a * aa >= 0, Or(a * C < 0, a * B < 0)))
case (1, Le(), Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),
RootSpec(signs=(-1, 0, 1, 0, -1), index=2),
RootSpec(signs=(1, 0, 1), index=1),
RootSpec(signs=(-1, 0, -1), index=1)))):
return Or(And(a * C <= 0, a * B >= 0), And(a * aa >= 0, a * B <= 0))
case _:
assert False, f'{self=}, {atom=}'
case _:
raise NotImplementedError(f'{self=}, {atom=}')
def _translate(self) -> str:
x = self.variable
deg_f = self.term.degree(x)
a = self.term.coefficient({x: 2})
b = self.term.coefficient({x: 1})
c = self.term.coefficient({x: 0})
match deg_f:
case 1:
match self.cluster:
# CLUSTERING.NONE
case Cluster((RootSpec(signs=(-1, 0, 1), index=1),)):
return f'({-c}) / ({b})'
# CLUSTERING.FULL
case Cluster((RootSpec(signs=(-1, 0, 1), index=1),
RootSpec(signs=(1, 0, -1), index=1))):
return f'({-c}) / ({b})'
case _:
assert False, self
case 2:
match self.cluster:
# CLUSTERING.NONE
case Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),)):
return f'({-b} - sqrt({b**2- 4*a*c})) / ({2*a})'
case Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=2),)):
return f'({-b} + sqrt({b**2- 4*a*c})) / ({2*a})'
case Cluster((RootSpec(signs=(1, 0, 1), index=1),)):
return f'({-b} ± sqrt({0})) / ({2*a})'
# CLUSTERING.FULL
case Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),
RootSpec(signs=(-1, 0, 1, 0, -1), index=2),
RootSpec(signs=(1, 0, 1), index=1),
RootSpec(signs=(-1, 0, -1), index=1))):
return f'({-b} - sqrt({b**2- 4*a*c})) / ({2*a})'
case _:
assert False, self
case _:
assert False, self
@dataclass(frozen=True)
class CandidateSolution:
# CandidateSolutions are used as elements of sets. In order to become
# hashable, the dataclass is frozen, along with RootSpec, PRD, and
# RealType.
prd: PRD
with_epsilon: bool
tag: TAG
@dataclass
class TestPoint:
prd: Optional[PRD] = None
nsp: NSP = NSP.NONE
def guard(self, assumptions: Assumptions):
if self.prd is None:
return _T()
else:
guard = self.prd.guard(assumptions)
assert guard is not _F(), self
return guard
def _translate(self) -> str:
assert self.prd is not None
match self.nsp:
case NSP.NONE:
return self.prd._translate()
case NSP.PLUS_EPSILON:
return self.prd._translate() + ' + epsilon'
case NSP.MINUS_EPSILON:
return self.prd._translate() + ' - epsilon'
case NSP.PLUS_INFINITY:
return '+inf'
case NSP.MINUS_INFINITY:
return '-inf'
case _:
assert False, self
@dataclass
class EliminationSet:
variable: Variable
test_points: list[TestPoint]
method: str
def _translate(self, assumptions: Assumptions):
return (self.method,
self.variable,
[(tp.guard(assumptions), tp._translate()) for tp in self.test_points])
[docs]
@dataclass
class Node(abc.qe.Node[Formula, Variable, Assumptions]):
"""Implements the abstract methods :meth:`copy() <.abc.qe.Node.copy>` and
:meth:`process() <.abc.qe.Node.process>` of its super class
:class:`.abc.qe.Node`. Required by :class:`.VirtualSubstitution` for
instantiating the type variable :data:`.abc.qe.ν` of
:class:`.abc.qe.QuantifierElimination`.
"""
answer: list
outermost_block: bool
options: Options
real_type_selection: ClassVar[dict[CLUSTERING,
dict[int, list[Cluster]]]] = {
# W.l.o.g. the last sign in the first SignSequence of each tuple is always +1.
CLUSTERING.NONE: {
1: [Cluster((RootSpec(signs=(-1, 0, 1), index=1),))],
2: [Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),)),
Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=2),)),
Cluster((RootSpec(signs=(1, 0, 1), index=1),))]
},
CLUSTERING.FULL: {
1: [Cluster((RootSpec(signs=(-1, 0, 1), index=1),
RootSpec(signs=(1, 0, -1), index=1)))],
2: [Cluster((RootSpec(signs=(1, 0, -1, 0, 1), index=1),
RootSpec(signs=(-1, 0, 1, 0, -1), index=2),
RootSpec(signs=(1, 0, 1), index=1),
RootSpec(signs=(-1, 0, -1), index=1)))]
}
}
def __str__(self):
return (f'Node({self.variables}, {self.formula}, {self.answer}, {self.outermost_block}, '
f'{self.options})')
def copy(self) -> Node:
"""Implements the abstract method :meth:`.abc.qe.Node.copy`.
"""
return Node(variables=self.variables,
formula=self.formula,
answer=self.answer,
outermost_block=self.outermost_block,
options=self.options)
def eset(self, assumptions: Assumptions) -> EliminationSet:
return self.gauss_eset(assumptions) or self.regular_eset(assumptions)
def gauss_eset(self, assumptions: Assumptions) -> Optional[EliminationSet]:
if not isinstance(self.formula, And):
return None
for degree in (1, 2):
# Look for degree-Gauss with a non-zero coefficient modulo assumptions
for round_ in (GENERIC.NONE, GENERIC.MONOMIAL, GENERIC.FULL):
if round_ == GENERIC.MONOMIAL and not self.outermost_block:
break
if round_ == GENERIC.MONOMIAL and self.options.generic == GENERIC.NONE:
break
if round_ == GENERIC.FULL and self.options.generic == GENERIC.MONOMIAL:
break
for x in self.variables:
for arg in self.formula.args:
if not isinstance(arg, Eq):
continue
lhs = arg.lhs
if lhs.degree(x) != degree:
# Possibly lhs.degree(x) < 0 when x does not occur
continue
a = lhs.coefficient({x: degree})
match round_:
case GENERIC.NONE:
if not is_valid(a != 0, assumptions.atoms):
continue
abc.qe.logger.debug(f'{degree}-Gauss')
case GENERIC.MONOMIAL:
if len(a.monomials()) > 1:
continue
if not set(a.vars()).isdisjoint(self.variables):
continue
assumptions.append(a != 0)
abc.qe.logger.debug(f'{degree}-Gauss assuming {a != 0}')
case GENERIC.FULL:
if not set(a.vars()).isdisjoint(self.variables):
continue
assumptions.append(a != 0)
abc.qe.logger.debug(f'{degree}-Gauss assuming {a != 0}')
self.variables.remove(x)
test_points = []
for cluster in self.real_type_selection[self.options.clustering][degree]:
for sign in (1, -1):
prd = PRD(sign * lhs, x, cluster)
if prd.guard(assumptions) is not _F():
test_points.append(TestPoint(prd))
eset = EliminationSet(variable=x, test_points=test_points, method='g')
return eset
return None
def is_admissible_assumption(self, atom: Ne) -> bool:
match self.options.generic:
case GENERIC.NONE:
return False
case GENERIC.MONOMIAL:
if len(atom.lhs.monomials()) > 1:
return False
if not set(atom.fvars()).isdisjoint(self.variables):
return False
return True
case GENERIC.FULL:
if not set(atom.fvars()).isdisjoint(self.variables):
return False
return True
case _:
assert False, self.options.generic
def process(self, assumptions: Assumptions) -> list[Node]:
"""Implements the abstract method :meth:`.abc.qe.Node.process`.
"""
eset = self.eset(assumptions)
nodes = self.vsubs(eset, assumptions)
return nodes
def regular_eset(self, assumptions: Assumptions) -> EliminationSet:
def red(f: Term, x: Variable, d: int) -> Term:
return f - f.coefficient({x: d}) * x ** d
def at_cs(atom: AtomicFormula, x: Variable) -> set[CandidateSolution]:
"""Produce the set of candidate solutions of an atomic formula.
"""
candidate_solutions = set()
xguard: Formula = _T()
while (d := atom.lhs.degree(x)) > 0:
clusters = Node.real_type_selection[self.options.clustering][d]
for cluster in clusters:
prd = PRD(atom.lhs, x, cluster, xguard)
(with_epsilon, tag) = cluster.bound_type(atom, x, assumptions)
if tag is not None:
cs = CandidateSolution(prd, with_epsilon, tag)
candidate_solutions.add(cs)
if set(cluster) != set(- cluster):
prd = PRD(- atom.lhs, x, cluster, xguard)
(with_epsilon, tag) = (- cluster).bound_type(atom, x, assumptions)
if tag is not None:
cs = CandidateSolution(prd, with_epsilon, tag)
candidate_solutions.add(cs)
lc = atom.lhs.coefficient({x: d})
if self.is_admissible_assumption(lc != 0):
assumptions.append(lc != 0)
break
atom = atom.op(red(atom.lhs, x, d), 0)
if self.options.traditional_guards:
xguard = And(xguard, lc == 0)
return candidate_solutions
smallest_eset_size = None
assert self.variables
for x in self.variables:
# We can use (with_epsilon, TAG) as a key in the future.
candidates: dict[TAG, set[CandidateSolution]] = {tag: set() for tag in TAG}
for atom in sorted(set(self.formula.atoms())):
assert isinstance(atom, AtomicFormula)
assert atom.rhs == Term(0)
match atom.lhs.degree(x):
case -1:
assert False, atom
case 0 | 1 | 2:
for candidate in at_cs(atom, x):
if candidate.prd.guard(assumptions) is not _F():
candidates[candidate.tag].add(candidate)
case _:
raise DegreeViolation(atom, x, atom.lhs.degree(x))
num_xub = len(candidates[TAG.XUB])
num_xlb = len(candidates[TAG.XLB])
num_any = len(candidates[TAG.ANY])
eset_size = min(num_xub, num_xlb) + num_any
if smallest_eset_size is None or eset_size < smallest_eset_size:
smallest_eset_size = eset_size
best_variable = x
best_candidates = candidates
if num_xub < num_xlb:
best_inf, best_eps, best_xb = NSP.PLUS_INFINITY, NSP.MINUS_EPSILON, TAG.XUB
else:
best_inf, best_eps, best_xb = NSP.MINUS_INFINITY, NSP.PLUS_EPSILON, TAG.XLB
self.variables.remove(best_variable)
test_points = [TestPoint(nsp=best_inf)]
for tag in (TAG.ANY, best_xb):
for candidate in best_candidates[tag]:
if candidate.with_epsilon:
test_points.append(TestPoint(candidate.prd, best_eps))
else:
test_points.append(TestPoint(candidate.prd))
eset = EliminationSet(variable=best_variable, test_points=test_points, method='e')
return eset
def vsubs(self, eset: EliminationSet, assumptions: Assumptions) -> list[Node]:
def vs_at(atom: AtomicFormula, tp: TestPoint, x: Variable) -> Formula:
"""Virtually substitute a test point into an atom.
"""
match tp.nsp:
case NSP.NONE:
assert tp.prd is not None
h = pseudo_sgn_rem(atom.lhs, tp.prd, x)
return vs_prd_at(atom.op(h, 0), tp.prd, x)
case NSP.PLUS_EPSILON | NSP.MINUS_EPSILON:
phi = expand_eps_at(atom, tp.nsp, x)
recurse = lambda atom: vs_at(atom, TestPoint(tp.prd, NSP.NONE), x) # noqa E731
return phi.transform_atoms(recurse)
case NSP.PLUS_INFINITY | NSP.MINUS_INFINITY:
return vs_inf_at(atom, tp.nsp, x)
case _:
assert False, tp.nsp
def pseudo_sgn_rem(g: Term, prd: PRD, x: Variable) -> Term:
"""Sign-corrected pseudo-remainder
"""
f = prd.term
if g.degree(x) < f.degree(x):
return g
_, h = g.pseudo_quo_rem(f, x)
delta = g.degree(x) - f.degree(x) + 1
if delta % 2 == 1:
lc_signs = set(root_spec.signs[-1] for root_spec in prd.cluster)
if len(lc_signs) == 1:
lc_sign = next(iter(lc_signs))
assert lc_sign in (-1, 1)
if lc_sign == -1:
h = - h
else:
# Since there are no assumptions, we need not worry about
# f_lc == 0. We currently believe that otherwise the guard
# takes care that parametric f_lc cannot vanish.
f_lc = f.coefficient({x: f.degree(x)})
if is_valid(f_lc >= 0):
pass
elif is_valid(f_lc <= 0):
h = - h
else:
h *= f_lc
# One could check for even powers of f_lc in h. Currently, the
# simplifier takes care of this.
return h
def vs_prd_at(atom: AtomicFormula, prd: PRD, x: Variable) -> Formula:
"""Virtually substitute a parametric root description into an atom.
"""
return prd.vsubs(atom)
def vs_inf_at(atom: AtomicFormula, nsp: NSP, x: Variable) -> Formula:
"""Virtually substitute ±∞ into an atom
"""
assert nsp in (NSP.PLUS_INFINITY, NSP.MINUS_INFINITY), nsp
match atom:
case Eq() | Ne():
return tau(atom, x)
case Le() | Lt() | Ge() | Gt():
c = atom.lhs.coefficient({x: 0})
mu: Formula = atom.op(c, 0)
for e in range(1, atom.lhs.degree(x) + 1):
c = atom.lhs.coefficient({x: e})
if nsp == NSP.MINUS_INFINITY and e % 2 == 1:
c = - c
mu = Or(atom.op.strict_part()(c, 0), And(Eq(c, 0), mu))
return mu
case _:
assert False, atom
def expand_eps_at(atom: AtomicFormula, nsp: NSP, x: Variable) -> Formula:
"""Reduce virtual substitution of a parametric root description ±ε
to virtual substitution of a parametric root description.
"""
assert nsp in (NSP.PLUS_EPSILON, NSP.MINUS_EPSILON), nsp
match atom:
case Eq() | Ne():
return tau(atom, x)
case Le() | Lt() | Ge() | Gt():
return nu(atom, nsp, x)
case _:
assert False, atom
def nu(atom: AtomicFormula, nsp: NSP, x: Variable) -> Formula:
"""Recursion on the vanishing of derivatives
"""
if atom.lhs.degree(x) <= 0:
return atom
lhs_prime = atom.lhs.derivative(x)
if nsp == NSP.MINUS_EPSILON:
lhs_prime = - lhs_prime
atom_strict = atom.op.strict_part()(atom.lhs, 0)
atom_prime = atom.op(lhs_prime, 0)
return Or(atom_strict, And(Eq(atom.lhs, 0), nu(atom_prime, nsp, x)))
def tau(atom: AtomicFormula, x: Variable) -> Formula:
"""Virtually substitute a transcendental element into an equation
or inequation.
"""
args: list[AtomicFormula] = []
match atom:
case Eq():
for e in range(atom.lhs.degree(x) + 1):
c = atom.lhs.coefficient({x: e})
if c.is_zero():
continue
if c.is_constant():
return _F()
args.append(Eq(c, 0))
return And(*args)
case Ne():
for e in range(atom.lhs.degree(x) + 1):
c = atom.lhs.coefficient({x: e})
if c.is_zero():
continue
if c.is_constant():
return _T()
args.append(Ne(c, 0))
return Or(*args)
case _:
assert False, atom
variables = self.variables
x = eset.variable
new_nodes = []
for tp in eset.test_points:
new_formula = self.formula.transform_atoms(lambda atom: vs_at(atom, tp, x))
# requires discussion: guard will be simplified twice
new_formula = simplify(And(tp.guard(assumptions), new_formula), assume=assumptions.atoms)
if new_formula is _T():
raise abc.qe.FoundT()
new_nodes.append(
Node(variables=variables.copy(),
formula=new_formula,
answer=[],
outermost_block=self.outermost_block,
options=self.options))
return new_nodes
[docs]
@dataclass
class Options(abc.qe.Options):
"""The options specified here, as well as the options inherited from
:class:`.abc.qe.Options`, can be passed to the callable class
:class:`.VirtualSubstitution` as keyword arguments.
Required by :class:`.VirtualSubstitution` for instantiating the type
variable :data:`.abc.qe.ω` of :class:`.abc.qe.QuantifierElimination`.
"""
clustering: CLUSTERING = CLUSTERING.FULL
"""The clustering strategy used by :class:`.VirtualSubstitution`. See
[Kosta-2016]_ for details on clustering.
"""
generic: GENERIC = GENERIC.NONE
"""The degree of genericity used by :class:`.VirtualSubstitution`. See
[DolzmannSturmWeispfenning-1998]_, [Sturm-1999]_ for details on generic
quantifier elimination.
>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> qe(Ex(x, (a**2 - 2) * x**2 + b * x + c == 0),
... assume=[c > 0])
Or(And(b != 0, a^2 - 2 == 0),
And(a^2 - 2 != 0, 4*a^2*c - b^2 - 8*c <= 0))
>>> qe.assumptions
[c > 0]
>>> qe(Ex(x, (a**2 - 2) * x**2 + b * x + c == 0),
... assume=[c > 0], generic=GENERIC.FULL)
4*a^2*c - b^2 - 8*c <= 0
>>> qe.assumptions
[c > 0, a^2 - 2 != 0]
>>> qe(Ex(x, (a**2 - 2) * x**2 + b * x + c == 0),
... assume=[c > 0], generic=GENERIC.MONOMIAL)
Or(a^2 - 2 == 0, 4*a^2*c - b^2 - 8*c <= 0)
>>> qe.assumptions
[c > 0, b != 0]
"""
traditional_guards: bool = True
"""`traditional_guards=False` strictly follows the construction of guards
as described in [Kosta-2016]_.
>>> from logic1.firstorder import *
>>> from logic1.theories.RCF import *
>>> a, b, c, x = VV.get('a', 'b', 'c', 'x')
>>> qe(Ex(x, a * x**2 + b * x + c == 0))
Or(And(c == 0, b == 0, a == 0),
And(b != 0, a == 0),
And(a != 0, 4*a*c - b^2 <= 0))
>>> qe(Ex(x, a * x**2 + b * x + c == 0), traditional_guards=False)
Or(And(c == 0, b == 0, a == 0),
And(b != 0, Or(c == 0, a == 0)),
And(a != 0, 4*a*c - b^2 <= 0))
"""
[docs]
@dataclass
class VirtualSubstitution(abc.qe.QuantifierElimination[
Node, Assumptions, list[str], Options, AtomicFormula, Term, Variable, int]):
"""Real quantifier elimination by virtual substitution.
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) -> Options:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.create_options`.
"""
return 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
return [Node(variables=list(variables),
formula=simplify(matrix, assume=self._assumptions.atoms),
answer=[],
outermost_block=not self.blocks,
options=self.options)]
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(),
answer=[],
outermost_block=False,
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, ring_vars: list[str]):
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.init_env`.
"""
polynomial_ring.ensure_vars(ring_vars)
def init_env_arg(self) -> list[str]:
"""Implements the abstract method :meth:`.abc.qe.QuantifierElimination.init_env_arg`.
"""
# We pass the ring variables to the workers. The workers
# reconstruct the ring.
return [str(v) for v in polynomial_ring.get_vars()]
qe = virtual_substitution = VirtualSubstitution()
"""
Real quantifier elimination by virtual substitution. The implementation
essentially follows [Kosta-2016]_ up to degree two. It also offers generic
quantifier elimination [DolzmannSturmWeispfenning-1998]_, [Sturm-1999]_.
Technically, :func:`.qe` is an instance of the callable class
:class:`.VirtualSubstitution`.
:param f:
The input formula to which quantifier elimination will be applied.
:param assume:
A list of atomic formulas that are assumed to hold. The return value
is equivalent modulo those assumptions.
:param 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.
:param `**options`:
Keyword arguments with keywords corresponding to attributes of
:class:`.Options`. Those are :attr:`.clustering`, :attr:`.generic`,
:attr:`.log_level`, :attr:`.log_rate`, :attr:`.traditional_guards`.
:returns:
A quantifier-free equivalent of `f` modulo assumptions that are available in
:attr:`qe.assumptions <.abc.qe.QuantifierElimination.assumptions>` at the end of
the computation. With regular quantifier elimination, the assumptions are
those passed as the `assume` parameter, modulo simplification. With
*generic quantifier elimination*, inequations in the parameters can be
added in the course of the elimination. See :attr:`.Options.generic` for
examples.
"""