sfmInt.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "sat/bsat/satSolver.h"
#include "sfm.h"

Go to the source code of this file.

Data Structures
struct	Sfm_Ntk_t_
	BASIC TYPES ///. More...

Macros
#define	SFM_FANIN_MAX   6
	INCLUDES ///. More...
#define	SFM_SAT_UNDEC   0x1234567812345678
#define	SFM_SAT_SAT   0x8765432187654321
#define	Sfm_NtkForEachPi(p, i)   for ( i = 0; i < p->nPis; i++ )
	MACRO DEFINITIONS ///. More...
#define	Sfm_NtkForEachPo(p, i)   for ( i = p->nObjs - p->nPos; i < p->nObjs; i++ )
#define	Sfm_NtkForEachNode(p, i)   for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
#define	Sfm_NtkForEachNodeReverse(p, i)   for ( i = p->nObjs - p->nPos - 1; i >= p->nPis; i-- )
#define	Sfm_ObjForEachFanin(p, Node, Fan, i)   for ( i = 0; i < Sfm_ObjFaninNum(p, Node) && ((Fan = Sfm_ObjFanin(p, Node, i)), 1); i++ )
#define	Sfm_ObjForEachFanout(p, Node, Fan, i)   for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )

Functions
static int	Sfm_NtkPiNum (Sfm_Ntk_t *p)
static int	Sfm_NtkPoNum (Sfm_Ntk_t *p)
static int	Sfm_NtkNodeNum (Sfm_Ntk_t *p)
static int	Sfm_ObjIsPi (Sfm_Ntk_t *p, int i)
static int	Sfm_ObjIsPo (Sfm_Ntk_t *p, int i)
static int	Sfm_ObjIsNode (Sfm_Ntk_t *p, int i)
static int	Sfm_ObjIsFixed (Sfm_Ntk_t *p, int i)
static int	Sfm_ObjAddsLevelArray (Vec_Str_t *p, int i)
static int	Sfm_ObjAddsLevel (Sfm_Ntk_t *p, int i)
static Vec_Int_t *	Sfm_ObjFiArray (Sfm_Ntk_t *p, int i)
static Vec_Int_t *	Sfm_ObjFoArray (Sfm_Ntk_t *p, int i)
static int	Sfm_ObjFaninNum (Sfm_Ntk_t *p, int i)
static int	Sfm_ObjFanoutNum (Sfm_Ntk_t *p, int i)
static int	Sfm_ObjRefIncrement (Sfm_Ntk_t *p, int iObj)
static int	Sfm_ObjRefDecrement (Sfm_Ntk_t *p, int iObj)
static int	Sfm_ObjFanin (Sfm_Ntk_t *p, int i, int k)
static int	Sfm_ObjFanout (Sfm_Ntk_t *p, int i, int k)
static int	Sfm_ObjSatVar (Sfm_Ntk_t *p, int iObj)
static void	Sfm_ObjSetSatVar (Sfm_Ntk_t *p, int iObj, int Num)
static void	Sfm_ObjCleanSatVar (Sfm_Ntk_t *p, int Num)
static void	Sfm_NtkCleanVars (Sfm_Ntk_t *p)
static int	Sfm_ObjLevel (Sfm_Ntk_t *p, int iObj)
static void	Sfm_ObjSetLevel (Sfm_Ntk_t *p, int iObj, int Lev)
static int	Sfm_ObjLevelR (Sfm_Ntk_t *p, int iObj)
static void	Sfm_ObjSetLevelR (Sfm_Ntk_t *p, int iObj, int Lev)
static int	Sfm_ObjUpdateFaninCount (Sfm_Ntk_t *p, int iObj)
static void	Sfm_ObjResetFaninCount (Sfm_Ntk_t *p, int iObj)
void	Kit_DsdPrintFromTruth (unsigned *pTruth, int nVars)
void	Sfm_PrintCnf (Vec_Str_t *vCnf)
	FUNCTION DECLARATIONS ///. More...
int	Sfm_TruthToCnf (word Truth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vCnf)
Vec_Wec_t *	Sfm_CreateCnf (Sfm_Ntk_t *p)
void	Sfm_TranslateCnf (Vec_Wec_t *vRes, Vec_Str_t *vCnf, Vec_Int_t *vFaninMap, int iPivotVar)
Sfm_Ntk_t *	Sfm_ConstructNetwork (Vec_Wec_t *vFanins, int nPis, int nPos)
void	Sfm_NtkPrepare (Sfm_Ntk_t *p)
void	Sfm_NtkUpdate (Sfm_Ntk_t *p, int iNode, int f, int iFaninNew, word uTruth)
int	Sfm_NtkWindowToSolver (Sfm_Ntk_t *p)
	FUNCTION DEFINITIONS ///. More...
word	Sfm_ComputeInterpolant (Sfm_Ntk_t *p)
int	Sfm_ObjMffcSize (Sfm_Ntk_t *p, int iObj)
int	Sfm_NtkCreateWindow (Sfm_Ntk_t *p, int iNode, int fVerbose)

Macro Definition Documentation

#define SFM_FANIN_MAX   6

INCLUDES ///.

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

FileName [rsbInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]PARAMETERS ///

Definition at line 44 of file sfmInt.h.

#define Sfm_NtkForEachNode	(		p,
			i
	)		for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )

Definition at line 170 of file sfmInt.h.

#define Sfm_NtkForEachNodeReverse	(		p,
			i
	)		for ( i = p->nObjs - p->nPos - 1; i >= p->nPis; i-- )

Definition at line 171 of file sfmInt.h.

#define Sfm_NtkForEachPi	(		p,
			i
	)		for ( i = 0; i < p->nPis; i++ )

MACRO DEFINITIONS ///.

Definition at line 168 of file sfmInt.h.

#define Sfm_NtkForEachPo	(		p,
			i
	)		for ( i = p->nObjs - p->nPos; i < p->nObjs; i++ )

Definition at line 169 of file sfmInt.h.

#define Sfm_ObjForEachFanin	(		p,
			Node,
			Fan,
			i
	)		for ( i = 0; i < Sfm_ObjFaninNum(p, Node) && ((Fan = Sfm_ObjFanin(p, Node, i)), 1); i++ )

Definition at line 172 of file sfmInt.h.

#define Sfm_ObjForEachFanout	(		p,
			Node,
			Fan,
			i
	)		for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )

Definition at line 173 of file sfmInt.h.

#define SFM_SAT_SAT   0x8765432187654321

Definition at line 46 of file sfmInt.h.

#define SFM_SAT_UNDEC   0x1234567812345678

Definition at line 45 of file sfmInt.h.

Function Documentation

void Kit_DsdPrintFromTruth	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 490 of file kitDsd.c.

{
    Kit_DsdNtk_t * pTemp, * pTemp2;
//    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
//    Kit_DsdPrintExpanded( pTemp );
    pTemp2 = Kit_DsdExpand( pTemp );
    Kit_DsdPrint( stdout, pTemp2 );
    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
    Kit_DsdNtkFree( pTemp2 );
    Kit_DsdNtkFree( pTemp );
}

word Sfm_ComputeInterpolant

(

Sfm_Ntk_t *

p

)

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

Synopsis [Takes SAT solver and returns interpolant.]

Description [If interpolant does not exist, records difference variables.]

SideEffects []

SeeAlso []

Definition at line 162 of file sfmSat.c.

{
    word * pSign, uCube, uTruth = 0;
    int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
    int pLits[2], nVars = sat_solver_nvars( p->pSat );
    sat_solver_setnvars( p->pSat, nVars + 1 );
    pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
    pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
    while ( 1 ) 
    {
        // find onset minterm
        p->nSatCalls++;
        status = sat_solver_solve( p->pSat, pLits, pLits + 2, p->pPars->nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return SFM_SAT_UNDEC;
        if ( status == l_False )
            return uTruth;
        assert( status == l_True );
        // remember variable values
        Vec_IntClear( p->vValues );
        Vec_IntForEachEntry( p->vDivVars, iVar, i )
            Vec_IntPush( p->vValues, sat_solver_var_value(p->pSat, iVar) );
        // collect divisor literals
        Vec_IntClear( p->vLits );
        Vec_IntPush( p->vLits, Abc_LitNot(pLits[0]) ); // F = 0
        Vec_IntForEachEntry( p->vDivIds, Div, i )
            Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat, Div) );
        // check against offset
        p->nSatCalls++;
        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return SFM_SAT_UNDEC;
        if ( status == l_True )
            break;
        assert( status == l_False );
        // compute cube and add clause
        nFinal = sat_solver_final( p->pSat, &pFinal );
        uCube = ~(word)0;
        Vec_IntClear( p->vLits );
        Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
        for ( i = 0; i < nFinal; i++ )
        {
            if ( pFinal[i] == pLits[0] )
                continue;
            Vec_IntPush( p->vLits, pFinal[i] );
            iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
            uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
        }
        uTruth |= uCube;
        status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
        assert( status );
        nIter++;
    }
    assert( status == l_True );
    // store the counter-example
    Vec_IntForEachEntry( p->vDivVars, iVar, i )
        if ( Vec_IntEntry(p->vValues, i) ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
        {
            pSign = Vec_WrdEntryP( p->vDivCexes, i );
            assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
            Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
        }
    p->nCexes++;
    return SFM_SAT_SAT;
}

Sfm_Ntk_t* Sfm_ConstructNetwork	(	Vec_Wec_t *	vFanins,
		int	nPis,
		int	nPos
	)

Vec_Wec_t* Sfm_CreateCnf

(

Sfm_Ntk_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 122 of file sfmCnf.c.

{
    Vec_Wec_t * vCnfs;
    Vec_Str_t * vCnf, * vCnfBase;
    word uTruth;
    int i, nCubes;
    vCnf = Vec_StrAlloc( 100 );
    vCnfs = Vec_WecStart( p->nObjs );
    Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
    {
        nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
        vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
        Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
        memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
        vCnfBase->nSize = Vec_StrSize(vCnf);
    }
    Vec_StrFree( vCnf );
    return vCnfs;
}

static void Sfm_NtkCleanVars ( Sfm_Ntk_t *  p )

inlinestatic

Definition at line 151 of file sfmInt.h.

{ int i; for ( i = 1; i < p->nSatVars; i++ )  if ( Vec_IntEntry(&p->vVar2Id, i) != -1 ) Sfm_ObjCleanSatVar( p, i ); }

int Sfm_NtkCreateWindow	(	Sfm_Ntk_t *	p,
		int	iNode,
		int	fVerbose
	)

Definition at line 334 of file sfmWin.c.

{
    int i, k, iTemp;
    abctime clkDiv, clkWin = Abc_Clock();

    assert( Sfm_ObjIsNode( p, iNode ) );
    p->iPivotNode = iNode;
    Vec_IntClear( p->vNodes );  // internal
    Vec_IntClear( p->vDivs );   // divisors
    Vec_IntClear( p->vRoots );  // roots
    Vec_IntClear( p->vTfo );    // roots
    Vec_IntClear( p->vOrder );  // variable order

    // collect transitive fanin
    Sfm_NtkIncrementTravId( p );
    if ( Sfm_NtkCollectTfi_rec( p, iNode, p->vNodes ) )
    {
        p->nMaxDivs++;
        p->timeWin += Abc_Clock() - clkWin;
        return 0;
    }

    // create divisors
    clkDiv = Abc_Clock();
    Vec_IntClear( p->vDivs );
    Vec_IntAppend( p->vDivs, p->vNodes );
    Vec_IntPop( p->vDivs );
    // add non-topological divisors
    if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
    {
        Sfm_NtkIncrementTravId2( p );
        Vec_IntForEachEntry( p->vDivs, iTemp, i )
            if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
//                Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) - 1 );
                Sfm_NtkAddDivisors( p, iTemp, p->nLevelMax - Sfm_ObjLevelR(p, iNode) ); 
    }
    if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax )
    {
/*
        k = 0;
        Vec_IntForEachEntryStart( p->vDivs, iTemp, i, Vec_IntSize(p->vDivs) - p->pPars->nWinSizeMax )
            Vec_IntWriteEntry( p->vDivs, k++, iTemp );
        assert( k == p->pPars->nWinSizeMax );
*/
        Vec_IntShrink( p->vDivs, p->pPars->nWinSizeMax );
    }
    assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
    p->nMaxDivs += (int)(Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax);
    // remove node/fanins from divisors
    // mark fanins
    Sfm_NtkIncrementTravId2( p );
    Sfm_ObjSetTravIdCurrent2( p, iNode );
    Sfm_ObjForEachFanin( p, iNode, iTemp, i )
        Sfm_ObjSetTravIdCurrent2( p, iTemp );
    // compact divisors
    k = 0;
    Vec_IntForEachEntry( p->vDivs, iTemp, i )
        if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) && Sfm_ObjIsUseful(p, iTemp) )
            Vec_IntWriteEntry( p->vDivs, k++, iTemp );
    Vec_IntShrink( p->vDivs, k );
    assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
    clkDiv = Abc_Clock() - clkDiv;
    p->timeDiv += clkDiv;
    p->nTotalDivs += Vec_IntSize(p->vDivs);
 
    // collect TFO and window roots
    if ( p->pPars->nTfoLevMax > 0 && !Sfm_NtkCheckRoot(p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax) )
    {
        // explore transitive fanout
        Sfm_NtkIncrementTravId( p );
        Sfm_NtkComputeRoots_rec( p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax, p->vRoots, p->vTfo );
        assert( Vec_IntSize(p->vRoots) > 0 );
        assert( Vec_IntSize(p->vTfo) > 0 );
        // compute new leaves and nodes
        Sfm_NtkIncrementTravId( p );
        Vec_IntForEachEntry( p->vRoots, iTemp, i )
            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
            {
                Vec_IntClear( p->vRoots );
                Vec_IntClear( p->vTfo );
                Vec_IntClear( p->vOrder );
                break;
            }
        if ( Vec_IntSize(p->vRoots) > 0 )
        Vec_IntForEachEntry( p->vTfo, iTemp, i )
            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
            {
                Vec_IntClear( p->vRoots );
                Vec_IntClear( p->vTfo );
                Vec_IntClear( p->vOrder );
                break;
            }
        if ( Vec_IntSize(p->vRoots) > 0 )
        Vec_IntForEachEntry( p->vDivs, iTemp, i )
            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
            {
                Vec_IntClear( p->vRoots );
                Vec_IntClear( p->vTfo );
                Vec_IntClear( p->vOrder );
                break;
            }
    }

    if ( Vec_IntSize(p->vOrder) == 0 )
    {
        int Temp = p->pPars->nWinSizeMax;
        p->pPars->nWinSizeMax = 0;
        Sfm_NtkIncrementTravId( p );
        Sfm_NtkCollectTfi_rec( p, iNode, p->vOrder );
        Vec_IntForEachEntry( p->vDivs, iTemp, i )
            Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder );
        p->pPars->nWinSizeMax = Temp;
    }

    // statistics
    p->timeWin += Abc_Clock() - clkWin - clkDiv;
    if ( !fVerbose )
        return 1;

    // print stats about the window
    printf( "%6d : ", iNode );
    printf( "Leaves = %5d. ", 0 );
    printf( "Nodes = %5d. ",  Vec_IntSize(p->vNodes) );
    printf( "Roots = %5d. ",  Vec_IntSize(p->vRoots) );
    printf( "Divs = %5d. ",   Vec_IntSize(p->vDivs) );
    printf( "\n" );
    return 1;
}

static int Sfm_NtkNodeNum ( Sfm_Ntk_t *  p )

inlinestatic

Definition at line 127 of file sfmInt.h.

{ return p->nObjs - p->nPis - p->nPos;              }

static int Sfm_NtkPiNum ( Sfm_Ntk_t *  p )

inlinestatic

Definition at line 125 of file sfmInt.h.

{ return p->nPis;                                   }

static int Sfm_NtkPoNum ( Sfm_Ntk_t *  p )

inlinestatic

Definition at line 126 of file sfmInt.h.

{ return p->nPos;                                   }

void Sfm_NtkPrepare

(

Sfm_Ntk_t *

p

)

Definition at line 195 of file sfmNtk.c.

{
    p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
    p->vNodes    = Vec_IntAlloc( 1000 );
    p->vDivs     = Vec_IntAlloc( 100 );
    p->vRoots    = Vec_IntAlloc( 1000 );
    p->vTfo      = Vec_IntAlloc( 1000 );
    p->vDivCexes = Vec_WrdStart( p->pPars->nWinSizeMax );
    p->vOrder    = Vec_IntAlloc( 100 );
    p->vDivVars  = Vec_IntAlloc( 100 );
    p->vDivIds   = Vec_IntAlloc( 1000 );
    p->vLits     = Vec_IntAlloc( 100 );
    p->vValues   = Vec_IntAlloc( 100 );
    p->vClauses  = Vec_WecAlloc( 100 );
    p->vFaninMap = Vec_IntAlloc( 10 );
    p->pSat      = sat_solver_new();
    sat_solver_setnvars( p->pSat, p->pPars->nWinSizeMax );
}

void Sfm_NtkUpdate	(	Sfm_Ntk_t *	p,
		int	iNode,
		int	f,
		int	iFaninNew,
		word	uTruth
	)

Definition at line 314 of file sfmNtk.c.

{
    int iFanin = Sfm_ObjFanin( p, iNode, f );
    assert( Sfm_ObjIsNode(p, iNode) );
    assert( iFanin != iFaninNew );
    if ( uTruth == 0 || ~uTruth == 0 )
    {
        Sfm_ObjForEachFanin( p, iNode, iFanin, f )
        {
            int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
            Sfm_NtkDeleteObj_rec( p, iFanin );
        }
        Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
    }
    else
    {
        // replace old fanin by new fanin
        Sfm_NtkRemoveFanin( p, iNode, iFanin );
        Sfm_NtkAddFanin( p, iNode, iFaninNew );
        // recursively remove MFFC
        Sfm_NtkDeleteObj_rec( p, iFanin );
    }
    // update logic level
    Sfm_NtkUpdateLevel_rec( p, iNode );
    if ( iFaninNew != -1 )
        Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
    if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
        Sfm_NtkUpdateLevelR_rec( p, iFanin );
    // update truth table
    Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
    Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
}

int Sfm_NtkWindowToSolver

(

Sfm_Ntk_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Converts a window into a SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file sfmSat.c.

{
    // p->vOrder contains all variables in the window in a good order
    // p->vDivs is a subset of nodes in p->vOrder used as divisor candidates
    // p->vTfo contains TFO of the node (does not include node)
    // p->vRoots contains roots of the TFO of the node (may include node)
    Vec_Int_t * vClause;
    int RetValue, iNode = -1, iFanin, i, k;
    abctime clk = Abc_Clock();
//    if ( p->pSat )
//        printf( "%d  ", p->pSat->stats.learnts );
    sat_solver_restart( p->pSat );
    sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vOrder) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 10 );
    // create SAT variables
    Sfm_NtkCleanVars( p );
    p->nSatVars = 1;
    Vec_IntForEachEntry( p->vOrder, iNode, i )
        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
    // collect divisor variables
    Vec_IntClear( p->vDivVars );
    Vec_IntForEachEntry( p->vDivs, iNode, i )
        Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) );
    // add CNF clauses for the TFI
    Vec_IntForEachEntry( p->vOrder, iNode, i )
    {
        if ( Sfm_ObjIsPi(p, iNode) )
            continue;
        // collect fanin variables
        Vec_IntClear( p->vFaninMap );
        Sfm_ObjForEachFanin( p, iNode, iFanin, k )
            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
        Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
        // generate CNF 
        Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, -1 );
        // add clauses
        Vec_WecForEachLevel( p->vClauses, vClause, k )
        {
            if ( Vec_IntSize(vClause) == 0 )
                break;
            RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
            if ( RetValue == 0 )
                return 0;
        }
    }
    if ( Vec_IntSize(p->vTfo) > 0 )
    {
        assert( p->pPars->nTfoLevMax > 0 );
        assert( Vec_IntSize(p->vRoots) > 0 );
        assert( Vec_IntEntry(p->vTfo, 0) != p->iPivotNode );
        // collect variables of root nodes
        Vec_IntClear( p->vLits );
        Vec_IntForEachEntry( p->vRoots, iNode, i )
            Vec_IntPush( p->vLits, Sfm_ObjSatVar(p, iNode) );
        // assign new variables to the TFO nodes
        Vec_IntForEachEntry( p->vTfo, iNode, i )
        {
            Sfm_ObjCleanSatVar( p, Sfm_ObjSatVar(p, iNode) );
            Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
        }
        // add CNF clauses for the TFO
        Vec_IntForEachEntry( p->vTfo, iNode, i )
        {
            assert( Sfm_ObjIsNode(p, iNode) );
            // collect fanin variables
            Vec_IntClear( p->vFaninMap );
            Sfm_ObjForEachFanin( p, iNode, iFanin, k )
                Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
            // generate CNF 
            Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, Sfm_ObjSatVar(p, p->iPivotNode) );
            // add clauses
            Vec_WecForEachLevel( p->vClauses, vClause, k )
            {
                if ( Vec_IntSize(vClause) == 0 )
                    break;
                RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
                if ( RetValue == 0 )
                    return 0;
            }
        }
        // create XOR clauses for the roots
        Vec_IntForEachEntry( p->vRoots, iNode, i )
        {
            sat_solver_add_xor( p->pSat, Vec_IntEntry(p->vLits, i), Sfm_ObjSatVar(p, iNode), p->nSatVars++, 0 );
            Vec_IntWriteEntry( p->vLits, i, Abc_Var2Lit(p->nSatVars-1, 0) );
        }
        // make OR clause for the last nRoots variables
        RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
        if ( RetValue == 0 )
            return 0;
    }
    // finalize
    RetValue = sat_solver_simplify( p->pSat );
    p->timeCnf += Abc_Clock() - clk;
    return RetValue;
} 

static int Sfm_ObjAddsLevel ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 134 of file sfmInt.h.

{ return Sfm_ObjAddsLevelArray(p->vEmpty, i);       }

static int Sfm_ObjAddsLevelArray ( Vec_Str_t *  p, int  i  )

inlinestatic

Definition at line 133 of file sfmInt.h.

{ return p == NULL || Vec_StrEntry(p, i) == 0;      }

static void Sfm_ObjCleanSatVar ( Sfm_Ntk_t *  p, int  Num  )

inlinestatic

Definition at line 150 of file sfmInt.h.

{ int iObj = Vec_IntEntry(&p->vVar2Id, Num); assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); Vec_IntWriteEntry(&p->vId2Var, iObj, -1);  Vec_IntWriteEntry(&p->vVar2Id, Num, -1); }

static int Sfm_ObjFanin ( Sfm_Ntk_t *  p, int  i, int  k  )

inlinestatic

Definition at line 145 of file sfmInt.h.

{ return Vec_IntEntry(Sfm_ObjFiArray(p, i), k);     }

static int Sfm_ObjFaninNum ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 139 of file sfmInt.h.

{ return Vec_IntSize(Sfm_ObjFiArray(p, i));         }

static int Sfm_ObjFanout ( Sfm_Ntk_t *  p, int  i, int  k  )

inlinestatic

Definition at line 146 of file sfmInt.h.

{ return Vec_IntEntry(Sfm_ObjFoArray(p, i), k);     }

static int Sfm_ObjFanoutNum ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 140 of file sfmInt.h.

{ return Vec_IntSize(Sfm_ObjFoArray(p, i));         }

static Vec_Int_t* Sfm_ObjFiArray ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 136 of file sfmInt.h.

{ return Vec_WecEntry(&p->vFanins, i);              }

static Vec_Int_t* Sfm_ObjFoArray ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 137 of file sfmInt.h.

{ return Vec_WecEntry(&p->vFanouts, i);             }

static int Sfm_ObjIsFixed ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 132 of file sfmInt.h.

{ return Vec_StrEntry(p->vFixed, i);                }

static int Sfm_ObjIsNode ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 131 of file sfmInt.h.

{ return i >= p->nPis && i + p->nPos < p->nObjs;    }

static int Sfm_ObjIsPi ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 129 of file sfmInt.h.

{ return i < p->nPis;                               }

static int Sfm_ObjIsPo ( Sfm_Ntk_t *  p, int  i  )

inlinestatic

Definition at line 130 of file sfmInt.h.

{ return i + p->nPos >= p->nObjs;                   }

static int Sfm_ObjLevel ( Sfm_Ntk_t *  p, int  iObj  )

inlinestatic

Definition at line 153 of file sfmInt.h.

{ return Vec_IntEntry( &p->vLevels, iObj );                         }

static int Sfm_ObjLevelR ( Sfm_Ntk_t *  p, int  iObj  )

inlinestatic

Definition at line 156 of file sfmInt.h.

{ return Vec_IntEntry( &p->vLevelsR, iObj );                        }

int Sfm_ObjMffcSize	(	Sfm_Ntk_t *	p,
		int	iObj
	)

Definition at line 89 of file sfmWin.c.

{
    int Count1, Count2;
    if ( Sfm_ObjIsPi(p, iObj) )
        return 0;
    if ( Sfm_ObjFanoutNum(p, iObj) != 1 )
        return 0;
    assert( Sfm_ObjIsNode( p, iObj ) );
    Count1 = Sfm_ObjDeref( p, iObj );
    Count2 = Sfm_ObjRef( p, iObj );
    assert( Count1 == Count2 );
    return Count1;
}

static int Sfm_ObjRefDecrement ( Sfm_Ntk_t *  p, int  iObj  )

inlinestatic

Definition at line 143 of file sfmInt.h.

{ return --Sfm_ObjFoArray(p, iObj)->nSize;          } 

static int Sfm_ObjRefIncrement ( Sfm_Ntk_t *  p, int  iObj  )

inlinestatic

Definition at line 142 of file sfmInt.h.

{ return ++Sfm_ObjFoArray(p, iObj)->nSize;          } 

static void Sfm_ObjResetFaninCount ( Sfm_Ntk_t *  p, int  iObj  )

inlinestatic

Definition at line 160 of file sfmInt.h.

{ Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); }

static int Sfm_ObjSatVar ( Sfm_Ntk_t *  p, int  iObj  )

inlinestatic

Definition at line 148 of file sfmInt.h.

{ assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); return Vec_IntEntry(&p->vId2Var, iObj);  }

static void Sfm_ObjSetLevel ( Sfm_Ntk_t *  p, int  iObj, int  Lev  )

inlinestatic

Definition at line 154 of file sfmInt.h.

{ Vec_IntWriteEntry( &p->vLevels, iObj, Lev );                      }

static void Sfm_ObjSetLevelR ( Sfm_Ntk_t *  p, int  iObj, int  Lev  )

inlinestatic

Definition at line 157 of file sfmInt.h.

{ Vec_IntWriteEntry( &p->vLevelsR, iObj, Lev );                     }

static void Sfm_ObjSetSatVar ( Sfm_Ntk_t *  p, int  iObj, int  Num  )

inlinestatic

Definition at line 149 of file sfmInt.h.

{ assert(Vec_IntEntry(&p->vId2Var, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num);  Vec_IntWriteEntry(&p->vVar2Id, Num, iObj);  }

static int Sfm_ObjUpdateFaninCount ( Sfm_Ntk_t *  p, int  iObj  )

inlinestatic

Definition at line 159 of file sfmInt.h.

{ return Vec_IntAddToEntry(&p->vCounts, iObj, -1);                  }

void Sfm_PrintCnf

(

Vec_Str_t *

vCnf

)

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [sfmCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [CNF computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file sfmCnf.c.

{
    char Entry;
    int i, Lit;
    Vec_StrForEachEntry( vCnf, Entry, i )
    {
        Lit = (int)Entry;
        if ( Lit == -1 )
            printf( "\n" );
        else
            printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
    }
}

void Sfm_TranslateCnf	(	Vec_Wec_t *	vRes,
		Vec_Str_t *	vCnf,
		Vec_Int_t *	vFaninMap,
		int	iPivotVar
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file sfmCnf.c.

{
    Vec_Int_t * vClause;
    char Entry;
    int i, Lit;
    Vec_WecClear( vRes );
    vClause = Vec_WecPushLevel( vRes );
    Vec_StrForEachEntry( vCnf, Entry, i )
    {
        if ( (int)Entry == -1 )
        {
            vClause = Vec_WecPushLevel( vRes );
            continue;
        }
        Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
        Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
        Vec_IntPush( vClause, Lit );
    }
}

int Sfm_TruthToCnf	(	word	Truth,
		int	nVars,
		Vec_Int_t *	vCover,
		Vec_Str_t *	vCnf
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file sfmCnf.c.

{
    Vec_StrClear( vCnf );
    if ( Truth == 0 || ~Truth == 0 )
    {
//        assert( nVars == 0 );
        Vec_StrPush( vCnf, (char)(Truth == 0) );
        Vec_StrPush( vCnf, (char)-1 );
        return 1;
    }
    else 
    {
        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
        assert( nVars > 0 );
        for ( c = 0; c < 2; c ++ )
        {
            Truth = c ? ~Truth : Truth;
            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
            assert( RetValue == 0 );
            nCubes += Vec_IntSize( vCover );
            Vec_IntForEachEntry( vCover, Cube, i )
            {
                for ( k = 0; k < nVars; k++ )
                {
                    Literal = 3 & (Cube >> (k << 1));
                    if ( Literal == 1 )      // '0'  -> pos lit
                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
                    else if ( Literal == 2 ) // '1'  -> neg lit
                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
                    else if ( Literal != 0 )
                        assert( 0 );
                }
                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
                Vec_StrPush( vCnf, (char)-1 );
            }
        }
        return nCubes;
    }
}