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


#include <dictionary.h>
#include <hash.h>
#include <expr.h>


static int cf(int x, int y) { return (x<y) ? -1 : (x==y) ? 0 : 1; }  // compare
static int hf(const int x) { return x; }                             // hash
static int mf(const int x, const int y) { return x==y; }             // match


typedef Hash_Table<int, Bool> CareSet;
typedef Hash_Ptr<int, Bool> CareSetPtr;
typedef Dict<int, CareSet*> Queue;
typedef Dict_Ptr<int, CareSet*> QueuePtr;
typedef Hash_Table<int, int> Table;
typedef Hash_Ptr<int, int> TablePtr;


static void update_queue(Queue *q, int e, CareSet *cs_prime)
{
  CareSet **cs=q->Fetch(e);

  // if there is already an entry for this expr,
  // AND the new careset with the old careset

  if (cs) {
    CareSetPtr p(*cs);
    while (p!=NULL) {
      if (!cs_prime->Fetch(p->Key()) ||
	  (*cs_prime)[p->Key()]!=p->Data()) {
	int key=p->Key();
	++p;
	(*cs)->Delete(key);
      }
      else
	++p;
    }
  }

  else
    q->Insert(e, new CareSet(*cs_prime));
}


PExpr substitute(PExpr, Table *init_st=NULL);
static PExpr do_substitute(PExpr e) { return substitute(e); }

PExpr substitute(PExpr e, Table *init_st)
{
  static Table *memoize;
  static Table *st;

  // initialize?

  if (init_st) {
    if (memoize) delete memoize;
    memoize = new Table(hf, mf);
    st = init_st;
  }

  // atomic things don't change

  if (e->IsAtomic())
    return e;

  // has the result been memoized?

  int *result=memoize->Fetch(e->ExprNum());
  if (result) 
    return Expr::Lookup(*result);

  // do substitution?

  int *subs=st->Fetch(e->ExprNum());
  if (subs)
    return substitute(Expr::Lookup(*subs));

  // build new expr with all sub-exprs substituted

  PExpr eNew = e->ReplaceChildren(&do_substitute);
  IF_DEBUG(int rc =) memoize->Insert(e->ExprNum(), eNew->ExprNum());
  ASSERT_MSG(!rc, ("entry already in table"));
  return eNew;
}


static CareSet *c_ptr = NULL;
static Queue *q_ptr = NULL;
static void do_update(PExpr e) { update_queue(q_ptr, e->ExprNum(), c_ptr); }


PExpr ite_simplify(PExpr e)
{
  Queue q(cf);
  Table st(hf, mf);

  // go through all the exprs in reverse topological order
  // and build up the substitution table

  q.Insert(e->ExprNum(), new CareSet(hf, mf));
  for (QueuePtr p(&q); p!=NULL; ++p) {
    PExpr e=Expr::Lookup(p->Key());
    CareSet cs(*p->Data());

    // free up memory so that we don't
    // run out of the stuff!

    delete p->Data();
    p->Data() = NULL;

    if (e->IsAtomic())
      continue;

    // can we simplify an ite because its 
    // ifpart belongs to the care set?

    if (e->Sort()==ITE_SORT) {
      const PITE_Expr &ite = PITE_Expr(e);
      Bool *v = cs.Fetch(ite->ifpart()->ExprNum());
      if (v) {
	if (*v==TRUE) {
	  IF_DEBUG(int rc =)
	  st.Insert(ite->ExprNum(), ite->thenpart()->ExprNum());
	  assert_msg(!rc, ("entry already in table"));
	  update_queue(&q, ite->thenpart()->ExprNum(), &cs);
	}
	else { /* v==FALSE */
	  IF_DEBUG(int rc =)
	  st.Insert(ite->ExprNum(), ite->elsepart()->ExprNum());
	  assert_msg(!rc, ("entry already in table"));
	  update_queue(&q, ite->elsepart()->ExprNum(), &cs);
	}
	continue;
      }
    }

    // add children to the queue, updating their caresets
    // in the case of an ite-expr

    if (e->Sort()==ITE_SORT) {
      CareSet cs_prime(cs);
      const PITE_Expr &ite=PITE_Expr(e);
      update_queue(&q, ite->ifpart()->ExprNum(), &cs);

      // add if-part==TRUE to the care-set for the then-part

      IF_DEBUG(int rc =) cs_prime.Insert(ite->ifpart()->ExprNum(), TRUE);
      assert_msg(!rc, ("entry already in table"));
      update_queue(&q, ite->thenpart()->ExprNum(), &cs_prime);

      // add if-part==FALSE to the care-set for the else-part

      cs_prime[ite->ifpart()->ExprNum()]=FALSE;
      update_queue(&q, ite->elsepart()->ExprNum(), &cs_prime);
    }

    else {
      q_ptr = &q;  c_ptr = &cs;
      e->ForAllChildren(&do_update);
    }
  }

  // perform all the substituations

  return substitute(e, &st);
}