literal.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include "bool/kit/kit.h"
#include "misc/vec/vec.h"
#include "misc/util/abc_global.h"

Go to the source code of this file.

Data Structures
struct	Literal_t_

Typedefs
typedef struct Literal_t_	Literal_t

Enumerations
enum	Operator_t { LIT_NONE = 0, LIT_AND, LIT_OR, LIT_XOR }
	INCLUDES ///. More...

Functions
static void	Lit_TruthPositiveTransition (unsigned *pIn, unsigned *pOut, int nVars, int varIdx)
	FUNCTION DEFINITIONS ///. More...
static void	Lit_TruthNegativeTransition (unsigned *pIn, unsigned *pOut, int nVars, int varIdx)
static Literal_t *	Lit_Alloc (unsigned *pTruth, int nVars, int varIdx, char pol)
static Literal_t *	Lit_GroupLiterals (Literal_t *lit1, Literal_t *lit2, Operator_t op, int nVars)
static Literal_t *	Lit_CreateLiteralConst (unsigned *pTruth, int nVars, int constant)
static Literal_t *	Lit_Copy (Literal_t *lit, int nVars)
static void	Lit_PrintTT (unsigned *tt, int nVars)
static void	Lit_PrintExp (Literal_t *lit)
static void	Lit_Free (Literal_t *lit)

Typedef Documentation

typedef struct Literal_t_ Literal_t

Definition at line 50 of file literal.h.

Enumeration Type Documentation

enum Operator_t

INCLUDES ///.

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

]PARAMETERS ///

Enumerator
LIT_NONE
LIT_AND
LIT_OR
LIT_XOR

Definition at line 42 of file literal.h.

             {
    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;

Function Documentation

static Literal_t* Lit_Alloc ( unsigned *  pTruth, int  nVars, int  varIdx, char  pol  )

inlinestatic

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 []

Definition at line 131 of file literal.h.

                                                                                      {
    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;
    }
}

static Literal_t* Lit_Copy ( Literal_t *  lit, int  nVars  )

inlinestatic

Definition at line 249 of file literal.h.

                                                             {
    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 Literal_t* Lit_CreateLiteralConst ( unsigned *  pTruth, int  nVars, int  constant  )

inlinestatic

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

Synopsis [Create a const literal ]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file literal.h.

                                                                                           {
    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 void Lit_Free ( Literal_t *  lit )

inlinestatic

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

Synopsis [Delete the literal ]

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file literal.h.

                                             {
    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);
}

static Literal_t* Lit_GroupLiterals ( Literal_t *  lit1, Literal_t *  lit2, Operator_t  op, int  nVars  )

inlinestatic

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

Synopsis [Group 2 literals using AND or OR]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file literal.h.

                                                                                                       {
    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;
}

static void Lit_PrintExp ( Literal_t *  lit )

inlinestatic

Definition at line 267 of file literal.h.

                                                {
    Abc_Print(-2, "%s", lit->expression->pArray);
}

static void Lit_PrintTT ( unsigned *  tt, int  nVars  )

inlinestatic

Definition at line 260 of file literal.h.

                                                        {
    int w;
    for(w=nVars-1; w>=0; w--) {
            Abc_Print(-2, "%08X", tt[w]);
    }
}

static void Lit_TruthNegativeTransition ( unsigned *  pIn, unsigned *  pOut, int  nVars, int  varIdx  )

inlinestatic

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 []

Definition at line 103 of file literal.h.

{
    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);
}

static void Lit_TruthPositiveTransition ( unsigned *  pIn, unsigned *  pOut, int  nVars, int  varIdx  )

inlinestatic

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 []

Definition at line 75 of file literal.h.

{
    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);
}