Source code for pygplib.absneg
"""Class of abstract logical formula with true/false constants and negation"""
from .absexpr import AbsExpr
from .absexpr import IndexGen
from .baserelst import BaseRelSt
[docs]
class AbsNeg(AbsExpr):
"""Class of abstract expressions with true and false and negation only.
::
Node | self._aux[0] | self._aux[1]
---------------|----------------|--------------
True constant | - | -
False constant | - | -
Attributes:
_NEG: string, representing logical negation.
_TRUE_CONST: string, representing true.
_FALSE_CONST: string, representing false.
_ATOM_TAGS: tuple of strings, representing types of atom.
_BINOP_TAGS: tuple of strings, representing types of binary operator.
_UNOP_TAGS: tuple of strings, representing types of uniary operator.
_EXPR_TAGS: tuple of available tags in this class.
"""
# Tag-related Variables and Methods
_NEG = "~"
_TRUE_CONST = "T"
_FALSE_CONST = "F"
_ATOM_TAGS = AbsExpr._ATOM_TAGS + (_TRUE_CONST, _FALSE_CONST)
_BINOP_TAGS = AbsExpr._BINOP_TAGS
_UNOP_TAGS = (_NEG,)
_EXPR_TAGS = _ATOM_TAGS + _BINOP_TAGS + _UNOP_TAGS
[docs]
@classmethod
def get_neg_tag(cls) -> str:
"""Gets tag of negation."""
return cls._NEG
[docs]
@classmethod
def get_true_const_tag(cls) -> str:
"""Gets tag of true constant."""
return cls._TRUE_CONST
[docs]
@classmethod
def get_false_const_tag(cls) -> str:
"""Gets tag of false constant."""
return cls._FALSE_CONST
# Constructor-related Methods
[docs]
@classmethod
def neg(cls, left: AbsExpr) -> AbsExpr:
"""Gets the formula obtained by applying negation to the operand.
Args:
left: the formula to be negated
"""
return cls(cls._NEG, left)
[docs]
@classmethod
def true_const(cls) -> AbsExpr:
"""Gets the true atom, the atom that always evaluates to true."""
return cls(cls._TRUE_CONST)
[docs]
@classmethod
def false_const(cls) -> AbsExpr:
"""Gets the false atom, the atom that always evaluates to false."""
return cls(cls._FALSE_CONST)
# Instance Methods
[docs]
def is_neg_term(self) -> bool:
"""Is the top-most operator the logical negation ?"""
warn_msg = "`is_neg_term()` has been deprecated and will be removed in v3.0.0"
warnings.warn(warn_msg, UserWarning)
return self.is_neg()
[docs]
def is_neg(self) -> bool:
"""Is the top-most operator the logical negation ?"""
return self.get_tag() == type(self)._NEG
[docs]
def is_true_atom(self) -> bool:
"""Is it the true constant atom ?"""
return self.get_tag() == type(self)._TRUE_CONST
[docs]
def is_false_atom(self) -> bool:
"""Is it the false constant atom ?"""
return self.get_tag() == type(self)._FALSE_CONST
[docs]
def is_const_atom(self) -> bool:
"""Is it either the true constant atom or the false constant atom ?"""
return self.is_true_atom() or self.is_false_atom()
[docs]
def compute_nnf_step(self, negated: bool, s: list[list], t: list[list]) -> None:
"""Perform NNF computation for this object."""
if self.is_neg(): # not not f = f
f = self.get_operand(1)
s.append([not negated, f])
t.append([1, lambda x: x])
return
if self.is_true_atom() or self.is_false_atom():
if negated:
t.append([0, lambda: type(self).neg(self)])
else:
t.append([0, lambda: self])
return
super().compute_nnf_step(negated, s, t)
[docs]
def compute_cnf_step(self, igen: IndexGen, \
assoc: dict, cnf: list) -> None:
"""Performs CNF computation for this object."""
if self.is_neg(): # a <-> -b : (-a or -b) and (a or b)
a = igen.get_next()
b = assoc[id(self.get_operand(1))]
cnf.append((-a, -b))
cnf.append((a, b))
assoc[id(self)] = a
return
assert (
not self.is_true_atom() and not self.is_false_atom()
), "compute_cnf_step() assumes reduced formulas"
super().compute_cnf_step(igen, assoc, cnf)
[docs]
def make_str_pre_step(self) -> str:
"""Makes string in prefix order for this object."""
if self.is_neg():
out = "(" + type(self).get_neg_tag() + " "
return out
if self.is_true_atom():
return type(self).get_true_const_tag()
if self.is_false_atom():
return type(self).get_false_const_tag()
return super().make_str_pre_step()
[docs]
def make_str_in_step(self) -> str:
"""Makes string in infix order for this object."""
if self.is_neg():
return ""
if self.is_true_atom():
return ""
if self.is_false_atom():
return ""
return super().make_str_in_step()
[docs]
def make_str_post_step(self) -> str:
"""Makes string in postfix order for this object."""
if self.is_neg():
return ")"
if self.is_true_atom():
return ""
if self.is_false_atom():
return ""
return super().make_str_post_step()
[docs]
def make_node_str_step(self) -> str:
"""Makes string of this object for DOT print."""
if self.is_neg():
return "NOT"
if self.is_true_atom():
return "T"
if self.is_false_atom():
return "F"
return super().make_node_str_step()