fra.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "aig/aig/aig.h"
#include "opt/dar/dar.h"
#include "sat/bsat/satSolver.h"
#include "aig/ioa/ioa.h"

Go to the source code of this file.

Data Structures
struct	Fra_Par_t_
struct	Fra_Ssw_t_
struct	Fra_Sec_t_
struct	Fra_Cla_t_
struct	Fra_Sml_t_
struct	Fra_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_	Fra_Par_t
	INCLUDES ///. More...
typedef struct Fra_Ssw_t_	Fra_Ssw_t
typedef struct Fra_Sec_t_	Fra_Sec_t
typedef struct Fra_Man_t_	Fra_Man_t
typedef struct Fra_Cla_t_	Fra_Cla_t
typedef struct Fra_Sml_t_	Fra_Sml_t
typedef struct Fra_Bmc_t_	Fra_Bmc_t

Functions
static unsigned *	Fra_ObjSim (Fra_Sml_t *p, int Id)
	MACRO DEFINITIONS ///. More...
static unsigned	Fra_ObjRandomSim ()
static Aig_Obj_t *	Fra_ObjFraig (Aig_Obj_t *pObj, int i)
static void	Fra_ObjSetFraig (Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
static Vec_Ptr_t *	Fra_ObjFaninVec (Aig_Obj_t *pObj)
static void	Fra_ObjSetFaninVec (Aig_Obj_t *pObj, Vec_Ptr_t *vFanins)
static int	Fra_ObjSatNum (Aig_Obj_t *pObj)
static void	Fra_ObjSetSatNum (Aig_Obj_t *pObj, int Num)
static Aig_Obj_t *	Fra_ClassObjRepr (Aig_Obj_t *pObj)
static void	Fra_ClassObjSetRepr (Aig_Obj_t *pObj, Aig_Obj_t *pNode)
static Aig_Obj_t *	Fra_ObjChild0Fra (Aig_Obj_t *pObj, int i)
static Aig_Obj_t *	Fra_ObjChild1Fra (Aig_Obj_t *pObj, int i)
static int	Fra_ImpLeft (int Imp)
static int	Fra_ImpRight (int Imp)
static int	Fra_ImpCreate (int Left, int Right)
int	Fra_FraigSat (Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
	ITERATORS ///. More...
int	Fra_FraigCec (Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
int	Fra_FraigCecPartitioned (Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
int	Fra_BmcNodeIsConst (Aig_Obj_t *pObj)
int	Fra_BmcNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
	FUNCTION DEFINITIONS ///. More...
void	Fra_BmcStop (Fra_Bmc_t *p)
void	Fra_BmcPerform (Fra_Man_t *p, int nPref, int nDepth)
void	Fra_BmcPerformSimple (Aig_Man_t *pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose)
Fra_Cla_t *	Fra_ClassesStart (Aig_Man_t *pAig)
	FUNCTION DEFINITIONS ///. More...
void	Fra_ClassesStop (Fra_Cla_t *p)
void	Fra_ClassesCopyReprs (Fra_Cla_t *p, Vec_Ptr_t *vFailed)
void	Fra_ClassesPrint (Fra_Cla_t *p, int fVeryVerbose)
void	Fra_ClassesPrepare (Fra_Cla_t *p, int fLatchCorr, int nMaxLevs)
int	Fra_ClassesRefine (Fra_Cla_t *p)
int	Fra_ClassesRefine1 (Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
int	Fra_ClassesCountLits (Fra_Cla_t *p)
int	Fra_ClassesCountPairs (Fra_Cla_t *p)
void	Fra_ClassesTest (Fra_Cla_t *p, int Id1, int Id2)
void	Fra_ClassesLatchCorr (Fra_Man_t *p)
void	Fra_ClassesPostprocess (Fra_Cla_t *p)
void	Fra_ClassesSelectRepr (Fra_Cla_t *p)
Aig_Man_t *	Fra_ClassesDeriveAig (Fra_Cla_t *p, int nFramesK)
void	Fra_CnfNodeAddToSolver (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
void	Fra_FraigSweep (Fra_Man_t *pManAig)
int	Fra_FraigMiterStatus (Aig_Man_t *p)
	DECLARATIONS ///. More...
int	Fra_FraigMiterAssertedOutput (Aig_Man_t *p)
Aig_Man_t *	Fra_FraigPerform (Aig_Man_t *pManAig, Fra_Par_t *pPars)
Aig_Man_t *	Fra_FraigChoice (Aig_Man_t *pManAig, int nConfMax, int nLevelMax)
Aig_Man_t *	Fra_FraigEquivence (Aig_Man_t *pManAig, int nConfMax, int fProve)
Vec_Int_t *	Fra_OneHotCompute (Fra_Man_t *p, Fra_Sml_t *pSim)
void	Fra_OneHotAssume (Fra_Man_t *p, Vec_Int_t *vOneHots)
void	Fra_OneHotCheck (Fra_Man_t *p, Vec_Int_t *vOneHots)
int	Fra_OneHotRefineUsingCex (Fra_Man_t *p, Vec_Int_t *vOneHots)
int	Fra_OneHotCount (Fra_Man_t *p, Vec_Int_t *vOneHots)
void	Fra_OneHotEstimateCoverage (Fra_Man_t *p, Vec_Int_t *vOneHots)
Aig_Man_t *	Fra_OneHotCreateExdc (Fra_Man_t *p, Vec_Int_t *vOneHots)
void	Fra_OneHotAddKnownConstraint (Fra_Man_t *p, Vec_Ptr_t *vOnehots)
Vec_Int_t *	Fra_ImpDerive (Fra_Man_t *p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr)
void	Fra_ImpAddToSolver (Fra_Man_t *p, Vec_Int_t *vImps, int *pSatVarNums)
int	Fra_ImpCheckForNode (Fra_Man_t *p, Vec_Int_t *vImps, Aig_Obj_t *pNode, int Pos)
int	Fra_ImpRefineUsingCex (Fra_Man_t *p, Vec_Int_t *vImps)
void	Fra_ImpCompactArray (Vec_Int_t *vImps)
double	Fra_ImpComputeStateSpaceRatio (Fra_Man_t *p)
int	Fra_ImpVerifyUsingSimulation (Fra_Man_t *p)
void	Fra_ImpRecordInManager (Fra_Man_t *p, Aig_Man_t *pNew)
Aig_Man_t *	Fra_FraigInduction (Aig_Man_t *p, Fra_Ssw_t *pPars)
int	Fra_InvariantVerify (Aig_Man_t *p, int nFrames, Vec_Int_t *vClauses, Vec_Int_t *vLits)
	DECLARATIONS ///. More...
Aig_Man_t *	Fra_FraigLatchCorrespondence (Aig_Man_t *pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int *pnIter, float TimeLimit)
void	Fra_ParamsDefault (Fra_Par_t *pParams)
	DECLARATIONS ///. More...
void	Fra_ParamsDefaultSeq (Fra_Par_t *pParams)
Fra_Man_t *	Fra_ManStart (Aig_Man_t *pManAig, Fra_Par_t *pParams)
void	Fra_ManClean (Fra_Man_t *p, int nNodesMax)
Aig_Man_t *	Fra_ManPrepareComb (Fra_Man_t *p)
void	Fra_ManFinalizeComb (Fra_Man_t *p)
void	Fra_ManStop (Fra_Man_t *p)
void	Fra_ManPrint (Fra_Man_t *p)
int	Fra_NodesAreEquiv (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
	FUNCTION DEFINITIONS ///. More...
int	Fra_NodesAreImp (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
int	Fra_NodesAreClause (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
int	Fra_NodeIsConst (Fra_Man_t *p, Aig_Obj_t *pNew)
void	Fra_SecSetDefaultParams (Fra_Sec_t *p)
	DECLARATIONS ///. More...
int	Fra_FraigSec (Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
int	Fra_SmlNodeHash (Aig_Obj_t *pObj, int nTableSize)
	DECLARATIONS ///. More...
int	Fra_SmlNodeIsConst (Aig_Obj_t *pObj)
int	Fra_SmlNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
int	Fra_SmlNodeNotEquWeight (Fra_Sml_t *p, int Left, int Right)
int	Fra_SmlNodeCountOnes (Fra_Sml_t *p, Aig_Obj_t *pObj)
int	Fra_SmlCheckOutput (Fra_Man_t *p)
void	Fra_SmlSavePattern (Fra_Man_t *p)
void	Fra_SmlSimulate (Fra_Man_t *p, int fInit)
void	Fra_SmlResimulate (Fra_Man_t *p)
Fra_Sml_t *	Fra_SmlStart (Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
void	Fra_SmlStop (Fra_Sml_t *p)
Fra_Sml_t *	Fra_SmlSimulateComb (Aig_Man_t *pAig, int nWords, int fCheckMiter)
Fra_Sml_t *	Fra_SmlSimulateCombGiven (Aig_Man_t *pAig, char *pFileName, int fCheckMiter, int fVerbose)
Fra_Sml_t *	Fra_SmlSimulateSeq (Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Abc_Cex_t *	Fra_SmlGetCounterExample (Fra_Sml_t *p)
Abc_Cex_t *	Fra_SmlCopyCounterExample (Aig_Man_t *pAig, Aig_Man_t *pFrames, int *pModel)

Typedef Documentation

typedef struct Fra_Bmc_t_ Fra_Bmc_t

Definition at line 59 of file fra.h.

typedef struct Fra_Cla_t_ Fra_Cla_t

Definition at line 57 of file fra.h.

typedef struct Fra_Man_t_ Fra_Man_t

Definition at line 56 of file fra.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_ Fra_Par_t

INCLUDES ///.

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

FileName [fra.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [[New FRAIG package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 53 of file fra.h.

typedef struct Fra_Sec_t_ Fra_Sec_t

Definition at line 55 of file fra.h.

typedef struct Fra_Sml_t_ Fra_Sml_t

Definition at line 58 of file fra.h.

typedef struct Fra_Ssw_t_ Fra_Ssw_t

Definition at line 54 of file fra.h.

Function Documentation

int Fra_BmcNodeIsConst

(

Aig_Obj_t *

pObj

)

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

Synopsis [Returns 1 if the node is costant.]

Description []

SideEffects []

SeeAlso []

Definition at line 103 of file fraBmc.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
    return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
}

int Fra_BmcNodesAreEqual	(	Aig_Obj_t *	pObj0,
		Aig_Obj_t *	pObj1
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Returns 1 if the nodes are equivalent.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 of file fraBmc.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
    Aig_Obj_t * pObjFrames0, * pObjFrames1;
    Aig_Obj_t * pObjFraig0, * pObjFraig1;
    int i;
    for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ )
    {
        pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) );
        pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) );
        if ( pObjFrames0 == pObjFrames1 )
            continue;
        pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) );
        pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) );
        if ( pObjFraig0 != pObjFraig1 )
            return 0;
    }
    return 1;
}

void Fra_BmcPerform	(	Fra_Man_t *	p,
		int	nPref,
		int	nDepth
	)

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file fraBmc.c.

{
    Aig_Obj_t * pObj;
    int i, nImpsOld = 0;
    abctime clk = Abc_Clock();
    assert( p->pBmc == NULL );
    // derive and fraig the frames
    p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
    p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 );
    // if implications are present, configure the AIG manager to check them
    if ( p->pCla->vImps )
    {
        p->pBmc->pAigFrames->pImpFunc = (void (*) (void*, void*))Fra_BmcFilterImplications;
        p->pBmc->pAigFrames->pImpData = p->pBmc;
        p->pBmc->vImps = p->pCla->vImps;
        nImpsOld = Vec_IntSize(p->pCla->vImps);
    } 
    p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 );
    p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
    p->pBmc->pAigFrames->pObjCopies = NULL;
    // annotate frames nodes with pointers to the manager
    Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
        pObj->pData = p;
    // report the results
    if ( p->pPars->fVerbose )
    {
        printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d.  ", 
            Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
            Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
        ABC_PRT( "Time", Abc_Clock() - clk );
        printf( "Before BMC: " );  
//        Fra_ClassesPrint( p->pCla, 0 );
        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
        if ( p->pCla->vImps )
            printf( "Imp = %5d. ", nImpsOld );
        printf( "\n" );
    }
    // refine the classes
    p->pCla->pFuncNodeIsConst   = Fra_BmcNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
    Fra_ClassesRefine( p->pCla );
    Fra_ClassesRefine1( p->pCla, 1, NULL );
    p->pCla->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
    // report the results
    if ( p->pPars->fVerbose )
    {
        printf( "After  BMC: " );  
//        Fra_ClassesPrint( p->pCla, 0 );
        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
        if ( p->pCla->vImps )
            printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
        printf( "\n" );
    }
    // free the BMC manager
    Fra_BmcStop( p->pBmc );  
    p->pBmc = NULL;
}

void Fra_BmcPerformSimple	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	nBTLimit,
		int	fRewrite,
		int	fVerbose
	)

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file fraBmc.c.

{
    extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig );
    Fra_Man_t * pTemp;
    Fra_Bmc_t * pBmc;
    Aig_Man_t * pAigTemp;
    abctime clk;
    int iOutput;
    // derive and fraig the frames
    clk = Abc_Clock();
    pBmc = Fra_BmcStart( pAig, 0, nFrames );
    pTemp = Fra_LcrAigPrepare( pAig );
    pTemp->pBmc = pBmc;
    pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 );
    if ( fVerbose )
    {
        printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
            Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
            nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames), 
            Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    if ( fRewrite )
    {
        clk = Abc_Clock();
        pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
        Aig_ManStop( pAigTemp );
        if ( fVerbose )
        {
            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }
    clk = Abc_Clock();
    iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
    if ( iOutput >= 0 )
        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
    else
    {
        pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
        iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
        if ( pBmc->pAigFraig->pData )
        {
            pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, (int *)pBmc->pAigFraig->pData );
            ABC_FREE( pBmc->pAigFraig->pData );
        }
        else if ( iOutput >= 0 )
            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
    }
    if ( fVerbose )
    {
        printf( "Fraiged init frames: Node = %6d. Lev = %5d.  ", 
            pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1,
            pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    Fra_BmcStop( pBmc );  
    ABC_FREE( pTemp );
}

void Fra_BmcStop

(

Fra_Bmc_t *

p

)

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

Synopsis [Stops the BMC manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file fraBmc.c.

{
    Aig_ManStop( p->pAigFrames );
    if ( p->pAigFraig )
        Aig_ManStop( p->pAigFraig );
    ABC_FREE( p->pObjToFrames );
    ABC_FREE( p->pObjToFraig );
    ABC_FREE( p );
}

void Fra_ClassesCopyReprs	(	Fra_Cla_t *	p,
		Vec_Ptr_t *	vFailed
	)

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file fraClass.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
    memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
    {
        Aig_ManForEachObj( p->pAig, pObj, i )
        {
            if ( p->pAig->pReprs[i] != NULL )
                printf( "Classes are not cleared!\n" );
            assert( p->pAig->pReprs[i] == NULL );
        }
    }
    if ( vFailed )
        Vec_PtrForEachEntry( Aig_Obj_t *, vFailed, pObj, i )
            p->pAig->pReprs[pObj->Id] = NULL;
}

int Fra_ClassesCountLits

(

Fra_Cla_t *

p

)

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

Synopsis [Count the number of literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    int i, nNodes, nLits = 0;
    nLits = Vec_PtrSize( p->vClasses1 );
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        nNodes = Fra_ClassCount( pClass );
        assert( nNodes > 1 );
        nLits += nNodes - 1;
    }
    return nLits;
}

int Fra_ClassesCountPairs

(

Fra_Cla_t *

p

)

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

Synopsis [Count the number of pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    int i, nNodes, nPairs = 0;
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        nNodes = Fra_ClassCount( pClass );
        assert( nNodes > 1 );
        nPairs += nNodes * (nNodes - 1) / 2;
    }
    return nPairs;
}

Aig_Man_t* Fra_ClassesDeriveAig	(	Fra_Cla_t *	p,
		int	nFramesK
	)

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

Synopsis [Derives AIG for the partitioned problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 796 of file fraClass.c.

{
    Aig_Man_t * pManFraig;
    Aig_Obj_t * pObj, * pObjNew;
    Aig_Obj_t ** pLatches, ** ppEquivs;
    int i, k, f, nFramesAll = nFramesK + 1;
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    assert( nFramesK > 0 );
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
    pManFraig->pName = Abc_UtilStrsav( p->pAig->pName );
    pManFraig->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
    // allocate place for the node mapping
    ppEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
    // create latches for the first frame
    Aig_ManForEachLoSeq( p->pAig, pObj, i )
        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
    // add timeframes
    pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
    for ( f = 0; f < nFramesAll; f++ )
    {
        // create PIs for this frame
        Aig_ManForEachPiSeq( p->pAig, pObj, i )
            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
        // set the constraints on the latch outputs
        Aig_ManForEachLoSeq( p->pAig, pObj, i )
            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
        }
        if ( f == nFramesAll - 1 )
            break;
        if ( f == nFramesAll - 2 )
            pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
        // save the latch input values
        k = 0;
        Aig_ManForEachLiSeq( p->pAig, pObj, i )
            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
        // insert them to the latch output values
        k = 0;
        Aig_ManForEachLoSeq( p->pAig, pObj, i )
            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
    }
    ABC_FREE( pLatches );
    ABC_FREE( ppEquivs );
    // mark the asserts
    assert( Aig_ManCoNum(pManFraig) % nFramesAll == 0 );
printf( "Assert miters = %6d. Output miters = %6d.\n", 
       pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts );
    // remove dangling nodes
    Aig_ManCleanup( pManFraig );
    return pManFraig;
}

void Fra_ClassesLatchCorr

(

Fra_Man_t *

p

)

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

Synopsis [Creates latch correspondence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 615 of file fraClass.c.

{
    Aig_Obj_t * pObj;
    int i, nEntries = 0;
    Vec_PtrClear( p->pCla->vClasses1 );
    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
    {
        Vec_PtrPush( p->pCla->vClasses1, pObj );
        Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
    }
    // allocate room for classes
    p->pCla->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
    p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
}

void Fra_ClassesPostprocess

(

Fra_Cla_t *

p

)

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

Synopsis [Postprocesses the classes by removing half of the less useful.]

Description []

SideEffects []

SeeAlso []

Definition at line 641 of file fraClass.c.

{
    int Ratio = 2;
    Fra_Sml_t * pComb;
    Aig_Obj_t * pObj, * pRepr, ** ppClass;
    int * pWeights, WeightMax = 0, i, k, c;
    // perform combinational simulation
    pComb = Fra_SmlSimulateComb( p->pAig, 32, 0 );
    // compute the weight of each node in the classes
    pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
    memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
    Aig_ManForEachObj( p->pAig, pObj, i )
    { 
        pRepr = Fra_ClassObjRepr( pObj );
        if ( pRepr == NULL )
            continue;
        pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
        WeightMax = Abc_MaxInt( WeightMax, pWeights[i] );
    }
    Fra_SmlStop( pComb );
    printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
    // remove nodes from classes whose weight is less than WeightMax/Ratio
    k = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
    {
        if ( pWeights[pObj->Id] >= WeightMax/Ratio )
            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
        else
            Fra_ClassObjSetRepr( pObj, NULL );
    }
    Vec_PtrShrink( p->vClasses1, k );
    // in each class, compact the nodes
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
    {
        k = 1;
        for ( c = 1; ppClass[c]; c++ )
        {
            if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
                ppClass[k++] = ppClass[c];
            else
                Fra_ClassObjSetRepr( ppClass[c], NULL );
        }
        ppClass[k] = NULL;
    }
    // remove classes with only repr
    k = 0;
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
        if ( ppClass[1] != NULL )
            Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
    Vec_PtrShrink( p->vClasses, k );
    printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
    ABC_FREE( pWeights );
}

void Fra_ClassesPrepare	(	Fra_Cla_t *	p,
		int	fLatchCorr,
		int	nMaxLevs
	)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 276 of file fraClass.c.

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

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

    // add all the nodes to the hash table
    Vec_PtrClear( p->vClasses1 );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Aig_ObjIsCi(pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                continue;
        }
        // hash the node by its simulation info
        iEntry = p->pFuncNodeHash( pObj, nTableSize );
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( pObj ) )
        {
            Vec_PtrPush( p->vClasses1, pObj );
            Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
            continue;
        }
        // add the node to the class
        if ( ppTable[iEntry] == NULL )
        {
            ppTable[iEntry] = pObj;
            Fra_ObjSetNext( ppNexts, pObj, pObj );
        }
        else
        {
            Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
            Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
        }
    }

    // count the total number of nodes in the non-trivial classes
    // mark the representative nodes of each equivalence class
    nEntries = 0;
    for ( i = 0; i < nTableSize; i++ )
        if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
        {
            for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 
                  pTemp != ppTable[i]; 
                  pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
            assert( k > 1 );
            nEntries += k;
            // mark the node
            assert( ppTable[i]->fMarkA == 0 );
            ppTable[i]->fMarkA = 1;
        }

    // allocate room for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
    p->pMemClassesFree = p->pMemClasses + 2*nEntries;
 
    // copy the entries into storage in the topological order
    Vec_PtrClear( p->vClasses );
    nEntries = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
            continue;
        // skip the nodes that are not representatives of non-trivial classes
        if ( pObj->fMarkA == 0 )
            continue;
        pObj->fMarkA = 0;
        // add the class of nodes
        Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
        // count the number of entries in this class
        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
              pTemp != pObj; 
              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
        nNodes = k;
        assert( nNodes > 1 );
        // add the nodes to the class in the topological order
        p->pMemClasses[2*nEntries] = pObj;
        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
              pTemp != pObj; 
              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
        {
            p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
            Fra_ClassObjSetRepr( pTemp, pObj );
        }
        // add as many empty entries
        p->pMemClasses[2*nEntries + nNodes] = NULL;
        // increment the number of entries
        nEntries += k;
    }
    ABC_FREE( ppTable );
    ABC_FREE( ppNexts );
    // now it is time to refine the classes
    Fra_ClassesRefine( p );
//    Fra_ClassesPrint( p, 0 );
}

void Fra_ClassesPrint	(	Fra_Cla_t *	p,
		int	fVeryVerbose
	)

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    Aig_Obj_t * pObj;
    int i;

    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
        Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
    printf( "\n" );

    if ( fVeryVerbose )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
            assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
        printf( "Constants { " );
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
            printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
        printf( "}\n" );
        Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
        {
            printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
            Fra_PrintClass( p, pClass );
        }
        printf( "\n" );
    }
}

int Fra_ClassesRefine

(

Fra_Cla_t *

p

)

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

Synopsis [Refines the classes after simulation.]

Description [Assumes that simulation info is assigned. Returns the number of classes refined.]

SideEffects []

SeeAlso []

Definition at line 493 of file fraClass.c.

{
    Vec_Ptr_t * vTemp;
    Aig_Obj_t ** pClass;
    int i, nRefis;
    // refine the classes
    nRefis = 0;
    Vec_PtrClear( p->vClassesTemp );
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        // add the class to the new array
        assert( pClass[0] != NULL );
        Vec_PtrPush( p->vClassesTemp, pClass );
        // refine the class iteratively
        nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
    }
    // exchange the class representation
    vTemp = p->vClassesTemp;
    p->vClassesTemp = p->vClasses;
    p->vClasses = vTemp;
    return nRefis;
}

int Fra_ClassesRefine1	(	Fra_Cla_t *	p,
		int	fRefineNewClass,
		int *	pSkipped
	)

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

Synopsis [Refines constant 1 equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 527 of file fraClass.c.

{
    Aig_Obj_t * pObj, ** ppClass;
    int i, k, nRefis = 1;
    // check if there is anything to refine
    if ( Vec_PtrSize(p->vClasses1) == 0 )
        return 0;
    // make sure constant 1 class contains only non-constant nodes
    assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
    // collect all the nodes to be refined
    k = 0;
    Vec_PtrClear( p->vClassNew );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
    {
        if ( p->pFuncNodeIsConst( pObj ) )
            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
        else 
            Vec_PtrPush( p->vClassNew, pObj );
    }
    Vec_PtrShrink( p->vClasses1, k );
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
/*
    printf( "Refined const-1 class: {" );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
        printf( " %d", pObj->Id );
    printf( " }\n" );
*/
    if ( Vec_PtrSize(p->vClassNew) == 1 )
    {
        Fra_ClassObjSetRepr( (Aig_Obj_t *)Vec_PtrEntry(p->vClassNew,0), NULL );
        return 1;
    }
    // create a new class composed of these nodes
    ppClass = p->pMemClassesFree;
    p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        ppClass[i] = pObj;
        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
    }
    assert( ppClass[0] != NULL );
    Vec_PtrPush( p->vClasses, ppClass );
    // iteratively refine this class
    if ( fRefineNewClass )
        nRefis += Fra_RefineClassLastIter( p, p->vClasses );
    else if ( pSkipped )
        (*pSkipped)++;
    return nRefis;
}

void Fra_ClassesSelectRepr

(

Fra_Cla_t *

p

)

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

Synopsis [Postprocesses the classes by selecting representative lowest in top order.]

Description []

SideEffects []

SeeAlso []

Definition at line 706 of file fraClass.c.

{
    Aig_Obj_t ** pClass, * pNodeMin;
    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
    // reassign representatives in each class
    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
    {
        // collect support sizes and find the min-support node
        cMinSupp = -1;
        pNodeMin = NULL;
        nSuppSizeMin = ABC_INFINITY;
        for ( c = 0; pClass[c]; c++ )
        {
            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
//            nSuppSizeCur = 1;
            if ( nSuppSizeMin > nSuppSizeCur || 
                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
            {
                nSuppSizeMin = nSuppSizeCur;
                pNodeMin = pClass[c];
                cMinSupp = c; 
            }
        }
        // skip the case when the repr did not change
        if ( cMinSupp == 0 )
            continue;
        // make the new node the representative of the class
        pClass[cMinSupp] = pClass[0];
        pClass[0] = pNodeMin;
        // set the representative
        for ( c = 0; pClass[c]; c++ )
            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
    }
}

Fra_Cla_t* Fra_ClassesStart

(

Aig_Man_t *

pAig

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file fraClass.c.

{
    Fra_Cla_t * p;
    p = ABC_ALLOC( Fra_Cla_t, 1 );
    memset( p, 0, sizeof(Fra_Cla_t) );
    p->pAig = pAig;
    p->pMemRepr  = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
    p->vClasses     = Vec_PtrAlloc( 100 );
    p->vClasses1    = Vec_PtrAlloc( 100 );
    p->vClassesTemp = Vec_PtrAlloc( 100 );
    p->vClassOld    = Vec_PtrAlloc( 100 );
    p->vClassNew    = Vec_PtrAlloc( 100 );
    p->pFuncNodeHash      = Fra_SmlNodeHash;
    p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
    p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
    return p;
}

void Fra_ClassesStop

(

Fra_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file fraClass.c.

{
    ABC_FREE( p->pMemClasses );
    ABC_FREE( p->pMemRepr );
    if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
    if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
    if ( p->vClasses )     Vec_PtrFree( p->vClasses );
    if ( p->vImps )        Vec_IntFree( p->vImps );
    ABC_FREE( p );
}

void Fra_ClassesTest	(	Fra_Cla_t *	p,
		int	Id1,
		int	Id2
	)

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

Synopsis [Starts representation of equivalence classes with one class.]

Description []

SideEffects []

SeeAlso []

Definition at line 590 of file fraClass.c.

{
    Aig_Obj_t ** pClass;
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 4 );
    pClass = p->pMemClasses;
    assert( Id1 < Id2 );
    pClass[0] = Aig_ManObj( p->pAig, Id1 );
    pClass[1] = Aig_ManObj( p->pAig, Id2 );
    pClass[2] = NULL;
    pClass[3] = NULL;
    Fra_ClassObjSetRepr( pClass[1], pClass[0] );
    Vec_PtrPush( p->vClasses, pClass );
}

static Aig_Obj_t* Fra_ClassObjRepr ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 269 of file fra.h.

{ return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];  }

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

inlinestatic

Definition at line 270 of file fra.h.

{ ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }

void Fra_CnfNodeAddToSolver	(	Fra_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew
	)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file fraCnf.c.

{ 
    Vec_Ptr_t * vFrontier, * vFanins;
    Aig_Obj_t * pNode, * pFanin;
    int i, k, fUseMuxes = 1;
    assert( pOld || pNew );
    // quit if CNF is ready
    if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
        return;
    // start the frontier
    vFrontier = Vec_PtrAlloc( 100 );
    if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
    if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
    // explore nodes in the frontier
    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
    {
        // create the supergate
        assert( Fra_ObjSatNum(pNode) );
        assert( Fra_ObjFaninVec(pNode) == NULL );
        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
        {
            vFanins = Vec_PtrAlloc( 4 );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Fra_AddClausesMux( p, pNode );
        }
        else
        {
            vFanins = Fra_CollectSuper( pNode, fUseMuxes );
            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Fra_AddClausesSuper( p, pNode, vFanins );
        }
        assert( Vec_PtrSize(vFanins) > 1 );
        Fra_ObjSetFaninVec( pNode, vFanins );
    }
    Vec_PtrFree( vFrontier );
}

int Fra_FraigCec	(	Aig_Man_t **	ppAig,
		int	nConfLimit,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 320 of file fraCec.c.

{
    int nBTLimitStart =        300;   // starting SAT run
    int nBTLimitFirst =          2;   // first fraiging iteration
    int nBTLimitLast  = nConfLimit;   // the last-gasp SAT run

    Fra_Par_t Params, * pParams = &Params;
    Aig_Man_t * pAig = *ppAig, * pTemp;
    int i, RetValue;
    abctime clk;

    // report the original miter
    if ( fVerbose )
    {
        printf( "Original miter:   Nodes = %6d.\n", Aig_ManNodeNum(pAig) );
    }
    RetValue = Fra_FraigMiterStatus( pAig );
//    assert( RetValue == -1 );
    if ( RetValue == 0 )
    {
        pAig->pData = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
        memset( pAig->pData, 0, sizeof(int) * Aig_ManCiNum(pAig) );
        return RetValue;
    }

    // if SAT only, solve without iteration
clk = Abc_Clock();
    RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
    if ( fVerbose )
    {
        printf( "Initial SAT:      Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    if ( RetValue >= 0 )
        return RetValue;

    // duplicate the AIG
clk = Abc_Clock();
    pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
    Aig_ManStop( pTemp );
    if ( fVerbose )
    {
        printf( "Rewriting:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }

    // perform the loop
    Fra_ParamsDefault( pParams );
    pParams->nBTLimitNode = nBTLimitFirst;
    pParams->nBTLimitMiter = nBTLimitStart;
    pParams->fDontShowBar = 1;
    pParams->fProve = 1;
    for ( i = 0; i < 6; i++ )
    {
//printf( "Running fraiging with %d BTnode and %d BTmiter.\n", pParams->nBTLimitNode, pParams->nBTLimitMiter );
        // try XOR balancing
        if ( Aig_ManCountXors(pAig) * 30 > Aig_ManNodeNum(pAig) + 300 )
        {
clk = Abc_Clock();
            pAig = Dar_ManBalanceXor( pTemp = pAig, 1, 0, 0 );
            Aig_ManStop( pTemp );
            if ( fVerbose )
            {
                printf( "Balance-X:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
            } 
        }

        // run fraiging
clk = Abc_Clock();
        pAig = Fra_FraigPerform( pTemp = pAig, pParams );
        Aig_ManStop( pTemp );
        if ( fVerbose )
        {
            printf( "Fraiging (i=%d):   Nodes = %6d.  ", i+1, Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }

        // check the miter status
        RetValue = Fra_FraigMiterStatus( pAig );
        if ( RetValue >= 0 )
            break;

        // perform rewriting
clk = Abc_Clock();
        pAig = Dar_ManRewriteDefault( pTemp = pAig );
        Aig_ManStop( pTemp );
        if ( fVerbose )
        {
            printf( "Rewriting:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
        } 

        // check the miter status
        RetValue = Fra_FraigMiterStatus( pAig );
        if ( RetValue >= 0 )
            break;
        // try simulation

        // set the parameters for the next run
        pParams->nBTLimitNode = 8 * pParams->nBTLimitNode;
        pParams->nBTLimitMiter = 2 * pParams->nBTLimitMiter;
    }

    // if still unsolved try last gasp
    if ( RetValue == -1 )
    {
clk = Abc_Clock();
        RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
        if ( fVerbose )
        {
            printf( "Final SAT:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }

    *ppAig = pAig;
    return RetValue;
}

int Fra_FraigCecPartitioned	(	Aig_Man_t *	pMan1,
		Aig_Man_t *	pMan2,
		int	nConfLimit,
		int	nPartSize,
		int	fSmart,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file fraCec.c.

{
    Aig_Man_t * pAig;
    Vec_Ptr_t * vParts;
    int i, RetValue = 1, nOutputs;
    // create partitions
    vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
    // solve the partitions
    nOutputs = -1;
    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
    {
        nOutputs++;
        if ( fVerbose )
        {
            printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
                i+1, Vec_PtrSize(vParts), Aig_ManCiNum(pAig), Aig_ManCoNum(pAig), 
                Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
            fflush( stdout );
        }
        RetValue = Fra_FraigMiterStatus( pAig );
        if ( RetValue == 1 )
            continue;
        if ( RetValue == 0 )
            break;
        RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
        Vec_PtrWriteEntry( vParts, i, pAig );
        if ( RetValue == 1 )
            continue;
        if ( RetValue == 0 )
            break;
        break;
    }
    // clear the result
    if ( fVerbose )
    {
        printf( "                                                                                          \r" );
        fflush( stdout );
    }
    // report the timeout
    if ( RetValue == -1 )
    {
        printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
        fflush( stdout );
    }
    // free intermediate results
    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
        Aig_ManStop( pAig );
    Vec_PtrFree( vParts );
    return RetValue;
}

Aig_Man_t* Fra_FraigChoice	(	Aig_Man_t *	pManAig,
		int	nConfMax,
		int	nLevelMax
	)

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

Synopsis [Performs choicing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file fraCore.c.

{
    Fra_Par_t Pars, * pPars = &Pars; 
    Fra_ParamsDefault( pPars );
    pPars->nBTLimitNode = nConfMax;
    pPars->fChoicing    = 1;
    pPars->fDoSparse    = 1;
    pPars->fSpeculate   = 0;
    pPars->fProve       = 0;
    pPars->fVerbose     = 0;
    pPars->fDontShowBar = 1;
    pPars->nLevelMax    = nLevelMax;
    return Fra_FraigPerform( pManAig, pPars );
}

Aig_Man_t* Fra_FraigEquivence	(	Aig_Man_t *	pManAig,
		int	nConfMax,
		int	fProve
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file fraCore.c.

{
    Aig_Man_t * pFraig;
    Fra_Par_t Pars, * pPars = &Pars; 
    Fra_ParamsDefault( pPars );
    pPars->nBTLimitNode = nConfMax;
    pPars->fChoicing    = 0;
    pPars->fDoSparse    = 1;
    pPars->fSpeculate   = 0;
    pPars->fProve       = fProve;
    pPars->fVerbose     = 0;
    pPars->fDontShowBar = 1;
    pFraig = Fra_FraigPerform( pManAig, pPars );
    return pFraig;
} 

Aig_Man_t* Fra_FraigInduction	(	Aig_Man_t *	pManAig,
		Fra_Ssw_t *	pParams
	)

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

Synopsis [Performs sequential SAT sweeping.]

Description []

SideEffects []

SeeAlso []

Definition at line 344 of file fraInd.c.

{
    int fUseSimpleCnf = 0;
    int fUseOldSimulation = 0;
    // other paramaters affecting performance
    // - presence of FRAIGing in Abc_NtkDarSeqSweep()
    // - using distance-1 patterns in Fra_SmlAssignDist1()
    // - the number of simulation patterns
    // - the number of BMC frames

    Fra_Man_t * p;
    Fra_Par_t Pars, * pPars = &Pars; 
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    Aig_Man_t * pManAigNew = NULL;
    int nNodesBeg, nRegsBeg;
    int nIter = -1; // Suppress "might be used uninitialized"
    int i;
    abctime clk = Abc_Clock(), clk2;
    abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;

    if ( Aig_ManNodeNum(pManAig) == 0 )
    {
        pParams->nIters = 0;
        // Ntl_ManFinalize() needs the following to satisfy an assertion
        Aig_ManReprStart(pManAig,Aig_ManObjNumMax(pManAig));
        return Aig_ManDupOrdered(pManAig);
    }
    assert( Aig_ManRegNum(pManAig) > 0 );
    assert( pParams->nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );

    if ( pParams->fWriteImps && pParams->nPartSize > 0 )
    {
        pParams->nPartSize = 0;
        printf( "Partitioning was disabled to allow implication writing.\n" );
    }
    // perform partitioning
    if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
         || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0)  )
        return Fra_FraigInductionPart( pManAig, pParams );
 
    nNodesBeg = Aig_ManNodeNum(pManAig);
    nRegsBeg  = Aig_ManRegNum(pManAig);

    // enhance the AIG by adding timeframes
//    Fra_FramesAddMore( pManAig, 3 );

    // get parameters
    Fra_ParamsDefaultSeq( pPars );
    pPars->nFramesP   = pParams->nFramesP;
    pPars->nFramesK   = pParams->nFramesK;
    pPars->nMaxImps   = pParams->nMaxImps;
    pPars->nMaxLevs   = pParams->nMaxLevs;
    pPars->fVerbose   = pParams->fVerbose;
    pPars->fRewrite   = pParams->fRewrite;
    pPars->fLatchCorr = pParams->fLatchCorr;
    pPars->fUseImps   = pParams->fUseImps;
    pPars->fWriteImps = pParams->fWriteImps;
    pPars->fUse1Hot   = pParams->fUse1Hot;

    assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
    assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
 
    // start the fraig manager for this run
    p = Fra_ManStart( pManAig, pPars );
    p->pPars->nBTLimitNode = 0;
    // derive and refine e-classes using K initialized frames
    if ( fUseOldSimulation )
    {
        if ( pPars->nFramesP > 0 )
        {
            pPars->nFramesP = 0;
            printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
        }
        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
        Fra_SmlSimulate( p, 1 );
    }
    else
    {
        // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
        // refine the classes with more simulation rounds
if ( pPars->fVerbose )
printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1  ); //pPars->nFramesK + 1, 1 );  
if ( pPars->fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk );
}
        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
//        Fra_ClassesPostprocess( p->pCla );
        // compute one-hotness conditions
        if ( p->pPars->fUse1Hot )
            p->vOneHots = Fra_OneHotCompute( p, p->pSml );
        // allocate new simulation manager for simulating counter-examples
        Fra_SmlStop( p->pSml );
        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
    }

    // select the most expressive implications
    if ( pPars->fUseImps )
        p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );

    if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
    {
        if ( !pParams->fSilent )
            printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
        goto finish;
    }

    // perform BMC (for the min number of frames)
    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
//Fra_ClassesPrint( p->pCla, 1 );
//    if ( p->vCex == NULL )
//        p->vCex = Vec_IntAlloc( 1000 );

    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
    p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
    p->nRegsBeg  = nRegsBeg; // Aig_ManRegNum(pManAig);

    // dump AIG of the timeframes
//    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL );
//    Fra_ManPartitionTest2( pManAigNew );
//    Aig_ManStop( pManAigNew );
 
    // iterate the inductive case
    p->pCla->fRefinement = 1;
    for ( nIter = 0; p->pCla->fRefinement; nIter++ )
    {
        int nLitsOld = Fra_ClassesCountLits(p->pCla);
        int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
        int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
        abctime clk3 = Abc_Clock();

        if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
        {
            if ( !pParams->fSilent )
                printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
            goto finish;
        }

        // mark the classes as non-refined
        p->pCla->fRefinement = 0;
        // derive non-init K-timeframes while implementing e-classes
clk2 = Abc_Clock();
        p->pManFraig = Fra_FramesWithClasses( p );
p->timeTrav += Abc_Clock() - clk2;
//Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );

        // perform AIG rewriting
        if ( p->pPars->fRewrite )
            Fra_FraigInductionRewrite( p );

        // convert the manager to SAT solver (the last nLatches outputs are inputs)
        if ( fUseSimpleCnf || pPars->fUseImps )
            pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
        else
            pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
//        Cnf_DataTranformPolarity( pCnf, 0 );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );

        p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
        p->nSatVars = pCnf->nVars;
        assert( p->pSat != NULL );
        if ( p->pSat == NULL )
            printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
        if ( pPars->fUseImps )
        {
            Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
            if ( p->pSat == NULL )
                printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
        }

        // set the pointers to the manager
        Aig_ManForEachObj( p->pManFraig, pObj, i )
            pObj->pData = p;

        // prepare solver for fraiging the last timeframe
        Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );

        // transfer PI/LO variable numbers
        Aig_ManForEachObj( p->pManFraig, pObj, i )
        {
            if ( pCnf->pVarNums[pObj->Id] == -1 )
                continue;
            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
            Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 );
        }
        Cnf_DataFree( pCnf );

        // add one-hotness clauses
        if ( p->pPars->fUse1Hot )
            Fra_OneHotAssume( p, p->vOneHots );
//        if ( p->pManAig->vOnehots )
//            Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
 
        // report the intermediate results
        if ( pPars->fVerbose )
        {
            printf( "%3d : C = %6d. Cl = %6d.  L = %6d. LR = %6d.  ", 
                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
            if ( p->pCla->vImps )
                printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
            if ( p->pPars->fUse1Hot )
                printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
            printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
//            printf( "\n" );
        } 

        // perform sweeping
        p->nSatCallsRecent = 0;
        p->nSatCallsSkipped = 0;
clk2 = Abc_Clock();
        if ( p->pPars->fUse1Hot )
            Fra_OneHotCheck( p, p->vOneHots );
        Fra_FraigSweep( p );
        if ( pPars->fVerbose )
        {
            ABC_PRT( "T", Abc_Clock() - clk3 );
        } 

//        Sat_SolverPrintStats( stdout, p->pSat );
        // remove FRAIG and SAT solver
        Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
//        printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
        sat_solver_delete( p->pSat );  p->pSat = NULL; 
        memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
//        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
        assert( p->vTimeouts == NULL );
        if ( p->vTimeouts )
           printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
        // check if refinement has happened
//        p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
        if ( p->pCla->fRefinement && 
            nLitsOld == Fra_ClassesCountLits(p->pCla) && 
            nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) && 
            nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) )
        {
            printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
            break;
        }
    }
/*
    // verify implications using simulation
    if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
    {
        int Temp;
        abctime clk = Abc_Clock();
        if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
            printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
        else
            printf( "All %d implications have passed the simulation test.  ", Vec_IntSize(p->pCla->vImps) );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
*/

    // move the classes into representatives and reduce AIG
clk2 = Abc_Clock();
    if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
    {
        extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
        Aig_Man_t * pNew;
        char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
        printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
        pManAigNew = Aig_ManDupOrdered( pManAig );
        pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
        Ioa_WriteAiger( pNew, pFileName, 0, 1 );
        Aig_ManStop( pNew );
    }
    else 
    {
    //    Fra_ClassesPrint( p->pCla, 1 );
        Fra_ClassesSelectRepr( p->pCla );
        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
        pManAigNew = Aig_ManDupRepr( pManAig, 0 );
    }
    // add implications to the manager
//    if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
//        Fra_ImpRecordInManager( p, pManAigNew );
    // cleanup the new manager
    Aig_ManSeqCleanup( pManAigNew );
    // remove pointers to the dead nodes
//    Aig_ManForEachObj( pManAig, pObj, i )
//        if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
//            pObj->pData = NULL;
//    Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += Abc_Clock() - clk2;
p->timeTotal = Abc_Clock() - clk;
    // get the final stats
    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
    // free the manager
finish:
    Fra_ManStop( p );
    // check the output
//    if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
//        if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
//            printf( "Proved output constant 0.\n" );
    pParams->nIters = nIter;
    return pManAigNew;
}

Aig_Man_t* Fra_FraigLatchCorrespondence	(	Aig_Man_t *	pAig,
		int	nFramesP,
		int	nConfMax,
		int	fProve,
		int	fVerbose,
		int *	pnIter,
		float	TimeLimit
	)

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

Synopsis [Performs choicing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 531 of file fraLcr.c.

{
    int nPartSize    = 200;
    int fReprSelect  = 0;
    Fra_Lcr_t * p;
    Fra_Sml_t * pSml;
    Fra_Man_t * pTemp;
    Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
    Vec_Int_t * vPart;
    int i, nIter;
    abctime timeSim, clk2, clk3, clk = Abc_Clock();
    abctime TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
    if ( Aig_ManNodeNum(pAig) == 0 )
    {
        if ( pnIter ) *pnIter = 0;
        // Ntl_ManFinalize() requires the following to satisfy an assertion.
        Aig_ManReprStart(pAig,Aig_ManObjNumMax(pAig));
        return Aig_ManDupOrdered(pAig);
    }
    assert( Aig_ManRegNum(pAig) > 0 ); 

    // simulate the AIG 
clk2 = Abc_Clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
    pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1, 1  ); 
if ( fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk2 );
}
timeSim = Abc_Clock() - clk2;

    // check if simulation discovered non-constant-0 POs
    if ( fProve && pSml->fNonConstOut )
    {
        pAig->pSeqModel = Fra_SmlGetCounterExample( pSml );
        Fra_SmlStop( pSml );
        return NULL;
    }

    // start the manager
    p = Lcr_ManAlloc( pAig );
    p->nFramesP = nFramesP;
    p->fVerbose = fVerbose;
    p->timeSim += timeSim;

    pTemp = Fra_LcrAigPrepare( pAig );
    pTemp->pBmc = (Fra_Bmc_t *)p;
    pTemp->pSml = pSml;

    // get preliminary info about equivalence classes
    pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
    Fra_ClassesPrepare( p->pCla, 1, 0 );
    p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
    Fra_SmlStop( pTemp->pSml );

    // partition the AIG for latch correspondence computation
clk2 = Abc_Clock();
if ( fVerbose )
printf( "Partitioning AIG ...  " );
    pAigPart = Fra_LcrDeriveAigForPartitioning( p );
    p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
    Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
    Aig_ManStop( pAigPart );
if ( fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk2 );
p->timePart += Abc_Clock() - clk2;
}

    // get the initial stats
    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
    p->nRegsBeg  = Aig_ManRegNum(p->pAig);

    // perforn interative reduction of the partitions
    p->fRefining = 1;
    for ( nIter = 0; p->fRefining; nIter++ )
    {
        p->fRefining = 0;
        clk3 = Abc_Clock();
        // derive AIGs for each partition
        Fra_ClassNodesMark( p );
        Vec_PtrClear( p->vFraigs );
        Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i )
        {
            if ( TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
            {
                Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
                    Aig_ManStop( pAigPart );
                Aig_ManCleanMarkA( pAig );
                Aig_ManCleanMarkB( pAig );
                printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" );
                goto finish;
            }
clk2 = Abc_Clock();
            pAigPart = Fra_LcrCreatePart( p, vPart );
p->timeTrav += Abc_Clock() - clk2;
clk2 = Abc_Clock();
            pAigTemp  = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
p->timeFraig += Abc_Clock() - clk2;
            Vec_PtrPush( p->vFraigs, pAigTemp );
/*
            {
                char Name[1000];
                sprintf( Name, "part%04d.blif", i );
                Aig_ManDumpBlif( pAigPart, Name, NULL, NULL );
            }
printf( "Finished part %4d (out of %4d).  ", i, Vec_PtrSize(p->vParts) );
ABC_PRT( "Time", Abc_Clock() - clk3 );
*/

            Aig_ManStop( pAigPart );
        }
        Fra_ClassNodesUnmark( p );
        // report the intermediate results
        if ( fVerbose )
        {
            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. Part = %3d.  ", 
                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
            ABC_PRT( "T", Abc_Clock() - clk3 );
        }
        // refine the classes
        Fra_LcrAigPrepareTwo( p->pAig, pTemp );
        if ( Fra_ClassesRefine( p->pCla ) )
            p->fRefining = 1;
        if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
            p->fRefining = 1;
        // clean the fraigs
        Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
            Aig_ManStop( pAigPart );

        // repartition if needed
        if ( 1 )
        {
clk2 = Abc_Clock();
            Vec_VecFree( (Vec_Vec_t *)p->vParts );
            pAigPart = Fra_LcrDeriveAigForPartitioning( p );
            p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
            Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
            Aig_ManStop( pAigPart );
p->timePart += Abc_Clock() - clk2;
        }
    }
    p->nIters = nIter;

    // move the classes into representatives and reduce AIG
clk2 = Abc_Clock();
//    Fra_ClassesPrint( p->pCla, 1 );
    if ( fReprSelect )
        Fra_ClassesSelectRepr( p->pCla );
    Fra_ClassesCopyReprs( p->pCla, NULL );
    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
    Aig_ManSeqCleanup( pAigNew );
//    Aig_ManCountMergeRegs( pAigNew );
p->timeUpdate += Abc_Clock() - clk2;
p->timeTotal = Abc_Clock() - clk;
    // get the final stats
    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
finish:
    ABC_FREE( pTemp );
    Lcr_ManFree( p );
    if ( pnIter ) *pnIter = nIter;
    return pAigNew;
}

int Fra_FraigMiterAssertedOutput

(

Aig_Man_t *

p

)

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

Synopsis [Reports the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file fraCore.c.

{
    Aig_Obj_t * pObj, * pChild;
    int i;
    Aig_ManForEachPoSeq( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
            continue;
        // check if the output is constant 1
        if ( pChild == Aig_ManConst1(p) )
            return i;
        // check if the output can be not constant 0
        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
            return i;
    }
    return -1;
}

int Fra_FraigMiterStatus

(

Aig_Man_t *

p

)

DECLARATIONS ///.

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

FileName [fraCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Reports the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file fraCore.c.

{
    Aig_Obj_t * pObj, * pChild;
    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
    if ( p->pData )
        return 0;
    Aig_ManForEachPoSeq( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
        {
            CountConst0++;
            continue;
        }
        // check if the output is constant 1
        if ( pChild == Aig_ManConst1(p) )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output is a primary input
        if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjCioId(Aig_Regular(pChild)) < p->nTruePis )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output can be not constant 0
        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
        {
            CountNonConst0++;
            continue;
        }
        CountUndecided++;
    }
/*
    if ( p->pParams->fVerbose )
    {
        printf( "Miter has %d outputs. ", Aig_ManCoNum(p->pManAig) );
        printf( "Const0 = %d.  ", CountConst0 );
        printf( "NonConst0 = %d.  ", CountNonConst0 );
        printf( "Undecided = %d.  ", CountUndecided );
        printf( "\n" );
    }
*/
    if ( CountNonConst0 )
        return 0;
    if ( CountUndecided )
        return -1;
    return 1;
}

Aig_Man_t* Fra_FraigPerform	(	Aig_Man_t *	pManAig,
		Fra_Par_t *	pPars
	)

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

Synopsis [Performs fraiging of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file fraCore.c.

{
    Fra_Man_t * p;
    Aig_Man_t * pManAigNew;
    abctime clk;
    if ( Aig_ManNodeNum(pManAig) == 0 )
        return Aig_ManDupOrdered(pManAig);
clk = Abc_Clock();
    p = Fra_ManStart( pManAig, pPars );
    p->pManFraig = Fra_ManPrepareComb( p );
    p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
    Fra_SmlSimulate( p, 0 );
//    if ( p->pPars->fChoicing )
//        Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
    // collect initial states
    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
    p->nNodesBeg = Aig_ManNodeNum(pManAig);
    p->nRegsBeg  = Aig_ManRegNum(pManAig);
    // perform fraig sweep
if ( p->pPars->fVerbose )
Fra_ClassesPrint( p->pCla, 1 );
    Fra_FraigSweep( p );
    // call back the procedure to check implications
    if ( pManAig->pImpFunc )
        pManAig->pImpFunc( p, pManAig->pImpData );
    // no need to filter one-hot clauses because they satisfy base case by construction
    // finalize the fraiged manager
    Fra_ManFinalizeComb( p );
    if ( p->pPars->fChoicing )
    { 
abctime clk2 = Abc_Clock();
        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
        pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
        Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
        Aig_ManTransferRepr( pManAigNew, p->pManAig );
        Aig_ManMarkValidChoices( pManAigNew );
        Aig_ManStop( p->pManFraig );
        p->pManFraig = NULL;
p->timeTrav += Abc_Clock() - clk2;
    }
    else
    {
        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
        Aig_ManCleanup( p->pManFraig );
        pManAigNew = p->pManFraig;
        p->pManFraig = NULL;
    }
p->timeTotal = Abc_Clock() - clk;
    // collect final stats
    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
    Fra_ManStop( p );
    return pManAigNew;
}

int Fra_FraigSat	(	Aig_Man_t *	pMan,
		ABC_INT64_T	nConfLimit,
		ABC_INT64_T	nInsLimit,
		int	nLearnedStart,
		int	nLearnedDelta,
		int	nLearnedPerce,
		int	fFlipBits,
		int	fAndOuts,
		int	fNewSolver,
		int	fVerbose
	)

ITERATORS ///.

FUNCTION DECLARATIONS ///

ITERATORS ///.

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

FileName [fraCec.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [CEC engined based on fraiging.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file fraCec.c.

{
    if ( fNewSolver )
    {
        extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit );
        extern int    Cnf_DataWriteOrClause2( void * pSat, Cnf_Dat_t * pCnf );

        sat_solver2 * pSat;
        Cnf_Dat_t * pCnf;
        int status, RetValue;
        abctime clk = Abc_Clock();
        Vec_Int_t * vCiIds;

        assert( Aig_ManRegNum(pMan) == 0 );
        pMan->pData = NULL;

        // derive CNF
        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );

        if ( fFlipBits ) 
            Cnf_DataTranformPolarity( pCnf, 0 );

        if ( fVerbose )
        {
            printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }

        // convert into SAT solver
        pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 );
        if ( pSat == NULL )
        {
            Cnf_DataFree( pCnf );
            return 1;
        }

        if ( fAndOuts )
        {
            // assert each output independently
            if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
            {
                sat_solver2_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        else
        {
            // add the OR clause for the outputs
            if ( !Cnf_DataWriteOrClause2( pSat, pCnf ) )
            {
                sat_solver2_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
        Cnf_DataFree( pCnf );


        printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
        ABC_PRT( "Time", Abc_Clock() - clk );

        // simplify the problem
        clk = Abc_Clock();
        status = sat_solver2_simplify(pSat);
//        printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
//        ABC_PRT( "Time", Abc_Clock() - clk );
        if ( status == 0 )
        {
            Vec_IntFree( vCiIds );
            sat_solver2_delete( pSat );
    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
            return 1;
        }

        // solve the miter
        clk = Abc_Clock();
        if ( fVerbose )
            pSat->verbosity = 1;
        status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_Undef )
        {
    //        printf( "The problem timed out.\n" );
            RetValue = -1;
        }
        else if ( status == l_True )
        {
    //        printf( "The problem is SATISFIABLE.\n" );
            RetValue = 0;
        }
        else if ( status == l_False )
        {
    //        printf( "The problem is UNSATISFIABLE.\n" );
            RetValue = 1;
        }
        else
            assert( 0 );

    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
    //    Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
 
        // if the problem is SAT, get the counterexample
        if ( status == l_True )
        {
            pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize );
        }
        // free the sat_solver2
        if ( fVerbose )
            Sat_Solver2PrintStats( stdout, pSat );
    //sat_solver2_store_write( pSat, "trace.cnf" );
    //sat_solver2_store_free( pSat );
        sat_solver2_delete( pSat );
        Vec_IntFree( vCiIds );
        return RetValue;
    }
    else
    {
        sat_solver * pSat;
        Cnf_Dat_t * pCnf;
        int status, RetValue;
        abctime clk = Abc_Clock();
        Vec_Int_t * vCiIds;

        assert( Aig_ManRegNum(pMan) == 0 );
        pMan->pData = NULL;

        // derive CNF
        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );

        if ( fFlipBits ) 
            Cnf_DataTranformPolarity( pCnf, 0 );

        if ( fVerbose )
        {
            printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }

        // convert into SAT solver
        pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
        if ( pSat == NULL )
        {
            Cnf_DataFree( pCnf );
            return 1;
        }

        if ( nLearnedStart )
            pSat->nLearntStart = nLearnedStart;
        if ( nLearnedDelta )
            pSat->nLearntDelta = nLearnedDelta;
        if ( nLearnedPerce )
            pSat->nLearntRatio = nLearnedPerce;
        if ( fVerbose )
            pSat->fVerbose = fVerbose;

        if ( fAndOuts )
        {
            // assert each output independently
            if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
            {
                sat_solver_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        else
        {
            // add the OR clause for the outputs
            if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
            {
                sat_solver_delete( pSat );
                Cnf_DataFree( pCnf );
                return 1;
            }
        }
        vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
        Cnf_DataFree( pCnf );


    //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
    //    ABC_PRT( "Time", Abc_Clock() - clk );

        // simplify the problem
        clk = Abc_Clock();
        status = sat_solver_simplify(pSat);
    //    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
    //    ABC_PRT( "Time", Abc_Clock() - clk );
        if ( status == 0 )
        {
            Vec_IntFree( vCiIds );
            sat_solver_delete( pSat );
    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
            return 1;
        }

        // solve the miter
        clk = Abc_Clock();
//        if ( fVerbose )
//            pSat->verbosity = 1;
        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_Undef )
        {
    //        printf( "The problem timed out.\n" );
            RetValue = -1;
        }
        else if ( status == l_True )
        {
    //        printf( "The problem is SATISFIABLE.\n" );
            RetValue = 0;
        }
        else if ( status == l_False )
        {
    //        printf( "The problem is UNSATISFIABLE.\n" );
            RetValue = 1;
        }
        else
            assert( 0 );

    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
    //    Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
 
        // if the problem is SAT, get the counterexample
        if ( status == l_True )
        {
            pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
        }
        // free the sat_solver
        if ( fVerbose )
            Sat_SolverPrintStats( stdout, pSat );
    //sat_solver_store_write( pSat, "trace.cnf" );
    //sat_solver_store_free( pSat );
        sat_solver_delete( pSat );
        Vec_IntFree( vCiIds );
        return RetValue;
    }
}

int Fra_FraigSec	(	Aig_Man_t *	p,
		Fra_Sec_t *	pParSec,
		Aig_Man_t **	ppResult
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file fraSec.c.

{
    Ssw_Pars_t Pars2, * pPars2 = &Pars2;
    Fra_Ssw_t Pars, * pPars = &Pars;
    Fra_Sml_t * pSml;
    Aig_Man_t * pNew, * pTemp;
    int nFrames, RetValue, nIter;
    abctime clk, clkTotal = Abc_Clock();
    int TimeOut = 0;
    int fLatchCorr = 0;
    float TimeLeft = 0.0;
    pParSec->nSMnumber = -1;

    // try the miter before solving
    pNew = Aig_ManDupSimple( p );
    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue >= 0 )
        goto finish;

    // prepare parameters
    memset( pPars, 0, sizeof(Fra_Ssw_t) );
    pPars->fLatchCorr  = fLatchCorr;
    pPars->fVerbose = pParSec->fVeryVerbose;
    if ( pParSec->fVerbose )
    {
        printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
    }
//Aig_ManDumpBlif( pNew, "after.blif", NULL, NULL );

    // perform sequential cleanup
clk = Abc_Clock();
    if ( pNew->nRegs )
    pNew = Aig_ManReduceLaches( pNew, 0 );
    if ( pNew->nRegs )
    pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
    if ( pParSec->fVerbose )
    {
        printf( "Sequential cleanup:   Latches = %5d. Nodes = %6d. ", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue >= 0 )
        goto finish;

    // perform phase abstraction
clk = Abc_Clock();
    if ( pParSec->fPhaseAbstract )
    {
        extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
        pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
        Aig_ManStop( pTemp );
        if ( pParSec->fVerbose )
        {
            printf( "Phase abstraction:    Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }

    // perform forward retiming
    if ( pParSec->fRetimeFirst && pNew->nRegs )
    {
clk = Abc_Clock();
//    pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
    pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 );
    Aig_ManStop( pTemp );
    if ( pParSec->fVerbose )
    {
        printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }
     
    // run latch correspondence
clk = Abc_Clock();
    if ( pNew->nRegs )
    {
    pNew = Aig_ManDupOrdered( pTemp = pNew );
//    pNew = Aig_ManDupDfs( pTemp = pNew );
    Aig_ManStop( pTemp );
/*
    if ( RetValue == -1 && pParSec->TimeLimit )
    {
        TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
        TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
        if ( TimeLeft == 0.0 )
        {
            if ( !pParSec->fSilent )
                printf( "Runtime limit exceeded.\n" );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
    }
*/

//    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
//Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL );
    Ssw_ManSetDefaultParamsLcorr( pPars2 );
    pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 );
    nIter = pPars2->nIters;

    // prepare parameters for scorr
    Ssw_ManSetDefaultParams( pPars2 );

    if ( pTemp->pSeqModel )
    {
        if ( !Saig_ManVerifyCex( pTemp, pTemp->pSeqModel ) )
            printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
        if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
            printf( "The counter-example is invalid because of phase abstraction.\n" );
        else
        {
        ABC_FREE( p->pSeqModel );
        p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
        ABC_FREE( pTemp->pSeqModel );
        }
    }
    if ( pNew == NULL )
    {
        if ( p->pSeqModel )
        {
            RetValue = 0;
            if ( !pParSec->fSilent )
            {
                printf( "Networks are NOT EQUIVALENT after simulation.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            if ( pParSec->fReportSolution && !pParSec->fRecursive )
            {
            printf( "SOLUTION: FAIL       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            Aig_ManStop( pTemp );
            return RetValue;
        }
        pNew = pTemp;
        RetValue = -1;
        TimeOut = 1;
        goto finish;
    }
    Aig_ManStop( pTemp );

    if ( pParSec->fVerbose )
    {
        printf( "Latch-corr (I=%3d):   Latches = %5d. Nodes = %6d. ", 
            nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }
/*
    if ( RetValue == -1 && pParSec->TimeLimit )
    {
        TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
        TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
        if ( TimeLeft == 0.0 )
        {
            if ( !pParSec->fSilent )
                printf( "Runtime limit exceeded.\n" );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
    }
*/
    // perform fraiging
    if ( pParSec->fFraiging )
    {
clk = Abc_Clock();
    pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
    Aig_ManStop( pTemp );
    if ( pParSec->fVerbose )
    {
        printf( "Fraiging:             Latches = %5d. Nodes = %6d. ", 
            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }

    if ( pNew->nRegs == 0 )
        RetValue = Fra_FraigCec( &pNew, 100000, 0 );

    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue >= 0 )
        goto finish;
/*
    if ( RetValue == -1 && pParSec->TimeLimit )
    {
        TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
        TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
        if ( TimeLeft == 0.0 )
        {
            if ( !pParSec->fSilent )
                printf( "Runtime limit exceeded.\n" );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }
    }
*/
    // perform min-area retiming
    if ( pParSec->fRetimeRegs && pNew->nRegs )
    {
//    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
clk = Abc_Clock();
    pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
    pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
    pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
    Aig_ManStop( pTemp );
    pNew = Aig_ManDupOrdered( pTemp = pNew );
    Aig_ManStop( pTemp );
    if ( pParSec->fVerbose )
    {
    printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
        Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    }

    // perform seq sweeping while increasing the number of frames
    RetValue = Fra_FraigMiterStatus( pNew );
    if ( RetValue == -1 && pParSec->fInduction )
    for ( nFrames = 1; nFrames <= pParSec->nFramesMax; nFrames *= 2 )
    {
/*
        if ( RetValue == -1 && pParSec->TimeLimit )
        {
            TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
            TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
            if ( TimeLeft == 0.0 )
            {
                if ( !pParSec->fSilent )
                    printf( "Runtime limit exceeded.\n" );
                RetValue = -1;
                TimeOut = 1;
                goto finish;
            }
        }
*/ 

clk = Abc_Clock();
        pPars->nFramesK = nFrames;
        pPars->TimeLimit = TimeLeft;
        pPars->fSilent = pParSec->fSilent;
//        pNew = Fra_FraigInduction( pTemp = pNew, pPars );

        pPars2->nFramesK = nFrames;
        pPars2->nBTLimit = pParSec->nBTLimit;
        pPars2->nBTLimitGlobal = pParSec->nBTLimitGlobal;
//        pPars2->nBTLimit = 1000 * nFrames;

        if ( RetValue == -1 && pPars2->nConflicts > pPars2->nBTLimitGlobal )
        {
            if ( !pParSec->fSilent )
                printf( "Global conflict limit (%d) exceeded.\n", pPars2->nBTLimitGlobal );
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }

        Aig_ManSetRegNum( pNew, pNew->nRegs );
//        pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
        if ( Aig_ManRegNum(pNew) > 0 )
            pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
        else
            pNew = Aig_ManDupSimpleDfs( pTemp = pNew );

        if ( pNew == NULL )
        {
            pNew = pTemp;
            RetValue = -1;
            TimeOut = 1;
            goto finish;
        }

//        printf( "Total conflicts = %d.\n", pPars2->nConflicts );

        Aig_ManStop( pTemp );
        RetValue = Fra_FraigMiterStatus( pNew );
        if ( pParSec->fVerbose )
        { 
            printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
                nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( RetValue != -1 )
            break;

        // perform retiming
//        if ( pParSec->fRetimeFirst && pNew->nRegs )
        if ( pNew->nRegs )
        {
//        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
clk = Abc_Clock();
        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
        pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
        Aig_ManStop( pTemp );
        pNew = Aig_ManDupOrdered( pTemp = pNew );
        Aig_ManStop( pTemp );
        if ( pParSec->fVerbose )
        {
            printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
        }  

        if ( pNew->nRegs )
            pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );

        // perform rewriting
clk = Abc_Clock();
        pNew = Aig_ManDupOrdered( pTemp = pNew );
        Aig_ManStop( pTemp );
//        pNew = Dar_ManRewriteDefault( pTemp = pNew );
        pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0, 0 ); 
        Aig_ManStop( pTemp );
        if ( pParSec->fVerbose )
        {
            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        } 

        // perform sequential simulation
        if ( pNew->nRegs )
        {
clk = Abc_Clock();
        pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000), 1  ); 
        if ( pParSec->fVerbose )
        {
            printf( "Seq simulation  :     Latches = %5d. Nodes = %6d. ", 
                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
ABC_PRT( "Time", Abc_Clock() - clk );
        }
        if ( pSml->fNonConstOut )
        {
            pNew->pSeqModel = Fra_SmlGetCounterExample( pSml );
            // transfer to the original manager
            if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
                printf( "The counter-example is invalid because of phase abstraction.\n" );
            else
            {
            ABC_FREE( p->pSeqModel );
            p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
            ABC_FREE( pNew->pSeqModel );
            }

            Fra_SmlStop( pSml );
            Aig_ManStop( pNew );
            RetValue = 0;
            if ( !pParSec->fSilent )
            {
                printf( "Networks are NOT EQUIVALENT after simulation.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            if ( pParSec->fReportSolution && !pParSec->fRecursive )
            {
            printf( "SOLUTION: FAIL       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
            }
            return RetValue;
        }
        Fra_SmlStop( pSml );
        }
    }

    // get the miter status
    RetValue = Fra_FraigMiterStatus( pNew );

    // try interplation
clk = Abc_Clock();
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
    if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
    {
        Inter_ManParams_t Pars, * pPars = &Pars;
        int Depth;
        ABC_FREE( pNew->pSeqModel );
        Inter_ManSetDefaultParams( pPars );
//        pPars->nBTLimit = 100;
        pPars->nBTLimit = pParSec->nBTLimitInter;
        pPars->fVerbose = pParSec->fVeryVerbose;
        if ( Saig_ManPoNum(pNew) == 1 )
        {
            RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
        }
        else if ( pParSec->fInterSeparate )
        {
            Abc_Cex_t * pCex = NULL;
            Aig_Man_t * pTemp, * pAux;
            Aig_Obj_t * pObjPo;
            int i, Counter = 0;
            Saig_ManForEachPo( pNew, pObjPo, i )
            { 
                if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) )
                    continue;
                if ( pPars->fVerbose )
                    printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pNew) );
                pTemp = Aig_ManDupOneOutput( pNew, i, 1 );
                pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
                Aig_ManStop( pAux );
                if ( Saig_ManRegNum(pTemp) > 0 )
                {
                    RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
                    if ( pTemp->pSeqModel )
                    {
                        pCex = p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
                        pCex->iPo = i;
                        Aig_ManStop( pTemp );
                        break;
                    }
                    // if solved, remove the output
                    if ( RetValue == 1 )
                    {
                        Aig_ObjPatchFanin0( pNew, pObjPo, Aig_ManConst0(pNew) );
    //                    printf( "Output %3d : Solved ", i );
                    }
                    else
                    {
                        Counter++;
    //                    printf( "Output %3d : Undec  ", i );
                    }
                }
                else
                    Counter++;
//                Aig_ManPrintStats( pTemp );
                Aig_ManStop( pTemp );
                printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
            }
            Aig_ManCleanup( pNew );
            if ( pCex == NULL )
            {
                printf( "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pNew) );
                if ( Counter )
                    RetValue = -1;
            }
            pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 );
            Aig_ManStop( pTemp );
            pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0, -1, -1, 0, 0 );
            Aig_ManStop( pTemp );
        }
        else
        {
            Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
            RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
            if ( pNewOrpos->pSeqModel )
            {
                Abc_Cex_t * pCex;
                pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
                pCex->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
            }
            Aig_ManStop( pNewOrpos );
        }

        if ( pParSec->fVerbose )
        {
        if ( RetValue == 1 )
            printf( "Property proved using interpolation.  " );
        else if ( RetValue == 0 )
            printf( "Property DISPROVED in frame %d using interpolation.  ", Depth );
        else if ( RetValue == -1 )
            printf( "Property UNDECIDED after interpolation.  " );
        else
            assert( 0 ); 
ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }

    // try reachability analysis
    if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
    {
        Saig_ParBbr_t Pars, * pPars = &Pars;
        Bbr_ManSetDefaultParams( pPars );
        pPars->TimeLimit     = 0;
        pPars->nBddMax       = pParSec->nBddMax;
        pPars->nIterMax      = pParSec->nBddIterMax;
        pPars->fPartition    = 1;
        pPars->fReorder      = 1;
        pPars->fReorderImage = 1;
        pPars->fVerbose      = 0;
        pPars->fSilent       = pParSec->fSilent;
        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
        RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
    }

    // try PDR
    if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
    {
        Pdr_Par_t Pars, * pPars = &Pars;
        Pdr_ManSetDefaultParams( pPars );
        pPars->nTimeOut = pParSec->nPdrTimeout;
        pPars->fVerbose = pParSec->fVerbose;
        if ( pParSec->fVerbose )
            printf( "Running property directed reachability...\n" );
        RetValue = Pdr_ManSolve( pNew, pPars );
        if ( pNew->pSeqModel )
            pNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
    }

finish:
    // report the miter
    if ( RetValue == 1 )
    {
        if ( !pParSec->fSilent )
        {
            printf( "Networks are equivalent.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( pParSec->fReportSolution && !pParSec->fRecursive )
        {
        printf( "SOLUTION: PASS       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
    }
    else if ( RetValue == 0 )
    {
        if ( pNew->pSeqModel == NULL )
        {
            int i;
            // if the CEX is not derives, it is because tricial CEX should be assumed
            pNew->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pNew), pNew->nTruePis, 1 );
            // if the CEX does not work, we need to change PIs to 1 because 
            // the only way it can happen is when a PO is equal to a PI...
            if ( Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ) == -1 )
                for ( i = 0; i < pNew->nTruePis; i++ )
                    Abc_InfoSetBit( pNew->pSeqModel->pData, i );
        }
        if ( !pParSec->fSilent )
        {
            printf( "Networks are NOT EQUIVALENT.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( pParSec->fReportSolution && !pParSec->fRecursive )
        {
        printf( "SOLUTION: FAIL       " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
    }
    else 
    {
        ///////////////////////////////////
        // save intermediate result
        extern void Abc_FrameSetSave1( void * pAig );
        Abc_FrameSetSave1( Aig_ManDupSimple(pNew) );
        ///////////////////////////////////
        if ( !pParSec->fSilent )
        {
            printf( "Networks are UNDECIDED.   " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( pParSec->fReportSolution && !pParSec->fRecursive )
        {
        printf( "SOLUTION: UNDECIDED  " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
        }
        if ( !TimeOut && !pParSec->fSilent )
        {
            static int Counter = 1;
            char pFileName[1000];
            pParSec->nSMnumber = Counter;
            sprintf( pFileName, "sm%02d.aig", Counter++ );
            Ioa_WriteAiger( pNew, pFileName, 0, 0 );
            printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
        }
    }
    if ( pNew->pSeqModel )
    {
        if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
            printf( "The counter-example is invalid because of phase abstraction.\n" );
        else
        {
        ABC_FREE( p->pSeqModel );
        p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
        ABC_FREE( pNew->pSeqModel );
        }
    }
    if ( ppResult != NULL )
        *ppResult = Aig_ManDupSimpleDfs( pNew );
    if ( pNew )
        Aig_ManStop( pNew );
    return RetValue;
}

void Fra_FraigSweep

(

Fra_Man_t *

p

)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file fraCore.c.

{
//    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
    int i, Pos = 0;
    int nBTracksOld;
    // fraig latch outputs
    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
    {
        Fra_FraigNode( p, pObj );
        if ( p->pPars->fUseImps )
            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
    }
    if ( p->pPars->fLatchCorr )
        return;
    // fraig internal nodes
//    if ( !p->pPars->fDontShowBar )
//        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
    nBTracksOld = p->pPars->nBTLimitNode;
    Aig_ManForEachNode( p->pManAig, pObj, i )
    {
//        if ( pProgress )
//            Bar_ProgressUpdate( pProgress, i, NULL );
        // derive and remember the new fraig node
        pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
        Aig_Regular(pObjNew)->pData = p;
        // quit if simulation detected a counter-example for a PO
        if ( p->pManFraig->pData )
            continue;
//        if ( Aig_SupportSize(p->pManAig,pObj) > 16 )
//            continue;
        // perform fraiging
        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
            p->pPars->nBTLimitNode = 5;
        Fra_FraigNode( p, pObj );
        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
            p->pPars->nBTLimitNode = nBTracksOld;
        // check implications
        if ( p->pPars->fUseImps )
            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
    }
//    if ( pProgress )
//        Bar_ProgressStop( pProgress );
    // try to prove the outputs of the miter
    p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
//    Fra_MiterStatus( p->pManFraig );
//    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
//        Fra_MiterProve( p );
    // compress implications after processing all of them
    if ( p->pPars->fUseImps )
        Fra_ImpCompactArray( p->pCla->vImps );
}

void Fra_ImpAddToSolver	(	Fra_Man_t *	p,
		Vec_Int_t *	vImps,
		int *	pSatVarNums
	)

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

Synopsis [Add implication clauses to the SAT solver.]

Description [Note that implications should be checked in the first frame!]

SideEffects []

SeeAlso []

Definition at line 428 of file fraImp.c.

{
    sat_solver * pSat = p->pSat;
    Aig_Obj_t * pLeft, * pRight;
    Aig_Obj_t * pLeftF, * pRightF;
    int pLits[2], Imp, Left, Right, i, f, status;
    int fComplL, fComplR;
    Vec_IntForEachEntry( vImps, Imp, i )
    {
        // get the corresponding nodes
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
        // check if all the nodes are present
        for ( f = 0; f < p->pPars->nFramesK; f++ )
        {
            // map these info fraig
            pLeftF = Fra_ObjFraig( pLeft, f );
            pRightF = Fra_ObjFraig( pRight, f );
            if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
            {
                Vec_IntWriteEntry( vImps, i, 0 );
                break;
            }
        } 
        if ( f < p->pPars->nFramesK )
            continue;
        // add constraints in each timeframe
        for ( f = 0; f < p->pPars->nFramesK; f++ )
        {
            // map these info fraig
            pLeftF = Fra_ObjFraig( pLeft, f );
            pRightF = Fra_ObjFraig( pRight, f );
            // get the corresponding SAT numbers
            Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
            Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
            assert( Left > 0  && Left < p->nSatVars );
            assert( Right > 0 && Right < p->nSatVars );
            // get the complemented attributes
            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
            // get the constraint
            // L => R      L' v R     (complement = L & R')
            pLits[0] = 2 * Left  + !fComplL;
            pLits[1] = 2 * Right +  fComplR;
            // add constraint to solver
            if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
            {
                sat_solver_delete( pSat );
                p->pSat = NULL;
                return;
            }
        }
    }
    status = sat_solver_simplify(pSat);
    if ( status == 0 )
    {
        sat_solver_delete( pSat );
        p->pSat = NULL;
    }
//    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
    Fra_ImpCompactArray( vImps );
//    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
}

int Fra_ImpCheckForNode	(	Fra_Man_t *	p,
		Vec_Int_t *	vImps,
		Aig_Obj_t *	pNode,
		int	Pos
	)

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

Synopsis [Check implications for the node (if they are present).]

Description [Returns the new position in the array.]

SideEffects []

SeeAlso []

Definition at line 503 of file fraImp.c.

{
    Aig_Obj_t * pLeft, * pRight;
    Aig_Obj_t * pLeftF, * pRightF;
    int i, Imp, Left, Right, Max, RetValue;
    int fComplL, fComplR;
    Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
    {
        if ( Imp == 0 )
            continue;
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        Max = Abc_MaxInt( Left, Right );
        assert( Max >= pNode->Id );
        if ( Max > pNode->Id )
            return i;
        // get the corresponding nodes
        pLeft  = Aig_ManObj( p->pManAig, Left );
        pRight = Aig_ManObj( p->pManAig, Right );
        // get the corresponding FRAIG nodes
        pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
        pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
        // get the complemented attributes
        fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
        fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
        // check equality
        if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
        {
            if ( fComplL == fComplR ) // x => x  - always true
                continue;
            assert( fComplL != fComplR );
            // consider 4 possibilities:
            // NOT(1) => 1    or   0 => 1  - always true
            // 1 => NOT(1)    or   1 => 0  - never true
            // NOT(x) => x    or   x       - not always true
            // x => NOT(x)    or   NOT(x)  - not always true
            if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
                continue;
            // disproved implication
            p->pCla->fRefinement = 1;
            Vec_IntWriteEntry( vImps, i, 0 );
            continue;
        }
        // check the implication 
        // - if true, a clause is added
        // - if false, a cex is simulated
        // make sure the implication is refined
        RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
        if ( RetValue != 1 )
        {
            p->pCla->fRefinement = 1;
            if ( RetValue == 0 )
                Fra_SmlResimulate( p );
            if ( Vec_IntEntry(vImps, i) != 0 )
                printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
            assert( Vec_IntEntry(vImps, i) == 0 );
        }
    }
    return i;
}

void Fra_ImpCompactArray

(

Vec_Int_t *

vImps

)

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

Synopsis [Removes empty implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 607 of file fraImp.c.

{
    int i, k, Imp;
    k = 0;
    Vec_IntForEachEntry( vImps, Imp, i )
        if ( Imp )
            Vec_IntWriteEntry( vImps, k++, Imp );
    Vec_IntShrink( vImps, k );
}

double Fra_ImpComputeStateSpaceRatio

(

Fra_Man_t *

p

)

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

Synopsis [Determines the ratio of the state space by computed implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 628 of file fraImp.c.

{
    int nSimWords = 64;
    Fra_Sml_t * pComb;
    unsigned * pResult;
    double Ratio = 0.0;
    int Left, Right, Imp, i;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return Ratio;
    // simulate the AIG manager with combinational patterns
    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
    // go through the implications and collect where they do not hold
    pResult = Fra_ObjSim( pComb, 0 );
    assert( pResult[0] == 0 );
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
    }
    // count the number of ones in this area
    Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
    Fra_SmlStop( pComb );
    return Ratio;
}

static int Fra_ImpCreate ( int  Left, int  Right  )

inlinestatic

Definition at line 277 of file fra.h.

{ return (Right << 16) | Left; }

Vec_Int_t* Fra_ImpDerive	(	Fra_Man_t *	p,
		int	nImpMaxLimit,
		int	nImpUseLimit,
		int	fLatchCorr
	)

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

Synopsis [Derives implication candidates.]

Description [Implication candidates have the property that (1) they hold using sequential simulation information (2) they do not hold using combinational simulation information (3) they have as high expressive power as possible (heuristically) that is, they are easy to disprove combinationally meaning they cover relatively larger sequential subspace.]

SideEffects []

SeeAlso []

Definition at line 321 of file fraImp.c.

{
    int nSimWords = 64;
    Fra_Sml_t * pSeq, * pComb;
    Vec_Int_t * vImps, * vTemp;
    Vec_Ptr_t * vNodes;
    int * pImpCosts, * pNodesI, * pNodesK;
    int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
    int CostMin = ABC_INFINITY, CostMax = 0;
    int i, k, Imp, CostRange;
    abctime clk = Abc_Clock();
    assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
    assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
    // normalize both managers
    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 );
    // get the nodes sorted by the number of 1s
    vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
    // count the total number of implications
    for ( k = nSimWords * 32; k > 0; k-- )
    for ( i = k - 1; i > 0; i-- )
    for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
    for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
        nImpsTotal++;

    // compute implications and their costs
    pImpCosts = ABC_ALLOC( int, nImpMaxLimit );
    vImps = Vec_IntAlloc( nImpMaxLimit );
    for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
        for ( i = k - 1; i > 0; i-- )
        {
            // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)

            for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
            for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
            {
                nImpsTried++;
                if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
                {
                    nImpsNonSeq++;
                    continue;
                }
                if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
                {
                    nImpsComb++;
                    continue;
                }
                nImpsCollected++;
                Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
                pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
                CostMin = Abc_MinInt( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
                CostMax = Abc_MaxInt( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
                Vec_IntPush( vImps, Imp );
                if ( Vec_IntSize(vImps) == nImpMaxLimit )
                    goto finish;
            } 
        }
finish:
    Fra_SmlStop( pComb );
    Fra_SmlStop( pSeq );

    // select implications with the highest cost
    CostRange = CostMin;
    if ( Vec_IntSize(vImps) > nImpUseLimit )
    {
        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
        Vec_IntFree( vTemp );  
    }

    // dealloc
    ABC_FREE( pImpCosts ); 
    {
    void * pTemp = Vec_PtrEntry(vNodes, 0);
    ABC_FREE( pTemp );
    }
    Vec_PtrFree( vNodes );
    // reorder implications topologically
    qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
            (int (*)(const void *, const void *)) Sml_CompareMaxId );
if ( p->pPars->fVerbose )
{
printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
       CostMin, CostRange, CostMax );
ABC_PRT( "Time", Abc_Clock() - clk );
}
    return vImps;
}

static int Fra_ImpLeft ( int  Imp )

inlinestatic

Definition at line 275 of file fra.h.

{ return Imp & 0xFFFF;         }

void Fra_ImpRecordInManager	(	Fra_Man_t *	p,
		Aig_Man_t *	pNew
	)

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

Synopsis [Record proven implications in the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 705 of file fraImp.c.

{
    Aig_Obj_t * pLeft, * pRight, * pMiter;
    int nPosOld, Imp, i;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return;
    // go through the implication
    nPosOld = Aig_ManCoNum(pNew);
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
        // record the implication: L' + R
        pMiter = Aig_Or( pNew, 
            Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), 
            Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); 
        Aig_ObjCreateCo( pNew, pMiter );
    }
    pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld;
}

int Fra_ImpRefineUsingCex	(	Fra_Man_t *	p,
		Vec_Int_t *	vImps
	)

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 575 of file fraImp.c.

{
    Aig_Obj_t * pLeft, * pRight;
    int Imp, i, RetValue = 0;
    Vec_IntForEachEntry( vImps, Imp, i )
    {
        if ( Imp == 0 )
            continue;
        // get the corresponding nodes
        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
        // check if implication holds using this simulation info
        if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
        {
            Vec_IntWriteEntry( vImps, i, 0 );
            RetValue = 1;
        }
    }
    return RetValue;
}

static int Fra_ImpRight ( int  Imp )

inlinestatic

Definition at line 276 of file fra.h.

{ return Imp >> 16;            }

int Fra_ImpVerifyUsingSimulation

(

Fra_Man_t *

p

)

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

Synopsis [Returns the number of failed implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 665 of file fraImp.c.

{
    int nFrames = 2000;
    int nSimWords = 8;
    Fra_Sml_t * pSeq;
    char * pfFails;
    int Left, Right, Imp, i, Counter;
    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
        return 0;
    // simulate the AIG manager with combinational patterns
    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1  );
    // go through the implications and check how many of them do not hold
    pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) );
    memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
    {
        Left = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
    }
    // count how many has failed
    Counter = 0;
    for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
        Counter += pfFails[i];
    ABC_FREE( pfFails );
    Fra_SmlStop( pSeq );
    return Counter;
}

int Fra_InvariantVerify	(	Aig_Man_t *	pAig,
		int	nFrames,
		Vec_Int_t *	vClauses,
		Vec_Int_t *	vLits
	)

DECLARATIONS ///.

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

FileName [fraIndVer.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Verification of the inductive invariant.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fraIndVer.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Verifies the inductive invariant.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraIndVer.c.

{
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    int * pStart;
    int RetValue, Beg, End, i, k;
    int CounterBase = 0, CounterInd = 0;
    abctime clk = Abc_Clock();

    if ( nFrames != 1 )
    {
        printf( "Invariant verification: Can only verify for K = 1\n" );
        return 1;
    }

    // derive CNF
    pCnf = Cnf_DeriveSimple( pAig, Aig_ManCoNum(pAig) );
/*
    // add the property
    {
        Aig_Obj_t * pObj;
        int Lits[1];

        pObj = Aig_ManCo( pAig, 0 );
        Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); 

        Vec_IntPush( vLits, Lits[0] );
        Vec_IntPush( vClauses, Vec_IntSize(vLits) );
        printf( "Added the target property to the set of clauses to be inductively checked.\n" );
    }
*/
    // derive initialized frames for the base case
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 );
    // check clauses in the base case
    Beg = 0;
    pStart = Vec_IntArray( vLits );
    Vec_IntForEachEntry( vClauses, End, i )
    {
        // complement the literals
        for ( k = Beg; k < End; k++ )
            pStart[k] = lit_neg(pStart[k]);
        RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 );
        for ( k = Beg; k < End; k++ )
            pStart[k] = lit_neg(pStart[k]);
        Beg = End;
        if ( RetValue == l_False )
            continue;
//        printf( "Clause %d failed the base case.\n", i );
        CounterBase++;
    }
    sat_solver_delete( pSat );

    // derive initialized frames for the base case
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 );
    assert( pSat->size == 2 * pCnf->nVars );
    // add clauses to the first frame
    Beg = 0;
    pStart = Vec_IntArray( vLits );
    Vec_IntForEachEntry( vClauses, End, i )
    {
        RetValue = sat_solver_addclause( pSat, pStart + Beg, pStart + End );
        Beg = End;
        if ( RetValue == 0 )
        {
            Cnf_DataFree( pCnf );
            sat_solver_delete( pSat );
            printf( "Invariant verification: SAT solver is unsat after adding a clause.\n" );
            return 0;
        }
    }
    // simplify the solver
    if ( pSat->qtail != pSat->qhead )
    {
        RetValue = sat_solver_simplify(pSat);
        assert( RetValue != 0 );
        assert( pSat->qtail == pSat->qhead );
    }

    // check clauses in the base case
    Beg = 0;
    pStart = Vec_IntArray( vLits );
    Vec_IntForEachEntry( vClauses, End, i )
    {
        // complement the literals
        for ( k = Beg; k < End; k++ )
        {
            pStart[k] += 2 * pCnf->nVars;
            pStart[k] = lit_neg(pStart[k]);
        }
        RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 );
        for ( k = Beg; k < End; k++ )
        {
            pStart[k] = lit_neg(pStart[k]);
            pStart[k] -= 2 * pCnf->nVars;
        }
        Beg = End;
        if ( RetValue == l_False )
            continue;
//        printf( "Clause %d failed the inductive case.\n", i );
        CounterInd++;
    }
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    if ( CounterBase )
        printf( "Invariant verification: %d clauses (out of %d) FAILED the base case.\n", CounterBase, Vec_IntSize(vClauses) );
    if ( CounterInd )
        printf( "Invariant verification: %d clauses (out of %d) FAILED the inductive case.\n", CounterInd, Vec_IntSize(vClauses) );
    if ( CounterBase || CounterInd )
        return 0;
    printf( "Invariant verification: %d clauses verified correctly.  ", Vec_IntSize(vClauses) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    return 1;
}

void Fra_ManClean	(	Fra_Man_t *	p,
		int	nNodesMax
	)

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file fraMan.c.

{
    int i;
    // remove old arrays
    for ( i = 0; i < p->nMemAlloc; i++ )
        if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
            Vec_PtrFree( p->pMemFanins[i] );
    // realloc for the new size
    if ( p->nMemAlloc < nNodesMax )
    {
        int nMemAllocNew = nNodesMax + 5000;
        p->pMemFanins = ABC_REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
        p->pMemSatNums = ABC_REALLOC( int, p->pMemSatNums, nMemAllocNew );
        p->nMemAlloc = nMemAllocNew;
    }
    // prepare for the new run
    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
}

void Fra_ManFinalizeComb

(

Fra_Man_t *

p

)

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

Synopsis [Finalizes the combinational miter after fraiging.]

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file fraMan.c.

{
    Aig_Obj_t * pObj;
    int i;
    // add the POs
    Aig_ManForEachCo( p->pManAig, pObj, i )
        Aig_ObjCreateCo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
    // postprocess
    Aig_ManCleanMarkB( p->pManFraig );
}

Aig_Man_t* Fra_ManPrepareComb

(

Fra_Man_t *

p

)

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

Synopsis [Prepares the new manager to begin fraiging.]

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file fraMan.c.

{
    Aig_Man_t * pManFraig;
    Aig_Obj_t * pObj;
    int i;
    assert( p->pManFraig == NULL );
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
    pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName );
    pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec );
    pManFraig->nRegs    = p->pManAig->nRegs;
    pManFraig->nAsserts = p->pManAig->nAsserts;
    // set the pointers to the available fraig nodes
    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
    Aig_ManForEachCi( p->pManAig, pObj, i )
        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
    // set the pointers to the manager
    Aig_ManForEachObj( pManFraig, pObj, i )
        pObj->pData = p;
    // allocate memory for mapping FRAIG nodes into SAT numbers and fanins
    p->nMemAlloc = p->nSizeAlloc;
    p->pMemFanins = ABC_ALLOC( Vec_Ptr_t *, p->nMemAlloc );
    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
    p->pMemSatNums = ABC_ALLOC( int, p->nMemAlloc );
    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
    // make sure the satisfying assignment is node assigned
    assert( pManFraig->pData == NULL );
    return pManFraig;
}

void Fra_ManPrint

(

Fra_Man_t *

p

)

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

Synopsis [Prints stats for the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file fraMan.c.

{
    double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
    printf( "SimWord = %d. Round = %d.  Mem = %0.2f MB.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
        p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
    printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", 
        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
    if ( p->pSat )             Sat_SolverPrintStats( stdout, p->pSat );
    if ( p->pPars->fUse1Hot )  Fra_OneHotEstimateCoverage( p, p->vOneHots );
    ABC_PRT( "AIG simulation  ", p->pSml->timeSim  );
    ABC_PRT( "AIG traversal   ", p->timeTrav );
    if ( p->timeRwr )
    {
    ABC_PRT( "AIG rewriting   ", p->timeRwr  );
    }
    ABC_PRT( "SAT solving     ", p->timeSat  );
    ABC_PRT( "    Unsat       ", p->timeSatUnsat );
    ABC_PRT( "    Sat         ", p->timeSatSat   );
    ABC_PRT( "    Fail        ", p->timeSatFail  );
    ABC_PRT( "Class refining  ", p->timeRef   );
    ABC_PRT( "TOTAL RUNTIME   ", p->timeTotal );
    if ( p->time1 ) { ABC_PRT( "time1           ", p->time1 ); }
    if ( p->nSpeculs )
    printf( "Speculations = %d.\n", p->nSpeculs );
    fflush( stdout );
}

Fra_Man_t* Fra_ManStart	(	Aig_Man_t *	pManAig,
		Fra_Par_t *	pPars
	)

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file fraMan.c.

{
    Fra_Man_t * p;
    Aig_Obj_t * pObj;
    int i;
    // allocate the fraiging manager
    p = ABC_ALLOC( Fra_Man_t, 1 );
    memset( p, 0, sizeof(Fra_Man_t) );
    p->pPars      = pPars;
    p->pManAig    = pManAig;
    p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
    p->nFramesAll = pPars->nFramesK + 1;
    // allocate storage for sim pattern
    p->nPatWords  = Abc_BitWordNum( (Aig_ManCiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
    p->pPatWords  = ABC_ALLOC( unsigned, p->nPatWords ); 
    p->vPiVars    = Vec_PtrAlloc( 100 );
    // equivalence classes
    p->pCla       = Fra_ClassesStart( pManAig );
    // allocate other members
    p->pMemFraig  = ABC_ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
    // set random number generator
//    srand( 0xABCABC );
    Aig_ManRandom(1);
    // set the pointer to the manager
    Aig_ManForEachObj( p->pManAig, pObj, i )
        pObj->pData = p;
    return p;
}

void Fra_ManStop

(

Fra_Man_t *

p

)

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

Synopsis [Stops the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file fraMan.c.

{
    if ( p->pPars->fVerbose )
        Fra_ManPrint( p );
    // save mapping from original nodes into FRAIG nodes
    if ( p->pManAig )
    {
        if ( p->pManAig->pObjCopies )
            ABC_FREE( p->pManAig->pObjCopies );
        p->pManAig->pObjCopies = p->pMemFraig;
        p->pMemFraig = NULL;
    }
    Fra_ManClean( p, 0 );
    if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
    if ( p->vPiVars )   Vec_PtrFree( p->vPiVars );
    if ( p->pSat )      sat_solver_delete( p->pSat );
    if ( p->pCla  )     Fra_ClassesStop( p->pCla );
    if ( p->pSml )      Fra_SmlStop( p->pSml );
    if ( p->vCex )      Vec_IntFree( p->vCex );
    if ( p->vOneHots )  Vec_IntFree( p->vOneHots );
    ABC_FREE( p->pMemFraig );
    ABC_FREE( p->pMemFanins );
    ABC_FREE( p->pMemSatNums );
    ABC_FREE( p->pPatWords );
    ABC_FREE( p );
}

int Fra_NodeIsConst	(	Fra_Man_t *	p,
		Aig_Obj_t *	pNew
	)

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

Synopsis [Runs equivalence test for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 425 of file fraSat.c.

{
    int pLits[2], RetValue1, RetValue;
    abctime clk;

    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( pNew != p->pManFraig->pConst1 );
    p->nSatCalls++;

    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }

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

    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, NULL, pNew ); 

    // solve under assumptions
clk = Abc_Clock();
    pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
        (ABC_INT64_T)p->pPars->nBTLimitMiter, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        if ( p->pPatWords )
            Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }

    // return SAT proof
    p->nSatProof++;
    return 1;
}

int Fra_NodesAreClause	(	Fra_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew,
		int	fComplL,
		int	fComplR
	)

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

Synopsis [Runs the result of test for pObj => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file fraSat.c.

{
    int pLits[4], RetValue, RetValue1, nBTLimit;
    abctime clk;//, clk2 = Abc_Clock();
    int status;

    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );

    // if at least one of the nodes is a failed node, perform adjustments:
    // if the backtrack limit is small, simply skip this node
    // if the backtrack limit is > 10, take the quare root of the limit
    nBTLimit = p->pPars->nBTLimitNode;
/*
    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
    {
        p->nSatFails++;
        // fail immediately
//        return -1;
        if ( nBTLimit <= 10 )
            return -1;
        nBTLimit = (int)pow(nBTLimit, 0.7);
    }
*/
    p->nSatCalls++;

    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }

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

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

    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, pOld, pNew ); 

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
clk = Abc_Clock();
//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), !fComplL );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        if ( pOld != p->pManFraig->pConst1 ) 
            pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}

int Fra_NodesAreEquiv	(	Fra_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file fraSat.c.

{
    int pLits[4], RetValue, RetValue1, nBTLimit;
    abctime clk;//, clk2 = Abc_Clock();
    int status;

    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );

    // if at least one of the nodes is a failed node, perform adjustments:
    // if the backtrack limit is small, simply skip this node
    // if the backtrack limit is > 10, take the quare root of the limit
    nBTLimit = p->pPars->nBTLimitNode;
    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
    {
        p->nSatFails++;
        // fail immediately
//        return -1;
        if ( nBTLimit <= 10 )
            return -1;
        nBTLimit = (int)pow(nBTLimit, 0.7);
    }

    p->nSatCalls++;
    p->nSatCallsRecent++;

    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }

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

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

    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, pOld, pNew ); 

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
clk = Abc_Clock();
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        if ( pOld != p->pManFraig->pConst1 ) 
            pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }

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

    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
clk = Abc_Clock();
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
/*
    // check BDD proof
    {
        int RetVal;
        ABC_PRT( "Sat", Abc_Clock() - clk2 );
        clk2 = Abc_Clock();
        RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
//        printf( "%d ", RetVal );
        assert( RetVal );
        ABC_PRT( "Bdd", Abc_Clock() - clk2 );
        printf( "\n" );
    }
*/
    // return SAT proof
    p->nSatProof++;
    return 1;
}

int Fra_NodesAreImp	(	Fra_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew,
		int	fComplL,
		int	fComplR
	)

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

Synopsis [Runs the result of test for pObj => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file fraSat.c.

{
    int pLits[4], RetValue, RetValue1, nBTLimit;
    abctime clk;//, clk2 = Abc_Clock();
    int status;

    // make sure the nodes are not complemented
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );

    // if at least one of the nodes is a failed node, perform adjustments:
    // if the backtrack limit is small, simply skip this node
    // if the backtrack limit is > 10, take the quare root of the limit
    nBTLimit = p->pPars->nBTLimitNode;
/*
    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
    {
        p->nSatFails++;
        // fail immediately
//        return -1;
        if ( nBTLimit <= 10 )
            return -1;
        nBTLimit = (int)pow(nBTLimit, 0.7);
    }
*/
    p->nSatCalls++;

    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        p->nSatVars = 1;
        sat_solver_setnvars( p->pSat, 1000 );
        // var 0 is reserved for const1 node - add the clause
        pLits[0] = toLit( 0 );
        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }

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

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

    // prepare variable activity
    if ( p->pPars->fConeBias )
        Fra_SetActivityFactors( p, pOld, pNew ); 

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
clk = Abc_Clock();
//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
    pLits[0] = toLitCond( Fra_ObjSatNum(pOld),  fComplL );
    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Fra_SmlSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
        // mark the node as the failed node
        if ( pOld != p->pManFraig->pConst1 ) 
            pOld->fMarkB = 1;
        pNew->fMarkB = 1;
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}

static Aig_Obj_t* Fra_ObjChild0Fra ( Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 272 of file fra.h.

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

static Aig_Obj_t* Fra_ObjChild1Fra ( Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 273 of file fra.h.

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

static Vec_Ptr_t* Fra_ObjFaninVec ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 263 of file fra.h.

{ return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }

static Aig_Obj_t* Fra_ObjFraig ( Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 260 of file fra.h.

{ return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }

static unsigned Fra_ObjRandomSim ( )

inlinestatic

Definition at line 258 of file fra.h.

{ return Aig_ManRandom(0);               }

static int Fra_ObjSatNum ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 266 of file fra.h.

{ return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }

static void Fra_ObjSetFaninVec ( Aig_Obj_t *  pObj, Vec_Ptr_t *  vFanins  )

inlinestatic

Definition at line 264 of file fra.h.

{ ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins;   }

static void Fra_ObjSetFraig ( Aig_Obj_t *  pObj, int  i, Aig_Obj_t *  pNode  )

inlinestatic

Definition at line 261 of file fra.h.

{ ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }

static void Fra_ObjSetSatNum ( Aig_Obj_t *  pObj, int  Num  )

inlinestatic

Definition at line 267 of file fra.h.

{ ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }

static unsigned* Fra_ObjSim ( Fra_Sml_t *  p, int  Id  )

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 257 of file fra.h.

{ return p->pData + p->nWordsTotal * Id; }

void Fra_OneHotAddKnownConstraint	(	Fra_Man_t *	p,
		Vec_Ptr_t *	vOnehots
	)

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

Synopsis [Assumes one-hot implications in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file fraHot.c.

{
    Vec_Int_t * vGroup;
    Aig_Obj_t * pObj1, * pObj2;
    int k, i, j, Out1, Out2, pLits[2];
    //
    // these constrants should be added to different timeframes!
    // (also note that PIs follow first - then registers)
    //
    Vec_PtrForEachEntry( Vec_Int_t *, vOnehots, vGroup, k )
    {
        Vec_IntForEachEntry( vGroup, Out1, i )
        Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
        {
            pObj1 = Aig_ManCi( p->pManFraig, Out1 );
            pObj2 = Aig_ManCi( p->pManFraig, Out2 );
            pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
            pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
            // add constraint to solver
            if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
            {
                printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
                sat_solver_delete( p->pSat );
                p->pSat = NULL;
                return;
            }
        }
    }
}

void Fra_OneHotAssume	(	Fra_Man_t *	p,
		Vec_Int_t *	vOneHots
	)

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

Synopsis [Assumes one-hot implications in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file fraHot.c.

{
    Aig_Obj_t * pObj1, * pObj2;
    int i, Out1, Out2, pLits[2];
    int nPiNum = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
    assert( p->pPars->nFramesK == 1 ); // add to only one frame
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        pObj1 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
        pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
        pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
        // add constraint to solver
        if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
        {
            printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" );
            sat_solver_delete( p->pSat );
            p->pSat = NULL;
            return;
        }
    }
}

void Fra_OneHotCheck	(	Fra_Man_t *	p,
		Vec_Int_t *	vOneHots
	)

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

Synopsis [Checks one-hot implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file fraHot.c.

{
    Aig_Obj_t * pObj1, * pObj2;
    int RetValue, i, Out1, Out2;
    int nTruePos = Aig_ManCoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        pObj1 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
        RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) );
        if ( RetValue != 1 )
        {
            p->pCla->fRefinement = 1;
            if ( RetValue == 0 )
                Fra_SmlResimulate( p );
            if ( Vec_IntEntry(vOneHots, i) != 0 )
                printf( "Fra_OneHotCheck(): Clause is not refined!\n" );
            assert( Vec_IntEntry(vOneHots, i) == 0 );
        }
    }
}

Vec_Int_t* Fra_OneHotCompute	(	Fra_Man_t *	p,
		Fra_Sml_t *	pSim
	)

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

Synopsis [Computes one-hot implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file fraHot.c.

{
    int fSkipConstEqu = 1;
    Vec_Int_t * vOneHots;
    Aig_Obj_t * pObj1, * pObj2;
    int i, k;
    int nTruePis = Aig_ManCiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
    assert( pSim->pAig == p->pManAig );
    vOneHots = Vec_IntAlloc( 100 );
    Aig_ManForEachLoSeq( pSim->pAig, pObj1, i )
    {
        if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj1) )
            continue;
        assert( i-nTruePis >= 0 );
//        Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
//        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vCis, pObj2, k, i+1 )
        {
            if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
                continue;
            if ( fSkipConstEqu && Fra_OneHotNodesAreEqual( pSim, pObj1, pObj2 ) )
                continue;
            assert( k-nTruePis >= 0 );
            if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 1 ) )
            {
                Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
                Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
                continue;
            }
            if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 0, 1 ) )
            {
                Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 0) );
                Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
                continue;
            }
            if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 0 ) )
            {
                Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
                Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 0) );
                continue;
            }
        }
    }
    return vOneHots;
}

int Fra_OneHotCount	(	Fra_Man_t *	p,
		Vec_Int_t *	vOneHots
	)

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 303 of file fraHot.c.

{
    int i, Out1, Out2, Counter = 0;
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        Counter++;
    }
    return Counter;
}

Aig_Man_t* Fra_OneHotCreateExdc	(	Fra_Man_t *	p,
		Vec_Int_t *	vOneHots
	)

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

Synopsis [Creates one-hotness EXDC.]

Description []

SideEffects []

SeeAlso []

Definition at line 398 of file fraHot.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj1, * pObj2, * pObj;
    int i, Out1, Out2, nTruePis;
    pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
//    for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
//        Aig_ObjCreateCi(pNew);
    Aig_ManForEachCi( p->pManAig, pObj, i )
        Aig_ObjCreateCi(pNew);
    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        pObj1 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out2) );
        pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
        pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
        pObj  = Aig_Or( pNew, pObj1, pObj2 );
        Aig_ObjCreateCo( pNew, pObj );
    }
    Aig_ManCleanup(pNew);
//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManCoNum(pNew) );
    return pNew;
}

void Fra_OneHotEstimateCoverage	(	Fra_Man_t *	p,
		Vec_Int_t *	vOneHots
	)

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

Synopsis [Estimates the coverage of state space by clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file fraHot.c.

{
    int nSimWords = (1<<14);
    int nRegs = Aig_ManRegNum(p->pManAig);
    Vec_Ptr_t * vSimInfo;
    unsigned * pSim1, * pSim2, * pSimTot;
    int i, w, Out1, Out2, nCovered, Counter = 0;
    abctime clk = Abc_Clock();

    // generate random sim-info at register outputs
    vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
//    srand( 0xAABBAABB );
    Aig_ManRandom(1);
    for ( i = 0; i < nRegs; i++ )
    {
        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, i );
        for ( w = 0; w < nSimWords; w++ )
            pSim1[w] = Fra_ObjRandomSim();
    }
    pSimTot = (unsigned *)Vec_PtrEntry( vSimInfo, nRegs );

    // collect simulation info
    memset( pSimTot, 0, sizeof(unsigned) * nSimWords );
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
//printf( "(%c%d,%c%d) ", 
//Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1), 
//Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) ); 
        Counter++;
        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) );
        pSim2 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) );
        if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) )
            for ( w = 0; w < nSimWords; w++ )
                pSimTot[w] |=  pSim1[w] &  pSim2[w];
        else if ( Fra_LitSign(Out1) )
            for ( w = 0; w < nSimWords; w++ )
                pSimTot[w] |=  pSim1[w] & ~pSim2[w];
        else if ( Fra_LitSign(Out2) )
            for ( w = 0; w < nSimWords; w++ )
                pSimTot[w] |= ~pSim1[w] &  pSim2[w];
        else
            assert( 0 );
    }
//printf( "\n" );
    // count the total number of patterns contained in the don't-care
    nCovered = 0;
    for ( w = 0; w < nSimWords; w++ )
        nCovered += Aig_WordCountOnes( pSimTot[w] );
    Vec_PtrFree( vSimInfo );
    // print the result
    printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
    printf( "(%d out of %d patterns)  ", nSimWords * 32 - nCovered, nSimWords * 32 );
    ABC_PRT( "Time", Abc_Clock() - clk );
}

int Fra_OneHotRefineUsingCex	(	Fra_Man_t *	p,
		Vec_Int_t *	vOneHots
	)

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 266 of file fraHot.c.

{
    Aig_Obj_t * pObj1, * pObj2;
    int i, Out1, Out2, RetValue = 0;
    int nPiNum = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
    assert( p->pSml->pAig == p->pManAig );
    for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
    {
        Out1 = Vec_IntEntry( vOneHots, i );
        Out2 = Vec_IntEntry( vOneHots, i+1 );
        if ( Out1 == 0 && Out2 == 0 )
            continue;
        // get the corresponding nodes
        pObj1 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
        pObj2 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
        // check if implication holds using this simulation info
        if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) )
        {
            Vec_IntWriteEntry( vOneHots, i, 0 );
            Vec_IntWriteEntry( vOneHots, i+1, 0 );
            RetValue = 1;
        }
    }
    return RetValue;
}

void Fra_ParamsDefault

(

Fra_Par_t *

pPars

)

DECLARATIONS ///.

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

FileName [fraMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Starts the FRAIG manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Sets the default solving parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fraMan.c.

{
    memset( pPars, 0, sizeof(Fra_Par_t) );
    pPars->nSimWords        =       32;  // the number of words in the simulation info
    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
    pPars->fPatScores       =        0;  // enables simulation pattern scoring
    pPars->MaxScore         =       25;  // max score after which resimulation is used
    pPars->fDoSparse        =        1;  // skips sparse functions
//    pPars->dActConeRatio    =     0.05;  // the ratio of cone to be bumped
//    pPars->dActConeBumpMax  =      5.0;  // the largest bump of activity
    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
    pPars->nBTLimitNode     =      100;  // conflict limit at a node
    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
    pPars->nFramesK         =        0;  // the number of timeframes to unroll
    pPars->fConeBias        =        1;
    pPars->fRewrite         =        0;
}

void Fra_ParamsDefaultSeq

(

Fra_Par_t *

pPars

)

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

Synopsis [Sets the default solving parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file fraMan.c.

{
    memset( pPars, 0, sizeof(Fra_Par_t) );
    pPars->nSimWords        =        1;  // the number of words in the simulation info
    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
    pPars->fPatScores       =        0;  // enables simulation pattern scoring
    pPars->MaxScore         =       25;  // max score after which resimulation is used
    pPars->fDoSparse        =        1;  // skips sparse functions
    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
    pPars->nBTLimitNode     = 10000000;  // conflict limit at a node
    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
    pPars->nFramesK         =        1;  // the number of timeframes to unroll
    pPars->fConeBias        =        0;
    pPars->fRewrite         =        0;
    pPars->fLatchCorr       =        0;
} 

void Fra_SecSetDefaultParams

(

Fra_Sec_t *

p

)

DECLARATIONS ///.

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

FileName [fraSec.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Performs SEC based on seq sweeping.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file fraSec.c.

{
    memset( p, 0, sizeof(Fra_Sec_t) );
    p->fTryComb          =       1;  // try CEC call as a preprocessing step
    p->fTryBmc           =       1;  // try BMC call as a preprocessing step 
    p->nFramesMax        =       4;  // the max number of frames used for induction
    p->nBTLimit          =    1000;  // conflict limit at a node during induction 
    p->nBTLimitGlobal    = 5000000;  // global conflict limit during induction
    p->nBTLimitInter     =   10000;  // conflict limit during interpolation
    p->nBddVarsMax       =     150;  // the limit on the number of registers in BDD reachability
    p->nBddMax           =   50000;  // the limit on the number of BDD nodes 
    p->nBddIterMax       = 1000000;  // the limit on the number of BDD iterations
    p->fPhaseAbstract    =       0;  // enables phase abstraction
    p->fRetimeFirst      =       1;  // enables most-forward retiming at the beginning
    p->fRetimeRegs       =       1;  // enables min-register retiming at the beginning
    p->fFraiging         =       1;  // enables fraiging at the beginning
    p->fInduction        =       1;  // enables the use of induction (signal correspondence)
    p->fInterpolation    =       1;  // enables interpolation
    p->fInterSeparate    =       0;  // enables interpolation for each outputs separately
    p->fReachability     =       1;  // enables BDD based reachability
    p->fReorderImage     =       1;  // enables variable reordering during image computation
    p->fStopOnFirstFail  =       1;  // enables stopping after first output of a miter has failed to prove
    p->fUseNewProver     =       0;  // enables new prover
    p->fUsePdr           =       1;  // enables PDR
    p->nPdrTimeout       =      60;  // enabled PDR timeout
    p->fSilent           =       0;  // disables all output
    p->fVerbose          =       0;  // enables verbose reporting of statistics
    p->fVeryVerbose      =       0;  // enables very verbose reporting  
    p->TimeLimit         =       0;  // enables the timeout
    // internal parameters
    p->fReportSolution   =       0;  // enables specialized format for reporting solution
}

int Fra_SmlCheckOutput

(

Fra_Man_t *

p

)

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

Synopsis [Returns 1 if the one of the output is already non-constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file fraSim.c.

{
    Aig_Obj_t * pObj;
    int i;
    // make sure the reference simulation pattern does not detect the bug
    pObj = Aig_ManCo( p->pManAig, 0 );
    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
    Aig_ManForEachCo( p->pManAig, pObj, i )
    {
        if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
        {
            // create the counter-example from this pattern
            Fra_SmlCheckOutputSavePattern( p, pObj );
            return 1;
        }
    }
    return 0;
}

Abc_Cex_t* Fra_SmlCopyCounterExample	(	Aig_Man_t *	pAig,
		Aig_Man_t *	pFrames,
		int *	pModel
	)

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

Synopsis [Generates seq counter-example from the combinational one.]

Description []

SideEffects []

SeeAlso []

Definition at line 1117 of file fraSim.c.

{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj;
    int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
    // get the number of frames
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManRegNum(pFrames) == 0 );
    nTruePis = Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig);
    nTruePos = Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig);
    nFrames = Aig_ManCiNum(pFrames) / nTruePis;
    assert( nTruePis * nFrames == Aig_ManCiNum(pFrames) );
    assert( nTruePos * nFrames == Aig_ManCoNum(pFrames) );
    // find the PO that failed
    iPo = -1;
    iFrame = -1;
    Aig_ManForEachCo( pFrames, pObj, i )
        if ( pObj->Id == pModel[Aig_ManCiNum(pFrames)] )
        {
            iPo = i % nTruePos;
            iFrame = i / nTruePos;
            break;
        }
    assert( iPo >= 0 );
    // allocate the counter example
    pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
    pCex->iPo    = iPo;
    pCex->iFrame = iFrame;

    // copy the bit data
    for ( i = 0; i < Aig_ManCiNum(pFrames); i++ )
    {
        if ( pModel[i] )
            Abc_InfoSetBit( pCex->pData, pCex->nRegs + i );
        if ( pCex->nRegs + i == pCex->nBits - 1 )
            break;
    }

    // verify the counter example
    if ( !Saig_ManVerifyCex( pAig, pCex ) )
    {
        printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
        Abc_CexFree( pCex );
        pCex = NULL;
    }
    return pCex;

}

Abc_Cex_t* Fra_SmlGetCounterExample

(

Fra_Sml_t *

p

)

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

Synopsis [Creates sequential counter-example from the simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 1043 of file fraSim.c.

{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj;
    unsigned * pSims;
    int iPo, iFrame, iBit, i, k;

    // make sure the simulation manager has it
    assert( p->fNonConstOut );

    // find the first output that failed
    iPo = -1;
    iBit = -1;
    iFrame = -1;
    Aig_ManForEachPoSeq( p->pAig, pObj, iPo )
    {
        if ( Fra_SmlNodeIsZero(p, pObj) )
            continue;
        pSims = Fra_ObjSim( p, pObj->Id );
        for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
            if ( pSims[i] )
            {
                iFrame = i / p->nWordsFrame;
                iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
                break;
            }
        break;
    }
    assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
    assert( iFrame < p->nFrames );
    assert( iBit < 32 * p->nWordsFrame );

    // allocate the counter example
    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
    pCex->iPo    = iPo;
    pCex->iFrame = iFrame;

    // copy the bit data
    Aig_ManForEachLoSeq( p->pAig, pObj, k )
    {
        pSims = Fra_ObjSim( p, pObj->Id );
        if ( Abc_InfoHasBit( pSims, iBit ) )
            Abc_InfoSetBit( pCex->pData, k );
    }
    for ( i = 0; i <= iFrame; i++ )
    {
        Aig_ManForEachPiSeq( p->pAig, pObj, k )
        {
            pSims = Fra_ObjSim( p, pObj->Id );
            if ( Abc_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
                Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
        }
    }
    // verify the counter example
    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
    {
        printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
        Abc_CexFree( pCex );
        pCex = NULL;
    }
    return pCex;
}

int Fra_SmlNodeCountOnes	(	Fra_Sml_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Counts the number of one's in the patten of the output.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file fraSim.c.

{
    unsigned * pSims;
    int i, Counter = 0;
    pSims = Fra_ObjSim(p, pObj->Id);
    for ( i = 0; i < p->nWordsTotal; i++ )
        Counter += Aig_WordCountOnes( pSims[i] );
    return Counter;
}

int Fra_SmlNodeHash	(	Aig_Obj_t *	pObj,
		int	nTableSize
	)

DECLARATIONS ///.

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

FileName [fraSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraSim.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
    static int s_FPrimes[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->pSml->nWordsTotal <= 128 );
    uHash = 0;
    pSims = Fra_ObjSim(p->pSml, pObj->Id);
    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
        uHash ^= pSims[i] * s_FPrimes[i & 0x7F];
    return uHash % nTableSize;
}

int Fra_SmlNodeIsConst

(

Aig_Obj_t *

pObj

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file fraSim.c.

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

int Fra_SmlNodeNotEquWeight	(	Fra_Sml_t *	p,
		int	Left,
		int	Right
	)

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

Synopsis [Counts the number of 1s in the XOR of simulation data.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file fraSim.c.

{
    unsigned * pSimL, * pSimR;
    int k, Counter = 0;
    pSimL = Fra_ObjSim( p, Left );
    pSimR = Fra_ObjSim( p, Right );
    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
    return Counter;
}

int Fra_SmlNodesAreEqual	(	Aig_Obj_t *	pObj0,
		Aig_Obj_t *	pObj1
	)

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file fraSim.c.

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

void Fra_SmlResimulate

(

Fra_Man_t *

p

)

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

Synopsis [Resimulates fraiging manager after finding a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 703 of file fraSim.c.

{
    int nChanges;
    abctime clk;
    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
    Fra_SmlSimulateOne( p->pSml );
//    if ( p->pPars->fPatScores )
//        Fra_CleanPatScores( p );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
clk = Abc_Clock();
    nChanges = Fra_ClassesRefine( p->pCla );
    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
    if ( p->pCla->vImps )
        nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
    if ( p->vOneHots )
        nChanges += Fra_OneHotRefineUsingCex( p, p->vOneHots );
p->timeRef += Abc_Clock() - clk;
    if ( !p->pPars->nFramesK && nChanges < 1 )
        printf( "Error: A counter-example did not refine classes!\n" );
//    assert( nChanges >= 1 );
//printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
}

void Fra_SmlSavePattern

(

Fra_Man_t *

p

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file fraSim.c.

{
    Aig_Obj_t * pObj;
    int i;
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
    Aig_ManForEachCi( p->pManFraig, pObj, i )
//        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
        if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) )
            Abc_InfoSetBit( p->pPatWords, i );

    if ( p->vCex )
    {
        Vec_IntClear( p->vCex );
        for ( i = 0; i < Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
            Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
        for ( i = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManCiNum(p->pManFraig); i++ )
            Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
    }

/*
    printf( "Pattern: " );
    Aig_ManForEachCi( p->pManFraig, pObj, i )
        printf( "%d", Abc_InfoHasBit( p->pPatWords, i ) );
    printf( "\n" );
*/
}

void Fra_SmlSimulate	(	Fra_Man_t *	p,
		int	fInit
	)

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

Synopsis [Performs simulation of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file fraSim.c.

{
    int fVerbose = 0;
    int nChanges, nClasses;
    abctime clk;
    assert( !fInit || Aig_ManRegNum(p->pManAig) );
    // start the classes
    Fra_SmlInitialize( p->pSml, fInit );
    Fra_SmlSimulateOne( p->pSml );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
//    Fra_ClassesPrint( p->pCla, 0 );
if ( fVerbose )
printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );

//return;

    // refine classes by walking 0/1 patterns
    Fra_SmlSavePattern0( p, fInit );
    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
    Fra_SmlSimulateOne( p->pSml );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
clk = Abc_Clock();
    nChanges = Fra_ClassesRefine( p->pCla );
    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += Abc_Clock() - clk;
if ( fVerbose )
printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
    Fra_SmlSavePattern1( p, fInit );
    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
    Fra_SmlSimulateOne( p->pSml );
    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
        return;
clk = Abc_Clock();
    nChanges = Fra_ClassesRefine( p->pCla );
    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += Abc_Clock() - clk;

if ( fVerbose )
printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
    // refine classes by random simulation
    do {
        Fra_SmlInitialize( p->pSml, fInit );
        Fra_SmlSimulateOne( p->pSml );
        nClasses = Vec_PtrSize(p->pCla->vClasses);
        if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
            return;
clk = Abc_Clock();
        nChanges = Fra_ClassesRefine( p->pCla );
        nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += Abc_Clock() - clk;
if ( fVerbose )
printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
    } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );

//    if ( p->pPars->fVerbose )
//    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
//        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
//    Fra_ClassesPrint( p->pCla, 0 );
}

Fra_Sml_t* Fra_SmlSimulateComb	(	Aig_Man_t *	pAig,
		int	nWords,
		int	fCheckMiter
	)

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

Synopsis [Performs simulation of the uninitialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 856 of file fraSim.c.

{
    Fra_Sml_t * p;
    p = Fra_SmlStart( pAig, 0, 1, nWords );
    Fra_SmlInitialize( p, 0 );
    Fra_SmlSimulateOne( p );
    if ( fCheckMiter )
        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
    return p;
}

Fra_Sml_t* Fra_SmlSimulateCombGiven	(	Aig_Man_t *	pAig,
		char *	pFileName,
		int	fCheckMiter,
		int	fVerbose
	)

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

Synopsis [Assigns simulation patters derived from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 981 of file fraSim.c.

{
    Vec_Str_t * vSimInfo;
    Fra_Sml_t * p;
    int nPatterns;
    assert( Aig_ManRegNum(pAig) == 0 );
    // read comb patterns from file
    vSimInfo = Fra_SmlSimulateReadFile( pFileName );
    if ( vSimInfo == NULL )
        return NULL;
    if ( Vec_StrSize(vSimInfo) % Aig_ManCiNum(pAig) != 0 )
    {
        printf( "File \"%s\": The number of binary digits (%d) is not divisible by the number of primary inputs (%d).\n", 
            pFileName, Vec_StrSize(vSimInfo), Aig_ManCiNum(pAig) );
        Vec_StrFree( vSimInfo );
        return NULL;
    }
    p = Fra_SmlStart( pAig, 0, 1, Abc_BitWordNum(Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig)) );
    Fra_SmlInitializeGiven( p, vSimInfo );
    nPatterns = Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig);
    Vec_StrFree( vSimInfo );
    Fra_SmlSimulateOne( p );
    if ( fCheckMiter )
        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
    if ( fVerbose )
        Fra_SmlPrintOutputs( p, nPatterns );
    return p;
}

Fra_Sml_t* Fra_SmlSimulateSeq	(	Aig_Man_t *	pAig,
		int	nPref,
		int	nFrames,
		int	nWords,
		int	fCheckMiter
	)

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

Synopsis [Performs simulation of the initialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 1021 of file fraSim.c.

{
    Fra_Sml_t * p;
    p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
    Fra_SmlInitialize( p, 1 );
    Fra_SmlSimulateOne( p );
    if ( fCheckMiter )
        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
    return p;
}

Fra_Sml_t* Fra_SmlStart	(	Aig_Man_t *	pAig,
		int	nPref,
		int	nFrames,
		int	nWordsFrame
	)

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 813 of file fraSim.c.

{
    Fra_Sml_t * p;
    p = (Fra_Sml_t *)ABC_ALLOC( char, sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
    memset( p, 0, sizeof(Fra_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;
    // constant 1 is initialized to 0 because we store values modulus phase (pObj->fPhase)
    return p;
}

void Fra_SmlStop

(

Fra_Sml_t *

p

)

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 839 of file fraSim.c.

{
    ABC_FREE( p );
}