//Christian Tirella
//Brian Sweeney
//CSU670 Project

import java.util.*;

public class Main {
	public static boolean testOutPutOn;
	public static final TruthTable tt = new TruthTable();
	/**
	 * @param args
	 */
	

	public static void main(String[] args) {		
		
		testOutPutOn();
		/*
		testOutPutOff();
		*/
		
		/*if (testOutPutOn) {
			//Test TruthTable
			tt.getRelationTable(0);
			System.out.println();
			tt.getRelationTable(1);
			System.out.println();
			tt.getRelationTable(2);
			System.out.println();
			tt.getRelationTable(3);
			System.out.println();
			tt.getRelationTable(4);
			System.out.println();
			tt.getRelationTable(5);
			System.out.println();
			tt.getRelationTable(6);
			System.out.println();
			tt.getRelationTable(22);
			System.out.println();
			tt.getRelationTable(255);
			System.out.println();
			tt.getRelationTable(256);
			//TruthTable looks good
		}*/
		
		/*Test Formula*/
		
		//M literals
		final MLiteral m1 = new MLiteral(1, true);
		final MLiteral m2 = new MLiteral(2, false);
		final MLiteral m3 = new MLiteral(3, true);
		final MLiteral m4 = new MLiteral(4, false);
		final MLiteral m5 = new MLiteral(5, true);
		final MLiteral m6 = new MLiteral(6, false);
		final MLiteral m7 = new MLiteral(7, false);
		final MLiteral m8 = new MLiteral(8, false);
		final MLiteral m9 = new MLiteral(9, true);
		final MLiteral m10 = new MLiteral(10, true);
		
		//D literals
		final DLiteral d1 = new DLiteral(1, false);
		final DLiteral d2 = new DLiteral(2, true);
		final DLiteral d3 = new DLiteral(3, true);
		final DLiteral d4 = new DLiteral(4, false);
		final DLiteral d5 = new DLiteral(5, true);
		final DLiteral d6 = new DLiteral(6, false);
		final DLiteral d7 = new DLiteral(7, true);
		final DLiteral d8 = new DLiteral(8, true);
		final DLiteral d9 = new DLiteral(9, false);
		final DLiteral d10 = new DLiteral(10, false);
		
		//F literals
		final FLiteral f1 = new FLiteral(1, true);
		final FLiteral f2 = new FLiteral(2, true);
		final FLiteral f3 = new FLiteral(3, false);
		final FLiteral f4 = new FLiteral(4, false);
		final FLiteral f5 = new FLiteral(5, false);
		final FLiteral f6 = new FLiteral(6, true);
		final FLiteral f7 = new FLiteral(7, false);
		final FLiteral f8 = new FLiteral(8, true);
		final FLiteral f9 = new FLiteral(9, true);
		final FLiteral f10 = new FLiteral(10, false);
		
		//CREATE F
		
		//FClause
		FClause fc22 = new FClause(22);
		fc22.addFLit(f1);
		fc22.addFLit(f2);
		fc22.addFLit(f3);
		
		FClause fc254 = new FClause (254);
		fc254.addFLit(f4);
		fc254.addFLit(f5);
		fc254.addFLit(f6);
		
		//FCSP
		FCSP fcsp1 = new FCSP();
		
		fcsp1.addClause(fc22);
		fcsp1.addClause(fc254);
		
		//CREATE M
		
		//Formula
		Formula form1 = new Formula();
		form1.addToF(fcsp1);
		form1.addToM(m1);
		form1.addToM(m2);
		form1.addToM(d5);
		form1.addToM(m10);
		form1.addToM(d6);
		form1.addToM(d8);
		form1.addToM(m6);
		form1.addToM(m7);
		form1.addToM(d6);

		
		//test rules:
		/*
		 * unitPropogate needs to be fixed
		 * look:
		 * at TruthRow.bitAt(TruthRow.java:21)
			at FClause.setCandidateRows(FClause.java:168)
			at FClause.forced(FClause.java:112)
			at FCSP.cspForced(FCSP.java:47)
			at Formula.unitPropagate(Formula.java:59)
			at Main.main(Main.java:100)*/
		/***UNIT PROPOGATE***/
		//form1.unitPropagate();
		
		/***DECIDE***/
		//only decides the same literal so far
		form1.decide();
		
		/***FAILSTATE***/
		form1.failState();
		
		/***RESTART***/
		form1.restart();
		
		form1.addToF(fcsp1);
		form1.addToM(d5);
		form1.addToM(d6);
		form1.addToM(d8);
		form1.addToM(m6);
		form1.addToM(m7);
		form1.addToM(d6);
		
		form1.printM();
		System.out.println();
		form1.printF();
		
		/***SEMI-SUPERRESOLUTION***/
		form1.semiSuperResolution();
	
	}
	
	
	private static void testOutPutOn() {
		testOutPutOn = true;
	}
	private static void testOutPutOff() {
		testOutPutOn= false;
	}
	
}