/********************************************************************
 * AUTHORS: Vijay Ganesh, David L. Dill
 *
 * BEGIN DATE: April, 2006
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/

// -*- c++ -*-

// Simplifying create methods for Boolean operations.
// These are only very simple local simplifications.

// This is somewhat redundant with Vijay's simplifier code.  They
// need to be merged.
// FIXME: control with optimize flag.

static bool _trace_simpbool = 0;
static bool _disable_simpbool = 0;

#include "AST.h"

// SMTLIB experimental hack.  Try allocating a single stack here for
// children to reduce growing of vectors.
//BEEV::ASTVec child_stack;

namespace BEEV {

  ASTNode BeevMgr::CreateSimpForm(Kind kind, ASTVec &children = _empty_ASTVec) {
    if (_disable_simpbool) {
      return CreateNode(kind, children);
    }
    else {
      switch (kind) {
      case NOT: return CreateSimpNot(children[0]); break; 
      case AND: return CreateSimpAndOr(1, children); break; 
      case OR: return CreateSimpAndOr(0, children); break;
      case NAND: return CreateSimpNot(CreateSimpAndOr(1, children)); break;
      case NOR: return CreateSimpNot(CreateSimpAndOr(0, children)); break;
      case IFF: {
	// Not sure children can ever be empty, but what the heck.
	//	if (children.size() == 0) {
	//	  return ASTTrue;
	//	}
	// Convert IFF to XOR ASAP.  IFF is not associative, so this makes
	// flattening much easier.
	children[0] = CreateSimpNot(children[0]);
	return CreateSimpXor(children); break;
      }
      case XOR: 
	return CreateSimpXor(children); break;
	// FIXME: Earlier, check that this only has two arguments
      case IMPLIES: return CreateSimpAndOr(0, CreateSimpNot(children[0]), children[1]); break;
      case ITE: return CreateSimpFormITE(children[0], children[1], children[2]);
      default: return CreateNode(kind, children);
      }
    }
  }

  // specialized versions
  
  ASTNode BeevMgr::CreateSimpForm(Kind kind,
				  const ASTNode& child0) {
    ASTVec children;
    //child_stack.clear();	// could just reset top pointer.
    children.push_back(child0);
    //child_stack.push_back(child0);
    return CreateSimpForm(kind, children);
    //return CreateSimpForm(kind, child_stack);
  }
  
  ASTNode BeevMgr::CreateSimpForm(Kind kind,
				  const ASTNode& child0,
				  const ASTNode& child1) {
    ASTVec children;
    //child_stack.clear();	// could just reset top pointer.
    children.push_back(child0);
    //child_stack.push_back(child0);
    children.push_back(child1);
    //child_stack.push_back(child1);
    return CreateSimpForm(kind, children);
    //return CreateSimpForm(kind, child_stack);
  }
  
  
  ASTNode BeevMgr::CreateSimpForm(Kind kind,
				  const ASTNode& child0,
				  const ASTNode& child1,
				  const ASTNode& child2) {
    ASTVec children;
    //child_stack.clear();	// could just reset top pointer.
    children.push_back(child0);
    //child_stack.push_back(child0);
    children.push_back(child1);
    //child_stack.push_back(child1);
    children.push_back(child2);
    //child_stack.push_back(child2);
    return CreateSimpForm(kind, children);
    //return CreateSimpForm(kind, child_stack);
  }
    
  ASTNode BeevMgr::CreateSimpNot(const ASTNode& form) {
    Kind k = form.GetKind();
    switch (k) {
    case FALSE: { return ASTTrue; }
    case TRUE: { return ASTFalse; }
    case NOT: { return form[0]; } // NOT NOT cancellation
    case XOR: {
      // Push negation down in this case.
      // FIXME: Separate pre-pass to push negation down?
      // CreateSimp should be local, and this isn't.  
      // It isn't memoized.  Arg.
      ASTVec children = form.GetChildren();
      children[0] = CreateSimpNot(children[0]);
      return CreateSimpXor(children);
    }
    default: { return CreateNode(NOT, form); }
    }
  }

  // I don't think this is even called, since it called
  // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no
  // ill effects.  Calls seem to go to the version that takes a vector
  // of children.
  ASTNode BeevMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2) {
    ASTVec children;
    children.push_back(form1);
    children.push_back(form2);
    return CreateSimpXor(children);
  }


  ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2) {
    ASTVec children;
    children.push_back(form1);
    children.push_back(form2);
    return CreateSimpAndOr(IsAnd, children);
  }

  ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, ASTVec &children) {

    if (_trace_simpbool) {
      cout << "========" << endl << "CreateSimpAndOr " << (IsAnd ? "AND " : "OR ") ;
      lpvec(children);
      cout << endl;
    }

    ASTVec new_children;

    // sort so that identical nodes occur in sequential runs, followed by
    // their negations.

    SortByExprNum(children);
    
    ASTNode annihilator = (IsAnd ? ASTFalse : ASTTrue);
    ASTNode identity = (IsAnd ? ASTTrue : ASTFalse);

    ASTNode retval;

    ASTVec::const_iterator it_end = children.end();
    ASTVec::const_iterator next_it;
    for(ASTVec::const_iterator it = children.begin(); it != it_end; it = next_it) {
      next_it = it + 1;
      bool nextexists = (next_it < it_end);

      if (*it == annihilator) {
	retval = annihilator;
	if (_trace_simpbool) {
	  cout << "returns " << retval << endl;
	}
	return retval;
      }
      else if (*it == identity) {
	// just drop it
      }
      else if (nextexists && (*next_it == *it)) {
	// drop it
	//	cout << "Dropping [" << it->GetNodeNum() << "]" << endl;
      }
      else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) {
	// form and negation -- return FALSE for AND, TRUE for OR.
	retval = annihilator;
	// cout << "X and/or NOT X" << endl; 
	if (_trace_simpbool) {
	  cout << "returns " << retval << endl;
	}
	return retval;
      }
      else {
	// add to children
	new_children.push_back(*it);
      }
    }

    // If we get here, we saw no annihilators, and children should
    // be only the non-True nodes.
    if (new_children.size() < 2) {
      if (0 == new_children.size()) {
	retval = identity;
      }
      else {
	// there is just one child
	retval = new_children[0];
      }
    }
    else {
      // 2 or more children.  Create a new node.
      retval = CreateNode(IsAnd ? AND : OR, new_children);
    }
    if (_trace_simpbool) {
      cout << "returns " << retval << endl;
    }
    return retval;
  }


  // Constant children are accumulated in "accumconst".  
  ASTNode BeevMgr::CreateSimpXor(ASTVec &children) {

    if (_trace_simpbool) {
      cout << "========" << endl
	   << "CreateSimpXor ";
      lpvec(children);
      cout << endl;
    }

    // Change this not to init to children if flattening code is present.
    // ASTVec flat_children = children;		// empty vector

    ASTVec flat_children;		// empty vector

    ASTVec::const_iterator it_end = children.end();

    if (xor_flatten) {

      bool fflag = 0;		// ***Temp debugging
      
      // Experimental flattening code.
      
      for(ASTVec::iterator it = children.begin(); it != it_end; it++) {
	Kind ck = it->GetKind();
	const ASTVec &gchildren = it->GetChildren();
	if (XOR == ck) {
	  fflag = 1;
	  // append grandchildren to children
	  flat_children.insert(flat_children.end(), gchildren.begin(), gchildren.end());
	}
	else {
	  flat_children.push_back(*it);
	}
      }
      
      if (_trace_simpbool && fflag) {
	cout << "========" << endl;
	cout << "Flattening: " << endl;
	lpvec(children);
	
	cout << "--------" << endl;
	cout << "Flattening result: " << endl;
	lpvec(flat_children);
      }
    }
    else {
      flat_children = children;
    }
      

    // sort so that identical nodes occur in sequential runs, followed by
    // their negations.
    SortByExprNum(flat_children);

    ASTNode retval;

    // This is the C Boolean value of all constant args seen.  It is initially
    // 0.  TRUE children cause it to change value.
    bool accumconst = 0;

    ASTVec new_children;

    it_end = flat_children.end();
    ASTVec::iterator next_it;
    for(ASTVec::iterator it = flat_children.begin(); it != it_end; it++) {
      next_it = it + 1;
      bool nextexists = (next_it < it_end);

      if (ASTTrue == *it) {
	accumconst = !accumconst;
      }
      else if (ASTFalse == *it) {
	// Ignore it
      }
      else if (nextexists && (*next_it == *it)) {
	// x XOR x = FALSE.  Skip current, write "false" into next_it
	// so that it gets tossed, too.
	*next_it = ASTFalse;
      }
      else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it)) {
	// x XOR NOT x = TRUE.  Skip current, write "true" into next_it
	// so that it gets tossed, too.
	*next_it = ASTTrue;
      }
      else if (NOT == it->GetKind()) {
	// If child is (NOT alpha), we can flip accumconst and use alpha.
	// This is ok because (NOT alpha) == TRUE XOR alpha
	accumconst = !accumconst;
	// CreateSimpNot just takes child of not.
	new_children.push_back(CreateSimpNot(*it));
      }
      else {
	new_children.push_back(*it);
      }
    }

    // Children should be non-constant.
    if (new_children.size() < 2) {
      if (0 == new_children.size()) {
	// XOR(TRUE, FALSE) -- accumconst will be 1.
	if (accumconst) {
	  retval = ASTTrue;
	}
	else {
	  retval = ASTFalse;
	}
      }
      else {
	// there is just one child
	// XOR(x, TRUE) -- accumconst will be 1.
	if (accumconst) {
	  retval =  CreateSimpNot(new_children[0]);
	}
	else {
	  retval = new_children[0];
	}
      }
    }
    else {
      // negate first child if accumconst == 1
      if (accumconst) {
	new_children[0] = CreateSimpNot(new_children[0]);
      }
      retval = CreateNode(XOR, new_children);
    }

    if (_trace_simpbool) {    
      cout << "returns " << retval << endl;
    }
    return retval;
  }

  // FIXME:  How do I know whether ITE is a formula or not?
  ASTNode BeevMgr::CreateSimpFormITE(const ASTNode& child0,
				     const ASTNode& child1,
				     const ASTNode& child2) {

    ASTNode retval;
    
    if (_trace_simpbool) {
      cout << "========" << endl << "CreateSimpFormITE "
	   << child0 
	   << child1 
	   << child2 << endl;
    }

    if (ASTTrue == child0) {
      retval = child1;
    }
    else if (ASTFalse == child0) {
      retval = child2;
    }
    else if (child1 == child2) {
      retval = child1;
    }    
    // ITE(x, TRUE, y ) == x OR y
    else if (ASTTrue == child1) {
      retval = CreateSimpAndOr(0, child0, child2);
    }
    // ITE(x, FALSE, y ) == (!x AND y)
    else if (ASTFalse == child1) {
      retval = CreateSimpAndOr(1, CreateSimpNot(child0), child2); 
    }
    // ITE(x, y, TRUE ) == (!x OR y)
    else if (ASTTrue == child2) {
      retval = CreateSimpAndOr(0, CreateSimpNot(child0), child1); 
    }
    // ITE(x, y, FALSE ) == (x AND y)
    else if (ASTFalse == child2) {
      retval = CreateSimpAndOr(1, child0, child1); 
    }
    // ITE (x, !y, y) == x XOR y
//     else if (NOT == child1.GetKind() && (child1[0] == child2)) {
//       retval = CreateSimpXor(child0, child2);
//     }
//     // ITE (x, y, !y) == x IFF y.  I think other cases are covered
//     // by XOR/IFF optimizations
//     else if (NOT == child2.GetKind() && (child2[0] == child1)) {
//       retval = CreateSimpXor(CreateSimpNot(child0), child2);
//     }
    else {
      retval = CreateNode(ITE, child0, child1, child2);
    }

    if (_trace_simpbool) {
      cout << "returns " << retval << endl;
    }

    return retval;
  }
} // BEEV namespace