Class ForallQuantifiedFormula

    • Constructor Detail

      • ForallQuantifiedFormula

        public ForallQuantifiedFormula​(PlFormula f,
                                       java.util.Set<Proposition> variables)
        Create a new universal boolean quantification.
        Parameters:
        f - inner formula
        variables - quantifier variables
      • ForallQuantifiedFormula

        public ForallQuantifiedFormula​(PlFormula f,
                                       Proposition variable)
        Create a new universal boolean quantification.
        Parameters:
        f - inner formula
        variable - quantifier variable
      • ForallQuantifiedFormula

        public ForallQuantifiedFormula​(ForallQuantifiedFormula other)
        Create a new existential boolean quantification.
        Parameters:
        other - other universal quantified formula
    • Method Detail

      • getQuantifierVariables

        public java.util.Set<Proposition> getQuantifierVariables()
        Returns:
        the quantified variables (propositions)
      • getFormula

        public PlFormula getFormula()
        Returns:
        the quantified formula
      • getLiterals

        public java.util.Set<PlFormula> getLiterals()
        Description copied from class: PlFormula
        Returns all literals, i.e. all formulas of the form "a" or "!a" where "a" is a proposition, that appear in this formula.
        Specified by:
        getLiterals in class PlFormula
        Returns:
        all literals appearing in this formula.
      • collapseAssociativeFormulas

        public PlFormula collapseAssociativeFormulas()
        Description copied from class: PlFormula
        This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.
        Specified by:
        collapseAssociativeFormulas in class PlFormula
        Returns:
        the collapsed formula.
      • trim

        public PlFormula trim()
        Description copied from class: PlFormula
        Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations. Simplifies equivalences and implications with equivalent formulas (A=>A, A<=>A) to tautologies.
        Specified by:
        trim in class PlFormula
        Returns:
        an equivalent formula without duplicates.
      • toNnf

        public PlFormula toNnf()
        Description copied from class: PlFormula
        This method returns this formula in negation normal form (NNF). A formula is in NNF iff negations occur only directly in front of a proposition.
        Specified by:
        toNnf in class PlFormula
        Returns:
        the formula in NNF.
      • toCnf

        public Conjunction toCnf()
        In this case, this method returns this quantified boolean formula's cnf kernel.
        Specified by:
        toCnf in class PlFormula
        Returns:
        the formula in CNF.
      • getModels

        public java.util.Set<PossibleWorld> getModels​(PlSignature sig)
        Description copied from class: PlFormula
        Returns the set of models of this formula wrt. the given signature.
        Specified by:
        getModels in class PlFormula
        Parameters:
        sig - some propositional signature
        Returns:
        the set of models of this formula wrt. the given signature.
      • numberOfOccurrences

        public int numberOfOccurrences​(Proposition p)
        Description copied from class: PlFormula
        Returns the number of occurrences of the given proposition within this formula
        Specified by:
        numberOfOccurrences in class PlFormula
        Parameters:
        p - some proposition
        Returns:
        the number of occurrences of the given proposition within this formula
      • replace

        public PlFormula replace​(Proposition p,
                                 PlFormula f,
                                 int i)
        Description copied from class: PlFormula
        Replaces the ith instance of the proposition p by f.
        Specified by:
        replace in class PlFormula
        Parameters:
        p - some proposition
        f - some formula
        i - the index of the proposition
        Returns:
        a new formula with the ith instance of the proposition p replaced by f.
      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object
      • getSignature

        public PlSignature getSignature()
        Description copied from interface: Formula
        Returns the signature of the language of this formula.
        Specified by:
        getSignature in interface Formula
        Overrides:
        getSignature in class PlFormula
        Returns:
        the signature of the language of this formula.