/**CFile**************************************************************** FileName [literal.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [RPO] Synopsis [Literal structure] Author [Mayler G. A. Martins / Vinicius Callegaro] Affiliation [UFRGS] Date [Ver. 1.0. Started - May 08, 2013.] Revision [$Id: literal.h,v 1.00 2013/05/08 00:00:00 mgamartins Exp $] ***********************************************************************/ #ifndef ABC__bool__rpo__literal_h #define ABC__bool__rpo__literal_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include #include #include "bool/kit/kit.h" #include "misc/vec/vec.h" #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// // associations typedef enum { LIT_NONE = 0, // 0: unknown LIT_AND, // 1: AND association LIT_OR, // 2: OR association LIT_XOR // 3: XOR association (not used yet) } Operator_t; typedef struct Literal_t_ Literal_t; struct Literal_t_ { unsigned * transition; unsigned * function; Vec_Str_t * expression; }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Compute the positive transition] Description [The inputs are a function, the number of variables and a variable index and the output is a function] SideEffects [Should this function be in kitTruth.c ?] SeeAlso [] // ***********************************************************************/ static inline void Lit_TruthPositiveTransition( unsigned * pIn, unsigned * pOut, int nVars, int varIdx ) { unsigned * cof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); unsigned * cof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); unsigned * ncof0; Kit_TruthCofactor0New(cof0, pIn,nVars,varIdx); Kit_TruthCofactor1New(cof1, pIn,nVars,varIdx); ncof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); Kit_TruthNot(ncof0,cof0,nVars); Kit_TruthAnd(pOut,ncof0,cof1, nVars); ABC_FREE(cof0); ABC_FREE(ncof0); ABC_FREE(cof1); } /**Function************************************************************* Synopsis [Compute the negative transition] Description [The inputs are a function, the number of variables and a variable index and the output is a function] SideEffects [Should this function be in kitTruth.c ?] SeeAlso [] ***********************************************************************/ static inline void Lit_TruthNegativeTransition( unsigned * pIn, unsigned * pOut, int nVars, int varIdx ) { unsigned * cof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); unsigned * cof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); unsigned * ncof1; Kit_TruthCofactor0New(cof0, pIn,nVars,varIdx); Kit_TruthCofactor1New(cof1, pIn,nVars,varIdx); ncof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) ); Kit_TruthNot(ncof1,cof1,nVars); Kit_TruthAnd(pOut,ncof1,cof0,nVars); ABC_FREE(cof0); ABC_FREE(cof1); ABC_FREE(ncof1); } /**Function************************************************************* Synopsis [Create a literal given a polarity ] Description [The inputs are the function, index and its polarity and a the output is a literal] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Literal_t* Lit_Alloc(unsigned* pTruth, int nVars, int varIdx, char pol) { unsigned * transition; unsigned * function; Vec_Str_t * exp; Literal_t* lit; assert(pol == '+' || pol == '-'); transition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); if (pol == '+') { Lit_TruthPositiveTransition(pTruth, transition, nVars, varIdx); } else { Lit_TruthNegativeTransition(pTruth, transition, nVars, varIdx); } if (!Kit_TruthIsConst0(transition,nVars)) { function = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); Kit_TruthIthVar(function, nVars, varIdx); //Abc_Print(-2, "Allocating function %X %d %c \n", *function, varIdx, pol); exp = Vec_StrAlloc(5); if (pol == '-') { Kit_TruthNot(function, function, nVars); Vec_StrPutC(exp, '!'); } Vec_StrPutC(exp, (char)('a' + varIdx)); Vec_StrPutC(exp, '\0'); lit = ABC_ALLOC(Literal_t, 1); lit->function = function; lit->transition = transition; lit->expression = exp; return lit; } else { ABC_FREE(transition); // free the function. return NULL; } } /**Function************************************************************* Synopsis [Group 2 literals using AND or OR] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Literal_t* Lit_GroupLiterals(Literal_t* lit1, Literal_t* lit2, Operator_t op, int nVars) { unsigned * newFunction = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); unsigned * newTransition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); Vec_Str_t * newExp = Vec_StrAlloc(lit1->expression->nSize + lit2->expression->nSize + 3); Literal_t* newLiteral; char opChar = '%'; switch (op) { case LIT_AND: { //Abc_Print(-2, "Grouping AND %X %X \n", *lit1->function, *lit2->function); Kit_TruthAnd(newFunction, lit1->function, lit2->function, nVars); opChar = '*'; break; } case LIT_OR: { //Abc_Print(-2, "Grouping OR %X %X \n", *lit1->function, *lit2->function); Kit_TruthOr(newFunction, lit1->function, lit2->function, nVars); opChar = '+'; break; } default: { Abc_Print(-2, "Lit_GroupLiterals with op not defined."); //TODO Call ABC Abort } } Kit_TruthOr(newTransition, lit1->transition, lit2->transition, nVars); // create a new expression. Vec_StrPutC(newExp, '('); Vec_StrAppend(newExp, lit1->expression->pArray); //Vec_StrPop(newExp); // pop the \0 Vec_StrPutC(newExp, opChar); Vec_StrAppend(newExp, lit2->expression->pArray); //Vec_StrPop(newExp); // pop the \0 Vec_StrPutC(newExp, ')'); Vec_StrPutC(newExp, '\0'); newLiteral = ABC_ALLOC(Literal_t, 1); newLiteral->function = newFunction; newLiteral->transition = newTransition; newLiteral->expression = newExp; return newLiteral; } /**Function************************************************************* Synopsis [Create a const literal ] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Literal_t* Lit_CreateLiteralConst(unsigned* pTruth, int nVars, int constant) { Vec_Str_t * exp = Vec_StrAlloc(3); Literal_t* lit; Vec_StrPutC(exp, (char)('0' + constant)); Vec_StrPutC(exp, '\0'); lit = ABC_ALLOC(Literal_t, 1); lit->expression = exp; lit->function = pTruth; lit->transition = pTruth; // wrong but no effect ### return lit; } static inline Literal_t* Lit_Copy(Literal_t* lit, int nVars) { Literal_t* newLit = ABC_ALLOC(Literal_t,1); newLit->function = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); Kit_TruthCopy(newLit->function,lit->function,nVars); newLit->transition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); Kit_TruthCopy(newLit->transition,lit->transition,nVars); newLit->expression = Vec_StrDup(lit->expression); // Abc_Print(-2,"Copying: %s\n",newLit->expression->pArray); return newLit; } static inline void Lit_PrintTT(unsigned* tt, int nVars) { int w; for(w=nVars-1; w>=0; w--) { Abc_Print(-2, "%08X", tt[w]); } } static inline void Lit_PrintExp(Literal_t* lit) { Abc_Print(-2, "%s", lit->expression->pArray); } /**Function************************************************************* Synopsis [Delete the literal ] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline void Lit_Free(Literal_t * lit) { if(lit == NULL) { return; } // Abc_Print(-2,"Freeing: %s\n",lit->expression->pArray); ABC_FREE(lit->function); ABC_FREE(lit->transition); Vec_StrFree(lit->expression); ABC_FREE(lit); } ABC_NAMESPACE_HEADER_END #endif /* LITERAL_H */