sswInt.h File Reference

#include "aig/saig/saig.h"
#include "sat/bsat/satSolver.h"
#include "ssw.h"
#include "aig/ioa/ioa.h"

Go to the source code of this file.

Data Structures
struct	Ssw_Man_t_
struct	Ssw_Sat_t_
struct	Ssw_Frm_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_	Ssw_Man_t
	INCLUDES ///. More...
typedef struct Ssw_Frm_t_	Ssw_Frm_t
typedef struct Ssw_Sat_t_	Ssw_Sat_t
typedef struct Ssw_Cla_t_	Ssw_Cla_t

Functions
static int	Ssw_ObjSatNum (Ssw_Sat_t *p, Aig_Obj_t *pObj)
	MACRO DEFINITIONS ///. More...
static void	Ssw_ObjSetSatNum (Ssw_Sat_t *p, Aig_Obj_t *pObj, int Num)
static int	Ssw_ObjIsConst1Cand (Aig_Man_t *pAig, Aig_Obj_t *pObj)
static void	Ssw_ObjSetConst1Cand (Aig_Man_t *pAig, Aig_Obj_t *pObj)
static Aig_Obj_t *	Ssw_ObjFrame (Ssw_Man_t *p, Aig_Obj_t *pObj, int i)
static void	Ssw_ObjSetFrame (Ssw_Man_t *p, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
static Aig_Obj_t *	Ssw_ObjChild0Fra (Ssw_Man_t *p, Aig_Obj_t *pObj, int i)
static Aig_Obj_t *	Ssw_ObjChild1Fra (Ssw_Man_t *p, Aig_Obj_t *pObj, int i)
static Aig_Obj_t *	Ssw_ObjFrame_ (Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
static void	Ssw_ObjSetFrame_ (Ssw_Frm_t *p, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
static Aig_Obj_t *	Ssw_ObjChild0Fra_ (Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
static Aig_Obj_t *	Ssw_ObjChild1Fra_ (Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
Ssw_Frm_t *	Ssw_FrmStart (Aig_Man_t *pAig)
	FUNCTION DECLARATIONS ///. More...
void	Ssw_FrmStop (Ssw_Frm_t *p)
Aig_Man_t *	Ssw_FramesWithClasses (Ssw_Man_t *p)
Aig_Man_t *	Ssw_SpeculativeReduction (Ssw_Man_t *p)
Ssw_Cla_t *	Ssw_ClassesStart (Aig_Man_t *pAig)
void	Ssw_ClassesSetData (Ssw_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	Ssw_ClassesStop (Ssw_Cla_t *p)
Aig_Man_t *	Ssw_ClassesReadAig (Ssw_Cla_t *p)
Vec_Ptr_t *	Ssw_ClassesGetRefined (Ssw_Cla_t *p)
void	Ssw_ClassesClearRefined (Ssw_Cla_t *p)
int	Ssw_ClassesCand1Num (Ssw_Cla_t *p)
int	Ssw_ClassesClassNum (Ssw_Cla_t *p)
int	Ssw_ClassesLitNum (Ssw_Cla_t *p)
Aig_Obj_t **	Ssw_ClassesReadClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, int *pnSize)
void	Ssw_ClassesCollectClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, Vec_Ptr_t *vClass)
void	Ssw_ClassesCheck (Ssw_Cla_t *p)
void	Ssw_ClassesPrint (Ssw_Cla_t *p, int fVeryVerbose)
void	Ssw_ClassesRemoveNode (Ssw_Cla_t *p, Aig_Obj_t *pObj)
Ssw_Cla_t *	Ssw_ClassesPrepare (Aig_Man_t *pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose)
Ssw_Cla_t *	Ssw_ClassesPrepareSimple (Aig_Man_t *pAig, int fLatchCorr, int nMaxLevs)
Ssw_Cla_t *	Ssw_ClassesPrepareFromReprs (Aig_Man_t *pAig)
Ssw_Cla_t *	Ssw_ClassesPrepareTargets (Aig_Man_t *pAig)
Ssw_Cla_t *	Ssw_ClassesPreparePairs (Aig_Man_t *pAig, Vec_Int_t **pvClasses)
Ssw_Cla_t *	Ssw_ClassesPreparePairsSimple (Aig_Man_t *pMiter, Vec_Int_t *vPairs)
int	Ssw_ClassesRefine (Ssw_Cla_t *p, int fRecursive)
int	Ssw_ClassesRefineGroup (Ssw_Cla_t *p, Vec_Ptr_t *vReprs, int fRecursive)
int	Ssw_ClassesRefineOneClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, int fRecursive)
int	Ssw_ClassesRefineConst1Group (Ssw_Cla_t *p, Vec_Ptr_t *vRoots, int fRecursive)
int	Ssw_ClassesRefineConst1 (Ssw_Cla_t *p, int fRecursive)
int	Ssw_ClassesPrepareRehash (Ssw_Cla_t *p, Vec_Ptr_t *vCands, int fConstCorr)
Ssw_Sat_t *	Ssw_SatStart (int fPolarFlip)
	DECLARATIONS ///. More...
void	Ssw_SatStop (Ssw_Sat_t *p)
void	Ssw_CnfNodeAddToSolver (Ssw_Sat_t *p, Aig_Obj_t *pObj)
int	Ssw_CnfGetNodeValue (Ssw_Sat_t *p, Aig_Obj_t *pObjFraig)
int	Ssw_ManSweepBmcConstr (Ssw_Man_t *p)
int	Ssw_ManSweepConstr (Ssw_Man_t *p)
void	Ssw_ManRefineByConstrSim (Ssw_Man_t *p)
Aig_Man_t *	Ssw_SignalCorrespondenceRefine (Ssw_Man_t *p)
void	Ssw_ManLoadSolver (Ssw_Man_t *p, Aig_Obj_t *pRepr, Aig_Obj_t *pObj)
int	Ssw_ManSweepDyn (Ssw_Man_t *p)
int	Ssw_ManSweepLatch (Ssw_Man_t *p)
Ssw_Man_t *	Ssw_ManCreate (Aig_Man_t *pAig, Ssw_Pars_t *pPars)
	DECLARATIONS ///. More...
void	Ssw_ManCleanup (Ssw_Man_t *p)
void	Ssw_ManStop (Ssw_Man_t *p)
int	Ssw_NodesAreEquiv (Ssw_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
	DECLARATIONS ///. More...
int	Ssw_NodesAreConstrained (Ssw_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
int	Ssw_NodeIsConstrained (Ssw_Man_t *p, Aig_Obj_t *pPoObj)
int	Ssw_FilterUsingSemi (Ssw_Man_t *pMan, int fCheckTargets, int nConfMax, int fVerbose)
unsigned	Ssw_SmlObjHashWord (Ssw_Sml_t *p, Aig_Obj_t *pObj)
	FUNCTION DEFINITIONS ///. More...
int	Ssw_SmlObjIsConstWord (Ssw_Sml_t *p, Aig_Obj_t *pObj)
int	Ssw_SmlObjsAreEqualWord (Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
int	Ssw_SmlObjIsConstBit (void *p, Aig_Obj_t *pObj)
int	Ssw_SmlObjsAreEqualBit (void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
void	Ssw_SmlAssignRandomFrame (Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Ssw_Sml_t *	Ssw_SmlStart (Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
void	Ssw_SmlClean (Ssw_Sml_t *p)
void	Ssw_SmlStop (Ssw_Sml_t *p)
void	Ssw_SmlObjAssignConst (Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
void	Ssw_SmlObjSetWord (Ssw_Sml_t *p, Aig_Obj_t *pObj, unsigned Word, int iWord, int iFrame)
void	Ssw_SmlAssignDist1Plus (Ssw_Sml_t *p, unsigned *pPat)
void	Ssw_SmlSimulateOne (Ssw_Sml_t *p)
void	Ssw_SmlSimulateOneFrame (Ssw_Sml_t *p)
void	Ssw_SmlSimulateOneDyn_rec (Ssw_Sml_t *p, Aig_Obj_t *pObj, int f, int *pVisited, int nVisCounter)
void	Ssw_SmlResimulateSeq (Ssw_Sml_t *p)
void	Ssw_ManResimulateBit (Ssw_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
	DECLARATIONS ///. More...
void	Ssw_ManResimulateWord (Ssw_Man_t *p, Aig_Obj_t *pCand, Aig_Obj_t *pRepr, int f)
int	Ssw_ManGetSatVarValue (Ssw_Man_t *p, Aig_Obj_t *pObj, int f)
	DECLARATIONS ///. More...
void	Ssw_SmlSavePatternAig (Ssw_Man_t *p, int f)
int	Ssw_ManSweepNode (Ssw_Man_t *p, Aig_Obj_t *pObj, int f, int fBmc, Vec_Int_t *vPairs)
int	Ssw_ManSweepBmc (Ssw_Man_t *p)
int	Ssw_ManSweep (Ssw_Man_t *p)
void	Ssw_UniqueRegisterPairInfo (Ssw_Man_t *p)
	DECLARATIONS ///. More...
int	Ssw_ManUniqueOne (Ssw_Man_t *p, Aig_Obj_t *pRepr, Aig_Obj_t *pObj, int fVerbose)
int	Ssw_ManUniqueAddConstraint (Ssw_Man_t *p, Vec_Ptr_t *vCommon, int f1, int f2)

Typedef Documentation

typedef struct Ssw_Cla_t_ Ssw_Cla_t

Definition at line 50 of file sswInt.h.

typedef struct Ssw_Frm_t_ Ssw_Frm_t

Definition at line 48 of file sswInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t

INCLUDES ///.

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

FileName [sswInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 47 of file sswInt.h.

typedef struct Ssw_Sat_t_ Ssw_Sat_t

Definition at line 49 of file sswInt.h.

Function Documentation

int Ssw_ClassesCand1Num

(

Ssw_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file sswClass.c.

{
    return p->nCands1;
}

void Ssw_ClassesCheck

(

Ssw_Cla_t *

p

)

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

Synopsis [Checks candidate equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file sswClass.c.

{
    Aig_Obj_t * pObj, * pPrev, ** ppClass;
    int i, k, nLits, nClasses, nCands1;
    nClasses = nLits = 0;
    Ssw_ManForEachClass( p, ppClass, k )
    {
        pPrev = NULL;
        assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
        Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
        {
            if ( i == 0 )
                assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
            else
            {
                assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
                assert( pPrev->Id < pObj->Id );
                nLits++;
            }
            pPrev = pObj;
        }
        nClasses++;
    }
    nCands1 = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
        nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
    assert( p->nLits == nLits );
    assert( p->nCands1 == nCands1 );
    assert( p->nClasses == nClasses );
}

int Ssw_ClassesClassNum

(

Ssw_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file sswClass.c.

{
    return p->nClasses;
}

void Ssw_ClassesClearRefined

(

Ssw_Cla_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file sswClass.c.

{
    Vec_PtrClear( p->vRefined );
}

void Ssw_ClassesCollectClass	(	Ssw_Cla_t *	p,
		Aig_Obj_t *	pRepr,
		Vec_Ptr_t *	vClass
	)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file sswClass.c.

{
    int i;
    Vec_PtrClear( vClass );
    if ( p->pId2Class[pRepr->Id] == NULL )
        return;
    assert( p->pClassSizes[pRepr->Id] > 1 );
    for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
        Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
}

Vec_Ptr_t* Ssw_ClassesGetRefined

(

Ssw_Cla_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file sswClass.c.

{
    return p->vRefined;
}

int Ssw_ClassesLitNum

(

Ssw_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file sswClass.c.

{
    return p->nLits;
}

Ssw_Cla_t* Ssw_ClassesPrepare	(	Aig_Man_t *	pAig,
		int	nFramesK,
		int	fLatchCorr,
		int	fConstCorr,
		int	fOutputCorr,
		int	nMaxLevs,
		int	fVerbose
	)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 596 of file sswClass.c.

{
//    int nFrames =  4;
//    int nWords  =  1;
//    int nIters  = 16;

//    int nFrames = 32;
//    int nWords  =  4;
//    int nIters  =  0;

    int nFrames =  Abc_MaxInt( nFramesK, 4 );
    int nWords  =  2;
    int nIters  = 16;
    Ssw_Cla_t * p;
    Ssw_Sml_t * pSml;
    Vec_Ptr_t * vCands;
    Aig_Obj_t * pObj;
    int i, k, RetValue;
    abctime clk;

    // start the classes
    p = Ssw_ClassesStart( pAig );
    p->fConstCorr = fConstCorr;

    // perform sequential simulation
clk = Abc_Clock();
    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
if ( fVerbose )
{
    Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
        1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
    Abc_Print( 1, "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
    ABC_PRT( "Time", Abc_Clock() - clk );
}

    // set comparison procedures
clk = Abc_Clock();
    Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );

    // collect nodes to be considered as candidates
    vCands = Vec_PtrAlloc( 1000 );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Saig_ObjIsLo(p->pAig, 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;
        }
        Vec_PtrPush( vCands, pObj );
    }

    // this change will consider all PO drivers
    if ( fOutputCorr )
    {
        Vec_PtrClear( vCands );
        Aig_ManForEachObj( p->pAig, pObj, i )
            pObj->fMarkB = 0;
        Saig_ManForEachPo( p->pAig, pObj, i )
            if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) )
                Aig_ObjFanin0(pObj)->fMarkB = 1;
        Aig_ManForEachObj( p->pAig, pObj, i )
            if ( pObj->fMarkB )
                Vec_PtrPush( vCands, pObj );
        Aig_ManForEachObj( p->pAig, pObj, i )
            pObj->fMarkB = 0;
    }

    // allocate room for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
    p->pMemClassesFree = p->pMemClasses;

    // now it is time to refine the classes
    Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
if ( fVerbose )
{
    Abc_Print( 1, "Collecting candidate equivalence classes.        " );
ABC_PRT( "Time", Abc_Clock() - clk );
}

clk = Abc_Clock();
    // perform iterative refinement using simulation
    for ( i = 1; i < nIters; i++ )
    {
        // collect const1 candidates
        Vec_PtrClear( vCands );
        Aig_ManForEachObj( p->pAig, pObj, k )
            if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
                Vec_PtrPush( vCands, pObj );
        assert( Vec_PtrSize(vCands) == p->nCands1 );
        // perform new round of simulation
        Ssw_SmlResimulateSeq( pSml );
        // check equivalence classes
        RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
        if ( RetValue == 0 )
            break;
    }
    Ssw_SmlStop( pSml );
    Vec_PtrFree( vCands );
if ( fVerbose )
{
    Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
        nFrames, nWords, i-1 );
    ABC_PRT( "Time", Abc_Clock() - clk );
}
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Ssw_Cla_t* Ssw_ClassesPrepareFromReprs

(

Aig_Man_t *

pAig

)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 768 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj, * pRepr;
    int * pClassSizes, nEntries, i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // allocate memory for classes
    p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    // count classes
    p->nCands1 = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
        {
            p->nCands1++;
            continue;
        }
        if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
        {
            if ( p->pClassSizes[pRepr->Id]++ == 0 )
                p->pClassSizes[pRepr->Id]++;
        }
    }
    // add nodes
    nEntries = 0;
    p->nClasses = 0;
    pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( p->pClassSizes[i] )
        {
            p->pId2Class[i] = p->pMemClasses + nEntries;
            nEntries += p->pClassSizes[i];
            p->pId2Class[i][pClassSizes[i]++] = pObj;
            p->nClasses++;
            continue;
        }
        if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
            continue;
        if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
            p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj;
    }
    p->pMemClassesFree = p->pMemClasses + nEntries;
    p->nLits = nEntries - p->nClasses;
    assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
    ABC_FREE( pClassSizes );
//    Abc_Print( 1, "After converting:\n" );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Ssw_Cla_t* Ssw_ClassesPreparePairs	(	Aig_Man_t *	pAig,
		Vec_Int_t **	pvClasses
	)

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

Synopsis [Creates classes from the temporary representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 862 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t ** ppClassNew;
    Aig_Obj_t * pObj, * pRepr, * pPrev;
    int i, k, nTotalObjs, nEntries, Entry;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // count the number of entries in the classes
    nTotalObjs = 0;
    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
        nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
    // allocate memory for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
    // create constant-1 class
    if ( pvClasses[0] )
    Vec_IntForEachEntry( pvClasses[0], Entry, i )
    {
        assert( (i == 0) == (Entry == 0) );
        if ( i == 0 )
            continue;
        pObj = Aig_ManObj( pAig, Entry );
        Ssw_ObjSetConst1Cand( pAig, pObj );
        p->nCands1++;
    }
    // create classes
    nEntries = 0;
    for ( i = 1; i < Aig_ManObjNumMax(pAig); i++ )
    {
        if ( pvClasses[i] == NULL )
            continue;
        // get room for storing the class
        ppClassNew = p->pMemClasses + nEntries;
        nEntries  += Vec_IntSize( pvClasses[i] );
        // store the nodes of the class
        pPrev = pRepr = Aig_ManObj( pAig, Vec_IntEntry(pvClasses[i],0) );
        ppClassNew[0] = pRepr;
        Vec_IntForEachEntryStart( pvClasses[i], Entry, k, 1 )
        {
            pObj = Aig_ManObj( pAig, Entry );
            assert( pPrev->Id < pObj->Id );
            pPrev = pObj;
            ppClassNew[k] = pObj;
            Aig_ObjSetRepr( pAig, pObj, pRepr );
        }
        // create new class
        Ssw_ObjAddClass( p, pRepr, ppClassNew, Vec_IntSize(pvClasses[i]) );
    }
    // prepare room for new classes
    p->pMemClassesFree = p->pMemClasses + nEntries;
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Ssw_Cla_t* Ssw_ClassesPreparePairsSimple	(	Aig_Man_t *	pMiter,
		Vec_Int_t *	vPairs
	)

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

Synopsis [Creates classes from the temporary representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 928 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t ** ppClassNew;
    Aig_Obj_t * pObj, * pRepr;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pMiter );
    // allocate memory for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
    // create classes
    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
    {
        pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
        pObj  = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
        assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
        Aig_ObjSetRepr( pMiter, pObj, pRepr );
        // get room for storing the class
        ppClassNew = p->pMemClasses + i;
        ppClassNew[0] = pRepr;
        ppClassNew[1] = pObj;
        // create new class
        Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
    }
    // prepare room for new classes
    p->pMemClassesFree = NULL;
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

int Ssw_ClassesPrepareRehash	(	Ssw_Cla_t *	p,
		Vec_Ptr_t *	vCands,
		int	fConstCorr
	)

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

Synopsis [Takes the set of const1 cands and rehashes them using sim info.]

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file sswClass.c.

{
//    Aig_Man_t * pAig = p->pAig;
    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( Vec_PtrSize(vCands)/2 );
    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );

    // sort through the candidates
    nEntries = 0;
    p->nCands1 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
    {
        assert( p->pClassSizes[pObj->Id] == 0 );
        Aig_ObjSetRepr( p->pAig, pObj, NULL );
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
        {
            Ssw_ObjSetConst1Cand( p->pAig, pObj );
            p->nCands1++;
            continue;
        }
        if ( fConstCorr )
            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 ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
            { // this will be the second entry
                p->pClassSizes[pRepr->Id]++;
                nEntries++;
            }
            // add the entry to the list
            Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
            Ssw_ObjSetNext( ppNexts, pRepr, pObj );
            p->pClassSizes[pRepr->Id]++;
            nEntries++;
        }
    }

    // copy the entries into storage in the topological order
    nEntries2 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
    {
        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->pMemClassesFree + nEntries2;
        ppClassNew[0] = pObj;
        for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
              pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
        {
            ppClassNew[nNodes-k] = pTemp;
        }
        // add the class of nodes
        p->pClassSizes[pObj->Id] = 0;
        Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
        // increment the number of entries
        nEntries2 += nNodes;
    }
    p->pMemClassesFree += nEntries2;
    assert( nEntries == nEntries2 );
    ABC_FREE( ppTable );
    ABC_FREE( ppNexts );
    // now it is time to refine the classes
    return Ssw_ClassesRefine( p, 1 );
}

Ssw_Cla_t* Ssw_ClassesPrepareSimple	(	Aig_Man_t *	pAig,
		int	fLatchCorr,
		int	nMaxLevs
	)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 724 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // go through the nodes
    p->nCands1 = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Saig_ObjIsLo(pAig, pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                continue;
        }
        Ssw_ObjSetConst1Cand( pAig, pObj );
        p->nCands1++;
    }
    // allocate room for classes
    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Ssw_Cla_t* Ssw_ClassesPrepareTargets

(

Aig_Man_t *

pAig

)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 831 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // go through the nodes
    p->nCands1 = 0;
    Saig_ManForEachPo( pAig, pObj, i )
    {
        Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) );
        p->nCands1++;
    }
    // allocate room for classes
    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

void Ssw_ClassesPrint	(	Ssw_Cla_t *	p,
		int	fVeryVerbose
	)

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 414 of file sswClass.c.

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

Aig_Man_t* Ssw_ClassesReadAig

(

Ssw_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file sswClass.c.

{
    return p->pAig;
}

Aig_Obj_t** Ssw_ClassesReadClass	(	Ssw_Cla_t *	p,
		Aig_Obj_t *	pRepr,
		int *	pnSize
	)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file sswClass.c.

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

int Ssw_ClassesRefine	(	Ssw_Cla_t *	p,
		int	fRecursive
	)

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1034 of file sswClass.c.

{
    Aig_Obj_t ** ppClass;
    int i, nRefis = 0;
    Ssw_ManForEachClass( p, ppClass, i )
        nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], fRecursive );
    return nRefis;
}

int Ssw_ClassesRefineConst1	(	Ssw_Cla_t *	p,
		int	fRecursive
	)

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1119 of file sswClass.c.

{
    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
    int i;
    // collect the nodes to be refined
    Vec_PtrClear( p->vClassNew );
    for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
        if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
        {
            pObj = Aig_ManObj( p->pAig, i );
            if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
            {
                Vec_PtrPush( p->vClassNew, pObj );
//                Vec_PtrPush( p->vRefined, pObj );
            }
        }
    // check if there is a new class
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
    if ( p->fConstCorr )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
            Aig_ObjSetRepr( p->pAig, pObj, NULL );
        return 1;
    }
    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 );
    }
    Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

int Ssw_ClassesRefineConst1Group	(	Ssw_Cla_t *	p,
		Vec_Ptr_t *	vRoots,
		int	fRecursive
	)

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1074 of file sswClass.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 );
    }
    Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

int Ssw_ClassesRefineGroup	(	Ssw_Cla_t *	p,
		Vec_Ptr_t *	vReprs,
		int	fRecursive
	)

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1054 of file sswClass.c.

{
    Aig_Obj_t * pObj;
    int i, nRefis = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
        nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
    return nRefis;
}

int Ssw_ClassesRefineOneClass	(	Ssw_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 970 of file sswClass.c.

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

    // split the class
    Vec_PtrClear( p->vClassOld );
    Vec_PtrClear( p->vClassNew );
    Ssw_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;
    // remember that this class is refined
//    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
//        Vec_PtrPush( p->vRefined, pObj );

    // 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 = Ssw_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 )
        Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
    if ( Vec_PtrSize(p->vClassNew) > 1 )
        Ssw_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 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

void Ssw_ClassesRemoveNode	(	Ssw_Cla_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 448 of file sswClass.c.

{
    Aig_Obj_t * pRepr, * pTemp;
    assert( p->pClassSizes[pObj->Id] == 0 );
    assert( p->pId2Class[pObj->Id] == NULL );
    pRepr = Aig_ObjRepr( p->pAig, pObj );
    assert( pRepr != NULL );
//    Vec_PtrPush( p->vRefined, pObj );
    if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
    {
        assert( p->pClassSizes[pRepr->Id] == 0 );
        assert( p->pId2Class[pRepr->Id] == NULL );
        Aig_ObjSetRepr( p->pAig, pObj, NULL );
        p->nCands1--;
        return;
    }
//    Vec_PtrPush( p->vRefined, pRepr );
    Aig_ObjSetRepr( p->pAig, pObj, NULL );
    assert( p->pId2Class[pRepr->Id][0] == pRepr );
    assert( p->pClassSizes[pRepr->Id] >= 2 );
    if ( p->pClassSizes[pRepr->Id] == 2 )
    {
        p->pId2Class[pRepr->Id] = NULL;
        p->nClasses--;
        p->pClassSizes[pRepr->Id] = 0;
        p->nLits--;
    }
    else
    {
        int i, k = 0;
        // remove the entry from the class
        Ssw_ClassForEachNode( p, pRepr, pTemp, i )
            if ( pTemp != pObj )
                p->pId2Class[pRepr->Id][k++] = pTemp;
        assert( k + 1 == p->pClassSizes[pRepr->Id] );
        // reduce the class
        p->pClassSizes[pRepr->Id]--;
        p->nLits--;
    }
}

void Ssw_ClassesSetData	(	Ssw_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 167 of file sswClass.c.

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

Ssw_Cla_t* Ssw_ClassesStart

(

Aig_Man_t *

pAig

)

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file sswClass.c.

{
    Ssw_Cla_t * p;
    p = ABC_ALLOC( Ssw_Cla_t, 1 );
    memset( p, 0, sizeof(Ssw_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 );
    p->vRefined     = Vec_PtrAlloc( 1000 );
    if ( pAig->pReprs == NULL )
        Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    return p;
}

void Ssw_ClassesStop

(

Ssw_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file sswClass.c.

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

int Ssw_CnfGetNodeValue	(	Ssw_Sat_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file sswCnf.c.

{
    int Value0, Value1, nVarNum;
    assert( !Aig_IsComplement(pObj) );
    nVarNum = Ssw_ObjSatNum( p, pObj );
    if ( nVarNum > 0 )
        return sat_solver_var_value( p->pSat, nVarNum );
//    if ( pObj->fMarkA == 1 )
//        return 0;
    if ( Aig_ObjIsCi(pObj) )
        return 0;
    assert( Aig_ObjIsNode(pObj) );
    Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
    Value0 ^= Aig_ObjFaninC0(pObj);
    Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
    Value1 ^= Aig_ObjFaninC1(pObj);
    return Value0 & Value1;
}

void Ssw_CnfNodeAddToSolver	(	Ssw_Sat_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file sswCnf.c.

{
    Vec_Ptr_t * vFrontier;
    Aig_Obj_t * pNode, * pFanin;
    int i, k, fUseMuxes = 1;
    // quit if CNF is ready
    if ( Ssw_ObjSatNum(p,pObj) )
        return;
    // start the frontier
    vFrontier = Vec_PtrAlloc( 100 );
    Ssw_ObjAddToFrontier( p, pObj, vFrontier );
    // explore nodes in the frontier
    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
    {
        // create the supergate
        assert( Ssw_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 )
                Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Ssw_AddClausesMux( p, pNode );
        }
        else
        {
            Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
            Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
                Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Ssw_AddClausesSuper( p, pNode, p->vFanins );
        }
        assert( Vec_PtrSize(p->vFanins) > 1 );
    }
    Vec_PtrFree( vFrontier );
}

int Ssw_FilterUsingSemi	(	Ssw_Man_t *	pMan,
		int	fCheckTargets,
		int	nConfMax,
		int	fVerbose
	)

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

Synopsis [Returns 1 if one of the targets has failed.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file sswSemi.c.

{
    Ssw_Sem_t * p;
    int RetValue, Frames, Iter;
    abctime clk = Abc_Clock();
    p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
    if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
    {
        assert( 0 );
        Ssw_SemManStop( p );
        return 1;
    }
    if ( fVerbose )
    {
        Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d.  ConfMax = %6d. FramesMax = %6d.\n",
            Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
            Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
    }
    RetValue = 0;
    for ( Iter = 0; Iter < p->nPatterns; Iter++ )
    {
clk = Abc_Clock();
        pMan->pMSat = Ssw_SatStart( 0 );
        Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
        if ( fVerbose )
        {
            Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
                Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
                Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
                p->pMan->nSatFailsReal? "f" : " " );
            ABC_PRT( "T", Abc_Clock() - clk );
        }
        Ssw_ManCleanup( p->pMan );
        if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
        {
            Abc_Print( 1, "Target is hit!!!\n" );
            RetValue = 1;
        }
        if ( p->nPatterns >= p->nPatternsAlloc )
            break;
    }
    Ssw_SemManStop( p );

    pMan->nStrangers = 0;
    pMan->nSatCalls = 0;
    pMan->nSatProof = 0;
    pMan->nSatFailsReal = 0;
    pMan->nSatCallsUnsat = 0;
    pMan->nSatCallsSat = 0;
    pMan->timeSimSat = 0;
    pMan->timeSat = 0;
    pMan->timeSatSat = 0;
    pMan->timeSatUnsat = 0;
    pMan->timeSatUndec = 0;
    return RetValue;
}

Aig_Man_t* Ssw_FramesWithClasses

(

Ssw_Man_t *

p

)

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file sswAig.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
    int i, f, iLits;
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    p->nConstrTotal = p->nConstrReduced = 0;

    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // add timeframes
    iLits = 0;
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjNew = Aig_ObjCreateCi(pFrames);
            pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
        }
        // set the constraints on the latch outputs
        Saig_ManForEachLo( p->pAig, pObj, i )
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
        }
        // transfer to the primary outputs
        Aig_ManForEachCo( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
        // transfer latch input to the latch outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
            Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) );
    }
    assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );

    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    // make sure the satisfying assignment is node assigned
    assert( pFrames->pData == NULL );
//Aig_ManShow( pFrames, 0, NULL );
    return pFrames;
}

Ssw_Frm_t* Ssw_FrmStart

(

Aig_Man_t *

pAig

)

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [sswAig.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [AIG manipulation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswAig.c.

{
    Ssw_Frm_t * p;
    p = ABC_ALLOC( Ssw_Frm_t, 1 );
    memset( p, 0, sizeof(Ssw_Frm_t) );
    p->pAig          = pAig;
    p->nObjs         = Aig_ManObjNumMax( pAig );
    p->nFrames       = 0;
    p->pFrames       = NULL;
    p->vAig2Frm      = Vec_PtrAlloc( 0 );
    Vec_PtrFill( p->vAig2Frm, 2 * p->nObjs, NULL );
    return p;
}

void Ssw_FrmStop

(

Ssw_Frm_t *

p

)

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file sswAig.c.

{
    if ( p->pFrames )
        Aig_ManStop( p->pFrames );
    Vec_PtrFree( p->vAig2Frm );
    ABC_FREE( p );
}

void Ssw_ManCleanup

(

Ssw_Man_t *

p

)

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file sswMan.c.

{
//    Aig_ManCleanMarkAB( p->pAig );
    assert( p->pMSat == NULL );
    if ( p->pFrames )
    {
        Aig_ManCleanMarkAB( p->pFrames );
        Aig_ManStop( p->pFrames );
        p->pFrames = NULL;
        memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
    }
    if ( p->vSimInfo )
    {
        Vec_PtrFree( p->vSimInfo );
        p->vSimInfo = NULL;
    }
    p->nConstrTotal = 0;
    p->nConstrReduced = 0;
}

Ssw_Man_t* Ssw_ManCreate	(	Aig_Man_t *	pAig,
		Ssw_Pars_t *	pPars
	)

DECLARATIONS ///.

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

FileName [sswMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Calls to the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Creates the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswMan.c.

{
    Ssw_Man_t * p;
    // prepare the sequential AIG
    assert( Saig_ManRegNum(pAig) > 0 );
    Aig_ManFanoutStart( pAig );
    Aig_ManSetCioIds( pAig );
    // create interpolation manager
    p = ABC_ALLOC( Ssw_Man_t, 1 );
    memset( p, 0, sizeof(Ssw_Man_t) );
    p->pPars         = pPars;
    p->pAig          = pAig;
    p->nFrames       = pPars->nFramesK + 1;
    p->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
    p->vCommon       = Vec_PtrAlloc( 100 );
    p->iOutputLit    = -1;
    // allocate storage for sim pattern
    p->nPatWords     = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
    p->pPatWords     = ABC_CALLOC( unsigned, p->nPatWords );
    // other
    p->vNewLos       = Vec_PtrAlloc( 100 );
    p->vNewPos       = Vec_IntAlloc( 100 );
    p->vResimConsts  = Vec_PtrAlloc( 100 );
    p->vResimClasses = Vec_PtrAlloc( 100 );
//    p->pPars->fVerbose = 1;
    return p;
}

int Ssw_ManGetSatVarValue	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	f
	)

DECLARATIONS ///.

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

FileName [sswSweep.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [One round of SAT sweeping.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswSweep.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Retrives value of the PI in the original AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file sswSweep.c.

{
    int fUseNoBoundary = 0;
    Aig_Obj_t * pObjFraig;
    int Value;
//    assert( Aig_ObjIsCi(pObj) );
    pObjFraig = Ssw_ObjFrame( p, pObj, f );
    if ( fUseNoBoundary )
    {
        Value = Ssw_CnfGetNodeValue( p->pMSat, Aig_Regular(pObjFraig) );
        Value ^= Aig_IsComplement(pObjFraig);
    }
    else
    {
        int nVarNum = Ssw_ObjSatNum( p->pMSat, Aig_Regular(pObjFraig) );
        Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pMSat->pSat, nVarNum ));
    }

//    Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum )));
//    Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
    if ( p->pPars->fPolarFlip )
    {
        if ( Aig_Regular(pObjFraig)->fPhase )  Value ^= 1;
    }
    return Value;
}

void Ssw_ManLoadSolver	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pRepr,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Loads logic cones and relevant constraints.]

Description [Both pRepr and pObj are objects of the AIG. The result is the current SAT solver loaded with the logic cones for pRepr and pObj corresponding to them in the frames, as well as all the relevant constraints.]

SideEffects []

SeeAlso []

Definition at line 142 of file sswDyn.c.

{
    Aig_Obj_t * pObjFrames, * pReprFrames;
    Aig_Obj_t * pTemp, * pObj0, * pObj1;
    int i, iConstr, RetValue;

    assert( pRepr != pObj );
    // get the corresponding frames nodes
    pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
    pObjFrames  = Aig_Regular( Ssw_ObjFrame( p, pObj,  p->pPars->nFramesK ) );
    assert( pReprFrames != pObjFrames );
 /*
    // compute the AIG support
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
    Ssw_ManCollectPis_rec( pObj,  p->vNewLos );
    // add logic cones for register outputs
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
    {
        pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
        Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
    }
*/
    // add cones for the nodes
    Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
    Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );

    // compute the frames support
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
    Ssw_ManCollectPis_rec( pObjFrames,  p->vNewLos );
    // these nodes include both nodes corresponding to PIs and LOs
    // (the nodes corresponding to PIs should be labeled with fMarkB!)

    // collect the related constraint POs
    Vec_IntClear( p->vNewPos );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
        Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
    // check if the corresponding pairs are added
    Vec_IntForEachEntry( p->vNewPos, iConstr, i )
    {
        pObj0 = Aig_ManCo( p->pFrames, 2*iConstr   );
        pObj1 = Aig_ManCo( p->pFrames, 2*iConstr+1 );
//        if ( pObj0->fMarkB && pObj1->fMarkB )
        if ( pObj0->fMarkB || pObj1->fMarkB )
        {
            pObj0->fMarkB = 1;
            pObj1->fMarkB = 1;
            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
        }
    }
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        assert( RetValue != 0 );
    }
}

void Ssw_ManRefineByConstrSim

(

Ssw_Man_t *

p

)

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

Synopsis [Performs fraiging for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 247 of file sswConstr.c.

{
    Aig_Obj_t * pObj, * pObjLi;
    int f, i, iLits, RetValue1, RetValue2;
    int nFrames = Vec_IntSize(p->vInits) / Saig_ManPiNum(p->pAig);
    assert( Vec_IntSize(p->vInits) % Saig_ManPiNum(p->pAig) == 0 );
    // assign register outputs
    Saig_ManForEachLi( p->pAig, pObj, i )
        pObj->fMarkB = 0;
    // simulate the timeframes
    iLits = 0;
    for ( f = 0; f < nFrames; f++ )
    {
        // set the PI simulation information
        Aig_ManConst1(p->pAig)->fMarkB = 1;
        Saig_ManForEachPi( p->pAig, pObj, i )
            pObj->fMarkB = Vec_IntEntry( p->vInits, iLits++ );
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
            pObj->fMarkB = pObjLi->fMarkB;
        // simulate internal nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                         & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
        // assign the COs
        Aig_ManForEachCo( p->pAig, pObj, i )
            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
        // check the outputs
        Saig_ManForEachPo( p->pAig, pObj, i )
        {
            if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
            {
                if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
                    Abc_Print( 1, "output %d failed in frame %d.\n", i, f );
            }
            else
            {
                if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
                    Abc_Print( 1, "constraint %d failed in frame %d.\n", i, f );
            }
        }
        // transfer
        if ( f == 0 )
        { // copy markB into phase
            Aig_ManForEachObj( p->pAig, pObj, i )
                pObj->fPhase = pObj->fMarkB;
        }
        else
        { // refine classes
            RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
            RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
        }
    }
    assert( iLits == Vec_IntSize(p->vInits) );
}

void Ssw_ManResimulateBit	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pCand,
		Aig_Obj_t *	pRepr
	)

DECLARATIONS ///.

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

FileName [sswSimSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Performs resimulation using counter-examples.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswSimSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswSimSat.c.

{
    Aig_Obj_t * pObj;
    int i, RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // set the PI simulation information
    Aig_ManConst1(p->pAig)->fMarkB = 1;
    Aig_ManForEachCi( p->pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit( p->pPatWords, i );
    // simulate internal nodes
    Aig_ManForEachNode( p->pAig, pObj, i )
        pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                     & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
    // if repr is given, perform refinement
    if ( pRepr )
    {
        // check equivalence classes
        RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
        RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
        // make sure refinement happened
        if ( Aig_ObjIsConst1(pRepr) )
        {
            assert( RetValue1 );
            if ( RetValue1 == 0 )
                Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
        }
        else
        {
            assert( RetValue2 );
            if ( RetValue2 == 0 )
                Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
        }
    }
p->timeSimSat += Abc_Clock() - clk;
}

void Ssw_ManResimulateWord	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pCand,
		Aig_Obj_t *	pRepr,
		int	f
	)

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file sswSimSat.c.

{
    int RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // set the PI simulation information
    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
    // simulate internal nodes
    Ssw_SmlSimulateOne( p->pSml );
    // check equivalence classes
    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
    // make sure refinement happened
    if ( Aig_ObjIsConst1(pRepr) )
    {
        assert( RetValue1 );
        if ( RetValue1 == 0 )
            Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
    }
    else
    {
        assert( RetValue2 );
        if ( RetValue2 == 0 )
            Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
    }
p->timeSimSat += Abc_Clock() - clk;
}

void Ssw_ManStop

(

Ssw_Man_t *

p

)

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file sswMan.c.

{
    ABC_FREE( p->pVisited );
    if ( p->pPars->fVerbose )//&& p->pPars->nStepsMax == -1 )
        Ssw_ManPrintStats( p );
    if ( p->ppClasses )
        Ssw_ClassesStop( p->ppClasses );
    if ( p->pSml )
        Ssw_SmlStop( p->pSml );
    if ( p->vDiffPairs )
        Vec_IntFree( p->vDiffPairs );
    if ( p->vInits )
        Vec_IntFree( p->vInits );
    Vec_PtrFree( p->vResimConsts );
    Vec_PtrFree( p->vResimClasses );
    Vec_PtrFree( p->vNewLos );
    Vec_IntFree( p->vNewPos );
    Vec_PtrFree( p->vCommon );
    ABC_FREE( p->pNodeToFrames );
    ABC_FREE( p->pPatWords );
    ABC_FREE( p );
}

int Ssw_ManSweep

(

Ssw_Man_t *

p

)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file sswSweep.c.

{
    static int Counter;
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObj2, * pObjNew;
    int nConstrPairs, i, f;
    abctime clk;
    Vec_Int_t * vDisproved;

    // perform speculative reduction
clk = Abc_Clock();
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    // add constants
    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
    assert( (nConstrPairs & 1) == 0 );
    for ( i = 0; i < nConstrPairs; i += 2 )
    {
        pObj  = Aig_ManCo( p->pFrames, i   );
        pObj2 = Aig_ManCo( p->pFrames, i+1 );
        Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
    }
    // build logic cones for register inputs
    for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
    {
        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
        Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
    }
    sat_solver_simplify( p->pMSat->pSat );

    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
p->timeReduce += Abc_Clock() - clk;

    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
    vDisproved = p->pPars->fEquivDump? Vec_IntAlloc(1000) : NULL;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
        else if ( Aig_ObjIsNode(pObj) )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
        }
    }
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );

    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    if ( p->pPars->fEquivDump )
        Ssw_ManDumpEquivMiter( p->pAig, vDisproved, Counter++ );
    Vec_IntFreeP( &vDisproved );
    return p->fRefined;
}

int Ssw_ManSweepBmc

(

Ssw_Man_t *

p

)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file sswSweep.c.

{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
    int i, f;
    abctime clk;
clk = Abc_Clock();

    // start initialized timeframes
    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );

    // sweep internal nodes
    p->fRefined = 0;
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
        // sweep internal nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            if ( p->pPars->fVerbose )
                Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
        }
        // quit if this is the last timeframe
        if ( f == p->pPars->nFramesK - 1 )
            break;
        // transfer latch input to the latch outputs
        Aig_ManForEachCo( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
        // build logic cones for register outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
        {
            pObjNew = Ssw_ObjFrame( p, pObjLi, f );
            Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
            Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
        }
    }
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );

    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += Abc_Clock() - clk;
    return p->fRefined;
}

int Ssw_ManSweepBmcConstr

(

Ssw_Man_t *

p

)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file sswConstr.c.

{
    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
    int i, f, iLits;
    abctime clk;
clk = Abc_Clock();

    // start initialized timeframes
    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );

    // build the constraint outputs
    iLits = 0;
    p->fRefined = 0;
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjNew = Aig_ObjCreateCi(p->pFrames);
            pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
        }
        // build the constraint cones
        Saig_ManForEachPo( p->pAig, pObj, i )
        {
            if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
                continue;
            pObjNew = Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObj), f );
            pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
            if ( Aig_Regular(pObjNew) == Aig_ManConst1(p->pFrames) )
            {
                assert( Aig_IsComplement(pObjNew) );
                continue;
            }
            Ssw_NodesAreConstrained( p, pObjNew, Aig_ManConst0(p->pFrames) );
        }

        // sweep internal nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 );
        }
        // quit if this is the last timeframe
        if ( f == p->pPars->nFramesK - 1 )
            break;
        // transfer latch input to the latch outputs
        Aig_ManForEachCo( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
        // build logic cones for register outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
        {
            pObjNew = Ssw_ObjFrame( p, pObjLi, f );
            Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
            Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
        }
    }
    assert( Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );

    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += Abc_Clock() - clk;
    return p->fRefined;
}

int Ssw_ManSweepConstr

(

Ssw_Man_t *

p

)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 619 of file sswConstr.c.

{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObj2, * pObjNew;
    int nConstrPairs, i, f, iLits;
    abctime clk;
//Ssw_ManPrintPolarity( p->pAig );

    // perform speculative reduction
clk = Abc_Clock();
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    // add constants
    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
    assert( (nConstrPairs & 1) == 0 );
    for ( i = 0; i < nConstrPairs; i += 2 )
    {
        pObj  = Aig_ManCo( p->pFrames, i   );
        pObj2 = Aig_ManCo( p->pFrames, i+1 );
        Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
    }
    // build logic cones for register inputs
    for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
    {
        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
        Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
    }

    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
//    iLits = 0;
    iLits = f * Saig_ManPiNum(p->pAig);
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
    {
        pObjNew = Aig_ObjCreateCi(p->pFrames);
        pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
        Ssw_ObjSetFrame( p, pObj, f, pObjNew );
    }
    assert( Vec_IntSize(p->vInits) == iLits );
p->timeReduce += Abc_Clock() - clk;

    // add constraints to all timeframes
    for ( f = 0; f <= p->pPars->nFramesK; f++ )
    {
        Saig_ManForEachPo( p->pAig, pObj, i )
        {
            if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
                continue;
            Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObj), f );
//            if ( Aig_Regular(Ssw_ObjChild0Fra(p,pObj,f)) == Aig_ManConst1(p->pFrames) )
            if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst0(p->pFrames) )
                continue;
            assert( Ssw_ObjChild0Fra(p,pObj,f) != Aig_ManConst1(p->pFrames) );
            if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst1(p->pFrames) )
            {
                Abc_Print( 1, "Polarity violation.\n" );
                continue;
            }
            Ssw_NodesAreConstrained( p, Ssw_ObjChild0Fra(p,pObj,f), Aig_ManConst0(p->pFrames) );
        }
    }
    f = p->pPars->nFramesK;
    // clean the solver
    sat_solver_simplify( p->pMSat->pSat );


    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
        else if ( Aig_ObjIsNode(pObj) )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
        }
    }
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );
    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

int Ssw_ManSweepDyn

(

Ssw_Man_t *

p

)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file sswDyn.c.

{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
    int i, f;
    abctime clk;

    // perform speculative reduction
clk = Abc_Clock();
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    Aig_ManFanoutStart( p->pFrames );
    p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );

    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
    Aig_ManSetCioIds( p->pFrames );
    // label nodes corresponding to primary inputs
    Ssw_ManLabelPiNodes( p );
p->timeReduce += Abc_Clock() - clk;

    // prepare simulation info
    assert( p->vSimInfo == NULL );
    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );

    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
    p->iNodeStart = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( p->iNodeStart == 0 )
            p->iNodeStart = i;
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
        else if ( Aig_ObjIsNode(pObj) )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
        }
        // check if it is time to recycle the solver
        if ( p->pMSat->pSat == NULL ||
            (p->pPars->nSatVarMax2 &&
             p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
             p->nRecycleCalls > p->pPars->nRecycleCalls2) )
        {
            // resimulate
            if ( p->nPatterns > 0 )
            {
                p->iNodeLast = i;
                if ( p->pPars->fLocalSim )
                    Ssw_ManSweepResimulateDynLocal( p, f );
                else
                    Ssw_ManSweepResimulateDyn( p, f );
                p->iNodeStart = i+1;
            }
//                Abc_Print( 1, "Recycling SAT solver with %d vars and %d calls.\n", 
//                    p->pMSat->nSatVars, p->nRecycleCalls );
//            Aig_ManCleanMarkAB( p->pAig );
            Aig_ManCleanMarkAB( p->pFrames );
            // label nodes corresponding to primary inputs
            Ssw_ManLabelPiNodes( p );
            // replace the solver
            if ( p->pMSat )
            {
                p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
                p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
                Ssw_SatStop( p->pMSat );
                p->nRecycles++;
                p->nRecyclesTotal++;
                p->nRecycleCalls = 0;
            }
            p->pMSat = Ssw_SatStart( 0 );
            assert( p->nPatterns == 0 );
        }
        // resimulate
        if ( p->nPatterns == 32 )
        {
            p->iNodeLast = i;
            if ( p->pPars->fLocalSim )
                Ssw_ManSweepResimulateDynLocal( p, f );
            else
                Ssw_ManSweepResimulateDyn( p, f );
            p->iNodeStart = i+1;
        }
    }
    // resimulate
    if ( p->nPatterns > 0 )
    {
        p->iNodeLast = i;
        if ( p->pPars->fLocalSim )
            Ssw_ManSweepResimulateDynLocal( p, f );
        else
            Ssw_ManSweepResimulateDyn( p, f );
    }
    // collect stats
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );

    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

int Ssw_ManSweepLatch

(

Ssw_Man_t *

p

)

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

Synopsis [Performs one iteration of sweeping latches.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file sswLcorr.c.

{
//    Bar_Progress_t * pProgress = NULL;
    Vec_Ptr_t * vClass;
    Aig_Obj_t * pObj, * pRepr, * pTemp;
    int i, k;

    // start the timeframe
    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
    // map constants and PIs
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(p->pFrames) );

    // implement equivalence classes
    Saig_ManForEachLo( p->pAig, pObj, i )
    {
        pRepr = Aig_ObjRepr( p->pAig, pObj );
        if ( pRepr == NULL )
        {
            pTemp = Aig_ObjCreateCi(p->pFrames);
            pTemp->pData = pObj;
        }
        else
            pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
        Ssw_ObjSetFrame( p, pObj, 0, pTemp );
    }
    Aig_ManSetCioIds( p->pFrames );

    // prepare simulation info
    assert( p->vSimInfo == NULL );
    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );

    // go through the registers
//    if ( p->pPars->fVerbose )
//        pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
    vClass = Vec_PtrAlloc( 100 );
    p->fRefined = 0;
    p->nCallsCount = p->nCallsSat = p->nCallsUnsat = 0;
    Saig_ManForEachLo( p->pAig, pObj, i )
    {
//        if ( p->pPars->fVerbose )
//            Bar_ProgressUpdate( pProgress, i, NULL );
        // consider the case of constant candidate
        if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
            Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
        else
        {
            // consider the case of equivalence class
            Ssw_ClassesCollectClass( p->ppClasses, pObj, vClass );
            if ( Vec_PtrSize(vClass) == 0 )
                continue;
            // try to prove equivalences in this class
            Vec_PtrForEachEntry( Aig_Obj_t *, vClass, pTemp, k )
                if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
                {
                    Ssw_ManSweepLatchOne( p, pObj, pTemp );
                    if ( p->nPatterns == 32 )
                        break;
                }
        }
        // resimulate
        if ( p->nPatterns == 32 )
            Ssw_ManSweepResimulate( p );
        // attempt recycling the SAT solver
        if ( p->pPars->nSatVarMax &&
             p->pMSat->nSatVars > p->pPars->nSatVarMax &&
             p->nRecycleCalls > p->pPars->nRecycleCalls )
        {
            p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
            p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
            Ssw_SatStop( p->pMSat );
            p->pMSat = Ssw_SatStart( 0 );
            p->nRecycles++;
            p->nRecycleCalls = 0;
        }
    }
//    ABC_PRT( "reduce", p->timeReduce );
//    Aig_TableProfile( p->pFrames );
//    Abc_Print( 1, "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
    // resimulate
    if ( p->nPatterns > 0 )
        Ssw_ManSweepResimulate( p );
    // cleanup
    Vec_PtrFree( vClass );
//    if ( p->pPars->fVerbose )
//        Bar_ProgressStop( pProgress );

    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

int Ssw_ManSweepNode	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	f,
		int	fBmc,
		Vec_Int_t *	vPairs
	)

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

Synopsis [Performs fraiging for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 187 of file sswSweep.c.

{
    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
    int RetValue;
    abctime clk;
    // get representative of this class
    pObjRepr = Aig_ObjRepr( p->pAig, pObj );
    if ( pObjRepr == NULL )
        return 0;
    // get the fraiged node
    pObjFraig = Ssw_ObjFrame( p, pObj, f );
    // get the fraiged representative
    pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
    // check if constant 0 pattern distinquishes these nodes
    assert( pObjFraig != NULL && pObjReprFraig != NULL );
    assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
    // if the fraiged nodes are the same, return
    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
        return 0;
    // add constraints on demand
    if ( !fBmc && p->pPars->fDynamic )
    {
clk = Abc_Clock();
        Ssw_ManLoadSolver( p, pObjRepr, pObj );
        p->nRecycleCalls++;
p->timeMarkCones += Abc_Clock() - clk;
    }
    // call equivalence checking
    if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
    else
        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
    if ( RetValue == 1 )  // proved equivalent
    {
        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
        Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
        return 0;
    }
    if ( vPairs )
    {
        Vec_IntPush( vPairs, pObjRepr->Id );
        Vec_IntPush( vPairs, pObj->Id );
    }
    if ( RetValue == -1 ) // timed out
    {
        Ssw_ClassesRemoveNode( p->ppClasses, pObj );
        return 1;
    }
    // disproved the equivalence
    if ( !fBmc && p->pPars->fDynamic )
    {
        Ssw_SmlAddPatternDyn( p );
        p->nPatterns++;
        return 1;
    }
    else
        Ssw_SmlSavePatternAig( p, f );
    if ( !p->pPars->fConstrs )
        Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
    else
        Ssw_ManResimulateBit( p, pObj, pObjRepr );
    assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
    if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
    {
        Abc_Print( 1, "Ssw_ManSweepNode(): Failed to refine representative.\n" );
    }
    return 1;
}

int Ssw_ManUniqueAddConstraint	(	Ssw_Man_t *	p,
		Vec_Ptr_t *	vCommon,
		int	f1,
		int	f2
	)

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

Synopsis [Returns the output of the uniqueness constraint.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file sswUnique.c.

{
    Aig_Obj_t * pObj, * pObj1New, * pObj2New, * pMiter, * pTotal;
    int i, pLits[2];
//    int RetValue;
    assert( Vec_PtrSize(vCommon) > 0 );
    // generate the constraint
    pTotal = Aig_ManConst0(p->pFrames);
    Vec_PtrForEachEntry( Aig_Obj_t *, vCommon, pObj, i )
    {
        assert( Saig_ObjIsLo(p->pAig, pObj) );
        pObj1New = Ssw_ObjFrame( p, pObj, f1 );
        pObj2New = Ssw_ObjFrame( p, pObj, f2 );
        pMiter = Aig_Exor( p->pFrames, pObj1New, pObj2New );
        pTotal = Aig_Or( p->pFrames, pTotal, pMiter );
    }
    if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
    {
//        Abc_Print( 1, "Skipped\n" );
        return 0;
    }
    // create CNF
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pTotal) );
    // add output constraint
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
/*
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    assert( RetValue );
    // simplify the solver
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pSat);
        assert( RetValue != 0 );
    }
*/
    assert( p->iOutputLit == -1 );
    p->iOutputLit = pLits[0];
    return 1;
}

int Ssw_ManUniqueOne	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pRepr,
		Aig_Obj_t *	pObj,
		int	fVerbose
	)

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

Synopsis [Returns 1 if uniqueness constraints can be added.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file sswUnique.c.

{
    Aig_Obj_t * ppObjs[2], * pTemp;
    int i, k, Value0, Value1, RetValue, fFeasible;

    assert( p->pPars->nFramesK > 1 );
    assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );

    // compute the first support in terms of LOs
    ppObjs[0] = pRepr;
    ppObjs[1] = pObj;
    Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon );
    // keep only LOs
    RetValue = Vec_PtrSize( p->vCommon );
    fFeasible = 0;
    k = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
    {
        assert( Aig_ObjIsCi(pTemp) );
        if ( !Saig_ObjIsLo(p->pAig, pTemp) )
            continue;
        assert( Aig_ObjCioId(pTemp) > 0 );
        Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
        if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjCioId(pTemp) - Saig_ManPiNum(p->pAig)) )
            fFeasible = 1;
    }
    Vec_PtrShrink( p->vCommon, k );

    if ( fVerbose )
        Abc_Print( 1, "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
            Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon),
            fFeasible? "yes": "no " );

    // check the current values
    RetValue = 1;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
    {
        Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 );
        Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 );
        if ( Value0 != Value1 )
            RetValue = 0;
        if ( fVerbose )
            Abc_Print( 1, "%d", Value0 ^ Value1 );
    }
    if ( fVerbose )
        Abc_Print( 1, "\n" );

    return RetValue && fFeasible;
}

int Ssw_NodeIsConstrained	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pPoObj
	)

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

Synopsis [Constrains one node in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file sswSat.c.

{
    int RetValue, Lit;
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pPoObj) );
    // add constraint A = 1  ---->  A
    Lit = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_ObjFanin0(pPoObj)), !Aig_ObjFaninC0(pPoObj) );
    if ( p->pPars->fPolarFlip )
    {
        if ( Aig_ObjFanin0(pPoObj)->fPhase )  Lit = lit_neg( Lit );
    }
    RetValue = sat_solver_addclause( p->pMSat->pSat, &Lit, &Lit + 1 );
    assert( RetValue );
    return 1;
}

int Ssw_NodesAreConstrained	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew
	)

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

Synopsis [Constrains two nodes to be equivalent in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file sswSat.c.

{
    int pLits[2], RetValue, fComplNew;
    Aig_Obj_t * pTemp;

    // sanity checks
    assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
    assert( p->pPars->fConstrs || Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) );

    // move constant to the old node
    if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
    {
        assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
        pTemp = pOld;
        pOld  = pNew;
        pNew  = pTemp;
    }

    // move complement to the new node
    if ( Aig_IsComplement(pOld) )
    {
        pOld = Aig_Regular(pOld);
        pNew = Aig_Not(pNew);
    }
    assert( p->pMSat != NULL );

    // if the nodes do not have SAT variables, allocate them
    Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pNew) );

    // transform the new node
    fComplNew = Aig_IsComplement( pNew );
    pNew = Aig_Regular( pNew );

    // consider the constant 1 case
    if ( pOld == Aig_ManConst1(p->pFrames) )
    {
        // add constraint A = 1  ---->  A
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
        if ( p->pPars->fPolarFlip )
        {
            if ( pNew->fPhase )  pLits[0] = lit_neg( pLits[0] );
        }
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 1 );
        assert( RetValue );
    }
    else
    {
        // add constraint A = B  ---->  (A v !B)(!A v B)

        // (A v !B)
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew );
        if ( p->pPars->fPolarFlip )
        {
            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
        }
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
        assert( RetValue );

        // (!A v B)
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew);
        if ( p->pPars->fPolarFlip )
        {
            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
        }
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
        assert( RetValue );
    }
    return 1;
}

int Ssw_NodesAreEquiv	(	Ssw_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew
	)

DECLARATIONS ///.

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

FileName [sswSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Calls to the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Runs equivalence test for the two nodes.]

Description [Both nodes should be regular and different from each other.]

SideEffects []

SeeAlso []

Definition at line 45 of file sswSat.c.

{
    int nBTLimit = p->pPars->nBTLimit;
    int pLits[3], nLits, RetValue, RetValue1;
    abctime clk;//, status;
    p->nSatCalls++;
    p->pMSat->nSolverCalls++;

    // sanity checks
    assert( !Aig_IsComplement(pOld) );
    assert( !Aig_IsComplement(pNew) );
    assert( pOld != pNew );
    assert( p->pMSat != NULL );

    // if the nodes do not have SAT variables, allocate them
    Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
    Ssw_CnfNodeAddToSolver( p->pMSat, pNew );

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    nLits = 2;
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
    pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase == pNew->fPhase );
    if ( p->iOutputLit > -1 )
        pLits[nLits++] = p->iOutputLit;
    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 );

    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        assert( RetValue != 0 );
    }

clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
        (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;
        if ( nLits == 2 )
        {
            pLits[0] = lit_neg( pLits[0] );
            pLits[1] = lit_neg( pLits[1] );
            RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
            assert( RetValue );
/*
            if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
            {
                RetValue = sat_solver_simplify(p->pMSat->pSat);
                assert( RetValue != 0 );
            }
*/
        }
        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->pFrames) )
    {
        p->nSatProof++;
        return 1;
    }

    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
    nLits = 2;
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
    pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase );
    if ( p->iOutputLit > -1 )
        pLits[nLits++] = p->iOutputLit;
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }

    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        assert( RetValue != 0 );
    }

clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
        (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;
        if ( nLits == 2 )
        {
            pLits[0] = lit_neg( pLits[0] );
            pLits[1] = lit_neg( pLits[1] );
            RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
            assert( RetValue );
/*
            if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
            {
                RetValue = sat_solver_simplify(p->pMSat->pSat);
                assert( RetValue != 0 );
            }
*/
        }
        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* Ssw_ObjChild0Fra ( Ssw_Man_t *  p, Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 185 of file sswInt.h.

{ assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }

static Aig_Obj_t* Ssw_ObjChild0Fra_ ( Ssw_Frm_t *  p, Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 191 of file sswInt.h.

{ assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }

static Aig_Obj_t* Ssw_ObjChild1Fra ( Ssw_Man_t *  p, Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 186 of file sswInt.h.

{ assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }

static Aig_Obj_t* Ssw_ObjChild1Fra_ ( Ssw_Frm_t *  p, Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 192 of file sswInt.h.

{ assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }

static Aig_Obj_t* Ssw_ObjFrame ( Ssw_Man_t *  p, Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 182 of file sswInt.h.

{ return p->pNodeToFrames[p->nFrames*pObj->Id + i];  }

static Aig_Obj_t* Ssw_ObjFrame_ ( Ssw_Frm_t *  p, Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 188 of file sswInt.h.

{ return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     }

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

inlinestatic

Definition at line 172 of file sswInt.h.

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

static int Ssw_ObjSatNum ( Ssw_Sat_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 169 of file sswInt.h.

{ return Vec_IntGetEntry( p->vSatVars, pObj->Id );  }

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

inlinestatic

Definition at line 176 of file sswInt.h.

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

static void Ssw_ObjSetFrame ( Ssw_Man_t *  p, Aig_Obj_t *  pObj, int  i, Aig_Obj_t *  pNode  )

inlinestatic

Definition at line 183 of file sswInt.h.

{ p->pNodeToFrames[p->nFrames*pObj->Id + i] = pNode; }

static void Ssw_ObjSetFrame_ ( Ssw_Frm_t *  p, Aig_Obj_t *  pObj, int  i, Aig_Obj_t *  pNode  )

inlinestatic

Definition at line 189 of file sswInt.h.

{ Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );     }

static void Ssw_ObjSetSatNum ( Ssw_Sat_t *  p, Aig_Obj_t *  pObj, int  Num  )

inlinestatic

Definition at line 170 of file sswInt.h.

{ Vec_IntSetEntry(p->vSatVars, pObj->Id, Num);      }

Ssw_Sat_t* Ssw_SatStart

(

int

fPolarFlip

)

DECLARATIONS ///.

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

FileName [sswCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Computation of CNF.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswCnf.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswCnf.c.

{
    Ssw_Sat_t * p;
    int Lit;
    p = ABC_ALLOC( Ssw_Sat_t, 1 );
    memset( p, 0, sizeof(Ssw_Sat_t) );
    p->pAig          = NULL;
    p->fPolarFlip    = fPolarFlip;
    p->vSatVars      = Vec_IntStart( 10000 );
    p->vFanins       = Vec_PtrAlloc( 100 );
    p->vUsedPis      = Vec_PtrAlloc( 100 );
    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;
    Lit = toLit( p->nSatVars );
    if ( fPolarFlip )
        Lit = lit_neg( Lit );
    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
//    Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
    Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
    return p;
}

void Ssw_SatStop

(

Ssw_Sat_t *

p

)

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

Synopsis [Stop the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file sswCnf.c.

{
//    Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n", 
//        p->pSat->size, p->pSat->stats.starts );
    if ( p->pSat )
        sat_solver_delete( p->pSat );
    Vec_IntFree( p->vSatVars );
    Vec_PtrFree( p->vFanins );
    Vec_PtrFree( p->vUsedPis );
    ABC_FREE( p );
}

Aig_Man_t* Ssw_SignalCorrespondenceRefine

(

Ssw_Man_t *

p

)

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

Synopsis [Performs computation of signal correspondence with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 234 of file sswCore.c.

{
    int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
    Aig_Man_t * pAigNew;
    int RetValue, nIter = -1;
    abctime clk, clkTotal = Abc_Clock();
    // get the starting stats
    p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
    p->nRegsBeg  = Aig_ManRegNum(p->pAig);
    // refine classes using BMC
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Before BMC: " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    if ( !p->pPars->fLatchCorr )
    {
        p->pMSat = Ssw_SatStart( 0 );
        if ( p->pPars->fConstrs )
            Ssw_ManSweepBmcConstr( p );
        else
            Ssw_ManSweepBmc( p );
        Ssw_SatStop( p->pMSat );
        p->pMSat = NULL;
        Ssw_ManCleanup( p );
    }
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "After  BMC: " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    // apply semi-formal filtering
/*
    if ( p->pPars->fSemiFormal )
    {
        Aig_Man_t * pSRed;
        Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose );
//        Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose );
        pSRed = Ssw_SpeculativeReduction( p );
        Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
        Aig_ManStop( pSRed );
    }
*/
    if ( p->pPars->pFunc )
    {
        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
    }
    if ( p->pPars->nStepsMax == 0 )
    {
        Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
        goto finalize;
    }
    // refine classes using induction
    nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
    for ( nIter = 0; ; nIter++ )
    {
        if ( p->pPars->nStepsMax == nIter )
        {
            Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter );
            goto finalize;
        }
        if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
        {
            Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
            Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
            Aig_ManStop( pSRed );
            Abc_Print( 1, "Iterative refinement is stopped before iteration %d.\n", nIter );
            Abc_Print( 1, "The network is reduced using candidate equivalences.\n" );
            Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
            Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" );
            break;
        }

clk = Abc_Clock();
        p->pMSat = Ssw_SatStart( 0 );
        if ( p->pPars->fLatchCorrOpt )
        {
            RetValue = Ssw_ManSweepLatch( p );
            if ( p->pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
                    p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
                    p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
                ABC_PRT( "T", Abc_Clock() - clk );
            }
        }
        else
        {
            if ( p->pPars->fConstrs )
                RetValue = Ssw_ManSweepConstr( p );
            else if ( p->pPars->fDynamic )
                RetValue = Ssw_ManSweepDyn( p );
            else
                RetValue = Ssw_ManSweep( p );

            p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
            if ( p->pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
                if ( p->pPars->fDynamic )
                {
                    Abc_Print( 1, "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
                    Abc_Print( 1, "R =%4d. ",   p->nRecycles-nRecycles );
                }
                Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
                    (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
                ABC_PRT( "T", Abc_Clock() - clk );
            }
//            if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
//                p->pPars->nBTLimit = 10000;

            if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) )
            {
                printf( "Iterative refinement is stopped after iteration %d\n", nIter );
                printf( "because the property output is no longer a candidate constant.\n" );
                // prepare to quite
                p->nLitsEnd  = p->nLitsBeg;
                p->nNodesEnd = p->nNodesBeg;
                p->nRegsEnd  = p->nRegsBeg;
                // cleanup
                Ssw_SatStop( p->pMSat );
                p->pMSat = NULL;
                Ssw_ManCleanup( p );
                // cleanup
                Aig_ManSetPhase( p->pAig );
                Aig_ManCleanMarkB( p->pAig );
                return Aig_ManDupSimple( p->pAig );
            }
        }
        nSatProof     = p->nSatProof;
        nSatCallsSat  = p->nSatCallsSat;
        nRecycles     = p->nRecycles;
        nSatFailsReal = p->nSatFailsReal;
        nUniques      = p->nUniques;

        p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
        p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
        Ssw_SatStop( p->pMSat );
        p->pMSat = NULL;
        Ssw_ManCleanup( p );
        if ( !RetValue )
            break;
        if ( p->pPars->pFunc )
            ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
    }

finalize:
    p->pPars->nIters = nIter + 1;
p->timeTotal = Abc_Clock() - clkTotal;

    Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
    Aig_ManSeqCleanup( pAigNew );
//Ssw_ClassesPrint( p->ppClasses, 1 );
    // get the final stats
    p->nLitsEnd  = Ssw_ClassesLitNum( p->ppClasses );
    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
    // cleanup
    Aig_ManSetPhase( p->pAig );
    Aig_ManCleanMarkB( p->pAig );
    return pAigNew;
}

void Ssw_SmlAssignDist1Plus	(	Ssw_Sml_t *	p,
		unsigned *	pPat
	)

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

Synopsis [Assings distance-1 simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 674 of file sswSim.c.

{
    Aig_Obj_t * pObj;
    int f, i, Limit;
    assert( p->nFrames > 0 );

    // copy the pattern into the primary inputs
    Aig_ManForEachCi( p->pAig, pObj, i )
        Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );

    // set distance one PIs for the first frame
    Limit = Abc_MinInt( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
    for ( i = 0; i < Limit; i++ )
        Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ), i+1 );

    // create random info for the remaining timeframes
    for ( f = 1; f < p->nFrames; f++ )
        Saig_ManForEachPi( p->pAig, pObj, i )
            Ssw_SmlAssignRandomFrame( p, pObj, f );
}

void Ssw_SmlAssignRandomFrame	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj,
		int	iFrame
	)

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

Synopsis [Assigns random patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 538 of file sswSim.c.

{
    unsigned * pSims;
    int i;
    assert( iFrame < p->nFrames );
    assert( Aig_ObjIsCi(pObj) );
    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
    for ( i = 0; i < p->nWordsFrame; i++ )
        pSims[i] = Ssw_ObjRandomSim();
}

void Ssw_SmlClean

(

Ssw_Sml_t *

p

)

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1173 of file sswSim.c.

{
    memset( p->pData, 0, sizeof(unsigned) * Aig_ManObjNumMax(p->pAig) * p->nWordsTotal );
}

void Ssw_SmlObjAssignConst	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj,
		int	fConst1,
		int	iFrame
	)

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file sswSim.c.

{
    unsigned * pSims;
    int i;
    assert( iFrame < p->nFrames );
    assert( Aig_ObjIsCi(pObj) );
    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
    for ( i = 0; i < p->nWordsFrame; i++ )
        pSims[i] = fConst1? ~(unsigned)0 : 0;
}

unsigned Ssw_SmlObjHashWord	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes hash value of the node using its simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file sswSim.c.

{
    static int s_SPrimes[128] = {
        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
    };
    unsigned * pSims;
    unsigned uHash;
    int i;
//    assert( p->nWordsTotal <= 128 );
    uHash = 0;
    pSims = Ssw_ObjSim(p, pObj->Id);
    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
        uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
    return uHash;
}

int Ssw_SmlObjIsConstBit	(	void *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Returns 1 if the node appears to be constant 1 candidate.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file sswSim.c.

{
    return pObj->fPhase == pObj->fMarkB;
}

int Ssw_SmlObjIsConstWord	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file sswSim.c.

{
    unsigned * pSims;
    int i;
    pSims = Ssw_ObjSim(p, pObj->Id);
    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
        if ( pSims[i] )
            return 0;
    return 1;
}

int Ssw_SmlObjsAreEqualBit	(	void *	p,
		Aig_Obj_t *	pObj0,
		Aig_Obj_t *	pObj1
	)

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

Synopsis [Returns 1 if the nodes appear equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file sswSim.c.

{
    return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
}

int Ssw_SmlObjsAreEqualWord	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj0,
		Aig_Obj_t *	pObj1
	)

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 124 of file sswSim.c.

{
    unsigned * pSims0, * pSims1;
    int i;
    pSims0 = Ssw_ObjSim(p, pObj0->Id);
    pSims1 = Ssw_ObjSim(p, pObj1->Id);
    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
        if ( pSims0[i] != pSims1[i] )
            return 0;
    return 1;
}

void Ssw_SmlObjSetWord	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj,
		unsigned	Word,
		int	iWord,
		int	iFrame
	)

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 603 of file sswSim.c.

{
    unsigned * pSims;
    assert( iFrame < p->nFrames );
    assert( Aig_ObjIsCi(pObj) );
    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
    pSims[iWord] = Word;
}

void Ssw_SmlResimulateSeq

(

Ssw_Sml_t *

p

)

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

Synopsis [Performs next round of sequential simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1269 of file sswSim.c.

{
    Ssw_SmlReinitialize( p );
    Ssw_SmlSimulateOne( p );
    p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
}

void Ssw_SmlSavePatternAig	(	Ssw_Man_t *	p,
		int	f
	)

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file sswSweep.c.

{
    Aig_Obj_t * pObj;
    int i;
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
    Aig_ManForEachCi( p->pAig, pObj, i )
        if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
            Abc_InfoSetBit( p->pPatWords, i );
}

void Ssw_SmlSimulateOne

(

Ssw_Sml_t *

p

)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1005 of file sswSim.c.

{
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int f, i;
    abctime clk;
clk = Abc_Clock();
    for ( f = 0; f < p->nFrames; f++ )
    {
        // simulate the nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
            Ssw_SmlNodeSimulate( p, pObj, f );
        // copy simulation info into outputs
        Saig_ManForEachPo( p->pAig, pObj, i )
            Ssw_SmlNodeCopyFanin( p, pObj, f );
        // copy simulation info into outputs
        Saig_ManForEachLi( p->pAig, pObj, i )
            Ssw_SmlNodeCopyFanin( p, pObj, f );
        // quit if this is the last timeframe
        if ( f == p->nFrames - 1 )
            break;
        // copy simulation info into the inputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
            Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
    }
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}

void Ssw_SmlSimulateOneDyn_rec	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj,
		int	f,
		int *	pVisited,
		int	nVisCounter
	)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1076 of file sswSim.c.

{
//    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
//        return;
//    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
    if ( pVisited[p->nFrames*pObj->Id+f] == nVisCounter )
        return;
    pVisited[p->nFrames*pObj->Id+f] = nVisCounter;
    if ( Saig_ObjIsPi( p->pAig, pObj ) || Aig_ObjIsConst1(pObj) )
        return;
    if ( Saig_ObjIsLo( p->pAig, pObj ) )
    {
        if ( f == 0 )
            return;
        Ssw_SmlSimulateOneDyn_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1, pVisited, nVisCounter );
        Ssw_SmlNodeTransferNext( p, Saig_ObjLoToLi(p->pAig, pObj), pObj, f-1 );
        return;
    }
    if ( Saig_ObjIsLi( p->pAig, pObj ) )
    {
        Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
        Ssw_SmlNodeCopyFanin( p, pObj, f );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
    Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin1(pObj), f, pVisited, nVisCounter );
    Ssw_SmlNodeSimulate( p, pObj, f );
}

void Ssw_SmlSimulateOneFrame

(

Ssw_Sml_t *

p

)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1117 of file sswSim.c.

{
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i;
    abctime clk;
clk = Abc_Clock();
    // simulate the nodes
    Aig_ManForEachNode( p->pAig, pObj, i )
        Ssw_SmlNodeSimulate( p, pObj, 0 );
    // copy simulation info into outputs
    Saig_ManForEachLi( p->pAig, pObj, i )
        Ssw_SmlNodeCopyFanin( p, pObj, 0 );
    // copy simulation info into the inputs
    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
        Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}

Ssw_Sml_t* Ssw_SmlStart	(	Aig_Man_t *	pAig,
		int	nPref,
		int	nFrames,
		int	nWordsFrame
	)

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1148 of file sswSim.c.

{
    Ssw_Sml_t * p;
    p = (Ssw_Sml_t *)ABC_ALLOC( char, sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
    memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
    p->pAig        = pAig;
    p->nPref       = nPref;
    p->nFrames     = nPref + nFrames;
    p->nWordsFrame = nWordsFrame;
    p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
    p->nWordsPref  = nPref * nWordsFrame;
    return p;
}

void Ssw_SmlStop

(

Ssw_Sml_t *

p

)

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1211 of file sswSim.c.

{
    ABC_FREE( p );
}

Aig_Man_t* Ssw_SpeculativeReduction

(

Ssw_Man_t *

p

)

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 212 of file sswAig.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    p->nConstrTotal = p->nConstrReduced = 0;

    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
    pFrames->pName = Abc_UtilStrsav( p->pAig->pName );
    // map constants and PIs
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // set the constraints on the latch outputs
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    // add internal nodes of this frame
    Aig_ManForEachNode( p->pAig, pObj, i )
    {
        pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
        Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    }
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLi( p->pAig, pObj, i )
        Aig_ObjCreateCo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
//    Abc_Print( 1, "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", 
//        p->nConstrTotal, p->nConstrReduced );
    return pFrames;
}

void Ssw_UniqueRegisterPairInfo

(

Ssw_Man_t *

p

)

DECLARATIONS ///.

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

FileName [sswSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [On-demand uniqueness constraints.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Performs computation of signal correspondence with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswUnique.c.

{
    Aig_Obj_t * pObjLo, * pObj0, * pObj1;
    int i, RetValue, Counter;
    if ( p->vDiffPairs == NULL )
        p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) );
    Vec_IntClear( p->vDiffPairs );
    Saig_ManForEachLo( p->pAig, pObjLo, i )
    {
        pObj0 = Ssw_ObjFrame( p, pObjLo, 0 );
        pObj1 = Ssw_ObjFrame( p, pObjLo, 1 );
        if ( pObj0 == pObj1 )
            Vec_IntPush( p->vDiffPairs, 0 );
        else if ( pObj0 == Aig_Not(pObj1) )
            Vec_IntPush( p->vDiffPairs, 1 );
//        else
//            Vec_IntPush( p->vDiffPairs, 1 );
        else if ( Aig_ObjPhaseReal(pObj0) != Aig_ObjPhaseReal(pObj1) )
            Vec_IntPush( p->vDiffPairs, 1 );
        else
        {
            RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObj0), Aig_Regular(pObj1) );
            Vec_IntPush( p->vDiffPairs, RetValue!=1 );
        }
    }
    assert( Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
    // count the number of ones
    Counter = 0;
    Vec_IntForEachEntry( p->vDiffPairs, RetValue, i )
        Counter += RetValue;
//    Abc_Print( 1, "The number of different register pairs = %d.\n", Counter );
}