giaSweeper.c File Reference

#include "gia.h"
#include "base/main/main.h"
#include "sat/bsat/satSolver.h"
#include "proof/ssc/ssc.h"

Include dependency graph for giaSweeper.c:

Go to the source code of this file.

Classes
struct	Swp_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Swp_Man_t_	Swp_Man_t
	DECLARATIONS ///.

Functions
Gia_Man_t *	Gia_SweeperStart (Gia_Man_t *pGia)
void	Gia_SweeperStop (Gia_Man_t *pGia)
int	Gia_SweeperIsRunning (Gia_Man_t *pGia)
double	Gia_SweeperMemUsage (Gia_Man_t *pGia)
void	Gia_SweeperPrintStats (Gia_Man_t *pGia)
void	Gia_SweeperSetConflictLimit (Gia_Man_t *p, int nConfMax)
void	Gia_SweeperSetRuntimeLimit (Gia_Man_t *p, int nSeconds)
Vec_Int_t *	Gia_SweeperGetCex (Gia_Man_t *p)
int	Gia_SweeperProbeCreate (Gia_Man_t *p, int iLit)
int	Gia_SweeperProbeDelete (Gia_Man_t *p, int ProbeId)
int	Gia_SweeperProbeUpdate (Gia_Man_t *p, int ProbeId, int iLitNew)
int	Gia_SweeperProbeLit (Gia_Man_t *p, int ProbeId)
Vec_Int_t *	Gia_SweeperCollectValidProbeIds (Gia_Man_t *p)
void	Gia_SweeperCondPush (Gia_Man_t *p, int ProbeId)
int	Gia_SweeperCondPop (Gia_Man_t *p)
Vec_Int_t *	Gia_SweeperCondVector (Gia_Man_t *p)
Gia_Man_t *	Gia_SweeperExtractUserLogic (Gia_Man_t *p, Vec_Int_t *vProbeIds, Vec_Ptr_t *vInNames, Vec_Ptr_t *vOutNames)
void	Gia_SweeperLogicDump (Gia_Man_t *p, Vec_Int_t *vProbeIds, int fDumpConds, char *pFileName)
Gia_Man_t *	Gia_SweeperCleanup (Gia_Man_t *p, char *pCommLime)
int	Gia_SweeperCheckEquiv (Gia_Man_t *pGia, int Probe1, int Probe2)
int	Gia_SweeperCondCheckUnsat (Gia_Man_t *pGia)
Vec_Int_t *	Gia_SweeperGraft (Gia_Man_t *pDst, Vec_Int_t *vProbes, Gia_Man_t *pSrc)
Gia_Man_t *	Gia_SweeperSweep (Gia_Man_t *p, Vec_Int_t *vProbeOuts, int nWords, int nConfs, int fVerify, int fVerbose)
int	Gia_SweeperFraig (Gia_Man_t *p, Vec_Int_t *vProbeIds, char *pCommLime, int nWords, int nConfs, int fVerify, int fVerbose)
int	Gia_SweeperRun (Gia_Man_t *p, Vec_Int_t *vProbeIds, char *pCommLime, int fVerbose)
Gia_Man_t *	Gia_SweeperFraigTest (Gia_Man_t *pInit, int nWords, int nConfs, int fVerbose)

Typedef Documentation

Swp_Man_t

typedef typedefABC_NAMESPACE_IMPL_START struct Swp_Man_t_ Swp_Man_t

DECLARATIONS ///.

CFile****************************************************************

FileName [giaSweeper.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Incremental SAT sweeper.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

giaSweeper.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 56 of file giaSweeper.c.

Function Documentation

Gia_SweeperCheckEquiv()

int Gia_SweeperCheckEquiv	(	Gia_Man_t *	pGia,
		int	Probe1,
		int	Probe2 )

Function*************************************************************

Synopsis [Runs equivalence test for probes.]

Description []

SideEffects []

SeeAlso []

Definition at line 789 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Gia_SweeperCleanup()

Gia_Man_t * Gia_SweeperCleanup	(	Gia_Man_t *	p,
		char *	pCommLime )

Function*************************************************************

Synopsis [Sweeper cleanup.]

Description [Returns new GIA with sweeper defined, which is the same as the original sweeper, with all the dangling logic removed and SAT solver restarted. The probe IDs are guaranteed to have the same logic functions as in the original manager.]

SideEffects [The input manager is deleted inside this procedure.]

SeeAlso []

Definition at line 461 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Gia_SweeperCollectValidProbeIds()

Vec_Int_t * Gia_SweeperCollectValidProbeIds

(

Gia_Man_t *

p

)

Function*************************************************************

Synopsis [This procedure returns indexes of all currently defined valid probes.]

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file giaSweeper.c.

{
    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;
}

Gia_SweeperCondCheckUnsat()

int Gia_SweeperCondCheckUnsat

(

Gia_Man_t *

pGia

)

Function*************************************************************

Synopsis [Returns 1 if the set of conditions is UNSAT (0 if SAT; -1 if undecided).]

Description []

SideEffects []

SeeAlso []

Definition at line 924 of file giaSweeper.c.

{
    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;
    }
}

Here is the call graph for this function:

Gia_SweeperCondPop()

int Gia_SweeperCondPop

(

Gia_Man_t *

p

)

Definition at line 324 of file giaSweeper.c.

{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    return Vec_IntPop( pSwp->vCondProbes );
}

Gia_SweeperCondPush()

void Gia_SweeperCondPush	(	Gia_Man_t *	p,
		int	ProbeId )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 319 of file giaSweeper.c.

{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    Vec_IntPush( pSwp->vCondProbes, ProbeId );
}

Here is the caller graph for this function:

Gia_SweeperCondVector()

Vec_Int_t * Gia_SweeperCondVector

(

Gia_Man_t *

p

)

Definition at line 329 of file giaSweeper.c.

{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    return pSwp->vCondProbes;
}

Here is the caller graph for this function:

Gia_SweeperExtractUserLogic()

Gia_Man_t * Gia_SweeperExtractUserLogic	(	Gia_Man_t *	p,
		Vec_Int_t *	vProbeIds,
		Vec_Ptr_t *	vInNames,
		Vec_Ptr_t *	vOutNames )

Definition at line 358 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_SweeperFraig()

int Gia_SweeperFraig	(	Gia_Man_t *	p,
		Vec_Int_t *	vProbeIds,
		char *	pCommLime,
		int	nWords,
		int	nConfs,
		int	fVerify,
		int	fVerbose )

Function*************************************************************

Synopsis [Procedure to perform conditional fraig sweeping on separate logic cones.]

Description [The procedure takes GIA with the sweeper defined. The sweeper is assumed to have some conditions currently pushed, which will be used as constraints for fraig sweeping. The second argument (vProbes) contains the array of probe IDs pointing to the user's logic cones to be SAT swept. Finally, the optional command line (pCommLine) is an ABC command line to be applied to the resulting GIA after SAT sweeping before it is grafted back into the original GIA manager. The return value is the status (success/failure) and the array of original probes possibly pointing to the new literals in the original GIA manager, corresponding to the user's logic cones after sweeping, synthesis and grafting.]

SideEffects []

SeeAlso []

Definition at line 1064 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Gia_SweeperFraigTest()

Gia_Man_t * Gia_SweeperFraigTest	(	Gia_Man_t *	pInit,
		int	nWords,
		int	nConfs,
		int	fVerbose )

Function*************************************************************

Synopsis [Sweeper sweeper test.]

Description []

SideEffects []

SeeAlso []

Definition at line 1152 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Gia_SweeperGetCex()

Vec_Int_t * Gia_SweeperGetCex

(

Gia_Man_t *

p

)

Definition at line 230 of file giaSweeper.c.

{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    assert( pSwp->vCexUser == NULL || Vec_IntSize(pSwp->vCexUser) == Gia_ManPiNum(p) );
    return pSwp->vCexUser;
}

Gia_SweeperGraft()

Vec_Int_t * Gia_SweeperGraft	(	Gia_Man_t *	pDst,
		Vec_Int_t *	vProbes,
		Gia_Man_t *	pSrc )

Function*************************************************************

Synopsis [Performs grafting from another manager.]

Description [Returns the array of resulting literals in the destination manager.]

SideEffects []

SeeAlso []

Definition at line 985 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_SweeperIsRunning()

int Gia_SweeperIsRunning

(

Gia_Man_t *

pGia

)

Definition at line 164 of file giaSweeper.c.

{
    return (pGia->pData != NULL);
}

Here is the caller graph for this function:

Gia_SweeperLogicDump()

void Gia_SweeperLogicDump	(	Gia_Man_t *	p,
		Vec_Int_t *	vProbeIds,
		int	fDumpConds,
		char *	pFileName )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 428 of file giaSweeper.c.

{
    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 );
}

Here is the call graph for this function:

Gia_SweeperMemUsage()

double Gia_SweeperMemUsage

(

Gia_Man_t *

pGia

)

Definition at line 168 of file giaSweeper.c.

{
    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;
}

Here is the caller graph for this function:

Gia_SweeperPrintStats()

void Gia_SweeperPrintStats

(

Gia_Man_t *

pGia

)

Definition at line 181 of file giaSweeper.c.

{
    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 );
}

Here is the call graph for this function:

Gia_SweeperProbeCreate()

int Gia_SweeperProbeCreate	(	Gia_Man_t *	p,
		int	iLit )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file giaSweeper.c.

{
    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;
}

Here is the caller graph for this function:

Gia_SweeperProbeDelete()

int Gia_SweeperProbeDelete	(	Gia_Man_t *	p,
		int	ProbeId )

Definition at line 258 of file giaSweeper.c.

{
    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;
}

Gia_SweeperProbeLit()

int Gia_SweeperProbeLit	(	Gia_Man_t *	p,
		int	ProbeId )

Definition at line 276 of file giaSweeper.c.

{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
    assert( iLit >= 0 );
    return iLit;
}

Here is the caller graph for this function:

Gia_SweeperProbeUpdate()

int Gia_SweeperProbeUpdate	(	Gia_Man_t *	p,
		int	ProbeId,
		int	iLitNew )

Definition at line 267 of file giaSweeper.c.

{
    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;
}

Here is the caller graph for this function:

Gia_SweeperRun()

int Gia_SweeperRun	(	Gia_Man_t *	p,
		Vec_Int_t *	vProbeIds,
		char *	pCommLime,
		int	fVerbose )

Function*************************************************************

Synopsis [Executes given command line for the logic defined by the probes.]

Description [ ]

SideEffects []

SeeAlso []

Definition at line 1106 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Gia_SweeperSetConflictLimit()

void Gia_SweeperSetConflictLimit	(	Gia_Man_t *	p,
		int	nConfMax )

Function*************************************************************

Synopsis [Setting resource limits.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file giaSweeper.c.

{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    pSwp->nConfMax = nConfMax;
}

Gia_SweeperSetRuntimeLimit()

void Gia_SweeperSetRuntimeLimit	(	Gia_Man_t *	p,
		int	nSeconds )

Definition at line 225 of file giaSweeper.c.

{
    Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
    pSwp->nTimeOut = nSeconds;
}

Gia_SweeperStart()

Gia_Man_t * Gia_SweeperStart

(

Gia_Man_t *

pGia

)

Definition at line 145 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_SweeperStop()

void Gia_SweeperStop

(

Gia_Man_t *

pGia

)

Definition at line 157 of file giaSweeper.c.

{
    pGia->fSweeper = 0;
    Swp_ManStop( pGia );
    Gia_ManHashStop( pGia );
//    Gia_ManStop( pGia );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_SweeperSweep()

Gia_Man_t * Gia_SweeperSweep	(	Gia_Man_t *	p,
		Vec_Int_t *	vProbeOuts,
		int	nWords,
		int	nConfs,
		int	fVerify,
		int	fVerbose )

Function*************************************************************

Synopsis [Performs conditional sweeping of the cone.]

Description [Returns the result as a new GIA manager with as many inputs as the original manager and as many outputs as there are logic cones.]

SideEffects []

SeeAlso []

Definition at line 1017 of file giaSweeper.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function: