ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
plaRead.c
Go to the documentation of this file.
1
20
21#include "pla.h"
22
24
28
32
44char * Pla_ReadFile( char * pFileName, char ** ppLimit )
45{
46 char * pBuffer;
47 int nFileSize, RetValue;
48 FILE * pFile = fopen( pFileName, "rb" );
49 if ( pFile == NULL )
50 {
51 printf( "Cannot open input file.\n" );
52 return NULL;
53 }
54 // get the file size, in bytes
55 fseek( pFile, 0, SEEK_END );
56 nFileSize = ftell( pFile );
57 // move the file current reading position to the beginning
58 rewind( pFile );
59 // load the contents of the file into memory
60 pBuffer = ABC_ALLOC( char, nFileSize + 16 );
61 pBuffer[0] = '\n';
62 RetValue = fread( pBuffer+1, nFileSize, 1, pFile );
63 fclose( pFile );
64 // terminate the string with '\0'
65 pBuffer[nFileSize + 1] = '\n';
66 pBuffer[nFileSize + 2] = '\0';
67 *ppLimit = pBuffer + nFileSize + 3;
68 return pBuffer;
69}
70
82void Pla_ReadPlaRemoveComments( char * pBuffer, char * pLimit )
83{
84 char * pTemp;
85 for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
86 if ( *pTemp == '#' )
87 while ( *pTemp && *pTemp != '\n' )
88 *pTemp++ = ' ';
89}
90int Pla_ReadPlaHeader( char * pBuffer, char * pLimit, int * pnIns, int * pnOuts, int * pnCubes, int * pType )
91{
92 char * pTemp;
93 *pType = PLA_FILE_FD;
94 *pnIns = *pnOuts = *pnCubes = -1;
95 for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
96 {
97 if ( *pTemp != '.' )
98 continue;
99 if ( !strncmp(pTemp, ".i ", 3) )
100 *pnIns = atoi( pTemp + 3 );
101 else if ( !strncmp(pTemp, ".o ", 3) )
102 *pnOuts = atoi( pTemp + 3 );
103 else if ( !strncmp(pTemp, ".p ", 3) )
104 *pnCubes = atoi( pTemp + 3 );
105 else if ( !strncmp(pTemp, ".e ", 3) )
106 break;
107 else if ( !strncmp(pTemp, ".type ", 6) )
108 {
109 char Buffer[100];
110 *pType = PLA_FILE_NONE;
111 sscanf( pTemp+6, "%s", Buffer );
112 if ( !strcmp(Buffer, "f") )
113 *pType = PLA_FILE_F;
114 else if ( !strcmp(Buffer, "fr") )
115 *pType = PLA_FILE_FR;
116 else if ( !strcmp(Buffer, "fd") )
117 *pType = PLA_FILE_FD;
118 else if ( !strcmp(Buffer, "fdr") )
119 *pType = PLA_FILE_FDR;
120 }
121 }
122 if ( *pnIns <= 0 )
123 printf( "The number of inputs (.i) should be positive.\n" );
124 if ( *pnOuts <= 0 )
125 printf( "The number of outputs (.o) should be positive.\n" );
126 return *pnIns > 0 && *pnOuts > 0;
127}
128Vec_Str_t * Pla_ReadPlaBody( char * pBuffer, char * pLimit, Pla_File_t Type )
129{
130 char * pTemp;
131 Vec_Str_t * vLits;
132 vLits = Vec_StrAlloc( 10000 );
133 for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
134 {
135 if ( *pTemp == '.' )
136 while ( *pTemp && *pTemp != '\n' )
137 pTemp++;
138 if ( *pTemp == '0' )
139 Vec_StrPush( vLits, (char)PLA_LIT_ZERO );
140 else if ( *pTemp == '1' )
141 Vec_StrPush( vLits, (char)PLA_LIT_ONE );
142 else if ( *pTemp == '-' || *pTemp == '2' )
143 Vec_StrPush( vLits, (char)PLA_LIT_DASH );
144 else if ( *pTemp == '~' ) // no meaning
145 {
146 if ( Type == PLA_FILE_F || Type == PLA_FILE_FD )
147 Vec_StrPush( vLits, (char)PLA_LIT_ZERO );
148 else if ( Type == PLA_FILE_FR )
149 Vec_StrPush( vLits, (char)PLA_LIT_DASH );
150 else if ( Type == PLA_FILE_FDR )
151 Vec_StrPush( vLits, (char)PLA_LIT_FULL );
152 else assert( 0 );
153 }
154 }
155 return vLits;
156}
158{
159 word * pCubeIn, * pCubeOut;
160 int i, k, Lit, Count = 0;
161 int nCubesReal = Vec_StrSize(vLits) / (p->nIns + p->nOuts);
162 assert( Vec_StrSize(vLits) % (p->nIns + p->nOuts) == 0 );
163 if ( nCubesReal != Pla_ManCubeNum(p) )
164 {
165 printf( "Warning: Declared number of cubes (%d) differs from the actual (%d).\n",
166 Pla_ManCubeNum(p), nCubesReal );
167 if ( nCubesReal < Pla_ManCubeNum(p) )
168 Vec_IntShrink( &p->vCubes, nCubesReal );
169 else
170 {
171 assert( nCubesReal > Pla_ManCubeNum(p) );
172 Vec_IntFillNatural( &p->vCubes, nCubesReal );
173 Vec_WrdFillExtra( &p->vInBits, nCubesReal * p->nInWords, 0 );
174 Vec_WrdFillExtra( &p->vOutBits, nCubesReal * p->nOutWords, 0 );
175 }
176 }
177 Pla_ForEachCubeInOut( p, pCubeIn, pCubeOut, i )
178 {
179 Pla_CubeForEachLit( p->nIns, pCubeIn, Lit, k )
180 Pla_CubeSetLit( pCubeIn, k, (Pla_Lit_t)Vec_StrEntry(vLits, Count++) );
181 Pla_CubeForEachLit( p->nOuts, pCubeOut, Lit, k )
182 Pla_CubeSetLit( pCubeOut, k, (Pla_Lit_t)Vec_StrEntry(vLits, Count++) );
183 }
184 assert( Count == Vec_StrSize(vLits) );
185}
186Pla_Man_t * Pla_ReadPla( char * pFileName )
187{
188 Pla_Man_t * p;
189 Vec_Str_t * vLits;
190 int nIns, nOuts, nCubes, Type;
191 char * pBuffer, * pLimit;
192 pBuffer = Pla_ReadFile( pFileName, &pLimit );
193 if ( pBuffer == NULL )
194 return NULL;
195 Pla_ReadPlaRemoveComments( pBuffer, pLimit );
196 if ( Pla_ReadPlaHeader( pBuffer, pLimit, &nIns, &nOuts, &nCubes, &Type ) )
197 {
198 vLits = Pla_ReadPlaBody( pBuffer, pLimit, (Pla_File_t)Type );
199 if ( Vec_StrSize(vLits) % (nIns + nOuts) == 0 )
200 {
201 if ( nCubes == -1 )
202 nCubes = Vec_StrSize(vLits) / (nIns + nOuts);
203 p = Pla_ManAlloc( pFileName, nIns, nOuts, nCubes );
204 p->Type = (Pla_File_t)Type;
205 Pla_ReadAddBody( p, vLits );
206 Vec_StrFree( vLits );
207 ABC_FREE( pBuffer );
208 return p;
209 }
210 printf( "Literal count is incorrect (in = %d; out = %d; lit = %d).\n", nIns, nOuts, Vec_StrSize(vLits) );
211 Vec_StrFree( vLits );
212 }
213 ABC_FREE( pBuffer );
214 return NULL;
215}
216
217
221
222
224
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Cube * p
Definition exorList.c:222
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
void Pla_ReadPlaRemoveComments(char *pBuffer, char *pLimit)
Definition plaRead.c:82
ABC_NAMESPACE_IMPL_START char * Pla_ReadFile(char *pFileName, char **ppLimit)
DECLARATIONS ///.
Definition plaRead.c:44
Pla_Man_t * Pla_ReadPla(char *pFileName)
Definition plaRead.c:186
Vec_Str_t * Pla_ReadPlaBody(char *pBuffer, char *pLimit, Pla_File_t Type)
Definition plaRead.c:128
void Pla_ReadAddBody(Pla_Man_t *p, Vec_Str_t *vLits)
Definition plaRead.c:157
int Pla_ReadPlaHeader(char *pBuffer, char *pLimit, int *pnIns, int *pnOuts, int *pnCubes, int *pType)
Definition plaRead.c:90
#define Pla_CubeForEachLit(nVars, pCube, Lit, i)
Definition pla.h:124
Pla_File_t
BASIC TYPES ///.
Definition pla.h:46
@ PLA_FILE_FR
Definition pla.h:49
@ PLA_FILE_FDR
Definition pla.h:50
@ PLA_FILE_NONE
Definition pla.h:51
@ PLA_FILE_F
Definition pla.h:48
@ PLA_FILE_FD
Definition pla.h:47
struct Pla_Man_t_ Pla_Man_t
Definition pla.h:63
#define Pla_ForEachCubeInOut(p, pCubeIn, pCubeOut, i)
Definition pla.h:121
Pla_Lit_t
Definition pla.h:55
@ PLA_LIT_ONE
Definition pla.h:58
@ PLA_LIT_FULL
Definition pla.h:59
@ PLA_LIT_ZERO
Definition pla.h:57
@ PLA_LIT_DASH
Definition pla.h:56
#define assert(ex)
Definition util_old.h:213
int strncmp()
int strcmp()
VOID_HACK rewind()
#define SEEK_END
Definition zconf.h:392