package cnf;

import java.util.ArrayList;
import java.util.List;

/**
 * A literal, represented as an integer.
 * 
 * @author Greg Dennis (gdennis@mit.edu)
 */
public final class Literal {

    // interned positive and negative literals
    // literal for variable i will be at index i - 1
    private static final List/*<Literal>*/ positive = new ArrayList();
    private static final List/*<Literal>*/ negative = new ArrayList();

    /**
     * Returns the literal represented by the specified integer.
     * A negative integer indicates a negated variable.
     *
     *@throws IllegalArgumentException - when lit == 0;
     */
    public static Literal getLiteral(int lit) {
      if (lit == 0) throw new IllegalArgumentException("lit cannot be zero");
      int requiredSize = Math.abs(lit);
      
      if (positive.size() < requiredSize) {
          for(int i = positive.size() + 1; i <= requiredSize; i++)	 {
              positive.add(new Literal(i));
              negative.add(new Literal(-i));
          }
      }
      
      return (Literal)(lit > 0 ? positive.get(lit - 1) : negative.get(-lit - 1));
    }

    private int lit;

    private Literal(int lit) {
      this.lit = lit;
    }

    /**
     * Returns the integer value associated with this literal.
     */
    public int intValue() {
      return lit;
    }

    /**
     * Return the integer associate with the variable in this literal,
     * i.e. the absolute value of intValue();
     */
    public int variable() {
      return Math.abs(lit);
    }
    
    /**
     * Returns the negated literal.
     */
    public Literal not() {
        return getLiteral(-lit);
    }
    
    public String toString() {
      return Integer.toString(lit);
    }

}