Interface Literal

public interface Literal
The Literal interface represents a logical literal, which can be either a positive or negative proposition. Literals are fundamental components in propositional logic and SAT solvers. They can be used to construct clauses, represent assumptions, and encode constraints.

Author:
Mathias Hofer

  • Method Summary

    Modifier and Type
    Method
    Description
    static Literal
    create()
    Creates a new unnamed atom literal.
    static Literal
    create(String name)
    Creates a new named atom literal with the specified name.
    static Literal
    createTransient()
    Creates a new transient atom literal.
    Literal
    getAtom()
    Retrieves the atom of this literal.
    String
    getName()
    Returns the name of this literal.
    boolean
    isPositive()
    Checks if this literal is positive.
    boolean
    isTransient()
    Checks if this literal is transient.
    Literal
    neg()
    Returns the negation of this literal.

  • Method Details

    • isTransient

      boolean isTransient()
      Checks if this literal is transient. Transient literals are usually temporary and are not used as permanent identifiers.
      Returns:
      true if the literal is transient, false otherwise

    • isPositive

      boolean isPositive()
      Checks if this literal is positive. A positive literal represents a proposition in its original form, whereas a negative literal represents the negation of a proposition.
      Returns:
      true if the literal is positive, false if it is negative

    • getAtom

      Literal getAtom()
      Retrieves the atom of this literal. If the literal is a negation, this method returns the encapsulated atom. If the literal is an atom, it returns itself.
      Returns:
      the atom of the literal, or this literal if it is an atom

    • getName

      String getName()
      Returns the name of this literal. The name may be null if the literal does not have a specific name (e.g., in the case of transient literals).
      Returns:
      the name of the literal, or null if it does not have a name

    • neg

      Literal neg()
      Returns the negation of this literal. The following properties hold for every literal l:
      • l.neg().neg() == l: The negation of the negation returns the original literal.
      • l.neg().getAtom() == l.getAtom(): The negation of the literal has the same atom.
      The following property might not hold for every literal l:
      • l.neg() == l.neg(): The negation of a literal might not be equal to itself.
      Returns:
      the negation of this literal

    • create

      static Literal create()
      Creates a new unnamed atom literal. This is a default literal without any specific name.
      Returns:
      a new unnamed atom literal

    • create

      static Literal create(String name)
      Creates a new named atom literal with the specified name. If the provided name is null, an unnamed atom literal is created instead.
      Parameters:
      name - the name of the literal, or null for an unnamed literal
      Returns:
      a new named atom literal, or an unnamed atom literal if the name is null

    • createTransient

      static Literal createTransient()
      Creates a new transient atom literal. Transient literals are typically used for temporary or intermediate purposes and do not have a permanent name.
      Returns:
      a new transient atom literal