giaSweeper.c

Go to the documentation of this file.

 
#include "gia.h"
#include "base/main/main.h"
#include "sat/bsat/satSolver.h"
#include "proof/ssc/ssc.h"
 
ABC_NAMESPACE_IMPL_START
 
/*
 
SAT sweeping/equivalence checking requires the following steps:
- Creating probes
  These APIs should be called for all internal points in the logic, which may be used as
      - nodes representing conditions to be used as constraints
      - nodes representing functions to be equivalence checked
      - nodes representing functions needed by the user at the end of SAT sweeping
  Creating new probe using  Gia_SweeperProbeCreate():   int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit );
  Delete existing probe using Gia_SweeperProbeDelete(): int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId );
  Update existing probe using Gia_SweeperProbeUpdate(): int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLit );
  Comments:
      - a probe is identified by its 0-based ID, which is returned by above procedures
      - GIA literal of the probe is returned by       int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
- Adding/removing conditions on the current path by calling Gia_SweeperCondPush() and Gia_SweeperCondPop()
      extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId );
      extern void Gia_SweeperCondPop( Gia_Man_t * p );
- Performing equivalence checking by calling     int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
      (resource limits, such as the number of conflicts, will be controllable by dedicated GIA APIs)
- The resulting AIG to be returned to the user by calling Gia_SweeperExtractUserLogic()
      Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames )
 
*/

 
typedef struct Swp_Man_t_ Swp_Man_t;
struct Swp_Man_t_
{
    Gia_Man_t *    pGia;        // GIA manager under construction
    int            nConfMax;    // conflict limit in seconds
    int            nTimeOut;    // runtime limit in seconds
    Vec_Int_t *    vProbes;     // probes
    Vec_Int_t *    vCondProbes; // conditions as probes
    Vec_Int_t *    vCondAssump; // conditions as SAT solver literals
    // equivalence checking
    sat_solver *   pSat;        // SAT solver 
    Vec_Int_t *    vId2Lit;     // mapping of Obj IDs into SAT literal
    Vec_Int_t *    vFront;      // temporary frontier
    Vec_Int_t *    vFanins;     // temporary fanins
    Vec_Int_t *    vCexSwp;     // sweeper counter-example
    Vec_Int_t *    vCexUser;    // user-visible counter-example
    int            nSatVars;    // counter of SAT variables
    // statistics
    int            nSatCalls;
    int            nSatCallsSat;
    int            nSatCallsUnsat;
    int            nSatCallsUndec;
    int            nSatProofs;
    abctime        timeStart;
    abctime        timeTotal;
    abctime        timeCnf;
    abctime        timeSat;
    abctime        timeSatSat;
    abctime        timeSatUnsat;
    abctime        timeSatUndec;
};
 
static inline int  Swp_ManObj2Lit( Swp_Man_t * p, int Id )              { return Vec_IntGetEntry( p->vId2Lit, Id );              }
static inline int  Swp_ManLit2Lit( Swp_Man_t * p, int Lit )             { assert( Vec_IntEntry(p->vId2Lit, Abc_Lit2Var(Lit)) ); return Abc_Lit2LitL( Vec_IntArray(p->vId2Lit), Lit );  }
static inline void Swp_ManSetObj2Lit( Swp_Man_t * p, int Id, int Lit )  { assert( Lit > 0 ); Vec_IntSetEntry( p->vId2Lit, Id, Lit );                }

    
static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
{
    Swp_Man_t * p;
    int Lit;
    assert( Vec_IntSize(&pGia->vHTable) );
    pGia->pData = p = ABC_CALLOC( Swp_Man_t, 1 );
    p->pGia         = pGia;
    p->nConfMax     = 1000;
    p->vProbes      = Vec_IntAlloc( 100 );
    p->vCondProbes  = Vec_IntAlloc( 100 );
    p->vCondAssump  = Vec_IntAlloc( 100 );
    p->vId2Lit      = Vec_IntAlloc( 10000 );
    p->vFront       = Vec_IntAlloc( 100 );
    p->vFanins      = Vec_IntAlloc( 100 );
    p->vCexSwp      = Vec_IntAlloc( 100 );
    p->pSat         = sat_solver_new();
    p->nSatVars     = 1;
    sat_solver_setnvars( p->pSat, 1000 );
    Swp_ManSetObj2Lit( p, 0, (Lit = Abc_Var2Lit(p->nSatVars++, 0)) );
    Lit = Abc_LitNot(Lit);
    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
    p->timeStart    = Abc_Clock();
    return p;
}
static inline void Swp_ManStop( Gia_Man_t * pGia )
{
    Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
    sat_solver_delete( p->pSat );
    Vec_IntFree( p->vFanins );
    Vec_IntFree( p->vCexSwp );
    Vec_IntFree( p->vId2Lit );
    Vec_IntFree( p->vFront );
    Vec_IntFree( p->vProbes );
    Vec_IntFree( p->vCondProbes );
    Vec_IntFree( p->vCondAssump );
    ABC_FREE( p );
    pGia->pData = NULL;
}
Gia_Man_t * Gia_SweeperStart( Gia_Man_t * pGia )
{
    if ( pGia == NULL )
        pGia = Gia_ManStart( 10000 );
    if ( Vec_IntSize(&pGia->vHTable) == 0 )
        Gia_ManHashStart( pGia );
    // recompute fPhase and fMark1 to mark multiple fanout nodes if AIG is already defined!!!
 
    Swp_ManStart( pGia );
    pGia->fSweeper = 1;
    return pGia;
}
void Gia_SweeperStop( Gia_Man_t * pGia )
{
    pGia->fSweeper = 0;
    Swp_ManStop( pGia );
    Gia_ManHashStop( pGia );
//    Gia_ManStop( pGia );
}
int Gia_SweeperIsRunning( Gia_Man_t * pGia )
{
    return (pGia->pData != NULL);
}
double Gia_SweeperMemUsage( Gia_Man_t * pGia )
{
    Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
    double nMem = sizeof(Swp_Man_t);
    nMem += Vec_IntCap(p->vProbes);
    nMem += Vec_IntCap(p->vCondProbes);
    nMem += Vec_IntCap(p->vCondAssump);
    nMem += Vec_IntCap(p->vId2Lit);
    nMem += Vec_IntCap(p->vFront);
    nMem += Vec_IntCap(p->vFanins);
    nMem += Vec_IntCap(p->vCexSwp);
    return 4.0 * nMem;
}
void Gia_SweeperPrintStats( Gia_Man_t * pGia )
{
    Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
    double nMemSwp = Gia_SweeperMemUsage(pGia);
    double nMemGia = (double)Gia_ManObjNum(pGia)*(sizeof(Gia_Obj_t) + sizeof(int));
    double nMemSat = sat_solver_memory(p->pSat);
    double nMemTot = nMemSwp + nMemGia + nMemSat;
    printf( "SAT sweeper statistics:\n" );
    printf( "Memory usage:\n" );
    ABC_PRMP( "Sweeper         ", nMemSwp, nMemTot );
    ABC_PRMP( "AIG manager     ", nMemGia, nMemTot );
    ABC_PRMP( "SAT solver      ", nMemSat, nMemTot );
    ABC_PRMP( "TOTAL           ", nMemTot, nMemTot );
    printf( "Runtime usage:\n" );
    p->timeTotal = Abc_Clock() - p->timeStart;
    ABC_PRTP( "CNF construction", p->timeCnf,      p->timeTotal );
    ABC_PRTP( "SAT solving     ", p->timeSat,      p->timeTotal );
    ABC_PRTP( "    Sat         ", p->timeSatSat,   p->timeTotal );
    ABC_PRTP( "    Unsat       ", p->timeSatUnsat, p->timeTotal );
    ABC_PRTP( "    Undecided   ", p->timeSatUndec, p->timeTotal );
    ABC_PRTP( "TOTAL RUNTIME   ", p->timeTotal,    p->timeTotal );
    printf( "GIA: " );
    Gia_ManPrintStats( pGia, NULL );
    printf( "SAT calls = %d. Sat = %d. Unsat = %d. Undecided = %d.  Proofs = %d.\n", 
        p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nSatCallsUndec, p->nSatProofs );
    Sat_SolverPrintStats( stdout, p->pSat );
}

void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    pSwp->nConfMax = nConfMax;
}
void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    pSwp->nTimeOut = nSeconds;
}
Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    assert( pSwp->vCexUser == NULL || Vec_IntSize(pSwp->vCexUser) == Gia_ManPiNum(p) );
    return pSwp->vCexUser;
}
    
// create new probe
int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    int ProbeId = Vec_IntSize(pSwp->vProbes);
    assert( iLit >= 0 );
    Vec_IntPush( pSwp->vProbes, iLit );
    return ProbeId;
}
// delete existing probe
int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
    assert( iLit >= 0 );
    Vec_IntWriteEntry(pSwp->vProbes, ProbeId, -1);
    return iLit;
}
// update existing probe
int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLitNew )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
    assert( iLit >= 0 );
    Vec_IntWriteEntry(pSwp->vProbes, ProbeId, iLitNew);
    return iLit;
}
// returns literal associated with the probe
int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
    assert( iLit >= 0 );
    return iLit;
}

Vec_Int_t * Gia_SweeperCollectValidProbeIds( Gia_Man_t * p )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    Vec_Int_t * vProbeIds = Vec_IntAlloc( 1000 );
    int iLit, ProbeId;
    Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
    {
        if ( iLit < 0 ) continue;
        Vec_IntPush( vProbeIds, ProbeId );
    }
    return vProbeIds;
}

void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    Vec_IntPush( pSwp->vCondProbes, ProbeId );
}
int Gia_SweeperCondPop( Gia_Man_t * p )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    return Vec_IntPop( pSwp->vCondProbes );
}
Vec_Int_t * Gia_SweeperCondVector( Gia_Man_t * p )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    return pSwp->vCondProbes;
}
 

static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjIds )
{
    if ( !Gia_ObjIsAnd(pObj) )
        return;
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    Gia_ManExtract_rec( p, Gia_ObjFanin0(pObj), vObjIds );
    Gia_ManExtract_rec( p, Gia_ObjFanin1(pObj), vObjIds );
    Vec_IntPush( vObjIds, Gia_ObjId(p, pObj) );
}
Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames )
{
    Vec_Int_t * vObjIds, * vValues;
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj;
    int i, ProbeId;
    assert( vInNames  == NULL || Gia_ManPiNum(p) == Vec_PtrSize(vInNames) );
    assert( vOutNames == NULL || Vec_IntSize(vProbeIds) == Vec_PtrSize(vOutNames) );
    // create new
    Gia_ManIncrementTravId( p );
    vObjIds = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntry( vProbeIds, ProbeId, i )
    {
        pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
        Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
    }
    // create new manager
    pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + Vec_IntSize(vProbeIds) + 100 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachPi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create internal nodes
    Gia_ManHashStart( pNew );
    vValues = Vec_IntAlloc( Vec_IntSize(vObjIds) );
    Gia_ManForEachObjVec( vObjIds, p, pObj, i )
    {
        Vec_IntPush( vValues, pObj->Value );
        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    }
    Gia_ManHashStop( pNew );
    // create outputs
    Vec_IntForEachEntry( vProbeIds, ProbeId, i )
    {
        pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
        Gia_ManAppendCo( pNew, Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj) );
    }
    // return the values back
    Gia_ManForEachPi( p, pObj, i )
        pObj->Value = 0;
    Gia_ManForEachObjVec( vObjIds, p, pObj, i )
        pObj->Value = Vec_IntEntry( vValues, i );
    Vec_IntFree( vObjIds );
    Vec_IntFree( vValues );
    // duplicate if needed
    if ( Gia_ManHasDangling(pNew) )
    {
        pNew = Gia_ManCleanup( pTemp = pNew );
        Gia_ManStop( pTemp );
    }
    // copy names if present
    if ( vInNames )
        pNew->vNamesIn = Vec_PtrDupStr( vInNames );
    if ( vOutNames )
        pNew->vNamesOut = Vec_PtrDupStr( vOutNames );
    return pNew;
}

void Gia_SweeperLogicDump( Gia_Man_t * p, Vec_Int_t * vProbeIds, int fDumpConds, char * pFileName )
{
    Gia_Man_t * pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeIds, NULL, NULL );
    Vec_Int_t * vProbeConds = Gia_SweeperCondVector( p );
    printf( "Dumping logic cones" );
    if ( fDumpConds && Vec_IntSize(vProbeConds) > 0 )
    {
        Gia_Man_t * pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
        Gia_ManDupAppendShare( pGiaOuts, pGiaCond );
        pGiaOuts->nConstrs = Gia_ManPoNum(pGiaCond);
        Gia_ManHashStop( pGiaOuts );
        Gia_ManStop( pGiaCond );
        printf( " and conditions" );
    }
    Gia_AigerWrite( pGiaOuts, pFileName, 0, 0, 0 );
    Gia_ManStop( pGiaOuts );
    printf( " into file \"%s\".\n", pFileName );
}

Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime )
{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    Vec_Int_t * vObjIds;
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj;
    int i, iLit, ProbeId;
 
    // collect all internal nodes pointed to by currently-used probes
    Gia_ManIncrementTravId( p );
    vObjIds = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
    {
        if ( iLit < 0 ) continue;
        pObj = Gia_Lit2Obj( p, iLit );
        Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
    }
    // create new manager
    pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + 100 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachPi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create internal nodes
    Gia_ManHashStart( pNew );
    Gia_ManForEachObjVec( vObjIds, p, pObj, i )
        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    Gia_ManHashStop( pNew );
    // create outputs
    Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
    {
        if ( iLit < 0 ) continue;
        pObj = Gia_Lit2Obj( p, iLit );
        iLit = Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj);
        Vec_IntWriteEntry( pSwp->vProbes, ProbeId, iLit );
    }
    Vec_IntFree( vObjIds );
    // duplicate if needed
    if ( Gia_ManHasDangling(pNew) )
    {
        pNew = Gia_ManCleanup( pTemp = pNew );
        Gia_ManStop( pTemp );
    }
    // execute command line
    if ( pCommLime )
    {
        // set pNew to be current GIA in ABC
        Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
        // execute command line pCommLine using Abc_CmdCommandExecute()
        Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
        // get pNew to be current GIA in ABC     
        pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
    }
    // restart the SAT solver
    Vec_IntClear( pSwp->vId2Lit );
    sat_solver_delete( pSwp->pSat );
    pSwp->pSat         = sat_solver_new();
    pSwp->nSatVars     = 1;
    sat_solver_setnvars( pSwp->pSat, 1000 );
    Swp_ManSetObj2Lit( pSwp, 0, (iLit = Abc_Var2Lit(pSwp->nSatVars++, 0)) );
    iLit = Abc_LitNot(iLit);
    sat_solver_addclause( pSwp->pSat, &iLit, &iLit + 1 );
    pSwp->timeStart    = Abc_Clock();
    // return the result
    pNew->pData = p->pData; p->pData = NULL;
    Gia_ManStop( p );
    return pNew;
}
 

static void Gia_ManAddClausesMux( Swp_Man_t * p, Gia_Obj_t * pNode )
{
    Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
    int pLits[4], LitF, LitI, LitT, LitE, RetValue;
    assert( !Gia_IsComplement( pNode ) );
    assert( Gia_ObjIsMuxType( pNode ) );
    // get nodes (I = if, T = then, E = else)
    pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
    // get the Litiable numbers
    LitF = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
    LitI = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeI) );
    LitT = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeT) );
    LitE = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeE) );
 
    // f = ITE(i, t, e)
 
    // i' + t' + f
    // i' + t  + f'
    // i  + e' + f
    // i  + e  + f'
 
    // create four clauses
    pLits[0] = Abc_LitNotCond(LitI, 1);
    pLits[1] = Abc_LitNotCond(LitT, 1);
    pLits[2] = Abc_LitNotCond(LitF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = Abc_LitNotCond(LitI, 1);
    pLits[1] = Abc_LitNotCond(LitT, 0);
    pLits[2] = Abc_LitNotCond(LitF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = Abc_LitNotCond(LitI, 0);
    pLits[1] = Abc_LitNotCond(LitE, 1);
    pLits[2] = Abc_LitNotCond(LitF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = Abc_LitNotCond(LitI, 0);
    pLits[1] = Abc_LitNotCond(LitE, 0);
    pLits[2] = Abc_LitNotCond(LitF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
 
    // two additional clauses
    // t' & e' -> f'
    // t  & e  -> f
 
    // t  + e   + f'
    // t' + e'  + f
 
    if ( LitT == LitE )
    {
//        assert( fCompT == !fCompE );
        return;
    }
 
    pLits[0] = Abc_LitNotCond(LitT, 0);
    pLits[1] = Abc_LitNotCond(LitE, 0);
    pLits[2] = Abc_LitNotCond(LitF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = Abc_LitNotCond(LitT, 1);
    pLits[1] = Abc_LitNotCond(LitE, 1);
    pLits[2] = Abc_LitNotCond(LitF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
}

static void Gia_ManAddClausesSuper( Swp_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSuper )
{
    int i, RetValue, Lit, LitNode, pLits[2];
    assert( !Gia_IsComplement(pNode) );
    assert( Gia_ObjIsAnd( pNode ) );
    // suppose AND-gate is A & B = C
    // add !A => !C   or   A + !C
    // add !B => !C   or   B + !C
    LitNode = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
    Vec_IntForEachEntry( vSuper, Lit, i )
    {
        pLits[0] = Swp_ManLit2Lit( p, Lit );
        pLits[1] = Abc_LitNot( LitNode );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // update literals
        Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
    }
    // add A & B => C   or   !A + !B + C
    Vec_IntPush( vSuper, LitNode );
    RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) );
    assert( RetValue );
    (void) RetValue;
}
 

static void Gia_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
{
    // stop at complements, shared, PIs, and MUXes
    if ( Gia_IsComplement(pObj) || pObj->fMark1 || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
    {
        Vec_IntPushUnique( vSuper, Gia_Obj2Lit(p, pObj) );
        return;
    }
    Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
    Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
}
static void Gia_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
{
    assert( !Gia_IsComplement(pObj) );
    assert( Gia_ObjIsAnd(pObj) );
    Vec_IntClear( vSuper );
    Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
    Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
}

static void Gia_ManObjAddToFrontier( Swp_Man_t * p, int Id, Vec_Int_t * vFront )
{
    Gia_Obj_t * pObj;
    if ( Id == 0 || Swp_ManObj2Lit(p, Id) )
        return;
    pObj = Gia_ManObj( p->pGia, Id );
    Swp_ManSetObj2Lit( p, Id, Abc_Var2Lit(p->nSatVars++, pObj->fPhase) );
    sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
    if ( Gia_ObjIsAnd(pObj) )
        Vec_IntPush( vFront, Id );
}
static void Gia_ManCnfNodeAddToSolver( Swp_Man_t * p, int NodeId )
{
    Gia_Obj_t * pNode;
    int i, k, Id, Lit;
    abctime clk;
    // quit if CNF is ready
    if ( NodeId == 0 || Swp_ManObj2Lit(p, NodeId) )
        return;
clk = Abc_Clock();
    // start the frontier
    Vec_IntClear( p->vFront );
    Gia_ManObjAddToFrontier( p, NodeId, p->vFront );
    // explore nodes in the frontier
    Gia_ManForEachObjVec( p->vFront, p->pGia, pNode, i )
    {
        // create the supergate
        assert( Swp_ManObj2Lit(p, Gia_ObjId(p->pGia, pNode)) );
        if ( Gia_ObjIsMuxType(pNode) )
        {
            Vec_IntClear( p->vFanins );
            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin0(pNode) ) );
            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin1(pNode) ) );
            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin0(pNode) ) );
            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin1(pNode) ) );
            Vec_IntForEachEntry( p->vFanins, Id, k )
                Gia_ManObjAddToFrontier( p, Id, p->vFront );
            Gia_ManAddClausesMux( p, pNode );
        }
        else
        {
            Gia_ManCollectSuper( p->pGia, pNode, p->vFanins );
            Vec_IntForEachEntry( p->vFanins, Lit, k )
                Gia_ManObjAddToFrontier( p, Abc_Lit2Var(Lit), p->vFront );
            Gia_ManAddClausesSuper( p, pNode, p->vFanins );
        }
        assert( Vec_IntSize(p->vFanins) > 1 );
    }
p->timeCnf += Abc_Clock() - clk;
}
 

static Vec_Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_solver * pSat, Vec_Int_t * vCex )
{
    Gia_Obj_t * pObj;
    int i, LitSat, Value;
    Vec_IntClear( vCex );
    Gia_ManForEachPi( pGia, pObj, i )
    {
        if ( Gia_ObjId(pGia, pObj) >= Vec_IntSize(vId2Lit) )
        {
            Vec_IntPush( vCex, 2 );
            continue;
        }
        LitSat = Vec_IntEntry( vId2Lit, Gia_ObjId(pGia, pObj) );
        if ( LitSat == 0 )
        {
            Vec_IntPush( vCex, 2 );
            continue;
        }
        assert( LitSat > 0 );
        Value = sat_solver_var_value(pSat, Abc_Lit2Var(LitSat)) ^ Abc_LitIsCompl(LitSat);
        Vec_IntPush( vCex, Value );
    }
    return vCex;
}

int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
{
    Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
    int iLitOld, iLitNew, iLitAig, pLitsSat[2], RetValue, RetValue1, ProbeId, i;
    abctime clk;
    p->nSatCalls++;
    assert( p->pSat != NULL );
    p->vCexUser = NULL;
 
    // get the literals
    iLitOld = Gia_SweeperProbeLit( pGia, Probe1 );
    iLitNew = Gia_SweeperProbeLit( pGia, Probe2 );
    // if the literals are identical, the probes are equivalent
    if ( iLitOld == iLitNew )
        return 1;
    // if the literals are opposites, the probes are not equivalent
    if ( Abc_LitRegular(iLitOld) == Abc_LitRegular(iLitNew) )
    {
        Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 2 );
        p->vCexUser = p->vCexSwp;
        return 0;
    }
    // order the literals
    if ( iLitOld < iLitNew )
        ABC_SWAP( int, iLitOld, iLitNew );
    assert( iLitOld > iLitNew );
 
    // create logic cones and the array of assumptions
    Vec_IntClear( p->vCondAssump );
    Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
    {
        iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
        Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
        Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
    }
    Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) );
    Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) );
    sat_solver_compress( p->pSat );
 
    // set the SAT literals
    pLitsSat[0] = Swp_ManLit2Lit( p, iLitOld );
    pLitsSat[1] = Swp_ManLit2Lit( p, iLitNew );
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    Vec_IntPush( p->vCondAssump, pLitsSat[0] );
    Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[1]) );
 
    // set runtime limit for this call
    if ( p->nTimeOut )
        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
 
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump), 
        (ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
        pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
        RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
        assert( RetValue );
        pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
p->timeSatUnsat += Abc_Clock() - clk;
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
        p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatCallsUndec++;
        return -1;
    }
 
    // if the old node was constant 0, we already know the answer
    if ( Gia_ManIsConstLit(iLitNew) )
    {
        p->nSatProofs++;
        return 1;
    }
 
    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
    Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[0]) );
    Vec_IntPush( p->vCondAssump, pLitsSat[1] );
 
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump), 
        (ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
        pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
        RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
        assert( RetValue );
        pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
p->timeSatUnsat += Abc_Clock() - clk;
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
        p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatCallsUndec++;
        return -1;
    }
    // return SAT proof
    p->nSatProofs++;
    return 1;
}

int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
{
    Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
    int RetValue, ProbeId, iLitAig, i;
    abctime clk;
    assert( p->pSat != NULL );
    p->nSatCalls++;
    p->vCexUser = NULL;
 
    // create logic cones and the array of assumptions
    Vec_IntClear( p->vCondAssump );
    Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
    {
        iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
        Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
        Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
    }
    sat_solver_compress( p->pSat );
 
    // set runtime limit for this call
    if ( p->nTimeOut )
        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
 
clk = Abc_Clock();
    RetValue = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump), 
        (ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue == l_False )
    {
        assert( Vec_IntSize(p->vCondProbes) > 0 );
p->timeSatUnsat += Abc_Clock() - clk;
        p->nSatCallsUnsat++;
        p->nSatProofs++;
        return 1;
    }
    else if ( RetValue == l_True )
    {
        p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatCallsUndec++;
        return -1;
    }
}

Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc )
{
    Vec_Int_t * vOutLits;
    Gia_Obj_t * pObj;
    int i;
    assert( Gia_SweeperIsRunning(pDst) );
    if ( vProbes )
        assert( Vec_IntSize(vProbes) == Gia_ManPiNum(pSrc) );
    else
        assert( Gia_ManPiNum(pDst) == Gia_ManPiNum(pSrc) );
    Gia_ManForEachPi( pSrc, pObj, i )
        pObj->Value = vProbes ? Gia_SweeperProbeLit(pDst, Vec_IntEntry(vProbes, i)) : Gia_Obj2Lit(pDst,Gia_ManPi(pDst, i));
    Gia_ManForEachAnd( pSrc, pObj, i )
        pObj->Value = Gia_ManHashAnd( pDst, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    vOutLits = Vec_IntAlloc( Gia_ManPoNum(pSrc) );
    Gia_ManForEachPo( pSrc, pObj, i )
        Vec_IntPush( vOutLits, Gia_ObjFanin0Copy(pObj) );
    return vOutLits;
}

Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, int nConfs, int fVerify, int fVerbose )
{
    Vec_Int_t * vProbeConds;
    Gia_Man_t * pGiaCond, * pGiaOuts, * pGiaRes;
    Ssc_Pars_t Pars, * pPars = &Pars;
    Ssc_ManSetDefaultParams( pPars );
    pPars->nWords   = nWords;
    pPars->nBTLimit = nConfs;
    pPars->fVerify  = fVerify;
    pPars->fVerbose = fVerbose;
    // sweeper is running
    assert( Gia_SweeperIsRunning(p) );
    // extract conditions and logic cones
    vProbeConds = Gia_SweeperCondVector( p );
    pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
    pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
    Gia_ManSetPhase( pGiaOuts );
    // if there is no conditions, define constant true constraint (constant 0 output)
    if ( Gia_ManPoNum(pGiaCond) == 0 )
        Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() );
    // perform sweeping under constraints
    pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars );
    Gia_ManStop( pGiaCond );
    Gia_ManStop( pGiaOuts );
    return pGiaRes;
}

int Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerify, int fVerbose )
{
    Gia_Man_t * pNew;
    Vec_Int_t * vLits;
    int ProbeId, i;
    // sweeper is running
    assert( Gia_SweeperIsRunning(p) );
    // sweep the logic
    pNew = Gia_SweeperSweep( p, vProbeIds, nWords, nConfs, fVerify, fVerbose );
    if ( pNew == NULL )
        return 0;
    // execute command line
    if ( pCommLime )
    {
        // set pNew to be current GIA in ABC
        Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
        // execute command line pCommLine using Abc_CmdCommandExecute()
        Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
        // get pNew to be current GIA in ABC     
        pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
    }
    // return logic back into the main manager
    vLits = Gia_SweeperGraft( p, NULL, pNew );
    Gia_ManStop( pNew );
    // update the array of probes
    Vec_IntForEachEntry( vProbeIds, ProbeId, i )
        Gia_SweeperProbeUpdate( p, ProbeId, Vec_IntEntry(vLits, i) );
    Vec_IntFree( vLits );        
    return 1;
}

int Gia_SweeperRun( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int fVerbose )
{
    Gia_Man_t * pNew;
    Vec_Int_t * vLits;
    int ProbeId, i;
    // sweeper is running
    assert( Gia_SweeperIsRunning(p) );
    // sweep the logic
    pNew = Gia_SweeperExtractUserLogic( p, vProbeIds, NULL, NULL );
    // execute command line
    if ( pCommLime )
    {
        if ( fVerbose )
            printf( "GIA manager statistics before and after applying \"%s\":\n", pCommLime );
        if ( fVerbose )
            Gia_ManPrintStats( pNew, NULL );
        // set pNew to be current GIA in ABC
        Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
        // execute command line pCommLine using Abc_CmdCommandExecute()
        Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
        // get pNew to be current GIA in ABC     
        pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
        if ( fVerbose )
            Gia_ManPrintStats( pNew, NULL );
    }
    // return logic back into the main manager
    vLits = Gia_SweeperGraft( p, NULL, pNew );
    Gia_ManStop( pNew );
    // update the array of probes
    Vec_IntForEachEntry( vProbeIds, ProbeId, i )
        Gia_SweeperProbeUpdate( p, ProbeId, Vec_IntEntry(vLits, i) );
    Vec_IntFree( vLits );        
    return 1;
}

Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * pInit, int nWords, int nConfs, int fVerbose )
{
    Gia_Man_t * p, * pGia;
    Gia_Obj_t * pObj;
    Vec_Int_t * vOuts;
    int i;
    // add one-hotness constraints
    p = Gia_ManDupOneHot( pInit );
    // create sweeper
    Gia_SweeperStart( p );
    // collect outputs and create conditions
    vOuts = Vec_IntAlloc( Gia_ManPoNum(p) );
    Gia_ManForEachPo( p, pObj, i )
        if ( i < Gia_ManPoNum(p) - p->nConstrs )  // this is the user's output
            Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p,  Gia_ObjFaninLit0p(p, pObj) ) );
        else // this is a constraint
            Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) );
    // perform the sweeping
    pGia = Gia_SweeperSweep( p, vOuts, nWords, nConfs, fVerbose, 0 );
//    pGia = Gia_ManDup( p );
    Vec_IntFree( vOuts );
    // sop the sweeper
    Gia_SweeperStop( p );
    Gia_ManStop( p );
    return pGia;
}
 

 
ABC_NAMESPACE_IMPL_END