//******************************************************
// Class Definition for GamePosn Record used
// in SAT-TPI Game.
//
// Ref: Dunne, P.E. TPI-Disputes and Proof by Clausal Tableaux
//                  Tech. Report ULCS-02-008
//******************************************************
// The Game is recorded as a linked list, in which each
// list cell has the following structure:
//  int: MoveNum(ber) (>=0)
//  char: MoveMade : the move type (A, C, or R)
//  int:  Arg(ument) The argument in C(ounter) moves.
//  boolean[] Defence : the current Defender commitments.
//  boolean[] Attack : the current attacks.
//******************************************************
// The Defence and Attack structures assume argument
// arrays indexed as follows:
// Index i 1..n :  Arguments corresponding to x_i
//       n+1..2n:  Arguments corresponding to -x_i
//    2n+1..2n+m:  Clause C_k with k=i-2n;
//        2n+m+1:  Argument representing CNF 
//******************************************************
// Paul E. Dunne 
// Dept. of Computer Science
// Univ. of Liverpool
//******************************************************
// Version: 22/05/2002
//******************************************************
public class GamePosn
  {
  // Game Position Fields                                *
  //******************************************************
  private int MoveNum;
  private char MoveMade;  // A(ssert) or C(ounter) or R(etract)
  private int Arg;        // Argument Number for A or C.
  private boolean[] Defence;
  private boolean[] Attack;
  private boolean[] Retrctd;
  private int vars;
  private int clauses;
  //******************************************************
  // Game Position Constructor                           *
  //******************************************************
  public GamePosn(int n, int m)
    {
    vars=n; clauses=m;
    Defence = new boolean[2*vars+clauses+2];
    Attack  = new boolean[2*vars+clauses+2];
    Retrctd = new boolean[2*vars+clauses+2];
    };
  //******************************************************
  // Instance Methods                        *
  //******************************************************
  //
  public void SetMoveNumber(int k)
    {
    MoveNum = k;
    };
  public void SetArg(int x)
    {
    Arg = x;
    }
  public void SetMoveMade(char c)
    {
    MoveMade = c;
    }
  public void SetDefence(boolean[] D)
    {
    for (int i=0; i<Defence.length; i++)
      {
      Defence[i]= D[i];
      };
    }
  public void SetAttack(boolean[] A)
    {
    for (int i=0; i<Attack.length; i++)
      {
      Attack[i]= A[i];
      };
    }
  public void SetRetract(boolean[] R)
    {
    for (int i=0; i<Retrctd.length; i++)
      {
      Retrctd[i]= R[i];
      };
    }
  public int GetMoveNumber()
    {
    return MoveNum;
    };
  public int GetArg()
    {
    return Arg;
    }
  public char GetMoveMade()
    {
    return MoveMade;
    }
  public boolean[] GetDefence()
    {
    return Defence;
    }
  public boolean[] GetAttack()
    {
    return Attack;
    }
  public boolean[] GetRetract()
    {
    return Retrctd;
    }
  //*****************************************************
  // Convert GamePosn record to String for output.
  //*****************************************************
  public String toString()
    {
    String res = new String();
    res = res+MoveNum+" "+MoveMade+" ";
    if (!(MoveMade=='R'))
      {
      res = res+Arg;
      }
    else
      {
      for (int i=1; i<=vars; i++)
        {
        if (Retrctd[i])
          {
          res=res+i+" ";
          };
        if (Retrctd[vars+i])
          {
          res=res+"-"+i+" ";
          };
        };
      };
//    res = res+"\n"+"Defending Literals"+"\n";
//    for (int i=1; i<vars+1; i++)
//      {
//      if (Defence[i])
//        {
//        res=res+" "+i;
//        };
//      if (Defence[vars+i])
//        {
//        res=res+" -"+i;
//        };
//      }
//   res = res+"\n"+"Attacking Clauses"+"\n";
//   for (int i=2*vars+1; i<2*vars+clauses+1; i++)
//     {
//     if (Attack[i])
//       {
//       res=res+" "+(i-2*vars);
//       };
//     };
//   res=res+"\n";
   return res;
   };
  }