ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
llb2Dump.c
Go to the documentation of this file.
1
20
21#include "llbInt.h"
22
24
25
29
33
45char * Llb_ManGetDummyName( char * pPrefix, int Num, int nDigits )
46{
47 static char Buffer[2000];
48 sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
49 return Buffer;
50}
51
63void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char * pFileName )
64{
65 FILE * pFile;
66 Vec_Ptr_t * vNamesIn, * vNamesOut;
67 char * pName;
68 int i, nDigits;
69 // reorder the BDD
70 Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 );
71
72 // create input names
73 nDigits = Abc_Base10Log( Cudd_ReadSize(ddG) );
74 vNamesIn = Vec_PtrAlloc( Cudd_ReadSize(ddG) );
75 for ( i = 0; i < Cudd_ReadSize(ddG); i++ )
76 {
77 pName = Llb_ManGetDummyName( "ff", i, nDigits );
78 Vec_PtrPush( vNamesIn, Extra_UtilStrsav(pName) );
79 }
80 // create output names
81 vNamesOut = Vec_PtrAlloc( 1 );
82 Vec_PtrPush( vNamesOut, Extra_UtilStrsav("Reached") );
83
84 // write the file
85 pFile = fopen( pFileName, "wb" );
86 Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile, 0 );
87 fclose( pFile );
88
89 // cleanup
90 Vec_PtrForEachEntry( char *, vNamesIn, pName, i )
91 ABC_FREE( pName );
92 Vec_PtrForEachEntry( char *, vNamesOut, pName, i )
93 ABC_FREE( pName );
94 Vec_PtrFree( vNamesIn );
95 Vec_PtrFree( vNamesOut );
96}
97
101
102
104
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
char * Extra_UtilStrsav(const char *s)
ABC_NAMESPACE_IMPL_START char * Llb_ManGetDummyName(char *pPrefix, int Num, int nDigits)
DECLARATIONS ///.
Definition llb2Dump.c:45
void Llb_ManDumpReached(DdManager *ddG, DdNode *bReached, char *pModel, char *pFileName)
Definition llb2Dump.c:63
char * sprintf()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55