summaryrefslogtreecommitdiffstats
path: root/src/aig/cnf
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cnf')
-rw-r--r--src/aig/cnf/cnf.h21
-rw-r--r--src/aig/cnf/cnfCore.c9
-rw-r--r--src/aig/cnf/cnfCut.c17
-rw-r--r--src/aig/cnf/cnfData.c4
-rw-r--r--src/aig/cnf/cnfMan.c8
-rw-r--r--src/aig/cnf/cnfMap.c54
-rw-r--r--src/aig/cnf/cnfPost.c48
-rw-r--r--src/aig/cnf/cnfUtil.c41
-rw-r--r--src/aig/cnf/cnfWrite.c30
9 files changed, 124 insertions, 108 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 8c27b62d..c758867c 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -36,7 +36,8 @@ extern "C" {
#include <time.h>
#include "vec.h"
-#include "dar.h"
+#include "aig.h"
+#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -53,7 +54,7 @@ typedef struct Cnf_Cut_t_ Cnf_Cut_t;
// the CNF asserting outputs of AIG to be 1
struct Cnf_Dat_t_
{
- Dar_Man_t * pMan; // the AIG manager, for which CNF is computed
+ Aig_Man_t * pMan; // the AIG manager, for which CNF is computed
int nVars; // the number of variables
int nLiterals; // the number of CNF literals
int nClauses; // the number of CNF clauses
@@ -74,11 +75,11 @@ struct Cnf_Cut_t_
// the CNF computation manager
struct Cnf_Man_t_
{
- Dar_Man_t * pManAig; // the underlying AIG manager
+ Aig_Man_t * pManAig; // the underlying AIG manager
char * pSopSizes; // sizes of SOPs for 4-variable functions
char ** pSops; // the SOPs for 4-variable functions
int aArea; // the area of the mapping
- Dar_MmFlex_t * pMemCuts; // memory manager for cuts
+ Aig_MmFlex_t * pMemCuts; // memory manager for cuts
int nMergeLimit; // the limit on the size of merged cut
unsigned * pTruths[4]; // temporary truth tables
Vec_Int_t * vMemory; // memory for intermediate ISOP representation
@@ -88,8 +89,8 @@ static inline int Cnf_CutLeaveNum( Cnf_Cut_t * pCut ) { return pCut-
static inline int * Cnf_CutLeaves( Cnf_Cut_t * pCut ) { return pCut->pFanins; }
static inline unsigned * Cnf_CutTruth( Cnf_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
-static inline Cnf_Cut_t * Cnf_ObjBestCut( Dar_Obj_t * pObj ) { return pObj->pData; }
-static inline void Cnf_ObjSetBestCut( Dar_Obj_t * pObj, Cnf_Cut_t * pCut ) { pObj->pData = pCut; }
+static inline Cnf_Cut_t * Cnf_ObjBestCut( Aig_Obj_t * pObj ) { return pObj->pData; }
+static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut ) { pObj->pData = pCut; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
@@ -101,16 +102,16 @@ static inline void Cnf_ObjSetBestCut( Dar_Obj_t * pObj, Cnf_Cut_t * pCut
// iterator over leaves of the cut
#define Cnf_CutForEachLeaf( p, pCut, pLeaf, i ) \
- for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Dar_ManObj(p, (pCut)->pFanins[i])); i++ )
+ for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cnfCore.c ========================================================*/
-extern Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig );
+extern Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig );
/*=== cnfCut.c ========================================================*/
-extern Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj );
+extern Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj );
extern void Cnf_CutPrint( Cnf_Cut_t * pCut );
extern void Cnf_CutFree( Cnf_Cut_t * pCut );
extern void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes );
@@ -130,7 +131,7 @@ extern void Cnf_ManTransferCuts( Cnf_Man_t * p );
extern void Cnf_ManFreeCuts( Cnf_Man_t * p );
extern void Cnf_ManPostprocess( Cnf_Man_t * p );
/*=== cnfUtil.c ========================================================*/
-extern Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect );
+extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect );
/*=== cnfWrite.c ========================================================*/
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index b09f0bdc..a3a7efaa 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -39,20 +39,20 @@
SeeAlso []
***********************************************************************/
-Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig )
+Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig )
{
+ Aig_MmFixed_t * pMemCuts;
Cnf_Dat_t * pCnf = NULL;
Vec_Ptr_t * vMapped;
int nIters = 2;
int clk;
// connect the managers
- pAig->pManCnf = p;
p->pManAig = pAig;
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
- Dar_ManComputeCuts( pAig );
+ pMemCuts = Dar_ManComputeCuts( pAig );
PRT( "Cuts", clock() - clk );
/*
// iteratively improve area flow
@@ -65,7 +65,7 @@ PRT( "iter ", clock() - clk );
}
*/
// write the file
- vMapped = Dar_ManScanMapping( p, 1 );
+ vMapped = Aig_ManScanMapping( p, 1 );
Vec_PtrFree( vMapped );
clk = clock();
@@ -91,6 +91,7 @@ PRT( "Ext ", clock() - clk );
Dar_ManCutsFree( pAig );
return pCnf;
*/
+ Aig_MmFixedStop( pMemCuts, 0 );
return NULL;
}
diff --git a/src/aig/cnf/cnfCut.c b/src/aig/cnf/cnfCut.c
index feeef1f2..afe5920a 100644
--- a/src/aig/cnf/cnfCut.c
+++ b/src/aig/cnf/cnfCut.c
@@ -43,10 +43,10 @@
Cnf_Cut_t * Cnf_CutAlloc( Cnf_Man_t * p, int nLeaves )
{
Cnf_Cut_t * pCut;
- int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Dar_TruthWordNum(nLeaves);
- pCut = (Cnf_Cut_t *)Dar_MmFlexEntryFetch( p->pMemCuts, nSize );
+ int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Aig_TruthWordNum(nLeaves);
+ pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize );
pCut->nFanins = nLeaves;
- pCut->nWords = Dar_TruthWordNum(nLeaves);
+ pCut->nWords = Aig_TruthWordNum(nLeaves);
pCut->vIsop[0] = pCut->vIsop[1] = NULL;
return pCut;
}
@@ -81,13 +81,14 @@ void Cnf_CutFree( Cnf_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj )
+Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj )
{
Dar_Cut_t * pCutBest;
Cnf_Cut_t * pCut;
unsigned * pTruth;
- assert( Dar_ObjIsNode(pObj) );
- pCutBest = Dar_ObjBestCut( pObj );
+ assert( Aig_ObjIsNode(pObj) );
+// pCutBest = Aig_ObjBestCut( pObj );
+ pCutBest = NULL;
assert( pCutBest != NULL );
assert( pCutBest->nLeaves <= 4 );
pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
@@ -131,7 +132,7 @@ void Cnf_CutPrint( Cnf_Cut_t * pCut )
***********************************************************************/
void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
{
@@ -153,7 +154,7 @@ void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut )
***********************************************************************/
void Cnf_CutRef( Cnf_Man_t * p, Cnf_Cut_t * pCut )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
{
diff --git a/src/aig/cnf/cnfData.c b/src/aig/cnf/cnfData.c
index 57ce9392..7b8be51e 100644
--- a/src/aig/cnf/cnfData.c
+++ b/src/aig/cnf/cnfData.c
@@ -4614,7 +4614,7 @@ void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops )
SeeAlso []
***********************************************************************/
-int Dar_ManDeriveCnfTest()
+int Aig_ManDeriveCnfTest()
{
int i, k, Lit;
printf( "\n" );
@@ -4644,7 +4644,7 @@ int Dar_ManDeriveCnfTest()
SeeAlso []
***********************************************************************/
-int Dar_ManDeriveCnfTest2()
+int Aig_ManDeriveCnfTest2()
{
char s_Data3[81] = "!#&()*+,-.0123456789:;<=>?ABCDEFGHIJKLMNOPQRSTUVWXYZ[]abcdefghijklmnopqrstuvwxyz|";
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index d1d1fc21..e978e322 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -52,12 +52,12 @@ Cnf_Man_t * Cnf_ManStart()
// derive internal data structures
Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
// allocate memory manager for cuts
- p->pMemCuts = Dar_MmFlexStart();
+ p->pMemCuts = Aig_MmFlexStart();
p->nMergeLimit = 10;
// allocate temporary truth tables
- p->pTruths[0] = ALLOC( unsigned, 4 * Dar_TruthWordNum(p->nMergeLimit) );
+ p->pTruths[0] = ALLOC( unsigned, 4 * Aig_TruthWordNum(p->nMergeLimit) );
for ( i = 1; i < 4; i++ )
- p->pTruths[i] = p->pTruths[i-1] + Dar_TruthWordNum(p->nMergeLimit);
+ p->pTruths[i] = p->pTruths[i-1] + Aig_TruthWordNum(p->nMergeLimit);
p->vMemory = Vec_IntAlloc( 1 << 18 );
return p;
}
@@ -77,7 +77,7 @@ void Cnf_ManStop( Cnf_Man_t * p )
{
Vec_IntFree( p->vMemory );
free( p->pTruths[0] );
- Dar_MmFlexStop( p->pMemCuts, 0 );
+ Aig_MmFlexStop( p->pMemCuts, 0 );
free( p->pSopSizes );
free( p->pSops[1] );
free( p->pSops );
diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c
index 09be7701..a9ba41a0 100644
--- a/src/aig/cnf/cnfMap.c
+++ b/src/aig/cnf/cnfMap.c
@@ -28,6 +28,8 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#if 0
+
/**Function*************************************************************
Synopsis [Computes area of the first level.]
@@ -39,16 +41,16 @@
SeeAlso []
***********************************************************************/
-void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
+void Aig_CutDeref( Aig_Man_t * p, Dar_Cut_t * pCut )
{
- Dar_Obj_t * pLeaf;
+ Aig_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs > 0 );
- if ( --pLeaf->nRefs > 0 || !Dar_ObjIsAnd(pLeaf) )
+ if ( --pLeaf->nRefs > 0 || !Aig_ObjIsAnd(pLeaf) )
continue;
- Dar_CutDeref( p, Dar_ObjBestCut(pLeaf) );
+ Aig_CutDeref( p, Aig_ObjBestCut(pLeaf) );
}
}
@@ -63,16 +65,16 @@ void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
+int Aig_CutRef( Aig_Man_t * p, Dar_Cut_t * pCut )
{
- Dar_Obj_t * pLeaf;
- int i, Area = pCut->Cost;
+ Aig_Obj_t * pLeaf;
+ int i, Area = pCut->Value;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs >= 0 );
- if ( pLeaf->nRefs++ > 0 || !Dar_ObjIsAnd(pLeaf) )
+ if ( pLeaf->nRefs++ > 0 || !Aig_ObjIsAnd(pLeaf) )
continue;
- Area += Dar_CutRef( p, Dar_ObjBestCut(pLeaf) );
+ Area += Aig_CutRef( p, Aig_ObjBestCut(pLeaf) );
}
return Area;
}
@@ -88,11 +90,11 @@ int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-int Cnf_CutArea( Dar_Man_t * p, Dar_Cut_t * pCut )
+int Cnf_CutArea( Aig_Man_t * p, Dar_Cut_t * pCut )
{
int Area;
- Area = Dar_CutRef( p, pCut );
- Dar_CutDeref( p, pCut );
+ Area = Aig_CutRef( p, pCut );
+ Aig_CutDeref( p, pCut );
return Area;
}
@@ -136,7 +138,7 @@ static inline int Cnf_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
SeeAlso []
***********************************************************************/
-Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj )
+Dar_Cut_t * Cnf_ObjFindBestCut( Aig_Obj_t * pObj )
{
Dar_Cut_t * pCut, * pCutBest;
int i;
@@ -160,7 +162,7 @@ Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj )
***********************************************************************/
void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
{
- Dar_Obj_t * pLeaf;
+ Aig_Obj_t * pLeaf;
int i;
pCut->Cost = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
pCut->Area = (float)pCut->Cost;
@@ -168,16 +170,16 @@ void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
{
- if ( !Dar_ObjIsNode(pLeaf) )
+ if ( !Aig_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
- pCut->Area += Dar_ObjBestCut(pLeaf)->Area;
+ pCut->Area += Aig_ObjBestCut(pLeaf)->Area;
pCut->NoRefs++;
}
else
{
- pCut->Area += Dar_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
+ pCut->Area += Aig_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
if ( pCut->FanRefs + pLeaf->nRefs > 15 )
pCut->FanRefs = 15;
else
@@ -199,18 +201,18 @@ void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
***********************************************************************/
void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
{
- Dar_Obj_t * pLeaf;
+ Aig_Obj_t * pLeaf;
int i;
pCut->Area = (float)pCut->Cost;
pCut->NoRefs = 0;
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
{
- if ( !Dar_ObjIsNode(pLeaf) )
+ if ( !Aig_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
- pCut->Area += Dar_ObjBestCut(pLeaf)->Cost;
+ pCut->Area += Aig_ObjBestCut(pLeaf)->Cost;
pCut->NoRefs++;
}
else
@@ -236,18 +238,18 @@ void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
***********************************************************************/
int Cnf_ManMapForCnf( Cnf_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
Dar_Cut_t * pCut, * pCutBest;
int i, k;
// visit the nodes in the topological order and update their best cuts
- Dar_ManForEachNode( p->pManAig, pObj, i )
+ Aig_ManForEachNode( p->pManAig, pObj, i )
{
// find the old best cut
- pCutBest = Dar_ObjBestCut(pObj);
+ pCutBest = Aig_ObjBestCut(pObj);
Dar_ObjClearBestCut(pCutBest);
// if the node is used, dereference its cut
if ( pObj->nRefs )
- Dar_CutDeref( p->pManAig, pCutBest );
+ Aig_CutDeref( p->pManAig, pCutBest );
// evaluate the cuts of this node
Dar_ObjForEachCut( pObj, pCut, k )
@@ -259,11 +261,13 @@ int Cnf_ManMapForCnf( Cnf_Man_t * p )
Dar_ObjSetBestCut( pCutBest );
// if the node is used, reference its cut
if ( pObj->nRefs )
- Dar_CutRef( p->pManAig, pCutBest );
+ Aig_CutRef( p->pManAig, pCutBest );
}
return 1;
}
+#endif
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfPost.c b/src/aig/cnf/cnfPost.c
index 2f6a6424..988275b2 100644
--- a/src/aig/cnf/cnfPost.c
+++ b/src/aig/cnf/cnfPost.c
@@ -41,27 +41,30 @@
***********************************************************************/
void Cnf_ManPostprocess_old( Cnf_Man_t * p )
{
- extern int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
+// extern int Aig_ManLargeCutEval( Aig_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
int nNew, Gain, nGain = 0, nVars = 0;
- Dar_Obj_t * pObj, * pFan;
+ Aig_Obj_t * pObj, * pFan;
Dar_Cut_t * pCutBest, * pCut;
int i, k;//, a, b, Counter;
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_ManForEachObj( p->pManAig, pObj, i )
{
- if ( !Dar_ObjIsNode(pObj) )
+ if ( !Aig_ObjIsNode(pObj) )
continue;
if ( pObj->nRefs == 0 )
continue;
- pCutBest = Dar_ObjBestCut(pObj);
+// pCutBest = Aig_ObjBestCut(pObj);
+ pCutBest = NULL;
+
Dar_CutForEachLeaf( p->pManAig, pCutBest, pFan, k )
{
- if ( !Dar_ObjIsNode(pFan) )
+ if ( !Aig_ObjIsNode(pFan) )
continue;
assert( pFan->nRefs != 0 );
if ( pFan->nRefs != 1 )
continue;
- pCut = Dar_ObjBestCut(pFan);
+// pCut = Aig_ObjBestCut(pFan);
+ pCut = NULL;
/*
// find how many common variable they have
Counter = 0;
@@ -77,11 +80,16 @@ void Cnf_ManPostprocess_old( Cnf_Man_t * p )
printf( "%d ", Counter );
*/
// find the new truth table after collapsing these two cuts
- nNew = Dar_ManLargeCutEval( p->pManAig, pObj, pCutBest, pCut, pFan->Id );
+
+
+// nNew = Aig_ManLargeCutEval( p->pManAig, pObj, pCutBest, pCut, pFan->Id );
+ nNew = 0;
+
+
// printf( "%d+%d=%d:%d(%d) ", pCutBest->Cost, pCut->Cost,
// pCutBest->Cost+pCut->Cost, nNew, pCutBest->Cost+pCut->Cost-nNew );
- Gain = pCutBest->Cost+pCut->Cost-nNew;
+ Gain = pCutBest->Value + pCut->Value - nNew;
if ( Gain > 0 )
{
nGain += Gain;
@@ -105,12 +113,12 @@ void Cnf_ManPostprocess_old( Cnf_Man_t * p )
***********************************************************************/
void Cnf_ManTransferCuts( Cnf_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
- Dar_MmFlexRestart( p->pMemCuts );
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_MmFlexRestart( p->pMemCuts );
+ Aig_ManForEachObj( p->pManAig, pObj, i )
{
- if ( Dar_ObjIsNode(pObj) && pObj->nRefs > 0 )
+ if ( Aig_ObjIsNode(pObj) && pObj->nRefs > 0 )
pObj->pData = Cnf_CutCreate( p, pObj );
else
pObj->pData = NULL;
@@ -130,9 +138,9 @@ void Cnf_ManTransferCuts( Cnf_Man_t * p )
***********************************************************************/
void Cnf_ManFreeCuts( Cnf_Man_t * p )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_ManForEachObj( p->pManAig, pObj, i )
if ( pObj->pData )
{
Cnf_CutFree( pObj->pData );
@@ -154,10 +162,10 @@ void Cnf_ManFreeCuts( Cnf_Man_t * p )
void Cnf_ManPostprocess( Cnf_Man_t * p )
{
Cnf_Cut_t * pCut, * pCutFan, * pCutRes;
- Dar_Obj_t * pObj, * pFan;
+ Aig_Obj_t * pObj, * pFan;
int Order[16], Costs[16];
int i, k, fChanges;
- Dar_ManForEachNode( p->pManAig, pObj, i )
+ Aig_ManForEachNode( p->pManAig, pObj, i )
{
if ( pObj->nRefs == 0 )
continue;
@@ -167,7 +175,7 @@ void Cnf_ManPostprocess( Cnf_Man_t * p )
Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
{
Order[k] = k;
- Costs[k] = Dar_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
+ Costs[k] = Aig_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
}
// sort the cuts by Weight
do {
@@ -186,9 +194,9 @@ void Cnf_ManPostprocess( Cnf_Man_t * p )
// Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
- for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Dar_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
+ for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Aig_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
{
- if ( !Dar_ObjIsNode(pFan) )
+ if ( !Aig_ObjIsNode(pFan) )
continue;
assert( pFan->nRefs != 0 );
if ( pFan->nRefs != 1 )
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index 249f43fb..da5edef2 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -39,22 +39,23 @@
SeeAlso []
***********************************************************************/
-int Dar_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
+int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
{
- Dar_Obj_t * pLeaf;
+ Aig_Obj_t * pLeaf;
Dar_Cut_t * pCutBest;
int aArea, i;
- if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
+ if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
return 0;
- assert( Dar_ObjIsAnd(pObj) );
+ assert( Aig_ObjIsAnd(pObj) );
// collect the node first to derive pre-order
if ( vMapped )
Vec_PtrPush( vMapped, pObj );
// visit the transitive fanin of the selected cut
- pCutBest = Dar_ObjBestCut(pObj);
- aArea = pCutBest->Cost;
+// pCutBest = Aig_ObjBestCut(pObj);
+ pCutBest = NULL;
+ aArea = pCutBest->Value;
Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
- aArea += Dar_ManScanMapping_rec( p, pLeaf, vMapped );
+ aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
return aArea;
}
@@ -69,21 +70,21 @@ int Dar_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect )
+Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
{
Vec_Ptr_t * vMapped = NULL;
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
// clean all references
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
- Dar_ManForEachPo( p->pManAig, pObj, i )
- p->aArea += Dar_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
+ Aig_ManForEachPo( p->pManAig, pObj, i )
+ p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
return vMapped;
}
@@ -99,14 +100,14 @@ Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect )
SeeAlso []
***********************************************************************/
-int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
+int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
{
- Dar_Obj_t * pLeaf;
+ Aig_Obj_t * pLeaf;
Cnf_Cut_t * pCutBest;
int aArea, i;
- if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
+ if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
return 0;
- assert( Dar_ObjIsAnd(pObj) );
+ assert( Aig_ObjIsAnd(pObj) );
assert( pObj->pData != NULL );
// visit the transitive fanin of the selected cut
pCutBest = pObj->pData;
@@ -134,18 +135,18 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped
Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
{
Vec_Ptr_t * vMapped = NULL;
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
int i;
// clean all references
- Dar_ManForEachObj( p->pManAig, pObj, i )
+ Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
- Dar_ManForEachPo( p->pManAig, pObj, i )
- p->aArea += Cnf_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
+ Aig_ManForEachPo( p->pManAig, pObj, i )
+ p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
return vMapped;
}
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 2637d115..22c4240a 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -183,7 +183,7 @@ int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLite
***********************************************************************/
Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
{
- Dar_Obj_t * pObj;
+ Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Cnf_Cut_t * pCut;
int OutVar, pVars[32], * pLits, ** pClas;
@@ -191,11 +191,11 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
int i, k, nLiterals, nClauses, nCubes, Cube, Number;
// count the number of literals and clauses
- nLiterals = 1 + Dar_ManPoNum( p->pManAig );
- nClauses = 1 + Dar_ManPoNum( p->pManAig );
+ nLiterals = 1 + Aig_ManPoNum( p->pManAig );
+ nClauses = 1 + Aig_ManPoNum( p->pManAig );
Vec_PtrForEachEntry( vMapped, pObj, i )
{
- assert( Dar_ObjIsNode(pObj) );
+ assert( Aig_ObjIsNode(pObj) );
pCut = Cnf_ObjBestCut( pObj );
// positive polarity of the cut
@@ -224,7 +224,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
nClauses += Vec_IntSize(pCut->vIsop[0]);
}
-//printf( "%d ", nClauses-(1 + Dar_ManPoNum( p->pManAig )) );
+//printf( "%d ", nClauses-(1 + Aig_ManPoNum( p->pManAig )) );
}
//printf( "\n" );
@@ -239,13 +239,13 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
// set variable numbers
Number = 0;
- pCnf->pVarNums = ALLOC( int, 1+Dar_ManObjIdMax(p->pManAig) );
- memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Dar_ManObjIdMax(p->pManAig)) );
+ pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) );
+ memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) );
Vec_PtrForEachEntry( vMapped, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
- Dar_ManForEachPi( p->pManAig, pObj, i )
+ Aig_ManForEachPi( p->pManAig, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
- pCnf->pVarNums[Dar_ManConst1(p->pManAig)->Id] = Number++;
+ pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
pCnf->nVars = Number;
// assign the clauses
@@ -260,7 +260,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
for ( k = 0; k < (int)pCut->nFanins; k++ )
{
pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
- assert( pVars[k] <= Dar_ManObjIdMax(p->pManAig) );
+ assert( pVars[k] <= Aig_ManObjIdMax(p->pManAig) );
}
// positive polarity of the cut
@@ -310,17 +310,17 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
}
// write the constant literal
- OutVar = pCnf->pVarNums[ Dar_ManConst1(p->pManAig)->Id ];
- assert( OutVar <= Dar_ManObjIdMax(p->pManAig) );
+ OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
+ assert( OutVar <= Aig_ManObjIdMax(p->pManAig) );
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
// write the output literals
- Dar_ManForEachPo( p->pManAig, pObj, i )
+ Aig_ManForEachPo( p->pManAig, pObj, i )
{
- OutVar = pCnf->pVarNums[ Dar_ObjFanin0(pObj)->Id ];
+ OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
*pClas++ = pLits;
- *pLits++ = 2 * OutVar + Dar_ObjFaninC0(pObj);
+ *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
}
// verify that the correct number of literals and clauses was written
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 07:16:09 +0000