text: /**CFile****************************************************************
  
    FileName    [ifTune.c]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [FPGA mapping based on priority cuts.]
  
    Synopsis    [Library tuning.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - November 21, 2006.]
  
    Revision    [$Id: ifTune.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #include "if.h"
  #include "aig/gia/giaAig.h"
  #include "sat/bsat/satStore.h"
  #include "sat/cnf/cnf.h"
  #include "misc/extra/extra.h"
  #include "bool/kit/kit.h"
  
  ABC_NAMESPACE_IMPL_START
  
  ////////////////////////////////////////////////////////////////////////
  ///                        DECLARATIONS                              ///
  ////////////////////////////////////////////////////////////////////////
   
  #define IFN_INS    11
  #define IFN_WRD  (IFN_INS > 6 ? 1 << (IFN_INS-6) : 1)
  #define IFN_PAR  1024
  
  // network types
  typedef enum { 
      IFN_DSD_NONE = 0,              // 0:  unknown
      IFN_DSD_CONST0,                // 1:  constant
      IFN_DSD_VAR,                   // 2:  variable
      IFN_DSD_AND,                   // 3:  AND
      IFN_DSD_XOR,                   // 4:  XOR
      IFN_DSD_MUX,                   // 5:  MUX
      IFN_DSD_PRIME                  // 6:  PRIME
  } Ifn_DsdType_t;
  
  // object types
  static char * Ifn_Symbs[16] = { 
      NULL,                          // 0:  unknown
      "const",                       // 1:  constant
      "var",                         // 2:  variable
      "()",                          // 3:  AND
      "[]",                          // 4:  XOR
      "<>",                          // 5:  MUX
      "{}"                           // 6:  PRIME
  };
  
  typedef struct Ifn_Obj_t_  Ifn_Obj_t;
  struct Ifn_Obj_t_
  {
      unsigned               Type    :  3;      // node type
      unsigned               nFanins :  5;      // fanin counter
      unsigned               iFirst  :  8;      // first parameter
      unsigned               Var     : 16;      // current variable
      int                    Fanins[IFN_INS];   // fanin IDs
  };
  struct Ifn_Ntk_t_ 
  {
      // cell structure
      int                    nInps;             // inputs
      int                    nObjs;             // objects
      Ifn_Obj_t              Nodes[2*IFN_INS];  // nodes
      // constraints
      int                    pConstr[IFN_INS*IFN_INS];  // constraint pairs
      int                    nConstr;           // number of pairs
      // user data
      int                    nVars;             // variables
      int                    nWords;            // truth table words
      int                    nParsVNum;         // selection parameters per variable
      int                    nParsVIni;         // first selection parameter
      int                    nPars;             // total parameters
      word *                 pTruth;            // user truth table
      // matching procedures
      int                    Values[IFN_PAR];            // variable values
      word                   pTtElems[IFN_INS*IFN_WRD];  // elementary truth tables
      word                   pTtObjs[2*IFN_INS*IFN_WRD]; // object truth tables
  };
  
  static inline word *       Ifn_ElemTruth( Ifn_Ntk_t * p, int i ) { return p->pTtElems + i * Abc_TtWordNum(p->nInps); }
  static inline word *       Ifn_ObjTruth( Ifn_Ntk_t * p, int i )  { return p->pTtObjs + i * p->nWords;                }
   
  // variable ordering
  // - primary inputs            [0;            p->nInps)
  // - internal nodes            [p->nInps;     p->nObjs)
  // - configuration params      [p->nObjs;     p->nParsVIni)
  // - variable selection params [p->nParsVIni; p->nPars)
  
  ////////////////////////////////////////////////////////////////////////
  ///                     FUNCTION DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  /**Function*************************************************************
  
    Synopsis    [Prepare network to check the given function.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Ifn_Prepare( Ifn_Ntk_t * p, word * pTruth, int nVars )
  {
      int i, fVerbose = 0;
      assert( nVars <= p->nInps );
      p->pTruth = pTruth;
      p->nVars  = nVars;
      p->nWords = Abc_TtWordNum(nVars);
      p->nPars  = p->nObjs;
      for ( i = p->nInps; i < p->nObjs; i++ )
      {
          if ( p->Nodes[i].Type != IFN_DSD_PRIME )
              continue;
          p->Nodes[i].iFirst = p->nPars;
          p->nPars += (1 << p->Nodes[i].nFanins);
          if ( fVerbose )
              printf( "Node %d  Start %d  Vars %d\n", i, p->Nodes[i].iFirst, (1 << p->Nodes[i].nFanins) );
      }
      if ( fVerbose )
          printf( "Groups start %d\n", p->nPars );
      p->nParsVIni = p->nPars;
      p->nParsVNum = Abc_Base2Log(nVars);
      p->nPars    += p->nParsVNum * p->nInps;
      assert( p->nPars <= IFN_PAR );
      memset( p->Values, 0xFF, sizeof(int) * p->nPars );
      return p->nPars;
  }
  void Ifn_NtkPrint( Ifn_Ntk_t * p )
  {
      int i, k; 
      if ( p == NULL )
          printf( "String is empty.\n" );
      if ( p == NULL )
          return;
      for ( i = p->nInps; i < p->nObjs; i++ )
      {
          printf( "%c=", 'a'+i );
          printf( "%c", Ifn_Symbs[p->Nodes[i].Type][0] );
          for ( k = 0; k < (int)p->Nodes[i].nFanins; k++ )
              printf( "%c", 'a'+p->Nodes[i].Fanins[k] );
          printf( "%c", Ifn_Symbs[p->Nodes[i].Type][1] );
          printf( ";" );
      }
      printf( "\n" );
  }
  int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
  {
      int i, LutSize = 0;
      for ( i = p->nInps; i < p->nObjs; i++ )
          if ( p->Nodes[i].Type == IFN_DSD_PRIME )
              LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
      return LutSize;
  }
  int Ifn_NtkInputNum( Ifn_Ntk_t * p )
  {
      return p->nInps;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Ifn_ErrorMessage( const char * format, ...  )
  {
      char * pMessage;
      va_list args;
      va_start( args, format );
      pMessage = vnsprintf( format, args );
      va_end( args );
      printf( "%s", pMessage );
      ABC_FREE( pMessage );
      return 0;
  }
  int Inf_ManOpenSymb( char * pStr )
  {
      if ( pStr[0] == '(' )
          return 3;
      if ( pStr[0] == '[' )
          return 4;
      if ( pStr[0] == '<' )
          return 5;
      if ( pStr[0] == '{' )
          return 6;
      return 0;
  }
  int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
  {
      int i, nNodes = 0, Marks[32] = {0}, MaxVar = -1;
      for ( i = 0; pStr[i]; i++ )
      {
          if ( Inf_ManOpenSymb(pStr+i) )
              nNodes++;
          if ( pStr[i] == ';' || 
               pStr[i] == '(' || pStr[i] == ')' || 
               pStr[i] == '[' || pStr[i] == ']' || 
               pStr[i] == '<' || pStr[i] == '>' || 
               pStr[i] == '{' || pStr[i] == '}' )
              continue;
          if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
              continue;
          if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
          {
              MaxVar = Abc_MaxInt( MaxVar, (int)(pStr[i] - 'a') );
              Marks[pStr[i] - 'a'] = 1;
              continue;
          }
          return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
      }
      for ( i = 0; i <= MaxVar; i++ )
          if ( Marks[i] == 0 )
              return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
      *pnInps = MaxVar + 1;
      *pnObjs = MaxVar + 1 + nNodes;
      return 1;
  }
  static inline char * Ifn_NtkParseFindClosingParenthesis( char * pStr, char Open, char Close )
  {
      int Counter = 0;
      assert( *pStr == Open );
      for ( ; *pStr; pStr++ )
      {
          if ( *pStr == Open )
              Counter++;
          if ( *pStr == Close )
              Counter--;
          if ( Counter == 0 )
              return pStr;
      }
      return NULL;
  }
  int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNode )
  {
      Ifn_Obj_t * pObj;
      int nFanins = 0, pFanins[IFN_INS];
      int Type = Inf_ManOpenSymb( pStr );
      char * pLim = Ifn_NtkParseFindClosingParenthesis( pStr++, Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
      *ppFinal = NULL;
      if ( pLim == NULL )
          return Ifn_ErrorMessage( "For symbol \'%c\' cannot find matching symbol \'%c\'.\n", Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
      while ( pStr < pLim )
      {
          assert( nFanins < IFN_INS );
          if ( pStr[0] >= 'a' && pStr[0] <= 'z' )
              pFanins[nFanins++] = pStr[0] - 'a', pStr++; 
          else if ( Inf_ManOpenSymb(pStr) )
          {
              if ( !Ifn_NtkParseInt_rec( pStr, p, &pStr, piNode ) )
                  return 0;
              pFanins[nFanins++] = *piNode - 1;
          }
          else
              return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] );
      }
      assert( pStr == pLim );
      pObj = p->Nodes + (*piNode)++;
      pObj->Type = Type;
      assert( pObj->nFanins == 0 );
      pObj->nFanins = nFanins;
      memcpy( pObj->Fanins, pFanins, sizeof(int) * nFanins );
      *ppFinal = pLim + 1;
      if ( Type == IFN_DSD_MUX && nFanins != 3 )
          return Ifn_ErrorMessage( "MUX should have exactly three fanins.\n" );
      return 1;
  }
  int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
  {
      char * pFinal; int iNode;
      if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
          return 0;
      if ( p->nInps > IFN_INS )
          return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
      assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
      if ( !Inf_ManOpenSymb(pStr) )
          return Ifn_ErrorMessage( "The first symbol should be one of the symbols: (, [, <, {.\n" );
      iNode = p->nInps;
      if ( !Ifn_NtkParseInt_rec( pStr, p, &pFinal, &iNode ) )
          return 0;
      if ( pFinal[0] && pFinal[0] != ';' )
          return Ifn_ErrorMessage( "The last symbol should be \';\'.\n" );
      if ( iNode != p->nObjs )
          return Ifn_ErrorMessage( "Mismatch in the number of nodes.\n" );
      return 1;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Ifn_ManStrType2( char * pStr )
  {
      int i;
      for ( i = 0; pStr[i]; i++ )
          if ( pStr[i] == '=' )
              return 1;
      return 0;
  }
  int Ifn_ManStrCheck2( char * pStr, int * pnInps, int * pnObjs )
  {
      int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0;
      for ( i = 0; pStr[i]; i++ )
      {
          if ( pStr[i] == '=' || pStr[i] == ';' || 
               pStr[i] == '(' || pStr[i] == ')' || 
               pStr[i] == '[' || pStr[i] == ']' || 
               pStr[i] == '<' || pStr[i] == '>' || 
               pStr[i] == '{' || pStr[i] == '}' )
              continue;
          if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
              continue;
          if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
          {
              if ( pStr[i+1] == '=' )
                  Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a');
              continue;
          }
          return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
      }
      for ( i = 0; pStr[i]; i++ )
      {
          if ( pStr[i] == '=' || pStr[i] == ';' || 
               pStr[i] == '(' || pStr[i] == ')' || 
               pStr[i] == '[' || pStr[i] == ']' || 
               pStr[i] == '<' || pStr[i] == '>' || 
               pStr[i] == '{' || pStr[i] == '}' )
              continue;
          if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
              continue;
          if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
          {
              if ( pStr[i+1] != '=' && Marks[pStr[i] - 'a'] != 2 )
                  Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a');
              continue;
          }
          return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
      }
      MaxVar++;
      MaxDef++;
      for ( i = 0; i < MaxDef; i++ )
          if ( Marks[i] == 0 )
              return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
      for ( i = 0; i < MaxVar; i++ )
          if ( Marks[i] == 2 )
              return Ifn_ErrorMessage( "String \"%s\" has definition of input variable \'%c\'.\n", pStr, 'a' + i );
      for ( i = MaxVar; i < MaxDef; i++ )
          if ( Marks[i] == 1 )
              return Ifn_ErrorMessage( "String \"%s\" has no definition for internal variable \'%c\'.\n", pStr, 'a' + i );
      *pnInps = MaxVar;
      *pnObjs = MaxDef;
      return 1;
  }
  int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p )
  {
      int i, k, n, f, nFans, iFan;
      if ( !Ifn_ManStrCheck2(pStr, &p->nInps, &p->nObjs) )
          return 0;
      if ( p->nInps > IFN_INS )
          return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
      assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
      for ( i = p->nInps; i < p->nObjs; i++ )
      {
          char Next = 0;
          for ( k = 0; pStr[k]; k++ )
              if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
                  break;
          if ( pStr[k] == 0 )
              return Ifn_ErrorMessage( "Cannot find definition of signal \'%c\'.\n", 'a' + i );
          if ( pStr[k+2] == '(' )
              p->Nodes[i].Type = IFN_DSD_AND, Next = ')';
          else if ( pStr[k+2] == '[' )
              p->Nodes[i].Type = IFN_DSD_XOR, Next = ']';
          else if ( pStr[k+2] == '<' )
              p->Nodes[i].Type = IFN_DSD_MUX, Next = '>';
          else if ( pStr[k+2] == '{' )
              p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}';
          else 
              return Ifn_ErrorMessage( "Cannot find openning operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
          for ( n = k + 3; pStr[n]; n++ )
              if ( pStr[n] == Next )
                  break;
          if ( pStr[n] == 0 )
              return Ifn_ErrorMessage( "Cannot find closing operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
          nFans = n - k - 3;
          if ( nFans > 8 )
              return Ifn_ErrorMessage( "Cannot find matching operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
          for ( f = 0; f < nFans; f++ )
          {
              iFan = pStr[k + 3 + f] - 'a';
              if ( iFan < 0 || iFan >= i )
                  return Ifn_ErrorMessage( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i );
              p->Nodes[i].Fanins[f] = iFan;
          }
          p->Nodes[i].nFanins = nFans;
      }
      return 1;
  }
  void Ifn_NtkParseConstraints( char * pStr, Ifn_Ntk_t * p )
  {
      int i, k;
      // parse constraints
      p->nConstr = 0;
      for ( i = 0; i < p->nInps; i++ )
          for ( k = 0; pStr[k]; k++ )
              if ( pStr[k] == 'A' + i && pStr[k-1] == ';' )
              {
                  assert( p->nConstr < IFN_INS*IFN_INS );
                  p->pConstr[p->nConstr++] = ((int)(pStr[k] - 'A') << 16) | (int)(pStr[k+1] - 'A');
  //                printf( "Added constraint (%c < %c)\n", pStr[k], pStr[k+1] );
              }
  //    if ( p->nConstr )
  //        printf( "Total constraints = %d\n", p->nConstr );
  }
  
  Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
  {
      Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 );
      if ( Ifn_ManStrType2(pStr) )
      {
          if ( !Ifn_NtkParseInt2( pStr, p ) )
          {
              ABC_FREE( p );
              return NULL;
          }
      }
      else
      {
          if ( !Ifn_NtkParseInt( pStr, p ) )
          {
              ABC_FREE( p );
              return NULL;
          }
      }
      Ifn_NtkParseConstraints( pStr, p );
      Abc_TtElemInit2( p->pTtElems, p->nInps );
  //    printf( "Finished parsing: " ); Ifn_NtkPrint(p);
      return p;
  }
  int Ifn_NtkTtBits( char * pStr )
  {
      int i, Counter = 0;
      Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStr );
      for ( i = pNtk->nInps; i < pNtk->nObjs; i++ )
          if ( pNtk->Nodes[i].Type == IFN_DSD_PRIME )
              Counter += (1 << pNtk->Nodes[i].nFanins);
      ABC_FREE( pNtk );
      return Counter;
  }
  
  
  
  /**Function*************************************************************
  
    Synopsis    [Derive AIG.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Gia_Man_t * Ifn_ManStrFindModel( Ifn_Ntk_t * p )
  {
      Gia_Man_t * pNew, * pTemp;
      int i, k, iLit, * pVarMap = ABC_FALLOC( int, p->nParsVIni );
      pNew = Gia_ManStart( 1000 );
      pNew->pName = Abc_UtilStrsav( "model" );
      Gia_ManHashStart( pNew );
      for ( i = 0; i < p->nInps; i++ )
          pVarMap[i] = Gia_ManAppendCi(pNew);
      for ( i = p->nObjs; i < p->nParsVIni; i++ )
          pVarMap[i] = Gia_ManAppendCi(pNew);
      for ( i = p->nInps; i < p->nObjs; i++ )
      {
          int Type = p->Nodes[i].Type;
          int nFans = p->Nodes[i].nFanins;
          int * pFans = p->Nodes[i].Fanins;
          int iFanin = p->Nodes[i].iFirst;
          if ( Type == IFN_DSD_AND )
          {
              iLit = 1;
              for ( k = 0; k < nFans; k++ )
                  iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
              pVarMap[i] = iLit;
          }
          else if ( Type == IFN_DSD_XOR )
          {
              iLit = 0;
              for ( k = 0; k < nFans; k++ )
                  iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
              pVarMap[i] = iLit;
          }
          else if ( Type == IFN_DSD_MUX )
          {
              assert( nFans == 3 );
              pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
          }
          else if ( Type == IFN_DSD_PRIME )
          {
              int n, Step, pVarsData[256];
              int nMints = (1 << nFans);
              assert( nFans >= 0 && nFans <= 8 );
              for ( k = 0; k < nMints; k++ )
                  pVarsData[k] = pVarMap[iFanin + k];
              for ( Step = 1, k = 0; k < nFans; k++, Step <<= 1 )
                  for ( n = 0; n < nMints; n += Step << 1 )
                      pVarsData[n] = Gia_ManHashMux( pNew, pVarMap[pFans[k]], pVarsData[n+Step], pVarsData[n] );
              assert( Step == nMints );
              pVarMap[i] = pVarsData[0];
          }
          else assert( 0 );
      }
      Gia_ManAppendCo( pNew, pVarMap[p->nObjs-1] );
      ABC_FREE( pVarMap );
      pNew = Gia_ManCleanup( pTemp = pNew );
      Gia_ManStop( pTemp );
      assert( Gia_ManPiNum(pNew) == p->nParsVIni - (p->nObjs - p->nInps) );
      assert( Gia_ManPoNum(pNew) == 1 );
      return pNew;
  }
  // compute cofactors w.r.t. the first nIns variables
  Gia_Man_t * Ifn_ManStrFindCofactors( int nIns, Gia_Man_t * p )
  {
      Gia_Man_t * pNew, * pTemp; 
      Gia_Obj_t * pObj;
      int i, m, nMints = 1 << nIns;
      pNew = Gia_ManStart( Gia_ManObjNum(p) );
      pNew->pName = Abc_UtilStrsav( p->pName );
      Gia_ManHashAlloc( pNew );
      Gia_ManConst0(p)->Value = 0;
      Gia_ManForEachCi( p, pObj, i )
          if ( i >= nIns )
              pObj->Value = Gia_ManAppendCi( pNew );
      for ( m = 0; m < nMints; m++ )
      {
          Gia_ManForEachCi( p, pObj, i )
              if ( i < nIns )
                  pObj->Value = ((m >> i) & 1);
          Gia_ManForEachAnd( p, pObj, i )
              pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
          Gia_ManForEachPo( p, pObj, i )
              pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
      }
      pNew = Gia_ManCleanup( pTemp = pNew );
      Gia_ManStop( pTemp );
      return pNew;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Derive SAT solver.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
  {
      Cnf_Dat_t * pCnf;
      Aig_Man_t * pAig = Gia_ManToAigSimple( p );
      pAig->nRegs = 0;
      pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
      Aig_ManStop( pAig );
      return pCnf;
  }
  sat_solver * Ifn_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
  {
      sat_solver * pSat;
      Gia_Obj_t * pObj;
      Cnf_Dat_t * pCnf;
      int i;    
      pCnf = Cnf_DeriveGiaRemapped( p );
      // start the SAT solver
      pSat = sat_solver_new();
      sat_solver_setnvars( pSat, pCnf->nVars );
      // add timeframe clauses
      for ( i = 0; i < pCnf->nClauses; i++ )
          if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
              assert( 0 );
      // inputs/outputs
      *pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) );
      Gia_ManForEachCi( p, pObj, i )
          Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
      *pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) );
      Gia_ManForEachCo( p, pObj, i )
          Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
      Cnf_DataFree( pCnf );
      return pSat;
  }
  sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
  {
      Gia_Man_t * p1, * p2;
      sat_solver * pSat = NULL;
      *pvPiVars = *pvPoVars = NULL;
      p1 = Ifn_ManStrFindModel( p );
  //    Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
      p2 = Ifn_ManStrFindCofactors( p->nInps, p1 );
      Gia_ManStop( p1 );
  //    Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
      pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars );
      Gia_ManStop( p2 );
      return pSat;
  }
  void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk )
  {
      Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
      Ifn_Prepare( p, NULL, p->nInps );
      *ppNtk = p;
      if ( p == NULL )
          return NULL;
  //    Ifn_NtkPrint( p );
      return Ifn_ManSatBuild( p, pvPiVars, pvPoVars );
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
  {
      int i;
      for ( i = 0; i < nVars; i++ )
          printf( "%c", 'a' + pPerms[i] );
      printf( "\n" );
  }
  int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits )
  {
      int v, Value, m, mNew, nMints = (1 << nVars); // (1 << nInps);
      assert( (1 << nInps) == Vec_IntSize(vPoVars) );
      assert( nVars <= nInps );
      // remap minterms
      Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
      for ( m = 0; m < nMints; m++ )
      {
          mNew = 0;
          for ( v = 0; v < nInps; v++ )
          {
              assert( pPerm[v] < nVars );
              if ( ((m >> pPerm[v]) & 1) )
                  mNew |= (1 << v);
          }
          assert( Vec_IntEntry(vLits, mNew) == -1 );
          Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
      }
      // find assumptions
      v = 0;
      Vec_IntForEachEntry( vLits, Value, m )
          if ( Value >= 0 )
              Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) );
      Vec_IntShrink( vLits, v );
      // run SAT solver
      Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
      return (int)(Value == l_True);
  }
  void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues )
  {
      int i, iVar;
      Vec_IntClear( vValues );
      Vec_IntForEachEntry( vPiVars, iVar, i )
          Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
  }
  int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues )
  {
      // extract permutation
      int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
      assert( nInps <= IF_MAX_FUNC_LUTSIZE );
      for ( i = 0; i < nInps; i++ )
      {
          pPerm[i] = Abc_TtGetHex( &Perm, i );
          assert( pPerm[i] < nVars );
      }
      // perform SAT check 
      RetValue = Ifn_ManSatCheckOne( (sat_solver *)pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues );
      Vec_IntClear( vValues );
      if ( RetValue == 0 )
          return 0;
      Ifn_ManSatDeriveOne( (sat_solver*)pSat, vPiVars, vValues );
      return 1;
  }
  int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word Perm )
  {
      Vec_Int_t * vValues = Vec_IntAlloc( 100 );
      Vec_Int_t * vPiVars, * vPoVars;
      sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars );
      int RetValue = If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues );
      Vec_IntPrint( vValues );
      // cleanup
      sat_solver_delete( pSat );
      Vec_IntFreeP( &vPiVars );
      Vec_IntFreeP( &vPoVars );
      Vec_IntFreeP( &vValues );
      return RetValue;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Derive GIA using programmable bits.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, word * pConfigData, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
  {
      Gia_Man_t * pNew = (Gia_Man_t *)pGia;
      int i, k, iLit, iVar = 0, nVarsNew, pVarMap[1000];
      int nTtBits = p->nParsVIni - p->nObjs;
      int nPermBits = Abc_Base2Log(p->nInps + 1) + 1;
      int fCompl = Abc_TtGetBit( pConfigData, nTtBits + nPermBits * p->nInps );
      assert( Vec_IntSize(vLeaves) <= p->nInps && p->nParsVIni < 1000 );
      for ( i = 0; i < p->nInps; i++ )
      {
          for ( iLit = k = 0; k < nPermBits; k++ )
              if ( Abc_TtGetBit(pConfigData, nTtBits + i * nPermBits + k) )
                  iLit |= (1 << k);
          assert( Abc_Lit2Var(iLit) < Vec_IntSize(vLeaves) );
          pVarMap[i] = Abc_Lit2LitL( Vec_IntArray(vLeaves), iLit );
      }
      for ( i = p->nInps; i < p->nObjs; i++ )
      {
          int Type = p->Nodes[i].Type;
          int nFans = p->Nodes[i].nFanins;
          int * pFans = p->Nodes[i].Fanins;
          //int iFanin = p->Nodes[i].iFirst;
          assert( nFans <= 6 );
          if ( Type == IFN_DSD_AND )
          {
              iLit = 1;
              for ( k = 0; k < nFans; k++ )
                  iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
              pVarMap[i] = iLit;
          }
          else if ( Type == IFN_DSD_XOR )
          {
              iLit = 0;
              for ( k = 0; k < nFans; k++ )
                  iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
              pVarMap[i] = iLit;
          }
          else if ( Type == IFN_DSD_MUX )
          {
              assert( nFans == 3 );
              pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
          }
          else if ( Type == IFN_DSD_PRIME )
          {
              int pFaninLits[16];
              // collect truth table
              word uTruth = 0;
              int nMints = (1 << nFans);
              for ( k = 0; k < nMints; k++ )
                  if ( Abc_TtGetBit(pConfigData, iVar++) )
                      uTruth |= ((word)1 << k);
              uTruth = Abc_Tt6Stretch( uTruth, nFans );
              // collect function
              for ( k = 0; k < nFans; k++ )
                  pFaninLits[k] = pVarMap[pFans[k]];
              // implement the function
              nVarsNew = Abc_TtMinBase( &uTruth, pFaninLits, nFans, 6 );
              if ( nVarsNew == 0 )
                  pVarMap[i] = (int)(uTruth & 1);
              else
              {
                  extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
                  Vec_Int_t Leaves = { nVarsNew, nVarsNew, pFaninLits };
                  pVarMap[i] = Kit_TruthToGia( pNew, (unsigned *)&uTruth, nVarsNew, vCover, &Leaves, 1 ); // hashing enabled!!!
              }
          }
          else assert( 0 );
      }
      assert( iVar == nTtBits );
      return Abc_LitNotCond( pVarMap[p->nObjs - 1], fCompl );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Derive GIA using programmable bits.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void * If_ManDeriveGiaFromCells( void * pGia )
  {
      Gia_Man_t * p = (Gia_Man_t *)pGia;
      Gia_Man_t * pNew, * pTemp;
      Vec_Int_t * vCover, * vLeaves;
      Ifn_Ntk_t * pNtkCell;
      Gia_Obj_t * pObj; 
      word * pConfigData;
      //word * pTruth;
      int k, i, iLut, iVar;
      int nConfigInts, Count = 0;
      assert( p->vConfigs != NULL );
      assert( p->pCellStr != NULL );
      assert( Gia_ManHasMapping(p) );
      // derive cell network
      pNtkCell = Ifn_NtkParse( p->pCellStr );
      Ifn_Prepare( pNtkCell, NULL, pNtkCell->nInps );
      nConfigInts = Vec_IntEntry( p->vConfigs, 1 );
      // create new manager
      pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
      pNew->pName = Abc_UtilStrsav( p->pName );
      pNew->pSpec = Abc_UtilStrsav( p->pSpec );
      // map primary inputs
      Gia_ManFillValue(p);
      Gia_ManConst0(p)->Value = 0;
      Gia_ManForEachCi( p, pObj, i )
          pObj->Value = Gia_ManAppendCi(pNew);
      // iterate through nodes used in the mapping
      vLeaves = Vec_IntAlloc( 16 );
      vCover  = Vec_IntAlloc( 1 << 16 );
      Gia_ManHashStart( pNew );
      //Gia_ObjComputeTruthTableStart( p, Gia_ManLutSizeMax(p) );
      Gia_ManForEachAnd( p, pObj, iLut )
      {
          if ( Gia_ObjIsBuf(pObj) )
          {
              pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
              continue;
          }
          if ( !Gia_ObjIsLut(p, iLut) )
              continue;
          // collect leaves
          //Vec_IntClear( vLeaves );
          //Gia_LutForEachFanin( p, iLut, iVar, k )
          //    Vec_IntPush( vLeaves, iVar );
          //pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, iLut), vLeaves );
          // collect incoming literals
          Vec_IntClear( vLeaves );
          Gia_LutForEachFanin( p, iLut, iVar, k )
              Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value );
          pConfigData = (word *)Vec_IntEntryP( p->vConfigs, 2 + nConfigInts * Count++ );
          Gia_ManObj(p, iLut)->Value = If_ManSatDeriveGiaFromBits( pNew, pNtkCell, pConfigData, vLeaves, vCover );
      }
      assert( Vec_IntEntry(p->vConfigs, 0) == Count );
      assert( Vec_IntSize(p->vConfigs) == 2 + nConfigInts * Count );
      //Gia_ObjComputeTruthTableStop( p );
      Gia_ManForEachCo( p, pObj, i )
          pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
      Gia_ManHashStop( pNew );
      Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
      Vec_IntFree( vLeaves );
      Vec_IntFree( vCover );
      ABC_FREE( pNtkCell );
      // perform cleanup
      pNew = Gia_ManCleanup( pTemp = pNew );
      Gia_ManStop( pTemp );
      return pNew;
  
  }
  
  /**Function*************************************************************
  
    Synopsis    [Derive truth table given the configulation values.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  word * Ifn_NtkDeriveTruth( Ifn_Ntk_t * p, int * pValues )
  {
      int i, v, f, iVar, iStart;
      // elementary variables
      for ( i = 0; i < p->nInps; i++ )
      {
          // find variable
          iStart = p->nParsVIni + i * p->nParsVNum;
          for ( v = iVar = 0; v < p->nParsVNum; v++ )
              if ( p->Values[iStart+v] )
                  iVar += (1 << v);
          // assign variable
          Abc_TtCopy( Ifn_ObjTruth(p, i), Ifn_ElemTruth(p, iVar), p->nWords, 0 );
      }
      // internal variables
      for ( i = p->nInps; i < p->nObjs; i++ )
      {
          int nFans = p->Nodes[i].nFanins;
          int * pFans = p->Nodes[i].Fanins;
          word * pTruth = Ifn_ObjTruth( p, i );
          if ( p->Nodes[i].Type == IFN_DSD_AND )
          {
              Abc_TtFill( pTruth, p->nWords );
              for ( f = 0; f < nFans; f++ )
                  Abc_TtAnd( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
          }
          else if ( p->Nodes[i].Type == IFN_DSD_XOR )
          {
              Abc_TtClear( pTruth, p->nWords );
              for ( f = 0; f < nFans; f++ )
                  Abc_TtXor( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
          }
          else if ( p->Nodes[i].Type == IFN_DSD_MUX )
          {
              assert( nFans == 3 );
              Abc_TtMux( pTruth, Ifn_ObjTruth(p, pFans[0]), Ifn_ObjTruth(p, pFans[1]), Ifn_ObjTruth(p, pFans[2]), p->nWords );
          }
          else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
          {
              int nValues = (1 << nFans);
              word * pTemp = Ifn_ObjTruth(p, p->nObjs);
              Abc_TtClear( pTruth, p->nWords );
              for ( v = 0; v < nValues; v++ )
              {
                  if ( pValues[p->Nodes[i].iFirst + v] == 0 )
                      continue;
                  Abc_TtFill( pTemp, p->nWords );
                  for ( f = 0; f < nFans; f++ )
                      if ( (v >> f) & 1 )
                          Abc_TtAnd( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
                      else
                          Abc_TtSharp( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords );
                  Abc_TtOr( pTruth, pTruth, pTemp, p->nWords );
              }
          }
          else assert( 0 );
  //Dau_DsdPrintFromTruth( pTruth, p->nVars );
      }
      return Ifn_ObjTruth(p, p->nObjs-1);
  }
  
  /**Function*************************************************************
  
    Synopsis    [Compute more or equal]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Ifn_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
  {
      word Cond[4], Equa[4], Temp[4];
      word s_TtElems[8][4] = {
          { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
          { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
          { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
          { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
          { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
          { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
          { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
          { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
      };
      int i, nWords = Abc_TtWordNum(2*nVars);
      assert( nVars > 0 && nVars <= 4 );
      Abc_TtClear( pTruth, nWords );
      Abc_TtFill( Equa, nWords );
      for ( i = nVars - 1; i >= 0; i-- )
      {
          if ( fMore )
              Abc_TtSharp( Cond, s_TtElems[2*i+1], s_TtElems[2*i+0], nWords );
          else
              Abc_TtSharp( Cond, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords );
          Abc_TtAnd( Temp, Equa, Cond, nWords, 0 );
          Abc_TtOr( pTruth, pTruth, Temp, nWords );
          Abc_TtXor( Temp, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords, 1 );
          Abc_TtAnd( Equa, Equa, Temp, nWords, 0 );
      }
      if ( fEqual )
          Abc_TtNot( pTruth, nWords );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Adds parameter constraints.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Ifn_AddClause( sat_solver * pSat, int * pBeg, int * pEnd )
  {
      int fVerbose = 0;
      int RetValue = sat_solver_addclause( pSat, pBeg, pEnd );
      if ( fVerbose )
      {
          for ( ; pBeg < pEnd; pBeg++ )
              printf( "%c%d ", Abc_LitIsCompl(*pBeg) ? '-':'+', Abc_Lit2Var(*pBeg) );
          printf( "\n" );
      }
      return RetValue;
  }
  void Ifn_NtkAddConstrOne( sat_solver * pSat, Vec_Int_t * vCover, int * pVars, int nVars )
  {
      int RetValue, k, c, Cube, Literal, nLits, pLits[IFN_INS];
      Vec_IntForEachEntry( vCover, Cube, c )
      {
          nLits = 0;
          for ( k = 0; k < nVars; k++ )
          {
              Literal = 3 & (Cube >> (k << 1));
              if ( Literal == 1 )      // '0'  -> pos lit
                  pLits[nLits++] = Abc_Var2Lit(pVars[k], 0);
              else if ( Literal == 2 ) // '1'  -> neg lit
                  pLits[nLits++] = Abc_Var2Lit(pVars[k], 1);
              else if ( Literal != 0 )
                  assert( 0 );
          }
          RetValue = Ifn_AddClause( pSat, pLits, pLits + nLits );
          assert( RetValue );
      }
  }
  void Ifn_NtkAddConstraints( Ifn_Ntk_t * p, sat_solver * pSat )
  {
      int fAddConstr = 1;
      Vec_Int_t * vCover = Vec_IntAlloc( 0 );
      word uTruth = Abc_Tt6Stretch( ~Abc_Tt6Mask(p->nVars), p->nParsVNum );
      assert( p->nParsVNum <= 4 );
      if ( uTruth )
      {
          int i, k, pVars[IFN_INS];
          int RetValue = Kit_TruthIsop( (unsigned *)&uTruth, p->nParsVNum, vCover, 0 );
          assert( RetValue == 0 );
  //        Dau_DsdPrintFromTruth( &uTruth, p->nParsVNum );
          // add capacity constraints
          for ( i = 0; i < p->nInps; i++ )
          {
              for ( k = 0; k < p->nParsVNum; k++ )
                  pVars[k] = p->nParsVIni + i * p->nParsVNum + k;
              Ifn_NtkAddConstrOne( pSat, vCover, pVars, p->nParsVNum );
          }
      }
      // ordering constraints
      if ( fAddConstr && p->nConstr )
      {
          word pTruth[4];
          int i, k, RetValue, pVars[2*IFN_INS];
          int fForceDiff = (p->nVars == p->nInps);
          Ifn_TtComparisonConstr( pTruth, p->nParsVNum, fForceDiff, fForceDiff );
          RetValue = Kit_TruthIsop( (unsigned *)pTruth, 2*p->nParsVNum, vCover, 0 );
          assert( RetValue == 0 );
  //        Kit_TruthIsopPrintCover( vCover, 2*p->nParsVNum, 0 );
          for ( i = 0; i < p->nConstr; i++ )
          {
              int iVar1 = p->pConstr[i] >> 16;
              int iVar2 = p->pConstr[i] & 0xFFFF;
              for ( k = 0; k < p->nParsVNum; k++ )
              {
                  pVars[2*k+0] = p->nParsVIni + iVar1 * p->nParsVNum + k;
                  pVars[2*k+1] = p->nParsVIni + iVar2 * p->nParsVNum + k;
              }
              Ifn_NtkAddConstrOne( pSat, vCover, pVars, 2*p->nParsVNum );
  //            printf( "added constraint with %d clauses for %d and %d\n", Vec_IntSize(vCover), iVar1, iVar2 );
          }
      }
      Vec_IntFree( vCover );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Derive clauses given variable assignment.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
  {
      int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2];
      // assign new variables
      int nSatVars = sat_solver_nvars(pSat);
  //    for ( i = 0; i < p->nObjs-1; i++ )
      for ( i = 0; i < p->nObjs; i++ )
          p->Nodes[i].Var = nSatVars++;
      //p->Nodes[p->nObjs-1].Var = 0xFFFF;
      sat_solver_setnvars( pSat, nSatVars );
      // verify variable values
      for ( i = 0; i < p->nVars; i++ )
          assert( pValues[i] != -1 );
      for ( i = p->nVars; i < p->nObjs-1; i++ )
          assert( pValues[i] == -1 );
      assert( pValues[p->nObjs-1] != -1 );
      // internal variables
  //printf( "\n" );
      for ( i = 0; i < p->nInps; i++ )
      {
          int iParStart = p->nParsVIni + i * p->nParsVNum;
          for ( v = 0; v < p->nVars; v++ )
          {
              // add output literal
              pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, pValues[v]==0 );
              // add clause literals
              for ( f = 0; f < p->nParsVNum; f++ )
                  pLits[f+1] = Abc_Var2Lit( iParStart + f, (v >> f) & 1 ); 
              if ( !Ifn_AddClause( pSat, pLits, pLits+p->nParsVNum+1 ) )
                  return 0;
          }
      }
  //printf( "\n" );
      for ( i = p->nInps; i < p->nObjs; i++ )
      {
          int nFans = p->Nodes[i].nFanins;
          int * pFans = p->Nodes[i].Fanins;
          if ( p->Nodes[i].Type == IFN_DSD_AND )
          {
              nLits = 0;
              pLits[nLits++] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
              for ( f = 0; f < nFans; f++ )
              {
                  pLits[nLits++] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 1 );
                  // add small clause
                  pLits2[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
                  pLits2[1] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 0 );
                  if ( !Ifn_AddClause( pSat, pLits2, pLits2 + 2 ) )
                      return 0;
              }
              // add big clause
              if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) )
                  return 0;
          }
          else if ( p->Nodes[i].Type == IFN_DSD_XOR )
          {
              int m, nMints = (1 << (nFans+1));
              for ( m = 0; m < nMints; m++ )
              {
                  // skip even 
                  int Count = 0;
                  for ( v = 0; v <= nFans; v++ )
                      Count += ((m >> v) & 1);
                  if ( (Count & 1) == 0 )
                      continue;
                  // generate minterm
                  pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, (m >> nFans) & 1 );
                  for ( v = 0; v < nFans; v++ )
                      pLits[v+1] = Abc_Var2Lit( p->Nodes[pFans[v]].Var, (m >> v) & 1 );
                  if ( !Ifn_AddClause( pSat, pLits, pLits + nFans + 1 ) )
                      return 0;
              }
          }
          else if ( p->Nodes[i].Type == IFN_DSD_MUX )
          {
              pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
              pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
              pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 1 );
              if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
                  return 0;
  
              pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
              pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
              pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 0 );
              if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
                  return 0;
  
              pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
              pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
              pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 1 );
              if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
                  return 0;
  
              pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
              pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
              pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 0 );
              if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
                  return 0;
          }
          else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
          {
              int nValues = (1 << nFans);
              int iParStart = p->Nodes[i].iFirst;
              for ( v = 0; v < nValues; v++ )
              {
                  nLits = 0;
                  if ( pValues[i] == -1 )
                  {
                      pLits[nLits]  = Abc_Var2Lit( p->Nodes[i].Var, 0 );
                      pLits2[nLits] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
                      nLits++;
                  }
                  for ( f = 0; f < nFans; f++, nLits++ )
                      pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, (v >> f) & 1 ); 
                  pLits[nLits]  = Abc_Var2Lit( iParStart + v, 1 ); 
                  pLits2[nLits] = Abc_Var2Lit( iParStart + v, 0 ); 
                  nLits++;
                  if ( pValues[i] != 0 )
                  {
                      if ( !Ifn_AddClause( pSat, pLits2, pLits2 + nLits ) )
                          return 0;
                  }
                  if ( pValues[i] != 1 )
                  {
                      if ( !Ifn_AddClause( pSat, pLits,  pLits + nLits ) )
                          return 0;
                  }
              }
          }
          else assert( 0 );
  //printf( "\n" );
      }
      // add last clause (not needed if the root node is IFN_DSD_PRIME)
      pLits[0] = Abc_Var2Lit( p->Nodes[p->nObjs-1].Var, pValues[p->nObjs-1]==0 );
      if ( !Ifn_AddClause( pSat, pLits,  pLits + 1 ) )
          return 0;
      return 1;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Returns the minterm number for which there is a mismatch.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Ifn_NtkMatchPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk )
  {
      printf( "Iter = %5d  ",  Iter );
      printf( "Mint = %5d  ",  iMint );
      printf( "Value = %2d  ", Value );
      printf( "Var = %6d  ",   sat_solver_nvars(p) );
      printf( "Cla = %6d  ",   sat_solver_nclauses(p) );
      printf( "Conf = %6d  ",  sat_solver_nconflicts(p) );
      if ( status == l_False )
          printf( "status = unsat" );
      else if ( status == l_True )
          printf( "status = sat  " );
      else 
          printf( "status = undec" );
      Abc_PrintTime( 1, "Time", clk );
  }
  void Ifn_NtkMatchPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
  {
      int v, i;
      for ( v = p->nObjs; v < p->nPars; v++ )
      {
          for ( i = p->nInps; i < p->nObjs; i++ )
              if ( p->Nodes[i].Type == IFN_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
                  break;
          if ( i < p->nObjs )
              printf( " " );
          else if ( v >= p->nParsVIni && (v - p->nParsVIni) % p->nParsVNum == 0 )
              printf( " %d=", (v - p->nParsVIni) / p->nParsVNum );
          printf( "%d", sat_solver_var_value(pSat, v) );
      }
  }
  word Ifn_NtkMatchCollectPerm( Ifn_Ntk_t * p, sat_solver * pSat )
  {
      word Perm = 0;
      int i, v, Mint;
      assert( p->nParsVNum <= 4 );
      for ( i = 0; i < p->nInps; i++ )
      {
          for ( Mint = v = 0; v < p->nParsVNum; v++ )
              if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
                  Mint |= (1 << v);
          Abc_TtSetHex( &Perm, i, Mint );
      }
      return Perm;
  }
  void Ifn_NtkMatchCollectConfig( Ifn_Ntk_t * p, sat_solver * pSat, word * pConfig )
  {
      int i, v, Mint;
      assert( p->nParsVNum <= 4 );
      for ( i = 0; i < p->nInps; i++ )
      {
          for ( Mint = v = 0; v < p->nParsVNum; v++ )
              if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
                  Mint |= (1 << v);
          Abc_TtSetHex( pConfig, i, Mint );
      }
      for ( v = p->nObjs; v < p->nParsVIni; v++ )
          if ( sat_solver_var_value(pSat, v) )
              Abc_TtSetBit( pConfig + 1, v - p->nObjs );
  }
  void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
  {
      int i;
      assert( nInps <= 16 );
      for ( i = 0; i < nInps; i++ )
          printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) );
      printf( "\n" );
  }
  int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig )
  {
      word * pTruth1;
      int RetValue = 0;
      int nIterMax = (1<<nVars);
      int i, v, status, iMint = 0;
      abctime clk = Abc_Clock();
  //    abctime clkTru = 0, clkSat = 0, clk2;
      sat_solver * pSat;
      if ( nVars == 0 )
          return 1;
      pSat = sat_solver_new();
      Ifn_Prepare( p, pTruth, nVars );
      sat_solver_setnvars( pSat, p->nPars );
      Ifn_NtkAddConstraints( p, pSat );
      if ( fVeryVerbose )
          Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
      if ( pConfig ) assert( *pConfig == 0 );
      for ( i = 0; i < nIterMax; i++ )
      {
          // get variable assignment
          for ( v = 0; v < p->nObjs; v++ )
              p->Values[v] = v < p->nVars ? (iMint >> v) & 1 :  -1;
          p->Values[p->nObjs-1] = Abc_TtGetBit( pTruth, iMint );
          // derive clauses
          if ( !Ifn_NtkAddClauses( p, p->Values, pSat ) )
              break;
          // find assignment of parameters
  //        clk2 = Abc_Clock();
          status = sat_solver_solve( pSat, NULL, NULL, nConfls, 0, 0, 0 );
  //        clkSat += Abc_Clock() - clk2;
          if ( fVeryVerbose )
              Ifn_NtkMatchPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk );
          if ( status != l_True )
              break;
          // collect assignment
          for ( v = p->nObjs; v < p->nPars; v++ )
              p->Values[v] = sat_solver_var_value(pSat, v);
          // find truth table
  //        clk2 = Abc_Clock();
          pTruth1 = Ifn_NtkDeriveTruth( p, p->Values );
  //        clkTru += Abc_Clock() - clk2;
          Abc_TtXor( pTruth1, pTruth1, p->pTruth, p->nWords, 0 );
          // find mismatch if present
          iMint = Abc_TtFindFirstBit( pTruth1, p->nVars );
          if ( iMint == -1 )
          {
              if ( pConfig ) 
                  Ifn_NtkMatchCollectConfig( p, pSat, pConfig );
  /*
              if ( pPerm )
              {
                  int RetValue = Ifn_ManSatFindCofigBitsTest( p, pTruth, nVars, *pPerm );
                  Ifn_NtkMatchPrintPerm( *pPerm, p->nInps );
                  if ( RetValue == 0 )
                      printf( "Verification failed.\n" );
              }
  */
              RetValue = 1;
              break;
          }
      }
      assert( i < nIterMax );
      if ( fVerbose )
      {
          printf( "%s  Iter =%4d. Confl = %6d.  ", RetValue ? "yes":"no ", i, sat_solver_nconflicts(pSat) );
          if ( RetValue )
              Ifn_NtkMatchPrintConfig( p, pSat );
          printf( "\n" );
      }
      sat_solver_delete( pSat );
  //    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
  //    Abc_PrintTime( 1, "Sat", clkSat );
  //    Abc_PrintTime( 1, "Tru", clkTru );
      return RetValue;
  }
  
  /**Function*************************************************************
  
    Synopsis    []
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Ifn_NtkRead()
  {
      int RetValue;
      int nVars = 8;
  //    word * pTruth = Dau_DsdToTruth( "(abcdefghi)", nVars );
      word * pTruth = Dau_DsdToTruth( "1008{(1008{(ab)cde}f)ghi}", nVars );
  //    word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
  //    word * pTruth = Dau_DsdToTruth( "1008{(1008{[ab]cde}f)ghi}", nVars );
  //    word * pTruth = Dau_DsdToTruth( "(abcd)", nVars );
  //    word * pTruth = Dau_DsdToTruth( "(abc)", nVars );
  //    word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
  //    char * pStr = "e={abc};f={ed};";
  //    char * pStr = "d={ab};e={cd};";
  //    char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};";
  //    char * pStr = "i={abc};j={ide};k={ifg};l={jkh};";
  //    char * pStr = "h={abcde};i={abcdf};j=<ghi>;";
  //    char * pStr = "g=<abc>;h=<ade>;i={fgh};";
  //    char * pStr = "i=<abc>;j=(def);k=[gh];l={ijk};";
      char * pStr = "{({(ab)cde}f)ghi};AB;CD;DE;GH;HI";
      Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
      word Perm = 0;
      if ( p == NULL )
          return;
      Ifn_NtkPrint( p );
      Dau_DsdPrintFromTruth( pTruth, nVars );
      // get the given function
      RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1, &Perm );
      ABC_FREE( p );
  }
  
  ////////////////////////////////////////////////////////////////////////
  ///                       END OF FILE                                ///
  ////////////////////////////////////////////////////////////////////////
  
  
  ABC_NAMESPACE_IMPL_END
  
  