mfsInt.h File Reference

#include "base/abc/abc.h"
#include "mfs.h"
#include "aig/aig/aig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satStore.h"
#include "bool/bdc/bdc.h"
#include "aig/gia/gia.h"

Go to the source code of this file.

Data Structures
struct	Mfs_Man_t_

Macros
#define	MFS_FANIN_MAX   12
	INCLUDES ///. More...

Typedefs
typedef struct Mfs_Man_t_	Mfs_Man_t

Functions
static float	Abc_MfsObjProb (Mfs_Man_t *p, Abc_Obj_t *pObj)
Vec_Ptr_t *	Abc_MfsComputeDivisors (Mfs_Man_t *p, Abc_Obj_t *pNode, int nLevDivMax)
	BASIC TYPES ///. More...
sat_solver *	Abc_MfsCreateSolverResub (Mfs_Man_t *p, int *pCands, int nCands, int fInvert)
Hop_Obj_t *	Abc_NtkMfsInterplate (Mfs_Man_t *p, int *pCands, int nCands)
int	Abc_NtkMfsInterplateEval (Mfs_Man_t *p, int *pCands, int nCands)
Mfs_Man_t *	Mfs_ManAlloc (Mfs_Par_t *pPars)
	DECLARATIONS ///. More...
void	Mfs_ManStop (Mfs_Man_t *p)
void	Mfs_ManClean (Mfs_Man_t *p)
void	Abc_NtkMfsPrintResubStats (Mfs_Man_t *p)
int	Abc_NtkMfsEdgeSwapEval (Mfs_Man_t *p, Abc_Obj_t *pNode)
int	Abc_NtkMfsEdgePower (Mfs_Man_t *p, Abc_Obj_t *pNode)
int	Abc_NtkMfsResubNode (Mfs_Man_t *p, Abc_Obj_t *pNode)
int	Abc_NtkMfsResubNode2 (Mfs_Man_t *p, Abc_Obj_t *pNode)
int	Abc_NtkMfsSolveSat (Mfs_Man_t *p, Abc_Obj_t *pNode)
int	Abc_NtkAddOneHotness (Mfs_Man_t *p)
Aig_Man_t *	Abc_NtkConstructAig (Mfs_Man_t *p, Abc_Obj_t *pNode)
double	Abc_NtkConstraintRatio (Mfs_Man_t *p, Abc_Obj_t *pNode)
Vec_Ptr_t *	Abc_MfsComputeRoots (Abc_Obj_t *pNode, int nWinTfoMax, int nFanoutLimit)
void	Abc_NtkMfsConstructGia (Mfs_Man_t *p)
void	Abc_NtkMfsDeconstructGia (Mfs_Man_t *p)
int	Abc_NtkMfsTryResubOnceGia (Mfs_Man_t *p, int *pCands, int nCands)

Macro Definition Documentation

#define MFS_FANIN_MAX   12

INCLUDES ///.

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

FileName [mfsInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The good old minimization with complete don't-cares.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

mfsInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///

Definition at line 47 of file mfsInt.h.

Typedef Documentation

typedef struct Mfs_Man_t_ Mfs_Man_t

Definition at line 49 of file mfsInt.h.

Function Documentation

Vec_Ptr_t* Abc_MfsComputeDivisors	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode,
		int	nLevDivMax
	)

BASIC TYPES ///.

MACRO DEFINITIONS ///FUNCTION DECLARATIONS ///

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

Synopsis [Computes divisors and add them to nodes in the window.]

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file mfsDiv.c.

{
    Vec_Ptr_t * vCone, * vDivs;
    Abc_Obj_t * pObj, * pFanout, * pFanin;
    int k, f, m;
    int nDivsPlus = 0, nTrueSupp;
    assert( p->vDivs == NULL );

    // mark the TFI with the current trav ID
    Abc_NtkIncrementTravId( pNode->pNtk );
    vCone = Abc_MfsWinMarkTfi( pNode );

    // count the number of PIs
    nTrueSupp = 0;
    Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, k )
        nTrueSupp += Abc_ObjIsCi(pObj);
//    printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m );

    // mark with the current trav ID those nodes that should not be divisors:
    // (1) the node and its TFO
    // (2) the MFFC of the node
    // (3) the node's fanins (these are treated as a special case)
    Abc_NtkIncrementTravId( pNode->pNtk );
    Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax );
//    Abc_MfsWinVisitMffc( pNode );
    Abc_ObjForEachFanin( pNode, pObj, k )
        Abc_NodeSetTravIdCurrent( pObj );

    // at this point the nodes are marked with two trav IDs:
    // nodes to be collected as divisors are marked with previous trav ID
    // nodes to be avoided as divisors are marked with current trav ID

    // start collecting the divisors
    vDivs = Vec_PtrAlloc( p->pPars->nWinMax );
    Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, k )
    {
        if ( !Abc_NodeIsTravIdPrevious(pObj) )
            continue;
        if ( (int)pObj->Level > nLevDivMax )
            continue;
        Vec_PtrPush( vDivs, pObj );
        if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
            break;
    }
    Vec_PtrFree( vCone );

    // explore the fanouts of already collected divisors
    if ( Vec_PtrSize(vDivs) < p->pPars->nWinMax )
    Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, k )
    {
        // consider fanouts of this node
        Abc_ObjForEachFanout( pObj, pFanout, f )
        {
            // stop if there are too many fanouts
            if ( p->pPars->nFanoutsMax && f > p->pPars->nFanoutsMax )
                break;
            // skip nodes that are already added
            if ( Abc_NodeIsTravIdPrevious(pFanout) )
                continue;
            // skip nodes in the TFO or in the MFFC of node
            if ( Abc_NodeIsTravIdCurrent(pFanout) )
                continue;
            // skip COs
            if ( !Abc_ObjIsNode(pFanout) ) 
                continue;
            // skip nodes with large level
            if ( (int)pFanout->Level > nLevDivMax )
                continue;
            // skip nodes whose fanins are not divisors  -- here we skip more than we need to skip!!! (revise later)  August 7, 2009
            Abc_ObjForEachFanin( pFanout, pFanin, m )
                if ( !Abc_NodeIsTravIdPrevious(pFanin) )
                    break;
            if ( m < Abc_ObjFaninNum(pFanout) )
                continue;
            // make sure this divisor in not among the nodes
//            Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pFanin, m )
//                assert( pFanout != pFanin );
            // add the node to the divisors
            Vec_PtrPush( vDivs, pFanout );
//            Vec_PtrPush( p->vNodes, pFanout );
            Vec_PtrPushUnique( p->vNodes, pFanout );
            Abc_NodeSetTravIdPrevious( pFanout );
            nDivsPlus++;
            if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
                break;
        }
        if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
            break;
    }
    p->nMaxDivs += (Vec_PtrSize(vDivs) >= p->pPars->nWinMax);

    // sort the divisors by level in the increasing order
    Vec_PtrSort( vDivs, (int (*)(void))Abc_NodeCompareLevelsIncrease );

    // add the fanins of the node
    Abc_ObjForEachFanin( pNode, pFanin, k )
        Vec_PtrPush( vDivs, pFanin );

/*
    printf( "Node level = %d.  ", Abc_ObjLevel(p->pNode) );
    Vec_PtrForEachEntryStart( Abc_Obj_t *, vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
        printf( "%d ", Abc_ObjLevel(pObj) );
    printf( "\n" );
*/
//printf( "%d ", p->nDivsPlus );
//    printf( "(%d+%d)(%d+%d+%d) ", Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), 
//        nTrueSupp, Vec_PtrSize(vDivs)-nTrueSupp-nDivsPlus, nDivsPlus );
    return vDivs;
}

Vec_Ptr_t* Abc_MfsComputeRoots	(	Abc_Obj_t *	pNode,
		int	nWinTfoMax,
		int	nFanoutLimit
	)

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

Synopsis [Recursively collects the root candidates.]

Description [Returns 1 if the only root is this node.]

SideEffects []

SeeAlso []

Definition at line 99 of file mfsWin.c.

{
    Vec_Ptr_t * vRoots;
    vRoots = Vec_PtrAlloc( 10 );
    Abc_NtkIncrementTravId( pNode->pNtk );
    Abc_MfsComputeRoots_rec( pNode, pNode->Level + nWinTfoMax, nFanoutLimit, vRoots );
    assert( Vec_PtrSize(vRoots) > 0 );
//    if ( Vec_PtrSize(vRoots) == 1 && Vec_PtrEntry(vRoots, 0) == pNode )
//        return 0;
    return vRoots;
}

sat_solver* Abc_MfsCreateSolverResub	(	Mfs_Man_t *	p,
		int *	pCands,
		int	nCands,
		int	fInvert
	)

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

Synopsis [Creates miter for checking resubsitution.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file mfsInter.c.

{
    sat_solver * pSat;
    Aig_Obj_t * pObjPo;
    int Lits[2], status, iVar, i, c;

    // get the literal for the output of F
    pObjPo = Aig_ManCo( p->pAigWin, Aig_ManCoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
    Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );

    // collect the outputs of the divisors
    Vec_IntClear( p->vProjVarsCnf );
    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vCos, pObjPo, i, Aig_ManCoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
    {
        assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
        Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] );
    }
    assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) );

    // start the solver
    pSat = sat_solver_new();
    sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) );
    if ( pCands )
        sat_solver_store_alloc( pSat );

    // load the first copy of the clauses
    for ( i = 0; i < p->pCnf->nClauses; i++ )
    {
        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
        {
            sat_solver_delete( pSat );
            return NULL;
        }
    }
    // add the clause for the first output of F
    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
    {
        sat_solver_delete( pSat );
        return NULL;
    }

    // add one-hotness constraints
    if ( p->pPars->fOneHotness )
    {
        p->pSat = pSat;
        if ( !Abc_NtkAddOneHotness( p ) )
            return NULL;
        p->pSat = NULL;
    }

    // bookmark the clauses of A
    if ( pCands )
        sat_solver_store_mark_clauses_a( pSat );

    // transform the literals
    for ( i = 0; i < p->pCnf->nLiterals; i++ )
        p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars;
    // load the second copy of the clauses
    for ( i = 0; i < p->pCnf->nClauses; i++ )
    {
        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
        {
            sat_solver_delete( pSat );
            return NULL;
        }
    }
    // add one-hotness constraints
    if ( p->pPars->fOneHotness )
    {
        p->pSat = pSat;
        if ( !Abc_NtkAddOneHotness( p ) )
            return NULL;
        p->pSat = NULL;
    }
    // transform the literals
    for ( i = 0; i < p->pCnf->nLiterals; i++ )
        p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
    // add the clause for the second output of F
    Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] );
    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
    {
        sat_solver_delete( pSat );
        return NULL;
    }

    if ( pCands )
    {
        // add relevant clauses for EXOR gates
        for ( c = 0; c < nCands; c++ )
        {
            // get the variable number of this divisor
            i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
            // get the corresponding SAT variable
            iVar = Vec_IntEntry( p->vProjVarsCnf, i );
            // add the corresponding EXOR gate
            if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
            {
                sat_solver_delete( pSat );
                return NULL;
            }
            // add the corresponding clause
            if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) )
            {
                sat_solver_delete( pSat );
                return NULL;
            }
        }
        // bookmark the roots
        sat_solver_store_mark_roots( pSat );
    }
    else
    {
        // add the clauses for the EXOR gates - and remember their outputs
        Vec_IntClear( p->vProjVarsSat );
        Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i )
        {
            if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
            {
                sat_solver_delete( pSat );
                return NULL;
            }
            Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i );
        }
        assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) );
        // simplify the solver
        status = sat_solver_simplify(pSat);
        if ( status == 0 )
        {
//            printf( "Abc_MfsCreateSolverResub(): SAT solver construction has failed. Skipping node.\n" );
            sat_solver_delete( pSat );
            return NULL;
        }
    }
    return pSat;
}

static float Abc_MfsObjProb ( Mfs_Man_t *  p, Abc_Obj_t *  pObj  )

inlinestatic

Definition at line 137 of file mfsInt.h.

{ return (p->vProbs && pObj->Id < Vec_IntSize(p->vProbs))? Abc_Int2Float(Vec_IntEntry(p->vProbs,pObj->Id)) : 0.0; }

int Abc_NtkAddOneHotness

(

Mfs_Man_t *

p

)

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

Synopsis [Adds one-hotness constraints for the window inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file mfsSat.c.

{
    Aig_Obj_t * pObj1, * pObj2;
    int i, k, Lits[2];
    for ( i = 0; i < Vec_PtrSize(p->pAigWin->vCis); i++ )
    for ( k = i+1; k < Vec_PtrSize(p->pAigWin->vCis); k++ )
    {
        pObj1 = Aig_ManCi( p->pAigWin, i );
        pObj2 = Aig_ManCi( p->pAigWin, k );
        Lits[0] = toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 );
        Lits[1] = toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 );
        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
        {
            sat_solver_delete( p->pSat );
            p->pSat = NULL;
            return 0;
        }
    }
    return 1;
}

double Abc_NtkConstraintRatio	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Compute the ratio of don't-cares.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file mfsStrash.c.

{
    int nSimWords = 256;
    Aig_Man_t * pMan;
    Fra_Sml_t * pSim;
    int Counter;
    pMan = Abc_NtkAigForConstraints( p, pNode );
    pSim = Fra_SmlSimulateComb( pMan, nSimWords, 0 );
    Counter = Fra_SmlNodeCountOnes( pSim, Aig_ManCo(pMan, 0) );
    Aig_ManStop( pMan );
    Fra_SmlStop( pSim );
    return 1.0 * Counter / (32 * nSimWords);
}

Aig_Man_t* Abc_NtkConstructAig	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Creates AIG for the window with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file mfsStrash.c.

{
    Aig_Man_t * pMan;
    Abc_Obj_t * pFanin;
    Aig_Obj_t * pObjAig, * pPi, * pPo;
    Vec_Int_t * vOuts;
    int i, k, iOut;
    // start the new manager
    pMan = Aig_ManStart( 1000 );
    // construct the root node's AIG cone
    pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
//    assert( Aig_ManConst1(pMan) == pObjAig );
    Aig_ObjCreateCo( pMan, pObjAig );
    if ( p->pCare )
    {
        // mark the care set
        Aig_ManIncrementTravId( p->pCare );
        Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
        {
            pPi = Aig_ManCi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
            Aig_ObjSetTravIdCurrent( p->pCare, pPi );
            pPi->pData = pFanin->pCopy;
        }
        // construct the constraints
        Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
        {
            vOuts = (Vec_Int_t *)Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
            Vec_IntForEachEntry( vOuts, iOut, k )
            {
                pPo = Aig_ManCo( p->pCare, iOut );
                if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
                    continue;
                Aig_ObjSetTravIdCurrent( p->pCare, pPo );
                if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
                    continue;
                pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
                if ( pObjAig == NULL )
                    continue;
                pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
                Aig_ObjCreateCo( pMan, pObjAig );
            }
        }
/*
        Aig_ManForEachCo( p->pCare, pPo, i )
        {
//            assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
                continue;
            pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
            if ( pObjAig == NULL )
                continue;
            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
            Aig_ObjCreateCo( pMan, pObjAig );
        }
*/
    }
    if ( p->pPars->fResub )
    {
        // construct the node
        pObjAig = (Aig_Obj_t *)pNode->pCopy;
        Aig_ObjCreateCo( pMan, pObjAig );
        // construct the divisors
        Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, i )
        {
            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
            Aig_ObjCreateCo( pMan, pObjAig );
        }
    }
    else
    {
        // construct the fanins
        Abc_ObjForEachFanin( pNode, pFanin, i )
        {
            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
            Aig_ObjCreateCo( pMan, pObjAig );
        }
    }
    Aig_ManCleanup( pMan );
    return pMan;
}

void Abc_NtkMfsConstructGia

(

Mfs_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file mfsGia.c.

{
    int nBTLimit = 500;
    // prepare AIG
    assert( p->pGia == NULL );
    p->pGia = Gia_ManCreateResubMiter( p->pAigWin );
    // prepare AIG
    Gia_ManCreateRefs( p->pGia );
    Gia_ManCleanMark0( p->pGia );
    Gia_ManCleanMark1( p->pGia );
    Gia_ManFillValue ( p->pGia ); // maps nodes into trail ids
    Gia_ManCleanPhase( p->pGia ); 
    // prepare solver
    p->pTas = Tas_ManAlloc( p->pGia, nBTLimit );
    p->vCex = Tas_ReadModel( p->pTas );
    p->vGiaLits = Vec_PtrAlloc( 100 );
}

void Abc_NtkMfsDeconstructGia

(

Mfs_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file mfsGia.c.

{
    assert( p->pGia != NULL );
    Gia_ManStop( p->pGia ); p->pGia = NULL;
    Tas_ManStop( p->pTas ); p->pTas = NULL;
    Vec_PtrFree( p->vGiaLits );
}

int Abc_NtkMfsEdgePower	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Evaluates the possibility of replacing given edge by another edge.]

Description []

SideEffects []

SeeAlso []

Definition at line 508 of file mfsResub.c.

{
    Abc_Obj_t * pFanin;
    int i;
    // try replacing area critical fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
        if ( Abc_MfsObjProb(p, pFanin) >= 0.35 )
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                return 1;
        } else if ( Abc_MfsObjProb(p, pFanin) >= 0.25 ) // sjang
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                return 1;
        }
        }
    return 0;
}

int Abc_NtkMfsEdgeSwapEval	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Evaluates the possibility of replacing given edge by another edge.]

Description []

SideEffects []

SeeAlso []

Definition at line 488 of file mfsResub.c.

{
    Abc_Obj_t * pFanin;
    int i;
    Abc_ObjForEachFanin( pNode, pFanin, i )
        Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
    return 0;
}

Hop_Obj_t* Abc_NtkMfsInterplate	(	Mfs_Man_t *	p,
		int *	pCands,
		int	nCands
	)

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

Synopsis [Performs interpolation.]

Description [Derives the new function of the node.]

SideEffects []

SeeAlso []

Definition at line 329 of file mfsInter.c.

{
    extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
    int fDumpFile = 0;
    char FileName[32];
    sat_solver * pSat;
    Sto_Man_t * pCnf = NULL;
    unsigned * puTruth;
    Kit_Graph_t * pGraph;
    Hop_Obj_t * pFunc;
    int nFanins, status;
    int c, i, * pGloVars;
//    abctime clk = Abc_Clock();
//    p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );

    // derive the SAT solver for interpolation
    pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 );

    // dump CNF file (remember to uncomment two-lit clases in clause_create_new() in 'satSolver.c')
    if ( fDumpFile )
    {
        static int Counter = 0;
        sprintf( FileName, "cnf\\pj1_if6_mfs%03d.cnf", Counter++ );
        Sat_SolverWriteDimacs( pSat, FileName, NULL, NULL, 1 );
    }

    // solve the problem
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( fDumpFile )
        printf( "File %s has UNSAT problem with %d conflicts.\n", FileName, (int)pSat->stats.conflicts );
    if ( status != l_False )
    {
        p->nTimeOuts++;
        return NULL;
    }
//printf( "%d\n", pSat->stats.conflicts );
//    ABC_PRT( "S", Abc_Clock() - clk );
    // get the learned clauses
    pCnf = (Sto_Man_t *)sat_solver_store_release( pSat );
    sat_solver_delete( pSat );

    // set the global variables
    pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
    for ( c = 0; c < nCands; c++ )
    {
        // get the variable number of this divisor
        i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
        // get the corresponding SAT variable
        pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
    }

    // derive the interpolant
    nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
    Sto_ManFree( pCnf );
    assert( nFanins == nCands );

    // transform interpolant into AIG
    pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
    pFunc = Kit_GraphToHop( (Hop_Man_t *)p->pNtk->pManFunc, pGraph );
    Kit_GraphFree( pGraph );
    return pFunc;
}

int Abc_NtkMfsInterplateEval	(	Mfs_Man_t *	p,
		int *	pCands,
		int	nCands
	)

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

Synopsis [Performs interpolation.]

Description [Derives the new function of the node.]

SideEffects []

SeeAlso []

Definition at line 285 of file mfsInter.c.

{
    unsigned * pTruth, uTruth0[2], uTruth1[2];
    int nCounter;
    pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 0 );
    if ( nCands == 6 )
    {
        uTruth1[0] = pTruth[0];
        uTruth1[1] = pTruth[1];
    }
    else
    {
        uTruth1[0] = pTruth[0];
        uTruth1[1] = pTruth[0];
    }
    pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 1 );
    if ( nCands == 6 )
    {
        uTruth0[0] = ~pTruth[0];
        uTruth0[1] = ~pTruth[1];
    }
    else
    {
        uTruth0[0] = ~pTruth[0];
        uTruth0[1] = ~pTruth[0];
    }
    nCounter  = Extra_WordCountOnes( uTruth0[0] ^ uTruth1[0] );
    nCounter += Extra_WordCountOnes( uTruth0[1] ^ uTruth1[1] );
//    printf( "%d ", nCounter );
    return nCounter;
}

void Abc_NtkMfsPrintResubStats

(

Mfs_Man_t *

p

)

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

Synopsis [Prints resub candidate stats.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 of file mfsResub.c.

{
    Abc_Obj_t * pFanin, * pNode;
    int i, k, nAreaCrits = 0, nAreaExpanse = 0;
    int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
    Abc_NtkForEachNode( p->pNtk, pNode, i )
        Abc_ObjForEachFanin( pNode, pFanin, k )
        {
            if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
            {
                nAreaCrits++;
                nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
            }
        }
//    printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", 
//        nAreaCrits, nAreaExpanse );
}

int Abc_NtkMfsResubNode	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Performs resubstitution for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 539 of file mfsResub.c.

{
    Abc_Obj_t * pFanin;
    int i;
    // try replacing area critical fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                return 1;
        }
    // try removing redundant edges
    if ( !p->pPars->fArea )
    {
        Abc_ObjForEachFanin( pNode, pFanin, i )
            if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
            {
                if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                    return 1;
            }
    }
    if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
        return 0;
/*
    // try replacing area critical fanins while adding two new fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
        {
            if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
                return 1;
        }
*/
    return 0;
}

int Abc_NtkMfsResubNode2	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Performs resubstitution for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 585 of file mfsResub.c.

{
    Abc_Obj_t * pFanin, * pFanin2;
    int i, k;
/*
    Abc_ObjForEachFanin( pNode, pFanin, i )
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                return 1;
        }
*/
    if ( Abc_ObjFaninNum(pNode) < 2 )
        return 0;
    // try replacing one area critical fanin and one other fanin while adding two new fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
        {
            // consider second fanin to remove at the same time
            Abc_ObjForEachFanin( pNode, pFanin2, k )
            {
                if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
                    return 1;
            }
        }
    }
    return 0;
}

int Abc_NtkMfsSolveSat	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Enumerates through the SAT assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file mfsSat.c.

{
    Aig_Obj_t * pObjPo;
    int RetValue, i;
    // collect projection variables
    Vec_IntClear( p->vProjVarsSat );
    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vCos, pObjPo, i, Aig_ManCoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
    {
        assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
        Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] );
    }

    // prepare the truth table of care set
    p->nFanins = Vec_IntSize( p->vProjVarsSat );
    p->nWords = Abc_TruthWordNum( p->nFanins );
    memset( p->uCare, 0, sizeof(unsigned) * p->nWords );

    // iterate through the SAT assignments
    p->nCares = 0;
    p->nTotConfLim = p->pPars->nBTLimit;
    while ( (RetValue = Abc_NtkMfsSolveSat_iter(p)) == 1 );
    if ( RetValue == -1 )
        return 0;

    // write statistics
    p->nMintsCare  += p->nCares;
    p->nMintsTotal += (1<<p->nFanins);

    if ( p->pPars->fVeryVerbose )
    {
        printf( "Node %4d : Care = %2d. Total = %2d.  ", pNode->Id, p->nCares, (1<<p->nFanins) );
        Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
        printf( "\n" );
    }

    // map the care 
    if ( p->nFanins > 4 )
        return 1;
    if ( p->nFanins == 4 )
        p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
    if ( p->nFanins == 3 )
        p->uCare[0] = p->uCare[0] | (p->uCare[0] << 8) | (p->uCare[0] << 16) | (p->uCare[0] << 24);
    if ( p->nFanins == 2 )
        p->uCare[0] = p->uCare[0] | (p->uCare[0] <<  4) | (p->uCare[0] <<  8) | (p->uCare[0] << 12) |
              (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
    assert( p->nFanins != 1 );
    return 1;
}

int Abc_NtkMfsTryResubOnceGia	(	Mfs_Man_t *	p,
		int *	pCands,
		int	nCands
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file mfsGia.c.

{
    int fVeryVerbose = 0;
    int fUseGia = 1;
    unsigned * pData;
    int i, iVar, status, iOut;
    clock_t clk = clock();
    p->nSatCalls++;
//    return -1;
    assert( p->pGia != NULL );
    assert( p->pTas != NULL );
    // convert to literals
    Vec_PtrClear( p->vGiaLits );
    // create the first four literals
    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 0)) );
    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 1)) );
    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 2)) );
    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 3)) );
    for ( i = 0; i < nCands; i++ )
    {
        // get the output number
        iOut = Gia_Lit2Var(pCands[i]) - 2 * p->pCnf->nVars;
        // write the literal
        Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 4 + iOut)) );
    }
    // perform SAT solving
    status = Tas_ManSolveArray( p->pTas, p->vGiaLits );
    if ( status == -1 )
    {
        p->nTimeOuts++;
        if ( fVeryVerbose )
        printf( "t" );
//        p->nSatUndec++;
//        p->nConfUndec += p->Pars.nBTThis;
//        Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
//        p->timeSatUndec += clock() - clk;
    }
    else if ( status == 1 )
    {
        if ( fVeryVerbose )
        printf( "u" );
//        p->nSatUnsat++;
//        p->nConfUnsat += p->Pars.nBTThis;
//        p->timeSatUnsat += clock() - clk;
    }
    else
    {
        p->nSatCexes++;
        if ( fVeryVerbose )
        printf( "s" );
//        p->nSatSat++;
//        p->nConfSat += p->Pars.nBTThis;
//        Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
//        Cec_ManSatAddToStore( vCexStore, vCex, i );
//        p->timeSatSat += clock() - clk;

        // resimulate the counter-example
        Abc_NtkMfsResimulate( p->pGia, Tas_ReadModel(p->pTas) );
   
        if ( fUseGia )
        {
/*
            int Val0 = Gia_ManPo(p->pGia, 0)->fMark1;
            int Val1 = Gia_ManPo(p->pGia, 1)->fMark1;
            int Val2 = Gia_ManPo(p->pGia, 2)->fMark1;
            int Val3 = Gia_ManPo(p->pGia, 3)->fMark1;
            assert( Val0 == 1 );
            assert( Val1 == 1 );
            assert( Val2 == 1 );
            assert( Val3 == 1 );
*/
            // store the counter-example
            Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
            {
                pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
                iOut = iVar - 2 * p->pCnf->nVars;
//                if ( !Gia_ManPo( p->pGia, 4 + iOut )->fMark1 ) // remove 0s!!!
                if ( Gia_ManPo( p->pGia, 4 + iOut )->fMark1 ) // remove 0s!!!  - rememeber complemented attribute
                {
                    assert( Aig_InfoHasBit(pData, p->nCexes) );
                    Aig_InfoXorBit( pData, p->nCexes );
                }
            }
            p->nCexes++;
        }

    }
    return status;
}

Mfs_Man_t* Mfs_ManAlloc

(

Mfs_Par_t *

pPars

)

DECLARATIONS ///.

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

FileName [mfsMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The good old minimization with complete don't-cares.]

Synopsis [Procedures working with the manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file mfsMan.c.

{
    Mfs_Man_t * p;
    // start the manager
    p = ABC_ALLOC( Mfs_Man_t, 1 );
    memset( p, 0, sizeof(Mfs_Man_t) );
    p->pPars     = pPars;
    p->vProjVarsCnf = Vec_IntAlloc( 100 );
    p->vProjVarsSat = Vec_IntAlloc( 100 );
    p->vDivLits  = Vec_IntAlloc( 100 );
    p->nDivWords = Abc_BitWordNum(p->pPars->nWinMax + MFS_FANIN_MAX);
    p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nWinMax + MFS_FANIN_MAX + 1, p->nDivWords );
    p->pMan      = Int_ManAlloc();
    p->vMem      = Vec_IntAlloc( 0 );
    p->vLevels   = Vec_VecStart( 32 );
    p->vMfsFanins= Vec_PtrAlloc( 32 );
    return p;
}

void Mfs_ManClean

(

Mfs_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file mfsMan.c.

{
    if ( p->pAigWin )
        Aig_ManStop( p->pAigWin );
    if ( p->pCnf )
        Cnf_DataFree( p->pCnf );
    if ( p->pSat )
        sat_solver_delete( p->pSat );
    if ( p->vRoots )
        Vec_PtrFree( p->vRoots );
    if ( p->vSupp )
        Vec_PtrFree( p->vSupp );
    if ( p->vNodes )
        Vec_PtrFree( p->vNodes );
    if ( p->vDivs )
        Vec_PtrFree( p->vDivs );
    p->pAigWin = NULL;
    p->pCnf    = NULL;
    p->pSat    = NULL;
    p->vRoots  = NULL;
    p->vSupp   = NULL;
    p->vNodes  = NULL;
    p->vDivs   = NULL;
}

void Mfs_ManStop

(

Mfs_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file mfsMan.c.

{
    if ( p->pPars->fVerbose )
        Mfs_ManPrint( p );
    if ( p->vTruth )
        Vec_IntFree( p->vTruth );
    if ( p->pManDec )
        Bdc_ManFree( p->pManDec );
    if ( p->pCare )
        Aig_ManStop( p->pCare );
    if ( p->vSuppsInv )
        Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv );
    if ( p->vProbs )
        Vec_IntFree( p->vProbs );
    Mfs_ManClean( p );
    Int_ManFree( p->pMan );
    Vec_IntFree( p->vMem );
    Vec_VecFree( p->vLevels );
    Vec_PtrFree( p->vMfsFanins );
    Vec_IntFree( p->vProjVarsCnf );
    Vec_IntFree( p->vProjVarsSat );
    Vec_IntFree( p->vDivLits );
    Vec_PtrFree( p->vDivCexes );
    ABC_FREE( p );
}