text: 
  int  Saig_ManFilterUsingIndOne2( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter 
                                   , int type_ /* jlong --  */
                                   )
  {
    Aig_Obj_t * pObj;
    int Lit, status;
    pObj = Aig_ManCo( pFrame, Counter*3+type_ ); /* which co */
    Lit  = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
    status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
    if ( status == l_False )    /* unsat */
        return status;
    if ( status == l_Undef )
      {
        printf( "Solver returned undecided.\n" );
        return status;
      }
    assert( status == l_True );
    return status;
  }
  
  Aig_Man_t * Saig_ManCreateIndMiter2( Aig_Man_t * pAig, Vec_Vec_t * vCands )
  {
    int nFrames = 3;
      Vec_Ptr_t * vNodes;
      Aig_Man_t * pFrames;
      Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
      Aig_Obj_t ** pObjMap;
      int i, f, k;
  
      // create mapping for the frames nodes
      pObjMap  = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
  
      // start the fraig package
      pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
      pFrames->pName = Abc_UtilStrsav( pAig->pName );
      pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
      // map constant nodes
      for ( f = 0; f < nFrames; f++ )
          Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
      // create PI nodes for the frames
      for ( f = 0; f < nFrames; f++ )
          Aig_ManForEachPiSeq( pAig, pObj, i )
              Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
      // set initial state for the latches
      Aig_ManForEachLoSeq( pAig, pObj, i )
          Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
  
      // add timeframes
      for ( f = 0; f < nFrames; f++ )
      {
          // add internal nodes of this frame
          Aig_ManForEachNode( pAig, pObj, i )
          {
              pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
              Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
          }
          // set the latch inputs and copy them into the latch outputs of the next frame
          Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
          {
              pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
              if ( f < nFrames - 1 )
                  Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
          }
      }
      
      // go through the candidates
      Vec_VecForEachLevel( vCands, vNodes, i )
      {
          Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
          {
              Aig_Obj_t * pObjR  = Aig_Regular(pObj);
              Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
              Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
          {
            Aig_Obj_t * pFan0  = Aig_NotCond( pNode0,  Aig_IsComplement(pObj) );
            Aig_Obj_t * pFan1  = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
            Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
            Aig_ObjCreateCo( pFrames, pMiter );
          
          /* need to check p & Xp is satisfiable */
          /* jlong -- begin */
            {
            Aig_Obj_t * pMiter2 = Aig_And( pFrames, pFan0, Aig_Not(pFan1));
            Aig_ObjCreateCo( pFrames, pMiter2 ); 
            }
          /* jlong -- end  */
          }
  
          {            /* jlong -- begin */
            Aig_Obj_t * pNode2 = pObjMap[nFrames*Aig_ObjId(pObjR)+2];
            Aig_Obj_t * pFan0  = Aig_NotCond( pNode0,  Aig_IsComplement(pObj) );
            Aig_Obj_t * pFan1  = Aig_NotCond( pNode1,  Aig_IsComplement(pObj) );
            Aig_Obj_t * pFan2  = Aig_NotCond( pNode2, !Aig_IsComplement(pObj) );
            Aig_Obj_t * pMiter = Aig_And( pFrames, Aig_And(pFrames, pFan0, pFan1 ), pFan2);
            Aig_ObjCreateCo( pFrames, pMiter ); /* jlong -- end  */
          }
  
          }
      }
      Aig_ManCleanup( pFrames );
      ABC_FREE( pObjMap );
  
  //Aig_ManShow( pAig, 0, NULL );
  //Aig_ManShow( pFrames, 0, NULL );
      return pFrames;
  }
  
  /**Function*************************************************************
  
     Synopsis    [Detects constraints functionally.]
  
     Description []
                 
     SideEffects []
  
     SeeAlso     []
  
  ***********************************************************************/
  void Saig_ManFilterUsingInd2( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
  {
    Vec_Ptr_t * vNodes;
    Aig_Man_t * pFrames;
    sat_solver * pSat;
    Cnf_Dat_t * pCnf;
    Aig_Obj_t * pObj;
    int i, k, k2, Counter;
    /*
      Vec_VecForEachLevel( vCands, vNodes, i )
      Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
      printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
      printf( "\n" );
    */
    // create timeframes 
    //    pFrames = Saig_ManUnrollInd( p );
    pFrames = Saig_ManCreateIndMiter2( p, vCands );
    assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands)*3 );
    // start the SAT solver
    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // check candidates
    if ( fVerbose )
      printf( "Filtered cands:  \n" );
    Counter = 0;
    Vec_VecForEachLevel( vCands, vNodes, i )
      {
        assert(i==0);             /* only one item */
        k2 = 0;
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
          {
            if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ , 0) == l_False)
              //            if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
              {
                Vec_PtrWriteEntry( vNodes, k2++, pObj );
                if ( fVerbose )
                  printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
                printf( " type I : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
                Vec_PtrPush(p->unfold2_type_I, pObj);
              }
            /* jlong -- begin  */
            else if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 1) == l_True ) /* can be self-conflicting */
              {
                if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 2) == l_False ){
                  //Vec_PtrWriteEntry( vNodes, k2++, pObj );
                  if ( fVerbose )
                    printf( "%d:%s%d  \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
                  printf( " type II: %d:%s%d  \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
                  Vec_PtrWriteEntry( vNodes, k2++, pObj ); /* add type II constraints */
                  Vec_PtrPush(p->unfold2_type_II, pObj);
                }
              }
            /* jlong -- end  */
          }
        Vec_PtrShrink( vNodes, k2 );
      }
  
    // clean up
    Cnf_DataFree( pCnf );
    sat_solver_delete( pSat );
    if ( fVerbose )
      Aig_ManPrintStats( pFrames );
    Aig_ManStop( pFrames );
  }
  
  
  /**Function*************************************************************
  
     Synopsis    [Returns the number of variables implied by the output.]
  
     Description []
                 
     SideEffects []
  
     SeeAlso     []
  
  ***********************************************************************/
  Vec_Vec_t * Ssw_ManFindDirectImplications2( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
  {
    Vec_Vec_t * vCands = NULL;
    Vec_Ptr_t * vNodes;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pRepr, * pReprR;
    int i, f, k, value;
    assert(nFrames == 1);
    vCands = Vec_VecAlloc( nFrames );
    assert(nFrames == 1);
    // perform unrolling
    pFrames = Saig_ManUnrollCOI( p, nFrames );
    assert( Aig_ManCoNum(pFrames) == 1 );
    // start the SAT solver
    pCnf = Cnf_DeriveSimple( pFrames, 0 );
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    if ( pSat != NULL )
      {
        Aig_ManIncrementTravId( p );
        for ( f = 0; f < nFrames; f++ )
          {
            Aig_ManForEachObj( p, pObj, i )
              {
                if ( !Aig_ObjIsCand(pObj) )
                  continue;
                //--jlong : also use internal nodes as well
                /* if ( !Aig_ObjIsCi(pObj) ) */
                /*   continue; */ 
                if ( Aig_ObjIsTravIdCurrent(p, pObj) )
                  continue;
                // get the node from timeframes
                pRepr  = p->pObjCopies[nFrames*i + nFrames-1-f];
                pReprR = Aig_Regular(pRepr);
                if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
                  continue;
                //                value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
                value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
                if ( value == l_Undef )
                  continue;
                // label this node as taken
                Aig_ObjSetTravIdCurrent(p, pObj);
                if ( Saig_ObjIsLo(p, pObj) )
                  Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
                // remember the node
                Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
                //        printf( "%s%d ", (value == l_False)? "":"!", i );
              }
          }
        //    printf( "\n" );
        sat_solver_delete( pSat );
      }
    Aig_ManStop( pFrames );
    Cnf_DataFree( pCnf );
  
    if ( fVerbose )
      {
        printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
        Vec_VecForEachLevel( vCands, vNodes, k )
          {
            printf( "Level %d. Cands  =%d    ", k, Vec_PtrSize(vNodes) );
            //            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
            //                printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
            printf( "\n" );
          }
      }
  
    ABC_FREE( p->pObjCopies );
    /* -- jlong -- this does the SAT proof of the constraints */
    Saig_ManFilterUsingInd2( p, vCands, nConfs, nProps, fVerbose );
    if ( Vec_VecSizeSize(vCands) )
      printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
    if ( fVerbose )
      {
        Vec_VecForEachLevel( vCands, vNodes, k )
          {
            printf( "Level %d. Constr =%d    ", k, Vec_PtrSize(vNodes) );
            //            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
            //                printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
            printf( "\n" );
          }
      }
    
    return vCands;
  }
  
  /**Function*************************************************************
  
     Synopsis    [Duplicates the AIG while unfolding constraints.]
  
     Description []
                 
     SideEffects []
  
     SeeAlso     []
  
  ***********************************************************************/
  Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt){
    Aig_Man_t * pNew;
    Vec_Vec_t * vCands;
    Vec_Ptr_t  * vNewFlops;
    Aig_Obj_t * pObj;
    int i,  k, nNewFlops;
    const int fCompl = 0 ;
    if ( fOldAlgo )
      vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
    else
      vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose );
    if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
      {
        Vec_VecFreeP( &vCands );
        return Aig_ManDupDfs( pAig );
      }
    // create new manager
    pNew = Aig_ManDupWithoutPos( pAig ); /* good */
    pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
    pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II)
      + Vec_PtrSize(pAig->unfold2_type_I);
    //  pNew->nConstrsTypeII  = Vec_PtrSize(pAig->unfold2_type_II);
    *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II);
  
    /* new set of registers */
    
    // add normal POs
    Saig_ManForEachPo( pAig, pObj, i )
      Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    // create constraint outputs
    vNewFlops = Vec_PtrAlloc( 100 );
  
  
    Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){
      Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
      Aig_ObjCreateCo(pNew, x);
    }
     
    Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
      Aig_Obj_t * type_II_latch
        = Aig_ObjCreateCi(pNew); /* will get connected later; */
      Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
      
      Aig_Obj_t * n = Aig_And(pNew, 
                              Aig_NotCond(type_II_latch, fCompl),
                              Aig_NotCond(x, fCompl));
      Aig_ObjCreateCo(pNew, n);//Aig_Not(n));
    }                   
    
    // add latch outputs
    Saig_ManForEachLi( pAig, pObj, i )
      Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    
    Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){
      Aig_Obj_t * x = Aig_ObjRealCopy(pObj);
      Aig_ObjCreateCo(pNew, x);
    }                   
  
    // add new latch outputs
    nNewFlops = Vec_PtrSize(pAig->unfold2_type_II);
    //assert( nNewFlops == Vec_PtrSize(vNewFlops) );
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
    printf("#reg after unfold2: %d\n", Aig_ManRegNum(pAig) + nNewFlops );
    Vec_VecFreeP( &vCands );
    Vec_PtrFree( vNewFlops );
    return pNew;
  
  }
  
  /**Function*************************************************************
  
     Synopsis    [Duplicates the AIG while unfolding constraints.]
  
     Description []
                 
     SideEffects []
  
     SeeAlso     []
  
  ***********************************************************************/
  Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose , 
                                           int typeII_cnt)
  {
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
    int i, typeII_cc, type_II;
    if ( Aig_ManConstrNum(pAig) == 0 )
      return Aig_ManDupDfs( pAig );
    assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
      pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
      pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
  
    // OR the constraint outputs
    pMiter = Aig_ManConst0( pAigNew );
    typeII_cc = 0;//typeII_cnt;
    typeII_cnt = 0;  
    type_II = 0;
      
    Saig_ManForEachPo( pAig, pObj, i )
      {
        
        if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
          continue;
        if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
          type_II = 1;
        }
        /*  now we got the constraint */
        if (type_II) {
  
          Aig_Obj_t * type_II_latch
            = Aig_ObjCreateCi(pAigNew); /* will get connected later; */
          pMiter = Aig_Or(pAigNew, pMiter, 
                          Aig_And(pAigNew, 
                                  Aig_NotCond(type_II_latch, fCompl),
                                  Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) )
                          );
          printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
        } else 
          pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
      }
  
    // create additional flop
    if ( Saig_ManRegNum(pAig) > 0 )
      {
        pFlopOut = Aig_ObjCreateCi( pAigNew );
        pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
      }
    else 
      pFlopIn = pMiter;
  
    // create primary output
    Saig_ManForEachPo( pAig, pObj, i )
      {
        if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
          continue;
        pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
        Aig_ObjCreateCo( pAigNew, pMiter );
      }
  
    // transfer to register outputs
    {
      /* the same for type I and type II */
      Aig_Obj_t * pObjLi, *pObjLo;
  
      Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )    {
        if( i + typeII_cc < Aig_ManRegNum(pAig)) {
          Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn), 
                                 Aig_ObjChild0Copy(pObjLi) ,
                                 (Aig_Obj_t*)pObjLo->pData);
          Aig_ObjCreateCo( pAigNew, c);
        } else {
          printf ( "skipping: reg%d\n", i);
          Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi));
        }
      }
  
    }
    if(0)Saig_ManForEachLi( pAig, pObj, i ) {
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
      }
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
      
    type_II = 0;
    Saig_ManForEachPo( pAig, pObj, i )
      {
      
        if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
          continue;
        if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) {
          type_II = 1;
        }
        /*  now we got the constraint */
        if (type_II) {
          Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj));
          Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
          printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
        }
      }
  
       
    // create additional flop 
  
    if ( Saig_ManRegNum(pAig) > 0 )
      {
        Aig_ObjCreateCo( pAigNew, pFlopIn );
        Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 );
      }
    printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew));
    // perform cleanup
    Aig_ManCleanup( pAigNew );
    Aig_ManSeqCleanup( pAigNew );
    return pAigNew;
  }
  