/**CFile****************************************************************

  FileName    [verFormula.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Verilog parser.]

  Synopsis    [Formula parser to read Verilog assign statements.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - August 19, 2006.]

  Revision    [$Id: verFormula.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]

***********************************************************************/

#include "ver.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

// the list of operation symbols to be used in expressions
#define VER_PARSE_SYM_OPEN    '('   // opening parenthesis
#define VER_PARSE_SYM_CLOSE   ')'   // closing parenthesis
#define VER_PARSE_SYM_CONST0  '0'   // constant 0
#define VER_PARSE_SYM_CONST1  '1'   // constant 1
#define VER_PARSE_SYM_NEGBEF1 '!'   // negation before the variable
#define VER_PARSE_SYM_NEGBEF2 '~'   // negation before the variable
#define VER_PARSE_SYM_AND     '&'   // logic AND
#define VER_PARSE_SYM_OR      '|'   // logic OR
#define VER_PARSE_SYM_XOR     '^'   // logic XOR
#define VER_PARSE_SYM_MUX1    '?'   // first symbol of MUX
#define VER_PARSE_SYM_MUX2    ':'   // second symbol of MUX

// the list of opcodes (also specifying operation precedence)
#define VER_PARSE_OPER_NEG     7    // negation (highest precedence)
#define VER_PARSE_OPER_AND     6    // logic AND
#define VER_PARSE_OPER_XOR     5    // logic EXOR   (a'b | ab')   
#define VER_PARSE_OPER_OR      4    // logic OR
#define VER_PARSE_OPER_EQU     3    // equvalence   (a'b'| ab )
#define VER_PARSE_OPER_MUX     2    // MUX(a,b,c)   (ab | a'c )
#define VER_PARSE_OPER_MARK    1    // OpStack token standing for an opening parenthesis

// these are values of the internal Flag
#define VER_PARSE_FLAG_START   1    // after the opening parenthesis 
#define VER_PARSE_FLAG_VAR     2    // after operation is received
#define VER_PARSE_FLAG_OPER    3    // after operation symbol is received
#define VER_PARSE_FLAG_ERROR   4    // when error is detected

static Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper );
static int         Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Parser of the formula encountered in assign statements.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage )
{
    char * pTemp;
    Hop_Obj_t * bFunc, * bTemp;
    int nParans, Flag;
	int Oper, Oper1, Oper2;
    int v;

    // clear the stacks and the names
    Vec_PtrClear( vNames );
    Vec_PtrClear( vStackFn );
    Vec_IntClear( vStackOp );

    if ( !strcmp(pFormula, "0") || !strcmp(pFormula, "1\'b0") )
        return Hop_ManConst0((Hop_Man_t *)pMan);
    if ( !strcmp(pFormula, "1") || !strcmp(pFormula, "1\'b1") )
        return Hop_ManConst1((Hop_Man_t *)pMan);

    // make sure that the number of opening and closing parentheses is the same
    nParans = 0;
    for ( pTemp = pFormula; *pTemp; pTemp++ )
        if ( *pTemp == '(' )
            nParans++;
        else if ( *pTemp == ')' )
            nParans--;
    if ( nParans != 0 )
    {
        sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parentheses ()." );
        return NULL;
    }
 
    // add parentheses
    pTemp = pFormula + strlen(pFormula) + 2;
    *pTemp-- = 0; *pTemp = ')';
    while ( --pTemp != pFormula )
        *pTemp = *(pTemp - 1);
    *pTemp = '(';

    // perform parsing
    Flag = VER_PARSE_FLAG_START;
    for ( pTemp = pFormula; *pTemp; pTemp++ )
	{
		switch ( *pTemp )
	    {
		// skip all spaces, tabs, and end-of-lines
        case ' ':
        case '\t':
        case '\r':
        case '\n':
			continue;
/*
		// treat Constant 0 as a variable
		case VER_PARSE_SYM_CONST0:
		    Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) );  // Cudd_Ref( Hop_ManConst0(pMan) );
			if ( Flag == VER_PARSE_FLAG_VAR )
			{
				sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." );
				Flag = VER_PARSE_FLAG_ERROR; 
                break;
			}
            Flag = VER_PARSE_FLAG_VAR; 
            break;

		// the same for Constant 1
		case VER_PARSE_SYM_CONST1:
		    Vec_PtrPush( vStackFn, Hop_ManConst1(pMan) );  //  Cudd_Ref( Hop_ManConst1(pMan) );
			if ( Flag == VER_PARSE_FLAG_VAR )
			{
				sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." );
				Flag = VER_PARSE_FLAG_ERROR; 
                break;
			}
            Flag = VER_PARSE_FLAG_VAR; 
            break;
*/
		case VER_PARSE_SYM_NEGBEF1:
		case VER_PARSE_SYM_NEGBEF2:
			if ( Flag == VER_PARSE_FLAG_VAR )
			{// if NEGBEF follows a variable, AND is assumed
				sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." );
				Flag = VER_PARSE_FLAG_ERROR; 
                break;
			}
    		Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG );
			break;

        case VER_PARSE_SYM_AND:
        case VER_PARSE_SYM_OR:
        case VER_PARSE_SYM_XOR:
        case VER_PARSE_SYM_MUX1:
        case VER_PARSE_SYM_MUX2:
			if ( Flag != VER_PARSE_FLAG_VAR )
			{
				sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." );
				Flag = VER_PARSE_FLAG_ERROR; 
                break;
			}
			if ( *pTemp == VER_PARSE_SYM_AND )
				Vec_IntPush( vStackOp, VER_PARSE_OPER_AND );
			else if ( *pTemp == VER_PARSE_SYM_OR )
				Vec_IntPush( vStackOp, VER_PARSE_OPER_OR );
			else if ( *pTemp == VER_PARSE_SYM_XOR )
				Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR );
			else if ( *pTemp == VER_PARSE_SYM_MUX1 )
				Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
//			else if ( *pTemp == VER_PARSE_SYM_MUX2 )
//				Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
			Flag = VER_PARSE_FLAG_OPER; 
            break;

        case VER_PARSE_SYM_OPEN:
			if ( Flag == VER_PARSE_FLAG_VAR )
			{
				sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a parenthesis." );
				Flag = VER_PARSE_FLAG_ERROR; 
                break;
			}
			Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK );
			// after an opening bracket, it feels like starting over again
			Flag = VER_PARSE_FLAG_START; 
            break;

		case VER_PARSE_SYM_CLOSE:
			if ( Vec_IntSize( vStackOp ) )
            {
				while ( 1 )
			    {
				    if ( !Vec_IntSize( vStackOp ) )
					{
						sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening parenthesis\n" );
						Flag = VER_PARSE_FLAG_ERROR; 
                        break;
					}
					Oper = Vec_IntPop( vStackOp );
					if ( Oper == VER_PARSE_OPER_MARK )
						break;
                    // skip the second MUX operation
//                    if ( Oper == VER_PARSE_OPER_MUX2 )
//                    {
//					    Oper = Vec_IntPop( vStackOp );
//                        assert( Oper == VER_PARSE_OPER_MUX1 );
//                    }

                    // perform the given operation
                    if ( Ver_FormulaParserTopOper( (Hop_Man_t *)pMan, vStackFn, Oper ) == NULL )
	                {
		                sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
		                return NULL;
	                }
			    }
            }
		    else
			{
				sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening parenthesis\n" );
				Flag = VER_PARSE_FLAG_ERROR; 
                break;
			}
			if ( Flag != VER_PARSE_FLAG_ERROR )
			    Flag = VER_PARSE_FLAG_VAR; 
			break;


		default:
            // scan the next name
            v = Ver_FormulaParserFindVar( pTemp, vNames );
            if ( *pTemp == '\\' )
                pTemp++;
            pTemp += (int)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*v ) - 1;

			// assume operation AND, if vars follow one another
			if ( Flag == VER_PARSE_FLAG_VAR )
            {
		        sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." );
                return NULL;
            }
            bTemp = Hop_IthVar( (Hop_Man_t *)pMan, v );
			Vec_PtrPush( vStackFn, bTemp ); //  Cudd_Ref( bTemp );
            Flag = VER_PARSE_FLAG_VAR; 
            break;
	    }

		if ( Flag == VER_PARSE_FLAG_ERROR )
			break;      // error exit
		else if ( Flag == VER_PARSE_FLAG_START )
			continue;  //  go on parsing
		else if ( Flag == VER_PARSE_FLAG_VAR )
			while ( 1 )
			{  // check if there are negations in the OpStack     
				if ( !Vec_IntSize(vStackOp) )
					break;
                Oper = Vec_IntPop( vStackOp );
				if ( Oper != VER_PARSE_OPER_NEG )
                {
					Vec_IntPush( vStackOp, Oper );
					break;
                }
				else
				{
//      				Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) );
      				Vec_PtrPush( vStackFn, Hop_Not((Hop_Obj_t *)Vec_PtrPop(vStackFn)) );
				}
			}
		else // if ( Flag == VER_PARSE_FLAG_OPER )
			while ( 1 )
			{  // execute all the operations in the OpStack
			   // with precedence higher or equal than the last one
				Oper1 = Vec_IntPop( vStackOp ); // the last operation
				if ( !Vec_IntSize(vStackOp) ) 
				{  // if it is the only operation, push it back
					Vec_IntPush( vStackOp, Oper1 );
					break;
				}
				Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
				if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) )  
				{  // if Oper2 precedence is higher or equal, execute it
                    if ( Ver_FormulaParserTopOper( (Hop_Man_t *)pMan, vStackFn, Oper2 ) == NULL )
	                {
		                sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
		                return NULL;
	                }
					Vec_IntPush( vStackOp,  Oper1 );     // push the last operation back
				}
				else
				{  // if Oper2 precedence is lower, push them back and done
					Vec_IntPush( vStackOp, Oper2 );
					Vec_IntPush( vStackOp, Oper1 );
					break;
				}
			}
    }

	if ( Flag != VER_PARSE_FLAG_ERROR )
    {
		if ( Vec_PtrSize(vStackFn) )
	    {	
			bFunc = (Hop_Obj_t *)Vec_PtrPop(vStackFn);
			if ( !Vec_PtrSize(vStackFn) )
				if ( !Vec_IntSize(vStackOp) )
                {
//                    Cudd_Deref( bFunc );
					return bFunc;
                }
				else
					sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" );
			else
				sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" );
	    }
	    else
			sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" );
    }
//    Cudd_Ref( bFunc );
//    Cudd_RecursiveDeref( dd, bFunc );
	return NULL;
}

/**Function*************************************************************

  Synopsis    [Performs the operation on the top entries in the stack.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper )
{
    Hop_Obj_t * bArg0, * bArg1, * bArg2, * bFunc;
    // perform the given operation
    bArg2 = (Hop_Obj_t *)Vec_PtrPop( vStackFn );
    bArg1 = (Hop_Obj_t *)Vec_PtrPop( vStackFn );
	if ( Oper == VER_PARSE_OPER_AND )
		bFunc = Hop_And( pMan, bArg1, bArg2 );
	else if ( Oper == VER_PARSE_OPER_XOR )
		bFunc = Hop_Exor( pMan, bArg1, bArg2 );
	else if ( Oper == VER_PARSE_OPER_OR )
		bFunc = Hop_Or( pMan, bArg1, bArg2 );
	else if ( Oper == VER_PARSE_OPER_EQU )
		bFunc = Hop_Not( Hop_Exor( pMan, bArg1, bArg2 ) );
	else if ( Oper == VER_PARSE_OPER_MUX )
    {
        bArg0 = (Hop_Obj_t *)Vec_PtrPop( vStackFn );
//		bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 );  Cudd_Ref( bFunc );
		bFunc = Hop_Mux( pMan, bArg0, bArg1, bArg2 ); 
//        Cudd_RecursiveDeref( dd, bArg0 );
//        Cudd_Deref( bFunc );
    }
	else
		return NULL;
//    Cudd_Ref( bFunc );
//    Cudd_RecursiveDeref( dd, bArg1 );
//    Cudd_RecursiveDeref( dd, bArg2 );
	Vec_PtrPush( vStackFn,  bFunc );
    return bFunc;
}

/**Function*************************************************************

  Synopsis    [Returns the index of the new variable found.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
{
    char * pTemp, * pTemp2;
    int nLength, nLength2, i;
    // start the string
    pTemp = pString;
    // find the end of the string delimited by other characters
    if ( *pTemp == '\\' )
    {
        pString++;
        while ( *pTemp && *pTemp != ' ' )
            pTemp++;
    }
    else
    {
        while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' && 
                *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && 
                *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && 
                *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && 
                *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 )
                pTemp++;
    }
    // look for this string in the array
    nLength = pTemp - pString;
    for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
    {
        nLength2 = (int)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*i + 0 );
        if ( nLength2 != nLength )
            continue;
        pTemp2   = (char *)Vec_PtrEntry( vNames, 2*i + 1 );
        if ( strncmp( pString, pTemp2, nLength ) )
            continue;
        return i;
    }
    // could not find - add and return the number
    Vec_PtrPush( vNames, (void *)(ABC_PTRUINT_T)nLength );
    Vec_PtrPush( vNames, pString );
    return i;
}

/**Function*************************************************************

  Synopsis    [Returns the AIG representation of the reduction formula.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage )
{
    Hop_Obj_t * pRes = NULL;
    int v, fCompl;
    char Symbol;

    // get the operation
    Symbol = *pFormula++;
    fCompl = ( Symbol == '~' );
    if ( fCompl )
        Symbol = *pFormula++;
    // check the operation
    if ( Symbol != '&' && Symbol != '|' && Symbol != '^' )
    {
		sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol );
		return NULL;
    }
    // skip the brace
    while ( *pFormula++ != '{' );
    // parse the names
    Vec_PtrClear( vNames );
    while ( *pFormula != '}' )
    {
        v = Ver_FormulaParserFindVar( pFormula, vNames );
        pFormula += (int)(ABC_PTRUINT_T)Vec_PtrEntry( vNames, 2*v );
        while ( *pFormula == ' ' || *pFormula == ',' )
            pFormula++;
    }
    // compute the function
    if ( Symbol == '&' )
        pRes = Hop_CreateAnd( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
    else if ( Symbol == '|' )
        pRes = Hop_CreateOr( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
    else if ( Symbol == '^' )
        pRes = Hop_CreateExor( (Hop_Man_t *)pMan, Vec_PtrSize(vNames)/2 );
    return Hop_NotCond( pRes, fCompl );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END