///////////////////////////////////////////////////////////////////////////////
//                                                                           //
//  Copyright (C) 1995-1999 by the Board of Trustees of Leland Stanford      //
//  Junior University.  See LICENSE for details.                             //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////

#ifndef _bitbool_h_
#define _bitbool_h_

#include "bitvec.h"

class Bit_And_Expr;
class Bit_Or_Expr;
class Bit_Xor_Expr;

extern Symbol BITAND_SYM;
extern Symbol BITOR_SYM;
extern Symbol BITXOR_SYM;

typedef Bit_And_Expr *PBit_And_Expr;
typedef Bit_Or_Expr *PBit_Or_Expr;
typedef Bit_Xor_Expr *PBit_Xor_Expr;

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: Bit_And_Expr							     //
// Description: Class for bit-wise negation of bit-vectors                   //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
class Bit_And_Expr : public Bit_Expr {
private:
  // Data
  PExpr _arg0;
  PExpr _arg1;

  // Constructor
  Bit_And_Expr(PExpr pexpr0, PExpr pexpr1);

  // Initialization function called by Bit_Expr::Init()
  friend void Bit_Expr::Init();
  static void Init() { BITAND_SORT = Install_Operator(BITAND_SYM, Parse); }

  // Implementation of Expr protected virtual functions
  PExpr Copy() const { return new Bit_And_Expr(_arg0, _arg1); }
  Bool TypeCheck();
  void Print1(ostream&) const;
  int Hash1() const { return abs(int(_arg0)*23+int(_arg1)); }
  int Match1(PCExpr) const;
  void FindBestSplitter1(Bool);

public:
  // Constants and statics
  static const Symbol BITAND_SYM;
  static int BITAND_SORT;

  // Access functions
  PExpr arg0() { return _arg0; }
  PExpr arg1() { return _arg1; }

  // Implementation of Expr public virtual functions
  void Solve(PExpr, PExpr&, PExpr&)
    { FATAL_ASSERT_MSG(FALSE, ("Should never have to solve for bit-and")); }
  void ForAllChildren(void (Expr::*f)()) { (_arg0->*f)(); (_arg1->*f)(); }
  PExpr ReplaceChildren(PExpr (Expr::*f)())
    { return NewSig((_arg0->*f)(), (_arg1->*f)(), this); }

  // Implementation of Bit_Expr public virtual functions
  int ComputeNumBits() const { return Bit_Expr::NumBits(_arg0); }

  // Static functions
  static PExpr Parse(Symbol, int, PExpr*);
  static PExpr NewSig(PExpr, PExpr, PExpr);
  static PExpr New(PExpr pexpr0, PExpr pexpr1)
    { return NewSig(pexpr0, pexpr1, NULL)->EC()->Simp(); }
};

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: Bit_Or_Expr							     //
// Description: Class for bit-wise negation of bit-vectors                   //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
class Bit_Or_Expr : public Bit_Expr {
private:
  // Data
  PExpr _arg0;
  PExpr _arg1;

  // Constructor
  Bit_Or_Expr(PExpr pexpr0, PExpr pexpr1);

  // Initialization function called by Bit_Expr::Init()
  friend void Bit_Expr::Init();
  static void Init() { BITOR_SORT = Install_Operator(BITOR_SYM, Parse); }

  // Implementation of Expr protected virtual functions
  PExpr Copy() const { return new Bit_Or_Expr(_arg0, _arg1); }
  Bool TypeCheck();
  void Print1(ostream&) const;
  int Hash1() const { return abs(int(_arg0)*23+int(_arg1)); }
  int Match1(PCExpr) const;
  void FindBestSplitter1(Bool);

public:
  // Constants or statics
  static const Symbol BITOR_SYM;
  static int BITOR_SORT;

  // Access functions
  PExpr arg0() { return _arg0; }
  PExpr arg1() { return _arg1; }

  // Implementation of Expr public virtual functions
  void Solve(PExpr, PExpr&, PExpr&)
    { FATAL_ASSERT_MSG(FALSE, ("Should never have to solve for bit-or")); }
  void ForAllChildren(void (Expr::*f)()) { (_arg0->*f)(); (_arg1->*f)(); }
  PExpr ReplaceChildren(PExpr (Expr::*f)())
    { return NewSig((_arg0->*f)(), (_arg1->*f)(), this); }

  // Implementation of Bit_Expr public virtual functions
  int ComputeNumBits() const { return Bit_Expr::NumBits(_arg0); }

  // Static functions
  static PExpr Parse(Symbol, int, PExpr*);
  static PExpr NewSig(PExpr, PExpr, PExpr);
  static PExpr New(PExpr pexpr0, PExpr pexpr1)
    { return NewSig(pexpr0, pexpr1, NULL)->EC()->Simp(); }
};

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: Bit_And_Expr							     //
// Description: Class for bit-wise negation of bit-vectors                   //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
class Bit_Xor_Expr : public Bit_Expr {
private:
  // Data
  PExpr _arg0;
  PExpr _arg1;

  // Constructor
  Bit_Xor_Expr(PExpr pexpr0, PExpr pexpr1);

  // Initialization function called by Bit_Expr::Init()
  friend void Bit_Expr::Init();
  static void Init() { BITXOR_SORT = Install_Operator(BITXOR_SYM, Parse); }

  // Implementation of Expr protected virtual functions
  PExpr Copy() const { return new Bit_Xor_Expr(_arg0, _arg1); }
  Bool TypeCheck();
  void Print1(ostream&) const;
  int Hash1() const { return abs(int(_arg0)*23+int(_arg1)); }
  int Match1(PCExpr) const;
  void FindBestSplitter1(Bool);

public:
  // Constants xor statics
  static const Symbol BITXOR_SYM;
  static int BITXOR_SORT;

  // Access functions
  PExpr arg0() { return _arg0; }
  PExpr arg1() { return _arg1; }

  // Implementation of Expr public virtual functions
  void Solve(PExpr, PExpr&, PExpr&)
    { FATAL_ASSERT_MSG(FALSE, ("Should never have to solve for bit-xor")); }
  void ForAllChildren(void (Expr::*f)()) { (_arg0->*f)(); (_arg1->*f)(); }
  PExpr ReplaceChildren(PExpr (Expr::*f)())
    { return NewSig((_arg0->*f)(), (_arg1->*f)(), this); }

  // Implementation of Bit_Expr public virtual functions
  int ComputeNumBits() const { return Bit_Expr::NumBits(_arg0); }

  // Static functions
  static PExpr Parse(Symbol, int, PExpr*);
  static PExpr NewSig(PExpr, PExpr, PExpr);
  static PExpr New(PExpr pexpr0, PExpr pexpr1)
    { return NewSig(pexpr0, pexpr1, NULL)->EC()->Simp(); }
};

#endif