Class FolFormula

    • Constructor Detail

      • FolFormula

        public FolFormula()
    • Method Detail

      • getQuantifierVariables

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

        public FolFormula toDnf()
        Makes a disjunctive normal form of this formula.
        Returns:
        the DNF of this formula
      • toNnf

        public abstract FolFormula toNnf()
        Makes the negation normal form of this formula.
        Returns:
        the NNF of this formula
      • collapseAssociativeFormulas

        public abstract RelationalFormula collapseAssociativeFormulas()
        This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.
        Returns:
        the collapsed formula.
      • isDnf

        public abstract boolean isDnf()
        Checks whether this formula is in disjunctive normal form.
        Returns:
        "true" iff this formula is in disjunctive normal form.
      • substitute

        public abstract FolFormula substitute​(Term<?> v,
                                              Term<?> t)
                                       throws java.lang.IllegalArgumentException
        Description copied from class: RelationalFormula
        Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula. NOTE: if "v" is a variable and bound to a quantifier then "v" is not substituted in that quantifiers inner formula.
        Specified by:
        substitute in interface ComplexLogicalFormula
        Specified by:
        substitute in class RelationalFormula
        Parameters:
        v - the term to be substituted.
        t - the term to substitute.
        Returns:
        a formula where every occurrence of "v" is replaced by "t".
        Throws:
        java.lang.IllegalArgumentException - if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).
      • getSignature

        public FolSignature getSignature()
        Description copied from interface: Formula
        Returns the signature of the language of this formula.
        Returns:
        the signature of the language of this formula.