// 2004-11-11 [21:15]
//  *. New 

/**
 * Last modified: 2004-11-14 [01:08]
 *
 * @author Takayuki Hoshi <hoshi103@chapman.edu>
 *
 */

import java.io.*;
import java.util.Vector;

public class Lister {
	
	public static final boolean DEBUG = false;
	private PropositionalLogicParser parser;
	private Vector vector;
	private int nElements;
	private String formula = "" ;
	private int limit;
	private Object[] answers;
	private String[] keys;
	private String[] possibilities;
	private LogicalSystem current_system;
	private boolean table_is_constructable;
	private int nTruthValues;
	
//  **. constructor 
// 2004-11-08 [22:12]
	
	public Lister(LogicalSystem current_system, String formula, 
				  Vector vector, PropositionalLogicParser parser) {
		
		this.vector = vector;
		this.nElements = vector.size();
		this.formula = formula;
		this.parser = parser;
		this.current_system = current_system;
		this.nTruthValues = current_system.getNTruthValues();
		if( nTruthValues == -1 ) 
			table_is_constructable = false;
		else table_is_constructable = true;
		limit = (int) Math.pow( nTruthValues , nElements );
		answers = new Object[limit];
		keys = new String[nElements];
		possibilities = new String[ limit ];
		
	}
	
	public void setFormula( String formula ) {
		this.formula = formula;
	}

	public void sortElements(String[] s) {
		/* SORT ELEMENTS  */
		StringCompare compare = new StringCompare();
		if(DEBUG) System.out.println("Sorting elements..." );
		Sort sort = new Sort();
		sort.quicksort(s, 0, (s.length - 1), compare );
	}
	
	
//  **. show table 
// 2004-11-08 [22:13]
	
/*
  Example:
  
  a	b	c	a |  ( b => c )
  1	1	1	1
  1	1	0	1
  1	0	1	1
  1	0	0	1
  0	1	1	1
  0	1	0	0
  0	0	1	1
  0	0	0	1
  
  in ths case, 
  
  keys = { "a" , "b" , "c" }
  
  possibilities = {
  "0	0	0" ,		// a	b	c
  "0	0	1" ,		// each has to be separated by \t
  "0	1	0" ,
  "0	1	1" ,
  "1	0	0" ,
  "1	0	1" ,
  "1	1	0" ,
  "1	1	1" ,
  }
  
  answers = {
  1	1	1	1	1	0	1	1
  }
  
*/
	public void listReversed() {
		
		if( table_is_constructable ) {
			
			init();
			
			/* list each sentence symbols and then the whole formula */
			for(int j = 0; j < nElements; j++) {
				System.out.print( keys[j] + "\t");
			}
			System.out.println(formula);
			
			/* make the truth value table in a reversed order */
			for(int i = (limit - 1); i >= 0; i-- ) {
				System.out.print( possibilities[i] + "\t");
				System.out.println(answers[i].toString());
			}
			System.out.println();
		}
		else {
			System.out.println( "The current logical system doesn't support the command."  );
		}
	}
	
	
// 2004-11-13 [08:22]
//  **. getSatisfyingTruthAssignmentsWithPropositionalAtoms 

/**
   Format:

   String[] =
   {
   "a	b	c" ,
   "1	0	1" ,
   "0	1	1" ,
   "1	0	1"
   }

   such that truth assignments "1 0 1" , "0 1 1" , "1 0 1" for a, b, and c yields true.

*/

	public Vector getSatisfyingTruthAssignmentsWithPropositionalAtoms() {
		init();
		
		Vector satisfyingTruthAssignments = new Vector();
		String propositional_atoms = "" ;

		if( possibilities != null ) {

			for(int j = 0; j < nElements; j++) {
				propositional_atoms = propositional_atoms + keys[j] + "\t" ;
			}
			propositional_atoms = propositional_atoms.trim();
			satisfyingTruthAssignments.add( propositional_atoms );		// add, eg. "a b c d" 
			
			for ( int i = 0 ; i < answers.length ; i++ ) {
				if ( current_system.trueOrFalse( answers[i] ) ) 
					satisfyingTruthAssignments.add( possibilities[i] );		// add the assignments which satisfy the formula.
			}		// end of for loop

			return satisfyingTruthAssignments;
		} else {
			return satisfyingTruthAssignments;		// either no truth assignment found or the
			// formula (request) is malformed
		}

		

	}



//  **. obtaining table information - init() 
// 2004-11-08 [22:13]
	
	//! POST-CONDITION: possibilities set
	//! POST-CONDITION: answers set
	public void init() {
		
		PropositionalLogicParser parser = new PropositionalLogicParser(System.in);
		
//  ***. when there's no symbol within the system 
// 2004-11-08 [22:13]
		
		if(nElements == 0) {
			StringReader reader;
			String changed_formula = "" ;
			reader = new StringReader( changed_formula );
			parser.ReInit(reader);		// REINITIALIZE THE PARSER
			
			try {
				
				answers[0] = parser.AdditiveExpression();
				if(DEBUG) System.out.println("The answer for " + changed_formula + " is: " + answers[0].toString() );
				
			} catch (ParseException e) {
				System.out.println("The input formula is ill-formed (i.e., doesn't follow the syntax).  Input ignored..." );
				
				e.printStackTrace();
				/* RECOVER FROM THE EXCEPTION */
				java.io.StringReader reader2 = new java.io.StringReader( ""  );
				parser.ReInit(reader2);		// REINITIALIZE THE PARSER
				parser.ReInit(System.in);		// REINITIALIZE THE PARSER
			} catch (TokenMgrError e2) {
				System.out.println("Illegal token encountered in the input formula.  Input ignored..." );
				/* RECOVER FROM THE EXCEPTION */
				java.io.StringReader reader2 = new java.io.StringReader( ""  );
				parser.ReInit(reader2);		// REINITIALIZE THE PARSER
				parser.ReInit(System.in);		// REINITIALIZE THE PARSER
			} catch (Exception e3) {
				System.out.println("Unexpected exception occurred during processing the input. Program exiting..." );
				e3.printStackTrace();
				System.exit(-1);
			}
			parser.ReInit(System.in);		// REINITIALIZE THE PARSER
			
		}
		
//  ***. when there is 1 or more sentence symbols within the formula 
// 2004-11-08 [22:14]
		
		else{
			StringReader reader;
			keys = new String[nElements];		// vector.size()
			
			/* SAFER WAY to get keys */
			synchronized (vector) {
				for (int i = 0; i < nElements; i++) {
					keys[i] = ((VariableEntry) vector.elementAt(i)).getKey();
					if(DEBUG) System.out.println("Lister.class: key[" + i + "] is: " + keys[i]);
				}
			}
			
			/* since hashtable gives us back the unsorted array of Strings, we sort
			 * them instead. */
			sortElements(keys);
			
			BaseNMatrix matrix = new BaseNMatrix();
			possibilities = matrix.getPossibleValues( nTruthValues, nElements );
			
			if( possibilities != null) {		// null means, something wrong with the request.
				
				String changed_formula = "" ;
				
				/* REVERSED order */
				for(int i = (limit - 1); i >= 0; i-- ) {
					Replacer replacer = new Replacer(nElements);
					changed_formula = replacer.replace( formula, keys, possibilities[i].replaceAll( "\t", "") );		// !remove \t in the string
// 					if(DEBUG) System.out.println("Changed formula (in Lister class) is: " + changed_formula  );
					
					reader = new StringReader( changed_formula );
					parser.ReInit(reader);		// REINITIALIZE THE PARSER
		// !
// 					System.out.println("Current system is: " +  (parser.getCurrentSystem()).getSystemName() );
					
					try {
						
						answers[i] = parser.AdditiveExpression();
						
// 						if(DEBUG) System.out.println("The answer for " + changed_formula + " is: " + answers[i].toString() );
						
					} catch (ParseException e) {
						System.out.println("The input formula is ill-formed (i.e., doesn't follow the syntax).  Input ignored..." );
						
						e.printStackTrace();
						
						/* RECOVER FROM THE EXCEPTION */
						java.io.StringReader reader2 = new java.io.StringReader( ""  );
						parser.ReInit(reader2);		// REINITIALIZE THE PARSER
						parser.ReInit(System.in);		// REINITIALIZE THE PARSER
					} catch (TokenMgrError e2) {
						System.out.println("Illegal token encountered in the input formula.  Input ignored..." );
						/* RECOVER FROM THE EXCEPTION */
						java.io.StringReader reader2 = new java.io.StringReader( ""  );
						parser.ReInit(reader2);		// REINITIALIZE THE PARSER
						parser.ReInit(System.in);		// REINITIALIZE THE PARSER
					} catch (Exception e3) {
						System.out.println("Unexpected exception occurred during processing the input. Program exiting..." );
						e3.printStackTrace();
						System.exit(-1);
					}
					
				}
				
				parser.ReInit(System.in);		// REINITIALIZE THE PARSER
				
			}
			else {		// when possibilities == null
				table_is_constructable = false;
			}
		}
	}
	
// 2004-11-13 [18:38]
//  **. isSatisfiable 

	public boolean isSatisfiable() {
		if( table_is_constructable ) {
			
			init();
			for(int i = 0; i < answers.length; i++) {
				if( current_system.trueOrFalse( answers[i] ) ) return true;
			}
			return false;
			
		}
		else {
			System.out.println( "The current logical system doesn't support the command."  );
			System.out.println( "Returning False ( value: " + (current_system.getFalseValue()).toString() + " ) instead. ");
			return false;
		}
		
	}
	
// 2004-11-13 [18:38]
//  **. isvalid 

	public boolean isValid() {
		if( table_is_constructable ) {
			
			init();
			
			for(int i = 0; i < answers.length; i++) {
				if(! current_system.trueOrFalse( answers[i] )  ) return false;
			}
			return true;
		}
		else {
			System.out.println( "The current logical system doesn't support the command."  );
			System.out.println( "Returning False ( value: " + (current_system.getFalseValue()).toString() + " ) instead. ");
			return false;
		}
	}
	
// 2004-11-13 [18:38]
//  **. models 

	/* this |= wff? */
	/* `{ alpha, beta, gamma }|= formula' iff `(alpha & beta & gamma) & (not
	 * formula)' is unsatisfiable.  */
	public boolean models() {
		
		return (isSatisfiable() ) ? false : true;
		
	}
	
	/* !!! we wanna do this with tableaux */
// 	/* Sigma |= wff   iff   Sigma |- wff  */
// 	public boolean proves() {
// 		return (isSatisfiable() ) ? false : true;
// 	}
	

// 2004-11-13 [20:21]
//  **. Entails


// 	public boolean entails(HashSet sigma, String formula)  {
// 		//! PRECONDITION: Lister object be initialized properly with proper arguments
		
// 		init() ;		// in order to get possible values for distinct symbols for all formulas.
// 		String[][] truth_assignments = new String[ limit ][ nElements ];		

// 		for (Iterator it = sigma.iterator() ; it.hasNext() ; ) {
// 			// use `(ObjectType) it.next();' to get the current object
// // 			keys[i]
// 		}		// end of for loop
// 	}

// 	public String[][] getTruthAssignmentsAndAnswersForFormulas( HashSet sigma ) {
// 		String concatenatedFormulas  = "" ;		// just to make variable table
// 		boolean firstContatenation = true;

// // bsh % bsh % HashSet sigma = new HashSet();
// // bsh % sigma.add ( "a | b | c" );
// // bsh % sigma.add ( "a | ~c" );
// // bsh % sigma.add ( "d" );
// // bsh % bsh % bsh % bsh % bsh % print( concatenatedFormulas );
// //  (d ) & ( a | b | c) & ( a | ~c) 
// 		for (Iterator it = sigma.iterator() ; it.hasNext() ; ) {
// 			if ( firstContatenation ) {
// 				concatenatedFormulas = " ( " + (String) it.next() + " ) " ;
// 				firstContatenation = false;
// 			}  else {
// 				concatenatedFormulas = concatenatedFormulas + "&" + " ( " + (String) it.next() + " ) " ;
// 			}
// 		}		// end of for loop

// 		setFormula( concatenatedFormulas );
// 		init() ;		// in order to get possible values for distinct symbols for all formulas.
		
// 	}


	
// 2004-11-13 [18:38]
//  **. main 

	public static void main(String[] args) {
// //		 VariableTable vt = new VariableTable();
//		  vt.put( "p" , new Integer(1) );
//		  vt.put( "r" , new Integer(0) );
//		  vt.put( "q" , new Integer(1) );
// //		 vt.put( "s" , new Integer(0) );
		
// //		 StringReader reader = new StringReader( "p & q | r & p & s | ~ p & q" );
//		 StringReader reader = new StringReader( "1 & 1" );
		
// // "p & q | r & p & s | ~ p & q"
//		 Lister lister = new Lister( "p |  ( q => r )" , vt);
// //		 lister.list();
//		 lister.listReversed();
		
// //		 System.out.println(lister.nElements );
//		 String[] keys = new String[vt.size()];
//		 keys = vt.getKeys();
//		 int[] elements = new int[vt.size()];
//		 elements = vt.getValues();
		
//		 for(int i = 0; i < keys.length; i++ ) {
//			 System.out.println(keys[i]);
//		 }
		
	} // end of main()
	
}		// end of class `Lister'




// 2004-11-11 [18:37]
// //  *. Older 

// /**
//  * Last modified: 2004-11-14 [01:08]
//  *
//  * @author Takayuki Hoshi <hoshi103@chapman.edu>
//  *
//  */

// import java.io.*;
// import java.util.Vector;

// public class Lister {

// 	public static final boolean DEBUG = false;
// 	private PropositionalLogicParser parser;
// 	private Vector vector;
// 	private int nElements;
// 	private String formula = "" ;
// 	private int limit;
// 	private Object[] answers;
// 	private String[] keys;
// 	private String[][] possibilities;
// 	private LogicalSystem current_system;
// 	private boolean table_is_constructable;
// 	private int nTruthValues;

// //  **. constructor 
// // 2004-11-08 [22:12]

// 	public Lister(LogicalSystem current_system, String formula, 
// 				  Vector vector, PropositionalLogicParser parser) {

// 		this.vector = vector;
// 		this.nElements = vector.size();
// 		this.formula = formula;
// 		this.parser = parser;
// 		this.current_system = current_system;
// 		this.nTruthValues = current_system.getNTruthValues();
// 		if( nTruthValues == -1 ) 
// 			table_is_constructable = false;
// 		else table_is_constructable = true;
// 		limit = (int) Math.pow( nTruthValues , nElements );
// 		answers = new Object[limit];
// 		keys = new String[nElements];
// 		possibilities = new String[ limit ][ nElements ];

// 	}

// 	public void sortElements(String[] s) {
// 		/* SORT ELEMENTS  */
// 		StringCompare compare = new StringCompare();
// 		if(DEBUG) System.out.println("Sorting elements..." );
// 		Sort sort = new Sort();
// 		sort.quicksort(s, 0, (s.length - 1), compare );
// 	}


// //  **. show table 
// // 2004-11-08 [22:13]

// /*
//   Example:

//   a	b	c	a |  ( b => c )
//   1	1	1	1
//   1	1	0	1
//   1	0	1	1
//   1	0	0	1
//   0	1	1	1
//   0	1	0	0
//   0	0	1	1
//   0	0	0	1

//   in ths case, 

//   keys = { "a" , "b" , "c" }

//   possibilities = {
//   0	0	0
//   0	0	1
//   0	1	0
//   0	1	1
//   1	0	0
//   1	0	1
//   1	1	0
//   1	1	1
//   }

//   answers = {
//   1	1	1	1	1	0	1	1
//   }

// */
// 	public void listReversed() {

// 		if( table_is_constructable ) {

// 			init();

// 			/* list each sentence symbols and then the whole formula */
// 			for(int j = 0; j < nElements; j++) {
// 				System.out.print( keys[j] + "\t");
// 			}
// 			System.out.println(formula);

// 			/* make the truth value table in a reversed order */
// 			for(int i = (limit - 1); i >= 0; i-- ) {
// 				/* LIST */
// 				for(int j = 0; j < keys.length; j++) {
// 					System.out.print( possibilities[i][j] + "\t");
// 				}
// 				System.out.println(answers[i].toString());
// 			}

// 			System.out.println();
// 		}
// 		else {
// 			System.out.println( "The current logical system doesn't support the command."  );
// 		}
// 	}


// //  **. obtaining table information - init() 
// // 2004-11-08 [22:13]

// 	public void init() {

// 		PropositionalLogicParser parser = new PropositionalLogicParser(System.in);

// //  ***. when there's no symbol within the system 
// // 2004-11-08 [22:13]

// 		if(nElements == 0) {
// 			StringReader reader;
// 			String changed_formula = "" ;
// 			reader = new StringReader( changed_formula );
// 			parser.ReInit(reader);		// REINITIALIZE THE PARSER

// 			try {

// 				answers[0] = parser.AdditiveExpression();
// 				if(DEBUG) System.out.println("The answer for " + changed_formula + " is: " + answers[0].toString() );

// 			} catch (ParseException e) {
// 				System.out.println("The input formula is ill-formed (i.e., doesn't follow the syntax).  Input ignored..." );

// 				e.printStackTrace();
// 				/* RECOVER FROM THE EXCEPTION */
// 				java.io.StringReader reader2 = new java.io.StringReader( ""  );
// 				parser.ReInit(reader2);		// REINITIALIZE THE PARSER
// 				parser.ReInit(System.in);		// REINITIALIZE THE PARSER
// 			} catch (TokenMgrError e2) {
// 				System.out.println("Illegal token encountered in the input formula.  Input ignored..." );
// 				/* RECOVER FROM THE EXCEPTION */
// 				java.io.StringReader reader2 = new java.io.StringReader( ""  );
// 				parser.ReInit(reader2);		// REINITIALIZE THE PARSER
// 				parser.ReInit(System.in);		// REINITIALIZE THE PARSER
// 			} catch (Exception e3) {
// 				System.out.println("Unexpected exception occurred during processing the input. Program exiting..." );
// 				e3.printStackTrace();
// 				System.exit(-1);
// 			}
// 			parser.ReInit(System.in);		// REINITIALIZE THE PARSER

// 		}

// //  ***. when there is 1 or more sentence symbols within the formula 
// // 2004-11-08 [22:14]

// 		else{
// 			StringReader reader;
// 			keys = new String[nElements];		// vector.size()

// 			/* SAFER WAY to get keys */
// 			synchronized (vector) {
// 				for (int i = 0; i < nElements; i++) {
// 					keys[i] = ((VariableEntry) vector.elementAt(i)).getKey();
// 					if(DEBUG) System.out.println("Lister.class: key[" + i + "] is: " + keys[i]);
// 				}
// 			}

// 			/* since hashtable gives us back the unsorted array of Strings, we sort
// 			 * them instead. */
// 			sortElements(keys);

// 			BaseNMatrix matrix = new BaseNMatrix();
// 			possibilities = matrix.getPossibleValues( nTruthValues, nElements );
// 			String changed_formula = "" ;

// 			/* REVERSED order */
// 			for(int i = (limit - 1); i >= 0; i-- ) {
// 				Replacer replacer = new Replacer(nElements);
// 				changed_formula = replacer.replace( formula, keys, possibilities[i]);
// 				if(DEBUG) System.out.println("Changed formula (in Lister class) is: " + changed_formula  );

// 				reader = new StringReader( changed_formula );
// 				parser.ReInit(reader);		// REINITIALIZE THE PARSER


// 				try {

// 					answers[i] = parser.AdditiveExpression();

// 					if(DEBUG) System.out.println("The answer for " + changed_formula + " is: " + answers[i].toString() );

// 				} catch (ParseException e) {
// 					System.out.println("The input formula is ill-formed (i.e., doesn't follow the syntax).  Input ignored..." );

// 					e.printStackTrace();

// 					/* RECOVER FROM THE EXCEPTION */
// 					java.io.StringReader reader2 = new java.io.StringReader( ""  );
// 					parser.ReInit(reader2);		// REINITIALIZE THE PARSER
// 					parser.ReInit(System.in);		// REINITIALIZE THE PARSER
// 				} catch (TokenMgrError e2) {
// 					System.out.println("Illegal token encountered in the input formula.  Input ignored..." );
// 					/* RECOVER FROM THE EXCEPTION */
// 					java.io.StringReader reader2 = new java.io.StringReader( ""  );
// 					parser.ReInit(reader2);		// REINITIALIZE THE PARSER
// 					parser.ReInit(System.in);		// REINITIALIZE THE PARSER
// 				} catch (Exception e3) {
// 					System.out.println("Unexpected exception occurred during processing the input. Program exiting..." );
// 					e3.printStackTrace();
// 					System.exit(-1);
// 				}


// 			}

// 			parser.ReInit(System.in);		// REINITIALIZE THE PARSER

// 		}
// 	}

// 	public boolean isSatisfiable() {
// 		if( table_is_constructable ) {

// 			init();
// 			for(int i = 0; i < answers.length; i++) {
// 				if( current_system.trueOrFalse( answers[i] ) ) return true;
// 			}
// 			return false;

// 		}
// 		else {
// 			System.out.println( "The current logical system doesn't support the command."  );
// 			System.out.println( "Returning False ( value: " + (current_system.getFalseValue()).toString() + " ) instead. ");
// 			return false;
// 		}

// 	}

// 	public boolean isValid() {
// 		if( table_is_constructable ) {

// 			init();

// 			for(int i = 0; i < answers.length; i++) {
// 				if(! current_system.trueOrFalse( answers[i] )  ) return false;
// 			}
// 			return true;
// 		}
// 		else {
// 			System.out.println( "The current logical system doesn't support the command."  );
// 			System.out.println( "Returning False ( value: " + (current_system.getFalseValue()).toString() + " ) instead. ");
// 			return false;
// 		}
// 	}

// 	/* this |= wff? */
// 	/* `{ alpha, beta, gamma }|= formula' iff `(alpha & beta & gamma) & (not
// 	 * formula)' is unsatisfiable.  */
// 	public boolean models() {

// 		return (isSatisfiable() ) ? false : true;

// 	}

// 	/* !!! we wanna do this with tableaux */
// // 	/* Sigma |= wff   iff   Sigma |- wff  */
// // 	public boolean proves() {
// // 		return (isSatisfiable() ) ? false : true;
// // 	}


// 	public static void main(String[] args) {
// // //		 VariableTable vt = new VariableTable();
// //		  vt.put( "p" , new Integer(1) );
// //		  vt.put( "r" , new Integer(0) );
// //		  vt.put( "q" , new Integer(1) );
// // //		 vt.put( "s" , new Integer(0) );

// // //		 StringReader reader = new StringReader( "p & q | r & p & s | ~ p & q" );
// //		 StringReader reader = new StringReader( "1 & 1" );

// // // "p & q | r & p & s | ~ p & q"
// //		 Lister lister = new Lister( "p |  ( q => r )" , vt);
// // //		 lister.list();
// //		 lister.listReversed();

// // //		 System.out.println(lister.nElements );
// //		 String[] keys = new String[vt.size()];
// //		 keys = vt.getKeys();
// //		 int[] elements = new int[vt.size()];
// //		 elements = vt.getValues();

// //		 for(int i = 0; i < keys.length; i++ ) {
// //			 System.out.println(keys[i]);
// //		 }

// 	} // end of main()

// }		// end of class `Lister'

