Class Sort

  • All Implemented Interfaces:
    LogicStructure

    public class Sort
    extends java.lang.Object
    implements LogicStructure
    A sort of first-order logic. i.e. a set of constant objects and a set of variables that represent constants of this sort. Note: The sort names "Thing" and "_Any" are reserved for the default sort and for the sort that represents all sorts. They should not be used when creating new sorts.
    Author:
    Matthias Thimm, Tim Janus, Anna Gessler
    • Field Summary

      Fields 
      Modifier and Type Field Description
      static Sort ANY
      Default sort for terms of equality/inequality predicates.
      static Sort THING
      Default sort for unsorted first-order logics
    • Constructor Summary

      Constructors 
      Constructor Description
      Sort​(java.lang.String name)
      Ctor: Creates an empty Sort with the given name.
      Sort​(java.lang.String name, java.util.Set<Constant> constants)
      Ctor: Creates a Sort with the given name and the given constants.
      Sort​(Sort other)
      Copy-Ctor creates a deep copy of the Sort
    • Method Summary

      Modifier and Type Method Description
      void add​(Term<?> term)
      Adds the given term to this sort.
      Sort clone()  
      <C extends Term<?>>
      boolean
      containsTermsOfType​(java.lang.Class<C> cls)
      Checks if this logical structure contains at least one term of type C.
      boolean equals​(java.lang.Object obj)  
      java.lang.String getName()  
      java.util.Set<Term<?>> getTerms()  
      <C extends Term<?>>
      java.util.Set<C>
      getTerms​(java.lang.Class<C> cls)
      Processes the set containing all terms of type C.
      int hashCode()  
      boolean remove​(Term<?> term)
      Removes the given term from this sort.
      static java.util.Map<Sort,​java.util.Set<Term<?>>> sortTerms​(java.util.Collection<? extends Term<?>> terms)
      Sorts the set of given terms by their sorts, i.e.
      java.lang.String toString()  
      • Methods inherited from class java.lang.Object

        getClass, notify, notifyAll, wait, wait, wait
    • Field Detail

      • THING

        public static final Sort THING
        Default sort for unsorted first-order logics
      • ANY

        public static final Sort ANY
        Default sort for terms of equality/inequality predicates. Note: This sort is always equal to any other sort.
    • Constructor Detail

      • Sort

        public Sort​(java.lang.String name)
        Ctor: Creates an empty Sort with the given name.
        Parameters:
        name - The name of the Sort
      • Sort

        public Sort​(java.lang.String name,
                    java.util.Set<Constant> constants)
        Ctor: Creates a Sort with the given name and the given constants.
        Parameters:
        name - The name of the Sort
        constants - A set of constants which are members of the sort.
      • Sort

        public Sort​(Sort other)
        Copy-Ctor creates a deep copy of the Sort
        Parameters:
        other - The Sort that acts as copy source
    • Method Detail

      • sortTerms

        public static java.util.Map<Sort,​java.util.Set<Term<?>>> sortTerms​(java.util.Collection<? extends Term<?>> terms)
        Sorts the set of given terms by their sorts, i.e. the set of terms is partitioned wrt. their sorts and set as value of the sort's key.
        Parameters:
        terms - a set of terms.
        Returns:
        a map which maps from sorts to terms of their sort.
      • add

        public void add​(Term<?> term)
        Adds the given term to this sort.
        Parameters:
        term - some term
      • remove

        public boolean remove​(Term<?> term)
        Removes the given term from this sort.
        Parameters:
        term - a term, either a variable or a constant.
        Returns:
        "true" if the given term has actually been removed.
      • getName

        public java.lang.String getName()
      • toString

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

        public int hashCode()
        Overrides:
        hashCode in class java.lang.Object
      • equals

        public boolean equals​(java.lang.Object obj)
        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
      • 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.
      • clone

        public Sort clone()