Class Proposition

    • Constructor Detail

      • Proposition

        public Proposition()
        Default-Ctor for dynamic instantiation
      • Proposition

        public Proposition​(java.lang.String name)
        Creates a new proposition of the given name.
        Parameters:
        name - the name of the proposition.
      • Proposition

        public Proposition​(Proposition other)
    • Method Detail

      • getName

        public java.lang.String getName()
        Specified by:
        getName in interface Atom
        Returns:
        the name of this proposition.
      • toString

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

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

        public PlSignature getSignature()
        Description copied from interface: Formula
        Returns the signature of the language of this formula.
        Specified by:
        getSignature in interface Formula
        Overrides:
        getSignature in class PlFormula
        Returns:
        the signature of the language of this formula.
      • toNnf

        public PlFormula toNnf()
        Description copied from class: PlFormula
        This method returns this formula in negation normal form (NNF). A formula is in NNF iff negations occur only directly in front of a proposition.
        Specified by:
        toNnf in class PlFormula
        Returns:
        the formula in NNF.
      • trim

        public PlFormula trim()
        Description copied from class: PlFormula
        Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations. Simplifies equivalences and implications with equivalent formulas (A=>A, A<=>A) to tautologies.
        Specified by:
        trim in class PlFormula
        Returns:
        an equivalent formula without duplicates.
      • addArgument

        public void addArgument​(Term<?> arg)
        Description copied from interface: Atom
        Adds an argument to the atom's argument list
        Specified by:
        addArgument in interface Atom
        Parameters:
        arg - The next argument
      • getArguments

        public java.util.List<? extends Term<?>> getArguments()
        Specified by:
        getArguments in interface Atom
        Returns:
        A list containing all the arguments of this specific atom
      • isComplete

        public boolean isComplete()
        Specified by:
        isComplete in interface Atom
        Returns:
        true if the size of the argument list is equal to the arity of the predicate
      • getLiterals

        public java.util.Set<PlFormula> getLiterals()
        Description copied from class: PlFormula
        Returns all literals, i.e. all formulas of the form "a" or "!a" where "a" is a proposition, that appear in this formula.
        Specified by:
        getLiterals in class PlFormula
        Returns:
        all literals appearing in this formula.
      • setPredicate

        public Atom.RETURN_SET_PREDICATE setPredicate​(Predicate predicate)
        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:
        predicate - some predicate
        Returns:
        Depends on the cases described above: 1. RSP_SUCCESS 2. RSP_INCOMPLETE 3. RSP_TRUNCATED 4. RSP_CLEARED
      • compareTo

        public int compareTo​(Proposition o)
        Specified by:
        compareTo in interface java.lang.Comparable<Proposition>
      • toCnf

        public Conjunction toCnf()
        Description copied from class: PlFormula
        This method returns this formula in conjunctive normal form (CNF). A formula is in CNF iff it is a conjunction of disjunctions and in NNF. The CNF generated by this method is not necessarily minimal.
        Specified by:
        toCnf in class PlFormula
        Returns:
        the formula in CNF.
      • numberOfOccurrences

        public int numberOfOccurrences​(Proposition p)
        Description copied from class: PlFormula
        Returns the number of occurrences of the given proposition within this formula
        Specified by:
        numberOfOccurrences in class PlFormula
        Parameters:
        p - some proposition
        Returns:
        the number of occurrences of the given proposition within this formula
      • replace

        public PlFormula replace​(Proposition p,
                                 PlFormula f,
                                 int i)
        Description copied from class: PlFormula
        Replaces the ith instance of the proposition p by f.
        Specified by:
        replace in class PlFormula
        Parameters:
        p - some proposition
        f - some formula
        i - the index of the proposition
        Returns:
        a new formula with the ith instance of the proposition p replaced by f.
      • getModels

        public java.util.Set<PossibleWorld> getModels​(PlSignature sig)
        Description copied from class: PlFormula
        Returns the set of models of this formula wrt. the given signature.
        Specified by:
        getModels in class PlFormula
        Parameters:
        sig - some propositional signature
        Returns:
        the set of models of this formula wrt. the given signature.