Class FolAtom

    • Constructor Detail

      • FolAtom

        public FolAtom()
        Default-Ctor: Creates new empty FOL-Atom
      • FolAtom

        public FolAtom​(Predicate predicate)
        Creates a new atom with the given predicate and initializes an empty argument list.
        Parameters:
        predicate - the predicate of the atom.
      • FolAtom

        public FolAtom​(Predicate predicate,
                       Term<?>... terms)
      • FolAtom

        public FolAtom​(Predicate predicate,
                       java.util.List<? extends Term<?>> arguments)
        Creates a new atom with the given predicate and list of terms
        Parameters:
        predicate - the predicate of the atom
        arguments - the arguments (terms) of the atom
      • FolAtom

        public FolAtom​(FolAtom other)
    • Method Detail

      • addArgument

        public void addArgument​(Term<?> term)
                         throws java.lang.IllegalArgumentException
        Appends the given argument to this atom's arguments and returns itself.
        Specified by:
        addArgument in interface Atom
        Parameters:
        term - an argument to be added
        Throws:
        java.lang.IllegalArgumentException - if the given term does not correspond to the expected sort or the argument list is complete.
      • substitute

        public FolAtom 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 FolFormula
        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).
      • isComplete

        public boolean isComplete()
        Checks whether this atom is complete, i.e. whether every argument is set.
        Specified by:
        isComplete in interface Atom
        Returns:
        "true" if the atom is complete.
      • isClosed

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

        public boolean isClosed​(java.util.Set<Variable> boundVariables)
        Description copied from interface: QuantifiedFormula
        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.
        Specified by:
        isClosed in interface QuantifiedFormula
        Parameters:
        boundVariables - the variables assumed to be bound.
        Returns:
        "true" if this formula is closed wrt. "boundVariables", "false" otherwise.
      • isWellBound

        public boolean isWellBound()
        Description copied from interface: QuantifiedFormula
        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.
        Specified by:
        isWellBound in interface QuantifiedFormula
        Returns:
        "true" if this formula is well-bound, "false" otherwise.
      • isWellBound

        public boolean isWellBound​(java.util.Set<Variable> boundVariables)
        Description copied from interface: QuantifiedFormula
        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.
        Specified by:
        isWellBound in interface QuantifiedFormula
        Parameters:
        boundVariables - the variables assumed to be bound.
        Returns:
        "true" if this formula is well-bound, "false" otherwise.
      • containsQuantifier

        public boolean containsQuantifier()
        Description copied from interface: QuantifiedFormula
        Checks whether this formula contains any quantification.
        Specified by:
        containsQuantifier in interface QuantifiedFormula
        Returns:
        "true" if this formula contains a quantification.
      • getPredicate

        public Predicate getPredicate()
        Returns the predicate of this atom
        Specified by:
        getPredicate in interface Atom
        Returns:
        the predicate of this atom
      • getArguments

        public java.util.List<Term<?>> getArguments()
        Specified by:
        getArguments in interface Atom
        Returns:
        the arguments of this atom.
      • isDnf

        public boolean isDnf()
        Description copied from class: FolFormula
        Checks whether this formula is in disjunctive normal form.
        Specified by:
        isDnf in class FolFormula
        Returns:
        "true" iff this formula is in disjunctive normal form.
      • isLiteral

        public boolean isLiteral()
        Specified by:
        isLiteral in interface SimpleLogicalFormula
        Returns:
        true if the formula represents a literal in the language or false otherwise
      • toNnf

        public FolFormula toNnf()
        Description copied from class: FolFormula
        Makes the negation normal form of this formula.
        Specified by:
        toNnf in class FolFormula
        Returns:
        the NNF of this formula
      • collapseAssociativeFormulas

        public FolFormula collapseAssociativeFormulas()
        Description copied from class: FolFormula
        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 FolFormula
        Returns:
        the collapsed formula.
      • hashCode

        public int hashCode()
        Specified by:
        hashCode in interface SimpleLogicalFormula
        Overrides:
        hashCode in class java.lang.Object
      • equals

        public boolean equals​(java.lang.Object obj)
        Specified by:
        equals in interface SimpleLogicalFormula
        Overrides:
        equals in class java.lang.Object
      • getTerms

        public java.util.Set<Term<?>> getTerms()
        Specified by:
        getTerms in interface LogicStructure
        Returns:
        a set containing all terms of this logical structure
      • getTerms

        public <C extends Term<?>> java.util.Set<C> getTerms​(java.lang.Class<C> cls)
        Description copied from interface: LogicStructure
        Processes the set containing all terms of type C. This method uses the equals method of the given Class and therefore does not add terms which are sub classes of type C to the set.
        Specified by:
        getTerms in interface LogicStructure
        Type Parameters:
        C - the type of terms
        Parameters:
        cls - The Class structure containing type information about the searched term
        Returns:
        A set containing all terms of type C of this logical structure
      • setPredicate

        public Atom.RETURN_SET_PREDICATE setPredicate​(Predicate newer)
        Description copied from interface: Atom
        Changes the predicate of the atom. Given an old Predicate po and a new predicate pn with their list of arguments types at(po) and at(pn) and the arguments of this Atom: arg(this) this method distinguishes between three cases: 1. The predicate only differ in the names, returning RSP_SUCCESS 2. The old predicates argument types is a sub-list of the new argument types then the method returns RSP_INCOMPLETE and the atoms isComplete() method returns false 3. The new predicates argument types is a sub-list of the old argument types then the method returns RSP_TRUNCATED and the arguments of this atom are truncated too and isComplete() returns true. 4. The old and new predicates' argument types differ then the list of arguments of the atom get cleared and isComplete() returns false.
        Specified by:
        setPredicate in interface Atom
        Parameters:
        newer - some predicate
        Returns:
        Depends on the cases described above: 1. RSP_SUCCESS 2. RSP_INCOMPLETE 3. RSP_TRUNCATED 4. RSP_CLEARED
      • getName

        public java.lang.String getName()
        Specified by:
        getName in interface Atom
        Returns:
        the name of the predicate