/**CFile***********************************************************************

  FileName    [puresatAig.c]

  PackageName [puresat]

  Synopsis    [Abstraction refinement for large scale invariant checking.]

  Description [This file contains the functions to check invariant properties
  by the PureSAT abstraction refinement algorithm, which is entirely based on
  SAT solver, the input of which could be either CNF or AIG. It has several
  parts:

  * Localization-reduction base Abstraction
  * K-induction or interpolation to prove the truth of a property
  * Bounded Model Checking to find bugs
  * Incremental concretization based methods to verify abstract bugs
  * Incremental SAT solver to improve efficiency
  * UNSAT proof based method to obtain refinement
  * AROSAT to bring in only necessary latches into unsat proofs
  * Bridge abstraction to get compact coarse refinement
  * Refinement minization to guarrantee minimal refinements
  * Unsat proof-based refinement minimization to eliminate multiple candidate
    by on SAT test
  * Refinement prediction to decrease the number of refinement iterations
  * Dynamic switching to redistribute computional resources to improve
    efficiency

  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure", "Efficient computation
  of small abstraction refinements", and "Efficient abstraction refinement in
  interpolation-based unbounded model checking"]

  Author      [Bing Li]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without
  license or royalty fees, to use, copy, modify, and distribute this
  software and its documentation for any purpose, provided that the
  above copyright notice and the following two paragraphs appear in
  all copies of this software.]

******************************************************************************/
#include "maigInt.h"
#include "baig.h"
#include "ntk.h"
#include "puresatInt.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/**AutomaticEnd***************************************************************/

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [For AIG recovery--unconnect output for nodes eliminated]

  Description [For AIG recovery--unconnect output for nodes eliminated]

  SideEffects []

  SeeAlso     []

******************************************************************************/

void
PureSat_unconnectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to)
{
   bAigEdge_t cur, *pfan, *newfan;
   int i, nfan,find=0;

  from = bAig_NonInvertedEdge(from);
  to = bAig_NonInvertedEdge(to);

  pfan = (bAigEdge_t *)fanout(from);
  nfan = nFanout(from);
  newfan = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*(nfan));
  for(i=0; i<nfan; i++) {
    cur = pfan[i];
    cur = cur >> 1;
    cur = bAig_NonInvertedEdge(cur);
    if(cur == to) {
      find = 1;
      memcpy(newfan, pfan, sizeof(bAigEdge_t)*i);
      memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(bAigEdge_t)*(nfan-i-1));
      newfan[nfan-1] = 0;

      fanout(from) = (bAigEdge_t)newfan;


      free(pfan);
      nFanout(from) = nfan-1;
      break;
    }
  }
  assert(find);
}


/**Function********************************************************************

  Synopsis    [for AIG generation---create connection between new and
	      old aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

void
PureSat_connectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to,
   int inputIndex)
{
  bAigEdge_t *pfan;
  bAigEdge_t nfan;

  to = bAig_NonInvertedEdge(to);
  pfan = (bAigEdge_t *)fanout(from);
  nfan = nFanout(from);
  if(nfan == 0) pfan = malloc((sizeof(bAigEdge_t)*2));
  else          pfan = realloc(pfan, sizeof(bAigEdge_t)*(nfan+2));
  to += bAig_IsInverted(from);
  to = to << 1;
  to += inputIndex;
  pfan[nfan++] = to;
  pfan[nfan] = 0;
  fanout(from) = (bAigEdge_t)pfan;
  nFanout(from) = nfan;
}


/**Function********************************************************************

  Synopsis    [Check whether a node has been created or not]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_HashTableLookup(
  bAig_Manager_t *manager,
  bAigEdge_t  node1,
  bAigEdge_t  node2)
{
  bAigEdge_t key = HashTableFunction(node1, node2);
  bAigEdge_t node;

  node = manager->HashTableArray[manager->class_][key];
  if  (node == bAig_NULL) {
    return bAig_NULL;
  }
  else{
    while ( (rightChild(bAig_NonInvertedEdge(node)) != node2) ||
	    (leftChild(bAig_NonInvertedEdge(node))  != node1)) {

      if (next(bAig_NonInvertedEdge(node)) == bAig_NULL){
	return(bAig_NULL);
      }
      node = next(bAig_NonInvertedEdge(node)); /* Get the next Node */
    } /* While loop */
    return(node);

  } /* If Then Else */

} /* End of HashTableLookup() */


/**Function********************************************************************

  Synopsis    [Add one new node to hash table]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

int
PureSat_HashTableAdd(
  bAig_Manager_t   *manager,
  bAigEdge_t  nodeIndexParent,
  bAigEdge_t  nodeIndex1,
  bAigEdge_t  nodeIndex2)
{
  bAigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
  bAigEdge_t nodeIndex;
  bAigEdge_t node;

  nodeIndex = manager->HashTableArray[manager->class_][key];
  if  (nodeIndex == bAig_NULL) {
    manager->HashTableArray[manager->class_][key] = nodeIndexParent;
    return TRUE;
  }
  else{
    node = nodeIndex;
    nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));  /* Get the Node */
    while (nodeIndex != bAig_NULL) {
      node = nodeIndex;
      nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
    }
    next(bAig_NonInvertedEdge(node)) = nodeIndexParent;
    return TRUE;
  }

}



/**Function********************************************************************

  Synopsis    [Create a node for AND operation]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_CreateAndNode(
   bAig_Manager_t  *manager,
   bAigEdge_t node1,
   bAigEdge_t node2)
{

  bAigEdge_t varIndex;
  char       *name = NIL(char);
  char       *node1Str = util_inttostr(node1);
  char       *node2Str = util_inttostr(node2);
  long class_ = manager->class_;

  name = util_strcat4("Nd", node1Str,"_", node2Str);
  while (st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
    fprintf(vis_stdout, "Find redundant node at %ld %ld\n", node1, node2);
    name = util_strcat3(name, node1Str, node2Str);
  }
  FREE(node1Str);
  FREE(node2Str);
  varIndex = bAig_CreateNode(manager, node1, node2);
  if (varIndex == bAig_NULL){
    FREE(name);
    return (varIndex);
  }
  /* Insert the varaible in the Symbol Table */
  st_insert(manager->SymbolTableArray[class_], name, (char*) (long) varIndex);
  manager->nameList[bAigNodeID(varIndex)] = name;

  return(varIndex);

}


/**Function********************************************************************

  Synopsis    [And function for 2 aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_And2(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
  bAigEdge_t newNodeIndex;

    newNodeIndex = PureSat_CreateAndNode(manager, nodeIndex1, nodeIndex2) ;

    PureSat_HashTableAdd(manager, newNodeIndex, nodeIndex1, nodeIndex2);
    PureSat_connectOutput(manager, nodeIndex1, newNodeIndex, 0);
    PureSat_connectOutput(manager, nodeIndex2, newNodeIndex, 1);

  return newNodeIndex;

}


/**Function********************************************************************

  Synopsis    [And function for 3 aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_And3(
	   bAig_Manager_t *manager,
	   bAigEdge_t l,
	   bAigEdge_t r)
{
  int caseIndex, caseSig;
  bAigEdge_t rl, rr;

  rl = leftChild(r);
  rr = rightChild(r);

  caseIndex = 0; /* (a)(b c) */
  if(bAigCompareNode(l, rl)) {
    caseIndex = 1; /* (a)(a b) */
  }
  else if(bAigCompareNode(l, rr)) {
    caseIndex = 2; /* (a)(b a) */
  }

  caseSig = 0;
  if(bAig_IsInverted(l))  caseSig += 8;
  if(bAig_IsInverted(rl)) caseSig += 4;
  if(bAig_IsInverted(rr)) caseSig += 2;
  if(bAig_IsInverted(r))  caseSig += 1;
  if(caseIndex == 0) {
    return(PureSat_And2(manager, l, r));
  }
  else if(caseIndex == 1) {
    switch(caseSig) {
	case 2 :
	case 0 :
	case 14 :
	case 12 :
      return(r);
	case 10 :
	case 8 :
	case 6 :
	case 4 :
      return(bAig_Zero);
	case 3 :
	case 1 :
	case 15 :
	case 13 :
      return(PureSat_And(manager, rl, bAig_Not(rr)));
	case 11 :
	case 9 :
	case 7 :
	case 5 :
      return(l);
    }
  }
  else if(caseIndex == 2) {
    switch(caseSig) {
	case 4 :
	case 0 :
	case 14 :
	case 10 :
      return(r);
	case 12 :
	case 8 :
	case 6 :
	case 2 :
      return(bAig_Zero);
	case 5 :
	case 1 :
	case 15 :
	case 11 :
      return(PureSat_And(manager, bAig_Not(rl), rr));
	case 13 :
	case 9 :
	case 7 :
	case 3 :
      return(l);
    }
  }
  return(0);
}


/**Function********************************************************************

  Synopsis    [And function for 4 aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_And4(
	   bAig_Manager_t *manager,
	   bAigEdge_t l,
	   bAigEdge_t r)
{
  int caseIndex, caseSig;
  bAigEdge_t ll, lr, rl, rr;
  bAigEdge_t t1, t2;

  ll = leftChild(l);
  lr = rightChild(l);
  rl = leftChild(r);
  rr = rightChild(r);

  if(bAigCompareNode(l, rl) ||
     bAigCompareNode(l, rr)) {
    return(PureSat_And3(manager, l, r));
  }
  else if(bAigCompareNode(r, ll) ||
     bAigCompareNode(r, lr)) {
    return(PureSat_And3(manager, r, l));
  }

  if(ll > lr+1) bAigSwap(ll, lr);
  if(rl > rr+1) bAigSwap(rl, rr);

  caseIndex = 0; /* (a b)(c d) */
  if(bAigCompareNode(ll, rl)) {
    if(bAigCompareNode(lr, rr)) {
      caseIndex = 4; /* (a b) (a b) */
    }
    else {
      caseIndex = 1; /* (a b) (a c) */
      if(lr > rr+1) {
	bAigSwap(ll, rl);
	bAigSwap(lr, rr);
	bAigSwap(l, r);
      }
    }
  }
  else if(bAigCompareNode(lr, rl)) {
    caseIndex = 2; /* (b a)(a c) */
  }
  else if(bAigCompareNode(lr, rr)) {
    caseIndex = 3; /* (b a)(c a) */
    if(ll > rl+1) {
      bAigSwap(ll, rl);
      bAigSwap(lr, rr);
      bAigSwap(l, r);
    }
  }
  else if(bAigCompareNode(ll, rr)) {
    /* (a b)(c a)  */
    bAigSwap(ll, rl);
    bAigSwap(lr, rr);
    bAigSwap(l, r);
    caseIndex = 2; /* (c a )(a b) because of c < b */
  }

  caseSig = 0;
  if(bAig_IsInverted(ll)) caseSig += 32;
  if(bAig_IsInverted(lr)) caseSig += 16;
  if(bAig_IsInverted(l))  caseSig += 8;
  if(bAig_IsInverted(rl)) caseSig += 4;
  if(bAig_IsInverted(rr)) caseSig += 2;
  if(bAig_IsInverted(r))  caseSig += 1;

  if(caseIndex == 0) {
    return(PureSat_And2(manager, l, r));
  }
  else if(caseIndex == 1) {
    switch(caseSig) {
	case 19 :
	case 17 :
	case 3 :
	case 1 :
	case 55 :
	case 53 :
	case 39 :
	case 37 :
      t1 = PureSat_And(manager, lr, bAig_Not(rr));
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
	case 18 :
	case 16 :
	case 2 :
	case 0 :
	case 54 :
	case 52 :
	case 38 :
	case 36 :
      t1 = PureSat_And(manager, lr, rr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
	case 26 :
	case 24 :
	case 10 :
	case 8 :
	case 62 :
	case 60 :
	case 46 :
	case 44 :
      t1 = PureSat_And(manager, bAig_Not(lr), rr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
	case 61 :
	case 27 :
	case 25 :
	case 11 :
	case 63 :
	case 47 :
	case 9 :
	case 45 :
      t1 = PureSat_And(manager, bAig_Not(lr), bAig_Not(rr));
      t2 = PureSat_Or(manager, bAig_Not(ll), t1);
      return(t2);
	case 23 :
	case 21 :
	case 7 :
	case 5 :
	case 51 :
	case 49 :
	case 35 :
	case 33 :
      return(l);
	case 30 :
	case 28 :
	case 14 :
	case 12 :
	case 58 :
	case 56 :
	case 42 :
	case 40 :
      return(r);
	case 22 :
	case 20 :
	case 6 :
	case 4 :
	case 50 :
	case 48 :
	case 34 :
	case 32 :
      return(bAig_Zero);
	case 31 :
	case 29 :
	case 15 :
	case 13 :
	case 59 :
	case 57 :
	case 43 :
	case 41 :
      t1 = PureSat_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 2) {
    switch(caseSig) {
	case 35 :
	case 33 :
	case 3 :
	case 1 :
	case 55 :
	case 53 :
	case 23 :
	case 21 :
      t1 = PureSat_And(manager, lr, bAig_Not(rr));
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
	case 34 :
	case 32 :
	case 2 :
	case 0 :
	case 54 :
	case 52 :
	case 22 :
	case 20 :
      t1 = PureSat_And(manager, lr, rr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
	case 42 :
	case 40 :
	case 10 :
	case 8 :
	case 62 :
	case 60 :
	case 30 :
	case 28 :
      t1 = PureSat_And(manager, lr, rr);
      t2 = PureSat_And(manager, bAig_Not(ll), t1);
      return(t2);
	case 43 :
	case 41 :
	case 11 :
	case 9 :
	case 63 :
	case 61 :
	case 31 :
	case 29 :
      t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rr));
      t2 = PureSat_Or(manager, bAig_Not(lr), t1);
      return(t2);
	case 39 :
	case 37 :
	case 7 :
	case 5 :
	case 51 :
	case 49 :
	case 19 :
	case 17 :
      return(l);
	case 46 :
	case 44 :
	case 14 :
	case 12 :
	case 58 :
	case 56 :
	case 26 :
	case 24 :
      return(r);
	case 38 :
	case 36 :
	case 6 :
	case 4 :
	case 50 :
	case 48 :
	case 18 :
	case 16 :
      return(bAig_Zero);
	case 45 :
	case 15 :
	case 13 :
	case 59 :
	case 57 :
	case 47 :
	case 27 :
	case 25 :
      t1 = PureSat_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 3) {
    switch(caseSig) {
	case 37 :
	case 33 :
	case 5 :
	case 1 :
	case 55 :
	case 51 :
	case 23 :
	case 19 :
      t1 = PureSat_And(manager, bAig_Not(rl), lr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
	case 36 :
	case 32 :
	case 4 :
	case 0 :
	case 54 :
	case 50 :
	case 22 :
	case 18 :
      t1 = PureSat_And(manager, rl, lr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
	case 44 :
	case 40 :
	case 12 :
	case 8 :
	case 62 :
	case 58 :
	case 30 :
	case 26 :
      t1 = PureSat_And(manager, rl, lr);
      t2 = PureSat_And(manager, bAig_Not(ll), t1);
      return(t2);
	case 45 :
	case 41 :
	case 13 :
	case 9 :
	case 63 :
	case 59 :
	case 31 :
	case 27 :
      t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rl));
      t2 = PureSat_Or(manager, bAig_Not(lr), t1);
      return(t2);
	case 39 :
	case 35 :
	case 7 :
	case 3 :
	case 53 :
	case 49 :
	case 21 :
	case 17 :
      return(l);
	case 46 :
	case 42 :
	case 14 :
	case 10 :
	case 60 :
	case 56 :
	case 28 :
	case 24 :
      return(r);
	case 38 :
	case 34 :
	case 6 :
	case 2 :
	case 52 :
	case 48 :
	case 20 :
	case 16 :
      return(bAig_Zero);
	case 47 :
	case 43 :
	case 15 :
	case 11 :
	case 61 :
	case 57 :
	case 29 :
	case 25 :
      t1 = PureSat_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 4) {
    switch(caseSig) {
	case 22 :
	case 20 :
	case 6 :
	case 4 :
	case 50 :
	case 48 :
	case 34 :
	case 32 :
	case 2 :
	case 16 :
	case 52 :
	case 1 :
	case 8 :
	case 19 :
	case 26 :
	case 37 :
	case 44 :
	case 38 :
	case 55 :
	case 62 :
      return(bAig_Zero);
	case 0 :
	case 18 :
	case 36 :
	case 54 :
	case 9 :
	case 27 :
	case 45 :
	case 63 :
	case 5 :
	case 23 :
	case 33 :
	case 51 :
	case 3 :
	case 17 :
	case 49 :
	case 7 :
	case 35 :
	case 21 :
	case 39 :
	case 53 :
      return(l);
	case 40 :
	case 58 :
	case 12 :
	case 30 :
	case 24 :
	case 10 :
	case 14 :
	case 56 :
	case 28 :
	case 42 :
	case 60 :
	case 46 :
      return(r);
	case 11 :
	case 47 :
	case 25 :
	case 61 :
      return(bAig_Not(ll));
	case 41 :
	case 59 :
	case 13 :
	case 31 :
      return(bAig_Not(lr));
	case 15 :
      t1 = PureSat_And(manager, ll, bAig_Not(lr));
      t2 = PureSat_And(manager, bAig_Not(ll), lr);
      return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
	case 57 :
      t1 = PureSat_And(manager, rl, bAig_Not(rr));
      t2 = PureSat_And(manager, bAig_Not(rl), rr);
      return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
	case 29 :
      t1 = PureSat_And(manager, ll, lr);
      t2 = PureSat_And(manager, bAig_Not(ll), bAig_Not(lr));
      return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
	case 43 :
      t1 = PureSat_And(manager, rl, rr);
      t2 = PureSat_And(manager, bAig_Not(rl), bAig_Not(rr));
      return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
    }
  }
  return(0);
}



/**Function********************************************************************

  Synopsis    [test whether two level minimization can be enabled--iff the two
	       nodes are in the same timeframe]

  Description [output, l,r,ll,lr,rl,rr must be in the same class to pass the test]

  SideEffects []

  SeeAlso     []

******************************************************************************/


int PureSat_Test2LevelMini(bAig_Manager_t *manager,
			   bAigEdge_t l,
			   bAigEdge_t r)
{
  int class_ = bAig_Class(l);
  bAigEdge_t ll,lr,rl,rr;

  if(!manager->test2LevelMini)
    return 0;

  if(class_!= bAig_Class(r) || class_ != manager->class_)
    return 0;

  ll = leftChild(l);
  if(ll!=bAig_NULL && class_!=bAig_Class(ll))
    return 0;
  lr = rightChild(l);
  if(lr!=bAig_NULL && class_!=bAig_Class(lr))
    return 0;
  rl = leftChild(r);
  if(rl!=bAig_NULL && class_!=bAig_Class(rl))
    return 0;
  rr = rightChild(r);
  if(rr!=bAig_NULL && class_!=bAig_Class(rr))
    return 0;

  return 1;
}

/**Function********************************************************************

  Synopsis [And function for two AIG nodes. The difference with
	    bAigCreateAndNode is that here two level minimization
	    is only allowed with the same timeframe, otherwise the
	    global variable for interpolation generation may not be
	    latch variables]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_And(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{

  bAigEdge_t newNodeIndex;

  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);

  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
    nodeIndex1 = nodeIndex2;
    nodeIndex2 = newNodeIndex;
  }

  if ( nodeIndex2 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex1 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex2 == bAig_One ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_One ) {
    return nodeIndex2;
  }
  if ( nodeIndex1 == nodeIndex2 ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
    return bAig_Zero;
  }

  /* Look for the new node in the Hash table */
  newNodeIndex = PureSat_HashTableLookup(manager, nodeIndex1, nodeIndex2);


  if (newNodeIndex == bAig_NULL){
    if(!PureSat_Test2LevelMini(manager,nodeIndex1,nodeIndex2)){
      newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
      return newNodeIndex;
    }

    if(bAigIsVar(manager, nodeIndex1) && bAigIsVar(manager, nodeIndex2))
      newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
    else if(bAigIsVar(manager, nodeIndex1))
      newNodeIndex = PureSat_And3(manager, nodeIndex1, nodeIndex2);
    else if(bAigIsVar(manager, nodeIndex2))
      newNodeIndex = PureSat_And3(manager, nodeIndex2, nodeIndex1);
    else {
      newNodeIndex = PureSat_And4(manager, nodeIndex1, nodeIndex2);
    }
  }

  return newNodeIndex;

}


/**Function********************************************************************

  Synopsis    [OR operation for two aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_Or(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
  return ( bAig_Not(PureSat_And(manager,  bAig_Not(nodeIndex1),  bAig_Not(nodeIndex2))));
}


/**Function********************************************************************

  Synopsis    [XOR operation for two aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_Xor(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return PureSat_Or(manager,
	    PureSat_And(manager, nodeIndex1, bAig_Not(nodeIndex2)),
	    PureSat_And(manager, bAig_Not(nodeIndex1),nodeIndex2)
	);
}


/**Function********************************************************************

  Synopsis    [EQ operation for two aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_Eq(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return bAig_Not(
	    PureSat_Xor(manager, nodeIndex1, nodeIndex2)
	    );
}


/**Function********************************************************************

  Synopsis    [THEN operation for two aig nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

bAigEdge_t
PureSat_Then(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return PureSat_Or(manager,
		bAig_Not(nodeIndex1),
		nodeIndex2);
}



/**Function********************************************************************

  Synopsis    [Create variable AIG nodes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/


bAigEdge_t
PureSat_CreateVarNode(
   bAig_Manager_t  *manager,
   nameType_t	   *name)
{

  bAigEdge_t varIndex;
  int class_ = manager->class_;


  if (!st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
    varIndex = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
    if (varIndex == bAig_NULL){
      return (varIndex);
    }
    /* Insert the varaible in the Symbol Table */
    st_insert(manager->SymbolTableArray[class_],
	      name, (char*) (long) varIndex);
    manager->nameList[bAigNodeID(varIndex)] = name;
    return(varIndex);
  }
  else {
    return (varIndex);
  }
}