dchInt.h File Reference

#include "aig/aig/aig.h"
#include "sat/bsat/satSolver.h"
#include "dch.h"

Go to the source code of this file.

Data Structures
struct	Dch_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Dch_Cla_t_	Dch_Cla_t
	INCLUDES ///. More...
typedef struct Dch_Man_t_	Dch_Man_t

Functions
static int	Dch_ObjSatNum (Dch_Man_t *p, Aig_Obj_t *pObj)
	MACRO DEFINITIONS ///. More...
static void	Dch_ObjSetSatNum (Dch_Man_t *p, Aig_Obj_t *pObj, int Num)
static Aig_Obj_t *	Dch_ObjFraig (Aig_Obj_t *pObj)
static void	Dch_ObjSetFraig (Aig_Obj_t *pObj, Aig_Obj_t *pNode)
static int	Dch_ObjIsConst1Cand (Aig_Man_t *pAig, Aig_Obj_t *pObj)
static void	Dch_ObjSetConst1Cand (Aig_Man_t *pAig, Aig_Obj_t *pObj)
int	Dch_DeriveChoiceCountReprs (Aig_Man_t *pAig)
	FUNCTION DECLARATIONS ///. More...
int	Dch_DeriveChoiceCountEquivs (Aig_Man_t *pAig)
Aig_Man_t *	Dch_DeriveChoiceAig (Aig_Man_t *pAig, int fSkipRedSupps)
Dch_Cla_t *	Dch_ClassesStart (Aig_Man_t *pAig)
void	Dch_ClassesSetData (Dch_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
void	Dch_ClassesStop (Dch_Cla_t *p)
int	Dch_ClassesLitNum (Dch_Cla_t *p)
Aig_Obj_t **	Dch_ClassesReadClass (Dch_Cla_t *p, Aig_Obj_t *pRepr, int *pnSize)
void	Dch_ClassesPrint (Dch_Cla_t *p, int fVeryVerbose)
void	Dch_ClassesPrepare (Dch_Cla_t *p, int fLatchCorr, int nMaxLevs)
int	Dch_ClassesRefine (Dch_Cla_t *p)
int	Dch_ClassesRefineOneClass (Dch_Cla_t *p, Aig_Obj_t *pRepr, int fRecursive)
void	Dch_ClassesCollectOneClass (Dch_Cla_t *p, Aig_Obj_t *pRepr, Vec_Ptr_t *vRoots)
void	Dch_ClassesCollectConst1Group (Dch_Cla_t *p, Aig_Obj_t *pObj, int nNodes, Vec_Ptr_t *vRoots)
int	Dch_ClassesRefineConst1Group (Dch_Cla_t *p, Vec_Ptr_t *vRoots, int fRecursive)
void	Dch_CnfNodeAddToSolver (Dch_Man_t *p, Aig_Obj_t *pObj)
Dch_Man_t *	Dch_ManCreate (Aig_Man_t *pAig, Dch_Pars_t *pPars)
	DECLARATIONS ///. More...
void	Dch_ManStop (Dch_Man_t *p)
void	Dch_ManSatSolverRecycle (Dch_Man_t *p)
int	Dch_NodesAreEquiv (Dch_Man_t *p, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
	DECLARATIONS ///. More...
Dch_Cla_t *	Dch_CreateCandEquivClasses (Aig_Man_t *pAig, int nWords, int fVerbose)
void	Dch_ManResimulateCex (Dch_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
void	Dch_ManResimulateCex2 (Dch_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
void	Dch_ManSweep (Dch_Man_t *p)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Dch_Cla_t_ Dch_Cla_t

INCLUDES ///.

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

FileName [dchInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 47 of file dchInt.h.

typedef struct Dch_Man_t_ Dch_Man_t

Definition at line 50 of file dchInt.h.

Function Documentation

void Dch_ClassesCollectConst1Group	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pObj,
		int	nNodes,
		Vec_Ptr_t *	vRoots
	)

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

Synopsis [Returns equivalence class of the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 546 of file dchClass.c.

{
    int i, Limit;
    Vec_PtrClear( vRoots );
    Limit = Abc_MinInt( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
    for ( i = pObj->Id; i < Limit; i++ )
    {
        pObj = Aig_ManObj( p->pAig, i );
        if ( pObj && Dch_ObjIsConst1Cand( p->pAig, pObj ) )
            Vec_PtrPush( vRoots, pObj );
    }
}

void Dch_ClassesCollectOneClass	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pRepr,
		Vec_Ptr_t *	vRoots
	)

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

Synopsis [Returns equivalence class of the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 525 of file dchClass.c.

{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrClear( vRoots );
    Dch_ClassForEachNode( p, pRepr, pObj, i )
        Vec_PtrPush( vRoots, pObj );
    assert( Vec_PtrSize(vRoots) > 1 ); 
}

int Dch_ClassesLitNum

(

Dch_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file dchClass.c.

{
    return p->nLits;
}

void Dch_ClassesPrepare	(	Dch_Cla_t *	p,
		int	fLatchCorr,
		int	nMaxLevs
	)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 336 of file dchClass.c.

{
    Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
    Aig_Obj_t * pObj, * pTemp, * pRepr;
    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;

    // allocate the hash table hashing simulation info into nodes
    nTableSize = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); 
    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 

    // add all the nodes to the hash table
    nEntries = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Aig_ObjIsCi(pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
                continue;
        }
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
        {
            Dch_ObjSetConst1Cand( p->pAig, pObj );
            p->nCands1++;
            continue;
        }
        // hash the node by its simulation info
        iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
        // add the node to the class
        if ( ppTable[iEntry] == NULL )
            ppTable[iEntry] = pObj;
        else
        {
            // set the representative of this node
            pRepr = ppTable[iEntry];
            Aig_ObjSetRepr( p->pAig, pObj, pRepr );
            // add node to the table
            if ( Dch_ObjNext( ppNexts, pRepr ) == NULL )
            { // this will be the second entry
                p->pClassSizes[pRepr->Id]++;
                nEntries++;
            }
            // add the entry to the list
            Dch_ObjSetNext( ppNexts, pObj, Dch_ObjNext( ppNexts, pRepr ) );
            Dch_ObjSetNext( ppNexts, pRepr, pObj );
            p->pClassSizes[pRepr->Id]++;
            nEntries++;
        }
    }

    // allocate room for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
    p->pMemClassesFree = p->pMemClasses + nEntries;
 
    // copy the entries into storage in the topological order
    nEntries2 = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
            continue;
        nNodes = p->pClassSizes[pObj->Id];
        // skip the nodes that are not representatives of non-trivial classes
        if ( nNodes == 0 )
            continue;
        assert( nNodes > 1 );
        // add the nodes to the class in the topological order
        ppClassNew = p->pMemClasses + nEntries2;
        ppClassNew[0] = pObj;
        for ( pTemp = Dch_ObjNext(ppNexts, pObj), k = 1; pTemp; 
              pTemp = Dch_ObjNext(ppNexts, pTemp), k++ )
        {
            ppClassNew[nNodes-k] = pTemp;
        }
        // add the class of nodes
        p->pClassSizes[pObj->Id] = 0;
        Dch_ObjAddClass( p, pObj, ppClassNew, nNodes );
        // increment the number of entries
        nEntries2 += nNodes;
    }
    assert( nEntries == nEntries2 );
    ABC_FREE( ppTable );
    ABC_FREE( ppNexts );
    // now it is time to refine the classes
    Dch_ClassesRefine( p );
    Dch_ClassesCheck( p );
}

void Dch_ClassesPrint	(	Dch_Cla_t *	p,
		int	fVeryVerbose
	)

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 303 of file dchClass.c.

{
    Aig_Obj_t ** ppClass;
    Aig_Obj_t * pObj;
    int i;
    Abc_Print( 1, "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", 
        p->nCands1, p->nClasses, p->nLits );
    if ( !fVeryVerbose )
        return;
    Abc_Print( 1, "Constants { " );
    Aig_ManForEachObj( p->pAig, pObj, i )
        if ( Dch_ObjIsConst1Cand( p->pAig, pObj ) )
            Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
    Abc_Print( 1, "}\n" );
    Dch_ManForEachClass( p, ppClass, i )
    {
        Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
        Dch_ClassesPrintOne( p, ppClass[0] );
    }
    Abc_Print( 1, "\n" );
}

Aig_Obj_t** Dch_ClassesReadClass	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pRepr,
		int *	pnSize
	)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file dchClass.c.

{
    assert( p->pId2Class[pRepr->Id] != NULL );
    assert( p->pClassSizes[pRepr->Id] > 1 );
    *pnSize = p->pClassSizes[pRepr->Id];
    return p->pId2Class[pRepr->Id];
}

int Dch_ClassesRefine

(

Dch_Cla_t *

p

)

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 504 of file dchClass.c.

{
    Aig_Obj_t ** ppClass;
    int i, nRefis = 0;
    Dch_ManForEachClass( p, ppClass, i )
        nRefis += Dch_ClassesRefineOneClass( p, ppClass[0], 0 );
    return nRefis;
}

int Dch_ClassesRefineConst1Group	(	Dch_Cla_t *	p,
		Vec_Ptr_t *	vRoots,
		int	fRecursive
	)

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 570 of file dchClass.c.

{
    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
    int i;
    if ( Vec_PtrSize(vRoots) == 0 )
        return 0;
    // collect the nodes to be refined
    Vec_PtrClear( p->vClassNew );
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
            Vec_PtrPush( p->vClassNew, pObj );
    // check if there is a new class
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
    p->nCands1 -= Vec_PtrSize(p->vClassNew);
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
    if ( Vec_PtrSize(p->vClassNew) == 1 )
        return 1;
    // create a new class composed of these nodes
    ppClassNew = p->pMemClassesFree;
    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        ppClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }
    Dch_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

int Dch_ClassesRefineOneClass	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pReprOld,
		int	fRecursive
	)

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

Synopsis [Iteratively refines the classes after simulation.]

Description [Returns the number of refinements performed.]

SideEffects []

SeeAlso []

Definition at line 443 of file dchClass.c.

{
    Aig_Obj_t ** pClassOld, ** pClassNew;
    Aig_Obj_t * pObj, * pReprNew;
    int i;

    // split the class
    Vec_PtrClear( p->vClassOld );
    Vec_PtrClear( p->vClassNew );
    Dch_ClassForEachNode( p, pReprOld, pObj, i )
        if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
            Vec_PtrPush( p->vClassOld, pObj );
        else
            Vec_PtrPush( p->vClassNew, pObj );
    // check if splitting happened
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;

    // get the new representative
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
    assert( Vec_PtrSize(p->vClassOld) > 0 );
    assert( Vec_PtrSize(p->vClassNew) > 0 );

    // create old class
    pClassOld = Dch_ObjRemoveClass( p, pReprOld );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
    {
        pClassOld[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
    }
    // create new class
    pClassNew = pClassOld + i;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        pClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }

    // put classes back
    if ( Vec_PtrSize(p->vClassOld) > 1 )
        Dch_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
    if ( Vec_PtrSize(p->vClassNew) > 1 )
        Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );

    // check if the class should be recursively refined
    if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
        return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

void Dch_ClassesSetData	(	Dch_Cla_t *	p,
		void *	pManData,
		unsigned(*)(void *, Aig_Obj_t *)	pFuncNodeHash,
		int(*)(void *, Aig_Obj_t *)	pFuncNodeIsConst,
		int(*)(void *, Aig_Obj_t *, Aig_Obj_t *)	pFuncNodesAreEqual
	)

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file dchClass.c.

{
    p->pManData           = pManData;
    p->pFuncNodeHash      = pFuncNodeHash;
    p->pFuncNodeIsConst   = pFuncNodeIsConst;
    p->pFuncNodesAreEqual = pFuncNodesAreEqual;
}

Dch_Cla_t* Dch_ClassesStart

(

Aig_Man_t *

pAig

)

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file dchClass.c.

{
    Dch_Cla_t * p;
    p = ABC_ALLOC( Dch_Cla_t, 1 );
    memset( p, 0, sizeof(Dch_Cla_t) );
    p->pAig         = pAig;
    p->pId2Class    = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
    p->pClassSizes  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    p->vClassOld    = Vec_PtrAlloc( 100 );
    p->vClassNew    = Vec_PtrAlloc( 100 );
    assert( pAig->pReprs == NULL );
    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    return p;
}

void Dch_ClassesStop

(

Dch_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file dchClass.c.

{
    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
    ABC_FREE( p->pId2Class );
    ABC_FREE( p->pClassSizes );
    ABC_FREE( p->pMemClasses );
    ABC_FREE( p );
}

void Dch_CnfNodeAddToSolver	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file dchCnf.c.

{ 
    Vec_Ptr_t * vFrontier;
    Aig_Obj_t * pNode, * pFanin;
    int i, k, fUseMuxes = 1;
    // quit if CNF is ready
    if ( Dch_ObjSatNum(p,pObj) )
        return;
    // start the frontier
    vFrontier = Vec_PtrAlloc( 100 );
    Dch_ObjAddToFrontier( p, pObj, vFrontier );
    // explore nodes in the frontier
    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
    {
        // create the supergate
        assert( Dch_ObjSatNum(p,pNode) );
        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
        {
            Vec_PtrClear( p->vFanins );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
            Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
                Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Dch_AddClausesMux( p, pNode );
        }
        else
        {
            Dch_CollectSuper( pNode, fUseMuxes, p->vFanins );
            Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
                Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Dch_AddClausesSuper( p, pNode, p->vFanins );
        }
        assert( Vec_PtrSize(p->vFanins) > 1 );
    }
    Vec_PtrFree( vFrontier );
}

Dch_Cla_t* Dch_CreateCandEquivClasses	(	Aig_Man_t *	pAig,
		int	nWords,
		int	fVerbose
	)

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

Synopsis [Derives candidate equivalence classes of AIG nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file dchSim.c.

{
    Dch_Cla_t * pClasses;
    Vec_Ptr_t * vSims;
    int i;
    // allocate simulation information
    vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
    // run random simulation from the primary inputs
    Dch_PerformRandomSimulation( pAig, vSims );
    // start storage for equivalence classes
    pClasses = Dch_ClassesStart( pAig );
    Dch_ClassesSetData( pClasses, vSims, Dch_NodeHash, Dch_NodeIsConst, Dch_NodesAreEqual );
    // hash nodes by sim info
    Dch_ClassesPrepare( pClasses, 0, 0 );
    // iterate random simulation
    for ( i = 0; i < 7; i++ )
    {
        Dch_PerformRandomSimulation( pAig, vSims );
        Dch_ClassesRefine( pClasses );
    }
    // clean up and return
    Vec_PtrFree( vSims );
    // prepare class refinement procedures
    Dch_ClassesSetData( pClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
    return pClasses;
}

Aig_Man_t* Dch_DeriveChoiceAig	(	Aig_Man_t *	pAig,
		int	fSkipRedSupps
	)

Definition at line 517 of file dchChoice.c.

{
    int fCheck = 0;
    Aig_Man_t * pChoices, * pTemp;
    // verify
    if ( fCheck )
        Aig_ManCheckReprs( pAig ); 
    // compute choices
    pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps );
    ABC_FREE( pChoices->pReprs );
    // verify
    if ( fCheck )
        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
    // find correct topo order with choices
    pChoices = Aig_ManDupDfs( pTemp = pChoices );
    Aig_ManStop( pTemp );
    // verify
    if ( fCheck )
        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
    return pChoices;
}

int Dch_DeriveChoiceCountEquivs

(

Aig_Man_t *

pAig

)

Definition at line 89 of file dchChoice.c.

{
    Aig_Obj_t * pObj, * pEquiv;
    int i, nEquivs = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pEquiv = Aig_ObjEquiv( pAig, pObj );
        if ( pEquiv == NULL )
            continue;
        assert( pEquiv->Id < pObj->Id );
        nEquivs++;
    }
    return nEquivs;
}

int Dch_DeriveChoiceCountReprs

(

Aig_Man_t *

pAig

)

FUNCTION DECLARATIONS ///.

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

Synopsis [Counts the number of representatives.]

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file dchChoice.c.

{
    Aig_Obj_t * pObj, * pRepr;
    int i, nReprs = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pRepr = Aig_ObjRepr( pAig, pObj );
        if ( pRepr == NULL )
            continue;
        assert( pRepr->Id < pObj->Id );
        nReprs++;
    }
    return nReprs;
}

Dch_Man_t* Dch_ManCreate	(	Aig_Man_t *	pAig,
		Dch_Pars_t *	pPars
	)

DECLARATIONS ///.

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

FileName [dchMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [Calls to the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

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

Synopsis [Creates the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file dchMan.c.

{
    Dch_Man_t * p;
    // create interpolation manager
    p = ABC_ALLOC( Dch_Man_t, 1 );
    memset( p, 0, sizeof(Dch_Man_t) );
    p->pPars        = pPars;
    p->pAigTotal    = pAig; //Dch_DeriveTotalAig( vAigs );
    Aig_ManFanoutStart( p->pAigTotal );
    // SAT solving
    p->nSatVars     = 1;
    p->pSatVars     = ABC_CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
    p->vUsedNodes   = Vec_PtrAlloc( 1000 );
    p->vFanins      = Vec_PtrAlloc( 100 );
    p->vSimRoots    = Vec_PtrAlloc( 1000 );
    p->vSimClasses  = Vec_PtrAlloc( 1000 );
    // equivalences proved
    p->pReprsProved = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) );
    return p;
}

void Dch_ManResimulateCex	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj,
		Aig_Obj_t *	pRepr
	)

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file dchSimSat.c.

{
    Aig_Obj_t * pRoot, ** ppClass;
    int i, k, nSize, RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // get the equivalence classes
    Dch_ManCollectTfoCands( p, pObj, pRepr );
    // resimulate the cone of influence of the solved nodes
    p->nConeThis = 0;
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
    Dch_ManResimulateSolved_rec( p, pObj );
    Dch_ManResimulateSolved_rec( p, pRepr );
    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
    // resimulate the cone of influence of the other nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
        Dch_ManResimulateOther_rec( p, pRoot );
    // refine these nodes
    RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
    // resimulate the cone of influence of the cand classes
    RetValue2 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i )
    {
        ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
        for ( k = 0; k < nSize; k++ )
            Dch_ManResimulateOther_rec( p, ppClass[k] );
        // refine this class
        RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
    }
    // make sure refinement happened
    if ( Aig_ObjIsConst1(pRepr) )
        assert( RetValue1 );
    else
        assert( RetValue2 );
p->timeSimSat += Abc_Clock() - clk;
}

void Dch_ManResimulateCex2	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj,
		Aig_Obj_t *	pRepr
	)

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file dchSimSat.c.

{
    Aig_Obj_t * pRoot;
    int i, RetValue;
    abctime clk = Abc_Clock();
    // get the equivalence class
    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
        Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
    else
        Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
    // resimulate the cone of influence of the solved nodes
    p->nConeThis = 0;
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
    Dch_ManResimulateSolved_rec( p, pObj );
    Dch_ManResimulateSolved_rec( p, pRepr );
    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
    // resimulate the cone of influence of the other nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
        Dch_ManResimulateOther_rec( p, pRoot );
    // refine this class
    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
        RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
    else
        RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
    assert( RetValue );
p->timeSimSat += Abc_Clock() - clk;
}

void Dch_ManSatSolverRecycle

(

Dch_Man_t *

p

)

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

Synopsis [Recycles the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file dchMan.c.

{
    int Lit;
    if ( p->pSat )
    {
        Aig_Obj_t * pObj;
        int i;
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vUsedNodes, pObj, i )
            Dch_ObjSetSatNum( p, pObj, 0 );
        Vec_PtrClear( p->vUsedNodes );
//        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
        sat_solver_delete( p->pSat );
    }
    p->pSat = sat_solver_new();
    sat_solver_setnvars( p->pSat, 1000 );
    // var 0 is not used
    // var 1 is reserved for const1 node - add the clause
    p->nSatVars = 1;
//    p->nSatVars = 0;
    Lit = toLit( p->nSatVars );
    if ( p->pPars->fPolarFlip )
        Lit = lit_neg( Lit );
    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
    Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ );

    p->nRecycles++;
    p->nCallsSince = 0;
}

void Dch_ManStop

(

Dch_Man_t *

p

)

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 122 of file dchMan.c.

{
    Aig_ManFanoutStop( p->pAigTotal );
    if ( p->pPars->fVerbose )
        Dch_ManPrintStats( p );
    if ( p->pAigFraig )
        Aig_ManStop( p->pAigFraig );
    if ( p->ppClasses )
        Dch_ClassesStop( p->ppClasses );
    if ( p->pSat )
        sat_solver_delete( p->pSat );
    Vec_PtrFree( p->vUsedNodes );
    Vec_PtrFree( p->vFanins );
    Vec_PtrFree( p->vSimRoots );
    Vec_PtrFree( p->vSimClasses );
    ABC_FREE( p->pReprsProved );
    ABC_FREE( p->pSatVars );
    ABC_FREE( p );
}

void Dch_ManSweep

(

Dch_Man_t *

p

)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file dchSweep.c.

{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    // map constants and PIs
    p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) );
    Aig_ManCleanData( p->pAigTotal );
    Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
    Aig_ManForEachCi( p->pAigTotal, pObj, i )
        pObj->pData = Aig_ObjCreateCi( p->pAigFraig );
    // sweep internal nodes
    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
    Aig_ManForEachNode( p->pAigTotal, pObj, i )
    {
        Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL || 
             Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
            continue;
        pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
        if ( pObjNew == NULL )
            continue;
        Dch_ObjSetFraig( pObj, pObjNew );
        Dch_ManSweepNode( p, pObj );
    }
    Bar_ProgressStop( pProgress );
    // update the representatives of the nodes (makes classes invalid)
    ABC_FREE( p->pAigTotal->pReprs );
    p->pAigTotal->pReprs = p->pReprsProved;
    p->pReprsProved = NULL;
    // clean the mark
    Aig_ManCleanMarkB( p->pAigTotal );
}

int Dch_NodesAreEquiv	(	Dch_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew
	)

DECLARATIONS ///.

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

FileName [dchSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [Calls to the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

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

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file dchSat.c.

{
    int nBTLimit = p->pPars->nBTLimit;
    int pLits[2], RetValue, RetValue1, status;
    abctime clk;
    p->nSatCalls++;

    // sanity checks
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );

    p->nCallsSince++;  // experiment with this!!!
    
    // check if SAT solver needs recycling
    if ( p->pSat == NULL || 
        (p->pPars->nSatVarMax && 
         p->nSatVars > p->pPars->nSatVarMax && 
         p->nCallsSince > p->pPars->nCallsRecycle) )
        Dch_ManSatSolverRecycle( p );

    // if the nodes do not have SAT variables, allocate them
    Dch_CnfNodeAddToSolver( p, pOld );
    Dch_CnfNodeAddToSolver( p, pNew );

    // propage unit clauses
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        status = sat_solver_simplify(p->pSat);
        assert( status != 0 );
        assert( p->pSat->qtail == p->pSat->qhead );
    }

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 );
    pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatFailsReal++;
        return -1;
    }

    // if the old node was constant 0, we already know the answer
    if ( pOld == Aig_ManConst1(p->pAigFraig) )
    {
        p->nSatProof++;
        return 1;
    }

    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
    pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 );
    pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}

static Aig_Obj_t* Dch_ObjFraig ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 105 of file dchInt.h.

{ return (Aig_Obj_t *)pObj->pData;  }

static int Dch_ObjIsConst1Cand ( Aig_Man_t *  pAig, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 108 of file dchInt.h.

{
    return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
}

static int Dch_ObjSatNum ( Dch_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 102 of file dchInt.h.

{ return p->pSatVars[pObj->Id]; }

static void Dch_ObjSetConst1Cand ( Aig_Man_t *  pAig, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 112 of file dchInt.h.

{
    assert( !Dch_ObjIsConst1Cand( pAig, pObj ) );
    Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}

static void Dch_ObjSetFraig ( Aig_Obj_t *  pObj, Aig_Obj_t *  pNode  )

inlinestatic

Definition at line 106 of file dchInt.h.

{ pObj->pData = pNode; }

static void Dch_ObjSetSatNum ( Dch_Man_t *  p, Aig_Obj_t *  pObj, int  Num  )

inlinestatic

Definition at line 103 of file dchInt.h.

{ p->pSatVars[pObj->Id] = Num;  }