//package GregDLLSolver;

//Author:Greg Viola
//Class: Algos
//Version: 5
//Due Date: 4/16/07
//Status: Complete up to specifications

import java.io.File;
import java.io.FileNotFoundException;
import java.util.*;

/**
* Formula class holds a vector of clauses, a vector of booleans,
* a vector of clause numbers, and a vector of integers.  The booleans
* correspond to the clauses,and if they are true or false.  The clause
* numbers are which clauses will be true when certain variables are true.
* The integers correspond to the number of times each term occurs in
* the formula. // DEE update this
*/
public class Formula
{
 private String fileName;
 private Scanner scan;
 private Vector <Clause> clauses;
 private Vector <Boolean> satisfied;
 private Vector <LinkedList> index;
 private double [] occurrences; // DEE change this to a jw_weight
 private int numVars;
 private int numClauses_;



/**
 * Constructor for class Formula.  Initializes the vector of booleans,
 * clauses, lists of clause numbers, and term occurrences.
 *
 * @param numClauses the number of clauses
 * @param numVars the number of variables
 */
 public Formula(String inputFileName) throws FileNotFoundException
 {
     scan = new Scanner(new File(inputFileName));
     while ((scan.next()).equals("c"))
     {
        String comment = scan.nextLine();
     }
     //in the declaration line, moves to the integers (number of
     //variables and number of clauses)
     String declare = scan.next();
     numVars = scan.nextInt();
     numClauses_ = scan.nextInt();
     clauses = new Vector <Clause> (numClauses_);
     satisfied = new Vector <Boolean> (numClauses_);
     for (int i=0; i<numClauses_; i++)
     {
        satisfied.addElement(false);
     }
     index = new Vector <LinkedList> (2*numVars);
     occurrences = new double [2*numVars];
     for (int i=0; i<(2*numVars); i++)
     {
        //One for each assignment of each variable
        index.addElement(new LinkedList <Integer> ());
        //occurrences.addElement(0.0); // vestige of Vector past
     }
     for (int i=0; i<numClauses_; i++) //creates the formula
     {
        Clause clause = new Clause();
        int varNum = scan.nextInt();
        while (varNum != 0) //Create a clause
        {
             clause.add(varNum);
             //Creates an index which stores clause numbers,
             //which become true when a given variable is true.
             if (varNum > 0)
             {
                setIndex(2*(varNum-1),i);
             }
             else
             {
                varNum *= -1;
                setIndex(2*(varNum-1)+1,i);
             }
             varNum = scan.nextInt();
        }
        add(clause);
     }

}



/**
 * Constructor that creates a copy of f.
 * Initializes the vector of booleans, clauses, lists of clause numbers, and term occurrences.
 *
 * @param f is another formula
 */
 public Formula(Formula f) 
 {
/*
 private double [] occurrences; // DEE change this to a jw_weight
*/
     numVars = f.getNumVars();
     clauses = new Vector <Clause> (f.getClauses());

     numClauses_ = clauses.size();

     occurrences = new double [2*numVars]; // JW-style weights that are init'd later

     satisfied = new Vector <Boolean> (f.getSatisfied());

     index = new Vector <LinkedList> ();

     // init the index
     for (int i=0; i<(2*numVars); i++)
     {
        // for the i-th literal
        index.addElement(new LinkedList <Integer> (f.getIndexedClauses(i)));
     }
} // constructor

 //Returns number of variables.
 public int getNumVars()
 {
	 return numVars;
 }


// returns the satisfied vector
protected Vector <Boolean> getSatisfied()
{
	return satisfied;
}


// returns the satisfied vector
protected Vector <LinkedList> getIndex()
{
	return index;
}


// returns the list of clauses that a literal appears in
// @param the index of the literal
protected LinkedList <Integer> getIndexedClauses(int i)
{
	return index.get(i);
}




 public String getInputFile()
 {
     return fileName;
 }  

 /**
  * Add a clause to the formula.
  *
  * @param c the clause to be added to the vector of clauses.
  */
  public void add(Clause c)
  {
       clauses.addElement(c);
  }

 /**
  * Sets a clause number to a spot in the index vector.
  *
  * @param pos the position in the vector.
  * @param clauseNum the clause number to be inserted.
  */
  public void setIndex(int pos, int clauseNum)
  {
       LinkedList <Integer> list = index.get(pos);
       list.add(clauseNum);
  }

 /**
   * Returns the vector of clauses.
   *
   * @return Vector with the list of clauses.
   */
   public Vector getClauses()
   {
        return clauses;
   }

 /**
   * Returns the vector of clauses.
   *
   * @return Vector the list of clauses.
   */
   public Vector getFormula()
   {
        return clauses;
   }

  /**
   * Returns true if the formula is empty.
   *
   * @return boolean true if the formula is empty.
   */
   public boolean isEmpty()
   {
        return clauses.isEmpty();
   }

  /**
   * Returns true if there is an empty clause.
   *
   * @return boolean true if there is an empty clause.
   */
   public boolean hasEmptyClause()
   {
        for (int i=0; i<clauses.size(); i++)
        {
           Clause c = clauses.get(i);
           if (c.getList().isEmpty())
           {
                return true;
           }
        }
        return false;
   }

  /**
   * Checks to see if the formula is satisfied by the given
   * partial assignment.
   *
   * @param partial the partial assignment to be checked.
   * @return boolean true if the formula is satisfied.
   */
   public boolean satisfied(Assignment partial)
   {
        //Resets all of the booleans to false
        for (int i=0; i<satisfied.size(); i++)
        {
            satisfied.setElementAt(false,i);
         }
         boolean done = true;
         Vector <Integer> assign = partial.getAssignment();
         for (int i=0; i<assign.size(); i++)
         {
            int assignment = assign.get(i);
            //The variable is assigned to true
            if (assignment == 1)
            {
                 //If true look at position 2i in the index vector.
                 LinkedList <Integer> list = index.get(2*i);
                 for (int j=0; j<list.size(); j++)
                 {
                    int clauseNum = list.get(j);
                    satisfied.setElementAt(true,clauseNum);
                 }
            }
            //The variable is assigned to false.
            if (assignment == 0)
            {
                 LinkedList <Integer> list = index.get(2*i+1);
                 for (int j=0; j<list.size(); j++)
                 {
                     int clauseNum = list.get(j);
                     satisfied.setElementAt(true,clauseNum);
                  }
             }
          }
          for (int i=0; i<satisfied.size() && done; i++)
          {
             //Stays true as long as every element is true.
             done = satisfied.get(i);
          }
          return done;
     }

    /**
     * Returns false if any clause can't be satisfied given the partial
     * assignment.
     *
     * @param partial the assignment to be checked.
     * @return boolean true if a clause can't be satisfied.
     */
     public boolean hasFalseClause(Assignment partial)
     {
          boolean done = false;

          boolean falseClause = true;
          Vector <Integer> assign = partial.getAssignment();
          for (int i=0; i<satisfied.size() && !done; i++)
          {
             //Look at any clauses that are not true.
             if (!satisfied.get(i))
             {
                  falseClause = true; //Resets for every false clause
                  Clause c = clauses.get(i);
                  LinkedList <Integer> list = c.getList();
                  //Look at each var for that clause.
                  for (int j=0; j<list.size() && falseClause; j++)
                  {
                     int var = list.get(j);
                     if (var < 0)
                          var *= -1;
                     //All vars in that clauses aren't assigned yet
                     if (assign.get(var-1) == -1)
                     {
                          falseClause = false;
                     }
                  }
                  if (falseClause)
                  {
                      done = true;
                  }
             }
          }
          return falseClause;
     }

    /**
     * Counts the occurrences of each term in the formula. This counting
     * happens each time the solver chooses the next variable. This method
     * sets up the Jeroslaw-Wang heuristic for choosing the next variable.
     *
     * @param pa the current partial assignment.
     */
     public void setOccurred(Assignment pa)
     {
          //Resets occurrences before updating it.
          for (int i=0; i<occurrences.length; i++)
          {
            occurrences[i] = 0.0; 
          }
          Vector <Integer> assign = pa.getAssignment();
          //Looks through each clause.
          for (int i=0; i<clauses.size(); i++)
          {
              int clauseSize = 0;
              Clause c = clauses.get(i);
              LinkedList <Integer> list = c.getList();
              for (int j=0; j<list.size(); j++)
              {
                if (assign.get(Math.abs(list.get(j))-1) == -1)
                {
                  clauseSize++;
                }
              }
              //As long as there is at least one unassigned var
              //in the clause.
              if (clauseSize!=0)
              {
                for (int j=0; j<list.size(); j++)
                {
                  int var = list.get(j);
                  if (assign.get(Math.abs(var)-1) == -1)
                  {
                    double occur = (1 / Math.pow(2,clauseSize));
                    if (var < 0)
                    {
                      var *= -1;
                      occur += occurrences[2*(var-1)+1];
                      occurrences[2*(var-1)+1]= occur;
                    }
                    if (var > 0)
                    {
                      occur += occurrences[2*(var-1)];
                      occurrences[2*(var-1)] = occur;
                    }
                  }//end if (variable assignment check)
                }//end for (j loop)
              }//end if  (clause size check)
            }//end for (i loop)
       }//end setOccurred

      /**
       * Returns the occurrences of each variable, in the form of a vector.
       *
       * @return Vector the vector of occurrences.
       */
       public double[] getOccurrences()
       {
            return occurrences;
       }

       /**
        * Checks for unit clauses in the formula.  This is checked against the
        * current partial assignment.  Returns a positive number if the
        * variable must be set to true, or a negative number if the variable
        * must be set to false (in order to satisfy the clause).  Returns zero
        * if there is no unit clause.
        *
        * @param pa the current partial assignment
        * @return int the variable in the unit clause, or zero if there is none
        */
        public int unitClause(Assignment pa)
        {
             int var = 0;
             Vector <Integer> assign = pa.getAssignment();
             for (int i=0; i<clauses.size() && var==0; i++)
             {
                //Only unsatisfied clauses can be unit clauses
                if (!satisfied.get(i))
                {
                  Clause c = clauses.get(i);
                  LinkedList <Integer> vars = c.getList();
                  int unit = 0; //Counts the number of unassigned vars.
                  for (int j=0; j<vars.size(); j++)
                  {
                      int variable = vars.get(j);
                      if (variable < 0)
                      {
                        variable *= -1;
                        //Checks if the variable is unassigned.
                        if (assign.get(variable-1) == -1)
                        {
                           unit++;
                           var = -1 * variable;
                        }
                      }
                      if (variable > 0)
                      {
                        //Checks if the variable is unassigned.
                        if (assign.get(variable-1) == -1)
                        {
                           unit++;
                           var = variable;
                        }
                      }
                    }//end for(j)
                    //There should have only been one unassigned variable.
                    //If not, reset var to go through the loop again.
                    if (unit != 1)
                    {
                        var = 0;
                      }
                    }//end if(satisfied)
                 }//end for(i)
                 return var;
            }//end unitClause

           /**
            * Makes the formula into a string.
            *
            * @return String the formula as a string.
            */
            public String toString()
            {
                 String result = "";
                 for (int i=0; i<clauses.size()-1; i++)
                 {
                    result += clauses.get(i) + " and\n";
                 }
                 result += clauses.get(clauses.size()-1);
                 return result;
            }
         }//end Formula