Interface QuantifiedFormula

    • Method Detail

      • getQuantifierVariables

        java.util.Set<Variable> getQuantifierVariables()
        Returns:
        a set containing all quantified variables
      • getUnboundVariables

        java.util.Set<Variable> getUnboundVariables()
        Returns:
        a set of of unbound variables
      • containsQuantifier

        boolean containsQuantifier()
        Checks whether this formula contains any quantification.
        Returns:
        "true" if this formula contains a quantification.
      • isWellBound

        boolean isWellBound()
        Checks whether this formula is well-bound, i.e. whether no variable bound by a quantifier is again bound by another quantifier within the first quantifier's range.
        Returns:
        "true" if this formula is well-bound, "false" otherwise.
      • isWellBound

        boolean isWellBound​(java.util.Set<Variable> boundVariables)
        Checks whether this formula is well-bound, i.e. whether no variable bound by a quantifier is again bound by another quantifier within the first quantifier range. Every variable in "boundVariables" is assumed to be bound already.
        Parameters:
        boundVariables - the variables assumed to be bound.
        Returns:
        "true" if this formula is well-bound, "false" otherwise.
      • isClosed

        boolean isClosed()
        Checks whether this formula is closed, i.e. whether every variables occurring in the formula is bound by a quantifier.
        Returns:
        "true" if this formula is closed, "false" otherwise.
      • isClosed

        boolean isClosed​(java.util.Set<Variable> boundVariables)
        Checks whether this formula is closed, i.e. whether every variables occurring in the formula is bound by a quantifier. Every variable in "boundVariables" is already assumed to be bound.
        Parameters:
        boundVariables - the variables assumed to be bound.
        Returns:
        "true" if this formula is closed wrt. "boundVariables", "false" otherwise.