ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
parseEqn.c File Reference
#include "parseInt.h"
Include dependency graph for parseEqn.c:

Go to the source code of this file.

Macros

#define PARSE_EQN_SYM_OPEN   '('
 DECLARATIONS ///.
 
#define PARSE_EQN_SYM_CLOSE   ')'
 
#define PARSE_EQN_SYM_CONST0   '0'
 
#define PARSE_EQN_SYM_CONST1   '1'
 
#define PARSE_EQN_SYM_NEG   '!'
 
#define PARSE_EQN_SYM_AND   '*'
 
#define PARSE_EQN_SYM_XOR   '^'
 
#define PARSE_EQN_SYM_OR   '+'
 
#define PARSE_EQN_OPER_NEG   10
 
#define PARSE_EQN_OPER_AND   9
 
#define PARSE_EQN_OPER_XOR   8
 
#define PARSE_EQN_OPER_OR   7
 
#define PARSE_EQN_OPER_MARK   1
 
#define PARSE_EQN_FLAG_START   1
 
#define PARSE_EQN_FLAG_VAR   2
 
#define PARSE_EQN_FLAG_OPER   3
 
#define PARSE_EQN_FLAG_ERROR   4
 
#define PARSE_EQN_STACKSIZE   1000
 

Functions

Hop_Obj_tParse_FormulaParserEqn (FILE *pOutput, char *pFormInit, Vec_Ptr_t *vVarNames, Hop_Man_t *pMan)
 FUNCTION DEFINITIONS ///.
 

Macro Definition Documentation

◆ PARSE_EQN_FLAG_ERROR

#define PARSE_EQN_FLAG_ERROR   4

Definition at line 49 of file parseEqn.c.

◆ PARSE_EQN_FLAG_OPER

#define PARSE_EQN_FLAG_OPER   3

Definition at line 48 of file parseEqn.c.

◆ PARSE_EQN_FLAG_START

#define PARSE_EQN_FLAG_START   1

Definition at line 46 of file parseEqn.c.

◆ PARSE_EQN_FLAG_VAR

#define PARSE_EQN_FLAG_VAR   2

Definition at line 47 of file parseEqn.c.

◆ PARSE_EQN_OPER_AND

#define PARSE_EQN_OPER_AND   9

Definition at line 40 of file parseEqn.c.

◆ PARSE_EQN_OPER_MARK

#define PARSE_EQN_OPER_MARK   1

Definition at line 43 of file parseEqn.c.

◆ PARSE_EQN_OPER_NEG

#define PARSE_EQN_OPER_NEG   10

Definition at line 39 of file parseEqn.c.

◆ PARSE_EQN_OPER_OR

#define PARSE_EQN_OPER_OR   7

Definition at line 42 of file parseEqn.c.

◆ PARSE_EQN_OPER_XOR

#define PARSE_EQN_OPER_XOR   8

Definition at line 41 of file parseEqn.c.

◆ PARSE_EQN_STACKSIZE

#define PARSE_EQN_STACKSIZE   1000

Definition at line 51 of file parseEqn.c.

◆ PARSE_EQN_SYM_AND

#define PARSE_EQN_SYM_AND   '*'

Definition at line 34 of file parseEqn.c.

◆ PARSE_EQN_SYM_CLOSE

#define PARSE_EQN_SYM_CLOSE   ')'

Definition at line 30 of file parseEqn.c.

◆ PARSE_EQN_SYM_CONST0

#define PARSE_EQN_SYM_CONST0   '0'

Definition at line 31 of file parseEqn.c.

◆ PARSE_EQN_SYM_CONST1

#define PARSE_EQN_SYM_CONST1   '1'

Definition at line 32 of file parseEqn.c.

◆ PARSE_EQN_SYM_NEG

#define PARSE_EQN_SYM_NEG   '!'

Definition at line 33 of file parseEqn.c.

◆ PARSE_EQN_SYM_OPEN

#define PARSE_EQN_SYM_OPEN   '('

DECLARATIONS ///.

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

FileNameIn [parseEqn.c]

PackageName [ABC: Logic synthesis and verification system.]

Synopsis [Boolean formula parser.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - December 18, 2006.]

Revision [

Id
parseEqn.c,v 1.0 2006/12/18 00:00:00 alanmi Exp

]

Definition at line 29 of file parseEqn.c.

◆ PARSE_EQN_SYM_OR

#define PARSE_EQN_SYM_OR   '+'

Definition at line 36 of file parseEqn.c.

◆ PARSE_EQN_SYM_XOR

#define PARSE_EQN_SYM_XOR   '^'

Definition at line 35 of file parseEqn.c.

Function Documentation

◆ Parse_FormulaParserEqn()

Hop_Obj_t * Parse_FormulaParserEqn ( FILE * pOutput,
char * pFormInit,
Vec_Ptr_t * vVarNames,
Hop_Man_t * pMan )

FUNCTION DEFINITIONS ///.

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

Synopsis [Derives the AIG corresponding to the equation.]

Description [Takes the stream to output messages, the formula, the vector of variable names and the AIG manager.]

SideEffects []

SeeAlso []

Definition at line 71 of file parseEqn.c.

72{
73 char * pFormula;
74 Parse_StackFn_t * pStackFn;
75 Parse_StackOp_t * pStackOp;
76 Hop_Obj_t * gFunc;
77 char * pTemp, * pName;
78 int nParans, fFound, Flag;
79 int Oper, Oper1, Oper2;
80 int i, v;
81
82 // make sure that the number of opening and closing parentheses is the same
83 nParans = 0;
84 for ( pTemp = pFormInit; *pTemp; pTemp++ )
85 if ( *pTemp == '(' )
86 nParans++;
87 else if ( *pTemp == ')' )
88 nParans--;
89 if ( nParans != 0 )
90 {
91 fprintf( pOutput, "Parse_FormulaParserEqn(): Different number of opening and closing parentheses ().\n" );
92 return NULL;
93 }
94
95 // copy the formula
96 pFormula = ABC_ALLOC( char, strlen(pFormInit) + 3 );
97 sprintf( pFormula, "(%s)", pFormInit );
98
99 // start the stacks
102
104 for ( pTemp = pFormula; *pTemp; pTemp++ )
105 {
106 switch ( *pTemp )
107 {
108 // skip all spaces, tabs, and end-of-lines
109 case ' ':
110 case '\t':
111 case '\r':
112 case '\n':
113 continue;
115 Parse_StackFnPush( pStackFn, Hop_ManConst0(pMan) ); // Cudd_Ref( b0 );
116 if ( Flag == PARSE_EQN_FLAG_VAR )
117 {
118 fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 0.\n" );
119 Flag = PARSE_EQN_FLAG_ERROR;
120 break;
121 }
122 Flag = PARSE_EQN_FLAG_VAR;
123 break;
125 Parse_StackFnPush( pStackFn, Hop_ManConst1(pMan) ); // Cudd_Ref( b1 );
126 if ( Flag == PARSE_EQN_FLAG_VAR )
127 {
128 fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 1.\n" );
129 Flag = PARSE_EQN_FLAG_ERROR;
130 break;
131 }
132 Flag = PARSE_EQN_FLAG_VAR;
133 break;
135 if ( Flag == PARSE_EQN_FLAG_VAR )
136 {// if NEGBEF follows a variable, AND is assumed
138 Flag = PARSE_EQN_FLAG_OPER;
139 }
141 break;
144 case PARSE_EQN_SYM_OR:
145 if ( Flag != PARSE_EQN_FLAG_VAR )
146 {
147 fprintf( pOutput, "Parse_FormulaParserEqn(): There is no variable before AND, EXOR, or OR.\n" );
148 Flag = PARSE_EQN_FLAG_ERROR;
149 break;
150 }
151 if ( *pTemp == PARSE_EQN_SYM_AND )
153 else if ( *pTemp == PARSE_EQN_SYM_OR )
155 else //if ( *pTemp == PARSE_EQN_SYM_XOR )
157 Flag = PARSE_EQN_FLAG_OPER;
158 break;
160 if ( Flag == PARSE_EQN_FLAG_VAR )
161 {
162// Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND );
163 fprintf( pOutput, "Parse_FormulaParserEqn(): An opening parenthesis follows a var without operation sign.\n" );
164 Flag = PARSE_EQN_FLAG_ERROR;
165 break;
166 }
168 // after an opening bracket, it feels like starting over again
169 Flag = PARSE_EQN_FLAG_START;
170 break;
172 if ( !Parse_StackOpIsEmpty( pStackOp ) )
173 {
174 while ( 1 )
175 {
176 if ( Parse_StackOpIsEmpty( pStackOp ) )
177 {
178 fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening parenthesis\n" );
179 Flag = PARSE_EQN_FLAG_ERROR;
180 break;
181 }
182 Oper = Parse_StackOpPop( pStackOp );
183 if ( Oper == PARSE_EQN_OPER_MARK )
184 break;
185
186 // perform the given operation
187 if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper ) == NULL )
188 {
189 Parse_StackFnFree( pStackFn );
190 Parse_StackOpFree( pStackOp );
191 fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
192 ABC_FREE( pFormula );
193 return NULL;
194 }
195 }
196 }
197 else
198 {
199 fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening parenthesis\n" );
200 Flag = PARSE_EQN_FLAG_ERROR;
201 break;
202 }
203 if ( Flag != PARSE_EQN_FLAG_ERROR )
204 Flag = PARSE_EQN_FLAG_VAR;
205 break;
206
207
208 default:
209 // scan the next name
210 for ( i = 0; pTemp[i] &&
211 pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
212 pTemp[i] != PARSE_EQN_SYM_AND && pTemp[i] != PARSE_EQN_SYM_OR && pTemp[i] != PARSE_EQN_SYM_XOR && pTemp[i] != PARSE_EQN_SYM_CLOSE; i++ )
213 {
214 if ( pTemp[i] == PARSE_EQN_SYM_NEG || pTemp[i] == PARSE_EQN_SYM_OPEN )
215 {
216 fprintf( pOutput, "Parse_FormulaParserEqn(): The negation sign or an opening parenthesis inside the variable name.\n" );
217 Flag = PARSE_EQN_FLAG_ERROR;
218 break;
219 }
220 }
221 // variable name is found
222 fFound = 0;
223 Vec_PtrForEachEntry( char *, vVarNames, pName, v )
224 if ( strncmp(pTemp, pName, i) == 0 && strlen(pName) == (unsigned)i )
225 {
226 pTemp += i-1;
227 fFound = 1;
228 break;
229 }
230 if ( !fFound )
231 {
232 fprintf( pOutput, "Parse_FormulaParserEqn(): The parser cannot find var \"%s\" in the input var list.\n", pTemp );
233 Flag = PARSE_EQN_FLAG_ERROR;
234 break;
235 }
236 if ( Flag == PARSE_EQN_FLAG_VAR )
237 {
238 fprintf( pOutput, "Parse_FormulaParserEqn(): The variable name \"%s\" follows another var without operation sign.\n", pTemp );
239 Flag = PARSE_EQN_FLAG_ERROR;
240 break;
241 }
242 Parse_StackFnPush( pStackFn, Hop_IthVar( pMan, v ) ); // Cudd_Ref( pbVars[v] );
243 Flag = PARSE_EQN_FLAG_VAR;
244 break;
245 }
246
247 if ( Flag == PARSE_EQN_FLAG_ERROR )
248 break; // error exit
249 else if ( Flag == PARSE_EQN_FLAG_START )
250 continue; // go on parsing
251 else if ( Flag == PARSE_EQN_FLAG_VAR )
252 while ( 1 )
253 { // check if there are negations in the OpStack
254 if ( Parse_StackOpIsEmpty(pStackOp) )
255 break;
256 Oper = Parse_StackOpPop( pStackOp );
257 if ( Oper != PARSE_EQN_OPER_NEG )
258 {
259 Parse_StackOpPush( pStackOp, Oper );
260 break;
261 }
262 else
263 {
264 Parse_StackFnPush( pStackFn, Hop_Not((Hop_Obj_t *)Parse_StackFnPop(pStackFn)) );
265 }
266 }
267 else // if ( Flag == PARSE_EQN_FLAG_OPER )
268 while ( 1 )
269 { // execute all the operations in the OpStack
270 // with precedence higher or equal than the last one
271 Oper1 = Parse_StackOpPop( pStackOp ); // the last operation
272 if ( Parse_StackOpIsEmpty(pStackOp) )
273 { // if it is the only operation, push it back
274 Parse_StackOpPush( pStackOp, Oper1 );
275 break;
276 }
277 Oper2 = Parse_StackOpPop( pStackOp ); // the operation before the last one
278 if ( Oper2 >= Oper1 )
279 { // if Oper2 precedence is higher or equal, execute it
280 if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper2 ) == NULL )
281 {
282 fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
283 ABC_FREE( pFormula );
284 Parse_StackFnFree( pStackFn );
285 Parse_StackOpFree( pStackOp );
286 return NULL;
287 }
288 Parse_StackOpPush( pStackOp, Oper1 ); // push the last operation back
289 }
290 else
291 { // if Oper2 precedence is lower, push them back and done
292 Parse_StackOpPush( pStackOp, Oper2 );
293 Parse_StackOpPush( pStackOp, Oper1 );
294 break;
295 }
296 }
297 }
298
299 if ( Flag != PARSE_EQN_FLAG_ERROR )
300 {
301 if ( !Parse_StackFnIsEmpty(pStackFn) )
302 {
303 gFunc = (Hop_Obj_t *)Parse_StackFnPop(pStackFn);
304 if ( Parse_StackFnIsEmpty(pStackFn) )
305 if ( Parse_StackOpIsEmpty(pStackOp) )
306 {
307 Parse_StackFnFree(pStackFn);
308 Parse_StackOpFree(pStackOp);
309// Cudd_Deref( gFunc );
310 ABC_FREE( pFormula );
311 return gFunc;
312 }
313 else
314 fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the operation stack\n" );
315 else
316 fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the function stack\n" );
317 }
318 else
319 fprintf( pOutput, "Parse_FormulaParserEqn(): The input string is empty\n" );
320 }
321 ABC_FREE( pFormula );
322 return NULL;
323}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition hopOper.c:63
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
#define PARSE_EQN_OPER_OR
Definition parseEqn.c:42
#define PARSE_EQN_SYM_CONST0
Definition parseEqn.c:31
#define PARSE_EQN_SYM_CONST1
Definition parseEqn.c:32
#define PARSE_EQN_OPER_XOR
Definition parseEqn.c:41
#define PARSE_EQN_SYM_OR
Definition parseEqn.c:36
#define PARSE_EQN_SYM_OPEN
DECLARATIONS ///.
Definition parseEqn.c:29
#define PARSE_EQN_FLAG_OPER
Definition parseEqn.c:48
#define PARSE_EQN_FLAG_START
Definition parseEqn.c:46
#define PARSE_EQN_FLAG_ERROR
Definition parseEqn.c:49
#define PARSE_EQN_SYM_XOR
Definition parseEqn.c:35
#define PARSE_EQN_SYM_AND
Definition parseEqn.c:34
#define PARSE_EQN_STACKSIZE
Definition parseEqn.c:51
#define PARSE_EQN_FLAG_VAR
Definition parseEqn.c:47
#define PARSE_EQN_SYM_NEG
Definition parseEqn.c:33
#define PARSE_EQN_SYM_CLOSE
Definition parseEqn.c:30
#define PARSE_EQN_OPER_NEG
Definition parseEqn.c:39
#define PARSE_EQN_OPER_AND
Definition parseEqn.c:40
#define PARSE_EQN_OPER_MARK
Definition parseEqn.c:43
struct ParseStackOpStruct Parse_StackOp_t
Definition parseInt.h:42
Parse_StackFn_t * Parse_StackFnStart(int nDepth)
GLOBAL VARIABLES ///.
Definition parseStack.c:57
void * Parse_StackFnPop(Parse_StackFn_t *p)
Definition parseStack.c:115
void Parse_StackFnFree(Parse_StackFn_t *p)
Definition parseStack.c:136
void Parse_StackFnPush(Parse_StackFn_t *p, void *bFunc)
Definition parseStack.c:94
Parse_StackOp_t * Parse_StackOpStart(int nDepth)
Definition parseStack.c:156
int Parse_StackOpIsEmpty(Parse_StackOp_t *p)
Definition parseStack.c:177
typedefABC_NAMESPACE_HEADER_START struct ParseStackFnStruct Parse_StackFn_t
INCLUDES ///.
Definition parseInt.h:41
void Parse_StackOpPush(Parse_StackOp_t *p, int Oper)
Definition parseStack.c:193
int Parse_StackFnIsEmpty(Parse_StackFn_t *p)
Definition parseStack.c:78
int Parse_StackOpPop(Parse_StackOp_t *p)
Definition parseStack.c:214
void Parse_StackOpFree(Parse_StackOp_t *p)
Definition parseStack.c:235
int strncmp()
int strlen()
char * sprintf()
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function: