package cnf;

import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

/**
 * A clause in a CNF formula, a disjunction of literals.
 * 
 * @author Greg Dennis (gdennis@mit.edu)
 */
public final class Clause {
    
    private final Set/*<Literal>*/ literals;

    /**
     * Constructs and empty clause.
     */
    public Clause() {
        this.literals = new HashSet();
    }
    
    /**
     * Constructs a copy of the specified clause.
     */
    public Clause(Clause clause) {
        this.literals = new HashSet(clause.literals);
    }

    /**
     * Adds the specified literal to this clause.
     * Rejects the literal if another literal (positive or negative)
     * with the same variable is already in this clause.
     *
     *@throws IllegalArgumentException if this clause already contains
     * 			a literal of the same variable.
     */
    public void addLiteral(Literal literal)	{
        if (containsVariable(literal.variable())) {
            throw new IllegalArgumentException(
                    "clause already contains variable " + literal.variable());
        }
        literals.add(literal);
    }
    
    /**
     * Returns true if this clause contains the specified literal.
     */
    public boolean containsLiteral(Literal literal)	{
        return literals.contains(literal);
    }
    
    /**
     * Returns true if this clause contains a literal with the
     * specified variable.
     */
    public boolean containsVariable(int var) {
        Literal lit = Literal.getLiteral(var);
        return literals.contains(lit) || literals.contains(lit.not());
    }
    
    /**
     * Returns the set of literals.
     */
    public Set/*<Literal>*/ literals() {
        return Collections.unmodifiableSet(literals);
    }
    
    /**
     * Returns the number of literals (same as the number of variables) in the clause. 
     */
    public int numLiterals() {
        return literals.size();
    }
    
    public int hashCode() {
        return literals.hashCode();
    }
    
    public boolean equals(Object o) {
        if (!(o instanceof Clause)) return false;
        return literals.equals(((Clause)o).literals);
    }
    
    public String toString() {
        StringBuilder sb = new StringBuilder("(");
        for(Iterator/*<Literal>*/ i = literals.iterator(); i.hasNext();) {
            sb.append(i.next());
            if (i.hasNext()) sb.append(" v ");
        }
        return sb.append(")").toString();
    }
}