/***************************************************************
 * ThreeCNF data structure
 * Updated by Mark Goadrich 2/16/2008
 *
 * ThreeCNF is a conjunction of disjunctive clauses, otherwise
 * known as conjunctive normal form.  Each clause in ThreeCNF 
 * consists of three literals.  Both the clauses and propositional
 * symbols are stored in arrays.  I have included what I believe
 * to be the necessary methods for this assignment.  Feel free to 
 * change and rewrite any part of this code.  
 **************************************************************/
public class ThreeCNF {
    private PropSymbol[] propSymbols;  // holds all our Propositional Symbols
    private Clause[] clauses;          // holds all our Clauses
   
    // the constructor initializes our arrays of PropSymbols and Clauses
    public ThreeCNF(int numberOfPropSymbols, int numberOfClauses) {

	// first create enough space based on input
	clauses = new Clause[numberOfClauses];
	propSymbols = new PropSymbol[numberOfPropSymbols];

	// randomly create new Propositional symbols and place 
	// them in the array propSymbols
	for (int i = 0; i < propSymbols.length; i++) {
	    propSymbols[i] = new PropSymbol(true, i);
	}	
	generateTruths();

	// for as many clauses as you need, randomly select three
	// propositional symbols with replacement to be included
	// in the Clause
	for (int i = 0; i < clauses.length; i++) {

	    // Make space for three literals
	    Literal[] lits = new Literal[3];
	    for (int j = 0; j < 3; j ++) {

		// select the index for a PropSymbol
		int temp = (int)(Math.random() * propSymbols.length);

		// randomly determine the negation status of each literal
		boolean neg = false;
		if (Math.random() > 0.5) {
		    neg = true;
		}

		// create the Literal
		lits[j] = new Literal(propSymbols[temp], neg);
	    }
	    
	    // place newly formed Clauses in the array of clauses
	    clauses[i] = new Clause(lits[0], lits[1], lits[2]); 
	}
    }

    // this method randomly assigns truth values to the Propositional
    // Symbols in our ThreeCNF.
    public void generateTruths() {
	for (int i = 0; i < propSymbols.length; i++) {
	    if (Math.random() > 0.5) {
		propSymbols[i].putValue(true);
	    } else { 
		propSymbols[i].putValue(false);
	    }
	}	
    }

    // returns true if all of the Clauses in this ThreeCNF are satisfied
    // if we ever find a false clause, return false, otherwise it's true.
    public boolean isSatisfied() {
	for (int i = 0; i < clauses.length; i++) {
	    if (!clauses[i].findTValue()) {
		return false;
	    }
	}
	return true;
    }

    // flips the given PropSymbol i to its negation.  If you try to flip
    // a nonexistant PropSymbol, it will print "Out of Bounds"
    public void flipPropSymbol(int i) {
	if (i > propSymbols.length-1) {
	    System.out.println("Out of Bounds");
	} else {
	    propSymbols[i].flip();
	}
    }
    
    // returns the number of true clauses in this ThreeCNF.
    // This is useful in evaluating whether or not to choose a certain
    // truth value assignment.
    public int numberOfTrueClauses() {
	int numTrue = 0;
	for (int i = 0; i < clauses.length; i++) {
	    if (clauses[i].findTValue()) {
		numTrue ++;
	    }
	}
	return numTrue;
    }    
    
    // prints out the clauses in a conjunctive notation for human
    // readability.  ie. (A v ~B v C) ^ (~B v ~D v A) ^ etc...
    public void printClauses() {
	System.out.println("Clauses:");
	for (int i = 0; i < clauses.length; i++) {
	    System.out.println(clauses[i]);
	    if (i != clauses.length-1) {
		System.out.print(" ^ ");
	    }
	}
	System.out.println("");
    }
    
    // prints the array of PropSymbols, with names followed by their
    // truth value.
    public void printPropSymbols() {
	System.out.println("PropSymbols:");
	for (int i = 0; i < propSymbols.length; i++) {
	    System.out.println(i + ": " + propSymbols[i].booleanValue());
	}
    }
    
    // A method for unit testing the ThreeCNF class
    public static void main (String[] args) {
	if (args.length != 2) {
	    System.out.println("You need to use the right arguments.");
	    System.exit(-1);
	}
	
	int ps = Integer.parseInt(args[0]);
	int cs = Integer.parseInt(args[1]);
	
	ThreeCNF testing = new ThreeCNF(ps, cs);
	testing.printClauses();
	testing.printPropSymbols();
	System.out.println("Is Satisfied? " + testing.isSatisfied());
	System.out.println("How Many Satisfied out of " + cs + "? " +
			   testing.numberOfTrueClauses());
	int symb = (int)(Math.random() * ps);
	testing.flipPropSymbol(symb);
	System.out.println("Flipped Symbol " + symb);
	System.out.println("Is Satisfied? " + testing.isSatisfied());
	System.out.println("How Many Satisfied out of " + cs + "? " +
			   testing.numberOfTrueClauses());
    }
}