summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaAiger.c8
-rw-r--r--src/aig/gia/giaMini.c16
-rw-r--r--src/aig/gia/giaPat2.c2
-rw-r--r--src/aig/gia/giaStr.c4
-rw-r--r--src/aig/miniaig/abcOper.h6
-rw-r--r--src/aig/miniaig/ndr.h53
-rw-r--r--src/base/main/abcapis.h1
-rw-r--r--src/base/wlc/wlcBlast.c2
-rw-r--r--src/base/wlc/wlcNdr.c9
-rw-r--r--src/misc/vec/vecInt.h64
-rw-r--r--src/proof/acec/acecFadds.c30
11 files changed, 157 insertions, 38 deletions
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 1bb70612..aafe311b 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1702,8 +1702,8 @@ int * Aiger_Read( char * pFileName, int * pnObjs, int * pnIns, int * pnLats, int
int uLit = 2*(1 + nIns + nLats + i);
int uLit1 = uLit - Aiger_ReadUnsigned( pFile );
int uLit0 = uLit1 - Aiger_ReadUnsigned( pFile );
- pObjs[2*(1+nIns+i)+0] = uLit0;
- pObjs[2*(1+nIns+i)+1] = uLit1;
+ pObjs[2*(1+nIns+nLats+i)+0] = uLit0;
+ pObjs[2*(1+nIns+nLats+i)+1] = uLit1;
}
fclose( pFile );
if ( pnObjs ) *pnObjs = nObjs;
@@ -1729,8 +1729,8 @@ void Aiger_Write( char * pFileName, int * pObjs, int nObjs, int nIns, int nLats,
for ( i = 0; i < nAnds; i++ )
{
int uLit = 2*(1 + nIns + nLats + i);
- int uLit0 = pObjs[2*(1+nIns+i)+0];
- int uLit1 = pObjs[2*(1+nIns+i)+1];
+ int uLit0 = pObjs[2*(1+nIns+nLats+i)+0];
+ int uLit1 = pObjs[2*(1+nIns+nLats+i)+1];
Aiger_WriteUnsigned( pFile, uLit - uLit1 );
Aiger_WriteUnsigned( pFile, uLit1 - uLit0 );
}
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index ad7ed197..6cc528f2 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -681,6 +681,22 @@ int * Abc_FrameReadMiniLutSwitching( Abc_Frame_t * pAbc )
Vec_IntFree( vSwitching );
return pRes;
}
+int * Abc_FrameReadMiniLutSwitchingPo( Abc_Frame_t * pAbc )
+{
+ Vec_Int_t * vSwitching;
+ int i, iObj, * pRes = NULL;
+ if ( pAbc->pGiaMiniAig == NULL )
+ {
+ printf( "GIA derived from MiniAIG is not available.\n" );
+ return NULL;
+ }
+ vSwitching = Gia_ManComputeSwitchProbs( pAbc->pGiaMiniAig, 48, 16, 0 );
+ pRes = ABC_CALLOC( int, Gia_ManCoNum(pAbc->pGiaMiniAig) );
+ Gia_ManForEachCoDriverId( pAbc->pGiaMiniAig, iObj, i )
+ pRes[i] = (int)(10000*Vec_FltEntry( (Vec_Flt_t *)vSwitching, iObj ));
+ Vec_IntFree( vSwitching );
+ return pRes;
+}
/**Function*************************************************************
diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c
index 094bdee1..f14ce34a 100644
--- a/src/aig/gia/giaPat2.c
+++ b/src/aig/gia/giaPat2.c
@@ -1242,6 +1242,8 @@ Vec_Wrd_t * Min_ManRemapSims( int nInputs, Vec_Int_t * vMap, Vec_Wrd_t * vSimsPi
{
int i, iObj, nWords = Vec_WrdSize(vSimsPi)/Vec_IntSize(vMap);
Vec_Wrd_t * vSimsNew = Vec_WrdStart( 2 * nInputs * nWords );
+ //Vec_Wrd_t * vSimsNew = Vec_WrdStartRandom( nInputs * nWords );
+ //Vec_WrdFillExtra( vSimsNew, 2 * nInputs * nWords, 0 );
assert( Vec_WrdSize(vSimsPi)%Vec_IntSize(vMap) == 0 );
Vec_WrdShrink( vSimsNew, Vec_WrdSize(vSimsNew)/2 );
Vec_IntForEachEntry( vMap, iObj, i )
diff --git a/src/aig/gia/giaStr.c b/src/aig/gia/giaStr.c
index 2233d0fc..a87662a8 100644
--- a/src/aig/gia/giaStr.c
+++ b/src/aig/gia/giaStr.c
@@ -736,7 +736,7 @@ Str_Ntk_t * Str_ManNormalizeInt( Gia_Man_t * p, Vec_Wec_t * vGroups, Vec_Int_t *
if ( p->vStore == NULL )
p->vStore = Vec_IntAlloc( STR_SUPER );
Gia_ManFillValue( p );
- pNtk = Str_NtkCreate( Gia_ManObjNum(p), 1 + Gia_ManCoNum(p) + 2 * Gia_ManAndNum(p) + Gia_ManMuxNum(p) );
+ pNtk = Str_NtkCreate( Gia_ManObjNum(p) + 10000, 1 + Gia_ManCoNum(p) + 2 * Gia_ManAndNum(p) + Gia_ManMuxNum(p) + 10000 );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@@ -749,7 +749,7 @@ Str_Ntk_t * Str_ManNormalizeInt( Gia_Man_t * p, Vec_Wec_t * vGroups, Vec_Int_t *
pObj->Value = Str_ObjCreate( pNtk, STR_PO, 1, &iFanin );
}
}
- assert( pNtk->nObjs <= Gia_ManObjNum(p) );
+ //assert( pNtk->nObjs <= Gia_ManObjNum(p) );
return pNtk;
}
Str_Ntk_t * Str_ManNormalize( Gia_Man_t * p )
diff --git a/src/aig/miniaig/abcOper.h b/src/aig/miniaig/abcOper.h
index 881810fd..c3d6e176 100644
--- a/src/aig/miniaig/abcOper.h
+++ b/src/aig/miniaig/abcOper.h
@@ -29,7 +29,9 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
+#ifndef _YOSYS_
ABC_NAMESPACE_HEADER_START
+#endif
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -264,9 +266,9 @@ static inline const char * Abc_OperNameSimple( int Type )
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-
+#ifndef _YOSYS_
ABC_NAMESPACE_HEADER_END
-
+#endif
#endif
diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h
index 91663616..68c2779c 100644
--- a/src/aig/miniaig/ndr.h
+++ b/src/aig/miniaig/ndr.h
@@ -33,7 +33,9 @@
#include "abcOper.h"
+#ifndef _YOSYS_
ABC_NAMESPACE_HEADER_START
+#endif
#ifdef _WIN32
#define inline __inline
@@ -215,8 +217,9 @@ static inline void Ndr_DataPushString( Ndr_Data_t * p, int ObjType, int Type, ch
return;
if ( ObjType == ABC_OPER_LUT )
{
- word Truth = (word)pFunc;
- Ndr_DataPushArray( p, Type, 2, (int *)&Truth );
+ //word Truth = (word)pFunc;
+ //Ndr_DataPushArray( p, Type, 2, (int *)&Truth );
+ Ndr_DataPushArray( p, Type, 2, (int *)&pFunc );
}
else
{
@@ -662,7 +665,7 @@ static inline void Ndr_ModuleTest()
// array of fanins of node s
int Fanins[2] = { NameIdA, NameIdC };
// map name IDs into char strings
- char * ppNames[5] = { NULL, "add10", "a", "s", "const10" };
+ //char * ppNames[5] = { NULL, "add10", "a", "s", "const10" };
// create a new module
void * pDesign = Ndr_Create( 1 );
@@ -671,13 +674,13 @@ static inline void Ndr_ModuleTest()
// add objects to the modele
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CI, 0, 3, 0, 0, 0, NULL, 1, &NameIdA, NULL ); // no fanins
- Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST, 0, 3, 0, 0, 0, NULL, 1, &NameIdC, "4'b1010" ); // no fanins
+ Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST, 0, 3, 0, 0, 0, NULL, 1, &NameIdC, (char*)"4'b1010" ); // no fanins
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_ARI_ADD, 0, 3, 0, 0, 2, Fanins, 1, &NameIdS, NULL ); // fanins are a and const10
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 3, 0, 0, 1, &NameIdS, 0, NULL, NULL ); // fanin is a
// write Verilog for verification
- Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
- Ndr_Write( "add4.ndr", pDesign );
+ //Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
+ Ndr_Write( (char*)"add4.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -706,6 +709,7 @@ static inline void Ndr_ModuleTest()
static inline void Ndr_ModuleTestAdder()
{
+/*
// map name IDs into char strings
char * ppNames[20] = { NULL,
"a", "b", "s", "co", // 1, 2, 3, 4
@@ -713,6 +717,7 @@ static inline void Ndr_ModuleTestAdder()
"r0", "s0", "rco", // 9, 10, 11
"r1", "s1", "add8" // 12, 13, 14
};
+*/
// fanins
int FaninA = 1;
int FaninB = 2;
@@ -764,8 +769,8 @@ static inline void Ndr_ModuleTestAdder()
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 0, 0, 0, 1, &FaninCO, 0, NULL, NULL );
// write Verilog for verification
- Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
- Ndr_Write( "add8.ndr", pDesign );
+ //Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
+ Ndr_Write( (char*)"add8.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -792,6 +797,7 @@ static inline void Ndr_ModuleTestAdder()
static inline void Ndr_ModuleTestHierarchy()
{
+/*
// map name IDs into char strings
char * ppNames[20] = { NULL,
"mux21w", "mux41w", // 1, 2
@@ -801,6 +807,7 @@ static inline void Ndr_ModuleTestHierarchy()
"t0", "t1", // 12, 13
"i0", "i1", "i2" // 14, 15, 16
};
+*/
// fanins
int FaninSel = 3;
int FaninSel0 = 10;
@@ -850,8 +857,8 @@ static inline void Ndr_ModuleTestHierarchy()
Ndr_AddObject( pDesign, Module41, ABC_OPER_CO, 0, 3, 0, 0, 1, &FaninOut, 0, NULL, NULL );
// write Verilog for verification
- Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
- Ndr_Write( "mux41w.ndr", pDesign );
+ //Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
+ Ndr_Write( (char*)"mux41w.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -879,6 +886,7 @@ static inline void Ndr_ModuleTestHierarchy()
static inline void Ndr_ModuleTestMemory()
{
+/*
// map name IDs into char strings
char * ppNames[20] = { NULL,
"clk", "raddr", "waddr", "data", "mem_init", "out", // 1, 2, 3, 4, 5, 6
@@ -888,6 +896,7 @@ static inline void Ndr_ModuleTestMemory()
"i_read1", "i_read2", // 15, 16
"i_write1", "i_write2", "memtest" // 17, 18, 19
};
+*/
// inputs
int NameIdClk = 1;
int NameIdRaddr = 2;
@@ -939,8 +948,8 @@ static inline void Ndr_ModuleTestMemory()
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_COMP_NOTEQU, 0, 0, 0, 0, 2, FaninsComp, 1, &NameIdComp, NULL );
// write Verilog for verification
- Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
- Ndr_Write( "memtest.ndr", pDesign );
+ //Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
+ Ndr_Write( (char*)"memtest.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -954,7 +963,7 @@ static inline void Ndr_ModuleTestMemory()
static inline void Ndr_ModuleTestFlop()
{
// map name IDs into char strings
- char * ppNames[12] = { NULL, "flop", "data", "clk", "reset", "set", "enable", "async", "sre", "init", "q" };
+ //char * ppNames[12] = { NULL, "flop", "data", "clk", "reset", "set", "enable", "async", "sre", "init", "q" };
// name IDs
int NameIdData = 2;
int NameIdClk = 3;
@@ -988,8 +997,8 @@ static inline void Ndr_ModuleTestFlop()
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 3, 0, 0, 1, &NameIdQ, 0, NULL, NULL );
// write Verilog for verification
- Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
- Ndr_Write( "flop.ndr", pDesign );
+ //Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
+ Ndr_Write( (char*)"flop.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -1043,7 +1052,7 @@ static inline void Ndr_ModuleTestSelSel()
// write Verilog for verification
//Ndr_WriteVerilog( NULL, pDesign, ppNames, 0 );
- Ndr_Write( "sel.ndr", pDesign );
+ Ndr_Write( (char*)"sel.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -1076,7 +1085,7 @@ static inline void Ndr_ModuleTestDec()
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_SEL_DEC, 0, 3, 0, 0, 1, &NameIdIn, 1, &NameIdOut, NULL );
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 3, 0, 0, 1, &NameIdOut, 0, NULL, NULL );
- Ndr_Write( "dec.ndr", pDesign );
+ Ndr_Write( (char*)"dec.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -1112,7 +1121,7 @@ static inline void Ndr_ModuleTestAddSub()
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_ARI_ADDSUB, 0, 3, 0, 0, 4, Fanins, 1, &NameIdOut, NULL );
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 3, 0, 0, 1, &NameIdOut, 0, NULL, NULL );
- Ndr_Write( "addsub.ndr", pDesign );
+ Ndr_Write( (char*)"addsub.ndr", pDesign );
Ndr_Delete( pDesign );
}
@@ -1136,16 +1145,20 @@ static inline void Ndr_ModuleTestLut()
int ModuleID = Ndr_AddModule( pDesign, 1 );
+ unsigned pTruth[2] = { 0x88888888, 0x88888888 };
+
// add objects to the modele
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CI, 0, 1, 0, 0, 0, NULL, 1, &NameIdIn, NULL );
- Ndr_AddObject( pDesign, ModuleID, ABC_OPER_LUT, 0, 0, 0, 0, 1, &NameIdIn, 1, &NameIdOut, (char *)(ABC_CONST(0x8)) );
+ Ndr_AddObject( pDesign, ModuleID, ABC_OPER_LUT, 0, 0, 0, 0, 1, &NameIdIn, 1, &NameIdOut, (char *)pTruth );
Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 0, 0, 0, 1, &NameIdOut, 0, NULL, NULL );
- Ndr_Write( "lut_test.ndr", pDesign );
+ Ndr_Write( (char*)"lut_test.ndr", pDesign );
Ndr_Delete( pDesign );
}
+#ifndef _YOSYS_
ABC_NAMESPACE_HEADER_END
+#endif
#endif
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
index 1bf52a89..d34306ba 100644
--- a/src/base/main/abcapis.h
+++ b/src/base/main/abcapis.h
@@ -82,6 +82,7 @@ extern ABC_DLL void Abc_FrameGiaInputMiniLut2( Abc_Frame_t * pAbc, void * pMin
extern ABC_DLL void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc );
extern ABC_DLL char * Abc_FrameGiaOutputMiniLutAttr( Abc_Frame_t * pAbc, void * pMiniLut );
extern ABC_DLL int * Abc_FrameReadMiniLutSwitching( Abc_Frame_t * pAbc );
+extern ABC_DLL int * Abc_FrameReadMiniLutSwitchingPo( Abc_Frame_t * pAbc );
// procedures to input/output NDR data-structure
extern ABC_DLL void Abc_FrameInputNdr( Abc_Frame_t * pAbc, void * pData );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 4ec8d7ff..6e910cd8 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -2110,7 +2110,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
// complement flop inputs whose init state is 1
for ( i = 0; i < nFf2Regs; i++ )
Gia_ManAppendCo( pNew, Gia_ManAppendCi(pNew) );
- //Gia_ManSetRegNum( pNew, nFf2Regs );
+ Gia_ManSetRegNum( pNew, nFf2Regs );
}
else
{
diff --git a/src/base/wlc/wlcNdr.c b/src/base/wlc/wlcNdr.c
index b06d9357..d401281a 100644
--- a/src/base/wlc/wlcNdr.c
+++ b/src/base/wlc/wlcNdr.c
@@ -368,7 +368,7 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
Ndr_Data_t * p = (Ndr_Data_t *)pData;
Wlc_Obj_t * pObj; Vec_Int_t * vName2Obj, * vFanins = Vec_IntAlloc( 100 );
int Mod = 2, i, k, Obj, * pArray, nDigits, fFound, NameId, NameIdMax;
- Vec_Wrd_t * vTruths = NULL;
+ Vec_Wrd_t * vTruths = NULL; int nTruths[2] = {0};
Wlc_Ntk_t * pTemp, * pNtk = Wlc_NtkAlloc( "top", Ndr_DataObjNum(p, Mod)+1 );
Wlc_NtkCheckIntegrity( pData );
Vec_IntClear( &pNtk->vFfs );
@@ -415,11 +415,14 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
Vec_IntPush( &pNtk->vFfs2, iObj );
if ( Type == ABC_OPER_LUT )
{
+ word * pTruth;
if ( vTruths == NULL )
vTruths = Vec_WrdStart( 1000 );
if ( NameId >= Vec_WrdSize(vTruths) )
Vec_WrdFillExtra( vTruths, 2*NameId, 0 );
- Vec_WrdWriteEntry( vTruths, NameId, *((word *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION)) );
+ pTruth = (word *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION);
+ Vec_WrdWriteEntry( vTruths, NameId, pTruth ? *pTruth : 0 );
+ nTruths[ pTruth != NULL ]++;
}
if ( Type == ABC_OPER_SLICE )
Vec_IntPushTwo( vFanins, End, Beg );
@@ -437,6 +440,8 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
Wlc_ObjFanin1(pNtk, pObj)->Signed = 1;
}
}
+ if ( nTruths[0] )
+ printf( "Warning! The number of LUTs without function is %d (out of %d).\n", nTruths[0], nTruths[0]+nTruths[1] );
// mark primary outputs
Ndr_ModForEachPo( p, Mod, Obj )
{
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 89a9096a..c15369d2 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1934,6 +1934,70 @@ static inline int Vec_IntTwoRemove( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
Synopsis [Returns the result of merging the two vectors.]
+ Description [Keeps only those entries of vArr1, which are in vArr2.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_IntTwoMerge1( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
+{
+ int * pBeg = vArr1->pArray;
+ int * pBeg1 = vArr1->pArray;
+ int * pBeg2 = vArr2->pArray;
+ int * pEnd1 = vArr1->pArray + vArr1->nSize;
+ int * pEnd2 = vArr2->pArray + vArr2->nSize;
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( *pBeg1 == *pBeg2 )
+ *pBeg++ = *pBeg1++, pBeg2++;
+ else if ( *pBeg1 < *pBeg2 )
+ pBeg1++;
+ else
+ pBeg2++;
+ }
+ assert( vArr1->nSize >= pBeg - vArr1->pArray );
+ vArr1->nSize = pBeg - vArr1->pArray;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the result of subtracting for two vectors.]
+
+ Description [Keeps only those entries of vArr1, which are not in vArr2.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_IntTwoRemove1( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
+{
+ int * pBeg = vArr1->pArray;
+ int * pBeg1 = vArr1->pArray;
+ int * pBeg2 = vArr2->pArray;
+ int * pEnd1 = vArr1->pArray + vArr1->nSize;
+ int * pEnd2 = vArr2->pArray + vArr2->nSize;
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( *pBeg1 == *pBeg2 )
+ pBeg1++, pBeg2++;
+ else if ( *pBeg1 < *pBeg2 )
+ *pBeg++ = *pBeg1++;
+ else
+ pBeg2++;
+ }
+ while ( pBeg1 < pEnd1 )
+ *pBeg++ = *pBeg1++;
+ assert( vArr1->nSize >= pBeg - vArr1->pArray );
+ vArr1->nSize = pBeg - vArr1->pArray;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the result of merging the two vectors.]
+
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c
index d55eefe2..a2bdcfbe 100644
--- a/src/proof/acec/acecFadds.c
+++ b/src/proof/acec/acecFadds.c
@@ -314,16 +314,21 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
if ( Type == 0 )
continue;
vTemp = Type == 1 ? vCutsXor : vCutsMaj;
- if ( fVerbose )
- printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
- for ( c = 1; c <= pCut[0]; c++ )
+ if ( 0 && Type == 2 )
{
+ fVerbose = 1;
+ if ( fVerbose )
+ printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
+ for ( c = 1; c <= pCut[0]; c++ )
+ {
+ if ( fVerbose )
+ printf( " %d", pCut[c] );
+ Vec_IntPush( vTemp, pCut[c] );
+ }
if ( fVerbose )
- printf( " %d", pCut[c] );
- Vec_IntPush( vTemp, pCut[c] );
+ printf( " )\n" );
+ fVerbose = 0;
}
- if ( fVerbose )
- printf( " )\n" );
Vec_IntPush( vTemp, iObj );
}
}
@@ -450,6 +455,16 @@ Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** p
Vec_IntFree( vCutsMaj );
return vFadds;
}
+void Gia_ManDetectFullAdders2( Gia_Man_t * p, int fVerbose )
+{
+ Vec_Int_t * vCutsXor2, * vCutsXor, * vCutsMaj;
+ Dtc_ManComputeCuts( p, &vCutsXor2, &vCutsXor, &vCutsMaj, fVerbose );
+ if ( fVerbose )
+ printf( "XOR3 cuts = %d. MAJ cuts = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4 );
+ Vec_IntFree( vCutsXor2 );
+ Vec_IntFree( vCutsXor );
+ Vec_IntFree( vCutsMaj );
+}
/**Function*************************************************************
@@ -1238,6 +1253,7 @@ Gia_Man_t * Gia_ManDupWithArtificialBoxes( Gia_Man_t * p, int DelayC, int nPathM
return pNew;
}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 10:40:57 +0000