aigPartSat.c File Reference

#include "aig.h"
#include "sat/bsat/satSolver.h"
#include "sat/cnf/cnf.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Aig_Man_t *	Dar_ManRwsat (Aig_Man_t *pAig, int fBalance, int fVerbose)
	DECLARATIONS ///. More...
Vec_Int_t *	Aig_ManPartitionMonolithic (Aig_Man_t *p)
	FUNCTION DEFINITIONS ///. More...
Vec_Int_t *	Aig_ManPartitionLevelized (Aig_Man_t *p, int nPartSize)
Vec_Int_t *	Aig_ManPartitionDfs (Aig_Man_t *p, int nPartSize, int fPreorder)
void	Aig_ManPartSplitOne_rec (Aig_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Int_t *vPio2Id)
Aig_Man_t *	Aig_ManPartSplitOne (Aig_Man_t *p, Vec_Ptr_t *vNodes, Vec_Int_t **pvPio2Id)
Vec_Ptr_t *	Aig_ManPartSplit (Aig_Man_t *p, Vec_Int_t *vNode2Part, Vec_Ptr_t **pvPio2Id, Vec_Ptr_t **pvPart2Pos)
void	Aig_ManPartResetNodePolarity (Aig_Man_t *pPart)
void	Aig_ManPartSetNodePolarity (Aig_Man_t *p, Aig_Man_t *pPart, Vec_Int_t *vPio2Id)
void	Aig_ManDeriveCounterExample (Aig_Man_t *p, Vec_Int_t *vNode2Var, sat_solver *pSat)
int	Aig_ManAddNewCnfToSolver (sat_solver *pSat, Aig_Man_t *pAig, Vec_Int_t *vNode2Var, Vec_Int_t *vPioIds, Vec_Ptr_t *vPartPos, int fAlignPol)
int	Aig_ManPartitionedSat (Aig_Man_t *p, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose)

Function Documentation

int Aig_ManAddNewCnfToSolver	(	sat_solver *	pSat,
		Aig_Man_t *	pAig,
		Vec_Int_t *	vNode2Var,
		Vec_Int_t *	vPioIds,
		Vec_Ptr_t *	vPartPos,
		int	fAlignPol
	)

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

Synopsis [Derives CNF for the partition (pAig) and adds it to solver.]

Description [Array vPio2Id contains mapping of the PI/PO terminal of pAig into the IDs of the corresponding original nodes. Array vNode2Var contains mapping of the original nodes into their SAT variable numbers.]

SideEffects []

SeeAlso []

Definition at line 378 of file aigPartSat.c.

{
    Cnf_Dat_t * pCnf;
    Aig_Obj_t * pObj;
    int * pBeg, * pEnd;
    int i, Lits[2], iSatVarOld, iNodeIdOld;
    // derive CNF and express it using new SAT variables
    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
    Cnf_DataTranformPolarity( pCnf, 1 );
    Cnf_DataLift( pCnf, sat_solver_nvars(pSat) );
    // create new variables in the SAT solver
    sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + pCnf->nVars );
    // add clauses for this CNF
    Cnf_CnfForClause( pCnf, pBeg, pEnd, i )
        if ( !sat_solver_addclause( pSat, pBeg, pEnd ) )
        {
            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
            return 1;
        }
    // derive the connector clauses
    Aig_ManForEachCi( pAig, pObj, i )
    {
        iNodeIdOld = Vec_IntEntry( vPioIds, i );
        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
        if ( iSatVarOld == 0 ) // iNodeIdOld in the original AIG has no SAT var
        { 
            // map the corresponding original AIG node into this SAT var
            Vec_IntWriteEntry( vNode2Var, iNodeIdOld, pCnf->pVarNums[Aig_ObjId(pObj)] );
            continue;
        }
        // add connector clauses 
        Lits[0] = toLitCond( iSatVarOld, 0 );
        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
            assert( 0 );
        Lits[0] = toLitCond( iSatVarOld, 1 );
        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
            assert( 0 );
    }
    // derive the connector clauses
    Aig_ManForEachCo( pAig, pObj, i )
    {
        iNodeIdOld = Vec_IntEntry( vPioIds, Aig_ManCiNum(pAig) + i );
        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
        if ( iSatVarOld == 0 ) // iNodeIdOld in the original AIG has no SAT var
        { 
            // map the corresponding original AIG node into this SAT var
            Vec_IntWriteEntry( vNode2Var, iNodeIdOld, pCnf->pVarNums[Aig_ObjId(pObj)] );
            continue;
        }
        // add connector clauses 
        Lits[0] = toLitCond( iSatVarOld, 0 );
        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
            assert( 0 );
        Lits[0] = toLitCond( iSatVarOld, 1 );
        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
            assert( 0 );
    }
    // transfer the ID of constant 1 node
    if ( Vec_IntEntry( vNode2Var, 0 ) == 0 )
        Vec_IntWriteEntry( vNode2Var, 0, pCnf->pVarNums[0] );
    // remove the CNF
    Cnf_DataFree( pCnf );
    // constrain the solver with the literals corresponding to the original POs
    Vec_PtrForEachEntry( Aig_Obj_t *, vPartPos, pObj, i )
    {
        iNodeIdOld = Aig_ObjFaninId0( pObj );
        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
        assert( iSatVarOld != 0 );
        // assert the original PO to be 1
        Lits[0] = toLitCond( iSatVarOld, Aig_ObjFaninC0(pObj) );
        // correct the polarity if polarity alignment is enabled
        if ( fAlignPol && Aig_ObjFanin0(pObj)->fPhase ) 
            Lits[0] = lit_neg( Lits[0] );
        if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
        {
            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
            return 1;
        }
    }
    // constrain some the primary inputs to constant values
    Aig_ManForEachCi( pAig, pObj, i )
    {
        if ( !pObj->fMarkA && !pObj->fMarkB )
            continue;
        iNodeIdOld = Vec_IntEntry( vPioIds, i );
        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
        Lits[0] = toLitCond( iSatVarOld, pObj->fMarkA );
        if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
        {
            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
            return 1;
        }
        pObj->fMarkA = pObj->fMarkB = 0;
    }
    return 0;
}

void Aig_ManDeriveCounterExample	(	Aig_Man_t *	p,
		Vec_Int_t *	vNode2Var,
		sat_solver *	pSat
	)

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

Synopsis [Sets polarity according to the original nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file aigPartSat.c.

{ 
    Vec_Int_t * vPisIds;
    Aig_Obj_t * pObj;
    int i;
    // collect IDs of PI variables
    // (fanoutless PIs have SAT var 0, which is an unused in the SAT solver -> has value 0)
    vPisIds = Vec_IntAlloc( Aig_ManCiNum(p) );
    Aig_ManForEachCi( p, pObj, i )
        Vec_IntPush( vPisIds, Vec_IntEntry(vNode2Var, Aig_ObjId(pObj)) );
    // derive the SAT assignment
    p->pData = Sat_SolverGetModel( pSat, vPisIds->pArray, vPisIds->nSize );
    Vec_IntFree( vPisIds );
}

Vec_Int_t* Aig_ManPartitionDfs	(	Aig_Man_t *	p,
		int	nPartSize,
		int	fPreorder
	)

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

Synopsis [Partitioning using DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 103 of file aigPartSat.c.

{
    Vec_Int_t * vId2Part; 
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) );
    if ( fPreorder )
    {
        vNodes = Aig_ManDfsPreorder( p, 1 );
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
            Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
    }
    else
    {
        vNodes = Aig_ManDfs( p, 1 );
        Vec_PtrForEachEntryReverse( Aig_Obj_t *, vNodes, pObj, i )
            Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
    }
    Vec_PtrFree( vNodes );
    return vId2Part;
}

int Aig_ManPartitionedSat	(	Aig_Man_t *	p,
		int	nAlgo,
		int	nPartSize,
		int	nConfPart,
		int	nConfTotal,
		int	fAlignPol,
		int	fSynthesize,
		int	fVerbose
	)

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

Synopsis [Performs partitioned SAT solving.]

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file aigPartSat.c.

{
    sat_solver * pSat;
    Vec_Ptr_t * vAigs;
    Vec_Vec_t * vPio2Id, * vPart2Pos;
    Aig_Man_t * pAig, * pTemp;
    Vec_Int_t * vNode2Part, * vNode2Var;
    int nConfRemaining = nConfTotal, nNodes = 0;
    int i, status, RetValue = -1;
    abctime clk;

    // perform partitioning according to the selected algorithm
    clk = Abc_Clock();
    switch ( nAlgo )
    {
    case 0: 
        vNode2Part = Aig_ManPartitionMonolithic( p );
        break;
    case 1: 
        vNode2Part = Aig_ManPartitionLevelized( p, nPartSize );
        break;
    case 2: 
        vNode2Part = Aig_ManPartitionDfs( p, nPartSize, 0 );
        break;
    case 3: 
        vNode2Part = Aig_ManPartitionDfs( p, nPartSize, 1 );
        break;
    default:
        printf( "Unknown partitioning algorithm.\n" );
        return -1;
    }

    if ( fVerbose )
    {
    printf( "Partitioning derived %d partitions. ", Vec_IntFindMax(vNode2Part) + 1 );
    ABC_PRT( "Time", Abc_Clock() - clk );
    }

    // split the original AIG into partition AIGs (vAigs)
    // also, derives mapping of PIs/POs of partition AIGs into original nodes
    // also, derives mapping of POs of the original AIG into partitions
    vAigs = Aig_ManPartSplit( p, vNode2Part, (Vec_Ptr_t **)&vPio2Id, (Vec_Ptr_t **)&vPart2Pos );
    Vec_IntFree( vNode2Part );

    if ( fVerbose )
    {
    printf( "Partions were transformed into AIGs. " );
    ABC_PRT( "Time", Abc_Clock() - clk );
    }

    // synthesize partitions
    if ( fSynthesize )
    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
    {
        pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
        Vec_PtrWriteEntry( vAigs, i, pAig );
        Aig_ManStop( pTemp );
    }

    // start the SAT solver
    pSat = sat_solver_new();
//    pSat->verbosity = fVerbose;
    // start mapping of the original AIG IDs into their SAT variable numbers
    vNode2Var = Vec_IntStart( Aig_ManObjNumMax(p) );

    // add partitions, one at a time, and run the SAT solver 
    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
    {
clk = Abc_Clock();
        // transform polarity of the AIG
        if ( fAlignPol )
            Aig_ManPartSetNodePolarity( p, pAig, Vec_VecEntryInt(vPio2Id,i) );
        else
            Aig_ManPartResetNodePolarity( pAig );
        // add CNF of this partition to the SAT solver
        if ( Aig_ManAddNewCnfToSolver( pSat, pAig, vNode2Var, 
            Vec_VecEntryInt(vPio2Id,i), Vec_VecEntry(vPart2Pos,i), fAlignPol ) )
        {
            RetValue = 1;
            break;
        }
        // call the SAT solver
        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfRemaining, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( fVerbose )
        {
            printf( "%4d : Aig = %6d. Vs = %7d. RootCs = %7d. LearnCs = %6d. ",
                i, nNodes += Aig_ManNodeNum(pAig), sat_solver_nvars(pSat), 
                (int)pSat->stats.clauses, (int)pSat->stats.learnts );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
        // analize the result
        if ( status == l_False )
        {
            RetValue = 1;
            break;
        }
        else if ( status == l_True )
            RetValue = 0;
        else
            RetValue = -1;
        nConfRemaining -= pSat->stats.conflicts;
        if ( nConfRemaining <= 0 )
        {
            printf( "Exceeded the limit on the total number of conflicts (%d).\n", nConfTotal );
            break;
        }
    }
    if ( RetValue == 0 )
        Aig_ManDeriveCounterExample( p, vNode2Var, pSat );
    // cleanup
    sat_solver_delete( pSat );
    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
        Aig_ManStop( pTemp );
    Vec_PtrFree( vAigs );
    Vec_VecFree( vPio2Id );
    Vec_VecFree( vPart2Pos );
    Vec_IntFree( vNode2Var );
    return RetValue;
}

Vec_Int_t* Aig_ManPartitionLevelized	(	Aig_Man_t *	p,
		int	nPartSize
	)

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

Synopsis [Partitioning using levelized order.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file aigPartSat.c.

{
    Vec_Int_t * vId2Part;
    Vec_Vec_t * vNodes;
    Aig_Obj_t * pObj;
    int i, k, Counter = 0;
    vNodes = Aig_ManLevelize( p );
    vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) );
    Vec_VecForEachEntryReverseReverse( Aig_Obj_t *, vNodes, pObj, i, k )
        Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
    Vec_VecFree( vNodes );
    return vId2Part;
}

Vec_Int_t* Aig_ManPartitionMonolithic

(

Aig_Man_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [No partitioning.]

Description [The partitioner ]

SideEffects []

SeeAlso []

Definition at line 60 of file aigPartSat.c.

{
    Vec_Int_t * vId2Part;
    vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) );
    return vId2Part;
}

void Aig_ManPartResetNodePolarity

(

Aig_Man_t *

pPart

)

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

Synopsis [Resets node polarity to unbias the polarity of CNF variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 300 of file aigPartSat.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( pPart, pObj, i )
        pObj->fPhase = 0;
}

void Aig_ManPartSetNodePolarity	(	Aig_Man_t *	p,
		Aig_Man_t *	pPart,
		Vec_Int_t *	vPio2Id
	)

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

Synopsis [Sets polarity according to the original nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 319 of file aigPartSat.c.

{
    Aig_Obj_t * pObj, * pObjInit;
    int i;
    Aig_ManConst1(pPart)->fPhase = 1;
    Aig_ManForEachCi( pPart, pObj, i )
    {
        pObjInit = Aig_ManObj( p, Vec_IntEntry(vPio2Id, i) );
        pObj->fPhase = pObjInit->fPhase;
    }
    Aig_ManForEachNode( pPart, pObj, i )
        pObj->fPhase = (Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj));
    Aig_ManForEachCo( pPart, pObj, i )
    {
        pObjInit = Aig_ManObj( p, Vec_IntEntry(vPio2Id, Aig_ManCiNum(pPart) + i) );
        pObj->fPhase = (Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj));
        assert( pObj->fPhase == pObjInit->fPhase );
    }
}

Vec_Ptr_t* Aig_ManPartSplit	(	Aig_Man_t *	p,
		Vec_Int_t *	vNode2Part,
		Vec_Ptr_t **	pvPio2Id,
		Vec_Ptr_t **	pvPart2Pos
	)

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

Synopsis [Derives AIGs for each partition.]

Description [The first argument is a original AIG. The second argument is the array mapping each AND-node's ID into the 0-based number of its partition. The last argument is the array of arrays (one for each new AIG) mapping the index of each terminal in the new AIG (the index of each terminal is derived by ordering PIs followed by POs in their natural order) into the ID of the corresponding node in the original AIG. The returned value is the array of AIGs representing the partitions.]

SideEffects []

SeeAlso []

Definition at line 225 of file aigPartSat.c.

{
    Vec_Vec_t * vGroups, * vPart2Pos;
    Vec_Ptr_t * vAigs, * vPio2Id, * vNodes;
    Vec_Int_t * vPio2IdOne;
    Aig_Man_t * pAig;
    Aig_Obj_t * pObj, * pDriver;
    int i, nodePart, nParts;
    vAigs = Vec_PtrAlloc( 100 );
    vPio2Id = Vec_PtrAlloc( 100 );
    // put all nodes into levels according to their partition
    nParts = Vec_IntFindMax(vNode2Part) + 1;
    assert( nParts > 0 );
    vGroups = Vec_VecAlloc( nParts );
    Vec_IntForEachEntry( vNode2Part, nodePart, i )
    {
        pObj = Aig_ManObj( p, i );
        if ( Aig_ObjIsNode(pObj) )
            Vec_VecPush( vGroups, nodePart, pObj );
    }

    // label PIs that should be restricted to some values
    Aig_ManForEachCo( p, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        if ( Aig_ObjIsCi(pDriver) )
        {
            if ( Aig_ObjFaninC0(pObj) )
                pDriver->fMarkA = 1; // const0 PI
            else
                pDriver->fMarkB = 1; // const1 PI
        }
    }

    // create partitions
    Vec_VecForEachLevel( vGroups, vNodes, i )
    {
        if ( Vec_PtrSize(vNodes) == 0 )
        {
            printf( "Aig_ManPartSplit(): Skipping partition # %d without nodes (warning).\n", i );
            continue;
        }
        pAig = Aig_ManPartSplitOne( p, vNodes, &vPio2IdOne );
        Vec_PtrPush( vPio2Id, vPio2IdOne );
        Vec_PtrPush( vAigs, pAig );
    }
    Vec_VecFree( vGroups );

    // divide POs according to their partitions
    vPart2Pos = Vec_VecStart( Vec_PtrSize(vAigs) );
    Aig_ManForEachCo( p, pObj, i )
    {
        pDriver = Aig_ObjFanin0(pObj);
        if ( Aig_ObjIsCi(pDriver) )
            pDriver->fMarkA = pDriver->fMarkB = 0;
        else
            Vec_VecPush( vPart2Pos, Vec_IntEntry(vNode2Part, Aig_ObjFaninId0(pObj)), pObj );
    }

    *pvPio2Id = vPio2Id;
    *pvPart2Pos = (Vec_Ptr_t *)vPart2Pos;
    return vAigs;
}

Aig_Man_t* Aig_ManPartSplitOne	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vNodes,
		Vec_Int_t **	pvPio2Id
	)

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

Synopsis [Carves out one partition of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file aigPartSat.c.

{
    Vec_Int_t * vPio2Id;
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    // mark these nodes
    Aig_ManIncrementTravId( p );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        Aig_ObjSetTravIdCurrent( p, pObj );
        pObj->pData = NULL;
    }
    // add these nodes in a DFS order
    pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
    vPio2Id = Vec_IntAlloc( 100 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        Aig_ManPartSplitOne_rec( pNew, p, pObj, vPio2Id );
    // add the POs
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        if ( Aig_ObjRefs((Aig_Obj_t *)pObj->pData) != Aig_ObjRefs(pObj) )
        {
            assert( Aig_ObjRefs((Aig_Obj_t *)pObj->pData) < Aig_ObjRefs(pObj) );
            Aig_ObjCreateCo( pNew, (Aig_Obj_t *)pObj->pData );
            Vec_IntPush( vPio2Id, Aig_ObjId(pObj) );
        }
    assert( Aig_ManNodeNum(pNew) == Vec_PtrSize(vNodes) );
    *pvPio2Id = vPio2Id;
    return pNew;
}

void Aig_ManPartSplitOne_rec	(	Aig_Man_t *	pNew,
		Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Int_t *	vPio2Id
	)

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

Synopsis [Recursively constructs the partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file aigPartSat.c.

{
    if ( !Aig_ObjIsTravIdCurrent( p, pObj ) )
    { // new PI
        Aig_ObjSetTravIdCurrent( p, pObj );
/*
        if ( pObj->fMarkA ) // const0
            pObj->pData = Aig_ManConst0( pNew );
        else if ( pObj->fMarkB ) // const1
            pObj->pData = Aig_ManConst1( pNew );
        else
*/
        {
            pObj->pData = Aig_ObjCreateCi( pNew );
            if ( pObj->fMarkA ) // const0
                ((Aig_Obj_t *)pObj->pData)->fMarkA = 1;
            else if ( pObj->fMarkB ) // const1
                ((Aig_Obj_t *)pObj->pData)->fMarkB = 1;
            Vec_IntPush( vPio2Id, Aig_ObjId(pObj) );
        }
        return;
    }
    if ( pObj->pData ) 
        return;
    Aig_ManPartSplitOne_rec( pNew, p, Aig_ObjFanin0(pObj), vPio2Id );
    Aig_ManPartSplitOne_rec( pNew, p, Aig_ObjFanin1(pObj), vPio2Id );
    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}

ABC_NAMESPACE_IMPL_START Aig_Man_t* Dar_ManRwsat	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fVerbose
	)

DECLARATIONS ///.

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

FileName [aigPartSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Partitioning for SAT solving.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

aigPartSat.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

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

Synopsis [Reproduces script "rwsat".]

Description []

SideEffects [This procedure does not tighten level during restructuring.]

SeeAlso []

Definition at line 71 of file darScript.c.

{
    Aig_Man_t * pTemp;
    abctime Time = pAig->Time2Quit;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = 0;
    pParsRef->fUpdateLevel = 0;

    pParsRwr->fVerbose = fVerbose;
    pParsRef->fVerbose = fVerbose;
//printf( "1" );
    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );

//printf( "2" );
    // balance
    if ( fBalance )
    {
    pAig->Time2Quit = Time;
    pAig = Dar_ManBalance( pTemp = pAig, 0 );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
    }
   
//Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
//printf( "3" );
    // rewrite
    pAig->Time2Quit = Time;
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }

//printf( "4" );
    // refactor
    pAig->Time2Quit = Time;
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }

//printf( "5" );
    // balance
    if ( fBalance )
    {
    pAig->Time2Quit = Time;
    pAig = Dar_ManBalance( pTemp = pAig, 0 );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
    }

//printf( "6" );
    // rewrite
    pAig->Time2Quit = Time;
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }

//printf( "7" );
    return pAig;
}