sbdInt.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 "misc/util/utilNam.h"
#include "misc/util/utilTruth.h"
#include "map/scl/sclLib.h"
#include "map/scl/sclCon.h"
#include "bool/kit/kit.h"
#include "misc/st/st.h"
#include "map/mio/mio.h"
#include "base/abc/abc.h"
#include "sbd.h"

Include dependency graph for sbdInt.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Sbd_Str_t_

Macros
#define	SBD_SAT_UNDEC   0x1234567812345678
	INCLUDES ///.
#define	SBD_SAT_SAT   0x8765432187654321
#define	SBD_LUTS_MAX   2
#define	SBD_SIZE_MAX   4
#define	SBD_DIV_MAX   10
#define	SBD_FVAR_MAX   100

Typedefs
typedef struct Sbd_Sto_t_	Sbd_Sto_t
	BASIC TYPES ///.
typedef struct Sbd_Srv_t_	Sbd_Srv_t
typedef struct Sbd_Str_t_	Sbd_Str_t

Functions
Sbd_Sto_t *	Sbd_StoAlloc (Gia_Man_t *pGia, Vec_Int_t *vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose)
	MACRO DEFINITIONS ///.
void	Sbd_StoFree (Sbd_Sto_t *p)
int	Sbd_StoObjRefs (Sbd_Sto_t *p, int iObj)
void	Sbd_StoRefObj (Sbd_Sto_t *p, int iObj, int iMirror)
void	Sbd_StoDerefObj (Sbd_Sto_t *p, int iObj)
void	Sbd_StoComputeCutsConst0 (Sbd_Sto_t *p, int iObj)
void	Sbd_StoComputeCutsObj (Sbd_Sto_t *p, int iObj, int Delay, int Level)
void	Sbd_StoComputeCutsCi (Sbd_Sto_t *p, int iObj, int Delay, int Level)
int	Sbd_StoComputeCutsNode (Sbd_Sto_t *p, int iObj)
void	Sbd_StoSaveBestDelayCut (Sbd_Sto_t *p, int iObj, int *pCut)
int	Sbd_StoObjBestCut (Sbd_Sto_t *p, int iObj, int nSize, int *pLeaves)
Sbd_Srv_t *	Sbd_ManCutServerStart (Gia_Man_t *pGia, Vec_Int_t *vMirrors, Vec_Int_t *vLutLevs, Vec_Int_t *vLevs, Vec_Int_t *vRefs, int nLutSize, int nCutSize, int nCutNum, int fVerbose)
	FUNCTION DEFINITIONS ///.
void	Sbd_ManCutServerStop (Sbd_Srv_t *p)
int	Sbd_ManCutServerFirst (Sbd_Srv_t *p, int iObj, int *pLeaves)
word	Sbd_ManSolve (sat_solver *pSat, int PivotVar, int FreeVar, Vec_Int_t *vDivSet, Vec_Int_t *vDivVars, Vec_Int_t *vDivValues, Vec_Int_t *vTemp)
sat_solver *	Sbd_ManSatSolver (sat_solver *pSat, Gia_Man_t *p, Vec_Int_t *vMirrors, int Pivot, Vec_Int_t *vWinObjs, Vec_Int_t *vObj2Var, Vec_Int_t *vTfo, Vec_Int_t *vRoots, int fQbf)
	DECLARATIONS ///.
int	Sbd_ManCollectConstants (sat_solver *pSat, int nCareMints[2], int PivotVar, word *pVarSims[], Vec_Int_t *vInds)
int	Sbd_ManCollectConstantsNew (sat_solver *pSat, Vec_Int_t *vDivVars, int nConsts, int PivotVar, word *pOnset, word *pOffset)
Vec_Bit_t *	Sbc_ManCriticalPath (Gia_Man_t *p)
int	Sbd_ProblemSolve (Gia_Man_t *p, Vec_Int_t *vMirrors, int Pivot, Vec_Int_t *vWinObjs, Vec_Int_t *vObj2Var, Vec_Int_t *vTfo, Vec_Int_t *vRoots, Vec_Int_t *vDivSet, int nStrs, Sbd_Str_t *pStr0)

Macro Definition Documentation

SBD_DIV_MAX

#define SBD_DIV_MAX   10

Definition at line 57 of file sbdInt.h.

SBD_FVAR_MAX

#define SBD_FVAR_MAX   100

Definition at line 58 of file sbdInt.h.

SBD_LUTS_MAX

#define SBD_LUTS_MAX   2

Definition at line 55 of file sbdInt.h.

SBD_SAT_SAT

#define SBD_SAT_SAT   0x8765432187654321

Definition at line 53 of file sbdInt.h.

SBD_SAT_UNDEC

#define SBD_SAT_UNDEC   0x1234567812345678

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 52 of file sbdInt.h.

SBD_SIZE_MAX

#define SBD_SIZE_MAX   4

Definition at line 56 of file sbdInt.h.

Typedef Documentation

Sbd_Srv_t

typedef struct Sbd_Srv_t_ Sbd_Srv_t

Definition at line 65 of file sbdInt.h.

Sbd_Sto_t

typedef struct Sbd_Sto_t_ Sbd_Sto_t

BASIC TYPES ///.

Definition at line 64 of file sbdInt.h.

Sbd_Str_t

typedef struct Sbd_Str_t_ Sbd_Str_t

Definition at line 67 of file sbdInt.h.

Function Documentation

Sbc_ManCriticalPath()

Vec_Bit_t * Sbc_ManCriticalPath ( Gia_Man_t * p )

extern

Definition at line 119 of file sbdPath.c.

{
    int * pLevels = NULL, k, iDriver, Slack = 1;
    int nLevels = p->pManTime ? Gia_ManLutLevelWithBoxes(p) : Gia_ManLutLevel(p, &pLevels);
    Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
    if ( p->pManTime )
        pLevels = Vec_IntArray( p->vLevels );
    Gia_ManIncrementTravId( p );
    Gia_ManForEachCoDriverId( p, iDriver, k )
        if ( (pLevels[iDriver] == nLevels) && iDriver )
            Sbc_ManCriticalPath_rec( p, pLevels, iDriver, pLevels[iDriver], vPath, Slack );
    if ( !p->pManTime )
        ABC_FREE( pLevels );
    Sbc_ManAddInternalToPath( p, vPath );
    return vPath;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_ManCollectConstants()

int Sbd_ManCollectConstants ( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds )

extern

Definition at line 411 of file sbdWin.c.

{
    int nBTLimit = 0;
    int i, Ind; 
    assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] );
    Vec_IntForEachEntry( vInds, Ind, i )
    {
        int fOffSet = (int)(i < nCareMints[0]);
        int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet );
        sat_solver_random_polarity( pSat );
        status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return -2;
        if ( status == l_False )
            return fOffSet;
        for ( k = 0; k <= PivotVar; k++ )
            if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) )
                Abc_TtXorBit(pVarSims[k], Ind);
    }
    return -1;
}

Here is the caller graph for this function:

Sbd_ManCollectConstantsNew()

int Sbd_ManCollectConstantsNew ( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset )

extern

Definition at line 433 of file sbdWin.c.

{
    int nBTLimit = 0;
    int n, i, k, status, iLit, iVar; 
    word * pPats[2] = {pOnset, pOffset};
    assert( Vec_IntSize(vDivVars) < 64 );
    for ( n = 0; n < 2; n++ )
    for ( i = 0; i < nConsts; i++ )
    {
        sat_solver_random_polarity( pSat );
        iLit = Abc_Var2Lit( PivotVar, n );
        status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return -2;
        if ( status == l_False )
            return n;
        pPats[n][i] = ((word)!n) << Vec_IntSize(vDivVars);
        Vec_IntForEachEntry( vDivVars, iVar, k )
            if ( sat_solver_var_value(pSat, iVar) )
                Abc_TtXorBit(&pPats[n][i], k);
    }
    return -1;
}

Here is the caller graph for this function:

Sbd_ManCutServerFirst()

int Sbd_ManCutServerFirst ( Sbd_Srv_t * p, int iObj, int * pLeaves )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file sbdCut2.c.

{
    int RetValue, LevStop = Vec_IntEntry(p->vLutLevs, iObj) - 2;
 
    Vec_IntClear( p->vCut );
    Gia_ManIncrementTravId( p->pGia );
    RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop, p->vLutLevs, p->vCut );
    if ( RetValue == 0 ) // cannot build delay-improving cut
        return -1;
    // check if the current cut is good
    Vec_IntSort( p->vCut, 0 );
/*
    Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
    if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
    {
        //printf( "%d ", Vec_IntSize(p->vCut) );
        memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
        return Vec_IntSize(p->vCut);
    }
*/
    // try to expand the cut
    Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
    Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
    if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
    {
        //printf( "1=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
        //printf( "%d ", Vec_IntSize(p->vCut) );
        memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
        return Vec_IntSize(p->vCut);
    }
 
    // try to reduce the topmost
    Vec_IntClear( p->vCut0 );
    Vec_IntAppend( p->vCut0, p->vCut );
    if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
    {
        Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
        Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
        assert( Vec_IntSize(p->vCut) <= p->nCutSize );
        if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
        {
            //printf( "%d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
            memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
            return Vec_IntSize(p->vCut);
        }
        // try again
        if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
        {
            Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
            Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
            assert( Vec_IntSize(p->vCut) <= p->nCutSize );
            if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
            {
                //printf( "* %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
                memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
                return Vec_IntSize(p->vCut);
            }
            // try again
            if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
            {
                Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
                Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
                assert( Vec_IntSize(p->vCut) <= p->nCutSize );
                if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
                {
                    //printf( "** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
                    memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
                    return Vec_IntSize(p->vCut);
                }
                // try again
                if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
                {
                    Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
                    Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
                    assert( Vec_IntSize(p->vCut) <= p->nCutSize );
                    if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
                    {
                        //printf( "*** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
                        memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
                        return Vec_IntSize(p->vCut);
                    }
                }
            }
        }
    }
 
    // recompute the cut
    Vec_IntClear( p->vCut );
    Gia_ManIncrementTravId( p->pGia );
    RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop-1, p->vLutLevs, p->vCut );
    if ( RetValue == 0 ) // cannot build delay-improving cut
        return -1;
    // check if the current cut is good
    Vec_IntSort( p->vCut, 0 );
/*
    Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
    if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
    {
        //printf( "%d ", Vec_IntSize(p->vCut) );
        memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
        return Vec_IntSize(p->vCut);
    }
*/
    // try to expand the cut
    Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
    Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
    if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
    {
        //printf( "2=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
        //printf( "%d ", Vec_IntSize(p->vCut) );
        memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
        return Vec_IntSize(p->vCut);
    }
 
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_ManCutServerStart()

Sbd_Srv_t * Sbd_ManCutServerStart ( Gia_Man_t * pGia, Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, Vec_Int_t * vLevs, Vec_Int_t * vRefs, int nLutSize, int nCutSize, int nCutNum, int fVerbose )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file sbdCut2.c.

{
    Sbd_Srv_t * p;
    assert( nLutSize <= nCutSize );
    assert( nCutSize < SBD_CUT_NO_LEAF );
    assert( nCutSize > 1 && nCutSize <= SBD_MAX_CUTSIZE );
    assert( nCutNum > 1 && nCutNum < SBD_MAX_CUTNUM );
    p = ABC_CALLOC( Sbd_Srv_t, 1 );
    p->clkStart = Abc_Clock();
    p->nLutSize = nLutSize;
    p->nCutSize = nCutSize;
    p->nCutNum  = nCutNum;
    p->fVerbose = fVerbose;
    p->pGia     = pGia;
    p->vMirrors = vMirrors;
    p->vLutLevs = vLutLevs;
    p->vLevs    = vLevs;
    p->vRefs    = vRefs;
    p->vCut0    = Vec_IntAlloc( 100 );
    p->vCut     = Vec_IntAlloc( 100 );
    p->vCutTop  = Vec_IntAlloc( 100 );
    p->vCutBot  = Vec_IntAlloc( 100 );
    return p;
}

Here is the caller graph for this function:

Sbd_ManCutServerStop()

void Sbd_ManCutServerStop ( Sbd_Srv_t * p )

extern

Definition at line 110 of file sbdCut2.c.

{
    Vec_IntFree( p->vCut0 );
    Vec_IntFree( p->vCut );
    Vec_IntFree( p->vCutTop );
    Vec_IntFree( p->vCutBot );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Sbd_ManSatSolver()

sat_solver * Sbd_ManSatSolver ( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf )

extern

DECLARATIONS ///.

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

FileName [sbd.c]

SystemName [ABC: Logic synthesis and verification system.]

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

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Constructs SAT solver for the window.]

Description [The window for the pivot node (Pivot) is represented as a DFS ordered array of objects (vWinObjs) whose indexed in the array (which will be used as SAT variables) are given in array vObj2Var. The TFO nodes are listed as the last ones in vWinObjs. The root nodes are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots. If fQbf is 1, returns the instance meant for QBF solving. It is using the last variable (LastVar) as the placeholder for the second copy of the pivot node.]

SideEffects []

SeeAlso []

Definition at line 52 of file sbdWin.c.

{
    Gia_Obj_t * pObj;
    int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
    int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
    int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
    int LastVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
    //Vec_IntPrint( vWinObjs );
    //Vec_IntPrint( vTfo );
    //Vec_IntPrint( vRoots );
    // create SAT solver
    if ( pSat == NULL )
        pSat = sat_solver_new();
    else
        sat_solver_restart( pSat );
    sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX );
    // create constant 0 clause
    sat_solver_addclause( pSat, &iLit, &iLit + 1 );
    // add clauses for all nodes
    Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 )
    {
        pObj = Gia_ManObj( p, iObj );
        if ( Gia_ObjIsCi(pObj) )
            continue;
        assert( Gia_ObjIsAnd(pObj) );
        assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
        Node = Vec_IntEntry( vObj2Var, iObj );
        Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
        Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
        Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
        Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
        Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
        Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
        fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
        fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
        if ( Gia_ObjIsXor(pObj) )
            sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
        else
            sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
    }
    // add second clauses for the TFO
    Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart )
    {
        pObj = Gia_ManObj( p, iObj );
        assert( Gia_ObjIsAnd(pObj) );
        assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
        Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo);
        Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
        Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
        Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
        Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
        Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
        Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
        Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
        Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
        if ( fQbf )
        {
            Fan0 = Fan0 == PivotVar ? LastVar : Fan0;
            Fan1 = Fan1 == PivotVar ? LastVar : Fan1;
        }
        fCompl0 = Gia_ObjFaninC0(pObj) ^ (!fQbf && Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
        fCompl1 = Gia_ObjFaninC1(pObj) ^ (!fQbf && Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
        if ( Gia_ObjIsXor(pObj) )
            sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
        else
            sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
    }
    if ( Vec_IntSize(vRoots) > 0 )
    {
        // create XOR clauses for the roots
        int nVars = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo);
        Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) );
        Vec_IntForEachEntry( vRoots, iObj, i )
        {
            assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
            Node = Vec_IntEntry( vObj2Var, iObj );
            Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
            sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 );
        }
        // make OR clause for the last nRoots variables
        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
        Vec_IntFree( vFaninVars );
        if ( RetValue == 0 )
        {
            sat_solver_delete( pSat );
            return NULL;
        }
        assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX );
    }
    else if ( fQbf )
    {
        int n, pLits[2];
        for ( n = 0; n < 2; n++ )
        {
            pLits[0] = Abc_Var2Lit( PivotVar, n );
            pLits[1] = Abc_Var2Lit( LastVar, n );
            RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
            assert( RetValue );
        }
    }
    // finalize
    RetValue = sat_solver_simplify( pSat );
    if ( RetValue == 0 )
    {
        sat_solver_delete( pSat );
        return NULL;    
    }
    return pSat;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_ManSolve()

word Sbd_ManSolve ( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp )

extern

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

Synopsis [Solves one SAT problem.]

Description [Computes node function for PivotVar with fanins in vDivSet using don't-care represented in the SAT solver. Uses array vValues to return the values of the first Vec_IntSize(vValues) SAT variables in case the implementation of the node with the given fanins does not exist.]

SideEffects []

SeeAlso []

Definition at line 178 of file sbdWin.c.

{
    int nBTLimit = 0;
    word uCube, uTruth = 0;
    int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
    assert( FreeVar < sat_solver_nvars(pSat) );
    assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
    pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
    pLits[1] = Abc_Var2Lit( FreeVar, 0 );  // iNewLit
    while ( 1 ) 
    {
        // find onset minterm
        status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return SBD_SAT_UNDEC;
        if ( status == l_False )
            return uTruth;
        assert( status == l_True );
        // remember variable values
        Vec_IntForEachEntry( vDivVars, iVar, i )
            Vec_IntWriteEntry( vDivValues, i, 2*sat_solver_var_value(pSat, iVar) );
        // collect divisor literals
        Vec_IntClear( vTemp );
        Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
        Vec_IntForEachEntry( vDivSet, iVar, i )
            Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
        // check against offset
        status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            return SBD_SAT_UNDEC;
        if ( status == l_True )
            break;
        assert( status == l_False );
        // compute cube and add clause
        nFinal = sat_solver_final( pSat, &pFinal );
        uCube = ~(word)0;
        Vec_IntClear( vTemp );
        Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
        for ( i = 0; i < nFinal; i++ )
        {
            if ( pFinal[i] == pLits[0] )
                continue;
            Vec_IntPush( vTemp, pFinal[i] );
            iVar = Vec_IntFind( vDivSet, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
            uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
        }
        uTruth |= uCube;
        status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
        assert( status );
        nIter++;
    }
    assert( status == l_True );
    // store the counter-example
    Vec_IntForEachEntry( vDivVars, iVar, i )
        Vec_IntAddToEntry( vDivValues, i, sat_solver_var_value(pSat, iVar) );
 
    for ( i = 0; i < Vec_IntSize(vDivValues); i++ )
        Vec_IntAddToEntry( vDivValues, i, 0xC );
/*
    // reduce the counter example
    for ( n = 0; n < 2; n++ )
    {
        Vec_IntClear( vTemp );
        Vec_IntPush( vTemp, Abc_Var2Lit(PivotVar, n) ); // n = 0 => F = 1  (expanding offset against onset)
        for ( i = 0; i < Vec_IntSize(vValues); i++ )
            Vec_IntPush( vTemp, Abc_Var2Lit(i, !((Vec_IntEntry(vValues, i) >> n) & 1)) );
        status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
        assert( status == l_False );
        // compute cube and add clause
        nFinal = sat_solver_final( pSat, &pFinal );
        for ( i = 0; i < nFinal; i++ )
            if ( Abc_Lit2Var(pFinal[i]) != PivotVar )
                Vec_IntAddToEntry( vValues, Abc_Lit2Var(pFinal[i]), 1 << (n+2) );
    }
*/
    return SBD_SAT_SAT;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_ProblemSolve()

int Sbd_ProblemSolve ( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 )

extern

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

Synopsis [Solves QBF problem for the given window.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file sbdLut.c.

{
    extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
    
    int fVerbose = 0;
    abctime clk = Abc_Clock();
    Vec_Int_t * vLits    = Vec_IntAlloc( 100 );
    sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 );
    sat_solver * pSatQbf = sat_solver_new();
 
    int nVars      = Vec_IntSize( vDivSet );
    int nPars      = Sbd_ProblemCountParams( nStrs, pStr0 );
 
    int VarCecOut  = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
    int VarCecPar  = VarCecOut + nStrs;
 
    int VarQbfPar  = 0;
    int VarQbfFree = nPars;
 
    int pVarsCec[256];
    int pVarsQbf[256];
    int i, iVar, iLit, nIters;
    int RetValue = 0;
 
    assert( Vec_IntSize(vDivSet) <= SBD_DIV_MAX );
    assert( nVars + nStrs + nPars <= 256 );
 
    // collect CEC variables
    Vec_IntForEachEntry( vDivSet, iVar, i )
        pVarsCec[i] = iVar;
    for ( i = 0; i < nStrs; i++ )
        pVarsCec[nVars + i] = VarCecOut + i;
    for ( i = 0; i < nPars; i++ )
        pVarsCec[nVars + nStrs + i] = VarCecPar + i;
 
    // collect QBF variables
    for ( i = 0; i < nVars + nStrs; i++ )
        pVarsQbf[i] = -1;
    for ( i = 0; i < nPars; i++ )
        pVarsQbf[nVars + nStrs + i] = VarQbfPar + i;
 
    // add clauses to the CEC problem
    Sbd_ProblemAddClauses( pSatCec, nVars, nStrs, pVarsCec, pStr0 );
 
    // create QBF solver
    sat_solver_setnvars( pSatQbf, 1000 );
    Sbd_ProblemAddClausesInit( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 );
 
    // assume all parameter variables are 0
    Vec_IntClear( vLits );
    for ( i = 0; i < nPars; i++ )
        Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) );
    for ( nIters = 0; nIters < (1 << nVars); nIters++ )
    {
        // check if these parameters solve the problem
        int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
        if ( status == l_False ) // solution found
            break;
        assert( status == l_True );
 
        if ( fVerbose )
        {
            printf( "Iter %3d : ", nIters );
            for ( i = 0; i < nPars; i++ )
                printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) );
            printf( "    " );
        }
 
        Vec_IntClear( vLits );
        // create new QBF variables
        for ( i = 0; i < nVars + nStrs; i++ )
            pVarsQbf[i] = VarQbfFree++;
        // set their values
        Vec_IntForEachEntry( vDivSet, iVar, i )
        {
            iLit = Abc_Var2Lit( pVarsQbf[i], !sat_solver_var_value(pSatCec, iVar) );
            status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
            assert( status );
            if ( fVerbose )
                printf( "%d", sat_solver_var_value(pSatCec, iVar) );
        }
        iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) );
        status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
        assert( status );
        if ( fVerbose )
            printf( " %d\n", !sat_solver_var_value(pSatCec, VarCecOut) );
        // add clauses to the QBF problem
        if ( !Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ) )
            break; // solution does not exist
        // check if solution still exists
        status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 );
        if ( status == l_False ) // solution does not exist
            break;
        assert( status == l_True ); 
        // find the new values of parameters
        assert( Vec_IntSize(vLits) == 0 );
        for ( i = 0; i < nPars; i++ )
            Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, !sat_solver_var_value(pSatQbf, VarQbfPar + i)) );
    }
    if ( Vec_IntSize(vLits) > 0 )
    {
        //Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
        Sbd_ProblemCollectSolution( nStrs, pStr0, vLits );
        RetValue = 1;
    }
    sat_solver_delete( pSatCec );
    sat_solver_delete( pSatQbf );
    Vec_IntFree( vLits );
 
    if ( fVerbose )
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_StoAlloc()

Sbd_Sto_t * Sbd_StoAlloc ( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose )

extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Incremental cut computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 667 of file sbdCut.c.

{
    Sbd_Sto_t * p;
    assert( nLutSize <= nCutSize );
    assert( nCutSize < SBD_CUT_NO_LEAF );
    assert( nCutSize > 1 && nCutSize <= SBD_MAX_CUTSIZE );
    assert( nCutNum > 1 && nCutNum < SBD_MAX_CUTNUM );
    p = ABC_CALLOC( Sbd_Sto_t, 1 );
    p->clkStart = Abc_Clock();
    p->nLutSize = nLutSize;
    p->nCutSize = nCutSize;
    p->nCutNum  = nCutNum;
    p->fCutMin  = fCutMin;
    p->fVerbose = fVerbose;
    p->pGia     = pGia;
    p->vMirrors = vMirrors;
    p->vDelays  = Vec_IntStart( Gia_ManObjNum(pGia) );
    p->vLevels  = Vec_IntStart( Gia_ManObjNum(pGia) );
    p->vRefs    = Vec_IntAlloc( Gia_ManObjNum(pGia) );
    p->vCuts    = Vec_WecStart( Gia_ManObjNum(pGia) );
    p->vTtMem   = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL;
    return p;
}

Here is the caller graph for this function:

Sbd_StoComputeCutsCi()

void Sbd_StoComputeCutsCi ( Sbd_Sto_t * p, int iObj, int Delay, int Level )

extern

Definition at line 724 of file sbdCut.c.

{
    Sbd_StoComputeCutsObj( p, iObj, Delay, Level );
    Sbd_CutAddUnit( p, iObj );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_StoComputeCutsConst0()

void Sbd_StoComputeCutsConst0 ( Sbd_Sto_t * p, int iObj )

extern

Definition at line 719 of file sbdCut.c.

{
    Sbd_StoComputeCutsObj( p, iObj, 0, 0 );
    Sbd_CutAddZero( p, iObj );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_StoComputeCutsNode()

int Sbd_StoComputeCutsNode ( Sbd_Sto_t * p, int iObj )

extern

Definition at line 729 of file sbdCut.c.

{
    Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
    int Lev0 = Vec_IntEntry( p->vLevels, Gia_ObjFaninId0(pObj, iObj) );
    int Lev1 = Vec_IntEntry( p->vLevels, Gia_ObjFaninId1(pObj, iObj) );
    Sbd_StoComputeCutsObj( p, iObj, -1, 1 + Abc_MaxInt(Lev0, Lev1) );
    Sbd_StoMergeCuts( p, iObj );
    return Vec_IntEntry( p->vDelays, iObj );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_StoComputeCutsObj()

void Sbd_StoComputeCutsObj ( Sbd_Sto_t * p, int iObj, int Delay, int Level )

extern

Definition at line 702 of file sbdCut.c.

{
    if ( iObj < Vec_IntSize(p->vDelays) )
    {
        Vec_IntWriteEntry( p->vDelays, iObj, Delay );
        Vec_IntWriteEntry( p->vLevels, iObj, Level );
    }
    else
    {
        assert( iObj == Vec_IntSize(p->vDelays) );
        assert( iObj == Vec_IntSize(p->vLevels) );
        assert( iObj == Vec_WecSize(p->vCuts) );
        Vec_IntPush( p->vDelays, Delay );
        Vec_IntPush( p->vLevels, Level );
        Vec_WecPushLevel( p->vCuts );
    }
}

Here is the caller graph for this function:

Sbd_StoDerefObj()

void Sbd_StoDerefObj ( Sbd_Sto_t * p, int iObj )

extern

Definition at line 778 of file sbdCut.c.

{
    Gia_Obj_t * pObj;
    int Lit0m, Lit1m, Fan0, Fan1;
    return;
 
    pObj = Gia_ManObj(p->pGia, iObj);
    if ( Vec_IntEntry(p->vRefs, iObj) == 0 )
        printf( "Ref count mismatch at node %d\n", iObj );
    assert( Vec_IntEntry(p->vRefs, iObj) > 0 );
    Vec_IntAddToEntry( p->vRefs, iObj, -1 );
    if ( Vec_IntEntry( p->vRefs, iObj ) > 0 )
        return;
    if ( Gia_ObjIsCi(pObj) )
        return;
//printf( "Deref %d\n", iObj );
    assert( Gia_ObjIsAnd(pObj) );
    Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
    Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
    Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
    Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
    if ( Fan0 ) Sbd_StoDerefObj( p, Fan0 );
    if ( Fan1 ) Sbd_StoDerefObj( p, Fan1 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sbd_StoFree()

void Sbd_StoFree ( Sbd_Sto_t * p )

extern

Definition at line 690 of file sbdCut.c.

{
    Vec_IntFree( p->vDelays );
    Vec_IntFree( p->vLevels );
    Vec_IntFree( p->vRefs );
    Vec_WecFree( p->vCuts );
    if ( p->fCutMin )
        Vec_MemHashFree( p->vTtMem );
    if ( p->fCutMin )
        Vec_MemFree( p->vTtMem );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Sbd_StoObjBestCut()

int Sbd_StoObjBestCut ( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves )

extern

Definition at line 802 of file sbdCut.c.

{
    int fVerbose = 0;
    Sbd_Cut_t * pCutBest = NULL;   int i;
    assert( p->Pivot == iObj );
    if ( fVerbose && iObj % 1000 == 0 )
        printf( "Node %6d : \n", iObj );
    for ( i = 0; i < p->nCutsR; i++ )
    {
        if ( fVerbose && iObj % 1000 == 0 )
            Sbd_CutPrint( p, iObj, p->ppCuts[i] );
        if ( nSize && (int)p->ppCuts[i]->nLeaves != nSize )
            continue;
        if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize && 
             (int)p->ppCuts[i]->nSlowLeaves <= 1 &&
             (int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 &&
             (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
            pCutBest = p->ppCuts[i];
    }
    if ( fVerbose && iObj % 1000 == 0 )
    {
        printf( "Best cut of size %d:\n", nSize );
        Sbd_CutPrint( p, iObj, pCutBest );
    }
    if ( pCutBest == NULL )
        return -1;
    assert( pCutBest->nLeaves <= SBD_DIV_MAX );
    for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
        pLeaves[i] = pCutBest->pLeaves[i];
    return pCutBest->nLeaves;
}

Here is the caller graph for this function:

Sbd_StoObjRefs()

int Sbd_StoObjRefs ( Sbd_Sto_t * p, int iObj )

extern

Definition at line 746 of file sbdCut.c.

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

Sbd_StoRefObj()

void Sbd_StoRefObj ( Sbd_Sto_t * p, int iObj, int iMirror )

extern

Definition at line 750 of file sbdCut.c.

{
    Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
    assert( iObj == Vec_IntSize(p->vRefs) );
    assert( iMirror < iObj );
    Vec_IntPush( p->vRefs, 0 );
//printf( "Ref %d\n", iObj );
    if ( iMirror > 0 )
    {
        Vec_IntWriteEntry( p->vRefs, iObj, Vec_IntEntry(p->vRefs, iMirror) );
        Vec_IntWriteEntry( p->vRefs, iMirror, 1 );
    }
    if ( Gia_ObjIsAnd(pObj) )
    {
        int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
        int Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
        int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
        int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
        Vec_IntAddToEntry( p->vRefs, Fan0, 1 );
        Vec_IntAddToEntry( p->vRefs, Fan1, 1 );
    }
    else if ( Gia_ObjIsCo(pObj) )
    {
        int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
        assert( Lit0m == -1 );
        Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
    }
}

Here is the caller graph for this function:

Sbd_StoSaveBestDelayCut()

void Sbd_StoSaveBestDelayCut ( Sbd_Sto_t * p, int iObj, int * pCut )

extern

Definition at line 738 of file sbdCut.c.

{
    Sbd_Cut_t * pCutBest = p->ppCuts[p->iCutBest]; int i;
    assert( iObj == p->Pivot );
    pCut[0] = pCutBest->nLeaves;
    for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
        pCut[i+1] = pCutBest->pLeaves[i];
}

Here is the caller graph for this function: