ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
wlnGuide.c
Go to the documentation of this file.
1
20
21#include "wln.h"
22
24
28
32
44int Wln_ReadFindToken( char * pToken, Abc_Nam_t * p )
45{
46 char * pBuffer = Abc_UtilStrsavTwo( "\\", pToken );
47 int RetValue = Abc_NamStrFindOrAdd( p, pBuffer, NULL );
48 ABC_FREE( pBuffer );
49 return RetValue;
50}
52{
53 Vec_Int_t * vLevel; int i, k, Obj;
54 Vec_WecForEachLevel( vGuide, vLevel, i )
55 {
56 Vec_IntForEachEntry( vLevel, Obj, k )
57 printf( "%s ", Obj >= 0 ? Abc_NamStr(p, Obj) : "[unknown]" );
58 printf( "\n" );
59 }
60}
61Vec_Wec_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p )
62{
63 char * pBuffer = ABC_CALLOC( char, 10000 ), * pToken;
64 Vec_Wec_t * vTokens = Vec_WecAlloc( 100 ); Vec_Int_t * vLevel;
65 FILE * pFile = fopen( pFileName, "rb" );
66 while ( fgets( pBuffer, 10000, pFile ) )
67 {
68 if ( pBuffer[0] == '#' )
69 continue;
70 vLevel = Vec_WecPushLevel( vTokens );
71 pToken = strtok( pBuffer, " \t\r\n" );
72 while ( pToken )
73 {
74 Vec_IntPush( vLevel, Vec_IntSize(vLevel) < 2 ? Abc_NamStrFindOrAdd(p, pToken, NULL) : Wln_ReadFindToken(pToken, p) );
75 pToken = strtok( NULL, " \t\r\n" );
76 }
77 if ( Vec_IntSize(vLevel) % 4 == 3 ) // account for "property"
78 Vec_IntPush( vLevel, -1 );
79 assert( Vec_IntSize(vLevel) % 4 == 0 );
80 }
81 fclose( pFile );
82 if ( Vec_WecSize(vTokens) == 0 )
83 printf( "Guidance is empty.\n" );
84 //Wln_PrintGuidance( vTokens, p );
85 ABC_FREE( pBuffer );
86 return vTokens;
87}
88
92
93
95
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
int Abc_NamStrFindOrAdd(Abc_Nam_t *p, char *pStr, int *pfFound)
Definition utilNam.c:453
char * Abc_NamStr(Abc_Nam_t *p, int NameId)
Definition utilNam.c:555
typedefABC_NAMESPACE_HEADER_START struct Abc_Nam_t_ Abc_Nam_t
INCLUDES ///.
Definition utilNam.h:39
#define assert(ex)
Definition util_old.h:213
char * strtok()
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
ABC_NAMESPACE_IMPL_START int Wln_ReadFindToken(char *pToken, Abc_Nam_t *p)
DECLARATIONS ///.
Definition wlnGuide.c:44
void Wln_PrintGuidance(Vec_Wec_t *vGuide, Abc_Nam_t *p)
Definition wlnGuide.c:51
Vec_Wec_t * Wln_ReadGuidance(char *pFileName, Abc_Nam_t *p)
Definition wlnGuide.c:61