Module src.olaaaf.formula.unaryFormula.notOperator

Class representing the Not operator.

Classes

class Not (formulaInit: Formula, fmName: str = None)

Class representing the Not operator.

Attributes

children : olaaaf.formula.formula.Formula
The child of the current node.
Expand source code 
class Not(UnaryFormula):
    '''
    Class representing the Not operator.

    Attributes
    ----------
    children: `olaaaf.formula.formula.Formula`
        The child of the current node.
    '''
        
    def toDNF(self) -> Formula:
        '''
        Method returning the current Formula in Disjunctive Normal Form.

        Returns
        -------
        `olaaaf.formula.formula.Formula`
            The current `olaaaf.formula.formula.Formula` in Disjunctive Normal Form.
        '''
        
        return self.children._toDNFNeg()
    
    def _toDNFNeg(self) -> Formula:
        '''
        Protected method used in the algorithm to recursivly determine the
        Disjunctive Normal Form, used when a Negation is in play instead of toDNF().

        Returns
        -------
        `olaaaf.formula.formula.Formula`
            The current `olaaaf.formula.formula.Formula` in Disjunctive Normal Form.
        '''
        
        return self.children.toDNF()
    
    def getAdherence(self, var : Variable = None) -> list[list[Constraint]]:
        '''
        Returns a 2D list containing all the constraints of the adherence of 
        the Formula, in Disjunctive Normal Form.

        Attributes
        ----------
        var : olaaaf.variable.variable.Variable
            variable used in case of inequality.

        Returns
        -------
        list of list of olaaaf.formula.nullaryFormula.constraint.constraint.Constraint
            2D list containing all the constraints of discute vraiment de l'implémentationthe adherence of the Formula,
            in Disjunctive Normal Form.
        '''
        
        return self.children._getAdherenceNeg(var)
    
    def _getAdherenceNeg(self, var : Variable = None)  -> list[list[Constraint]]:
        '''
        Protected method used in the algorithm to recursivly determine the
        constraints of the adherence of the Formula, used when a Negation is in play
        instead of getAdherence().

        Attributes
        ----------
        var : olaaaf.variable.variable.Variable
            variable used in case of inequality.

        Returns
        -------
        list of list of olaaaf.formula.nullaryFormula.constraint.constraint.Constraint
            2D list containing all the constraints of the adherence of the Formula,
            in Disjunctive Normal Form under Negation.
        '''
        
        return self.children.getAdherence(var)
    
    def toLessOrEqConstraint(self):
        '''
        Method used to transform a `olaaaf.formula.formula.Formula` into another one, with only `olaaaf.formula.nullaryFormula.constraint.constraintOperator.ConstraintOperator.LEQ` constraints.

        Returns
        ------
        `olaaaf.formula.formula.Formula`
            A `olaaaf.formula.formula.Formula` with only `olaaaf.formula.nullaryFormula.constraint.constraintOperator.ConstraintOperator.LEQ` constraints.
        '''
        return Not(self.children.toLessOrEqConstraint())
    
    def copyNegLitteral(self, epsilon = Fraction(0)) -> Constraint:
        """
        Method used to transform the strict operators (i.e the negation) in an open one.

        Parameters
        ----------
        epsilon : Fraction, optional
            The approximation for the removed Not. By default, equals \(0\).

        Returns
        -------
        olaaaf.formula.nullaryFormula.constraint.constraint.Constraint
            The transformed `olaaaf.formula.nullaryFormula.constraint.constraint.Constraint`
        """
        
        if not isinstance(self.children, Constraint):
            raise TypeError("This method can only be called on a litteral")
                
        copyNeg = self.children.clone()

        for key in copyNeg.variables:
            copyNeg.variables[key] = -copyNeg.variables[key]
        copyNeg.bound = -(copyNeg.bound + epsilon)
                
        return copyNeg
    
    def toPCMLC(self, varDict) -> Formula:
        '''
        Method used to transform a `olaaaf.formula.formula.Formula` into a new one, in the PCMLC formalism.

        Parameters
        ----------
        varDict : dictionnary
            Dictionnary used to tell which variable should be replaced by which.

        Returns
        -------
        `olaaaf.formula.formula.Formula`
            A `olaaaf.formula.formula.Formula` in the PCMLC formalism.
        '''
        return self.children._toPCMLCNeg(varDict)
    
    def _toPCMLCNeg(self, varDict) -> Formula:
        '''
        Method used to transform a `olaaaf.formula.formula.Formula` into a new one, in the PCMLC formalism.

        Parameters
        ----------
        varDict : dictionnary
            Dictionnary used to tell which variable should be replaced by which.

        Returns
        -------
        `olaaaf.formula.formula.Formula`
            A `olaaaf.formula.formula.Formula` in the PCMLC formalism.
        '''
        return self.children.toPCMLC(varDict)

    def _getBranches(self):
        '''
        Method used to get the branches of the analytic tableau representing the `olaaaf.formula.formula.Formula`,
        automatically removing any closed one once it's caught. 

        Returns
        ------
        `list[dict[Constraint, bool]]`
            A list of all branches, represented by a dictionnary matching every atom
            `olaaaf.formula.nullaryFormula.constraint.constraint.Constraint` to a `bool` representing if it has a negation (`False`)
            or not (`True`).
            If all branches are closed, return `None`.
        '''

        return self.children._getBranchesNeg()

    def _getBranchesNeg(self):
        '''
        Method used to get the branches of the analytic tableau representing the `olaaaf.formula.formula.Formula`,
        automatically removing any closed one once it's caught. 
        Used when a Negation is in play instead of `_getBranches()`.

        Returns
        ------
        `list[dict[Constraint, bool]]`
            A list of all branches, represented by a dictionnary matching every atom
            `olaaaf.formula.nullaryFormula.constraint.constraint.Constraint` to a `bool` representing if it has a negation (`False`)
            or not (`True`).
            If all branches are closed, return `None`.
        '''
        
        return self.children._getBranches()

    def __str__(self):
        return Constants.NOT_STRING_OPERATOR + "(" + str(self.children) + ")"
    
    def toLatex(self):
        r"""
        Method returning a \(\LaTeX\) expression representing the Formula. Operators are customisable in `olaaaf.constants.Constants`.
        
        Returns
        -------
        String
            The \(\LaTeX\) expression representing the Formula.
        """

        return Constants.NOT_LATEX_OPERATOR + "(" + self.children.toLatex + ")"

Ancestors

Methods

def copyNegLitteral(self, epsilon=Fraction(0, 1)) ‑> Constraint

Method used to transform the strict operators (i.e the negation) in an open one.

Parameters

epsilon : Fraction, optional
The approximation for the removed Not. By default, equals 0.

Returns

olaaaf.formula.nullaryFormula.constraint.constraint.Constraint
The transformed olaaaf.formula.nullaryFormula.constraint.constraint.Constraint
def getAdherence(self, var: Variable = None) ‑> list[list[Constraint]]

Returns a 2D list containing all the constraints of the adherence of the Formula, in Disjunctive Normal Form.

Attributes

var : olaaaf.variable.variable.Variable
variable used in case of inequality.

Returns

list of list of olaaaf.formula.nullaryFormula.constraint.constraint.Constraint
2D list containing all the constraints of discute vraiment de l'implémentationthe adherence of the Formula, in Disjunctive Normal Form.

Inherited members