Class RelationalFormula

    • Constructor Detail

      • RelationalFormula

        public RelationalFormula()
    • Method Detail

      • getAtoms

        public abstract java.util.Set<? extends Atom> getAtoms()
        Description copied from interface: SimpleLogicalFormula
        Processes the set of all atoms which appear in this formula
        Specified by:
        getAtoms in interface SimpleLogicalFormula
        Returns:
        all atoms that appear in this formula.
      • getFunctors

        public abstract java.util.Set<Functor> getFunctors()
        Returns:
        all functors that appear in this formula.
      • substitute

        public abstract RelationalFormula substitute​(Term<?> v,
                                                     Term<?> t)
                                              throws java.lang.IllegalArgumentException
        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
        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).
      • substitute

        public RelationalFormula substitute​(java.util.Map<? extends Term<?>,​? extends Term<?>> map)
                                     throws java.lang.IllegalArgumentException
        Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.
        NOTE: variables bound to quantifiers are not substituted in their inner formulas even if they appear in the map.
        Specified by:
        substitute in interface ComplexLogicalFormula
        Parameters:
        map - a mapping defining which terms to be substituted.
        Returns:
        a formula where every term in map.keyset() has been replaced by map.get(v).
        Throws:
        java.lang.IllegalArgumentException - if any term and its mapping are of different sorts (NOTE: this exception is only thrown when the variable actually appears in this formula).
      • exchange

        public RelationalFormula exchange​(Term<?> v,
                                          Term<?> t)
                                   throws java.lang.IllegalArgumentException
        Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually 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:
        exchange in interface ComplexLogicalFormula
        Parameters:
        v - a term.
        t - a term.
        Returns:
        a new relational formula with both "v" and "t" exchanged.
        Throws:
        java.lang.IllegalArgumentException - if "v" and "t" are of different sorts
      • allSubstitutions

        public java.util.Set<java.util.Map<Variable,​Term<?>>> allSubstitutions​(java.util.Collection<? extends Term<?>> terms)
                                                                              throws java.lang.IllegalArgumentException
        Computes all possible substitutions, i.e. maps from variables to terms, of unbound variables of this formula to terms in "terms".
        Parameters:
        terms - a set of terms.
        Returns:
        a set of maps from variables to terms.
        Throws:
        java.lang.IllegalArgumentException - if there is an unbound variable in this formula for which there is no term in "terms" with the same sort.
      • allGroundInstances

        public java.util.Set<RelationalFormula> allGroundInstances​(java.util.Set<Constant> constants)
                                                            throws java.lang.IllegalArgumentException
        Computes all ground instances of this relational formula wrt. the given set of constants, i.e. every formula where each occurrence of some unbound variable is replaced by some constant.
        Parameters:
        constants - a set of constants
        Returns:
        a set of ground instances of this formula
        Throws:
        java.lang.IllegalArgumentException - if there is an unbound variable in this formula for which there is no constant in "constants" with the same sort.
      • getSatisfactionRatio

        public double getSatisfactionRatio()
        Returns the ratio of worlds not satisfying this formula to worlds satisfying this formula.
        Returns:
        the ratio of worlds not satisfying this formula to worlds satisfying this formula.
      • isGround

        public boolean isGround()
        Checks whether this formula is ground, i.e. whether there appears no variable in this formula.
        Specified by:
        isGround in interface ComplexLogicalFormula
        Returns:
        "true" if this formula is ground.
      • isWellFormed

        public boolean isWellFormed()
        Tests whether this formula is well-formed, i.e. whether
        - there are no two variables with the same name but different sort
        - there are no two constants with the same name but different sort
        - there are no two predicates with the same name but different arguments
        - there are no two functors with the same name but different sort or arguments
        - every atom is complete, i.e. has a complete list of arguments
        - every functional term is complete, i.e. has a complete list of arguments
        - no variable bound by a quantifier is again bound by another quantifier within the first quantifier range.
        - every functor has arity greater zero (otherwise it should be modeled by a constant
        Specified by:
        isWellFormed in interface ComplexLogicalFormula
        Returns:
        "true" if this formula is well-formed
      • containsTermsOfType

        public <C extends Term<?>> boolean containsTermsOfType​(java.lang.Class<C> cls)
        Description copied from interface: LogicStructure
        Checks if this logical structure contains at least one term of type C. This method is a shortcut for !getTerms(TermImplementation.class).isEmpty().
        Specified by:
        containsTermsOfType in interface LogicStructure
        Type Parameters:
        C - the type of terms
        Parameters:
        cls - The class structure representing the type C of the term.
        Returns:
        True if this logical structure contains at least one term of type C or false otherwise.
      • combineWithOr

        public abstract Conjunctable combineWithOr​(Disjunctable f)
        Specified by:
        combineWithOr in interface Disjunctable
        Parameters:
        f - a formula to be combined with OR and this.
        Returns:
        a disjunction of this and the given formula.
      • combineWithAnd

        public abstract Disjunctable combineWithAnd​(Conjunctable f)
        Description copied from interface: Conjunctable
        Returns a conjunction of this and the given formula.
        Specified by:
        combineWithAnd in interface Conjunctable
        Parameters:
        f - a formula to be combined with AND and this.
        Returns:
        a conjunction of this and the given formula.
      • toString

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