#include "gia.h"
#include "misc/extra/extra.h"
#include "misc/tim/tim.h"
#include "sat/bsat/satStore.h"

Include dependency graph for giaSatLE.c:

Classes
struct	Sle_Man_t_

Macros
#define	Sle_ForEachCut(pList, pCut, i)

#define	Sle_ForEachCut1(pList, pCut, i)

Typedefs
typedef struct Sle_Man_t_	Sle_Man_t

Functions
int	Sle_ManCutMerge (Gia_Man_t p, int iObj, Vec_Int_t vCuts, Vec_Int_t *vTemp, int nLutSize)

Vec_Int_t *	Sle_ManComputeCuts (Gia_Man_t *p, int nLutSize, int fVerbose)

int	Sle_ManComputeDelayCut (Gia_Man_t p, int pCut, Vec_Int_t *vTime)

int	Sle_ManComputeDelayOne (Gia_Man_t p, int iObj, Vec_Int_t vCuts, Vec_Int_t *vTime)

int	Sle_ManComputeDelay (Gia_Man_t p, Vec_Int_t vCuts)

void	Sle_ManPrintCut (int *pCut)

void	Sle_ManPrintCuts (Gia_Man_t p, Vec_Int_t vCuts, int iObj)

void	Sle_ManPrintCutsAll (Gia_Man_t p, Vec_Int_t vCuts)

void	Sle_ManComputeCutsTest (Gia_Man_t *p)

Vec_Bit_t *	Sle_ManInternalNodeMask (Gia_Man_t *pGia)

int	Sle_ManCutHasPisOnly (int pCut, Vec_Bit_t vMask)

void	Sle_ManCollectCutFaninsOne (Gia_Man_t pGia, int iObj, Vec_Int_t vCuts, Vec_Bit_t vMask, Vec_Int_t vCutFanins, Vec_Bit_t *vMap)

Vec_Wec_t *	Sle_ManCollectCutFanins (Gia_Man_t pGia, Vec_Int_t vCuts, Vec_Bit_t *vMask)

Sle_Man_t *	Sle_ManAlloc (Gia_Man_t *pGia, int nLevels, int fVerbose)

void	Sle_ManStop (Sle_Man_t *p)

void	Sle_ManMarkupVariables (Sle_Man_t *p)

void	Sle_ManDeriveInit (Sle_Man_t *p)

void	Sle_ManDeriveCnf (Sle_Man_t *p, int nBTLimit, int fDynamic)

int	Sle_ManAddEdgeConstraints (Sle_Man_t *p, int nEdges)

void	Sle_ManDeriveResult (Sle_Man_t p, Vec_Int_t vEdge2, Vec_Int_t *vMapping)

void	Sle_ManExplore (Gia_Man_t *pGia, int nBTLimit, int DelayInit, int fDynamic, int fTwoEdges, int fVerbose)

Macro Definition Documentation

◆ Sle_ForEachCut

#define Sle_ForEachCut	(	pList,
		pCut,
		i )

Value:

for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Sle_CutSize(pCut) + 1 )

Definition at line 43 of file giaSatLE.c.

◆ Sle_ForEachCut1

#define Sle_ForEachCut1	(	pList,
		pCut,
		i )

Value:

for ( i = 0, pCut = pList + 1; i <= pList[0]; i++, pCut += Sle_CutSize(pCut) + 1 )

Definition at line 44 of file giaSatLE.c.

Typedef Documentation

◆ Sle_Man_t

typedef struct Sle_Man_t_ Sle_Man_t

Definition at line 401 of file giaSatLE.c.

Function Documentation

◆ Sle_ManAddEdgeConstraints()

int Sle_ManAddEdgeConstraints	(	Sle_Man_t *	p,
		int	nEdges )

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

Synopsis [Add edge compatibility constraints.]

Description [Returns 1 if constraints have been added.]

SideEffects []

SeeAlso []

Definition at line 806 of file giaSatLE.c.

{
    Vec_Int_t * vArray;
    Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
    int value, iObj, nAdded = 0;
    assert( nEdges == 1 || nEdges == 2 );
    Vec_WecForEachLevel( p->vFanoutEdges, vArray, iObj )
    {
        int j, k, EdgeJ, EdgeK;
        // check if they are incompatible
        Vec_IntClear( vTemp );
        Vec_IntForEachEntry( vArray, EdgeJ, j )
            if ( sat_solver_var_value(p->pSat, EdgeJ) )
                Vec_IntPush( vTemp, EdgeJ );
        if ( Vec_IntSize(vTemp) <= nEdges )
            continue;
        nAdded++;
        if ( nEdges == 1 )
        {
            // generate pairs
            Vec_IntForEachEntry( vTemp, EdgeJ, j )
                Vec_IntForEachEntryStart( vTemp, EdgeK, k, j+1 )
                {
                    Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(EdgeJ, 1), Abc_Var2Lit(EdgeK, 1) );
                    value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                    assert( value );
                }
            p->nEdgeClas2 += Vec_IntSize(vTemp) * (Vec_IntSize(vTemp) - 1) / 2;
        }
        else if ( nEdges == 2 )
        {
            int m, EdgeM;
            // generate triples
            Vec_IntForEachEntry( vTemp, EdgeJ, j )
                Vec_IntForEachEntryStart( vTemp, EdgeK, k, j+1 )
                    Vec_IntForEachEntryStart( vTemp, EdgeM, m, k+1 )
                    {
                        Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(EdgeJ, 1), Abc_Var2Lit(EdgeK, 1) );
                        Vec_IntPush( p->vLits, Abc_Var2Lit(EdgeM, 1) );
                        value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                        assert( value );
                    }
            p->nEdgeClas2 += Vec_IntSize(vTemp) * (Vec_IntSize(vTemp) - 1) * (Vec_IntSize(vTemp) - 2) / 6;
        }
        else assert( 0 );
    }
    Vec_IntFree( vTemp );
    //printf( "Added clauses to %d nodes.\n", nAdded );
    return nAdded;
}

Here is the caller graph for this function:

◆ Sle_ManAlloc()

Sle_Man_t * Sle_ManAlloc	(	Gia_Man_t *	pGia,
		int	nLevels,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file giaSatLE.c.

{
    Sle_Man_t * p   = ABC_CALLOC( Sle_Man_t, 1 );
    p->pGia         = pGia;
    p->nLevels      = nLevels;
    p->fVerbose     = fVerbose;
    p->vMask        = Sle_ManInternalNodeMask( pGia );
    p->vCuts        = Sle_ManComputeCuts( pGia, 4, fVerbose );
    p->vCutFanins   = Sle_ManCollectCutFanins( pGia, p->vCuts, p->vMask );
    p->vFanoutEdges = Vec_WecStart( Gia_ManObjNum(pGia) );
    p->vEdgeCuts    = Vec_WecAlloc( 100 );
    p->vObjMap      = Vec_IntStartFull( Gia_ManObjNum(pGia) );
    p->vCutFirst    = Vec_IntStartFull( Gia_ManObjNum(pGia) );
    p->vEdgeFirst   = Vec_IntStartFull( Gia_ManObjNum(pGia) );
    p->vDelayFirst  = Vec_IntStartFull( Gia_ManObjNum(pGia) );
    p->vPolars      = Vec_IntAlloc( 100 );
    p->vLits        = Vec_IntAlloc( 100 );
    p->nLevels      = Sle_ManComputeDelay( pGia, p->vCuts );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManCollectCutFanins()

Vec_Wec_t * Sle_ManCollectCutFanins	(	Gia_Man_t *	pGia,
		Vec_Int_t *	vCuts,
		Vec_Bit_t *	vMask )

Definition at line 389 of file giaSatLE.c.

{
    int iObj;
    Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(pGia) );
    Vec_Wec_t * vCutFanins = Vec_WecStart( Gia_ManObjNum(pGia) );
    Gia_ManForEachAndId( pGia, iObj )
        Sle_ManCollectCutFaninsOne( pGia, iObj, vCuts, vMask, Vec_WecEntry(vCutFanins, iObj), vMap );
    Vec_BitFree( vMap );
    return vCutFanins;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManCollectCutFaninsOne()

void Sle_ManCollectCutFaninsOne	(	Gia_Man_t *	pGia,
		int	iObj,
		Vec_Int_t *	vCuts,
		Vec_Bit_t *	vMask,
		Vec_Int_t *	vCutFanins,
		Vec_Bit_t *	vMap )

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

Synopsis [Derive cut fanins of each node.]

Description [These are nodes that are fanins of some cut of this node.]

SideEffects []

SeeAlso []

Definition at line 371 of file giaSatLE.c.

{
    int i, iFanin, * pCut, * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) );
    Sle_ForEachCut( pList, pCut, i )
    {
        int nSize   = Sle_CutSize(pCut);
        int k, * pC = Sle_CutLeaves(pCut);
        assert( nSize > 1 );
        for ( k = 0; k < nSize; k++ )
            if ( Vec_BitEntry(vMask, pC[k]) && !Vec_BitEntry(vMap, pC[k]) )
            {
                Vec_BitWriteEntry( vMap, pC[k], 1 );
                Vec_IntPush( vCutFanins, pC[k] );
            }
    }
    Vec_IntForEachEntry( vCutFanins, iFanin, i )
        Vec_BitWriteEntry( vMap, iFanin, 0 );
}

Here is the caller graph for this function:

◆ Sle_ManComputeCuts()

Vec_Int_t * Sle_ManComputeCuts	(	Gia_Man_t *	p,
		int	nLutSize,
		int	fVerbose )

Definition at line 205 of file giaSatLE.c.

{
    int i, iObj, nCuts = 0;
    Vec_Int_t * vTemp = Vec_IntAlloc( 1000 );
    Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) );
    assert( nLutSize <= 6 );
    Vec_IntFill( vCuts, Gia_ManObjNum(p), 0 );
    Gia_ManForEachCiId( p, iObj, i )
    {
        Vec_IntWriteEntry( vCuts, iObj, Vec_IntSize(vCuts) );
        Vec_IntPush( vCuts, 0 );
        Vec_IntPush( vCuts, Sle_CutSetSizeSign(1, 1<<(iObj % 28)) );
        Vec_IntPush( vCuts, iObj );
    }
    Gia_ManForEachAndId( p, iObj )
        nCuts += Sle_ManCutMerge( p, iObj, vCuts, vTemp, nLutSize );
    if ( fVerbose )
        printf( "Nodes = %d.  Cuts = %d.  Cuts/Node = %.2f.  Ints/Node = %.2f.  Mem = %.2f MB.\n", 
            Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 
            1.0*(Vec_IntSize(vCuts)-Gia_ManObjNum(p))/Gia_ManAndNum(p), 
            1.0*Vec_IntMemory(vCuts) / (1<<20) );
    Vec_IntFree( vTemp );
    return vCuts;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManComputeCutsTest()

void Sle_ManComputeCutsTest ( Gia_Man_t * p )

Definition at line 311 of file giaSatLE.c.

{
    Vec_Int_t * vCuts = Sle_ManComputeCuts( p, 4, 1 );
    //Sle_ManPrintCutsAll( p, vCuts );
    Vec_IntFree( vCuts );
}

Here is the call graph for this function:

◆ Sle_ManComputeDelay()

int Sle_ManComputeDelay	(	Gia_Man_t *	p,
		Vec_Int_t *	vCuts )

Definition at line 262 of file giaSatLE.c.

{
    int iObj, Delay, DelayMax = 0;
    Vec_Int_t * vTime = Vec_IntStart( Gia_ManObjNum(p) );
    Gia_ManForEachAndId( p, iObj )
    {
        Delay = Sle_ManComputeDelayOne( p, iObj, vCuts, vTime );
        DelayMax = Abc_MaxInt( DelayMax, Delay );
    }
    Vec_IntFree( vTime );
    //printf( "Delay = %d.\n", DelayMax );
    return DelayMax;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManComputeDelayCut()

int Sle_ManComputeDelayCut	(	Gia_Man_t *	p,
		int *	pCut,
		Vec_Int_t *	vTime )

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

Synopsis [Cut delay computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file giaSatLE.c.

{
    int nSize   = Sle_CutSize(pCut);
    int k, * pC = Sle_CutLeaves(pCut);
    int DelayMax = 0;
    for ( k = 0; k < nSize; k++ )
        DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(vTime, pC[k]) );
    return DelayMax + 1;
}

Here is the caller graph for this function:

◆ Sle_ManComputeDelayOne()

int Sle_ManComputeDelayOne	(	Gia_Man_t *	p,
		int	iObj,
		Vec_Int_t *	vCuts,
		Vec_Int_t *	vTime )

Definition at line 250 of file giaSatLE.c.

{
    int i, * pCut, Delay, DelayMin = ABC_INFINITY;
    int * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) );
    Sle_ForEachCut( pList, pCut, i )
    {
        Delay = Sle_ManComputeDelayCut( p, pCut, vTime );
        DelayMin = Abc_MinInt( DelayMin, Delay );
    }
    Vec_IntWriteEntry( vTime, iObj, DelayMin );
    return DelayMin;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManCutHasPisOnly()

int Sle_ManCutHasPisOnly	(	int *	pCut,
		Vec_Bit_t *	vMask )

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

Synopsis [Check if the cut contains only primary inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file giaSatLE.c.

{
    int k, * pC = Sle_CutLeaves(pCut);
    for ( k = 0; k < Sle_CutSize(pCut); k++ )
        if ( Vec_BitEntry(vMask, pC[k]) ) // internal node
            return 0;
    return 1;
}

Here is the caller graph for this function:

◆ Sle_ManCutMerge()

int Sle_ManCutMerge	(	Gia_Man_t *	p,
		int	iObj,
		Vec_Int_t *	vCuts,
		Vec_Int_t *	vTemp,
		int	nLutSize )

Definition at line 170 of file giaSatLE.c.

{
    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
    int * pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, iObj)) );
    int * pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, iObj)) );
    int * pCut0, * pCut1, i, k, Cut[8], nCuts = 0;
    Vec_IntFill( vTemp, 1, 0 );
    Sle_ForEachCut1( pList0, pCut0, i )
    Sle_ForEachCut1( pList1, pCut1, k )
    {
        if ( Sle_CutSize(pCut0) + Sle_CutSize(pCut1) > nLutSize && Sle_CutCountBits(Sle_CutSign(pCut0) | Sle_CutSign(pCut1)) > nLutSize )
            continue;
        if ( !Sle_CutMergeOrder(pCut0, pCut1, Cut, nLutSize) )
            continue;
        if ( Sle_SetLastCutIsContained(vTemp, Cut) )
            continue;
        Sle_SetAddCut( vTemp, Cut );
    }
    // reload
    Vec_IntWriteEntry( vCuts, iObj, Vec_IntSize(vCuts) );
    Vec_IntPush( vCuts, -1 );
    pList0 = Vec_IntArray(vTemp);
    Sle_ForEachCut( pList0, pCut0, i )
    {
        if ( !Sle_CutIsUsed(pCut0) )
            continue;
        Vec_IntPushArray( vCuts, pCut0, Sle_CutSize(pCut0)+1 );
        nCuts++;
    }
    // add unit cut
    Vec_IntPush( vCuts, Sle_CutSetSizeSign(1, 1<<(iObj % 28)) );
    Vec_IntPush( vCuts, iObj );
    Vec_IntWriteEntry( vCuts, Vec_IntEntry(vCuts, iObj), nCuts );
    return nCuts;
}

Here is the caller graph for this function:

◆ Sle_ManDeriveCnf()

void Sle_ManDeriveCnf	(	Sle_Man_t *	p,
		int	nBTLimit,
		int	fDynamic )

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

Synopsis [Derive CNF.]

Description []

SideEffects []

SeeAlso []

Definition at line 627 of file giaSatLE.c.

{
    int nTimeOut = 0;
    int i, iObj, value;
    Vec_Int_t * vArray;
 
    // start the SAT solver
    p->pSat = sat_solver_new();
    sat_solver_setnvars( p->pSat, p->nVarsTotal );
    sat_solver_set_resource_limits( p->pSat, nBTLimit, 0, 0, 0 );
    sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
    sat_solver_set_random( p->pSat, 1 );
    sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolars), Vec_IntSize(p->vPolars) );
    //sat_solver_set_var_activity( p->pSat, NULL, p->nVarsTotal );
 
    // set drivers to be mapped
    Gia_ManForEachCoDriverId( p->pGia, iObj, i )
        if ( Vec_BitEntry(p->vMask, iObj) ) // internal node
        {
            Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iObj, 0) ); // pos lit
            value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
            assert( value );
        }
 
    // add cover clauses and edge-to-cut clauses
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        int e, iEdge, nEdges = 0, Entry;
        int iCutVar0  = Vec_IntEntry( p->vCutFirst, iObj );
        int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
        int * pCut, * pList  = Sle_ManList( p, iObj );
        Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
        assert( iCutVar0 > 0 && iEdgeVar0 > 0 );
        // node requires one of the cuts
        Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iObj, 1) ); // neg lit
        for ( i = 0; i < Sle_ListCutNum(pList); i++ )
            Vec_IntPush( p->vLits, Abc_Var2Lit(iCutVar0 + i, 0) );
        value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
        assert( value );
        // cuts are mutually exclusive
        for ( i = 0; i < Sle_ListCutNum(pList); i++ )
            for ( e = i+1; e < Sle_ListCutNum(pList); e++ )
            {
                Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iCutVar0 + i, 1), Abc_Var2Lit(iCutVar0 + e, 1) );
                value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                assert( value );
            }
        // cut requires fanin nodes
        Vec_WecInit( p->vEdgeCuts, Vec_IntSize(vCutFans) );
        Sle_ForEachCut( pList, pCut, i )
        {
            int nSize   = Sle_CutSize(pCut);
            int k, * pC = Sle_CutLeaves(pCut);
            assert( nSize > 1 );
            for ( k = 0; k < nSize; k++ )
            {
                if ( !Vec_BitEntry(p->vMask, pC[k]) )
                    continue;
                Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iCutVar0 + i, 1), Abc_Var2Lit(pC[k], 0) );
                value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                assert( value );
                // find the edge ID between pC[k] and iObj
                iEdge = Vec_IntEntry(p->vObjMap, pC[k]);
                if ( iEdge == -1 )
                {
                    Vec_IntWriteEntry( p->vObjMap, pC[k], (iEdge = nEdges++) );
                    Vec_WecPush( p->vFanoutEdges, pC[k], iEdgeVar0 + iEdge );
                }
                Vec_WecPush( p->vEdgeCuts, iEdge, iCutVar0 + i );
                p->nCutClas++;
            }
            // cut requires the node
            Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iCutVar0 + i, 1), Abc_Var2Lit(iObj, 0) );
            value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
            assert( value );
        }
        assert( nEdges == Vec_IntSize(vCutFans) );
 
        // edge requires one of the fanout cuts
        Vec_WecForEachLevel( p->vEdgeCuts, vArray, e )
        {
            assert( Vec_IntSize(vArray) > 0 );
            Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iEdgeVar0 + e, 1) ); // neg lit (edge)
            Vec_IntForEachEntry( vArray, Entry, i )
                Vec_IntPush( p->vLits, Abc_Var2Lit(Entry, 0) ); // pos lit (cut)
            value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
            assert( value );
            p->nEdgeClas++;
        }
 
        // clean object map
        Vec_IntForEachEntry( vCutFans, Entry, i )
            Vec_IntWriteEntry( p->vObjMap, Entry, -1 );
    }
 
    // mutual exclusivity of edges
    Vec_WecForEachLevel( p->vFanoutEdges, vArray, iObj )
    {
        int j, k, EdgeJ, EdgeK;
        int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
        Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
        // add fanin edges
        for ( i = 0; i < Vec_IntSize(vCutFans); i++ )
            Vec_IntPush( vArray, iEdgeVar0 + i );
        // generate pairs
        if ( fDynamic )
            continue;
        Vec_IntForEachEntry( vArray, EdgeJ, j )
            Vec_IntForEachEntryStart( vArray, EdgeK, k, j+1 )
            {
                Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(EdgeJ, 1), Abc_Var2Lit(EdgeK, 1) );
                value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                assert( value );
            }
        p->nEdgeClas2 += Vec_IntSize(vArray) * (Vec_IntSize(vArray) - 1) / 2;
    }
 
    // add delay clauses
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        int e, iFanin;
        int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
        int iDelayVar0 = Vec_IntEntry( p->vDelayFirst, iObj );
        Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
        // check if the node has cuts containing only primary inputs
        int * pCut, * pList = Sle_ManList( p, iObj );
        Sle_ForEachCut( pList, pCut, i )
            if ( Sle_ManCutHasPisOnly(pCut, p->vMask) )
            {
                Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iDelayVar0, 0) ); // pos lit
//                Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iObj, 1), Abc_Var2Lit(iDelayVar0, 0) );
                value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                assert( value );
                break;
            }
//        if ( i < Sle_ListCutNum(pList) )
//            continue;
        // create delay requirements for each cut fanin of this node
        Vec_IntForEachEntry( vCutFans, iFanin, e )
        {
            int d, iDelayVarIn = Vec_IntEntry( p->vDelayFirst, iFanin );
            for ( d = 0; d < p->nLevels; d++ )
            {
                Vec_IntClear( p->vLits );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iFanin, 1) );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iEdgeVar0 + e, 0) );
                if ( d < p->nLevels-1 )
                    Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVar0 + d+1, 0) );
                value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                assert( value );
 
                Vec_IntClear( p->vLits );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iFanin, 1) );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) );
                if ( d < p->nLevels-1 )
                    Vec_IntPush( p->vLits, Abc_Var2Lit(iEdgeVar0 + e, 1) );
                Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVar0 + d, 0) );
                value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
                assert( value );
            }
            p->nDelayClas += 2*p->nLevels;
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManDeriveInit()

void Sle_ManDeriveInit ( Sle_Man_t * p )

Definition at line 555 of file giaSatLE.c.

{
    Vec_Int_t * vEdges;
    int i, iObj, iFanin, iEdge;
    if ( !Gia_ManHasMapping(p->pGia) )
        return;
    // derive initial state
    Vec_IntClear( p->vPolars );
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        int nFanins, * pFanins, * pCut, * pList, iFound = -1;
        if ( !Gia_ObjIsLut(p->pGia, iObj) )
            continue;
        Vec_IntPush( p->vPolars, iObj ); // node var
        nFanins = Gia_ObjLutSize( p->pGia, iObj );
        pFanins = Gia_ObjLutFanins( p->pGia, iObj );
        // find cut
        pList = Sle_ManList( p, iObj );
        Sle_ForEachCut( pList, pCut, i )
            if ( Sle_ManCheckContained( Sle_CutLeaves(pCut), Sle_CutSize(pCut), pFanins, nFanins ) )
            {
                iFound = i;
                break;
            }
        if ( iFound == -1 )
        {
            printf( "Cannot find the following cut at node %d: {", iObj );
            for ( i = 0; i < nFanins; i++ )
                printf( " %d", pFanins[i] );
            printf( " }\n" );
            Sle_ManPrintCuts( p->pGia, p->vCuts, iObj );
            fflush( stdout );
        }
        assert( iFound >= 0 );
        Vec_IntPush( p->vPolars, Vec_IntEntry(p->vCutFirst, iObj) + iFound ); // cut var
        // check if the cut contains only primary inputs - if so, its delay is equal to 1
        if ( Sle_ManCutHasPisOnly(pCut, p->vMask) )
            Vec_IntPush( p->vPolars, Vec_IntEntry(p->vDelayFirst, iObj) ); // delay var
    }
    Vec_IntSort( p->vPolars, 0 );
    // find zero-delay edges
    if ( !p->pGia->vEdge1 )
        return;
    vEdges = Gia_ManEdgeToArray( p->pGia );
    Vec_IntForEachEntryDouble( vEdges, iFanin, iObj, i )
    {
        assert( iFanin < iObj );
        assert( Gia_ObjIsLut(p->pGia, iFanin) );
        assert( Gia_ObjIsLut(p->pGia, iObj) );
        assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) );
        assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) );
        // find edge
        iEdge = Vec_IntFind( Vec_WecEntry(p->vCutFanins, iObj), iFanin );
        if ( iEdge < 0 )
            continue;
        assert( iEdge >= 0 );
        Vec_IntPush( p->vPolars, Vec_IntEntry(p->vEdgeFirst, iObj) + iEdge ); // edge
    }
    Vec_IntFree( vEdges );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManDeriveResult()

void Sle_ManDeriveResult	(	Sle_Man_t *	p,
		Vec_Int_t *	vEdge2,
		Vec_Int_t *	vMapping )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 868 of file giaSatLE.c.

{
    Vec_Int_t * vMapTemp;
    int iObj;
    // create mapping
    Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        int i, iCut, iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj );
        int * pCut, * pCutThis = NULL, * pList = Sle_ManList( p, iObj );
        if ( !sat_solver_var_value(p->pSat, iObj) )
            continue;
        Sle_ForEachCut( pList, pCut, iCut )
            if ( sat_solver_var_value(p->pSat, iCutVar0 + iCut) )
            {
                assert( pCutThis == NULL );
                pCutThis = pCut;
            }
        assert( pCutThis != NULL );
        Vec_IntWriteEntry( vMapping, iObj, Vec_IntSize(vMapping) );
        Vec_IntPush( vMapping, Sle_CutSize(pCutThis) );
        for ( i = 0; i < Sle_CutSize(pCutThis); i++ )
            Vec_IntPush( vMapping, Sle_CutLeaves(pCutThis)[i] );
        Vec_IntPush( vMapping, iObj );
    }
    vMapTemp = p->pGia->vMapping;
    p->pGia->vMapping = vMapping;
    // collect edges
    Vec_IntClear( vEdge2 );
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        int i, iFanin, iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
        Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
        //int * pCut, * pList  = Sle_ManList( p, iObj );
        // int iCutVar0  = Vec_IntEntry( p->vCutFirst, iObj );
        if ( !sat_solver_var_value(p->pSat, iObj) )
            continue;
        //for ( i = 0; i < Sle_ListCutNum(pList); i++ )
        //    printf( "%d", sat_solver_var_value(p->pSat, iCutVar0 + i) );
        //printf( "\n" );
        Vec_IntForEachEntry( vCutFans, iFanin, i )
            if ( sat_solver_var_value(p->pSat, iFanin) && sat_solver_var_value(p->pSat, iEdgeVar0 + i) )
            {
                // verify edge
                int * pFanins = Gia_ObjLutFanins( p->pGia, iObj );
                int k, nFanins = Gia_ObjLutSize( p->pGia, iObj );
                for ( k = 0; k < nFanins; k++ )
                {
                    //printf( "%d ", pFanins[k] );
                    if ( pFanins[k] == iFanin )
                        break;
                }
                //printf( "\n" );
                if ( k == nFanins )
//                    printf( "Cannot find LUT with input %d at node %d.\n", iFanin, iObj );
                    continue;
                Vec_IntPushTwo( vEdge2, iFanin, iObj );
            }
    }
    p->pGia->vMapping = vMapTemp;
}

Here is the caller graph for this function:

◆ Sle_ManExplore()

void Sle_ManExplore	(	Gia_Man_t *	pGia,
		int	nBTLimit,
		int	DelayInit,
		int	fDynamic,
		int	fTwoEdges,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 941 of file giaSatLE.c.

{
    int fVeryVerbose = 0;
    abctime clk = Abc_Clock();
    Vec_Int_t * vEdges2  = Vec_IntAlloc(1000);
    Vec_Int_t * vMapping = Vec_IntAlloc(1000);
    int i, iLut, nConfs, status, Delay, iFirstVar;
    int DelayStart = (DelayInit || !Gia_ManHasMapping(pGia)) ? DelayInit : Gia_ManLutLevel(pGia, NULL);
    Sle_Man_t * p = Sle_ManAlloc( pGia, DelayStart, fVerbose );
    if ( fVerbose )
        printf( "Running solver with %d conflicts, %d initial delay, and %d edges. Dynamic constraints = %s.\n", nBTLimit, DelayInit, 1+fTwoEdges, fDynamic?"yes":"no" );
    Sle_ManMarkupVariables( p );
    if ( fVerbose )
        printf( "Vars:  Total = %d.  Node = %d. Cut = %d. Edge = %d. Delay = %d.\n", 
            p->nVarsTotal, p->nNodeVars, p->nCutVars, p->nEdgeVars, p->nDelayVars );
    Sle_ManDeriveInit( p );
    Sle_ManDeriveCnf( p, nBTLimit, fDynamic || fTwoEdges );
    if ( fVerbose )
        printf( "Clas:  Total = %d.  Cut = %d. Edge = %d. EdgeEx = %d. Delay = %d.\n", 
            sat_solver_nclauses(p->pSat), p->nCutClas, p->nEdgeClas, p->nEdgeClas2, p->nDelayClas );
    //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", NULL, NULL, 0 );
    for ( Delay = p->nLevels; Delay >= 0; Delay-- )
    {
        // we constrain COs, although it would be fine to constrain only POs
        if ( Delay < p->nLevels )
        {
            Gia_ManForEachCoDriverId( p->pGia, iLut, i )
                if ( Vec_BitEntry(p->vMask, iLut) ) // internal node
                {
                    iFirstVar = Vec_IntEntry( p->vDelayFirst, iLut );
                    if ( !sat_solver_push(p->pSat, Abc_Var2Lit(iFirstVar + Delay, 1)) )
                        break;
                }
            if ( i < Gia_ManCoNum(p->pGia) )
            {
                if ( fVerbose )
                {
                    printf( "Proved UNSAT for delay %d.  ", Delay );
                    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
                }
                break;
            }
        }
        // solve with assumptions
        //clk = Abc_Clock();
        nConfs = sat_solver_nconflicts( p->pSat );
        while ( 1 )
        {
            p->nSatCalls++;
            status = sat_solver_solve_internal( p->pSat );
            if ( status != l_True )
                break;
            if ( !Sle_ManAddEdgeConstraints(p, 1+fTwoEdges) )
                break;
        }
        nConfs = sat_solver_nconflicts( p->pSat ) - nConfs;
        if ( status == l_True )
        {
            if ( fVerbose )
            {
                int nNodes = 0, nEdges = 0;
                for ( i = 0; i < p->nNodeVars; i++ )
                    nNodes += sat_solver_var_value(p->pSat, i);
                for ( i = 0; i < p->nEdgeVars; i++ )
                    nEdges += sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + i);
                printf( "Solution with delay %2d, node count %5d, and edge count %5d exists. Conf = %8d.  ", Delay, nNodes, nEdges, nConfs );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            // save the result
            Sle_ManDeriveResult( p, vEdges2, vMapping );
            if ( fVeryVerbose )
            {
                printf( "Nodes:  " );
                for ( i = 0; i < p->nNodeVars; i++ )
                    if ( sat_solver_var_value(p->pSat, i) )
                        printf( "%d ", i );
                printf( "\n" );
                printf( "\n" );
 
                Vec_IntPrint( p->vCutFirst );
                printf( "Cuts:   " );
                for ( i = 0; i < p->nCutVars; i++ )
                    if ( sat_solver_var_value(p->pSat, p->nNodeVars + i) )
                        printf( "%d ", p->nNodeVars + i );
                printf( "\n" );
                printf( "\n" );
 
                Vec_IntPrint( p->vEdgeFirst );
                printf( "Edges:  " );
                for ( i = 0; i < p->nEdgeVars; i++ )
                    if ( sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + i) )
                        printf( "%d ", p->nNodeVars + p->nCutVars + i );
                printf( "\n" );
                printf( "\n" );
 
                Vec_IntPrint( p->vDelayFirst );
                printf( "Delays: " );
                for ( i = 0; i < p->nDelayVars; i++ )
                    if ( sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + p->nEdgeVars + i) )
                        printf( "%d ", p->nNodeVars + p->nCutVars + p->nEdgeVars + i );
                printf( "\n" );
                printf( "\n" );
            }
        }
        else
        {
            if ( fVerbose )
            {
                if ( status == l_False )
                    printf( "Proved UNSAT for delay %d. Conf = %8d.  ", Delay, nConfs );
                else
                    printf( "Resource limit reached for delay %d. Conf = %8d.  ", Delay, nConfs );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            break;
        }
    }
    if ( fVerbose )
        printf( "Clas:  Total = %d.  Cut = %d. Edge = %d. EdgeEx = %d. Delay = %d.  Calls = %d.\n", 
            sat_solver_nclauses(p->pSat), p->nCutClas, p->nEdgeClas, p->nEdgeClas2, p->nDelayClas, p->nSatCalls );
    if ( Vec_IntSize(vMapping) > 0 )
    {
        Gia_ManEdgeFromArray( p->pGia, vEdges2 );
        Vec_IntFree( vEdges2 );
        Vec_IntFreeP( &p->pGia->vMapping );
        p->pGia->vMapping = vMapping;
    }
    else
    {
        Vec_IntFree( vEdges2 );
        Vec_IntFree( vMapping );
    }
    Vec_IntFreeP( &p->pGia->vPacking );
    Sle_ManStop( p );
}

Here is the call graph for this function:

◆ Sle_ManInternalNodeMask()

Vec_Bit_t * Sle_ManInternalNodeMask ( Gia_Man_t * pGia )

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

Synopsis [Derive mask representing internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file giaSatLE.c.

{
    int iObj;
    Vec_Bit_t * vMask = Vec_BitStart( Gia_ManObjNum(pGia) );  
    Gia_ManForEachAndId( pGia, iObj )
        Vec_BitWriteEntry( vMask, iObj, 1 );
    return vMask;
}

Here is the caller graph for this function:

◆ Sle_ManMarkupVariables()

void Sle_ManMarkupVariables ( Sle_Man_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file giaSatLE.c.

{
    int iObj, Counter = Gia_ManObjNum(p->pGia);
    // node variables
    p->nNodeVars = Counter;
    // cut variables
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        Vec_IntWriteEntry( p->vCutFirst, iObj, Counter );
        Counter += Sle_ListCutNum( Sle_ManList(p, iObj) );
    }
    p->nCutVars = Counter - p->nNodeVars;
    // edge variables
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        Vec_IntWriteEntry( p->vEdgeFirst, iObj, Counter );
        Counter += Vec_IntSize( Vec_WecEntry(p->vCutFanins, iObj) );
    }
    p->nEdgeVars = Counter - p->nCutVars - p->nNodeVars;
    // delay variables
    Gia_ManForEachAndId( p->pGia, iObj )
    {
        Vec_IntWriteEntry( p->vDelayFirst, iObj, Counter );
        Counter += p->nLevels;
    }
    p->nDelayVars = Counter - p->nEdgeVars - p->nCutVars - p->nNodeVars;
    p->nVarsTotal = Counter;
}

Here is the caller graph for this function:

◆ Sle_ManPrintCut()

void Sle_ManPrintCut ( int * pCut )

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

Synopsis [Cut printing.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file giaSatLE.c.

{
    int nSize   = Sle_CutSize(pCut);
    int k, * pC = Sle_CutLeaves(pCut);
    printf( "{" );
    for ( k = 0; k < nSize; k++ )
        printf( " %d", pC[k] );
    printf( " }\n" );
}

Here is the caller graph for this function:

◆ Sle_ManPrintCuts()

void Sle_ManPrintCuts	(	Gia_Man_t *	p,
		Vec_Int_t *	vCuts,
		int	iObj )

Definition at line 296 of file giaSatLE.c.

{
    int i, * pCut;
    int * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) );
    printf( "Obj %3d\n", iObj );
    Sle_ForEachCut( pList, pCut, i )
        Sle_ManPrintCut( pCut );
    printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sle_ManPrintCutsAll()

void Sle_ManPrintCutsAll	(	Gia_Man_t *	p,
		Vec_Int_t *	vCuts )

Definition at line 305 of file giaSatLE.c.

{
    int iObj;
    Gia_ManForEachAndId( p, iObj )
        Sle_ManPrintCuts( p, vCuts, iObj );
}

Here is the call graph for this function:

◆ Sle_ManStop()

void Sle_ManStop ( Sle_Man_t * p )

Definition at line 470 of file giaSatLE.c.

{
    sat_solver_delete( p->pSat );
    Vec_BitFree( p->vMask );
    Vec_IntFree( p->vCuts );
    Vec_WecFree( p->vCutFanins );
    Vec_WecFree( p->vFanoutEdges );
    Vec_WecFree( p->vEdgeCuts );
    Vec_IntFree( p->vObjMap );
    Vec_IntFree( p->vCutFirst );
    Vec_IntFree( p->vEdgeFirst );
    Vec_IntFree( p->vDelayFirst );
    Vec_IntFree( p->vPolars );
    Vec_IntFree( p->vLits );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ Sle_ForEachCut

◆ Sle_ForEachCut1

Typedef Documentation

◆ Sle_Man_t

Function Documentation

◆ Sle_ManAddEdgeConstraints()

◆ Sle_ManAlloc()

◆ Sle_ManCollectCutFanins()

◆ Sle_ManCollectCutFaninsOne()

◆ Sle_ManComputeCuts()

◆ Sle_ManComputeCutsTest()

◆ Sle_ManComputeDelay()

◆ Sle_ManComputeDelayCut()

◆ Sle_ManComputeDelayOne()

◆ Sle_ManCutHasPisOnly()

◆ Sle_ManCutMerge()

◆ Sle_ManDeriveCnf()

◆ Sle_ManDeriveInit()

◆ Sle_ManDeriveResult()

◆ Sle_ManExplore()

◆ Sle_ManInternalNodeMask()

◆ Sle_ManMarkupVariables()

◆ Sle_ManPrintCut()

◆ Sle_ManPrintCuts()

◆ Sle_ManPrintCutsAll()

◆ Sle_ManStop()