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

Include dependency graph for giaSatEdge.c:

Classes
struct	Seg_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Seg_Man_t_	Seg_Man_t
	DECLARATIONS ///.

Functions
sat_solver *	Sbm_AddCardinSolver (int LogN, Vec_Int_t **pvVars)

Vec_Int_t *	Seg_ManCountIntEdges (Gia_Man_t p, Vec_Int_t vPolars, Vec_Int_t *vToSkip, int nFanouts)
	FUNCTION DEFINITIONS ///.

Vec_Wec_t *	Seg_ManCollectObjEdges (Vec_Int_t *vEdges, int nObjs)

int	Seg_ManCountIntLevels (Seg_Man_t *p, int iStartVar)

Seg_Man_t *	Seg_ManAlloc (Gia_Man_t *pGia, int nFanouts)

void	Seg_ManClean (Seg_Man_t *p)

void	Seg_ManStop (Seg_Man_t *p)

void	Seg_ManCreateCnf (Seg_Man_t *p, int fTwo, int fVerbose)

Vec_Int_t *	Seg_ManConvertResult (Seg_Man_t *p)

void	Seg_ManComputeDelay (Gia_Man_t *pGia, int DelayInit, int nFanouts, int fTwo, int fVerbose)

Typedef Documentation

◆ Seg_Man_t

typedef typedefABC_NAMESPACE_IMPL_START struct Seg_Man_t_ Seg_Man_t

DECLARATIONS ///.

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

FileName [giaSatEdge.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 32 of file giaSatEdge.c.

Function Documentation

◆ Sbm_AddCardinSolver()

sat_solver * Sbm_AddCardinSolver	(	int	LogN,
		Vec_Int_t **	pvVars )

extern

Definition at line 456 of file giaSatMap.c.

{
    int nVars = 1 << LogN;
    int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1), nVarsReal;
    Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
    sat_solver * pSat = sat_solver_new();
    sat_solver_setnvars( pSat, nVarsAlloc );
    nVarsReal = Sbm_AddCardinConstrPairWise( pSat, vVars, 2 );
    assert( nVarsReal == nVarsAlloc );
    *pvVars = vVars;
    return pSat;
}

Here is the call graph for this function:

◆ Seg_ManAlloc()

Seg_Man_t * Seg_ManAlloc	(	Gia_Man_t *	pGia,
		int	nFanouts )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file giaSatEdge.c.

{
    int nVarsAll;
    Seg_Man_t * p = ABC_CALLOC( Seg_Man_t, 1 );
    p->vPolars    = Vec_IntAlloc( 1000 ); 
    p->vToSkip    = Vec_IntAlloc( 1000 ); 
    p->vEdges     = Seg_ManCountIntEdges( pGia, p->vPolars, p->vToSkip, nFanouts );
    p->nVars      = Vec_IntSize(p->vEdges)/2;
    p->LogN       = Abc_Base2Log(p->nVars);
    p->Power2     = 1 << p->LogN;
    //p->pSat       = Sbm_AddCardinSolver( p->LogN, &p->vCardVars );
    p->pSat       = sat_solver_new();
    sat_solver_setnvars( p->pSat, p->nVars );
    p->FirstVar   = sat_solver_nvars( p->pSat );
    sat_solver_bookmark( p->pSat );
    p->pGia       = pGia;
    // internal
    p->vFirsts    = Vec_IntAlloc( 0 ); 
    p->vNvars     = Vec_IntAlloc( 0 ); 
    p->vLits      = Vec_IntAlloc( 0 ); 
    nVarsAll      = Seg_ManCountIntLevels( p, p->FirstVar );
    sat_solver_setnvars( p->pSat, nVarsAll );
    // other
    Gia_ManFillValue( pGia );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Seg_ManClean()

void Seg_ManClean ( Seg_Man_t * p )

Definition at line 181 of file giaSatEdge.c.

{
    p->timeStart = Abc_Clock();
    sat_solver_rollback( p->pSat );
    sat_solver_bookmark( p->pSat );
    // internal
    Vec_IntClear( p->vEdges );
    Vec_IntClear( p->vFirsts );
    Vec_IntClear( p->vNvars );
    Vec_IntClear( p->vLits );
    Vec_IntClear( p->vPolars );
    Vec_IntClear( p->vToSkip );
    // other
    Gia_ManFillValue( p->pGia );
}

Here is the call graph for this function:

◆ Seg_ManCollectObjEdges()

Vec_Wec_t * Seg_ManCollectObjEdges	(	Vec_Int_t *	vEdges,
		int	nObjs )

Definition at line 102 of file giaSatEdge.c.

{
    int iFanin, iObj, i;
    Vec_Wec_t * vRes = Vec_WecStart( nObjs );
    Vec_IntForEachEntryDouble( vEdges, iFanin, iObj, i )
    {
        Vec_WecPush( vRes, iFanin, i/2 );
        Vec_WecPush( vRes, iObj, i/2 );
    }
    return vRes;
}

Here is the caller graph for this function:

◆ Seg_ManComputeDelay()

void Seg_ManComputeDelay	(	Gia_Man_t *	pGia,
		int	DelayInit,
		int	nFanouts,
		int	fTwo,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file giaSatEdge.c.

{
    int nBTLimit = 0;
    int nTimeOut = 0;
    int fVeryVerbose = 0;
 
    Gia_Obj_t * pObj;
    abctime clk = Abc_Clock();
    Vec_Int_t * vEdges2 = NULL;
    int i, iLut, iFirst, nVars, status, Delay, nConfs;
    Seg_Man_t * p = Seg_ManAlloc( pGia, nFanouts );
    int DelayStart = DelayInit ? DelayInit : p->DelayMax;
 
    if ( fVerbose )
    printf( "Running SatEdge with starting delay %d and edge %d (edge vars %d, total vars %d)\n", 
        DelayStart, fTwo+1, p->FirstVar, sat_solver_nvars(p->pSat) );
    Seg_ManCreateCnf( p, fTwo, fVerbose );
    //Sat_SolverWriteDimacs( p->pSat, "test_edge.cnf", NULL, NULL, 0 );
    // set resource limits
    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->nVars );
    // increment delay gradually
    for ( Delay = p->DelayMax; Delay >= 0; Delay-- )
    {
        // we constrain COs, although it would be fine to constrain only POs
        Gia_ManForEachCoDriver( p->pGia, pObj, i )
        {
            iLut   = Gia_ObjId( p->pGia, pObj );
            iFirst = Vec_IntEntry( p->vFirsts, iLut );
            nVars  = Vec_IntEntry( p->vNvars, iLut );
            if ( Delay < nVars && !sat_solver_push(p->pSat, Abc_Var2Lit(iFirst + Delay, 1)) )
                break;
        }
        if ( i < Gia_ManCoNum(p->pGia) )
        {
            printf( "Proved UNSAT for delay %d.  ", Delay );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            break;
        }
        if ( Delay > DelayStart )
            continue;
        // solve with assumptions
        //clk = Abc_Clock();
        nConfs = sat_solver_nconflicts( p->pSat );
        status = sat_solver_solve_internal( p->pSat );
        nConfs = sat_solver_nconflicts( p->pSat ) - nConfs;
        if ( status == l_True )
        {
            if ( fVerbose )
            {
                int Count = 0;
                for ( i = 0; i < p->nVars; i++ )
                    Count += sat_solver_var_value(p->pSat, i);
                printf( "Solution with delay %2d and %5d edges exists. Conf = %8d.  ", Delay, Count, nConfs );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            // save the result
            Vec_IntFreeP( &vEdges2 );
            vEdges2 = Seg_ManConvertResult( p );
            if ( fVeryVerbose )
            {
                for ( i = 0; i < p->nVars; i++ )
                    printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
                printf( "   " );
 
                for ( i = p->nVars; i < sat_solver_nvars(p->pSat); i++ )
                    printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
                printf( "\n" );
            }
        }
        else
        {
            if ( fVerbose )
            {
                if ( status == l_False )
                    printf( "Proved UNSAT for delay %d.  ", Delay );
                else
                    printf( "Resource limit reached for delay %d.  ", Delay );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            break;
        }
    }
    Gia_ManEdgeFromArray( p->pGia, vEdges2 );
    Vec_IntFreeP( &vEdges2 );
    Seg_ManStop( p );
}

Here is the call graph for this function:

◆ Seg_ManConvertResult()

Vec_Int_t * Seg_ManConvertResult ( Seg_Man_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 418 of file giaSatEdge.c.

{
    int iFanin, iObj, i;
    Vec_Int_t * vEdges2 = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntryDouble( p->vEdges, iFanin, iObj, i )
        if ( sat_solver_var_value(p->pSat, i/2) )
            Vec_IntPushTwo( vEdges2, iFanin, iObj );
    return vEdges2;
}

Here is the caller graph for this function:

◆ Seg_ManCountIntEdges()

Vec_Int_t * Seg_ManCountIntEdges	(	Gia_Man_t *	p,
		Vec_Int_t *	vPolars,
		Vec_Int_t *	vToSkip,
		int	nFanouts )

FUNCTION DEFINITIONS ///.

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

Synopsis [Count the number of edges between internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file giaSatEdge.c.

{
    int i, iLut, iFanin;
    Vec_Int_t * vEdges = Vec_IntAlloc( 1000 );
    assert( Gia_ManHasMapping(p) );
    Vec_IntClear( vPolars );
    Vec_IntClear( vToSkip );
    if ( nFanouts )
        Gia_ManSetLutRefs( p );
    Gia_ManForEachLut( p, iLut )
        Gia_LutForEachFanin( p, iLut, iFanin, i )
            if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) )
            {
                if ( p->vEdge1 && Gia_ObjCheckEdge(p, iFanin, iLut) )
                    Vec_IntPush( vPolars, Vec_IntSize(vEdges)/2 );
                if ( nFanouts && Gia_ObjLutRefNumId(p, iFanin) >= nFanouts )
                    Vec_IntPush( vToSkip, Vec_IntSize(vEdges)/2 );
                Vec_IntPushTwo( vEdges, iFanin, iLut );
            }
    if ( nFanouts )
        ABC_FREE( p->pLutRefs );
    return vEdges;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Seg_ManCountIntLevels()

int Seg_ManCountIntLevels	(	Seg_Man_t *	p,
		int	iStartVar )

Definition at line 113 of file giaSatEdge.c.

{
    Gia_Obj_t * pObj;
    int iLut, nVars;
    Vec_IntFill( p->vFirsts, Gia_ManObjNum(p->pGia), -1 );
    Vec_IntFill( p->vNvars,  Gia_ManObjNum(p->pGia), 0 );
    ABC_FREE( p->pLevels );
    if ( p->pGia->pManTime )
    {
        p->DelayMax = Gia_ManLutLevelWithBoxes( p->pGia );
        p->pLevels = Vec_IntReleaseArray( p->pGia->vLevels );
        Vec_IntFreeP( &p->pGia->vLevels );
    }
    else
        p->DelayMax = Gia_ManLutLevel( p->pGia, &p->pLevels );
    Gia_ManForEachObj1( p->pGia, pObj, iLut )
    {
        if ( Gia_ObjIsCo(pObj) )
            continue;
        if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsLut(p->pGia, iLut) )
            continue;
        assert( Gia_ObjIsCi(pObj) || Gia_ObjIsLut(p->pGia, iLut) );
        Vec_IntWriteEntry( p->vFirsts, iLut, iStartVar );
        //assert( p->pLevels[iLut] > 0 );
        nVars = p->pLevels[iLut] < 2 ? 0 : p->pLevels[iLut];
        Vec_IntWriteEntry( p->vNvars,  iLut, nVars );
        iStartVar += nVars;
    }
    return iStartVar;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Seg_ManCreateCnf()

void Seg_ManCreateCnf	(	Seg_Man_t *	p,
		int	fTwo,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file giaSatEdge.c.

{
    Tim_Man_t * pTim = (Tim_Man_t *)p->pGia->pManTime;
    Gia_Obj_t * pObj;
    Vec_Wec_t * vObjEdges;
    Vec_Int_t * vLevel;
    int iLut, iFanin, iFirst;
    int pLits[3], Count = 0;
    int i, k, nVars, Edge, value;
    abctime clk = Abc_Clock();
    // edge delay constraints
    int nConstr = sat_solver_nclauses(p->pSat);
    Gia_ManForEachObj( p->pGia, pObj, iLut )
    {
        int iFirstLut = Vec_IntEntry( p->vFirsts, iLut );
        int nVarsLut  = Vec_IntEntry( p->vNvars, iLut );
        if ( pTim && Gia_ObjIsCi(pObj) )
        {
            int iBox = Tim_ManBoxForCi( pTim, Gia_ObjCioId(pObj) );
            if ( nVarsLut > 0 && iBox >= 0 )
            {
                int iCiId = Tim_ManBoxOutputFirst( pTim, iBox );
                if ( iCiId == Gia_ObjCioId(pObj) ) // first input
                {
                    int nIns = Tim_ManBoxInputNum( pTim, iBox );
                    int iIn0 = Tim_ManBoxInputFirst( pTim, iBox );
                    for ( i = 0; i < nIns-1; i++ ) // skip carry-in pin
                    {
                        Gia_Obj_t * pOut = Gia_ManCo( p->pGia, iIn0+i );
                        int iDriverId = Gia_ObjFaninId0p( p->pGia, pOut );
                        int AddOn;
 
                        iFirst = Vec_IntEntry( p->vFirsts, iDriverId );
                        nVars  = Vec_IntEntry( p->vNvars, iDriverId );
                        assert( nVars < nVarsLut );
                        AddOn = (int)(nVars < nVarsLut);
                        for ( k = 0; k < nVars; k++ )
                        {
                            pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                            pLits[1] = Abc_Var2Lit( iFirstLut+k+AddOn, 0 );
                            value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                            assert( value );
                        }
                    }
                }
                else // intermediate input
                {
                    Gia_Obj_t * pIn = Gia_ManCi( p->pGia, iCiId );
                    int iObjId = Gia_ObjId( p->pGia, pIn );
 
                    iFirst = Vec_IntEntry( p->vFirsts, iObjId );
                    nVars  = Vec_IntEntry( p->vNvars, iObjId );
                    if ( nVars > 0 )
                    {
                        for ( k = 0; k < nVars; k++ )
                        {
                            pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                            pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
                            value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                            assert( value );
                        }
                    }
                }
            }
            continue;
        }
        if ( !Gia_ObjIsLut(p->pGia, iLut) )
            continue;
        Gia_LutForEachFanin( p->pGia, iLut, iFanin, i )
            if ( pTim && Gia_ObjIsCi(Gia_ManObj(p->pGia, iFanin)) )
            {
                iFirst = Vec_IntEntry( p->vFirsts, iFanin );
                nVars  = Vec_IntEntry( p->vNvars, iFanin );
                assert( nVars <= nVarsLut );
                if ( nVars > 0 )
                {
                    for ( k = 0; k < nVars; k++ )
                    {
                        pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                        pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
                        value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                        assert( value );
                    }
                }
            }
            else if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) )
            {
                iFirst = Vec_IntEntry( p->vFirsts, iFanin );
                nVars  = Vec_IntEntry( p->vNvars, iFanin );
                assert( nVars != 1 && nVars < nVarsLut );
                // add initial
                if ( nVars == 0 )
                {
                    pLits[0] = Abc_Var2Lit( Count, 1 );
                    pLits[1] = Abc_Var2Lit( iFirstLut, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                    assert( value );
 
                    pLits[0] = Abc_Var2Lit( Count, 0 );
                    pLits[1] = Abc_Var2Lit( iFirstLut+1, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                    assert( value );
                }
                // add others
                for ( k = 0; k < nVars; k++ )
                {
                    pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                    pLits[1] = Abc_Var2Lit( Count, 1 );
                    pLits[2] = Abc_Var2Lit( iFirstLut+k, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
                    assert( value );
 
                    pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                    pLits[1] = Abc_Var2Lit( Count, 0 );
                    pLits[2] = Abc_Var2Lit( iFirstLut+k+1, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
                    assert( value );
                }
                Count++;
            }
    }
    assert( Count == p->nVars );
    if ( fVerbose )
    printf( "Delay constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
    nConstr = sat_solver_nclauses(p->pSat);
/*
    // delay relationship constraints
    Vec_IntForEachEntryTwo( p->vFirsts, p->vNvars, iFirst, nVars, iLut )
    {
        if ( nVars < 2 )
            continue;
        for ( i = 1; i < nVars; i++ )
        {
            pLits[0] = Abc_Var2Lit( iFirst + i - 1, 1 );
            pLits[1] = Abc_Var2Lit( iFirst + i,     0 );
            value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
            assert( value );
        }
    }
*/
    // edge compatibility constraint
    vObjEdges = Seg_ManCollectObjEdges( p->vEdges, Gia_ManObjNum(p->pGia) );
    Vec_WecForEachLevel( vObjEdges, vLevel, i )
    {
        int v1, v2, v3, Var1, Var2, Var3;
        if ( (!fTwo && Vec_IntSize(vLevel) >= 2) || (fTwo && Vec_IntSize(vLevel) > 10) )
        {
            Vec_IntForEachEntry( vLevel, Var1, v1 )
            Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 )
            {
                pLits[0] = Abc_Var2Lit( Var1, 1 );
                pLits[1] = Abc_Var2Lit( Var2, 1 );
                value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                assert( value );
            }
        }
        else if ( fTwo && Vec_IntSize(vLevel) >= 3 )
        {
            Vec_IntForEachEntry( vLevel, Var1, v1 )
            Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 )
            Vec_IntForEachEntryStart( vLevel, Var3, v3, v2 + 1 )
            {
                pLits[0] = Abc_Var2Lit( Var1, 1 );
                pLits[1] = Abc_Var2Lit( Var2, 1 );
                pLits[2] = Abc_Var2Lit( Var3, 1 );
                value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
                assert( value );
            }
        }
    }
    Vec_WecFree( vObjEdges );
    // block forbidden edges
    Vec_IntForEachEntry( p->vToSkip, Edge, i )
    {
        pLits[0] = Abc_Var2Lit( Edge, 1 );
        value = sat_solver_addclause( p->pSat, pLits, pLits+1 );
        assert( value );
    }
    if ( fVerbose )
    printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
    if ( fVerbose )
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Seg_ManStop()

void Seg_ManStop ( Seg_Man_t * p )

Definition at line 196 of file giaSatEdge.c.

{
    sat_solver_delete( p->pSat );
    //Vec_IntFree( p->vCardVars );
    // internal
    Vec_IntFree( p->vEdges );
    Vec_IntFree( p->vFirsts );
    Vec_IntFree( p->vNvars );
    Vec_IntFree( p->vLits );
    Vec_IntFree( p->vPolars );
    Vec_IntFree( p->vToSkip );
    ABC_FREE( p->pLevels );
    // other
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Classes

Typedefs

Functions

Typedef Documentation

◆ Seg_Man_t

Function Documentation

◆ Sbm_AddCardinSolver()

◆ Seg_ManAlloc()

◆ Seg_ManClean()

◆ Seg_ManCollectObjEdges()

◆ Seg_ManComputeDelay()

◆ Seg_ManConvertResult()

◆ Seg_ManCountIntEdges()

◆ Seg_ManCountIntLevels()

◆ Seg_ManCreateCnf()

◆ Seg_ManStop()