Class QueryProposition

    • Constructor Detail

      • QueryProposition

        public QueryProposition​(FolFormula formula,
                                java.lang.String name)
        Creates a new query proposition with the given formula and a unique name, which is used by the base class.
        Parameters:
        formula - a state formula.
        name - a unique name.
    • Method Detail

      • getInnerFormula

        public FolFormula getInnerFormula()
        Returns the inner formula of this query proposition, e.g. "F" in the case of a holds F proposition.
        Returns:
        the inner formula of this query proposition
      • getActionSignature

        public ActionSignature getActionSignature()
        Returns a new action signature containing all symbols of the inner formula of this proposition.
        Returns:
        a new action signature containing all symbols of the inner formula of this proposition.
      • getInnerActions

        public abstract java.util.Set<FolAction> getInnerActions()
        Returns the set of all actions contained in this query proposition. This is mainly a convenience function, as only necessarily propositions contain any actions.
        Returns:
        the set of all actions contained in this query proposition.
      • substitute

        public abstract QueryProposition substitute​(java.util.Map<? extends Term<?>,​? extends Term<?>> map)
        Returns a new query proposition of the same type, in which all variables in inner formulas and actions are replaced according to the given map.
        Parameters:
        map - a map from variables to constants.
        Returns:
        a new query proposition.
      • toString

        public abstract java.lang.String toString()
        Overrides:
        toString in class Proposition
      • getVariables

        public abstract java.util.Set<Variable> getVariables()
        Returns all variables occuring in inner formulas and actions of this query proposition.
        Returns:
        all variables occuring in inner formulas and actions of this query proposition.