package cnf;

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

/**
 * A CNF Formula, a conjunction of clauses.
 * 
 * @author Greg Dennis (gdennis@mit.edu)
 */
public final class CNF {
    
    private final Set/*<Clause>*/ clauses = new HashSet();
    private int maxVar = 0;

    /**
     * Constructs an empty CNF formula.
     */
    public CNF() {}

    /**
     * Adds the specified clause to the CNF.
     * This will reject the same clause object being added twice,
     * but will not reject two clauses with the same literals being added.
     * 
     * @throw IllegalArgumentException 
     */
    public void addClause(Clause clause) {
        if (clause == null) throw new NullPointerException("clause");
        if (!clauses.add(clause)) {
            throw new IllegalArgumentException("clause " + clause + " already in CNF");
        }
        
        for (Iterator/*<Literal>*/ i = clause.literals().iterator(); i.hasNext();) {
            int var = ((Literal)i.next()).variable();
            if (var > maxVar) maxVar = var;
        }
    }
    
    /**
     * Returns true if this CNF contains the specified clause.
     */
    public boolean containsClause(Clause clause) {
        return clauses.contains(clause);
    }
    
    /**
     * Returns a set of clauses.
     */
    public Set/*<Clause>*/ clauses() {
        return Collections.unmodifiableSet(clauses);
    }
    
    /**
     * Returns the number of clauses in the CNF.
     */
    public int numClauses() {
        return clauses.size();
    }
    
    public int numVariables() {
        return maxVar;
    }
    
    public String toString() {
        StringBuilder sb = new StringBuilder();
        for(Iterator/*<Clause>*/ i = clauses.iterator(); i.hasNext();) {
            sb.append(i.next());
            if (i.hasNext()) sb.append(" ^ ");
        }
        return sb.toString();
    }
    
}