#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

Data Structures
struct	Mini_Aig_t_

Macros
#define	MINI_AIG_NULL (0x7FFFFFFF)
	INCLUDES ///. More...

#define	MINI_AIG_START_SIZE (0x000000FF)

#define	MINI_AIG_ALLOC(type, num) ((type ) malloc(sizeof(type) (num)))
	MACRO DEFINITIONS ///. More...

#define	MINI_AIG_CALLOC(type, num) ((type *) calloc((num), sizeof(type)))

#define	MINI_AIG_FALLOC(type, num) ((type ) memset(malloc(sizeof(type) (num)), 0xff, sizeof(type) * (num)))

#define	MINI_AIG_FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)

#define	MINI_AIG_REALLOC(type, obj, num)

#define	Mini_AigForEachPi(p, i) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPi(p, i) ) {} else

#define	Mini_AigForEachPo(p, i) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPo(p, i) ) {} else

#define	Mini_AigForEachAnd(p, i) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsAnd(p, i) ) {} else

Typedefs
typedef struct Mini_Aig_t_	Mini_Aig_t
	BASIC TYPES ///. More...

Functions
static void	Mini_AigGrow (Mini_Aig_t *p, int nCapMin)

static void	Mini_AigPush (Mini_Aig_t *p, int Lit0, int Lit1)

static int	Mini_AigNodeFanin0 (Mini_Aig_t *p, int Id)

static int	Mini_AigNodeFanin1 (Mini_Aig_t *p, int Id)

static int	Mini_AigVar2Lit (int Var, int fCompl)

static int	Mini_AigLit2Var (int Lit)

static int	Mini_AigLitIsCompl (int Lit)

static int	Mini_AigLitNot (int Lit)

static int	Mini_AigLitNotCond (int Lit, int c)

static int	Mini_AigLitRegular (int Lit)

static int	Mini_AigLitConst0 ()

static int	Mini_AigLitConst1 ()

static int	Mini_AigLitIsConst0 (int Lit)

static int	Mini_AigLitIsConst1 (int Lit)

static int	Mini_AigLitIsConst (int Lit)

static int	Mini_AigNodeNum (Mini_Aig_t *p)

static int	Mini_AigNodeIsConst (Mini_Aig_t *p, int Id)

static int	Mini_AigNodeIsPi (Mini_Aig_t *p, int Id)

static int	Mini_AigNodeIsPo (Mini_Aig_t *p, int Id)

static int	Mini_AigNodeIsAnd (Mini_Aig_t *p, int Id)

static int	Mini_AigRegNum (Mini_Aig_t *p)

static void	Mini_AigSetRegNum (Mini_Aig_t *p, int n)

static Mini_Aig_t *	Mini_AigStart ()

static void	Mini_AigStop (Mini_Aig_t *p)

static void	Mini_AigPrintStats (Mini_Aig_t *p)

static void	Mini_AigDump (Mini_Aig_t p, char pFileName)

static Mini_Aig_t *	Mini_AigLoad (char *pFileName)

static int	Mini_AigCreatePi (Mini_Aig_t *p)

static int	Mini_AigCreatePo (Mini_Aig_t *p, int Lit0)

static int	Mini_AigAnd (Mini_Aig_t *p, int Lit0, int Lit1)

static int	Mini_AigOr (Mini_Aig_t *p, int Lit0, int Lit1)

static int	Mini_AigMux (Mini_Aig_t *p, int LitC, int Lit1, int Lit0)

static int	Mini_AigXor (Mini_Aig_t *p, int Lit0, int Lit1)

static int	Mini_AigCheck (Mini_Aig_t *p)

Macro Definition Documentation

#define MINI_AIG_ALLOC	(	type,
		num
	)	((type ) malloc(sizeof(type) (num)))

MACRO DEFINITIONS ///.

Definition at line 58 of file miniaig.h.

#define MINI_AIG_CALLOC	(	type,
		num
	)	((type *) calloc((num), sizeof(type)))

Definition at line 59 of file miniaig.h.

#define MINI_AIG_FALLOC	(	type,
		num
	)	((type ) memset(malloc(sizeof(type) (num)), 0xff, sizeof(type) * (num)))

Definition at line 60 of file miniaig.h.

#define MINI_AIG_FREE ( obj ) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)

Definition at line 61 of file miniaig.h.

#define MINI_AIG_NULL (0x7FFFFFFF)

INCLUDES ///.

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

FileName [miniaig.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic AIG package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 29, 2012.]

Revision [

Id:: miniaig.h,v 1.00 2012/09/29 00:00:00 alanmi Exp

]PARAMETERS ///

Definition at line 37 of file miniaig.h.

#define MINI_AIG_REALLOC	(	type,
		obj,
		num
	)

Value:

((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \

((type *) malloc(sizeof(type) * (num))))

malloc

char * malloc()

realloc

char * realloc()

Definition at line 62 of file miniaig.h.

#define MINI_AIG_START_SIZE (0x000000FF)

Definition at line 38 of file miniaig.h.

#define Mini_AigForEachAnd	(	p,
		i
	)	for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsAnd(p, i) ) {} else

Definition at line 127 of file miniaig.h.

#define Mini_AigForEachPi	(	p,
		i
	)	for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPi(p, i) ) {} else

Definition at line 125 of file miniaig.h.

#define Mini_AigForEachPo	(	p,
		i
	)	for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPo(p, i) ) {} else

Definition at line 126 of file miniaig.h.

Typedef Documentation

typedef struct Mini_Aig_t_ Mini_Aig_t

BASIC TYPES ///.

Definition at line 44 of file miniaig.h.

Function Documentation

static int Mini_AigAnd	(	Mini_Aig_t *	p,
		int	Lit0,
		int	Lit1
	)

static

Definition at line 215 of file miniaig.h.

 {
     int Lit = p->nSize;
     assert( Lit0 >= 0 && Lit0 < Lit );
     assert( Lit1 >= 0 && Lit1 < Lit );
     Mini_AigPush( p, Lit0, Lit1 );
     return Lit;
 }

static int Mini_AigCheck ( Mini_Aig_t * p )

static

Definition at line 239 of file miniaig.h.

 {
     int status = 1;
     int i, iFaninLit0, iFaninLit1;
     Mini_AigForEachAnd( p, i )
     {
         // get the fanin literals of this AND node
         iFaninLit0 = Mini_AigNodeFanin0( p, i );
         iFaninLit1 = Mini_AigNodeFanin1( p, i );
         // compare the fanin literals with the literal of the current node (2 * i)
         if ( iFaninLit0 >= 2 * i )
             printf( "Fanin0 of AND node %d is not in a topological order.\n", i ), status = 0;
         if ( iFaninLit1 >= 2 * i )
             printf( "Fanin0 of AND node %d is not in a topological order.\n", i ), status = 0;
     }
     Mini_AigForEachPo( p, i )
     {
         // get the fanin literal of this PO node
         iFaninLit0 = Mini_AigNodeFanin0( p, i );
         // compare the fanin literal with the literal of the current node (2 * i)
         if ( iFaninLit0 >= 2 * i )
             printf( "Fanin0 of PO node %d is not in a topological order.\n", i ), status = 0;
     }
     return status;
 }

static int Mini_AigCreatePi ( Mini_Aig_t * p )

static

Definition at line 200 of file miniaig.h.

 {
     int Lit = p->nSize;
     Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
     return Lit;
 }

static int Mini_AigCreatePo	(	Mini_Aig_t *	p,
		int	Lit0
	)

static

Definition at line 206 of file miniaig.h.

 {
     int Lit = p->nSize;
     assert( Lit0 >= 0 && Lit0 < Lit );
     Mini_AigPush( p, Lit0, MINI_AIG_NULL );
     return Lit;
 }

static void Mini_AigDump	(	Mini_Aig_t *	p,
		char *	pFileName
	)

static

Definition at line 161 of file miniaig.h.

 {
     FILE * pFile;
     int RetValue;
     pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
     {
         printf( "Cannot open file for writing \"%s\".\n", pFileName );
         return;
     }
     RetValue = fwrite( &p->nSize, sizeof(int), 1, pFile );
     RetValue = fwrite( &p->nRegs, sizeof(int), 1, pFile );
     RetValue = fwrite( p->pArray, sizeof(int), p->nSize, pFile );
     fclose( pFile );
 }

static void Mini_AigGrow	(	Mini_Aig_t *	p,
		int	nCapMin
	)

static

Definition at line 67 of file miniaig.h.

 {
     if ( p->nCap >= nCapMin )
         return;
     p->pArray = MINI_AIG_REALLOC( int, p->pArray, nCapMin ); 
     assert( p->pArray );
     p->nCap   = nCapMin;
 }

static int Mini_AigLit2Var ( int Lit )

static

Definition at line 102 of file miniaig.h.

102 { return Lit >> 1; }

static int Mini_AigLitConst0 ( )

static

Definition at line 108 of file miniaig.h.

108 { return 0; }

static int Mini_AigLitConst1 ( )

static

Definition at line 109 of file miniaig.h.

109 { return 1; }

static int Mini_AigLitIsCompl ( int Lit )

static

Definition at line 103 of file miniaig.h.

103 { return Lit & 1; }

static int Mini_AigLitIsConst ( int Lit )

static

Definition at line 112 of file miniaig.h.

112 { return Lit == 0 || Lit == 1; }

static int Mini_AigLitIsConst0 ( int Lit )

static

Definition at line 110 of file miniaig.h.

110 { return Lit == 0; }

static int Mini_AigLitIsConst1 ( int Lit )

static

Definition at line 111 of file miniaig.h.

111 { return Lit == 1; }

static int Mini_AigLitNot ( int Lit )

static

Definition at line 104 of file miniaig.h.

104 { return Lit ^ 1; }

static int Mini_AigLitNotCond	(	int	Lit,
		int	c
	)

static

Definition at line 105 of file miniaig.h.

105 { return Lit ^ (int)(c > 0); }

static int Mini_AigLitRegular ( int Lit )

static

Definition at line 106 of file miniaig.h.

106 { return Lit & ~01; }

static Mini_Aig_t* Mini_AigLoad ( char * pFileName )

static

Definition at line 176 of file miniaig.h.

 {
     Mini_Aig_t * p;
     FILE * pFile;
     int RetValue, nSize;
     pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
     {
         printf( "Cannot open file for reading \"%s\".\n", pFileName );
         return NULL;
     }
     RetValue = fread( &nSize, sizeof(int), 1, pFile );
     p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
     p->nSize = p->nCap = nSize;
     p->pArray = MINI_AIG_ALLOC( int, p->nCap );
     RetValue = fread( &p->nRegs, sizeof(int), 1, pFile );
     RetValue = fread( p->pArray, sizeof(int), p->nSize, pFile );
     fclose( pFile );
     return p;
 }

static int Mini_AigMux	(	Mini_Aig_t *	p,
		int	LitC,
		int	Lit1,
		int	Lit0
	)

static

Definition at line 227 of file miniaig.h.

 {
     int Res0 = Mini_AigAnd( p, LitC, Lit1 );
     int Res1 = Mini_AigAnd( p, Mini_AigLitNot(LitC), Lit0 );
     return Mini_AigOr( p, Res0, Res1 );
 }

static int Mini_AigNodeFanin0	(	Mini_Aig_t *	p,
		int	Id
	)

static

Definition at line 89 of file miniaig.h.

 {
     assert( Id >= 0 && 2*Id < p->nSize );
     return p->pArray[2*Id];
 }

static int Mini_AigNodeFanin1	(	Mini_Aig_t *	p,
		int	Id
	)

static

Definition at line 94 of file miniaig.h.

 {
     assert( Id >= 0 && 2*Id < p->nSize );
     return p->pArray[2*Id+1];
 }

static int Mini_AigNodeIsAnd	(	Mini_Aig_t *	p,
		int	Id
	)

static

Definition at line 118 of file miniaig.h.

118 { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) != MINI_AIG_NULL; }

Mini_AigNodeFanin0

static int Mini_AigNodeFanin0(Mini_Aig_t *p, int Id)

Definition: miniaig.h:89

Mini_AigNodeFanin1

static int Mini_AigNodeFanin1(Mini_Aig_t *p, int Id)

Definition: miniaig.h:94

assert

#define assert(ex)

Definition: util_old.h:213

MINI_AIG_NULL

#define MINI_AIG_NULL

INCLUDES ///.

Definition: miniaig.h:37

static int Mini_AigNodeIsConst	(	Mini_Aig_t *	p,
		int	Id
	)

static

Definition at line 115 of file miniaig.h.

115 { assert( Id >= 0 ); return Id == 0; }

assert

#define assert(ex)

Definition: util_old.h:213

static int Mini_AigNodeIsPi	(	Mini_Aig_t *	p,
		int	Id
	)

static

Definition at line 116 of file miniaig.h.

116 { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) == MINI_AIG_NULL; }

Mini_AigNodeFanin0

static int Mini_AigNodeFanin0(Mini_Aig_t *p, int Id)

Definition: miniaig.h:89

assert

#define assert(ex)

Definition: util_old.h:213

MINI_AIG_NULL

#define MINI_AIG_NULL

INCLUDES ///.

Definition: miniaig.h:37

static int Mini_AigNodeIsPo	(	Mini_Aig_t *	p,
		int	Id
	)

static

Definition at line 117 of file miniaig.h.

117 { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) == MINI_AIG_NULL; }

Mini_AigNodeFanin0

static int Mini_AigNodeFanin0(Mini_Aig_t *p, int Id)

Definition: miniaig.h:89

Mini_AigNodeFanin1

static int Mini_AigNodeFanin1(Mini_Aig_t *p, int Id)

Definition: miniaig.h:94

assert

#define assert(ex)

Definition: util_old.h:213

MINI_AIG_NULL

#define MINI_AIG_NULL

INCLUDES ///.

Definition: miniaig.h:37

static int Mini_AigNodeNum ( Mini_Aig_t * p )

static

Definition at line 114 of file miniaig.h.

114 { return p->nSize/2; }

Mini_Aig_t_::nSize

int nSize

Definition: miniaig.h:48

static int Mini_AigOr	(	Mini_Aig_t *	p,
		int	Lit0,
		int	Lit1
	)

static

Definition at line 223 of file miniaig.h.

 {
     return Mini_AigLitNot( Mini_AigAnd( p, Mini_AigLitNot(Lit0), Mini_AigLitNot(Lit1) ) );
 }

static void Mini_AigPrintStats ( Mini_Aig_t * p )

static

Definition at line 145 of file miniaig.h.

 {
     int i, nPis, nPos, nNodes;
     nPis = 0;
     Mini_AigForEachPi( p, i )
         nPis++;
     nPos = 0;
     Mini_AigForEachPo( p, i )
         nPos++;
     nNodes = 0;
     Mini_AigForEachAnd( p, i )
         nNodes++;
     printf( "PI = %d. PO = %d. Node = %d.\n", nPis, nPos, nNodes );
 }

static void Mini_AigPush	(	Mini_Aig_t *	p,
		int	Lit0,
		int	Lit1
	)

static

Definition at line 75 of file miniaig.h.

 {
     if ( p->nSize + 2 > p->nCap )
     {
         if ( p->nCap < MINI_AIG_START_SIZE )
             Mini_AigGrow( p, MINI_AIG_START_SIZE );
         else
             Mini_AigGrow( p, 2 * p->nCap );
     }
     p->pArray[p->nSize++] = Lit0;
     p->pArray[p->nSize++] = Lit1;
 }

static int Mini_AigRegNum ( Mini_Aig_t * p )

static

Definition at line 121 of file miniaig.h.

121 { return p->nRegs; }

Mini_Aig_t_::nRegs

int nRegs

Definition: miniaig.h:49

static void Mini_AigSetRegNum	(	Mini_Aig_t *	p,
		int	n
	)

static

Definition at line 122 of file miniaig.h.

122 { p->nRegs = n; }

Mini_Aig_t_::nRegs

int nRegs

Definition: miniaig.h:49

static Mini_Aig_t* Mini_AigStart ( )

static

Definition at line 131 of file miniaig.h.

 {
     Mini_Aig_t * p;
     p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
     p->nCap   = MINI_AIG_START_SIZE;
     p->pArray = MINI_AIG_ALLOC( int, p->nCap );
     Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
     return p;
 }

static void Mini_AigStop ( Mini_Aig_t * p )

static

Definition at line 140 of file miniaig.h.

 {
     MINI_AIG_FREE( p->pArray );
     MINI_AIG_FREE( p );
 }

static int Mini_AigVar2Lit	(	int	Var,
		int	fCompl
	)

static

Definition at line 101 of file miniaig.h.

101 { return Var + Var + fCompl; }

Minisat::Var

int Var

Definition: SolverTypes.h:42

static int Mini_AigXor	(	Mini_Aig_t *	p,
		int	Lit0,
		int	Lit1
	)

static

Definition at line 233 of file miniaig.h.

 {
     return Mini_AigMux( p, Lit0, Mini_AigLitNot(Lit1), Lit1 );
 }

Data Structures

Macros

Typedefs

Functions

Macro Definition Documentation

Typedef Documentation

Function Documentation