///////////////////////////////////////////////////////////////////////////////
//                                                                           //
//  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 cf1(int x, int y) { return (x<y) ? -1 : (x==y) ? 0 : 1; } // compare
static int cf2(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, PExpr> Queue;
typedef Dict_Ptr<int, PExpr> QueuePtr;
typedef Hash_Table<int, int> Table;
typedef Hash_Ptr<int, int> TablePtr;


class ITE_Tree {
private:
  Queue _conds;
  PExpr _leaf;
  PExpr _branch;

public:
  enum Tree_Type { NAND_TREE, OR_TREE };
  static Tree_Type _type;

  ITE_Tree(PExpr leaf) : _conds(&cf2), _leaf(leaf), _branch(NULL) {}
  ITE_Tree(ITE_Tree &t) : _conds(t._conds), _leaf(t._leaf), 
    _branch(t._branch) {}
  int NumConds() { return _conds.NumEntries(); }
  void AddCond(PExpr e) { _conds.Insert(e->ExprNum(), e); }
  void SetBranch(PExpr e) 
    { assert_msg(!_branch, ("unexpected value")); _branch=e; }
  PExpr Leaf() { return _leaf; }
  void SetLeaf(PExpr l) { _leaf=l; }
  PExpr Normalize();
};


ITE_Tree::Tree_Type ITE_Tree::_type;
typedef PExpr (ITE_Expr::*Func_Type)();
Func_Type leaf;
Func_Type trunk;
extern PExpr substitute(PExpr e, Table *init_st=NULL);


PExpr ITE_Tree::Normalize()
{
  assert_msg(_branch && _leaf, ("undefined values"));
  PExpr e=_branch;
  
  // produce an expr representing the normalized OR/NAND tree

  for (QueuePtr p(&_conds); p!=NULL; ++p) {
    switch (_type) {
    case OR_TREE:     e=ITE_Expr::New(p->Data(), _leaf, e);  break;
    case NAND_TREE:   e=ITE_Expr::New(p->Data(), e, _leaf);  break;
    default:          assert_msg(0, ("missing case statement"));
    }
  }
  
  return e;
}
  

void build_ite_tree(PExpr e, ITE_Tree *t, Table *st)
{
  // recursively move down the OR/NAND tree collecting
  // splitters until the leaf node is encountered

  if (e->Sort()==ITE_SORT &&
      (PITE_Expr(e)->*leaf)()==t->Leaf()) {
    const PITE_Expr &ite=PITE_Expr(e);

    // add the splitter and keep on looking for
    // more to add to the tree

    build_ite_tree((ite->*trunk)(), t, st);
    t->AddCond(ite->ifpart());

    if (t->NumConds() > 1) {
      PExpr e_prime=t->Normalize();
      if (e_prime!=e)
	st->Insert(e->ExprNum(), e_prime->ExprNum());
    }
  }

  else    
    // leaf node found
    t->SetBranch(e);
}


static Queue *q_ptr=NULL;
static void add_to_queue(PExpr e) { q_ptr->Insert(e->ExprNum(), NULL); }

PExpr ite_reorder1(PExpr e)
{
  static Table *st=new Table(&hf, &mf);

  Queue q(&cf1);
  q_ptr = &q;
  q.Insert(e->ExprNum(), NULL);

  // go through all the expressions in reverse topological order,
  // putting ite-trees in (pseudo) normal form where ever possible

  for (QueuePtr p(&q); p!=NULL; ++p) {
    PExpr e=Expr::Lookup(p->Key());

    if (e->IsAtomic())
      continue;

    // if there is a chain of ite's put them in normal form

    if (!st->Fetch(p->Key())) {
      if (e->Sort()==ITE_SORT) {
	const PITE_Expr &ite=PITE_Expr(e);

	if ((ite->*trunk)()->Sort()==ITE_SORT &&
	    ((PITE_Expr((ite->*trunk)()))->*leaf)()==(ite->*leaf)()) {
	  ITE_Tree *t=new ITE_Tree((ite->*leaf)());
	  build_ite_tree((ite->*trunk)(), t, st);
	  t->AddCond(ite->ifpart());
	  PExpr e_prime=t->Normalize();
	  if (e!=e_prime)
	    st->Insert(e->ExprNum(), e_prime->ExprNum());
	}
      }
    }

    // recursively put children in normal form

    e->ForAllChildren(&add_to_queue);
  }

  return substitute(e, st);
}


PExpr ite_reorder(PExpr e)
{
  // first reorder or-trees, then nand-trees

  ITE_Tree::_type = ITE_Tree::OR_TREE;
  trunk = &ITE_Expr::elsepart;
  leaf = &ITE_Expr::thenpart;
  e=ite_reorder1(e);
  
  ITE_Tree::_type = ITE_Tree::NAND_TREE;
  trunk = &ITE_Expr::thenpart;
  leaf = &ITE_Expr::elsepart;
  return ite_reorder1(e);
}