path: root/src/aig/gia/giaPat2.c

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

  FileName    [giaPat2.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Pattern generation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: giaPat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

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

#include "gia.h"
#include "misc/vec/vecHsh.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "misc/util/utilTruth.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Min_Man_t_ Min_Man_t;
struct Min_Man_t_
{
    int              nCis;
    int              nCos;
    int              FirstAndLit;
    int              FirstCoLit;
    Vec_Int_t        vFans;
    Vec_Str_t        vValsN;
    Vec_Str_t        vValsL;
    Vec_Int_t        vVis;
    Vec_Int_t        vPat;
};

static inline int    Min_ManCiNum( Min_Man_t * p )                 { return p->nCis;                                       }
static inline int    Min_ManCoNum( Min_Man_t * p )                 { return p->nCos;                                       }
static inline int    Min_ManObjNum( Min_Man_t * p )                { return Vec_IntSize(&p->vFans) >> 1;                   }
static inline int    Min_ManAndNum( Min_Man_t * p )                { return Min_ManObjNum(p) - p->nCis - p->nCos - 1;      }

static inline int    Min_ManCi( Min_Man_t * p, int i )             { return 1 + i;                                         }
static inline int    Min_ManCo( Min_Man_t * p, int i )             { return Min_ManObjNum(p) - Min_ManCoNum(p) + i;        }

static inline int    Min_ObjIsCi( Min_Man_t * p, int i )           { return i > 0 && i <= Min_ManCiNum(p);                 }
static inline int    Min_ObjIsNode( Min_Man_t * p, int i )         { return i > Min_ManCiNum(p) && i < Min_ManObjNum(p) - Min_ManCoNum(p);      }
static inline int    Min_ObjIsAnd( Min_Man_t * p, int i )          { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) < Vec_IntEntry(&p->vFans, 2*i+1);  }
static inline int    Min_ObjIsXor( Min_Man_t * p, int i )          { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) > Vec_IntEntry(&p->vFans, 2*i+1);  }
static inline int    Min_ObjIsBuf( Min_Man_t * p, int i )          { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) ==Vec_IntEntry(&p->vFans, 2*i+1);  }
static inline int    Min_ObjIsCo( Min_Man_t * p, int i )           { return i >= Min_ManObjNum(p) - Min_ManCoNum(p) && i < Min_ManObjNum(p);    }

static inline int    Min_ObjLit( Min_Man_t * p, int i, int n )     { return Vec_IntEntry(&p->vFans, i + i + n);            }
static inline int    Min_ObjLit0( Min_Man_t * p, int i )           { return Vec_IntEntry(&p->vFans, i + i + 0);            }
static inline int    Min_ObjLit1( Min_Man_t * p, int i )           { return Vec_IntEntry(&p->vFans, i + i + 1);            }
static inline int    Min_ObjCioId( Min_Man_t * p, int i )          { assert( i && !Min_ObjIsNode(p, i) ); return Min_ObjLit1(p, i);  }

static inline int    Min_ObjFan0( Min_Man_t * p, int i )           { return Abc_Lit2Var( Min_ObjLit0(p, i) );              }
static inline int    Min_ObjFan1( Min_Man_t * p, int i )           { return Abc_Lit2Var( Min_ObjLit1(p, i) );              }

static inline int    Min_ObjFanC0( Min_Man_t * p, int i )          { return Abc_LitIsCompl( Min_ObjLit0(p, i) );           }
static inline int    Min_ObjFanC1( Min_Man_t * p, int i )          { return Abc_LitIsCompl( Min_ObjLit1(p, i) );           }

static inline char   Min_ObjValN( Min_Man_t * p, int i )           { return Vec_StrEntry(&p->vValsN, i);                   }
static inline void   Min_ObjSetValN( Min_Man_t * p, int i, char v ){ Vec_StrWriteEntry(&p->vValsN, i, v);                  }

static inline char   Min_LitValL( Min_Man_t * p, int i )           { return Vec_StrEntry(&p->vValsL, i);                   }
static inline void   Min_LitSetValL( Min_Man_t * p, int i, char v ){ assert(v==0 || v==1); Vec_StrWriteEntry(&p->vValsL, i, v); Vec_StrWriteEntry(&p->vValsL, i^1, (char)!v); Vec_IntPush(&p->vVis, Abc_Lit2Var(i)); }
static inline void   Min_ObjCleanValL( Min_Man_t * p, int i )      { ((short *)Vec_StrArray(&p->vValsL))[i]  = 0x0202;     }
static inline void   Min_ObjMarkValL( Min_Man_t * p, int i )       { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0404;     }
static inline void   Min_ObjMark2ValL( Min_Man_t * p, int i )      { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0808;     }
static inline void   Min_ObjUnmark2ValL( Min_Man_t * p, int i )    { ((short *)Vec_StrArray(&p->vValsL))[i] &= 0xF7F7;     }

static inline int    Min_LitIsCi( Min_Man_t * p, int v )           { return v > 1 && v < p->FirstAndLit;                   }
static inline int    Min_LitIsNode( Min_Man_t * p, int v )         { return v >= p->FirstAndLit && v < p->FirstCoLit;      }
static inline int    Min_LitIsCo( Min_Man_t * p, int v )           { return v >= p->FirstCoLit;                            }

static inline int    Min_LitIsAnd( int v, int v0, int v1 )         { return Abc_LitIsCompl(v) ^ (v0 < v1);                 }
static inline int    Min_LitIsXor( int v, int v0, int v1 )         { return Abc_LitIsCompl(v) ^ (v0 > v1);                 }
static inline int    Min_LitIsBuf( int v, int v0, int v1 )         { return v0 == v1;                                      }

static inline int    Min_LitFan( Min_Man_t * p, int v )            { return Vec_IntEntry(&p->vFans, v);                    }
static inline int    Min_LitFanC( Min_Man_t * p, int v )           { return Abc_LitIsCompl( Min_LitFan(p, v) );            }

static inline void   Min_ManStartValsN( Min_Man_t * p )            { Vec_StrGrow(&p->vValsN, Vec_IntCap(&p->vFans)/2); Vec_StrFill(&p->vValsN, Min_ManObjNum(p), 2);       }
static inline void   Min_ManStartValsL( Min_Man_t * p )            { Vec_StrGrow(&p->vValsL, Vec_IntCap(&p->vFans));   Vec_StrFill(&p->vValsL, Vec_IntSize(&p->vFans), 2); }
static inline int    Min_ManCheckCleanValsL( Min_Man_t * p )       { int i; char c; Vec_StrForEachEntry( &p->vValsL, c, i ) if ( c != 2 ) return 0; return 1;  }
static inline void   Min_ManCleanVisitedValL( Min_Man_t * p )      { int i, iObj; Vec_IntForEachEntry(&p->vVis, iObj, i)  Min_ObjCleanValL(p, iObj); Vec_IntClear(&p->vVis); }


#define Min_ManForEachObj( p, i )                                  \
    for ( i = 0; i < Min_ManObjNum(p); i++ )
#define Min_ManForEachCi( p, i )                                   \
    for ( i = 1; i <= Min_ManCiNum(p); i++ )
#define Min_ManForEachCo( p, i )                                   \
    for ( i = Min_ManObjNum(p) - Min_ManCoNum(p); i < Min_ManObjNum(p); i++ )
#define Min_ManForEachAnd( p, i )                                  \
    for ( i = 1 + Min_ManCiNum(p); i < Min_ManObjNum(p) - Min_ManCoNum(p); i++ )


////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Min_Man_t * Min_ManStart( int nObjMax )
{
    Min_Man_t * p = ABC_CALLOC( Min_Man_t, 1 );
    Vec_IntGrow( &p->vFans,  nObjMax );
    Vec_IntPushTwo( &p->vFans, -1, -1 );
    return p;
}
static inline void Min_ManStop( Min_Man_t * p )
{
    Vec_IntErase( &p->vFans );
    Vec_StrErase( &p->vValsN );
    Vec_StrErase( &p->vValsL );
    Vec_IntErase( &p->vVis );
    Vec_IntErase( &p->vPat );
    ABC_FREE( p );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_ManAppendObj( Min_Man_t * p, int iLit0, int iLit1 )
{
    int iLit = Vec_IntSize(&p->vFans);
    Vec_IntPushTwo( &p->vFans, iLit0, iLit1 );
    return iLit;
}
static inline int Min_ManAppendCi( Min_Man_t * p )
{
    p->nCis++;
    p->FirstAndLit = Vec_IntSize(&p->vFans) + 2;
    return Min_ManAppendObj( p, 0, p->nCis-1 );
}
static inline int Min_ManAppendCo( Min_Man_t * p, int iLit0 )
{
    p->nCos++;
    if ( p->FirstCoLit == 0 )
        p->FirstCoLit = Vec_IntSize(&p->vFans);
    return Min_ManAppendObj( p, iLit0, p->nCos-1 );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Min_ManFromGia_rec( Min_Man_t * pNew, Gia_Man_t * p, int iObj )
{
    Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
    if ( ~pObj->Value )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj) );
    Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj) );
    pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Min_Man_t * Min_ManFromGia( Gia_Man_t * p, Vec_Int_t * vOuts )
{
    Gia_Obj_t * pObj;  int i;
    Min_Man_t * pNew = Min_ManStart( Gia_ManObjNum(p) );
    Gia_ManFillValue(p);
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
        pObj->Value = Min_ManAppendCi( pNew );
    if ( vOuts == NULL )
    {
        Gia_ManForEachAnd( p, pObj, i )
            pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
        Gia_ManForEachCo( p, pObj, i )
            pObj->Value = Min_ManAppendCo( pNew, Gia_ObjFaninLit0p(p, pObj) );
    }
    else
    {
        Gia_ManForEachCoVec( vOuts, p, pObj, i )
            Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0p(p, pObj) );
        Gia_ManForEachCoVec( vOuts, p, pObj, i )
            Min_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    }
    return pNew;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline char Min_XsimNot( char Val )   
{ 
    if ( Val < 2 )
        return Val ^ 1;
    return 2;
}
static inline char Min_XsimXor( char Val0, char Val1 )   
{ 
    if ( Val0 < 2 && Val1 < 2 )
        return Val0 ^ Val1;
    return 2;
}
static inline char Min_XsimAnd( char Val0, char Val1 )   
{ 
    if ( Val0 == 0 || Val1 == 0 )
        return 0;
    if ( Val0 == 1 && Val1 == 1 )
        return 1;
    return 2;
}



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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
char Min_LitVerify_rec( Min_Man_t * p, int iLit )
{
    char Val = Min_LitValL(p, iLit);
    if ( Val == 2 && Min_LitIsNode(p, iLit) ) // unassigned
    {
        int iLit0 = Min_LitFan(p, iLit);
        int iLit1 = Min_LitFan(p, iLit^1);
        char Val0 = Min_LitVerify_rec( p, iLit0 );
        char Val1 = Min_LitVerify_rec( p, iLit1 );
        assert( Val0 < 3 && Val1 < 3 );
        if ( Min_LitIsXor(iLit, iLit0, iLit1) )
            Val = Min_XsimXor( Val0, Val1 );
        else
            Val = Min_XsimAnd( Val0, Val1 );
        if ( Val < 2 )
        {
            Val ^= Abc_LitIsCompl(iLit);
            Min_LitSetValL( p, iLit, Val );
        }
        else
            Vec_IntPush( &p->vVis, Abc_Lit2Var(iLit) );
        Min_ObjMark2ValL( p, Abc_Lit2Var(iLit) );
    }
    return Val&3;
}
char Min_LitVerify( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
{
    int i, Entry; char Res;
    if ( iLit < 2 ) return 1;
    assert( !Min_LitIsCo(p, iLit) );
    //assert( Min_ManCheckCleanValsL(p) );
    assert( Vec_IntSize(&p->vVis) == 0 );
    Vec_IntForEachEntry( vLits, Entry, i )
        Min_LitSetValL( p, Entry, 1 ); // ms notation
    Res = Min_LitVerify_rec( p, iLit );
    Min_ManCleanVisitedValL( p );
    return Res;
}

void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
{
    int i, iObj, iTemp; char Res;
    Vec_IntClear( &p->vPat );
    if ( iLit < 2 ) return;
    assert( !Min_LitIsCo(p, iLit) );
    //assert( Min_ManCheckCleanValsL(p) );
    assert( Vec_IntSize(&p->vVis) == 0 );
    Vec_IntForEachEntry( vLits, iTemp, i )
        Min_LitSetValL( p, iTemp, 1 ); // ms notation
    Res = Min_LitVerify_rec( p, iLit );
    assert( Res == 1 );
    Min_ObjMarkValL( p, Abc_Lit2Var(iLit) );
    Vec_IntForEachEntryReverse( &p->vVis, iObj, i )
    {
        int iLit = Abc_Var2Lit( iObj, 0 );
        int Value = 7 & Min_LitValL(p, iLit);
        if ( Value >= 4 )
        {
            if ( Min_LitIsCi(p, iLit) )
                Vec_IntPush( &p->vPat, Abc_LitNotCond(iLit, !(Value&1)) );
            else
            {
                int iLit0 = Min_LitFan(p, iLit);
                int iLit1 = Min_LitFan(p, iLit^1);
                char Val0 = Min_LitValL( p, iLit0 );
                char Val1 = Min_LitValL( p, iLit1 );
                if ( Value&1 ) // value == 1
                {
                    assert( (Val0&1) && (Val1&1) );
                    Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
                    Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
                }
                else // value == 0
                {
                    int Zero0 = !(Val0&3);
                    int Zero1 = !(Val1&3);
                    assert( Zero0 || Zero1 );
                    if ( Zero0 && !Zero1 )
                        Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
                    else if ( !Zero0 && Zero1 )
                        Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
                    else if ( Val0 == 4 && Val1 != 4 )
                        Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
                    else if ( Val1 == 4 && Val0 != 4 )
                        Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
                    else if ( Abc_Random(0) & 1 )
                        Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
                    else
                        Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
                }
            }
        }
        Min_ObjCleanValL( p, Abc_Lit2Var(iLit) );
    }
    Vec_IntClear( &p->vVis );
    //Min_ManCleanVisitedValL( p );
    //assert( Min_LitVerify(p, iLit, &p->vPat) == 1 );
    assert( Vec_IntSize(&p->vPat) <= Vec_IntSize(vLits) );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline char Min_LitIsImplied1( Min_Man_t * p, int iLit )
{
    char Val = 2;
    int iLit0 = Min_LitFan(p, iLit);
    int iLit1 = Min_LitFan(p, iLit^1);
    char Val0 = Min_LitValL(p, iLit0);
    char Val1 = Min_LitValL(p, iLit1);
    assert( Min_LitIsNode(p, iLit) );    // internal node
    assert( Min_LitValL(p, iLit) == 2 ); // unassigned
    if ( Min_LitIsXor(iLit, iLit0, iLit1) )
        Val = Min_XsimXor( Val0, Val1 );
    else
        Val = Min_XsimAnd( Val0, Val1 );
    if ( Val < 2 )
    {
        Val ^= Abc_LitIsCompl(iLit);
        Min_LitSetValL( p, iLit, Val );
    }
    return Val;
}
static inline char Min_LitIsImplied2( Min_Man_t * p, int iLit )
{
    char Val = 2;
    int iLit0 = Min_LitFan(p, iLit);
    int iLit1 = Min_LitFan(p, iLit^1);
    char Val0 = Min_LitValL(p, iLit0);
    char Val1 = Min_LitValL(p, iLit1);
    assert( Min_LitIsNode(p, iLit) );    // internal node
    assert( Min_LitValL(p, iLit) == 2 ); // unassigned
    if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
        Val0 = Min_LitIsImplied1(p, iLit0);
    if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
        Val1 = Min_LitIsImplied1(p, iLit1);
    if ( Min_LitIsXor(iLit, iLit0, iLit1) )
        Val = Min_XsimXor( Val0, Val1 );
    else
        Val = Min_XsimAnd( Val0, Val1 );
    if ( Val < 2 )
    {
        Val ^= Abc_LitIsCompl(iLit);
        Min_LitSetValL( p, iLit, Val );
    }
    return Val;
}
static inline char Min_LitIsImplied3( Min_Man_t * p, int iLit )
{
    char Val = 2;
    int iLit0 = Min_LitFan(p, iLit);
    int iLit1 = Min_LitFan(p, iLit^1);
    char Val0 = Min_LitValL(p, iLit0);
    char Val1 = Min_LitValL(p, iLit1);
    assert( Min_LitIsNode(p, iLit) );    // internal node
    assert( Min_LitValL(p, iLit) == 2 ); // unassigned
    if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
        Val0 = Min_LitIsImplied2(p, iLit0);
    if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
        Val1 = Min_LitIsImplied2(p, iLit1);
    if ( Min_LitIsXor(iLit, iLit0, iLit1) )
        Val = Min_XsimXor( Val0, Val1 );
    else
        Val = Min_XsimAnd( Val0, Val1 );
    if ( Val < 2 )
    {
        Val ^= Abc_LitIsCompl(iLit);
        Min_LitSetValL( p, iLit, Val );
    }
    return Val;
}
static inline char Min_LitIsImplied4( Min_Man_t * p, int iLit )
{
    char Val = 2;
    int iLit0 = Min_LitFan(p, iLit);
    int iLit1 = Min_LitFan(p, iLit^1);
    char Val0 = Min_LitValL(p, iLit0);
    char Val1 = Min_LitValL(p, iLit1);
    assert( Min_LitIsNode(p, iLit) );    // internal node
    assert( Min_LitValL(p, iLit) == 2 ); // unassigned
    if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
        Val0 = Min_LitIsImplied3(p, iLit0);
    if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
        Val1 = Min_LitIsImplied3(p, iLit1);
    if ( Min_LitIsXor(iLit, iLit0, iLit1) )
        Val = Min_XsimXor( Val0, Val1 );
    else
        Val = Min_XsimAnd( Val0, Val1 );
    if ( Val < 2 )
    {
        Val ^= Abc_LitIsCompl(iLit);
        Min_LitSetValL( p, iLit, Val );
    }
    return Val;
}
static inline char Min_LitIsImplied5( Min_Man_t * p, int iLit )
{
    char Val = 2;
    int iLit0 = Min_LitFan(p, iLit);
    int iLit1 = Min_LitFan(p, iLit^1);
    char Val0 = Min_LitValL(p, iLit0);
    char Val1 = Min_LitValL(p, iLit1);
    assert( Min_LitIsNode(p, iLit) );    // internal node
    assert( Min_LitValL(p, iLit) == 2 ); // unassigned
    if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
        Val0 = Min_LitIsImplied4(p, iLit0);
    if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
        Val1 = Min_LitIsImplied4(p, iLit1);
    if ( Min_LitIsXor(iLit, iLit0, iLit1) )
        Val = Min_XsimXor( Val0, Val1 );
    else
        Val = Min_XsimAnd( Val0, Val1 );
    if ( Val < 2 )
    {
        Val ^= Abc_LitIsCompl(iLit);
        Min_LitSetValL( p, iLit, Val );
    }
    return Val;
}

// this recursive procedure is about 10% slower
char Min_LitIsImplied_rec( Min_Man_t * p, int iLit, int Depth )
{
    char Val = 2;
    int iLit0 = Min_LitFan(p, iLit);
    int iLit1 = Min_LitFan(p, iLit^1);
    char Val0 = Min_LitValL(p, iLit0);
    char Val1 = Min_LitValL(p, iLit1);
    assert( Depth > 0 );
    assert( Min_LitIsNode(p, iLit) );    // internal node
    assert( Min_LitValL(p, iLit) == 2 ); // unassigned
    if ( Depth > 1 && Val0 == 2 && Min_LitIsNode(p, iLit0) )
    {
        Val0 = Min_LitIsImplied_rec(p, iLit0, Depth-1);
        Val1 = Min_LitValL(p, iLit1);
    }
    if ( Depth > 1 && Val1 == 2 && Min_LitIsNode(p, iLit1) )
    {
        Val1 = Min_LitIsImplied_rec(p, iLit1, Depth-1);
        Val0 = Min_LitValL(p, iLit0);
    }
    if ( Min_LitIsXor(iLit, iLit0, iLit1) )
        Val = Min_XsimXor( Val0, Val1 );
    else
        Val = Min_XsimAnd( Val0, Val1 );
    if ( Val < 2 )
    {
        Val ^= Abc_LitIsCompl(iLit);
        Min_LitSetValL( p, iLit, Val );
    }
    return Val;
}
int Min_LitJustify_rec( Min_Man_t * p, int iLit )
{
    int Res = 1, LitValue = !Abc_LitIsCompl(iLit);
    int Val = (int)Min_LitValL(p, iLit);
    if ( Val < 2 ) // assigned
        return Val == LitValue;
    // unassigned
    if ( Min_LitIsCi(p, iLit) )
        Vec_IntPush( &p->vPat, iLit ); // ms notation
    else
    {
        int iLit0 = Min_LitFan(p, iLit);
        int iLit1 = Min_LitFan(p, iLit^1);
        char Val0 = Min_LitValL(p, iLit0);
        char Val1 = Min_LitValL(p, iLit1);
        if ( Min_LitIsXor(iLit, iLit0, iLit1) )
        {
            if ( Val0 < 2 && Val1 < 2 )
                Res = LitValue == (Val0 ^ Val1);
            else if ( Val0 < 2 )
                Res = Min_LitJustify_rec(p, iLit1^Val0^!LitValue);
            else if ( Val1 < 2 )
                Res = Min_LitJustify_rec(p, iLit0^Val1^!LitValue);
            else if ( Abc_Random(0) & 1 )
                Res = Min_LitJustify_rec(p, iLit0)   && Min_LitJustify_rec(p, iLit1^ LitValue);
            else
                Res = Min_LitJustify_rec(p, iLit0^1) && Min_LitJustify_rec(p, iLit1^!LitValue);
            assert( !Res || LitValue == Min_XsimXor(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
        }
        else if ( LitValue ) // value 1
        {
            if ( Val0 == 0 || Val1 == 0 )
                Res = 0;
            else if ( Val0 == 1 && Val1 == 1 )
                Res = 1;
            else if ( Val0 == 1 )
                Res = Min_LitJustify_rec(p, iLit1);
            else if ( Val1 == 1 )
                Res = Min_LitJustify_rec(p, iLit0);
            else 
                Res = Min_LitJustify_rec(p, iLit0) && Min_LitJustify_rec(p, iLit1);
            assert( !Res || 1 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
        }
        else // value 0
        {
/*
            int Depth = 3;
            if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
            {
                Val0 = Min_LitIsImplied_rec(p, iLit0, Depth);
                Val1 = Min_LitValL(p, iLit1);
            }
            if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
            {
                Val1 = Min_LitIsImplied_rec(p, iLit1, Depth);
                Val0 = Min_LitValL(p, iLit0);
            }
*/
            if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
            {
                Val0 = Min_LitIsImplied3(p, iLit0);
                Val1 = Min_LitValL(p, iLit1);
            }
            if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
            {
                Val1 = Min_LitIsImplied3(p, iLit1);
                Val0 = Min_LitValL(p, iLit0);
            }
            if ( Val0 == 0 || Val1 == 0 )
                Res = 1;
            else if ( Val0 == 1 && Val1 == 1 )
                Res = 0;
            else if ( Val0 == 1 )
                Res = Min_LitJustify_rec(p, iLit1^1);
            else if ( Val1 == 1 )
                Res = Min_LitJustify_rec(p, iLit0^1);
            else if ( Abc_Random(0) & 1 )
            //else if ( (p->Random >> (iLit & 0x1F)) & 1 )
                Res = Min_LitJustify_rec(p, iLit0^1);
            else
                Res = Min_LitJustify_rec(p, iLit1^1);
            //Val0 = Min_LitValL(p, iLit0);
            //Val1 = Min_LitValL(p, iLit1);
            assert( !Res || 0 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
        }
    }
    if ( Res )
        Min_LitSetValL( p, iLit, 1 );
    return Res;
}
int Min_LitJustify( Min_Man_t * p, int iLit )
{ 
    int Res, fCheck = 0;
    Vec_IntClear( &p->vPat );
    if ( iLit < 2 )  return 1;
    assert( !Min_LitIsCo(p, iLit) );
    //assert( Min_ManCheckCleanValsL(p) );
    assert( Vec_IntSize(&p->vVis) == 0 );
    //p->Random = Abc_Random(0);
    Res = Min_LitJustify_rec( p, iLit );
    Min_ManCleanVisitedValL( p );
    if ( Res )
    {
        if ( fCheck && Min_LitVerify(p, iLit, &p->vPat) != 1 )
            printf( "Verification FAILED for literal %d.\n", iLit );
        //else
        //    printf( "Verification succeeded for literal %d.\n", iLit );
    }
    //else
    //    printf( "Could not justify literal %d.\n", iLit );
    return Res;
}



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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Min_TargGenerateCexes( Min_Man_t * p, Vec_Int_t * vCoErrs, int nCexes, int nCexesStop, int * pnComputed, int fVerbose )
{
    abctime clk = Abc_Clock(); 
    int t, iObj, Count = 0, CountPos = 0, CountPosSat = 0, nRuns[2] = {0}, nCountCexes[2] = {0};
    Vec_Int_t * vPats    = Vec_IntAlloc( 1000 );
    Vec_Int_t * vPatBest = Vec_IntAlloc( Min_ManCiNum(p) );
    Hsh_VecMan_t * pHash = Hsh_VecManStart( 10000 );
    Min_ManForEachCo( p, iObj ) if ( Min_ObjLit0(p, iObj) > 1 )
    {
        int nCexesGenSim0 = 0;
        int nCexesGenSim = 0;
        int nCexesGenSat = 0;
        if ( vCoErrs && Vec_IntEntry(vCoErrs, Min_ObjCioId(p, iObj)) >= nCexesStop )
            continue;
        //printf( "%d ", i );
        for ( t = 0; t < nCexes; t++ )
        {
            nRuns[0]++;
            if ( Min_LitJustify( p, Min_ObjLit0(p, iObj) )  )
            {
                int Before, After;
                assert( Vec_IntSize(&p->vPat) > 0 );
                //printf( "%d   ", Vec_IntSize(vPat) );
                Vec_IntClear( vPatBest );
                if ( 1 ) // no minimization 
                    Vec_IntAppend( vPatBest, &p->vPat );
                else
                {
/*
                    for ( k = 0; k < 10; k++ )
                    {
                        Vec_IntClear( vPat2 );
                        Gia_ManIncrementTravId( p );
                        Cexes_MinimizePattern_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), vPat2 );
                        assert( Vec_IntSize(vPat2) <= Vec_IntSize(vPat) );
                        if ( Vec_IntSize(vPatBest) == 0 || Vec_IntSize(vPatBest) > Vec_IntSize(vPat2) )
                        {
                            Vec_IntClear( vPatBest );
                            Vec_IntAppend( vPatBest, vPat2 );
                        }
                        //printf( "%d ", Vec_IntSize(vPat2) );
                    }
*/
                }

                //Gia_CexVerify( p, Gia_ObjFaninId0p(p, pObj), !Gia_ObjFaninC0(pObj), vPatBest );
                //printf( "\n" );
                Before = Hsh_VecSize( pHash );
                Vec_IntSort( vPatBest, 0 );
                Hsh_VecManAdd( pHash, vPatBest );
                After = Hsh_VecSize( pHash );
                if ( Before != After )
                {
                    Vec_IntPush( vPats, Min_ObjCioId(p, iObj) );
                    Vec_IntPush( vPats, Vec_IntSize(vPatBest) );
                    Vec_IntAppend( vPats, vPatBest );
                    nCexesGenSim++;
                }
                nCexesGenSim0++;
                if ( nCexesGenSim0 > nCexesGenSim*10 )
                {
                    printf( "**** Skipping output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) );
                    break;
                }
            }
            if ( nCexesGenSim == nCexesStop )
                break;
        }
        //printf( "(%d %d)  ", nCexesGenSim0, nCexesGenSim );
        //printf( "%d ", t/nCexesGenSim );

        //printf( "The number of CEXes = %d\n", nCexesGen );
        //if ( fVerbose )
        //    printf( "%d ", nCexesGen );
        nCountCexes[0] += nCexesGenSim;
        nCountCexes[1] += nCexesGenSat;
        Count += nCexesGenSim + nCexesGenSat;
        CountPos++;

        if ( nCexesGenSim0 == 0 && t == nCexes )
            printf( "#### Output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) );
    }
    //printf( "\n" );
    if ( fVerbose )
    printf( "\n" );
    if ( fVerbose )
    printf( "Got %d unique CEXes using %d sim (%d) and %d SAT (%d) runs (ave size %.1f). PO = %d  ErrPO = %d  SatPO = %d  ", 
        Count, nRuns[0], nCountCexes[0], nRuns[1], nCountCexes[1], 
        1.0*Vec_IntSize(vPats)/Abc_MaxInt(1, Count)-2, Min_ManCoNum(p), CountPos, CountPosSat );
    if ( fVerbose )
        Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
    Hsh_VecManStop( pHash );
    Vec_IntFree( vPatBest );
    *pnComputed = Count;
    return vPats;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Min_ManTest3( Gia_Man_t * p, Vec_Int_t * vCoErrs )
{
    int fXor = 0;
    int nComputed;
    Vec_Int_t * vPats;
    Gia_Man_t * pXor = fXor ? Gia_ManDupMuxes(p, 1) : NULL;
    Min_Man_t * pNew = Min_ManFromGia( fXor ? pXor : p, NULL );
    Gia_ManStopP( &pXor );
    Min_ManStartValsL( pNew );
    //Vec_IntFill( vCoErrs, Vec_IntSize(vCoErrs), 0 );
    //vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 );
    vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 );
    Vec_IntFree( vPats );
    Min_ManStop( pNew );
}
void Min_ManTest4( Gia_Man_t * p )
{
    Vec_Int_t * vCoErrs = Vec_IntStartNatural( Gia_ManCoNum(p) );
    Min_ManTest3(p, vCoErrs);
    Vec_IntFree( vCoErrs );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManDupCones2CollectPis_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vMap )
{
    Gia_Obj_t * pObj;
    if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
        return;
    pObj = Gia_ManObj( p, iObj );
    if ( Gia_ObjIsAnd(pObj) )
    {
        Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId0(pObj, iObj), vMap );
        Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId1(pObj, iObj), vMap );
    }
    else if ( Gia_ObjIsCi(pObj) )
        Vec_IntPush( vMap, iObj );
    else assert( 0 );
}
void Gia_ManDupCones2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
    if ( Gia_ObjIsCi(pObj) || Gia_ObjUpdateTravIdCurrent(p, pObj) )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(pObj) );
    Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin1(pObj) );
    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Gia_Man_t * Gia_ManDupCones2( Gia_Man_t * p, int * pOuts, int nOuts, Vec_Int_t * vMap )
{
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj; int i;
    Vec_IntClear( vMap );
    Gia_ManIncrementTravId( p );
    for ( i = 0; i < nOuts; i++ )
        Gia_ManDupCones2CollectPis_rec( p, Gia_ManCoDriverId(p, pOuts[i]), vMap );
    pNew = Gia_ManStart( 1000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachObjVec( vMap, p, pObj, i )
        pObj->Value = Gia_ManAppendCi( pNew );
    Gia_ManIncrementTravId( p );
    for ( i = 0; i < nOuts; i++ )
        Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(Gia_ManCo(p, pOuts[i])) );
    for ( i = 0; i < nOuts; i++ )
        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, pOuts[i])) );
    return pNew;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Min_ManRemoveItem( Vec_Wec_t * vCexes, int iItem, int iFirst, int iLimit )
{
    Vec_Int_t * vLevel, * vLevel0 = Vec_WecEntry(vCexes, iItem);  int i;
    assert( iFirst <= iItem && iItem < iLimit );
    Vec_WecForEachLevelReverseStartStop( vCexes, vLevel, i, iLimit, iFirst )
        if ( Vec_IntSize(vLevel) > 0 )
            break;
    assert( iFirst <= i && iItem <= i );
    Vec_IntClear( vLevel0 );
    if ( iItem < i )
        ABC_SWAP( Vec_Int_t, *vLevel0, *vLevel );
    return -1;
}
int Min_ManAccumulate( Vec_Wec_t * vCexes, int iFirst, int iLimit, Vec_Int_t * vCex )
{
    Vec_Int_t * vLevel;  int i, nCommon, nDiff = 0;
    Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit )
    {
        if ( Vec_IntSize(vLevel) == 0 )
        {
            Vec_IntAppend(vLevel, vCex);
            return nDiff+1;
        }
        nCommon = Vec_IntTwoCountCommon( vLevel, vCex );
        if ( nCommon == Vec_IntSize(vLevel) ) // ignore vCex
            return nDiff;
        if ( nCommon == Vec_IntSize(vCex) ) // remove vLevel
            nDiff += Min_ManRemoveItem( vCexes, i, iFirst, iLimit );
    }
    assert( 0 );
    return ABC_INFINITY;
}
int Min_ManCountSize( Vec_Wec_t * vCexes, int iFirst, int iLimit )
{
    Vec_Int_t * vLevel;  int i, nTotal = 0;
    Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit )
        nTotal += Vec_IntSize(vLevel) > 0;
    return nTotal;
}
Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTries, int nMinCexes, Vec_Int_t * vStats[3], int fUseSim, int fUseSat, int fVerbose )
{
    int fUseSynthesis  = 1;
    abctime clkSim = Abc_Clock(), clkSat = Abc_Clock();
    Vec_Int_t * vOuts  = vOuts0 ? vOuts0 : Vec_IntStartNatural( Gia_ManCoNum(p) );
    Min_Man_t * pNew   = Min_ManFromGia( p, vOuts ); 
    Vec_Wec_t * vCexes = Vec_WecStart( Vec_IntSize(vOuts) * nMinCexes );
    Vec_Int_t * vPatBest = Vec_IntAlloc( 100 );
    Vec_Int_t * vLits = Vec_IntAlloc( 100 );
    Gia_Obj_t * pObj; int i, iObj, nOuts = 0, nSimOuts = 0, nSatOuts = 0;
    vStats[0] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // total calls
    vStats[1] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // successful calls + SAT runs
    vStats[2] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // results
    Min_ManStartValsL( pNew );
    Min_ManForEachCo( pNew, iObj )
    {
        int nAllCalls  = 0;
        int nGoodCalls = 0;
        int nCurrCexes = 0;
        if ( fUseSim && Min_ObjLit0(pNew, iObj) >= 2 )
        {
            while ( nAllCalls++ < nMaxTries )
            {
                if ( Min_LitJustify( pNew, Min_ObjLit0(pNew, iObj) ) )
                {
                    Vec_IntClearAppend( vLits, &pNew->vPat );
                    Vec_IntClearAppend( vPatBest, &pNew->vPat );
                    if ( 1 ) // minimization 
                    {
                        //printf( "%d -> ", Vec_IntSize(vPatBest) );
                        for ( i = 0; i < 20; i++ )
                        {
                            Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
                            if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) )
                                Vec_IntClearAppend( vPatBest, &pNew->vPat );
                        }
                        //printf( "%d   ", Vec_IntSize(vPatBest) );
                    }
                    assert( Vec_IntSize(vPatBest) > 0 );
                    Vec_IntSort( vPatBest, 0 );
                    nCurrCexes += Min_ManAccumulate( vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes, vPatBest );
                    nGoodCalls++;
                }
                if ( nCurrCexes == nMinCexes || nGoodCalls > 10*nCurrCexes )
                    break;
            }
            nSimOuts++;
        }
        assert( nCurrCexes <= nMinCexes );
        assert( nCurrCexes == Min_ManCountSize(vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes) );
        Vec_IntPush( vStats[0], nAllCalls );
        Vec_IntPush( vStats[1], nGoodCalls );
        Vec_IntPush( vStats[2], nCurrCexes );
        nOuts++;
    }
    assert( Vec_IntSize(vOuts) == nOuts );
    assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[0]) );
    assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[1]) );
    assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[2]) );
    clkSim = Abc_Clock() - clkSim;

    if ( fUseSat )
    Gia_ManForEachCoVec( vOuts, p, pObj, i )
    {
        if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) )
            continue;
        {
            abctime clk = Abc_Clock();
            int iObj  = Min_ManCo(pNew, i);
            int Index = Gia_ObjCioId(pObj);
            Vec_Int_t * vMap = Vec_IntAlloc( 100 );
            Gia_Man_t * pCon = Gia_ManDupCones2( p, &Index, 1, vMap );
            Gia_Man_t * pCon1= fUseSynthesis ? Gia_ManAigSyn2( pCon, 0, 1, 0, 100, 0, 0, 0 ) : NULL;
            Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( fUseSynthesis ? pCon1 : pCon, 8, 0, 0, 0, 0 );
            sat_solver* pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
            int Lit          = Abc_Var2Lit( 1, 0 );
            int status       = sat_solver_addclause( pSat, &Lit, &Lit+1 );
            int nAllCalls    = 0;
            int nCurrCexes   = Vec_IntEntry(vStats[2], i);
            //Gia_AigerWrite( pCon, "temp_miter.aig", 0, 0, 0 );
            if ( status == l_True )
            {
                nSatOuts++;
                //printf( "Running SAT for output %d\n", i );
                if ( Min_ObjLit0(pNew, iObj) >= 2 )
                {
                    while ( nAllCalls++ < 100 )
                    {
                        int v, iVar = pCnf->nVars - Gia_ManPiNum(pCon), nVars = Gia_ManPiNum(pCon);
                        if ( nAllCalls > 1 )
                            sat_solver_randomize( pSat, iVar, nVars );
                        status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
                        if ( status != l_True )
                            break;
                        assert( status == l_True );
                        Vec_IntClear( vLits );
                        for ( v = 0; v < nVars; v++ )
                            Vec_IntPush( vLits, Abc_Var2Lit(Vec_IntEntry(vMap, v), !sat_solver_var_value(pSat, iVar + v)) );
                        Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
                        Vec_IntClearAppend( vPatBest, &pNew->vPat );
                        if ( 1 ) // minimization 
                        {
                            //printf( "%d -> ", Vec_IntSize(vPatBest) );
                            for ( v = 0; v < 20; v++ )
                            {
                                Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
                                if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) )
                                    Vec_IntClearAppend( vPatBest, &pNew->vPat );
                            }
                            //printf( "%d   ", Vec_IntSize(vPatBest) );
                        }
                        Vec_IntSort( vPatBest, 0 );
                        nCurrCexes += Min_ManAccumulate( vCexes, i*nMinCexes, (i+1)*nMinCexes, vPatBest );
                        if ( nCurrCexes == nMinCexes || nAllCalls > 10*nCurrCexes )
                            break;
                    }
                }
            }
            Vec_IntWriteEntry( vStats[0], i, nAllCalls*nMaxTries );
            Vec_IntWriteEntry( vStats[1], i, nAllCalls*nMaxTries );
            Vec_IntWriteEntry( vStats[2], i, nCurrCexes );
            sat_solver_delete( pSat );
            Cnf_DataFree( pCnf );
            Gia_ManStop( pCon );
            Gia_ManStopP( &pCon1 );
            Vec_IntFree( vMap );
            if ( fVerbose )
            {
                printf( "SAT solving for output %3d (cexes = %5d) : ", i, nCurrCexes );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
        }
    }
    clkSat = Abc_Clock() - clkSat - clkSim;
    if ( fVerbose )
        printf( "Used simulation for %d and SAT for %d outputs (out of %d).\n", nSimOuts, nSatOuts, nOuts );
    if ( fVerbose )
        Abc_PrintTime( 1, "Simulation time  ", clkSim );
    if ( fVerbose )
        Abc_PrintTime( 1, "SAT solving time ", clkSat );
    //Vec_WecPrint( vCexes, 0 );
    if ( vOuts != vOuts0 )
        Vec_IntFreeP( &vOuts );
    Min_ManStop( pNew );
    Vec_IntFree( vPatBest );
    Vec_IntFree( vLits );
    return vCexes;
}

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

  Synopsis    [Bit-packing for selected patterns.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Min_ManBitPackTry( Vec_Wrd_t * vSimsPi, int nWords, int iPat, Vec_Int_t * vLits )
{
    int i, Lit;
    assert( iPat >= 0 && iPat < 64 * nWords );
    Vec_IntForEachEntry( vLits, Lit, i )
    {
        word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) );   // Lit is based on ObjId
        word * pCare = pInfo + Vec_WrdSize(vSimsPi);
        if ( Abc_InfoHasBit( (unsigned *)pCare, iPat ) && 
             Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation
             return 0;
    }
    Vec_IntForEachEntry( vLits, Lit, i )
    {
        word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) );   // Lit is based on ObjId
        word * pCare = pInfo + Vec_WrdSize(vSimsPi);
        Abc_InfoSetBit( (unsigned *)pCare, iPat );
        if ( Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation
             Abc_InfoXorBit( (unsigned *)pInfo, iPat );
    }
    return 1;
}
int Min_ManBitPackOne( Vec_Wrd_t * vSimsPi, int iPat0, int nWords, Vec_Int_t * vLits )
{
    int iPat, nTotal = 64*nWords;
    for ( iPat = iPat0 + 1; iPat != iPat0; iPat = (iPat + 1) % nTotal )
        if ( Min_ManBitPackTry( vSimsPi, nWords, iPat, vLits ) )
            break;
    return iPat;
}
Vec_Ptr_t * Min_ReloadCexes( Vec_Wec_t * vCexes, int nMinCexes )
{
    Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_WecSize(vCexes) );
    int i, c, nOuts = Vec_WecSize(vCexes)/nMinCexes;
    for ( i = 0; i < nMinCexes; i++ )
    for ( c = 0; c < nOuts; c++ )
    {
        Vec_Int_t * vLevel = Vec_WecEntry( vCexes, c*nMinCexes+i );
        if ( Vec_IntSize(vLevel) )
            Vec_PtrPush( vRes, vLevel );
    }
    return vRes;
}

Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, int nWords0, Vec_Wec_t * vCexes, int fRandom, int nMinCexes, Vec_Int_t * vScores, int fVerbose )
{
    abctime clk = Abc_Clock();
    //int fVeryVerbose = 0;
    Vec_Wrd_t * vSimsPi = NULL;
    Vec_Int_t * vLevel; 
    int w, nBits, nTotal = 0, fFailed = ABC_INFINITY;
    Vec_Int_t * vOrder  = NULL;
    Vec_Ptr_t * vReload = NULL;
    if ( 0 )
    {
        vOrder = Vec_IntStartNatural( Vec_WecSize(vCexes)/nMinCexes );
        assert( Vec_IntSize(vOrder) == Vec_IntSize(vScores) );
        assert( Vec_WecSize(vCexes)%nMinCexes == 0 );
        Abc_MergeSortCost2Reverse( Vec_IntArray(vOrder), Vec_IntSize(vOrder), Vec_IntArray(vScores) );
    }
    else
        vReload = Min_ReloadCexes( vCexes, nMinCexes );
    if ( fVerbose )
        printf( "Packing: " );
    for ( w = nWords0 ? nWords0 : 1; nWords0 ? w <= nWords0 : fFailed > 0; w++ )
    {
        int i, iPatUsed, iPat = 0;
        //int k, iOut;
        Vec_WrdFreeP( &vSimsPi );
        vSimsPi = fRandom ? Vec_WrdStartRandom(2 * Gia_ManCiNum(p) * w) : Vec_WrdStart(2 * Gia_ManCiNum(p) * w);
        Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 );
        Abc_TtClear( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) );
        fFailed = nTotal = 0;
        //Vec_IntForEachEntry( vOrder, iOut, k )
        //Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iOut*nMinCexes, (iOut+1)*nMinCexes )
        Vec_PtrForEachEntry( Vec_Int_t *, vReload, vLevel, i )
        {
            //if ( fVeryVerbose && i%nMinCexes == 0 )
            //    printf( "\n" );
            if ( Vec_IntSize(vLevel) == 0 )
                continue;
            iPatUsed = Min_ManBitPackOne( vSimsPi, iPat, w, vLevel );
            fFailed += iPatUsed == iPat;
            iPat = (iPatUsed + 1) % (64*(w-1) - 1);
            //if ( fVeryVerbose )
            //printf( "Adding output %3d cex %3d to pattern %3d   ", i/nMinCexes, i%nMinCexes, iPatUsed );
            //if ( fVeryVerbose )
            //Vec_IntPrint( vLevel );
            nTotal++;
        }
        if ( fVerbose )
            printf( "W = %d (F = %d)  ", w, fFailed );
//        printf( "Failed patterns = %d\n", fFailed );
    }
    if ( fVerbose )
        printf( "Total = %d\n", nTotal );
    if ( fVerbose )
    {
        nBits = Abc_TtCountOnesVec( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) );
        printf( "Bit-packing is using %d words and %d bits.  Density =%8.4f %%.  ", 
            Vec_WrdSize(vSimsPi)/Gia_ManCiNum(p), nBits, 100.0*nBits/64/Vec_WrdSize(vSimsPi) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    Vec_IntFreeP( &vOrder );
    Vec_PtrFreeP( &vReload );
    return vSimsPi;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Patt_ManOutputErrorCoverage( Vec_Wrd_t * vErrors, int nOuts )
{
    Vec_Int_t * vCounts = Vec_IntAlloc( nOuts );
    int i, nWords = Vec_WrdSize(vErrors)/nOuts;
    assert( Vec_WrdSize(vErrors) == nOuts * nWords );
    for ( i = 0; i < nOuts; i++ )
        Vec_IntPush( vCounts, Abc_TtCountOnesVec(Vec_WrdEntryP(vErrors, nWords * i), nWords) );
    return vCounts;
}
Vec_Wrd_t * Patt_ManTransposeErrors( Vec_Wrd_t * vErrors, int nOuts )
{
    extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
    int nWordsIn  = Vec_WrdSize(vErrors) / nOuts;
    int nWordsOut = Abc_Bit6WordNum(nOuts);
    Vec_Wrd_t * vSims1 = Vec_WrdStart( 64*nWordsIn*nWordsOut );
    Vec_Wrd_t * vSims2 = Vec_WrdStart( 64*nWordsIn*nWordsOut );
    assert( Vec_WrdSize(vErrors) == nWordsIn * nOuts );
    Abc_TtCopy( Vec_WrdArray(vSims1), Vec_WrdArray(vErrors), Vec_WrdSize(vErrors), 0 );
    Extra_BitMatrixTransposeP( vSims1, nWordsIn, vSims2, nWordsOut );
    Vec_WrdFree( vSims1 );
    return vSims2;
}
Vec_Int_t * Patt_ManPatternErrorCoverage( Vec_Wrd_t * vErrors, int nOuts )
{
    int nWords = Vec_WrdSize(vErrors)/nOuts;
    Vec_Wrd_t * vErrors2 = Patt_ManTransposeErrors( vErrors, nOuts );
    Vec_Int_t * vPatErrs = Patt_ManOutputErrorCoverage( vErrors2, 64*nWords );
    Vec_WrdFree( vErrors2 );
    return vPatErrs;
}

#define ERR_REPT_SIZE 32
void Patt_ManProfileErrors( Vec_Int_t * vOutErrs, Vec_Int_t * vPatErrs )
{
    int nOuts = Vec_IntSize(vOutErrs);
    int nPats = Vec_IntSize(vPatErrs);
    int ErrOuts[ERR_REPT_SIZE+1] = {0};
    int ErrPats[ERR_REPT_SIZE+1] = {0};
    int i, Errs, nErrors1 = 0, nErrors2 = 0;
    Vec_IntForEachEntry( vOutErrs, Errs, i )
    {
        nErrors1 += Errs;
        ErrOuts[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++;
    }
    Vec_IntForEachEntry( vPatErrs, Errs, i )
    {
        nErrors2 += Errs;
        ErrPats[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++;
    }
    assert( nErrors1 == nErrors2 );
    // errors/error_outputs/error_patterns
    //printf( "\nError statistics:\n" );
    printf( "Errors =%6d  ", nErrors1 );
    printf( "ErrPOs =%5d  (Ave = %5.2f)    ",  nOuts-ErrOuts[0], 1.0*nErrors1/Abc_MaxInt(1, nOuts-ErrOuts[0]) );
    printf( "Patterns =%5d  (Ave = %5.2f)   ", nPats, 1.0*nErrors1/nPats );
    printf( "Density =%8.4f %%\n",             100.0*nErrors1/nPats/Abc_MaxInt(1, nOuts-ErrOuts[0]) );
    // how many times each output fails
    printf( "Outputs: " );
    for ( i = 0; i <= ERR_REPT_SIZE; i++ )
        if ( ErrOuts[i] )
            printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrOuts[i] );
    printf( "\n" );
    // how many times each patterns fails an output
    printf( "Patterns: " );
    for ( i = 0; i <= ERR_REPT_SIZE; i++ )
        if ( ErrPats[i] )
            printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrPats[i] );
    printf( "\n" );
}
int Patt_ManProfileErrorsOne( Vec_Wrd_t * vErrors, int nOuts )
{
    Vec_Int_t * vCoErrs  = Patt_ManOutputErrorCoverage( vErrors, nOuts );
    Vec_Int_t * vPatErrs = Patt_ManPatternErrorCoverage( vErrors, nOuts );
    Patt_ManProfileErrors( vCoErrs, vPatErrs );
    Vec_IntFree( vPatErrs );
    Vec_IntFree( vCoErrs );
    return 1;
}

Vec_Int_t * Min_ManGetUnsolved( Gia_Man_t * p )
{
    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
    int i, Driver;
    Gia_ManForEachCoDriverId( p, Driver, i )
        if ( Driver > 0 )
            Vec_IntPush( vRes, i );
    if ( Vec_IntSize(vRes) == 0 )
        Vec_IntFreeP( &vRes );
    return vRes;
}
Vec_Wrd_t * Min_ManRemapSims( int nInputs, Vec_Int_t * vMap, Vec_Wrd_t * vSimsPi )
{
    int i, iObj, nWords = Vec_WrdSize(vSimsPi)/Vec_IntSize(vMap);
    Vec_Wrd_t * vSimsNew = Vec_WrdStart( 2 * nInputs * nWords );
    //Vec_Wrd_t * vSimsNew = Vec_WrdStartRandom( nInputs * nWords );
    //Vec_WrdFillExtra( vSimsNew, 2 * nInputs * nWords, 0 );
    assert( Vec_WrdSize(vSimsPi)%Vec_IntSize(vMap) == 0 );
    Vec_WrdShrink( vSimsNew, Vec_WrdSize(vSimsNew)/2 );
    Vec_IntForEachEntry( vMap, iObj, i )
    {
        Abc_TtCopy( Vec_WrdArray(vSimsNew) + (iObj-1)*nWords, Vec_WrdArray(vSimsPi) + i*nWords, nWords, 0 );
        Abc_TtCopy( Vec_WrdLimit(vSimsNew) + (iObj-1)*nWords, Vec_WrdLimit(vSimsPi) + i*nWords, nWords, 0 );
    }
    return vSimsNew;
}
Vec_Wrd_t * Gia_ManCollectSims( Gia_Man_t * pSwp, int nWords, Vec_Int_t * vOuts, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose )
{
    Vec_Int_t * vStats[3] = {0};  int i, iObj;
    Vec_Int_t * vMap    = Vec_IntAlloc( 100 );
    Gia_Man_t * pSwp2   = Gia_ManDupCones2( pSwp, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vMap );
    Vec_Wec_t * vCexes  = Min_ManComputeCexes( pSwp2, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );
    if ( Vec_IntSum(vStats[2]) == 0 )
    {
        for ( i = 0; i < 3; i++ )
            Vec_IntFree( vStats[i] );
        Vec_IntFree( vMap );
        Gia_ManStop( pSwp2 );
        Vec_WecFree( vCexes );
        return NULL;
    }
    else
    {
        Vec_Wrd_t * vSimsPi = Min_ManBitPack( pSwp2, nWords, vCexes, 1, nMinCexes, vStats[0], fVerbose );
        Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( pSwp2, vSimsPi, 1 );
        Vec_Int_t * vCounts = Patt_ManOutputErrorCoverage( vSimsPo, Vec_IntSize(vOuts) );
        if ( fVerbose )
            Patt_ManProfileErrorsOne( vSimsPo, Vec_IntSize(vOuts) );
        if ( fVeryVerbose )
        {
            printf( "Unsolved = %4d  ", Vec_IntSize(vOuts) );
            Gia_ManPrintStats( pSwp2, NULL );
            Vec_IntForEachEntry( vOuts, iObj, i )
            {
                printf( "%4d : ", i );
                printf( "Out = %5d  ",    Vec_IntEntry(vMap, i) );
                printf( "SimAll =%8d  ",  Vec_IntEntry(vStats[0], i) );
                printf( "SimGood =%8d  ", Vec_IntEntry(vStats[1], i) );
                printf( "PatsAll =%8d  ", Vec_IntEntry(vStats[2], i) );
                printf( "Count = %5d  ",  Vec_IntEntry(vCounts, i) );
                printf( "\n" );
                if ( i == 20 )
                    break;
            }
        }
        for ( i = 0; i < 3; i++ )
            Vec_IntFree( vStats[i] );
        Vec_IntFree( vCounts );
        Vec_WrdFree( vSimsPo );
        Vec_WecFree( vCexes );
        Gia_ManStop( pSwp2 );
        //printf( "Compressing inputs: %5d -> %5d\n", Gia_ManCiNum(pSwp), Vec_IntSize(vMap) );
        vSimsPi = Min_ManRemapSims( Gia_ManCiNum(pSwp), vMap, vSimsPo = vSimsPi );
        Vec_WrdFree( vSimsPo );
        Vec_IntFree( vMap );
        return vSimsPi;
    }
}
Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose )
{
    abctime clk = Abc_Clock();
    extern Gia_Man_t *    Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose );
    Gia_Man_t * pSwp    = Cec4_ManSimulateTest4( p, nConf, nConf2, 0 );
    abctime clkSweep    = Abc_Clock() - clk;
    int nArgs           = fVerbose ? printf( "Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.\n", 
                          nConf, nConf2, nMaxTries, nMinCexes, fUseSim, fUseSat ) : 0;
    Vec_Int_t * vOuts   = Min_ManGetUnsolved( pSwp );
    Vec_Wrd_t * vSimsPi = vOuts ? Gia_ManCollectSims( pSwp, 0, vOuts, nMaxTries, nMinCexes, fUseSim, fUseSat, fVerbose, fVeryVerbose ) : NULL;
    if ( vOuts == NULL )
        printf( "There is no satisfiable outputs.\n" );
    if ( fVerbose )
        Abc_PrintTime( 1, "Sweep time", clkSweep );
    if ( fVerbose )
        Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
    Vec_IntFreeP( &vOuts );
    Gia_ManStop( pSwp ); 
    nArgs = 0;
    return vSimsPi;
}
void Min_ManTest2( Gia_Man_t * p )
{
    Vec_Wrd_t * vSimsPi = Min_ManCollect( p, 100000, 100000, 10000, 20, 1, 0, 1, 1 );
    Vec_WrdFreeP( &vSimsPi );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END