Major restructuring of the code.

This commit is contained in:
Alan Mishchenko 2012-01-21 04:30:10 -08:00
parent c44cc5de94
commit 8014f25f6d
898 changed files with 4589 additions and 32360 deletions

View File

@ -8,41 +8,35 @@ PROG := abc
MODULES := \
$(wildcard src/ext) src/misc/ext \
src/base/abc src/base/abci src/base/cmd \
src/base/io src/base/main src/base/ver src/base/test \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
src/bdd/parse src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio src/map/super \
src/map/if src/map/amap src/map/cov \
src/misc/extra src/misc/mvc src/misc/st src/misc/util \
src/misc/nm src/misc/vec src/misc/hash \
src/misc/bzlib src/misc/zlib \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/mfs \
src/opt/sim src/opt/ret src/opt/res src/opt/lpk \
src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
src/sat/psat src/sat/pdr \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk \
src/aig/mfx src/aig/tim src/aig/saig src/aig/bbr \
src/aig/int src/aig/dch src/aig/ssw src/aig/cgt \
src/aig/cec src/aig/gia src/aig/bbl src/aig/live \
src/aig/llb \
src/base/abc src/base/abci src/base/cmd src/base/io \
src/base/main src/base/ver src/base/test \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse \
src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
src/map/amap src/map/cov \
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \
src/misc/mem src/misc/bar src/misc/bbl \
src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
src/opt/cgt src/opt/csw src/opt/dar \
src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit \
src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \
src/python
all: $(PROG)
default: $(PROG)
# Please note that to compile on 32-bit Linux the following optflags are required:
# -DLIN -DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4
arch_flags : arch_flags.c
gcc arch_flags.c -o arch_flags
#OPTFLAGS := -DNDEBUG -O3 -DLIN
#OPTFLAGS := -DNDEBUG -O3 -DLIN64
#OPTFLAGS := -g -O -DLIN -m32
OPTFLAGS := -g -O -DLIN64 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -DSIZEOF_INT=4 -DABC_NAMESPACE=xxx
ARCHFLAGS := $(shell gcc arch_flags.c -o arch_flags && ./arch_flags)
OPTFLAGS := -g -O #-DABC_NAMESPACE=xxx
CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES))
CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(ARCHFLAGS) -I$(PWD)
CXXFLAGS += $(CFLAGS)
#LIBS := -m32 -ldl -rdynamic -lreadline -ltermcap

View File

@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "src/ext/ext" /I "src/misc/ext" /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/cov" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "C:/_projects/abc_niklas/" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src/ext/ext" /I "src/misc/ext" /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/cov" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /I "src/sat/lsat" /I "src/aig/cec" /I "src/aig/cgt" /I "src/aig/sec" /I "src/map/amap" /I "src/aig/fsim" /I "src/aig/gia" /I "src/aig/bbl" /I "src/aig/llb" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "C:/_projects/abc_niklas/" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
BSC32=bscmake.exe

1958
abclib.dsp

File diff suppressed because it is too large Load Diff

17
arch_flags.c Normal file
View File

@ -0,0 +1,17 @@
#include <stdio.h>
int main()
{
if (sizeof(void*) == 8) // Assume 64-bit Linux if pointers are 8 bytes.
printf("-DLIN64 ");
else
printf("-DLIN ");
printf("-DSIZEOF_VOID_P=%d -DSIZEOF_LONG=%d -DSIZEOF_INT=%d\n",
(int)sizeof(void*),
(int)sizeof(long),
(int)sizeof(int) );
return 0;
}

View File

@ -18,8 +18,8 @@
***********************************************************************/
#ifndef __AIG_H__
#define __AIG_H__
#ifndef ABC__aig__aig__aig_h
#define ABC__aig__aig__aig_h
////////////////////////////////////////////////////////////////////////
@ -32,8 +32,8 @@
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "utilCex.h"
#include "src/misc/vec/vec.h"
#include "src/misc/util/utilCex.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -222,20 +222,6 @@ static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Aig_IntAbs( int n ) { return (n < 0)? -n : n; }
//static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); }
//static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Aig_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; }
static inline float Aig_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; }
static inline int Aig_Base2Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Aig_Base10Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
static inline char * Aig_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Aig_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Aig_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline int Aig_WordCountOnes( unsigned uWord )
{
@ -254,13 +240,6 @@ static inline int Aig_WordFindFirstBit( unsigned uWord )
return -1;
}
static inline int Aig_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Aig_Lit2Var( int Lit ) { return Lit >> 1; }
static inline int Aig_LitIsCompl( int Lit ) { return Lit & 1; }
static inline int Aig_LitNot( int Lit ) { return Lit ^ 1; }
static inline int Aig_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
static inline int Aig_LitRegular( int Lit ) { return Lit & ~01; }
static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
@ -335,10 +314,10 @@ static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { assert( !Aig
static inline Aig_Obj_t * Aig_ObjCopy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return (Aig_Obj_t *)pObj->pData; }
static inline void Aig_ObjSetCopy( Aig_Obj_t * pObj, Aig_Obj_t * pCopy ) { assert( !Aig_IsComplement(pObj) ); pObj->pData = pCopy; }
static inline Aig_Obj_t * Aig_ObjRealCopy( Aig_Obj_t * pObj ) { return Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj));}
static inline int Aig_ObjToLit( Aig_Obj_t * pObj ) { return Aig_Var2Lit( Aig_ObjId(Aig_Regular(pObj)), Aig_IsComplement(pObj) ); }
static inline Aig_Obj_t * Aig_ObjFromLit( Aig_Man_t * p,int iLit){ return Aig_NotCond( Aig_ManObj(p, Aig_Lit2Var(iLit)), Aig_LitIsCompl(iLit) ); }
static inline int Aig_ObjToLit( Aig_Obj_t * pObj ) { return Abc_Var2Lit( Aig_ObjId(Aig_Regular(pObj)), Aig_IsComplement(pObj) ); }
static inline Aig_Obj_t * Aig_ObjFromLit( Aig_Man_t * p,int iLit){ return Aig_NotCond( Aig_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); }
static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level; }
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + ABC_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + Abc_MaxInt(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
static inline int Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i; }
static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); }
@ -653,7 +632,6 @@ extern unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves,
/*=== aigTsim.c ========================================================*/
extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
/*=== aigUtil.c =========================================================*/
extern unsigned Aig_PrimeCudd( unsigned p );
extern void Aig_ManIncrementTravId( Aig_Man_t * p );
extern char * Aig_TimeStamp();
extern int Aig_ManHasNoGaps( Aig_Man_t * p );

View File

@ -19,9 +19,9 @@
***********************************************************************/
#include "aig.h"
#include "kit.h"
#include "bdc.h"
#include "ioa.h"
#include "src/bool/kit/kit.h"
#include "src/bool/bdc/bdc.h"
#include "src/aig/ioa/ioa.h"
ABC_NAMESPACE_IMPL_START
@ -106,7 +106,7 @@ Aig_RMan_t * Aig_RManStart()
p->pAig = Aig_ManStart( 1000000 );
Aig_IthVar( p->pAig, p->nVars-1 );
// create hash table
p->nBins = Aig_PrimeCudd(5000);
p->nBins = Abc_PrimeCudd(5000);
p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
p->pMemTrus = Aig_MmFlexStart();
// bi-decomposition manager
@ -182,7 +182,7 @@ clk = clock();
pBinsOld = p->pBins;
nBinsOld = p->nBins;
// get the new Bins
p->nBins = Aig_PrimeCudd( 3 * nBinsOld );
p->nBins = Abc_PrimeCudd( 3 * nBinsOld );
p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
// rehash the entries from the old table
Counter = 0;
@ -628,7 +628,7 @@ void Aig_RManRecord( unsigned * pTruth, int nVarsInit )
else
s_pRMan->nTtDsdNot++;
// compute the number of words
nWords = Aig_TruthWordNum( nVars );
nWords = Abc_TruthWordNum( nVars );
// copy the function
memcpy( s_pRMan->pTruthInit, Kit_DsdObjTruth(pObj), 4*nWords );
Kit_DsdNtkFree( pNtk );

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "aig.h"
#include "kit.h"
#include "src/bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
@ -58,7 +58,7 @@ Aig_ManCut_t * Aig_ManCutStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, in
p->pAig = pMan;
p->pCuts = ABC_CALLOC( Aig_Cut_t *, Aig_ManObjNumMax(pMan) );
// allocate memory manager
p->nTruthWords = Aig_TruthWordNum(nLeafMax);
p->nTruthWords = Abc_TruthWordNum(nLeafMax);
p->nCutSize = sizeof(Aig_Cut_t) + sizeof(int) * nLeafMax + fTruth * sizeof(unsigned) * p->nTruthWords;
p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
// room for temporary truth tables

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "aig.h"
#include "tim.h"
#include "src/misc/tim/tim.h"
ABC_NAMESPACE_IMPL_START
@ -477,7 +477,7 @@ int Aig_ManLevelNum( Aig_Man_t * p )
int i, LevelsMax;
LevelsMax = 0;
Aig_ManForEachPo( p, pObj, i )
LevelsMax = ABC_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
LevelsMax = Abc_MaxInt( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
return LevelsMax;
}

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "aig.h"
#include "saig.h"
#include "src/aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START

View File

@ -18,8 +18,8 @@
***********************************************************************/
#include "saig.h"
#include "tim.h"
#include "src/aig/saig/saig.h"
#include "src/misc/tim/tim.h"
ABC_NAMESPACE_IMPL_START
@ -52,8 +52,8 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -124,7 +124,7 @@ Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints )
assert( p->nAsserts == 0 || p->nConstrs == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@ -203,8 +203,8 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -303,8 +303,8 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
int i, nNodes;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -379,8 +379,8 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -456,8 +456,8 @@ Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p )
int i, nNodes;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
// create the PIs
Aig_ManCleanData( p );
@ -505,8 +505,8 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->fCatchExor = 1;
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -608,8 +608,8 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
int i, nNodes;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -749,8 +749,8 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
int i, nNodes;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -821,8 +821,8 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
int i, k;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
@ -895,8 +895,8 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@ -980,8 +980,8 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
int i;
// start the HOP package
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@ -1054,8 +1054,8 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
int i;
// start the HOP package
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@ -1163,8 +1163,8 @@ Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs )
}
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@ -1212,8 +1212,8 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs )
assert( iPoNum < Aig_ManPoNum(p)-Aig_ManRegNum(p) );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@ -1263,8 +1263,8 @@ Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
}
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@ -1321,7 +1321,7 @@ Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray )
}
// create the new manager
pNew = Aig_ManStart( 10000 );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Aig_ManForEachPi( p, pObj, i )
Aig_ObjCreatePi(pNew);
// create the PIs

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "aig.h"
#include "kit.h"
#include "src/bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
@ -289,7 +289,7 @@ Vec_Ptr_t * Aig_SuppMinPerform( Aig_Man_t * p, Vec_Ptr_t * vOrGate, Vec_Ptr_t *
Aig_Obj_t * pObj;
Vec_Ptr_t * vTrSupp, * vTrNode, * vCofs;
unsigned * uFunc, * uCare, * uFunc0, * uFunc1, * uCof;
int i, nWords = Aig_TruthWordNum( Vec_PtrSize(vSupp) );
int i, nWords = Abc_TruthWordNum( Vec_PtrSize(vSupp) );
// assign support nodes
vTrSupp = Vec_PtrAllocTruthTables( Vec_PtrSize(vSupp) );
Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )

View File

@ -112,7 +112,7 @@ void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
assert( pFanout->Id > 0 );
if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc )
{
int nFansAlloc = 2 * ABC_MAX( pObj->Id, pFanout->Id );
int nFansAlloc = 2 * Abc_MaxInt( pObj->Id, pFanout->Id );
p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;

View File

@ -61,8 +61,8 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs );
pFrames->pName = Aig_UtilStrsav( pAig->pName );
pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
// map constant nodes
for ( f = 0; f < nFs; f++ )
Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );

View File

@ -19,8 +19,8 @@
***********************************************************************/
#include "aig.h"
#include "cnf.h"
#include "satStore.h"
#include "src/sat/cnf/cnf.h"
#include "src/sat/bsat/satStore.h"
ABC_NAMESPACE_IMPL_START

View File

@ -114,7 +114,7 @@ int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Ve
// if ( Aig_ObjId(pNode) % 1000 == 0 )
// Value ^= 1;
if ( vSuppLits )
Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
return 1;
}
assert( Aig_ObjIsNode(pNode) );
@ -221,8 +221,8 @@ int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLi
Aig_ManIncrementTravId( pAig );
Vec_IntForEachEntry( vSuppLits, Entry, i )
{
pObj = Aig_ManPi( pAig, Aig_Lit2Var(Entry) );
Aig_ObjSetTerValue( pObj, Aig_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
pObj = Aig_ManPi( pAig, Abc_Lit2Var(Entry) );
Aig_ObjSetTerValue( pObj, Abc_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
Aig_ObjSetTravIdCurrent( pAig, pObj );
//printf( "%d ", Entry );
}

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "aig.h"
#include "tim.h"
#include "src/misc/tim/tim.h"
ABC_NAMESPACE_IMPL_START
@ -68,7 +68,7 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
p->pConst1->fPhase = 1;
p->nObjs[AIG_OBJ_CONST1]++;
// start the table
p->nTableSize = Aig_PrimeCudd( nNodesMax );
p->nTableSize = Abc_PrimeCudd( nNodesMax );
p->pTable = ABC_ALLOC( Aig_Obj_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
return p;
@ -92,8 +92,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
@ -149,8 +149,8 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t *
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);

View File

@ -269,7 +269,7 @@ int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
// dereference the current cut
LevelMax = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
LevelMax = ABC_MAX( LevelMax, (int)pObj->Level );
LevelMax = Abc_MaxInt( LevelMax, (int)pObj->Level );
if ( LevelMax == 0 )
return 0;
// dereference the cut

View File

@ -122,11 +122,11 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
// create the power counter
if ( p->vProbs )
{
float Prob0 = Aig_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId0(pObj) ) );
float Prob1 = Aig_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId1(pObj) ) );
float Prob0 = Abc_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId0(pObj) ) );
float Prob1 = Abc_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId1(pObj) ) );
Prob0 = Aig_ObjFaninC0(pObj)? 1.0 - Prob0 : Prob0;
Prob1 = Aig_ObjFaninC1(pObj)? 1.0 - Prob1 : Prob1;
Vec_IntSetEntry( p->vProbs, pObj->Id, Aig_Float2Int(Prob0 * Prob1) );
Vec_IntSetEntry( p->vProbs, pObj->Id, Abc_Float2Int(Prob0 * Prob1) );
}
return pObj;
}
@ -563,7 +563,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
{
Vec_PtrPush( p->vBufs, pObjOld );
p->nBufMax = ABC_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
p->nBufMax = Abc_MaxInt( p->nBufMax, Vec_PtrSize(p->vBufs) );
Aig_ManPropagateBuffers( p, fUpdateLevel );
}
}

View File

@ -295,19 +295,19 @@ int Aig_ManPackAddPatternTry( Aig_ManPack_t * p, int iBit, Vec_Int_t * vLits )
int i, Lit;
Vec_IntForEachEntry( vLits, Lit, i )
{
pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
if ( Aig_InfoHasBit( (unsigned *)pPres, iBit ) &&
Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) )
pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
if ( Abc_InfoHasBit( (unsigned *)pPres, iBit ) &&
Abc_InfoHasBit( (unsigned *)pInfo, iBit ) == Abc_LitIsCompl(Lit) )
return 0;
}
Vec_IntForEachEntry( vLits, Lit, i )
{
pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
Aig_InfoSetBit( (unsigned *)pPres, iBit );
if ( Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) )
Aig_InfoXorBit( (unsigned *)pInfo, iBit );
pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
Abc_InfoSetBit( (unsigned *)pPres, iBit );
if ( Abc_InfoHasBit( (unsigned *)pInfo, iBit ) == Abc_LitIsCompl(Lit) )
Abc_InfoXorBit( (unsigned *)pInfo, iBit );
}
return 1;
}
@ -335,16 +335,16 @@ void Aig_ManPackAddPattern( Aig_ManPack_t * p, Vec_Int_t * vLits )
word * pInfo, * pPres;
int i, Lit;
Vec_IntForEachEntry( vLits, Lit, i )
printf( "%d", Aig_LitIsCompl(Lit) );
printf( "%d", Abc_LitIsCompl(Lit) );
printf( "\n\n" );
for ( k = 1; k < 64; k++ )
{
Vec_IntForEachEntry( vLits, Lit, i )
{
pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
if ( Aig_InfoHasBit( (unsigned *)pPres, k ) )
printf( "%d", Aig_InfoHasBit( (unsigned *)pInfo, k ) );
pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
if ( Abc_InfoHasBit( (unsigned *)pPres, k ) )
printf( "%d", Abc_InfoHasBit( (unsigned *)pInfo, k ) );
else
printf( "-" );
}

View File

@ -19,8 +19,8 @@
***********************************************************************/
#include "aig.h"
#include "tim.h"
#include "fra.h"
#include "src/misc/tim/tim.h"
#include "src/proof/fra/fra.h"
ABC_NAMESPACE_IMPL_START
@ -471,13 +471,13 @@ unsigned * Aig_ManSuppCharStart( Vec_Int_t * vOne, int nPis )
{
unsigned * pBuffer;
int i, Entry;
int nWords = Aig_BitWordNum(nPis);
int nWords = Abc_BitWordNum(nPis);
pBuffer = ABC_ALLOC( unsigned, nWords );
memset( pBuffer, 0, sizeof(unsigned) * nWords );
Vec_IntForEachEntry( vOne, Entry, i )
{
assert( Entry < nPis );
Aig_InfoSetBit( pBuffer, Entry );
Abc_InfoSetBit( pBuffer, Entry );
}
return pBuffer;
}
@ -499,7 +499,7 @@ void Aig_ManSuppCharAdd( unsigned * pBuffer, Vec_Int_t * vOne, int nPis )
Vec_IntForEachEntry( vOne, Entry, i )
{
assert( Entry < nPis );
Aig_InfoSetBit( pBuffer, Entry );
Abc_InfoSetBit( pBuffer, Entry );
}
}
@ -518,7 +518,7 @@ int Aig_ManSuppCharCommon( unsigned * pBuffer, Vec_Int_t * vOne )
{
int i, Entry, nCommon = 0;
Vec_IntForEachEntry( vOne, Entry, i )
nCommon += Aig_InfoHasBit(pBuffer, Entry);
nCommon += Abc_InfoHasBit(pBuffer, Entry);
return nCommon;
}
@ -558,7 +558,7 @@ int Aig_ManPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
if ( Vec_IntSize(vPartSupp) < 100 )
Repulse = 1;
else
Repulse = 1+Aig_Base2Log(Vec_IntSize(vPartSupp)-100);
Repulse = 1+Abc_Base2Log(Vec_IntSize(vPartSupp)-100);
Value = Attract/Repulse;
if ( ValueBest < Value )
{

View File

@ -19,8 +19,8 @@
***********************************************************************/
#include "aig.h"
#include "satSolver.h"
#include "cnf.h"
#include "src/sat/bsat/satSolver.h"
#include "src/sat/cnf/cnf.h"
ABC_NAMESPACE_IMPL_START

View File

@ -19,8 +19,8 @@
***********************************************************************/
#include "aig.h"
#include "cnf.h"
#include "satSolver2.h"
#include "src/sat/cnf/cnf.h"
#include "src/sat/bsat/satSolver2.h"
ABC_NAMESPACE_IMPL_START
@ -313,7 +313,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
// start the interpolant
pBase = Aig_ManStart( 1000 );
pBase->pName = Aig_UtilStrsav( "repar" );
pBase->pName = Abc_UtilStrsav( "repar" );
for ( k = 0; k < 2*nOuts; k++ )
Aig_IthVar(pBase, i);
@ -338,7 +338,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
Sat_Solver2PrintStats( stdout, pSat );
// derive interpolant
pInter = Sat_ProofInterpolant( pSat, vVars );
pInter = (Aig_Man_t *)Sat_ProofInterpolant( pSat, vVars );
Aig_ManPrintStats( pInter );
// make sure interpolant does not depend on useless vars
Aig_ManForEachPi( pInter, pObj, i )

View File

@ -271,8 +271,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
int i;
// start the HOP package
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );

View File

@ -176,7 +176,7 @@ void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
assert( pEdge->nLats == 10 );
if ( p->nExtraCur + 1 > p->nExtraAlloc )
{
int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
int nExtraAllocNew = Abc_MaxInt( 2 * p->nExtraAlloc, 1024 );
p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
p->nExtraAlloc = nExtraAllocNew;
}
@ -202,7 +202,7 @@ void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
nWords = (pEdge->nLats + 1) >> 4;
if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc )
{
int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
int nExtraAllocNew = Abc_MaxInt( 2 * p->nExtraAlloc, 1024 );
p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
p->nExtraAlloc = nExtraAllocNew;
}
@ -360,7 +360,7 @@ int Rtm_ManLatchMax( Rtm_Man_t * p )
assert( Val == 1 || Val == 2 );
}
*/
nLatchMax = ABC_MAX( nLatchMax, (int)pEdge->nLats );
nLatchMax = Abc_MaxInt( nLatchMax, (int)pEdge->nLats );
}
return nLatchMax;
}
@ -477,7 +477,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
Rtm_Obj_t * pFanin;
int i, Degree = 0;
Rtm_ObjForEachFanin( pObj, pFanin, i )
Degree = ABC_MAX( Degree, (int)pFanin->Num );
Degree = Abc_MaxInt( Degree, (int)pFanin->Num );
return Degree + 1;
}
@ -497,7 +497,7 @@ int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj )
Rtm_Obj_t * pFanout;
int i, Degree = 0;
Rtm_ObjForEachFanout( pObj, pFanout, i )
Degree = ABC_MAX( Degree, (int)pFanout->Num );
Degree = Abc_MaxInt( Degree, (int)pFanout->Num );
return Degree + 1;
}
@ -910,7 +910,7 @@ clk = clock();
if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable
continue;
Degree = Rtm_ObjGetDegreeFwd( pNext );
DegreeMax = ABC_MAX( DegreeMax, Degree );
DegreeMax = Abc_MaxInt( DegreeMax, Degree );
if ( Degree > nStepsMax ) // skip nodes with high degree
continue;
pNext->fMark = 1;
@ -931,7 +931,7 @@ clk = clock();
if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable
continue;
Degree = Rtm_ObjGetDegreeBwd( pNext );
DegreeMax = ABC_MAX( DegreeMax, Degree );
DegreeMax = Abc_MaxInt( DegreeMax, Degree );
if ( Degree > nStepsMax ) // skip nodes with high degree
continue;
pNext->fMark = 1;
@ -952,8 +952,8 @@ clk = clock();
// get the new manager
pNew = Rtm_ManToAig( pRtm );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Rtm_ManFree( pRtm );
// group the registers
clk = clock();

View File

@ -50,8 +50,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
int i, nTruePis;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );

View File

@ -19,9 +19,8 @@
***********************************************************************/
#include "aig.h"
#include "saig.h"
#include "cuddInt.h"
#include "extra.h"
#include "src/aig/saig/saig.h"
#include "src/misc/extra/extraBdd.h"
ABC_NAMESPACE_IMPL_START
@ -84,7 +83,7 @@ Aig_Man_t * Aig_ManConvertBddsToAigs( Aig_Man_t * p, DdManager * dd, Vec_Ptr_t *
Aig_ManCleanData( p );
// generate AIG for BDD
pNew = Aig_ManStart( Aig_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );

View File

@ -77,7 +77,7 @@ clk = clock();
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
// get the new table
p->nTableSize = Aig_PrimeCudd( 2 * Aig_ManNodeNum(p) );
p->nTableSize = Abc_PrimeCudd( 2 * Aig_ManNodeNum(p) );
p->pTable = ABC_ALLOC( Aig_Obj_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
// rehash the entries from the old table

View File

@ -121,7 +121,7 @@ int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
{
LevelCur = Aig_ObjReverseLevel( p, pFanout );
Level = ABC_MAX( Level, LevelCur );
Level = Abc_MaxInt( Level, LevelCur );
}
return Level + 1;
}

View File

@ -88,7 +88,7 @@ unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t *
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
pObj->pData = Vec_PtrEntry( vTruthElem, i );
// compute truths for other nodes
nWords = Aig_TruthWordNum( Vec_PtrSize(vLeaves) );
nWords = Abc_TruthWordNum( Vec_PtrSize(vLeaves) );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
pObj->pData = Aig_ManCutTruthOne( pObj, (unsigned *)Vec_PtrEntry(vTruthStore, i), nWords );
return (unsigned *)pRoot->pData;

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "aig.h"
#include "saig.h"
#include "src/aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
@ -133,10 +133,10 @@ Aig_Tsi_t * Aig_TsiStart( Aig_Man_t * pAig )
p = ABC_ALLOC( Aig_Tsi_t, 1 );
memset( p, 0, sizeof(Aig_Tsi_t) );
p->pAig = pAig;
p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
p->nWords = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) );
p->vStates = Vec_PtrAlloc( 1000 );
p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
p->nBins = Aig_PrimeCudd(TSI_MAX_ROUNDS/2);
p->nBins = Abc_PrimeCudd(TSI_MAX_ROUNDS/2);
p->pBins = ABC_ALLOC( unsigned *, p->nBins );
memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
return p;
@ -274,7 +274,7 @@ void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
if ( Value == 1 )
printf( "0" ), nZeros++;
else if ( Value == 2 )
@ -304,7 +304,7 @@ int Aig_TsiStateCount( Aig_Tsi_t * p, unsigned * pState )
int i, Value, nCounter = 0;
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
nCounter += (Value == 1 || Value == 2);
}
return nCounter;
@ -369,9 +369,9 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose, int fVeryVerbos
{
Value = Aig_ObjGetXsim(pObjLo);
if ( Value & 1 )
Aig_InfoSetBit( pState, 2 * i );
Abc_InfoSetBit( pState, 2 * i );
if ( Value & 2 )
Aig_InfoSetBit( pState, 2 * i + 1 );
Abc_InfoSetBit( pState, 2 * i + 1 );
}
// printf( "%d ", Aig_TsiStateCount(pTsi, pState) );
@ -446,7 +446,7 @@ Aig_TsiStatePrint( pTsi, pState );
for ( i = 0; i < pTsi->nWords - 1; i++ )
if ( pState[i] != ~0 )
fConstants = 1;
if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
if ( pState[i] != Abc_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
fConstants = 1;
}
if ( fConstants == 0 )
@ -465,7 +465,7 @@ Aig_TsiStatePrint( pTsi, pState );
nCounter = 0;
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
nCounter += (Value == 1 || Value == 2);
if ( Value == 1 )
Vec_PtrPush( vMap, Aig_ManConst0(p) );

View File

@ -30,42 +30,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function********************************************************************
Synopsis [Returns the next prime >= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Aig_PrimeCudd( unsigned int p )
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
/**Function*************************************************************
Synopsis [Increments the current traversal ID of the network.]
@ -140,7 +104,7 @@ int Aig_ManLevels( Aig_Man_t * p )
Aig_Obj_t * pObj;
int i, LevelMax = 0;
Aig_ManForEachPo( p, pObj, i )
LevelMax = ABC_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
LevelMax = Abc_MaxInt( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
return LevelMax;
}
@ -791,7 +755,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec
pObj->iData = Counter++;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
pObj->iData = Counter++;
nDigits = Aig_Base10Log( Counter );
nDigits = Abc_Base10Log( Counter );
// write the file
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
@ -906,7 +870,7 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
pObj->iData = Counter++;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
pObj->iData = Counter++;
nDigits = Aig_Base10Log( Counter );
nDigits = Abc_Base10Log( Counter );
// write the file
pFile = fopen( pFileName, "w" );
fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog()\n" );
@ -1299,7 +1263,7 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, ABC_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
Vec_PtrGrow( vArr, Abc_MaxInt( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
@ -1324,8 +1288,8 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
ABC_NAMESPACE_IMPL_END
#include "fra.h"
#include "saig.h"
#include "src/proof/fra/fra.h"
#include "src/aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
@ -1353,45 +1317,45 @@ void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex )
assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs
assert( pAig->pData2 == NULL ); // if this fail, there may be a memory leak
// allocate memory to store simulation bits for internal nodes
pAig->pData2 = ABC_CALLOC( unsigned, Aig_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNum(pAig) ) );
pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNum(pAig) ) );
// the register values in the counter-example should be zero
Saig_ManForEachLo( pAig, pObj, k )
assert( Aig_InfoHasBit(pCex->pData, iBit++) == 0 );
assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
// iterate through the timeframes
nObjs = Aig_ManObjNum(pAig);
for ( i = 0; i <= pCex->iFrame; i++ )
{
// set constant 1 node
Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
// set primary inputs according to the counter-example
Saig_ManForEachPi( pAig, pObj, k )
if ( Aig_InfoHasBit(pCex->pData, iBit++) )
Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
if ( Abc_InfoHasBit(pCex->pData, iBit++) )
Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
// compute values for each node
Aig_ManForEachNode( pAig, pObj, k )
{
Val0 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
Val1 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
Val1 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
}
// derive values for combinational outputs
Aig_ManForEachPo( pAig, pObj, k )
{
Val0 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
if ( Val0 ^ Aig_ObjFaninC0(pObj) )
Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
}
if ( i == pCex->iFrame )
continue;
// transfer values to the register output of the next frame
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
if ( Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
if ( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
}
assert( iBit == pCex->nBits );
// check that the counter-example is correct, that is, the corresponding output is asserted
assert( Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
assert( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
}
/**Function*************************************************************
@ -1428,7 +1392,7 @@ void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig )
int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame )
{
assert( Id >= 0 && Id < Aig_ManObjNum(pAig) );
return Aig_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
return Abc_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
}
/**Function*************************************************************
@ -1445,7 +1409,7 @@ int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame )
void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNum(pAig)/2 );
int iFrame = ABC_MAX( 0, pCex->iFrame - 1 );
int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
Aig_ManCounterExampleValueStart( pAig, pCex );
printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame,

View File

@ -1 +0,0 @@
SRC += src/aig/bar/bar.c

View File

@ -1 +0,0 @@
SRC += src/aig/bbl/bblif.c

View File

@ -1,4 +0,0 @@
SRC += src/aig/bbr/bbrCex.c \
src/aig/bbr/bbrImage.c \
src/aig/bbr/bbrNtbdd.c \
src/aig/bbr/bbrReach.c

View File

@ -1,5 +0,0 @@
SRC += src/aig/bdc/bdcCore.c \
src/aig/bdc/bdcDec.c \
src/aig/bdc/bdcSpfd.c \
src/aig/bdc/bdcTable.c

View File

@ -1,13 +0,0 @@
SRC += src/aig/cec/cecCec.c \
src/aig/cec/cecChoice.c \
src/aig/cec/cecClass.c \
src/aig/cec/cecCore.c \
src/aig/cec/cecCorr.c \
src/aig/cec/cecIso.c \
src/aig/cec/cecMan.c \
src/aig/cec/cecPat.c \
src/aig/cec/cecSeq.c \
src/aig/cec/cecSim.c \
src/aig/cec/cecSolve.c \
src/aig/cec/cecSynth.c \
src/aig/cec/cecSweep.c

View File

@ -1,5 +0,0 @@
SRC += src/aig/cgt/cgtAig.c \
src/aig/cgt/cgtCore.c \
src/aig/cgt/cgtDecide.c \
src/aig/cgt/cgtMan.c \
src/aig/cgt/cgtSat.c

View File

@ -1,9 +0,0 @@
SRC += src/aig/cnf/cnfCore.c \
src/aig/cnf/cnfCut.c \
src/aig/cnf/cnfData.c \
src/aig/cnf/cnfFast.c \
src/aig/cnf/cnfMan.c \
src/aig/cnf/cnfMap.c \
src/aig/cnf/cnfPost.c \
src/aig/cnf/cnfUtil.c \
src/aig/cnf/cnfWrite.c

View File

@ -1,4 +0,0 @@
SRC += src/aig/csw/cswCore.c \
src/aig/csw/cswCut.c \
src/aig/csw/cswMan.c \
src/aig/csw/cswTable.c

View File

@ -1,10 +0,0 @@
SRC += src/aig/dar/darBalance.c \
src/aig/dar/darCore.c \
src/aig/dar/darCut.c \
src/aig/dar/darData.c \
src/aig/dar/darLib.c \
src/aig/dar/darMan.c \
src/aig/dar/darPrec.c \
src/aig/dar/darRefact.c \
src/aig/dar/darResub.c \
src/aig/dar/darScript.c

View File

@ -1,10 +0,0 @@
SRC += src/aig/dch/dchAig.c \
src/aig/dch/dchChoice.c \
src/aig/dch/dchClass.c \
src/aig/dch/dchCnf.c \
src/aig/dch/dchCore.c \
src/aig/dch/dchMan.c \
src/aig/dch/dchSat.c \
src/aig/dch/dchSim.c \
src/aig/dch/dchSimSat.c \
src/aig/dch/dchSweep.c

View File

@ -1,17 +0,0 @@
SRC += src/aig/fra/fraBmc.c \
src/aig/fra/fraCec.c \
src/aig/fra/fraClass.c \
src/aig/fra/fraClau.c \
src/aig/fra/fraClaus.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraHot.c \
src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraIndVer.c \
src/aig/fra/fraLcr.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraPart.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSec.c \
src/aig/fra/fraSim.c

View File

@ -1,6 +0,0 @@
SRC += src/aig/fsim/fsimCore.c \
src/aig/fsim/fsimFront.c \
src/aig/fsim/fsimMan.c \
src/aig/fsim/fsimSim.c \
src/aig/fsim/fsimSwitch.c \
src/aig/fsim/fsimTsim.c

View File

@ -18,8 +18,8 @@
***********************************************************************/
#ifndef __GIA_H__
#define __GIA_H__
#ifndef ABC__aig__gia__gia_h
#define ABC__aig__gia__gia_h
////////////////////////////////////////////////////////////////////////
@ -32,8 +32,8 @@
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "utilCex.h"
#include "src/misc/vec/vec.h"
#include "src/misc/util/utilCex.h"
#include "giaAbs.h"
////////////////////////////////////////////////////////////////////////
@ -210,19 +210,6 @@ struct Gia_ParVta_t_
int iFrame; // the number of frames covered
};
static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; }
static inline int Gia_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; }
static inline float Gia_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; }
static inline int Gia_Base2Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Gia_Base10Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
static inline int Gia_Base16Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 16, r++ ); return r; }
static inline char * Gia_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
static inline int Gia_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Gia_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Gia_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; }
static inline int Gia_WordHasOnePair( unsigned uWord ) { return Gia_WordHasOneBit(uWord & (uWord>>1) & 0x55555555); }
@ -246,7 +233,7 @@ static inline int Gia_WordFindFirstBit( unsigned uWord )
static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars )
{
int w;
for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn[w] )
return 0;
return 1;
@ -254,7 +241,7 @@ static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars )
static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars )
{
int w;
for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn[w] != ~(unsigned)0 )
return 0;
return 1;
@ -262,35 +249,28 @@ static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars )
static inline void Gia_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn[w];
}
static inline void Gia_ManTruthClear( unsigned * pOut, int nVars )
{
int w;
for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = 0;
}
static inline void Gia_ManTruthFill( unsigned * pOut, int nVars )
{
int w;
for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~(unsigned)0;
}
static inline void Gia_ManTruthNot( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~pIn[w];
}
static inline int Gia_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Gia_Lit2Var( int Lit ) { return Lit >> 1; }
static inline int Gia_LitIsCompl( int Lit ) { return Lit & 1; }
static inline int Gia_LitNot( int Lit ) { return Lit ^ 1; }
static inline int Gia_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
static inline int Gia_LitRegular( int Lit ) { return Lit & ~01; }
static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
@ -358,33 +338,33 @@ static inline int Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId ) {
static inline int Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff1; }
static inline int Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) ); }
static inline int Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) ); }
static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); }
static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); }
static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; }
static inline int Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); }
static inline Gia_Obj_t * Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Gia_Lit2Var(pObj->Value) ); }
static inline Gia_Obj_t * Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) ); }
static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); }
static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); }
static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; }
static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; }
static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); }
static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); }
static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); }
static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); }
static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) ); }
static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); }
static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); }
static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntGetEntry(p->vLevels, Gia_ObjId(p,pObj)); }
static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); }
static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Vec_IntSetEntry(p->vLevels, Gia_ObjId(p,pObj), l); }
static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); }
static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+ABC_MAX(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; }
static inline int Gia_ObjRefsId( Gia_Man_t * p, int Id ) { assert( p->pRefs); return p->pRefs[Id]; }
@ -457,17 +437,17 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
assert( iLit0 != iLit1 );
if ( iLit0 < iLit1 )
{
pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0);
pObj->fCompl0 = Gia_LitIsCompl(iLit0);
pObj->iDiff1 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1);
pObj->fCompl1 = Gia_LitIsCompl(iLit1);
pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
pObj->fCompl0 = Abc_LitIsCompl(iLit0);
pObj->iDiff1 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1);
pObj->fCompl1 = Abc_LitIsCompl(iLit1);
}
else
{
pObj->iDiff1 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0);
pObj->fCompl1 = Gia_LitIsCompl(iLit0);
pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1);
pObj->fCompl0 = Gia_LitIsCompl(iLit1);
pObj->iDiff1 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
pObj->fCompl1 = Abc_LitIsCompl(iLit0);
pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1);
pObj->fCompl0 = Abc_LitIsCompl(iLit1);
}
if ( p->pFanData )
{
@ -480,8 +460,8 @@ static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 )
{
Gia_Obj_t * pObj = Gia_ManAppendObj( p );
pObj->fTerm = 1;
pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0);
pObj->fCompl0 = Gia_LitIsCompl(iLit0);
pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
pObj->fCompl0 = Abc_LitIsCompl(iLit0);
pObj->iDiff1 = Vec_IntSize( p->vCos );
Vec_IntPush( p->vCos, Gia_ObjId(p, pObj) );
if ( p->pFanData )
@ -490,9 +470,9 @@ static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 )
}
static inline int Gia_ManAppendMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
{
int iTemp0 = Gia_ManAppendAnd( p, Gia_LitNot(iCtrl), iData0 );
int iTemp0 = Gia_ManAppendAnd( p, Abc_LitNot(iCtrl), iData0 );
int iTemp1 = Gia_ManAppendAnd( p, iCtrl, iData1 );
return Gia_LitNotCond( Gia_ManAppendAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 );
return Abc_LitNotCond( Gia_ManAppendAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
}
#define GIA_ZER 1
@ -587,7 +567,7 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
#define Gia_ManForEachObjVec( vVec, p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
#define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ )
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Abc_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Abc_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ )
#define Gia_ManForEachObjReverse( p, pObj, i ) \
for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
#define Gia_ManForEachAnd( p, pObj, i ) \
@ -817,7 +797,6 @@ extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
/*=== giaUtil.c ===========================================================*/
extern unsigned Gia_ManRandom( int fReset );
extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
extern unsigned int Gia_PrimeCudd( unsigned int p );
extern char * Gia_TimeStamp();
extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
extern void Gia_ManIncrementTravId( Gia_Man_t * p );

View File

@ -20,7 +20,7 @@
#include "gia.h"
#include "giaAig.h"
#include "saig.h"
#include "src/aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
@ -472,7 +472,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
// this obj was abstracted before
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) );
// if corresponding AIG object is not abstracted, remove abstraction
if ( !Vec_IntEntry(vGateClasses, Gia_Lit2Var(pObj->Value)) )
if ( !Vec_IntEntry(vGateClasses, Abc_Lit2Var(pObj->Value)) )
{
Vec_IntWriteEntry( pGia->vGateClasses, i, 0 );
Counter++;

View File

@ -18,8 +18,8 @@
***********************************************************************/
#ifndef __GIA_ABS_H__
#define __GIA_ABS_H__
#ifndef ABC__aig__gia__giaAbs_h
#define ABC__aig__gia__giaAbs_h
////////////////////////////////////////////////////////////////////////

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "satSolver2.h"
#include "src/sat/bsat/satSolver2.h"
ABC_NAMESPACE_IMPL_START
@ -210,7 +210,7 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 );
assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
// get the bitmask
nObjMask = (1 << Gia_Base2Log(nObjs)) - 1;
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
vPresent = Vec_IntStart( nObjs );
@ -248,7 +248,7 @@ static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords )
pTotal[w] |= pThis[i];
}
for ( i = nWords * 32 - 1; i >= 0; i-- )
if ( Gia_InfoHasBit(pTotal, i) )
if ( Abc_InfoHasBit(pTotal, i) )
{
ABC_FREE( pTotal );
return i+1;
@ -716,7 +716,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
if ( Gia_ObjIsRo(p->pGia, pObj) )
assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 );
else if ( Gia_ObjIsPi(p->pGia, pObj) && pThis->Value == VTA_VAR1 )
Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
}
}
// perform refinement
@ -776,7 +776,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->pBins = ABC_CALLOC( int, p->nBins );
p->vOrder = Vec_IntAlloc( 1013 );
// abstraction
p->nObjBits = Gia_Base2Log( Gia_ManObjNum(pGia) );
p->nObjBits = Abc_Base2Log( Gia_ManObjNum(pGia) );
p->nObjMask = (1 << p->nObjBits) - 1;
assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
p->nWords = 1;
@ -922,7 +922,8 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
***********************************************************************/
void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
{
unsigned * pInfo, * pCountAll, * pCountUni;
unsigned * pInfo;
int * pCountAll, * pCountUni;
int i, k, iFrame, iObj, Entry;
// print info about frames
pCountAll = ABC_CALLOC( int, nFrames + 1 );
@ -933,9 +934,9 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
iFrame = (Entry >> p->nObjBits);
assert( iFrame < nFrames );
pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
if ( Gia_InfoHasBit(pInfo, iFrame) == 0 )
if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
{
Gia_InfoSetBit( pInfo, iFrame );
Abc_InfoSetBit( pInfo, iFrame );
pCountUni[iFrame+1]++;
pCountUni[0]++;
}
@ -1062,7 +1063,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
assert( pThis != NULL && pThis->fAdded );
return Gia_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
}
/**Function*************************************************************
@ -1105,7 +1106,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
if ( f < p->pPars->nFramesStart )
{
// load this timeframe
Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 );
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
// run SAT solver
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status );
assert( (vCore != NULL) == (Status == 1) );
@ -1123,7 +1124,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
pObj = Gia_ManObj( p->pGia, pThis->iObj );
if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
}
}
}
@ -1133,7 +1134,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// load the time frame
int Limit = Abc_MinInt(5, p->pPars->nFramesStart);
for ( i = 1; i <= Limit; i++ )
Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i );
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
// iterate as long as there are counter-examples
do {
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status );

View File

@ -19,9 +19,9 @@
***********************************************************************/
#include "giaAig.h"
#include "fra.h"
#include "dch.h"
#include "dar.h"
#include "src/proof/fra/fra.h"
#include "src/proof/dch/dch.h"
#include "src/opt/dar/dar.h"
ABC_NAMESPACE_IMPL_START
@ -30,8 +30,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj ) { return Gia_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj ) { return Gia_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
static inline Aig_Obj_t * Gia_ObjChild0Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); }
static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); }
@ -64,8 +64,8 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
int iObjNew, iNextNew;
Gia_ManFromAig_rec( pNew, p, pNext );
iObjNew = Gia_Lit2Var(pObj->iData);
iNextNew = Gia_Lit2Var(pNext->iData);
iObjNew = Abc_Lit2Var(pObj->iData);
iNextNew = Abc_Lit2Var(pNext->iData);
if ( pNew->pNexts )
pNew->pNexts[iObjNew] = iNextNew;
}
@ -89,7 +89,7 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
int i;
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->nConstrs = p->nConstrs;
// create room to store equivalences
if ( p->pEquivs )
@ -128,7 +128,7 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
int i;
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->nConstrs = p->nConstrs;
// create the PIs
Aig_ManCleanData( p );
@ -167,7 +167,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
int i;
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->nConstrs = p->nConstrs;
// create the PIs
Aig_ManCleanData( p );
@ -246,9 +246,9 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
assert( !fChoices || (p->pNexts && p->pReprs) );
// create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->nConstrs = p->nConstrs;
// pNew->pSpec = Gia_UtilStrsav( p->pName );
// pNew->pSpec = Abc_UtilStrsav( p->pName );
// duplicate representation of choice nodes
if ( fChoices )
pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
@ -293,9 +293,9 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
// create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->nConstrs = p->nConstrs;
// pNew->pSpec = Gia_UtilStrsav( p->pName );
// pNew->pSpec = Abc_UtilStrsav( p->pName );
// create the PIs
ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
ppNodes[0] = Aig_ManConst0(pNew);
@ -334,7 +334,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
// create the new manager
pNew = Aig_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->nConstrs = p->nConstrs;
// create the PIs
Gia_ManForEachObj( p, pObj, i )
@ -349,7 +349,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
ppNodes[i] = Aig_ManConst0(pNew);
else
assert( 0 );
pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
}
Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
@ -402,8 +402,8 @@ void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
// move pointers from AIG to GIA
Aig_ManForEachObj( pAig, pObj, i )
{
assert( i == 0 || !Gia_LitIsCompl(pObj->iData) );
pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) );
assert( i == 0 || !Abc_LitIsCompl(pObj->iData) );
pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) );
pGiaObj->Value = i;
}
// set the pointers to the nodes in AIG
@ -441,7 +441,7 @@ void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
pGiaRepr = Gia_ObjReprObj( pGia, i );
if ( pGiaRepr == NULL )
continue;
Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Gia_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Gia_Lit2Var(pGiaObj->Value)) );
Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) );
}
}
@ -472,8 +472,8 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
// Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 );
if ( Gia_ObjIsCo(pObjGia) )
continue;
assert( i == 0 || !Gia_LitIsCompl(Gia_ObjValue(pObjGia)) );
pObjAig = Aig_ManObj( pAig, Gia_Lit2Var(Gia_ObjValue(pObjGia)) );
assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
pObjAig = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) );
pObjAig->iData = i;
}
Aig_ManForEachObj( pAig, pObjAig, i )

View File

@ -18,15 +18,15 @@
***********************************************************************/
#ifndef __GIA_AIG_H__
#define __GIA_AIG_H__
#ifndef ABC__aig__gia__giaAig_h
#define ABC__aig__gia__giaAig_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig.h"
#include "src/aig/aig/aig.h"
#include "gia.h"
ABC_NAMESPACE_HEADER_START

View File

@ -146,7 +146,7 @@ int Gia_FileSize( char * pFileName )
char * Gia_FileNameGeneric( char * FileName )
{
char * pDot, * pRes;
pRes = Gia_UtilStrsav( FileName );
pRes = Abc_UtilStrsav( FileName );
if ( (pDot = strrchr( pRes, '.' )) )
*pDot = 0;
return pRes;
@ -445,8 +445,8 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
pName = Gia_FileNameGeneric( pFileName );
pNew->pName = Gia_UtilStrsav( pName );
// pNew->pSpec = Gia_UtilStrsav( pFileName );
pNew->pName = Abc_UtilStrsav( pName );
// pNew->pSpec = Abc_UtilStrsav( pFileName );
ABC_FREE( pName );
pNew->nConstrs = nConstr;
@ -482,8 +482,8 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
uLit1 = uLit - Gia_ReadAigerDecode( &pCur );
uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur );
// assert( uLit1 > uLit0 );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
// Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
@ -500,14 +500,14 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
for ( i = 0; i < nLatches; i++ )
{
uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
// read the PO driver literals
for ( i = 0; i < nOutputs; i++ )
{
uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
@ -518,14 +518,14 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
for ( i = 0; i < nLatches; i++ )
{
uLit0 = Vec_IntEntry( vLits, i );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
// read the PO driver literals
for ( i = 0; i < nOutputs; i++ )
{
uLit0 = Vec_IntEntry( vLits, i+nLatches );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
Vec_IntFree( vLits );
@ -604,7 +604,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
pCur++;
// read model name
ABC_FREE( pNew->pName );
pNew->pName = Gia_UtilStrsav( (char *)pCur );
pNew->pName = Abc_UtilStrsav( (char *)pCur );
}
}
Vec_IntFree( vNodes );
@ -753,8 +753,8 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
uLit1 = uLit - Gia_ReadAigerDecode( &pCur );
uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur );
// assert( uLit1 > uLit0 );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
// Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
@ -772,14 +772,14 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
for ( i = 0; i < nLatches; i++ )
{
uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
// read the PO driver literals
for ( i = 0; i < nOutputs; i++ )
{
uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
@ -790,14 +790,14 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
for ( i = 0; i < nLatches; i++ )
{
uLit0 = Vec_IntEntry( vLits, i );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
// read the PO driver literals
for ( i = 0; i < nOutputs; i++ )
{
uLit0 = Vec_IntEntry( vLits, i+nLatches );
iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Vec_IntPush( vDrivers, iNode0 );
}
Vec_IntFree( vLits );
@ -877,7 +877,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
pCur++;
// read model name
ABC_FREE( pNew->pName );
pNew->pName = Gia_UtilStrsav( (char *)pCur );
pNew->pName = Abc_UtilStrsav( (char *)pCur );
}
}
@ -1094,7 +1094,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
{
ABC_FREE( pNew->pName );
pName = Gia_FileNameGeneric( pFileName );
pNew->pName = Gia_UtilStrsav( pName );
pNew->pName = Abc_UtilStrsav( pName );
// pNew->pSpec = Ioa_UtilStrsav( pFileName );
ABC_FREE( pName );
}
@ -1246,30 +1246,30 @@ unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize )
}
pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) );
// write constant class
iPos = Gia_WriteAigerEncode( pBuffer, 4, Gia_Var2Lit(0, 1) );
iPos = Gia_WriteAigerEncode( pBuffer, 4, Abc_Var2Lit(0, 1) );
//printf( "\nRepr = %d ", 0 );
iPrevNode = 0;
for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ )
if ( Gia_ObjIsConst(p, iNode) )
{
//printf( "Node = %d ", iNode );
iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
iPrevNode = iNode;
iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) );
iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
}
// write non-constant classes
iPrevRepr = 0;
Gia_ManForEachClass( p, iRepr )
{
//printf( "\nRepr = %d ", iRepr );
iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iRepr - iPrevRepr, 1) );
iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) );
iPrevRepr = iPrevNode = iRepr;
Gia_ClassForEachObj1( p, iRepr, iNode )
{
//printf( "Node = %d ", iNode );
iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
iPrevNode = iNode;
iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) );
iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
}
}
Gia_WriteInt( pBuffer, iPos );
@ -1291,8 +1291,8 @@ unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize )
int Gia_WriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis )
{
if ( iPrev < iThis )
return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iThis - iPrev, 1) );
return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iPrev - iThis, 0) );
return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) );
return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) );
}
/**Function*************************************************************
@ -1420,7 +1420,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
Gia_ManForEachAnd( p, pObj, i )
{
uLit = Gia_Var2Lit( i, 0 );
uLit = Abc_Var2Lit( i, 0 );
uLit0 = Gia_ObjFaninLit0( pObj, i );
uLit1 = Gia_ObjFaninLit1( pObj, i );
assert( uLit0 < uLit1 );

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "bdc.h"
#include "src/bool/bdc/bdc.h"
ABC_NAMESPACE_IMPL_START
@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj ) { return Gia_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); }
static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj ) { return Abc_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); }
static inline int Bdc_FunFanin0Copy( Bdc_Fun_t * pObj ) { return Bdc_FunObjCopy( Bdc_FuncFanin0(pObj) ); }
static inline int Bdc_FunFanin1Copy( Bdc_Fun_t * pObj ) { return Bdc_FunObjCopy( Bdc_FuncFanin1(pObj) ); }
@ -109,7 +109,7 @@ unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t
int i, nWords, nVars;
// get the number of variables and words
nVars = Vec_IntSize( vLeaves );
nWords = Gia_TruthWordNum( nVars );
nWords = Abc_TruthWordNum( nVars );
// check the case of a constant
if ( Gia_ObjIsConst0( Gia_Regular(pRoot) ) )
{
@ -263,7 +263,7 @@ Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose )
Gia_ManConst0(p)->Value = 0;
// start the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
// Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) );
pManDec = Bdc_ManAlloc( pPars );

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "satSolver.h"
#include "src/sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
@ -134,10 +134,10 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
}
static inline int Gia_Obj0Copy( Vec_Int_t * vCopies, int Fan0, int fCompl0 )
{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); }
{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); }
static inline int Gia_Obj1Copy( Vec_Int_t * vCopies, int Fan1, int fCompl1 )
{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); }
{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); }
/**Function*************************************************************
@ -173,7 +173,7 @@ void Gia_ManCofOneDerive_rec( Ccf_Man_t * p, int Id )
else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI
Res = sat_solver_var_value( p->pSat, Id );
else
Res = Gia_Var2Lit( Id, 0 );
Res = Abc_Var2Lit( Id, 0 );
Vec_IntWriteEntry( p->vCopies, Id, Res );
}
@ -193,15 +193,15 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
int LitOut;
// derive the cofactor of the property node
Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 );
Gia_ManCofOneDerive_rec( p, Gia_Lit2Var(LitProp) );
LitOut = Vec_IntEntry( p->vCopies, Gia_Lit2Var(LitProp) );
LitOut = Gia_LitNotCond( LitOut, Gia_LitIsCompl(LitProp) );
Gia_ManCofOneDerive_rec( p, Abc_Lit2Var(LitProp) );
LitOut = Vec_IntEntry( p->vCopies, Abc_Lit2Var(LitProp) );
LitOut = Abc_LitNotCond( LitOut, Abc_LitIsCompl(LitProp) );
// add new PO for the cofactor
Gia_ManAppendCo( p->pFrames, LitOut );
// add SAT clauses
Gia_ManCofExtendSolver( p );
// return negative literal of the cofactor
return Gia_LitNot(LitOut);
return Abc_LitNot(LitOut);
}
/**Function*************************************************************

View File

@ -238,8 +238,8 @@ static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex )
p->pProp.iHead = 0;
Cbs_QueForEachEntry( p->pProp, pVar, i )
if ( Gia_ObjIsCi(pVar) )
// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
}
/**Function*************************************************************
@ -377,7 +377,7 @@ static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj )
assert( Gia_ObjIsAnd(pObj) );
Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
return ABC_MAX( Count0, Count1 );
return Abc_MaxInt( Count0, Count1 );
}
/**Function*************************************************************
@ -504,7 +504,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi
Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
// s_Counter++;
// s_Counter = Abc_MaxInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
// s_Counter = Abc_MaxIntInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
}
@ -872,7 +872,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
if ( Cbs_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs_ManCheckLimits( p ) )
return 0;
// remember the state before branching
@ -946,7 +946,7 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
p->pJust.iHead = p->pJust.iTail = 0;
p->pClauses.iHead = p->pClauses.iTail = 1;
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs_ManCheckLimits( p ) )
RetValue = -1;

View File

@ -213,8 +213,8 @@ static inline void Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex )
p->pProp.iHead = 0;
Cbs0_QueForEachEntry( p->pProp, pVar, i )
if ( Gia_ObjIsCi(pVar) )
// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
}
/**Function*************************************************************
@ -332,7 +332,7 @@ static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
assert( Gia_ObjIsAnd(pObj) );
Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
return ABC_MAX( Count0, Count1 );
return Abc_MaxInt( Count0, Count1 );
}
/**Function*************************************************************
@ -596,7 +596,7 @@ int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
if ( Cbs0_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs0_ManCheckLimits( p ) )
return 0;
// remember the state before branching
@ -656,7 +656,7 @@ int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
Cbs0_ManCancelUntil( p, 0 );
p->pJust.iHead = p->pJust.iTail = 0;
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs0_ManCheckLimits( p ) )
RetValue = -1;
// printf( "Outcome = %2d. Confs = %6d. Decision level max = %3d.\n",

View File

@ -122,8 +122,8 @@ static inline void Tas_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fM
static inline int Tas_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); }
static inline int Tas_VarFanin0Value( Gia_Obj_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
static inline int Tas_VarFanin1Value( Gia_Obj_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
static inline int Tas_VarToLit( Tas_Man_t * p, Gia_Obj_t * pObj ) { assert( Tas_VarIsAssigned(pObj) ); return Gia_Var2Lit( Gia_ObjId(p->pAig, pObj), !Tas_VarValue(pObj) ); }
static inline int Tas_LitIsTrue( Gia_Obj_t * pObj, int Lit ) { assert( Tas_VarIsAssigned(pObj) ); return Tas_VarValue(pObj) != Gia_LitIsCompl(Lit); }
static inline int Tas_VarToLit( Tas_Man_t * p, Gia_Obj_t * pObj ) { assert( Tas_VarIsAssigned(pObj) ); return Abc_Var2Lit( Gia_ObjId(p->pAig, pObj), !Tas_VarValue(pObj) ); }
static inline int Tas_LitIsTrue( Gia_Obj_t * pObj, int Lit ) { assert( Tas_VarIsAssigned(pObj) ); return Tas_VarValue(pObj) != Abc_LitIsCompl(Lit); }
static inline int Tas_ClsHandle( Tas_Man_t * p, Tas_Cls_t * pClause ) { return ((int *)pClause) - p->pStore.pData; }
static inline Tas_Cls_t * Tas_ClsFromHandle( Tas_Man_t * p, int h ) { return (Tas_Cls_t *)(p->pStore.pData + h); }
@ -292,8 +292,8 @@ static inline void Tas_ManSaveModel( Tas_Man_t * p, Vec_Int_t * vCex )
Tas_QueForEachEntry( p->pProp, pVar, i )
{
if ( Gia_ObjIsCi(pVar) )
// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Tas_VarValue(pVar)) );
Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Tas_VarValue(pVar)) );
// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Tas_VarValue(pVar)) );
Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Tas_VarValue(pVar)) );
/*
printf( "%5d(%d) = ", Gia_ObjId(p->pAig, pVar), Tas_VarValue(pVar) );
if ( Gia_ObjIsCi(pVar) )
@ -443,7 +443,7 @@ static inline int Tas_VarFaninFanoutMax( Tas_Man_t * p, Gia_Obj_t * pObj )
assert( Gia_ObjIsAnd(pObj) );
Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
return ABC_MAX( Count0, Count1 );
return Abc_MaxInt( Count0, Count1 );
}
@ -793,11 +793,11 @@ static inline void Tas_ManDeriveReason( Tas_Man_t * p, int Level )
if ( Tas_VarHasReasonCls( p, pObj ) )
{
Tas_Cls_t * pCls = Tas_VarReasonCls( p, pObj );
pReason = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[0]) );
pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[0]) );
assert( pReason == pObj );
for ( j = 1; j < pCls->nLits; j++ )
{
pReason = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[j]) );
pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[j]) );
iLitLevel2 = Tas_VarDecLevel( p, pReason );
assert( Tas_VarIsAssigned( pReason ) );
assert( !Tas_LitIsTrue( pReason, pCls->pLits[j] ) );
@ -953,16 +953,16 @@ static inline Tas_Cls_t * Tas_ManAllocCls( Tas_Man_t * p, int nSize )
***********************************************************************/
static inline void Tas_ManWatchClause( Tas_Man_t * p, Tas_Cls_t * pClause, int Lit )
{
assert( Gia_Lit2Var(Lit) < Gia_ManObjNum(p->pAig) );
assert( Abc_Lit2Var(Lit) < Gia_ManObjNum(p->pAig) );
assert( pClause->nLits >= 2 );
assert( pClause->pLits[0] == Lit || pClause->pLits[1] == Lit );
if ( pClause->pLits[0] == Lit )
pClause->iNext[0] = p->pWatches[Gia_LitNot(Lit)];
pClause->iNext[0] = p->pWatches[Abc_LitNot(Lit)];
else
pClause->iNext[1] = p->pWatches[Gia_LitNot(Lit)];
if ( p->pWatches[Gia_LitNot(Lit)] == 0 )
Vec_IntPush( p->vWatchLits, Gia_LitNot(Lit) );
p->pWatches[Gia_LitNot(Lit)] = Tas_ClsHandle( p, pClause );
pClause->iNext[1] = p->pWatches[Abc_LitNot(Lit)];
if ( p->pWatches[Abc_LitNot(Lit)] == 0 )
Vec_IntPush( p->vWatchLits, Abc_LitNot(Lit) );
p->pWatches[Abc_LitNot(Lit)] = Tas_ClsHandle( p, pClause );
}
/**Function*************************************************************
@ -994,7 +994,7 @@ static inline Tas_Cls_t * Tas_ManCreateCls( Tas_Man_t * p, int hClause )
for ( i = hClause; (pObj = pQue->pData[i]); i++ )
{
assert( Tas_VarIsAssigned( pObj ) );
pClause->pLits[i-hClause] = Gia_LitNot( Tas_VarToLit(p, pObj) );
pClause->pLits[i-hClause] = Abc_LitNot( Tas_VarToLit(p, pObj) );
}
// add the clause as watched one
if ( nLits >= 2 )
@ -1027,7 +1027,7 @@ static inline int Tas_ManCreateFromCls( Tas_Man_t * p, Tas_Cls_t * pCls, int Lev
Tas_QuePush( pQue, NULL );
for ( i = 0; i < pCls->nLits; i++ )
{
pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[i]) );
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[i]) );
assert( Tas_VarIsAssigned(pObj) );
assert( !Tas_LitIsTrue( pObj, pCls->pLits[i] ) );
Tas_QuePush( pQue, pObj );
@ -1052,7 +1052,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
Gia_Obj_t * pObj;
Tas_Cls_t * pCur;
int * piPrev, iCur, iTemp;
int i, LitF = Gia_LitNot(Lit);
int i, LitF = Abc_LitNot(Lit);
// iterate through the clauses
piPrev = p->pWatches + Lit;
for ( iCur = p->pWatches[Lit]; iCur; iCur = *piPrev )
@ -1070,8 +1070,8 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
assert( pCur->pLits[1] == LitF );
// if the first literal is true, the clause is satisfied
// if ( pCur->pLits[0] == p->pAssigns[Gia_Lit2Var(pCur->pLits[0])] )
pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[0]) );
// if ( pCur->pLits[0] == p->pAssigns[Abc_Lit2Var(pCur->pLits[0])] )
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) );
if ( Tas_VarIsAssigned(pObj) && Tas_LitIsTrue( pObj, pCur->pLits[0] ) )
{
piPrev = &pCur->iNext[1];
@ -1082,8 +1082,8 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
for ( i = 2; i < (int)pCur->nLits; i++ )
{
// skip the case when the literal is false
// if ( Gia_LitNot(pCur->pLits[i]) == p->pAssigns[Gia_Lit2Var(pCur->pLits[i])] )
pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[i]) );
// if ( Abc_LitNot(pCur->pLits[i]) == p->pAssigns[Abc_Lit2Var(pCur->pLits[i])] )
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) );
if ( Tas_VarIsAssigned(pObj) && !Tas_LitIsTrue( pObj, pCur->pLits[i] ) )
continue;
// the literal is either true or unassigned - watch it
@ -1099,7 +1099,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
continue;
// clause is unit - enqueue new implication
pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[0]) );
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) );
if ( !Tas_VarIsAssigned(pObj) )
{
/*
@ -1107,7 +1107,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
int iLitLevel, iPlace;
for ( i = 1; i < (int)pCur->nLits; i++ )
{
pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[i]) );
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) );
iLitLevel = Tas_VarDecLevel( p, pObj );
iPlace = pObj->Value;
printf( "Lit = %d. Level = %d. Place = %d.\n", pCur->pLits[i], iLitLevel, iPlace );
@ -1300,7 +1300,7 @@ int Tas_ManSolve_rec( Tas_Man_t * p, int Level )
if ( Tas_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Tas_ManCheckLimits( p ) )
return 0;
// remember the state before branching
@ -1401,7 +1401,7 @@ int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
Vec_IntClear( p->vActiveVars );
// statistics
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Tas_ManCheckLimits( p ) )
RetValue = -1;
return RetValue;
@ -1460,7 +1460,7 @@ int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs )
Vec_IntClear( p->vActiveVars );
// statistics
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Tas_ManCheckLimits( p ) )
RetValue = -1;
@ -1644,19 +1644,19 @@ int Tas_StorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * p
int i;
for ( i = 0; i < nLits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
if ( Abc_InfoHasBit( pPres, iBit ) &&
Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
Abc_InfoSetBit( pPres, iBit );
if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
Abc_InfoXorBit( pInfo, iBit );
}
return 1;
}

View File

@ -457,7 +457,7 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 )
pRoot->iNext = 0;
p->pLevels[LevelStart] = Cof_ObjHandle( p, pRoot );
// set the new literal
pRoot->iLit = Gia_Var2Lit( 0, fConst1 );
pRoot->iLit = Abc_Var2Lit( 0, fConst1 );
// process nodes in the levelized order
for ( i = LevelStart; i < p->nLevels; i++ )
{
@ -465,7 +465,7 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 )
iHandle && (pTemp = Cof_ManObj(p, iHandle));
iHandle = pTemp->iNext )
{
assert( pTemp->Id != Gia_Lit2Var(pTemp->iLit) );
assert( pTemp->Id != Abc_Lit2Var(pTemp->iLit) );
Cof_ObjForEachFanout( pTemp, pNext, k )
{
if ( Cof_ObjIsCo(pNext) )
@ -477,11 +477,11 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 )
assert( pFanin0 == pTemp || pFanin1 == pTemp );
pNextGia = Gia_ManObj( p->pGia, pNext->Id );
if ( Cof_ObjIsTravIdCurrent(p, pFanin0) )
iLit0 = Gia_LitNotCond( pFanin0->iLit, Gia_ObjFaninC0(pNextGia) );
iLit0 = Abc_LitNotCond( pFanin0->iLit, Gia_ObjFaninC0(pNextGia) );
else
iLit0 = Gia_ObjFaninLit0( pNextGia, pNext->Id );
if ( Cof_ObjIsTravIdCurrent(p, pFanin1) )
iLit1 = Gia_LitNotCond( pFanin1->iLit, Gia_ObjFaninC1(pNextGia) );
iLit1 = Abc_LitNotCond( pFanin1->iLit, Gia_ObjFaninC1(pNextGia) );
else
iLit1 = Gia_ObjFaninLit1( pNextGia, pNext->Id );
iNextNew = Gia_ManHashAndTry( p->pGia, iLit0, iLit1 );
@ -578,12 +578,12 @@ void Cof_ManPrintFanio( Cof_Man_t * p )
nFanouts = Cof_ObjFanoutNum(pNode);
nFaninsAll += nFanins;
nFanoutsAll += nFanouts;
nFaninsMax = ABC_MAX( nFaninsMax, nFanins );
nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts );
nFaninsMax = Abc_MaxInt( nFaninsMax, nFanins );
nFanoutsMax = Abc_MaxInt( nFanoutsMax, nFanouts );
}
// allocate storage for fanin/fanout numbers
nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
nSizeMax = Abc_MaxInt( 10 * (Abc_Base10Log(nFaninsMax) + 1), 10 * (Abc_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@ -717,7 +717,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
return NULL;
}
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@ -728,7 +728,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
if ( pObj == pPivot )
{
iCofVar = pObj->Value;
pObj->Value = Gia_Var2Lit( 0, 0 );
pObj->Value = Abc_Var2Lit( 0, 0 );
}
}
Gia_ManForEachAnd( p, pObj, i )
@ -737,7 +737,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
if ( pObj == pPivot )
{
iCofVar = pObj->Value;
pObj->Value = Gia_Var2Lit( 0, 0 );
pObj->Value = Abc_Var2Lit( 0, 0 );
}
}
Gia_ManForEachCo( p, pObj, i )
@ -745,15 +745,15 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
// compute the positive cofactor
Gia_ManForEachCi( p, pObj, i )
{
pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 );
pObj->Value = Abc_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 );
if ( pObj == pPivot )
pObj->Value = Gia_Var2Lit( 0, 1 );
pObj->Value = Abc_Var2Lit( 0, 1 );
}
Gia_ManForEachAnd( p, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( pObj == pPivot )
pObj->Value = Gia_Var2Lit( 0, 1 );
pObj->Value = Abc_Var2Lit( 0, 1 );
}
// create MUXes
assert( iCofVar > 0 );
@ -836,9 +836,9 @@ Vec_Int_t * Gia_ManTransfer( Gia_Man_t * pAig, Gia_Man_t * pCof, Gia_Man_t * pNe
Gia_ManForEachObjVec( vSigs, pAig, pObj, i )
{
assert( Gia_ObjIsCand(pObj) );
pObjF = Gia_ManObj( pCof, Gia_Lit2Var(pObj->Value) );
pObjF = Gia_ManObj( pCof, Abc_Lit2Var(pObj->Value) );
if ( pObjF->Value && ~pObjF->Value )
Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) );
Vec_IntPushUnique( vSigsNew, Abc_Lit2Var(pObjF->Value) );
}
return vSigsNew;
}

View File

@ -55,14 +55,14 @@ void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p )
Gia_ObjSetRepr( pNew, i, GIA_VOID );
// iterate over constant candidates
Gia_ManForEachConst( p, i )
Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
// iterate over class candidates
vClass = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, i )
{
Vec_IntClear( vClass );
Gia_ClassForEachObj( p, i, k )
Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
assert( Vec_IntSize( vClass ) > 1 );
Vec_IntSort( vClass, 0 );
iRepr = iPrev = Vec_IntEntry( vClass, 0 );
@ -173,7 +173,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@ -205,7 +205,7 @@ Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
for ( i = iOutStart; i < iOutStop; i++ )
{
@ -240,8 +240,8 @@ void Gia_ManDupOrderDfsChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t *
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( pNext )
{
pNew->pNexts[Gia_Lit2Var(pObj->Value)] = Gia_Lit2Var( Gia_Lit2Var(pNext->Value) );
assert( Gia_Lit2Var(pObj->Value) > Gia_Lit2Var(pNext->Value) );
pNew->pNexts[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var( Abc_Lit2Var(pNext->Value) );
assert( Abc_Lit2Var(pObj->Value) > Abc_Lit2Var(pNext->Value) );
}
}
@ -264,7 +264,7 @@ Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p )
assert( p->pReprs && p->pNexts );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -297,7 +297,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCoReverse( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@ -329,7 +329,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -361,7 +361,7 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@ -371,13 +371,13 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
{
pObj->Value = Gia_ManAppendCi( pNew );
if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) )
pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
}
else if ( Gia_ObjIsCo(pObj) )
{
pObj->Value = Gia_ObjFanin0Copy(pObj);
if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) )
pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
}
}
@ -403,7 +403,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@ -437,7 +437,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i, iCtrl;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@ -477,7 +477,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
int i, Counter1 = 0, Counter2 = 0;
assert( p->vFlopClasses != NULL );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
@ -522,7 +522,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->nConstrs = p->nConstrs;
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@ -561,8 +561,8 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
// assert( ~pRepr->Value );
if ( !~pRepr->Value )
continue;
if ( Gia_Lit2Var(pObj->Value) != Gia_Lit2Var(pRepr->Value) )
Gia_ObjSetRepr( pNew, Gia_Lit2Var(pObj->Value), Gia_Lit2Var(pRepr->Value) );
if ( Abc_Lit2Var(pObj->Value) != Abc_Lit2Var(pRepr->Value) )
Gia_ObjSetRepr( pNew, Abc_Lit2Var(pObj->Value), Abc_Lit2Var(pRepr->Value) );
}
pNew->pNexts = Gia_ManDeriveNexts( pNew );
}
@ -588,7 +588,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
int i, t, Entry;
assert( nTimes > 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes );
vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes );
@ -604,17 +604,17 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
{
pObj->Value = Gia_ManAppendCi( pNew );
if ( Gia_ObjIsPi(p, pObj) )
Vec_IntPush( vPis, Gia_Lit2Var(pObj->Value) );
Vec_IntPush( vPis, Abc_Lit2Var(pObj->Value) );
else
Vec_IntPush( vRos, Gia_Lit2Var(pObj->Value) );
Vec_IntPush( vRos, Abc_Lit2Var(pObj->Value) );
}
else if ( Gia_ObjIsCo(pObj) )
{
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
if ( Gia_ObjIsPo(p, pObj) )
Vec_IntPush( vPos, Gia_Lit2Var(pObj->Value) );
Vec_IntPush( vPos, Abc_Lit2Var(pObj->Value) );
else
Vec_IntPush( vRis, Gia_Lit2Var(pObj->Value) );
Vec_IntPush( vRis, Abc_Lit2Var(pObj->Value) );
}
}
}
@ -667,7 +667,7 @@ int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprsOld[Gia_ObjId(p, pObj)] );
pRepr->Value = Gia_ManDupDfs2_rec( pNew, p, pRepr );
return pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
}
if ( Gia_ObjIsCi(pObj) )
return pObj->Value = Gia_ManAppendCi(pNew);
@ -698,7 +698,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupDfs2_rec( pNew, p, pObj );
@ -756,7 +756,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -789,7 +789,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -819,7 +819,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
assert( Gia_ObjIsCo(pRoot) );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -847,14 +847,14 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
int i, iLit, iLitRes;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Vec_IntForEachEntry( vLits, iLit, i )
{
iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) );
}
Gia_ManSetRegNum( pNew, 0 );
return pNew;
@ -877,7 +877,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -908,7 +908,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManSetRefs( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -943,7 +943,7 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
assert( Gia_ManRegNum(p) == 0 );
assert( Gia_ManRegNum(p2) == 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p)+Gia_ManObjNum(p2) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
// dup first AIG
Gia_ManConst0(p)->Value = 0;
@ -1005,13 +1005,13 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
{
pObj->Value = Gia_ManAppendCi(pNew);
if ( ~pCi2Lit[i] )
pObj->Value = Gia_LitNotCond( Gia_ManObj(p, Gia_Lit2Var(pCi2Lit[i]))->Value, Gia_LitIsCompl(pCi2Lit[i]) );
pObj->Value = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(pCi2Lit[i]))->Value, Abc_LitIsCompl(pCi2Lit[i]) );
}
Gia_ManHashAlloc( pNew );
if ( vLits )
@ -1019,8 +1019,8 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
int iLit, iLitRes;
Vec_IntForEachEntry( vLits, iLit, i )
{
iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) );
}
}
else
@ -1055,7 +1055,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
assert( p->pReprsOld != NULL );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -1112,7 +1112,7 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose )
{
if ( Gia_ObjIsCi(pObj) )
{
Vec_IntPush( vLeaves, Gia_Var2Lit( Gia_ObjId(p, pObj), 0 ) );
Vec_IntPush( vLeaves, Abc_Var2Lit( Gia_ObjId(p, pObj), 0 ) );
continue;
}
assert( Gia_ObjIsAnd(pObj) );
@ -1132,16 +1132,16 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose )
pVar2Val = ABC_FALLOC( char, Gia_ManObjNum(p) );
Vec_IntForEachEntry( vLeaves, iLit, i )
{
iObjId = Gia_Lit2Var(iLit);
iObjId = Abc_Lit2Var(iLit);
pObj = Gia_ManObj(p, iObjId);
if ( Gia_ObjIsCi(pObj) )
{
pCi2Lit[Gia_ObjCioId(pObj)] = !Gia_LitIsCompl(iLit);
pCi2Lit[Gia_ObjCioId(pObj)] = !Abc_LitIsCompl(iLit);
nCiLits++;
}
if ( pVar2Val[iObjId] != 0 && pVar2Val[iObjId] != 1 )
pVar2Val[iObjId] = Gia_LitIsCompl(iLit);
else if ( pVar2Val[iObjId] != Gia_LitIsCompl(iLit) )
pVar2Val[iObjId] = Abc_LitIsCompl(iLit);
else if ( pVar2Val[iObjId] != Abc_LitIsCompl(iLit) )
break;
}
if ( i < Vec_IntSize(vLeaves) )
@ -1156,7 +1156,7 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose )
Vec_IntClear( vLeaves );
Gia_ManForEachObj( p, pObj, i )
if ( !Gia_ObjIsCi(pObj) && (pVar2Val[i] == 0 || pVar2Val[i] == 1) )
Vec_IntPush( vLeaves, Gia_Var2Lit(i, pVar2Val[i]) );
Vec_IntPush( vLeaves, Abc_Var2Lit(i, pVar2Val[i]) );
if ( fVerbose )
printf( "Detected %6d AND leaves and %6d CI leaves.\n", Vec_IntSize(vLeaves), nCiLits );
// create the input map
@ -1272,7 +1272,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
}
// start the manager
pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
pNew->pName = Gia_UtilStrsav( "miter" );
pNew->pName = Abc_UtilStrsav( "miter" );
// map combinational inputs
Gia_ManFillValue( p0 );
Gia_ManFillValue( p1 );
@ -1372,7 +1372,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
int i, iLit;
assert( (Gia_ManPoNum(p) & 1) == 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManHashAlloc( pNew );
Gia_ManForEachCi( p, pObj, i )
@ -1444,7 +1444,7 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
}
// start the new manager
pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
pNew->pName = Gia_UtilStrsav( pGia0->pName );
pNew->pName = Abc_UtilStrsav( pGia0->pName );
// create new CIs and assign them to the old manager CIs
for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
{
@ -1485,7 +1485,7 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
Gia_Obj_t * pObj;
int i, nConstr = 0;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -1546,7 +1546,7 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
Gia_ManFillValue( p );
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
// create PIs
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
@ -1647,7 +1647,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
// create constant
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@ -1681,7 +1681,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
if ( !~pObj->Value )
continue;
assert( !Gia_LitIsCompl(pObj->Value) );
assert( !Abc_LitIsCompl(pObj->Value) );
pCopy = Gia_ObjCopy( pTemp, pObj );
if ( !~pCopy->Value )
{
@ -1689,7 +1689,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
pObj->Value = ~0;
continue;
}
assert( !Gia_LitIsCompl(pCopy->Value) );
assert( !Abc_LitIsCompl(pCopy->Value) );
pObj->Value = pCopy->Value;
}
}

View File

@ -20,7 +20,7 @@
#include <math.h>
#include "gia.h"
#include "ioa.h"
#include "src/aig/ioa/ioa.h"
ABC_NAMESPACE_IMPL_START
@ -690,12 +690,12 @@ void Emb_ManPrintFanio( Emb_Man_t * p )
nFanouts = Emb_ObjFanoutNum(pNode);
nFaninsAll += nFanins;
nFanoutsAll += nFanouts;
nFaninsMax = ABC_MAX( nFaninsMax, nFanins );
nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts );
nFaninsMax = Abc_MaxInt( nFaninsMax, nFanins );
nFanoutsMax = Abc_MaxInt( nFanoutsMax, nFanouts );
}
// allocate storage for fanin/fanout numbers
nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
nSizeMax = Abc_MaxInt( 10 * (Abc_Base10Log(nFaninsMax) + 1), 10 * (Abc_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@ -1436,8 +1436,8 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
pY0 = Emb_ManSol( p, 0 );
for ( k = 0; k < p->nObjs; k++ )
{
Min0 = ABC_MIN( Min0, pY0[k] );
Max0 = ABC_MAX( Max0, pY0[k] );
Min0 = Abc_MinInt( Min0, pY0[k] );
Max0 = Abc_MaxInt( Max0, pY0[k] );
}
Str0 = 1.0*GIA_PLACE_SIZE/(Max0 - Min0);
// update the coordinates
@ -1450,8 +1450,8 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
pY1 = Emb_ManSol( p, 1 );
for ( k = 0; k < p->nObjs; k++ )
{
Min1 = ABC_MIN( Min1, pY1[k] );
Max1 = ABC_MAX( Max1, pY1[k] );
Min1 = Abc_MinInt( Min1, pY1[k] );
Max1 = Abc_MaxInt( Max1, pY1[k] );
}
Str1 = 1.0*GIA_PLACE_SIZE/(Max1 - Min1);
// update the coordinates
@ -1498,10 +1498,10 @@ double Emb_ManComputeHPWL( Emb_Man_t * p )
iMinY = iMaxY = p->pPlacement[2*pThis->Value+1];
Emb_ObjForEachFanout( pThis, pNext, k )
{
iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] );
iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] );
iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] );
iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] );
iMinX = Abc_MinInt( iMinX, p->pPlacement[2*pNext->Value+0] );
iMaxX = Abc_MaxInt( iMaxX, p->pPlacement[2*pNext->Value+0] );
iMinY = Abc_MinInt( iMinY, p->pPlacement[2*pNext->Value+1] );
iMaxY = Abc_MaxInt( iMaxY, p->pPlacement[2*pNext->Value+1] );
}
Result += (iMaxX - iMinX) + (iMaxY - iMinY);
}
@ -1548,10 +1548,10 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
iMinY = iMaxY = p->pPlacement[2*pThis->Value+1];
Emb_ObjForEachFanout( pThis, pNext, k )
{
iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] );
iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] );
iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] );
iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] );
iMinX = Abc_MinInt( iMinX, p->pPlacement[2*pNext->Value+0] );
iMaxX = Abc_MaxInt( iMaxX, p->pPlacement[2*pNext->Value+0] );
iMinY = Abc_MinInt( iMinY, p->pPlacement[2*pNext->Value+1] );
iMaxY = Abc_MaxInt( iMaxY, p->pPlacement[2*pNext->Value+1] );
}
pEdgeX[pThis->Value] = 0.5 * (iMaxX + iMinX);
pEdgeY[pThis->Value] = 0.5 * (iMaxY + iMinY);

View File

@ -338,9 +338,9 @@ Vec_Int_t * Gia_ManTransferFrames( Gia_Man_t * pAig, Gia_Man_t * pFrames, int nF
assert( Gia_ObjIsCand(pObj) );
for ( f = 0; f < nFrames; f++ )
{
pObjF = Gia_ManObj( pFrames, Gia_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) );
pObjF = Gia_ManObj( pFrames, Abc_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) );
if ( pObjF->Value && ~pObjF->Value )
Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) );
Vec_IntPushUnique( vSigsNew, Abc_Lit2Var(pObjF->Value) );
}
}
return vSigsNew;
@ -365,7 +365,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
ABC_FREE( p->pCopies );
p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, 0 );
@ -440,7 +440,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
Gia_Obj_t * pThis, * pNode;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@ -481,13 +481,13 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
{
// printf( "FlopIn compl = %d. FlopOut is d0. Complement = %d.\n",
// Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj0) );
pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj1)->Value, !Gia_IsComplement(pObj1));
pFlopIn->Value = Abc_LitNotCond(Gia_Regular(pObj1)->Value, !Gia_IsComplement(pObj1));
}
else if ( Gia_Regular(pObj1) == pFlopOut )
{
// printf( "FlopIn compl = %d. FlopOut is d1. Complement = %d.\n",
// Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj1) );
pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj0)->Value, !Gia_IsComplement(pObj0));
pFlopIn->Value = Abc_LitNotCond(Gia_Regular(pObj0)->Value, !Gia_IsComplement(pObj0));
}
}
Gia_ManForEachCo( p, pThis, i )
@ -610,7 +610,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@ -627,7 +627,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
if ( pData == NULL )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
else
pObj->Value = Gia_ManAppendCo( pNew, Gia_LitNotCond(Gia_Regular(pData)->Value, Gia_IsComplement(pData)) );
pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNotCond(Gia_Regular(pData)->Value, Gia_IsComplement(pData)) );
}
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Vec_PtrFree( vDatas );

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "cec.h"
#include "src/proof/cec/cec.h"
ABC_NAMESPACE_IMPL_START
@ -417,7 +417,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
{
Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
if ( ~pObj->Value )
@ -474,7 +474,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -536,7 +536,7 @@ void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew )
{
if ( !~pObj->Value )
continue;
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
if ( pObjNew->fMark0 )
pObj->Value = ~0;
}
@ -568,10 +568,10 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
pObj = Gia_ManObj( p, i );
if ( !~pObj->Value )
continue;
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
if ( Gia_Lit2Var(pObjNew->Value) == 0 )
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
if ( Abc_Lit2Var(pObjNew->Value) == 0 )
continue;
Gia_ObjSetRepr( pFinal, Gia_Lit2Var(pObjNew->Value), 0 );
Gia_ObjSetRepr( pFinal, Abc_Lit2Var(pObjNew->Value), 0 );
}
// iterate over class candidates
vClass = Vec_IntAlloc( 100 );
@ -583,8 +583,8 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
pObj = Gia_ManObj( p, k );
if ( !~pObj->Value )
continue;
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
Vec_IntPushUnique( vClass, Gia_Lit2Var(pObjNew->Value) );
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
Vec_IntPushUnique( vClass, Abc_Lit2Var(pObjNew->Value) );
}
if ( Vec_IntSize( vClass ) < 2 )
continue;
@ -624,14 +624,14 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
Gia_ObjSetRepr( pNew, i, GIA_VOID );
// iterate over constant candidates
Gia_ManForEachConst( p, i )
Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
// iterate over class candidates
vClass = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, i )
{
Vec_IntClear( vClass );
Gia_ClassForEachObj( p, i, k )
Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
assert( Vec_IntSize( vClass ) > 1 );
Vec_IntSort( vClass, 0 );
iRepr = iPrev = Vec_IntEntry( vClass, 0 );
@ -758,7 +758,7 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
// if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
return;
iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
{
if ( vTrace )
@ -847,7 +847,7 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
Gia_ManSetPhase( p );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -917,7 +917,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -983,7 +983,7 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve
// if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
return;
iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) );
Gia_ObjSetCopyF( p, f, pObj, iLitNew );
@ -1063,10 +1063,10 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
if ( fDualOut )
Gia_ManEquivSetColors( p, 0 );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, Gia_InfoHasBit(pInit->pData, i) );
Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) );
for ( f = 0; f < nFrames; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
@ -1463,7 +1463,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
{
if ( Gia_ObjIsConst0(pRepr) )
{
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
Gia_ManEquivToChoices_rec( pNew, p, pRepr );
@ -1471,22 +1471,22 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
{
assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
return;
}
if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
return;
assert( pRepr->Value < pObj->Value );
pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
{
// assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) != pReprNew )
return;
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
@ -1495,7 +1495,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
}
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
@ -1573,7 +1573,7 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
@ -1654,9 +1654,9 @@ int Gia_ManCountChoices( Gia_Man_t * p )
ABC_NAMESPACE_IMPL_END
#include "aig.h"
#include "saig.h"
#include "cec.h"
#include "src/aig/aig/aig.h"
#include "src/aig/saig/saig.h"
#include "src/proof/cec/cec.h"
#include "giaAig.h"
ABC_NAMESPACE_IMPL_START
@ -1826,7 +1826,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
{
if ( pObj1->Value == ~0 )
continue;
pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) );
pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
pObj->fMark0 = 1;
}
@ -1835,7 +1835,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
{
if ( pObj2->Value == ~0 )
continue;
pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) );
pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
pObj->fMark1 = 1;
}
@ -1965,7 +1965,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
{
if ( pObj1->Value == ~0 )
continue;
pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) );
pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
pObj->fMark0 = 1;
}
@ -1974,7 +1974,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
{
if ( pObj2->Value == ~0 )
continue;
pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) );
pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
pObj->fMark1 = 1;
}

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "mem.h"
#include "src/misc/mem/mem.h"
ABC_NAMESPACE_IMPL_START
@ -45,7 +45,7 @@ struct Gia_ManEra_t_
{
Gia_Man_t * pAig; // user's AIG manager
int nWordsSim; // 2^(PInum)
int nWordsDat; // Gia_BitWordNum
int nWordsDat; // Abc_BitWordNum
unsigned * pDataSim; // simulation data
Mem_Fixed_t * pMemory; // memory manager
Vec_Ptr_t * vStates; // reached states
@ -83,12 +83,12 @@ Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig )
int i;
p = ABC_CALLOC( Gia_ManEra_t, 1 );
p->pAig = pAig;
p->nWordsSim = Gia_TruthWordNum( Gia_ManPiNum(pAig) );
p->nWordsDat = Gia_BitWordNum( Gia_ManRegNum(pAig) );
p->nWordsSim = Abc_TruthWordNum( Gia_ManPiNum(pAig) );
p->nWordsDat = Abc_BitWordNum( Gia_ManRegNum(pAig) );
p->pDataSim = ABC_ALLOC( unsigned, p->nWordsSim*Gia_ManObjNum(pAig) );
p->pMemory = Mem_FixedStart( sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat );
p->vStates = Vec_PtrAlloc( 100000 );
p->nBins = Gia_PrimeCudd( 100000 );
p->nBins = Abc_PrimeCudd( 100000 );
p->pBins = ABC_CALLOC( unsigned, p->nBins );
Vec_PtrPush( p->vStates, NULL );
// assign primary input values
@ -226,7 +226,7 @@ void Gia_ManEraHashResize( Gia_ManEra_t * p )
// replace the table
pBinsOld = p->pBins;
nBinsOld = p->nBins;
p->nBins = Gia_PrimeCudd( 3 * p->nBins );
p->nBins = Abc_PrimeCudd( 3 * p->nBins );
p->pBins = ABC_CALLOC( unsigned, p->nBins );
// rehash the entries from the old table
Counter = 0;
@ -266,7 +266,7 @@ void Gia_ManInsertState( Gia_ManEra_t * p, Gia_ObjEra_t * pState )
Gia_ManForEachRo( p->pAig, pObj, i )
{
pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
if ( Gia_InfoHasBit(pState->pData, i) )
if ( Abc_InfoHasBit(pState->pData, i) )
memset( pSimInfo, 0xff, sizeof(unsigned) * p->nWordsSim );
else
memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim );
@ -465,8 +465,8 @@ int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter )
Gia_ManForEachRi( p->pAig, pObj, i )
{
pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
if ( Gia_InfoHasBit(p->pStateNew->pData, i) != Gia_InfoHasBit(pSimInfo, k) )
Gia_InfoXorBit( p->pStateNew->pData, i );
if ( Abc_InfoHasBit(p->pStateNew->pData, i) != Abc_InfoHasBit(pSimInfo, k) )
Abc_InfoXorBit( p->pStateNew->pData, i );
}
piPlace = Gia_ManEraHashFind( p, p->pStateNew );
if ( piPlace == NULL )

View File

@ -136,11 +136,11 @@ static inline Gia_ObjAre_t * Gia_ObjNextObj0( Gia_ManAre_t * p, Gia_ObjAre_t *
static inline Gia_ObjAre_t * Gia_ObjNextObj1( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[1] ); }
static inline Gia_ObjAre_t * Gia_ObjNextObj2( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[2] ); }
static inline int Gia_StaHasValue0( Gia_StaAre_t * p, int iReg ) { return Gia_InfoHasBit( p->pData, iReg << 1 ); }
static inline int Gia_StaHasValue1( Gia_StaAre_t * p, int iReg ) { return Gia_InfoHasBit( p->pData, (iReg << 1) + 1 ); }
static inline int Gia_StaHasValue0( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, iReg << 1 ); }
static inline int Gia_StaHasValue1( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, (iReg << 1) + 1 ); }
static inline void Gia_StaSetValue0( Gia_StaAre_t * p, int iReg ) { Gia_InfoSetBit( p->pData, iReg << 1 ); }
static inline void Gia_StaSetValue1( Gia_StaAre_t * p, int iReg ) { Gia_InfoSetBit( p->pData, (iReg << 1) + 1 ); }
static inline void Gia_StaSetValue0( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, iReg << 1 ); }
static inline void Gia_StaSetValue1( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, (iReg << 1) + 1 ); }
static inline Gia_StaAre_t * Gia_StaPrev( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iPrev); }
static inline Gia_StaAre_t * Gia_StaNext( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iNext); }
@ -198,7 +198,7 @@ void Gia_ManCountMintermsInCube( Gia_StaAre_t * pCube, int nVars, unsigned * pSt
for ( i = 0; i < nVars; i++ )
if ( m & (1 << i) )
Mint |= (1 << Dashes[i]);
Gia_InfoSetBit( pStore, Mint );
Abc_InfoSetBit( pStore, Mint );
}
}
@ -220,7 +220,7 @@ int Gia_ManCountMinterms( Gia_ManAre_t * p )
int i, nMemSize, Counter = 0;
if ( Gia_ManRegNum(p->pAig) > 30 )
return -1;
nMemSize = Gia_BitWordNum( 1 << Gia_ManRegNum(p->pAig) );
nMemSize = Abc_BitWordNum( 1 << Gia_ManRegNum(p->pAig) );
pMemory = ABC_CALLOC( unsigned, nMemSize );
Gia_ManAreForEachCubeStore( p, pCube, i )
if ( Gia_StaIsUsed(pCube) )
@ -477,7 +477,7 @@ Gia_ManAre_t * Gia_ManAreCreate( Gia_Man_t * pAig )
assert( sizeof(Gia_ObjAre_t) == 16 );
p = ABC_CALLOC( Gia_ManAre_t, 1 );
p->pAig = pAig;
p->nWords = Gia_BitWordNum( 2 * Gia_ManRegNum(pAig) );
p->nWords = Abc_BitWordNum( 2 * Gia_ManRegNum(pAig) );
p->nSize = sizeof(Gia_StaAre_t)/4 + p->nWords;
p->ppObjs = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
p->ppStas = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
@ -1421,7 +1421,7 @@ static inline Gia_Obj_t * Gia_ManAreMostUsedPi( Gia_ManAre_t * p )
if ( pObj->Value <= 1 )
continue;
Gia_ManIncrementTravId( p->pNew );
Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Gia_Lit2Var(pObj->Value)) );
Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Abc_Lit2Var(pObj->Value)) );
}
// check the CI counters
Gia_ManForEachCi( p->pNew, pObj, i )
@ -1471,7 +1471,7 @@ static inline int Gia_ManCheckPOs( Gia_ManAre_t * p )
int i, CountCur, CountMax = 0;
Gia_ManForEachPo( p->pAig, pObj, i )
{
pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) );
pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
if ( Gia_ObjIsConst0(pObjNew) )
CountCur = 0;
else
@ -1479,7 +1479,7 @@ static inline int Gia_ManCheckPOs( Gia_ManAre_t * p )
Gia_ManIncrementTravId( p->pNew );
CountCur = Gia_ManCheckPOs_rec( p->pNew, pObjNew );
}
CountMax = ABC_MAX( CountMax, CountCur );
CountMax = Abc_MaxInt( CountMax, CountCur );
}
return CountMax;
}
@ -1501,10 +1501,10 @@ static inline int Gia_ManCheckPOstatus( Gia_ManAre_t * p )
int i;
Gia_ManForEachPo( p->pAig, pObj, i )
{
pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) );
pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
if ( Gia_ObjIsConst0(pObjNew) )
{
if ( Gia_LitIsCompl(pObj->Value) )
if ( Abc_LitIsCompl(pObj->Value) )
{
p->iOutFail = i;
return 1;
@ -1638,7 +1638,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
else if ( Gia_StaHasValue1( pSta, i ) )
pObj->Value = 1;
else // don't-care literal
pObj->Value = Gia_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 );
pObj->Value = Abc_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 );
}
Gia_ManForEachAnd( p->pAig, pObj, i )
pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@ -1770,8 +1770,8 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
ABC_NAMESPACE_IMPL_END
#include "giaAig.h"
#include "cnf.h"
#include "satSolver.h"
#include "src/sat/cnf/cnf.h"
#include "src/sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
@ -1848,22 +1848,22 @@ void Gia_ManAreDeriveCexSat( Gia_ManAre_t * p, Gia_StaAre_t * pCur, Gia_StaAre_t
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
if ( Gia_StaHasValue0(pCur, i) )
Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) );
Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) );
else if ( Gia_StaHasValue1(pCur, i) )
Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) );
Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) );
}
if ( pNext )
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
if ( Gia_StaHasValue0(pNext, i) )
Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) );
Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) );
else if ( Gia_StaHasValue1(pNext, i) )
Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) );
Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) );
}
if ( iOutFailed >= 0 )
{
assert( iOutFailed < Gia_ManPoNum(p->pAig) );
Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) );
Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) );
}
// solve SAT
status = sat_solver_solve( (sat_solver *)p->pSat, (int *)Vec_IntArray(p->vAssumps), (int *)Vec_IntArray(p->vAssumps) + Vec_IntSize(p->vAssumps),
@ -1935,7 +1935,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast )
Vec_IntForEachEntry( p->vCofVars, Var, v )
{
assert( Var < Gia_ManPiNum(p->pAig) );
Gia_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var );
Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var );
}
}
// free temporary things

View File

@ -120,7 +120,7 @@ void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout )
assert( Gia_ObjId(p, pFanout) > 0 );
if ( Gia_ObjId(p, pObj) >= p->nFansAlloc || Gia_ObjId(p, pFanout) >= p->nFansAlloc )
{
int nFansAlloc = 2 * ABC_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
int nFansAlloc = 2 * Abc_MaxInt( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;

View File

@ -609,7 +609,7 @@ int Frc_ManCrossCut_rec( Frc_Man_t * p, Frc_Obj_t * pObj )
Frc_Obj_t * pFanin;
int i;
p->nCutCur++;
p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur );
p->nCutMax = Abc_MaxInt( p->nCutMax, p->nCutCur );
if ( !Frc_ObjIsCi(pObj) )
Frc_ObjForEachFanin( pObj, pFanin, i )
p->nCutCur -= Frc_ManCrossCut_rec( p, pFanin );
@ -636,7 +636,7 @@ int Frc_ManCrossCut2_rec( Frc_Man_t * p, Frc_Obj_t * pObj )
Frc_Obj_t * pFanin;
int i;
p->nCutCur++;
p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur );
p->nCutMax = Abc_MaxInt( p->nCutMax, p->nCutCur );
if ( !Frc_ObjIsCi(pObj) )
Frc_ObjForEachFaninReverse( pObj, pFanin, i )
p->nCutCur -= Frc_ManCrossCut2_rec( p, pFanin );
@ -912,8 +912,8 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose )
iMinX = iMaxX = pThis->pPlace;
Frc_ObjForEachFanout( pThis, pNext, k )
{
iMinX = ABC_MIN( iMinX, pNext->pPlace );
iMaxX = ABC_MAX( iMaxX, pNext->pPlace );
iMinX = Abc_MinInt( iMinX, pNext->pPlace );
iMaxX = Abc_MaxInt( iMaxX, pNext->pPlace );
}
pThis->fEdgeCenter = 0.5 * (iMaxX + iMinX);
CostThis += (iMaxX - iMinX);

View File

@ -90,7 +90,7 @@ void Gia_ManUnrollDup_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj, int Id )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
else assert( 0 );
Gia_ManObj(pNew, Gia_Lit2Var(pObj->Value))->Value = Id;
Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Id;
}
/**Function*************************************************************
@ -111,7 +111,7 @@ Gia_Man_t * Gia_ManUnrollDup( Gia_Man_t * p, Vec_Int_t * vLimit )
int i;
assert( Vec_IntSize(vLimit) == 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
// save constant class
Gia_ManFillValue( p );
@ -161,7 +161,7 @@ Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames )
int nObjBits, nObjMask;
int f, fMax, k, Entry, Prev, iStart, iStop, Size;
// get the bitmasks
nObjBits = Gia_Base2Log( Gia_ManObjNum(p) );
nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
nObjMask = (1 << nObjBits) - 1;
assert( Gia_ManObjNum(p) <= nObjMask );
// derive the tents
@ -349,12 +349,12 @@ static inline int Gia_ObjUnrRead( Gia_ManUnr_t * p, int Id, int Degree )
static inline int Gia_ObjUnrReadCopy0( Gia_ManUnr_t * p, Gia_Obj_t * pObj, int Id )
{
int Lit = Gia_ObjUnrRead(p, Gia_ObjFaninId0(pObj, Id), Vec_IntEntry(p->vDegDiff, 2*Id));
return Gia_LitNotCond( Lit, Gia_ObjFaninC0(pObj) );
return Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObj) );
}
static inline int Gia_ObjUnrReadCopy1( Gia_ManUnr_t * p, Gia_Obj_t * pObj, int Id )
{
int Lit = Gia_ObjUnrRead(p, Gia_ObjFaninId1(pObj, Id), Vec_IntEntry(p->vDegDiff, 2*Id+1));
return Gia_LitNotCond( Lit, Gia_ObjFaninC1(pObj) );
return Abc_LitNotCond( Lit, Gia_ObjFaninC1(pObj) );
}
static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t * pNew )
{
@ -367,7 +367,7 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
else
pObj = Gia_ManPi( pNew, Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
return Abc_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
}
if ( f == 0 ) // initialize!
{
@ -378,9 +378,9 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * p->pPars->nFrames + Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
else
pObj = Gia_ManPi( pNew, Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
return Abc_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
}
pObj = Gia_ManObj( p->pOrder, Gia_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) );
pObj = Gia_ManObj( p->pOrder, Abc_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) );
assert( Gia_ObjIsCo(pObj) );
return Gia_ObjUnrRead( p, Gia_ObjId(p->pOrder, pObj), 0 );
}
@ -405,7 +405,7 @@ void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
// start timeframes
assert( p->pNew == NULL );
p->pNew = Gia_ManStart( 10000 );
p->pNew->pName = Gia_UtilStrsav( p->pAig->pName );
p->pNew->pName = Abc_UtilStrsav( p->pAig->pName );
Gia_ManHashAlloc( p->pNew );
// create combinational inputs
if ( !p->pPars->fSaveLastLit ) // only in the case when unrolling depth is known
@ -541,7 +541,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
int fMax, f, i, Lit, Beg, End;
// start timeframes
pNew = Gia_ManStart( 10000 );
pNew->pName = Gia_UtilStrsav( p->pAig->pName );
pNew->pName = Abc_UtilStrsav( p->pAig->pName );
Gia_ManHashAlloc( pNew );
// create combinational inputs
for ( f = 0; f < p->pPars->nFrames; f++ )
@ -754,7 +754,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
Gia_ManFraSupports( p );
pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+
Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) );
pFrames->pName = Gia_UtilStrsav( pAig->pName );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )
@ -864,7 +864,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
if ( pPars->fInit )
return Gia_ManFramesInit( pAig, pPars );
pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) );
pFrames->pName = Gia_UtilStrsav( pAig->pName );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )

View File

@ -115,7 +115,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
Gia_ManSetRefs( p );
// start the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit);
// start the frontier
pFront = ABC_CALLOC( char, pNew->nFront );
@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
nCrossCutMax = nCrossCut;
// create new node
iLit = Gia_ManAppendCi( pNew );
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) );
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
// handle CIs without fanout
@ -147,7 +147,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
assert( Gia_ObjValue(pObj) == 0 );
// create new node
iLit = Gia_ManAppendCo( pNew, 0 );
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) );
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
// get the fanin
pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );

View File

@ -301,7 +301,7 @@ int Hcd_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
void Hcd_ManClassesRehash( Hcd_Man_t * p, Vec_Int_t * vRefined )
{
int * pTable, nTableSize, Key, i, k;
nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
@ -538,7 +538,7 @@ Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvR
vRoots = Vec_PtrAlloc( 100 );
// copy unmarked nodes
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -553,7 +553,7 @@ Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvR
{
// printf( "Substituting %d <--- %d\n", Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj) );
assert( pRepr < pObj );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
continue;
}
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@ -644,19 +644,19 @@ int Gia_GiarfStorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, in
int i;
for ( i = 0; i < nLits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
if ( Abc_InfoHasBit( pPres, iBit ) &&
Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
Abc_InfoSetBit( pPres, iBit );
if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
Abc_InfoXorBit( pInfo, iBit );
}
return 1;
}
@ -699,10 +699,10 @@ void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k )
int Lit, i;
Vec_IntForEachEntry( vCex, Lit, i )
{
pObj = Gia_ManCi( p->pGia, Gia_Lit2Var(Lit) );
pObj = Gia_ManCi( p->pGia, Abc_Lit2Var(Lit) );
pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) );
if ( Gia_InfoHasBit( pInfo, k ) == Gia_LitIsCompl(Lit) )
Gia_InfoXorBit( pInfo, k );
if ( Abc_InfoHasBit( pInfo, k ) == Abc_LitIsCompl(Lit) )
Abc_InfoXorBit( pInfo, k );
}
}
@ -737,7 +737,7 @@ void Gia_GiarfPrintClasses( Gia_Man_t * pGia )
ABC_NAMESPACE_IMPL_END
#include "cecInt.h"
#include "src/proof/cec/cecInt.h"
ABC_NAMESPACE_IMPL_START
@ -785,7 +785,7 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t
iRoot = Gia_ObjId( p->pGia, pRoot );
if ( !Gia_ObjIsConst( p->pGia, iRoot ) )
continue;
iRootNew = Gia_LitNotCond( pRoot->Value, pRoot->fPhase );
iRootNew = Abc_LitNotCond( pRoot->Value, pRoot->fPhase );
assert( iRootNew != 1 );
if ( fUse2Solver )
{
@ -880,8 +880,8 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t
pMemberPrev = (Gia_Obj_t *)Vec_PtrEntryLast( vMembers );
Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
{
iMemberPrev = Gia_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase );
iMember = Gia_LitNotCond( pMember->Value, !pMember->fPhase );
iMemberPrev = Abc_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase );
iMember = Abc_LitNotCond( pMember->Value, !pMember->fPhase );
assert( iMemberPrev != iMember );
if ( fUse2Solver )
{

View File

@ -333,7 +333,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i);
return Gia_InfoHasBit( pNode->uTruth, Phase );
return Abc_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@ -352,7 +352,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i);
return Gia_InfoHasBit( pNode->uTruth, Phase );
return Abc_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@ -593,7 +593,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
for ( k = 0; k < nFanins; k++ )
if ( (pSimInfos[k] >> i) & 1 )
Phase |= (1 << k);
if ( Gia_InfoHasBit( pNode->uTruth, Phase ) )
if ( Abc_InfoHasBit( pNode->uTruth, Phase ) )
Result |= (1 << i);
}
return Result;
@ -755,7 +755,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
}
else
{
int nIters = Gia_BitWordNum(nPatterns);
int nIters = Abc_BitWordNum(nPatterns);
Gli_ManSimulateSeqPref( p, 16 );
for ( i = 0; i < 32; i++ )
{

View File

@ -46,10 +46,10 @@ static inline int Gia_ManHashOne( int iLit0, int iLit1, int TableSize )
{
unsigned Key = 0;
assert( iLit0 < iLit1 );
Key ^= Gia_Lit2Var(iLit0) * 7937;
Key ^= Gia_Lit2Var(iLit1) * 2971;
Key ^= Gia_LitIsCompl(iLit0) * 911;
Key ^= Gia_LitIsCompl(iLit1) * 353;
Key ^= Abc_Lit2Var(iLit0) * 7937;
Key ^= Abc_Lit2Var(iLit1) * 2971;
Key ^= Abc_LitIsCompl(iLit0) * 911;
Key ^= Abc_LitIsCompl(iLit1) * 353;
return (int)(Key % TableSize);
}
@ -68,8 +68,8 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
{
Gia_Obj_t * pThis;
int * pPlace = p->pHTable + Gia_ManHashOne( iLit0, iLit1, p->nHTable );
for ( pThis = (*pPlace)? Gia_ManObj(p, Gia_Lit2Var(*pPlace)) : NULL; pThis;
pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Gia_Lit2Var(*pPlace)) : NULL )
for ( pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL; pThis;
pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL )
if ( Gia_ObjFaninLit0p(p, pThis) == iLit0 && Gia_ObjFaninLit1p(p, pThis) == iLit1 )
break;
return pPlace;
@ -109,7 +109,7 @@ int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
void Gia_ManHashAlloc( Gia_Man_t * p )
{
assert( p->pHTable == NULL );
p->nHTable = Gia_PrimeCudd( p->nObjsAlloc );
p->nHTable = Abc_PrimeCudd( p->nObjsAlloc );
p->pHTable = ABC_CALLOC( int, p->nHTable );
}
@ -134,7 +134,7 @@ void Gia_ManHashStart( Gia_Man_t * p )
{
pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
assert( *pPlace == 0 );
*pPlace = Gia_Var2Lit( i, 0 );
*pPlace = Abc_Var2Lit( i, 0 );
}
}
@ -175,20 +175,20 @@ void Gia_ManHashResize( Gia_Man_t * p )
// replace the table
pHTableOld = p->pHTable;
nHTableOld = p->nHTable;
p->nHTable = Gia_PrimeCudd( 2 * Gia_ManAndNum(p) );
p->nHTable = Abc_PrimeCudd( 2 * Gia_ManAndNum(p) );
p->pHTable = ABC_CALLOC( int, p->nHTable );
// rehash the entries from the old table
Counter = 0;
for ( i = 0; i < nHTableOld; i++ )
for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Gia_Lit2Var(pHTableOld[i])) : NULL),
for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Abc_Lit2Var(pHTableOld[i])) : NULL),
iNext = (pThis? pThis->Value : 0);
pThis; pThis = (iNext? Gia_ManObj(p, Gia_Lit2Var(iNext)) : NULL),
pThis; pThis = (iNext? Gia_ManObj(p, Abc_Lit2Var(iNext)) : NULL),
iNext = (pThis? pThis->Value : 0) )
{
pThis->Value = 0;
pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0p(p, pThis), Gia_ObjFaninLit1p(p, pThis) );
assert( *pPlace == 0 ); // should not be there
*pPlace = Gia_Var2Lit( Gia_ObjId(p, pThis), 0 );
*pPlace = Abc_Var2Lit( Gia_ObjId(p, pThis), 0 );
assert( *pPlace != 0 );
Counter++;
}
@ -220,9 +220,9 @@ void Gia_ManHashProfile( Gia_Man_t * p )
for ( i = 0; i < Limit; i++ )
{
Counter = 0;
for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Gia_Lit2Var(p->pHTable[i])) : NULL);
for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Abc_Lit2Var(p->pHTable[i])) : NULL);
pEntry;
pEntry = (pEntry->Value? Gia_ManObj(p, Gia_Lit2Var(pEntry->Value)) : NULL) )
pEntry = (pEntry->Value? Gia_ManObj(p, Abc_Lit2Var(pEntry->Value)) : NULL) )
Counter++;
if ( Counter )
printf( "%d ", Counter );
@ -480,7 +480,7 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
return iLit1 ? iLit0 : 0;
if ( iLit0 == iLit1 )
return iLit1;
if ( iLit0 == Gia_LitNot(iLit1) )
if ( iLit0 == Abc_LitNot(iLit1) )
return 0;
if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
Gia_ManHashResize( p );
@ -531,7 +531,7 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
return iLit1 ? iLit0 : 0;
if ( iLit0 == iLit1 )
return iLit1;
if ( iLit0 == Gia_LitNot(iLit1) )
if ( iLit0 == Abc_LitNot(iLit1) )
return 0;
if ( iLit0 > iLit1 )
iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
@ -556,10 +556,10 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
***********************************************************************/
int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
{
int fCompl = Gia_LitIsCompl(iLit0) ^ Gia_LitIsCompl(iLit1);
int iTemp0 = Gia_ManHashAnd( p, Gia_LitRegular(iLit0), Gia_LitNot(Gia_LitRegular(iLit1)) );
int iTemp1 = Gia_ManHashAnd( p, Gia_LitRegular(iLit1), Gia_LitNot(Gia_LitRegular(iLit0)) );
return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), !fCompl );
int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
}
/**Function*************************************************************
@ -575,9 +575,9 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
***********************************************************************/
int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
{
int iTemp0 = Gia_ManHashAnd( p, Gia_LitNot(iCtrl), iData0 );
int iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
int iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 );
return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
}
/**Function*************************************************************
@ -597,7 +597,7 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->fAddStrash = fAddStrash;
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;

View File

@ -20,8 +20,8 @@
#include "gia.h"
#include "giaAig.h"
#include "aig.h"
#include "dar.h"
#include "src/aig/aig/aig.h"
#include "src/opt/dar/dar.h"
ABC_NAMESPACE_IMPL_START
@ -332,7 +332,7 @@ Gia_Man_t * Hcd_ManChoiceMiter( Vec_Ptr_t * vGias )
}
// start the new manager
pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
pNew->pName = Gia_UtilStrsav( pGia0->pName );
pNew->pName = Abc_UtilStrsav( pGia0->pName );
// create new CIs and assign them to the old manager CIs
for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
{
@ -457,7 +457,7 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
{
if ( Gia_ObjIsConst0(pRepr) )
{
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
Hcd_ManEquivToChoices_rec( pNew, p, pRepr );
@ -465,20 +465,20 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
{
assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
return;
}
if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
return;
assert( pRepr->Value < pObj->Value );
pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
{
assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
if ( !Hcd_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
@ -487,7 +487,7 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
Hcd_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
}
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
@ -563,7 +563,7 @@ Gia_Man_t * Hcd_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )

View File

@ -19,9 +19,9 @@
***********************************************************************/
#include "gia.h"
#include "aig.h"
#include "if.h"
#include "dar.h"
#include "src/aig/aig/aig.h"
#include "src/map/if/if.h"
#include "src/opt/dar/dar.h"
ABC_NAMESPACE_IMPL_START
@ -306,11 +306,11 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
{
nLuts++;
nFanins += Gia_ObjLutSize(p, i);
nLutSize = ABC_MAX( nLutSize, Gia_ObjLutSize(p, i) );
nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p, i) );
Gia_LutForEachFanin( p, i, iFan, k )
pLevels[i] = ABC_MAX( pLevels[i], pLevels[iFan] );
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[iFan] );
pLevels[i]++;
LevelMax = ABC_MAX( LevelMax, pLevels[i] );
LevelMax = Abc_MaxInt( LevelMax, pLevels[i] );
}
ABC_FREE( pLevels );
Abc_Print( 1, "mapping (K=%d) : ", nLutSize );
@ -355,7 +355,7 @@ int Gia_ManLutSizeMax( Gia_Man_t * p )
{
int i, nSizeMax = -1;
Gia_ManForEachLut( p, i )
nSizeMax = ABC_MAX( nSizeMax, Gia_ObjLutSize(p, i) );
nSizeMax = Abc_MaxInt( nSizeMax, Gia_ObjLutSize(p, i) );
return nSizeMax;
}

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "tim.h"
#include "src/misc/tim/tim.h"
ABC_NAMESPACE_IMPL_START
@ -262,7 +262,8 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
Vec_Int_t * vAbs = p->vObjClasses;
int i, k, Entry, iStart, iStop, nFrames;
int nObjBits, nObjMask, iObj, iFrame, nWords;
unsigned * pInfo, * pCountAll, * pCountUni;
unsigned * pInfo;
int * pCountAll, * pCountUni;
if ( vAbs == NULL )
return;
nFrames = Vec_IntEntry( vAbs, 0 );
@ -270,10 +271,10 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
pCountAll = ABC_ALLOC( int, nFrames + 1 );
pCountUni = ABC_ALLOC( int, nFrames + 1 );
// start storage for seen objects
nWords = Gia_BitWordNum( nFrames );
nWords = Abc_BitWordNum( nFrames );
vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords );
// get the bitmasks
nObjBits = Gia_Base2Log( Gia_ManObjNum(p) );
nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
nObjMask = (1 << nObjBits) - 1;
assert( Gia_ManObjNum(p) <= nObjMask );
// print info about frames
@ -289,16 +290,16 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
iObj = (Entry & nObjMask);
iFrame = (Entry >> nObjBits);
pInfo = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj );
if ( Gia_InfoHasBit(pInfo, iFrame) == 0 )
if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
{
Gia_InfoSetBit( pInfo, iFrame );
Abc_InfoSetBit( pInfo, iFrame );
pCountUni[iFrame+1]++;
pCountUni[0]++;
}
pCountAll[iFrame+1]++;
pCountAll[0]++;
}
assert( pCountAll[0] == (unsigned)(iStop - iStart) );
assert( pCountAll[0] == (iStop - iStart) );
// printf( "%5d%5d ", pCountAll[0], pCountUni[0] );
printf( "%3d :", i );
printf( "%6d", pCountAll[0] );

View File

@ -100,8 +100,8 @@ void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, V
Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit );
// set binary values to nodes in the counter-example
Vec_IntForEachEntry( vCex, Entry, i )
// Sat_ObjSetXValue( Gia_ManObj(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
Sat_ObjSetXValue( Gia_ManCi(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
// Sat_ObjSetXValue( Gia_ManObj(p, Abc_Lit2Var(Entry)), Abc_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
Sat_ObjSetXValue( Gia_ManCi(p, Abc_Lit2Var(Entry)), Abc_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
// simulate
Gia_ManForEachObjVec( vVisit, p, pObj, i )
{

View File

@ -20,7 +20,7 @@
#include "gia.h"
#include "giaAig.h"
#include "saig.h"
#include "src/aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
@ -52,7 +52,7 @@ Gia_Man_t * Gia_ManDupIn2Ff( Gia_Man_t * p )
int i;
vPiOuts = Vec_IntAlloc( Gia_ManPiNum(p) );
pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * Gia_ManPiNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManDupFf2In( Gia_Man_t * p, int nFlopsOld )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachRo( p, pObj, i )

View File

@ -125,7 +125,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
int i;
// create the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
// create the true PIs
Gia_ManFillValue( p );
@ -135,7 +135,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
pObj->Value = Gia_ManAppendCi( pNew );
// create the registers
Vec_PtrForEachEntry( Gia_Obj_t *, vCut, pObj, i )
pObj->Value = Gia_LitNotCond( Gia_ManAppendCi(pNew), pObj->fPhase );
pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), pObj->fPhase );
// duplicate logic above the cut
Gia_ManForEachCo( p, pObj, i )
Gia_ManRetimeDup_rec( pNew, Gia_ObjFanin0(pObj) );
@ -156,7 +156,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
Vec_PtrForEachEntry( Gia_Obj_t *, vCut, pObj, i )
{
Gia_ManRetimeDup_rec( pNew, pObj );
Gia_ManAppendCo( pNew, Gia_LitNotCond( pObj->Value, pObj->fPhase ) );
Gia_ManAppendCo( pNew, Abc_LitNotCond( pObj->Value, pObj->fPhase ) );
}
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Vec_PtrSize(vCut) );

View File

@ -265,7 +265,7 @@ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int *
(*pnLeaves)++;
else
Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
return ABC_MAX( Level0, Level1 );
return Abc_MaxInt( Level0, Level1 );
}
/**Function*************************************************************

View File

@ -199,7 +199,7 @@ Gia_Man_t * Gia_ManReduceEquiv( Gia_Man_t * p, int fVerbose )
else if ( ~pMaps[iLit] ) // in this case, ID(pObj) > ID(pRepr)
pCi2Lit[Gia_ManPiNum(p)+i] = pMaps[iLit], Counter++;
else
pMaps[iLit] = Gia_Var2Lit( Gia_ObjId(p, pObjRo), 0 );
pMaps[iLit] = Abc_Var2Lit( Gia_ObjId(p, pObjRo), 0 );
}
/*
Gia_ManForEachCi( p, pObjRo, i )

View File

@ -19,8 +19,8 @@
***********************************************************************/
#include "gia.h"
#include "aig.h"
#include "dar.h"
#include "src/aig/aig/aig.h"
#include "src/opt/dar/dar.h"
ABC_NAMESPACE_IMPL_START
@ -75,7 +75,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
Gia_ManConst0(p)->Value = 0;
// start the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) );
Gia_ManForEachObj1( p, pObj, i )
@ -114,7 +114,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
else
{
pObj->Value = Dar_LibEvalBuild( pNew, vLeaves, 0xffff & *pTruth, fKeepLevel, vLeavesBest );
pObj->Value = Gia_LitNotCond( pObj->Value, Gia_ObjPhaseRealLit(pNew, pObj->Value) ^ pObj->fPhase );
pObj->Value = Abc_LitNotCond( pObj->Value, Gia_ObjPhaseRealLit(pNew, pObj->Value) ^ pObj->fPhase );
}
}
}

View File

@ -133,18 +133,18 @@ Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
{
if ( Count < nImpLimit )
continue;
pObj = Gia_ManObj( pGia, Gia_Lit2Var(Lit) );
if ( Gia_LitIsCompl(Lit) ) // const 0
pObj = Gia_ManObj( pGia, Abc_Lit2Var(Lit) );
if ( Abc_LitIsCompl(Lit) ) // const 0
{
// Ssm_ObjSetLogic0( pObj );
Vec_IntWriteEntry( vResult, Gia_Lit2Var(Lit), 0 );
Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 0 );
CounterPi0 += Gia_ObjIsPi(pGia, pObj);
Counter0++;
}
else
{
// Ssm_ObjSetLogic1( pObj );
Vec_IntWriteEntry( vResult, Gia_Lit2Var(Lit), 1 );
Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 1 );
CounterPi1 += Gia_ObjIsPi(pGia, pObj);
Counter1++;
}
@ -568,8 +568,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
continue;
for ( w = nWords-1; w >= 0; w-- )
pData[w] = Gia_ManRandom( 0 );
if ( Gia_InfoHasBit( pData, iPat ) )
Gia_InfoSetBit( p->pData, Counter + iPioId );
if ( Abc_InfoHasBit( pData, iPat ) )
Abc_InfoSetBit( p->pData, Counter + iPioId );
}
ABC_FREE( pData );
return p;

View File

@ -471,7 +471,7 @@ void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined )
int * pTable, nTableSize, i, k, Key;
if ( Vec_IntSize(vRefined) == 0 )
return;
nTableSize = Gia_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
nTableSize = Abc_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
@ -617,8 +617,8 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
{
for ( w = nWords-1; w >= 0; w-- )
pData[w] = Gia_ManRandom( 0 );
if ( Gia_InfoHasBit( pData, iPat ) )
Gia_InfoSetBit( p->pData, Counter + i );
if ( Abc_InfoHasBit( pData, iPat ) )
Abc_InfoSetBit( p->pData, Counter + i );
}
ABC_FREE( pData );
return p;

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "if.h"
#include "src/map/if/if.h"
ABC_NAMESPACE_IMPL_START
@ -597,7 +597,7 @@ void Gia_ManSpeedupObj( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_I
for ( i = 0; i < nCofs; i++ )
{
Gia_ManForEachObjVec( vLeaves, p, pTemp, k )
pTemp->Value = Gia_Var2Lit( Gia_ObjId(p, pTemp), 0 );
pTemp->Value = Abc_Var2Lit( Gia_ObjId(p, pTemp), 0 );
Gia_ManForEachObjVec( vTimes, p, pTemp, k )
pTemp->Value = ((i & (1<<k)) != 0);
Gia_ManForEachObjVec( vNodes, p, pTemp, k )
@ -611,7 +611,7 @@ void Gia_ManSpeedupObj( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_I
pCofs[i] = Gia_ManHashMux( pNew, Gia_ObjToLit(p,pTemp), pCofs[i+nSkip], pCofs[i] );
// create choice node (pObj is repr and ppCofs[0] is new)
iObj = Gia_ObjId( p, pObj );
iResult = Gia_Lit2Var( pCofs[0] );
iResult = Abc_Lit2Var( pCofs[0] );
if ( iResult <= iObj )
return;
Gia_ObjSetRepr( pNew, iResult, iObj );

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "gia.h"
#include "kit.h"
#include "src/bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "giaAig.h"
#include "main.h"
#include "src/base/main/main.h"
ABC_NAMESPACE_IMPL_START
@ -569,7 +569,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
{
printf( "Obj = %8d (%8d). F = %6d. ",
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront,
4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
4.0*Abc_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
@ -691,8 +691,8 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref
Aig_ManForEachObj( pAig, pObj, i )
{
// if ( Aig_ObjIsPo(pObj) )
// printf( "%d=%f\n", i, Aig_Int2Float( Vec_IntEntry(vSwitching, Gia_Lit2Var(pObj->iData)) ) );
Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vSwitching, Gia_Lit2Var(pObj->iData)) );
// printf( "%d=%f\n", i, Abc_Int2Float( Vec_IntEntry(vSwitching, Abc_Lit2Var(pObj->iData)) ) );
Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vSwitching, Abc_Lit2Var(pObj->iData)) );
}
// delete intermediate results
Vec_IntFree( vSwitching );

View File

@ -84,15 +84,15 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig )
p = ABC_CALLOC( Gia_ManTer_t, 1 );
p->pAig = Gia_ManFront( pAig );
p->nIters = 300;
p->pDataSim = ABC_ALLOC( unsigned, Gia_BitWordNum(2*p->pAig->nFront) );
p->pDataSimCis = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
p->pDataSimCos = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
p->pDataSim = ABC_ALLOC( unsigned, Abc_BitWordNum(2*p->pAig->nFront) );
p->pDataSimCis = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
p->pDataSimCos = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
// allocate storage for terminary states
p->nStateWords = Gia_BitWordNum( 2*Gia_ManRegNum(pAig) );
p->nStateWords = Abc_BitWordNum( 2*Gia_ManRegNum(pAig) );
p->vStates = Vec_PtrAlloc( 1000 );
p->pCount0 = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
p->pCountX = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
p->nBins = Gia_PrimeCudd( 500 );
p->nBins = Abc_PrimeCudd( 500 );
p->pBins = ABC_CALLOC( unsigned *, p->nBins );
p->vRetired = Vec_IntAlloc( 100 );
p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) );
@ -511,7 +511,7 @@ void Gia_ManTerAnalyze2( Vec_Ptr_t * vStates, int nRegs )
unsigned * pTemp, * pStates = (unsigned *)Vec_PtrPop( vStates );
int i, w, nZeros, nConsts, nStateWords;
// detect constant zero registers
nStateWords = Gia_BitWordNum( 2*nRegs );
nStateWords = Abc_BitWordNum( 2*nRegs );
memset( pStates, 0, sizeof(int) * nStateWords );
Vec_PtrForEachEntry( unsigned *, vStates, pTemp, i )
for ( w = 0; w < nStateWords; w++ )
@ -579,7 +579,7 @@ Vec_Ptr_t * Gia_ManTerTranspose( Gia_ManTer_t * p )
unsigned * pState, * pFlop;
int i, k, nFlopWords;
vFlops = Vec_PtrAlloc( 100 );
nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
nFlopWords = Abc_BitWordNum( 2*Vec_PtrSize(p->vStates) );
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
if ( p->pCount0[i] == Vec_PtrSize(p->vStates) )
@ -634,7 +634,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
Gia_Obj_t * pObj;
Vec_Int_t * vMapKtoI;
int i, iRepr, nFlopWords, Counter0 = 0, CounterE = 0;
nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
nFlopWords = Abc_BitWordNum( 2*Vec_PtrSize(p->vStates) );
p->vFlops = Gia_ManTerTranspose( p );
pCi2Lit = ABC_FALLOC( int, Gia_ManCiNum(p->pAig) );
vMapKtoI = Vec_IntAlloc( 100 );
@ -648,7 +648,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
if ( iRepr < 0 )
continue;
pObj = Gia_ManCi( p->pAig, Gia_ManPiNum(p->pAig)+Vec_IntEntry(vMapKtoI, iRepr) );
pCi2Lit[Gia_ManPiNum(p->pAig)+i] = Gia_Var2Lit( Gia_ObjId( p->pAig, pObj ), 0 );
pCi2Lit[Gia_ManPiNum(p->pAig)+i] = Abc_Var2Lit( Gia_ObjId( p->pAig, pObj ), 0 );
CounterE++;
}
Vec_IntFree( vMapKtoI );
@ -684,8 +684,8 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20),
4.0*Gia_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
4.0*Abc_BitWordNum(2 * p->pAig->nFront)/(1<<20),
4.0*Abc_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
ABC_PRT( "Time", clock() - clk );
}
// perform simulation

View File

@ -80,42 +80,6 @@ void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int
pInfo[w] = Gia_ManRandom(0);
}
/**Function********************************************************************
Synopsis [Returns the next prime >= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Gia_PrimeCudd( unsigned int p )
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
/**Function*************************************************************
@ -483,7 +447,7 @@ int Gia_ManLevelNum( Gia_Man_t * p )
else if ( Gia_ObjIsCo(pObj) )
{
Gia_ObjSetCoLevel( p, pObj );
p->nLevels = ABC_MAX( p->nLevels, Gia_ObjLevel(p, pObj) );
p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
}
else
Gia_ObjSetLevel( p, pObj, 0 );
@ -1150,11 +1114,11 @@ int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
int RetValue, i, k, iBit = 0;
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
@ -1194,12 +1158,12 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
assert( Gia_ManPiNum(pAig) == p->nPis );
Gia_ManCleanMark0(pAig);
// Gia_ManForEachRo( pAig, pObj, i )
// pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));

View File

@ -19,7 +19,7 @@
***********************************************************************/
#include "hop.h"
#include "st.h"
#include "misc/st/st.h"
ABC_NAMESPACE_IMPL_START

View File

@ -18,8 +18,8 @@
***********************************************************************/
#ifndef __CUDD2_H__
#define __CUDD2_H__
#ifndef ABC__aig__hop__cudd2_h
#define ABC__aig__hop__cudd2_h
// HA: Added for printing messages

View File

@ -18,8 +18,8 @@
***********************************************************************/
#ifndef __HOP_H__
#define __HOP_H__
#ifndef ABC__aig__hop__hop_h
#define ABC__aig__hop__hop_h
////////////////////////////////////////////////////////////////////////
@ -32,7 +32,7 @@
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "src/misc/vec/vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -186,7 +186,7 @@ static inline Hop_Obj_t * Hop_ObjChild1( Hop_Obj_t * pObj ) { return pObj-
static inline Hop_Obj_t * Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL; }
static inline Hop_Obj_t * Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL; }
static inline int Hop_ObjLevel( Hop_Obj_t * pObj ) { return pObj->nRefs; }
static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + ABC_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); }
static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + Abc_MaxInt(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); }
static inline int Hop_ObjPhaseCompl( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
static inline void Hop_ObjClean( Hop_Obj_t * pObj ) { memset( pObj, 0, sizeof(Hop_Obj_t) ); }
static inline int Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin )

View File

@ -128,13 +128,13 @@ int Hop_ManCountLevels( Hop_Man_t * p )
{
Level0 = (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData;
Level1 = (int)(ABC_PTRUINT_T)Hop_ObjFanin1(pObj)->pData;
pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + ABC_MAX(Level0, Level1));
pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + Abc_MaxInt(Level0, Level1));
}
Vec_PtrFree( vNodes );
// get levels of the POs
LevelsMax = 0;
Hop_ManForEachPo( p, pObj, i )
LevelsMax = ABC_MAX( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
LevelsMax = Abc_MaxInt( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
return LevelsMax;
}

View File

@ -52,7 +52,6 @@ static Hop_Obj_t ** Hop_TableFind( Hop_Man_t * p, Hop_Obj_t * pObj )
}
static void Hop_TableResize( Hop_Man_t * p );
static unsigned int Cudd_PrimeAig( unsigned int p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -174,7 +173,7 @@ clk = clock();
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
// get the new table
p->nTableSize = Cudd_PrimeAig( 2 * Hop_ManNodeNum(p) );
p->nTableSize = Abc_PrimeCudd( 2 * Hop_ManNodeNum(p) );
p->pTable = ABC_ALLOC( Hop_Obj_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize );
// rehash the entries from the old table
@ -223,41 +222,6 @@ void Hop_TableProfile( Hop_Man_t * p )
}
}
/**Function********************************************************************
Synopsis [Returns the next prime &gt;= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Cudd_PrimeAig( unsigned int p)
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1,11 +0,0 @@
SRC += src/aig/int/intCheck.c \
src/aig/int/intContain.c \
src/aig/int/intCore.c \
src/aig/int/intCtrex.c \
src/aig/int/intDup.c \
src/aig/int/intFrames.c \
src/aig/int/intInter.c \
src/aig/int/intM114.c \
src/aig/int/intM114p.c \
src/aig/int/intMan.c \
src/aig/int/intUtil.c

View File

@ -18,8 +18,8 @@
***********************************************************************/
#ifndef __IOA_H__
#define __IOA_H__
#ifndef ABC__aig__ioa__ioa_h
#define ABC__aig__ioa__ioa_h
////////////////////////////////////////////////////////////////////////
@ -32,9 +32,9 @@
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "src/misc/vec/vec.h"
//#include "bar.h"
#include "aig.h"
#include "src/aig/aig/aig.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///

View File

@ -392,7 +392,7 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
pCur++;
// read model name
ABC_FREE( pNew->pName );
pNew->pName = Aig_UtilStrsav( pCur );
pNew->pName = Abc_UtilStrsav( pCur );
}
}
@ -447,7 +447,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
if ( pNew )
{
pName = Ioa_FileNameGeneric( pFileName );
pNew->pName = Aig_UtilStrsav( pName );
pNew->pName = Abc_UtilStrsav( pName );
// pNew->pSpec = Ioa_UtilStrsav( pFileName );
ABC_FREE( pName );
}

View File

@ -73,7 +73,7 @@ int Ioa_FileSize( char * pFileName )
char * Ioa_FileNameGeneric( char * FileName )
{
char * pDot, * pRes;
pRes = Aig_UtilStrsav( FileName );
pRes = Abc_UtilStrsav( FileName );
if ( (pDot = strrchr( pRes, '.' )) )
*pDot = 0;
return pRes;

View File

@ -18,15 +18,15 @@
***********************************************************************/
#ifndef __ATTR_H__
#define __ATTR_H__
#ifndef ABC__aig__ivy__attr_h
#define ABC__aig__ivy__attr_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "extra.h"
#include "misc/extra/extra.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///

View File

@ -18,8 +18,8 @@
***********************************************************************/
#ifndef __IVY_H__
#define __IVY_H__
#ifndef ABC__aig__ivy__ivy_h
#define ABC__aig__ivy__ivy_h
////////////////////////////////////////////////////////////////////////
@ -27,8 +27,8 @@
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include "extra.h"
#include "vec.h"
#include "src/misc/extra/extra.h"
#include "src/misc/vec/vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///

View File

@ -18,8 +18,10 @@
***********************************************************************/
#include "satSolver.h"
#include "extra.h"
#include <math.h>
#include "src/sat/bsat/satSolver.h"
#include "src/misc/extra/extra.h"
#include "ivy.h"
ABC_NAMESPACE_IMPL_START
@ -2649,7 +2651,7 @@ p->timeTrav += clock() - clk;
ABC_NAMESPACE_IMPL_END
#include "cuddInt.h"
#include "src/bdd/cudd/cuddInt.h"
ABC_NAMESPACE_IMPL_START
@ -2807,7 +2809,7 @@ int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
ABC_NAMESPACE_IMPL_END
#include "aig.h"
#include "src/aig/aig/aig.h"
ABC_NAMESPACE_IMPL_START

View File

@ -19,8 +19,8 @@
***********************************************************************/
#include "ivy.h"
#include "deco.h"
#include "rwt.h"
#include "src/bool/deco/deco.h"
#include "src/opt/rwt/rwt.h"
ABC_NAMESPACE_IMPL_START

View File

@ -19,8 +19,8 @@
***********************************************************************/
#include "ivy.h"
#include "deco.h"
#include "rwt.h"
#include "src/bool/deco/deco.h"
#include "src/opt/rwt/rwt.h"
ABC_NAMESPACE_IMPL_START

View File

@ -212,7 +212,7 @@ clk = clock();
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
// get the new table
p->nTableSize = Cudd_PrimeAig( 5 * Ivy_ManHashObjNum(p) );
p->nTableSize = Abc_PrimeCudd( 5 * Ivy_ManHashObjNum(p) );
p->pTable = ABC_ALLOC( int, p->nTableSize );
memset( p->pTable, 0, sizeof(int) * p->nTableSize );
// rehash the entries from the old table
@ -261,41 +261,6 @@ void Ivy_TableProfile( Ivy_Man_t * p )
}
}
/**Function********************************************************************
Synopsis [Returns the next prime &gt;= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Cudd_PrimeAig( unsigned int p)
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

Some files were not shown because too many files have changed in this diff Show More