package cnf;

import java.util.Random;

/**
 * Generates random CNF Formulas. Every CNFRandom has four parameters:
 * 
 * <ul>
 * <li>numVars - the number of variables from which to randomly pick
 * <li>numClauses - the number of clauses in the random CNFs
 * <li>numLitsPerClause - the number of literals in each clause
 * <li>positiveProbability - the probability of making a literal positive
 * </ul>
 * 
 * @author Greg Dennis (gdennis@mit.edu)
 */
public class CNFRandom {
    
    private static final Random RANDOM = new Random();
    
    private final int numVars;
    private final int numClauses;
    private final int numLitsPerClause;
    private final double positiveProbability;
    
    /**
     * Constructs a new CNFRandom with the specified parameters.
     *
     * @throws IllegalArgumentException if 
     * 		numVars &lt; 0 or numClauses &lt; 0 or numLitsPerClause &lt; numVars or
     *      positiveProbability &lt 0 or positiveProbability &gt 1
     */
    public CNFRandom(int numVars, int numClauses, int numLitsPerClause,
            double positiveProbability) {
        this.numVars = numVars;
        this.numClauses = numClauses;
        this.numLitsPerClause = numLitsPerClause;
        this.positiveProbability = positiveProbability;
    }
    
    /**
     * Returns a random CNF of numClauses with each clause chosen
     * with randomClause.
     */
    public CNF randomCNF() {
        CNF cnf = new CNF();
        for (int i = 0; i < numClauses; i++) {
            Clause clause = randomClause();
            while (cnf.containsClause(clause)) {
                clause = randomClause();
            }
            cnf.addClause(clause);
        }
        return cnf;
    }
    
    /**
     * Returns a random clause of numLitsPerClause literals, with
     * each literal chosen with randomLiteral.
     */
    public Clause randomClause() {
        Clause clause = new Clause();
        
        for (int i = 0; i < numLitsPerClause; i++) {
            Literal lit = randomLiteral();
            while (clause.containsVariable(lit.variable())) {
                lit = randomLiteral();
            }
            clause.addLiteral(lit);
        }
        
        return clause;
    }

    /**
     * Returns a random literal whose variable is chosen with randomVariable
     * and which is positive with positiveProbability.
     */
    public Literal randomLiteral() {
        int var = randomVariable();
        if (RANDOM.nextDouble() < positiveProbability) var = -var;
        return Literal.getLiteral(var);
    }
    
    /**
     * Returns a random variable in the range [1, numVars].
     */
    public int randomVariable() {
        return RANDOM.nextInt(numVars) + 1;
    }
    
}