/**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 <stdio.h>
#include <stdlib.h>
#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 */