/* Copyright (c) 2001 by the Institute for Computer Science,               */
/* Alberts-Ludwigs-University of Freiburg, Germany.                        */
/* All Rights Reserved.  This software is for educational purposes only.   */
/* Permission is given to distribute this code provided that this intro-   */
/* ductory message is not removed and no monies are exchanged.             */
/* No guarantee is expressed or implied by the distribution of this code.  */
/* Software written by Alberto Lluch Lafuente and Stefan Edelkamp.         */
/* References:                                                             */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Directed Explicit Model Checking with HSF-SPIN, to appear in:         */
/*   Proc. 8th International SPIN Workshop on Model Checking Software,     */
/*   Springer LNCS 2057, Toronto, May 2001                                 */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Protocol Verification with Heuristic Search,                          */
/*   Proc. AAAI Spring Symposium on Model-Based Validation of Inteligence, */
/*   AAAI, Stanford, April 2001.                                           */
/* Send bug-reports or questions to: lafuente@informatik.uni-freiburg.de   */

#ifndef __BITSTATE_HASHTABLE_
#define __BITSTATE_HASHTABLE_

#include <stdio.h>                                 
#include <stdlib.h>
#include <global.h>


class BitStateHashTable{
 public:
  unsigned char *ba;
  int size;
  int max;
  
  BitStateHashTable(int m);
  void init();
  ~BitStateHashTable();
  void hash(PackedState& ps);
  State* search(State *S);
  void insert(State *S); 
  void remove(State *S); 
};


BitStateHashTable::BitStateHashTable(int m): size(0), max(m) {
  ssize=m; mask = ((1<<ssize)-1);
  ba = new unsigned char[1<<(m-3)];
}

void BitStateHashTable::init(){
  memset(ba, 0, 1<<(max-3));
}

BitStateHashTable::~BitStateHashTable() {
  delete ba;
}

State *BitStateHashTable::search (State *S) {
  d_hash((unsigned char*)S->ps,S->ps->_vsz);
  return (State*)((ba[j2]&j3) && (ba[j1]&j4));
}

void BitStateHashTable::insert (State *S) {
  d_hash((unsigned char*)S->ps,S->ps->_vsz);
  ba[j2]|= j3; ba[j1]|= j4;
  size++;
}

void BitStateHashTable::remove (State *S) {
  d_hash((unsigned char*)S->ps,S->ps->_vsz);
  ba[j2]&= (~j3); ba[j1]&= (~j4);
  size--;
}

#endif //
