/**
 * Last modified: 1 02 2004
 *
 */

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

public class ThreeValuedLister {

    public static final boolean DEBUG = false;
    public static final boolean CLASSICAL = true;
    private PropositionalLogicParser parser;
    private Vector vector;
    private int nElements;
    private String formula = "" ;
    private int limit;
    private int[] answers;
    private String[] keys;
    private String[][] possibilities;

    public ThreeValuedLister(String formula, Vector vector, PropositionalLogicParser parser) {
      this.vector = vector;
      nElements = vector.size();
      this.formula = formula;
//         parser = new PropositionalLogicParser();
      this.parser = parser;

      limit = (int) Math.pow(3, nElements);		// !!M
//         PropositionalLogicParser.NUMBER_OF_TRUTH_VALUES, nElements); //* modified
      answers = new int[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 );
    }


/*
  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
*/
    public void listReversed() {
        init();

        /* LIST  */
        for(int j = 0; j < nElements; j++) {
            System.out.print( keys[j] + "\t");
        }
        System.out.println(formula);

        /* 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]);
        }

        System.out.println();

    }

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

            try {

                int answer = parser.AdditiveExpression();
                answers[0] = answer;
                if(DEBUG) System.out.println("The answer for " + changed_formula + " is: " + answer);
            } catch (ParseException e) {
                e.printStackTrace();
            } // end of try-catch
            parser.ReInit(System.in);		// REINITIALIZE THE PARSER

        }
        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("ThreeValuedLister.class: key[" + i + "] is: " + keys[i]);

                }
            }

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

            ThreeValuedMatrix matrix = new ThreeValuedMatrix();
            possibilities = matrix.getPossibleValues(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 ThreeValuedLister class) is: " + changed_formula  );

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

                try {

                    int answer = parser.AdditiveExpression();
                    answers[i] = answer;

                    if(DEBUG) System.out.println("The answer for " + changed_formula + " is: " + answer);

                } catch (ParseException e) {
                    e.printStackTrace();
                } // end of try-catch
            }

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

        }
    }

    public boolean isSatisfiable() {
        init();
        for(int i = 0; i < answers.length; i++) {
            if(answers[i] == 1 ) return true;
        }
        return false;
    }

    public boolean isValid() {
        init();
        for(int i = 0; i < answers.length; i++) {
            if(answers[i] != 1 ) return false; //* modified; was == 0.
        }
        return 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"
//         ThreeValuedLister lister = new ThreeValuedLister( "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 `ThreeValuedLister'

