summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abcMiter.c14
-rw-r--r--src/base/abci/abcNtbdd.c2
-rw-r--r--src/base/abci/abcPrint.c5
-rw-r--r--src/base/abci/abcRr.c2
-rw-r--r--src/base/abci/abcSat.c13
-rw-r--r--src/base/abci/abcStrash.c4
-rw-r--r--src/base/abci/abcUnreach.c2
-rw-r--r--src/base/abci/abcVanEijk.c4
-rw-r--r--src/base/abci/abcVanImp.c2
9 files changed, 26 insertions, 22 deletions
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index dfd49f6e..ff05fe69 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -87,7 +87,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
assert( Abc_NtkIsStrash(pNtk2) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -304,7 +304,7 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -356,7 +356,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
assert( 1 == Abc_NtkCoNum(pNtk) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_miter", pNtk->pName );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -423,7 +423,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
assert( In2 < Abc_NtkCiNum(pNtk) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -488,7 +488,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
assert( In < Abc_NtkCiNum(pNtk) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
// get the root output
@@ -669,7 +669,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkIsDfsOrdered(pNtk) );
// start the new network
- pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
pNtkFrames->pName = Extra_UtilStrsav(Buffer);
// create new latches (or their initial values) and remember them in the new latches
@@ -806,7 +806,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
assert( nFrames > 0 );
assert( Abc_NtkIsStrash(pNtk) );
// start the new network
- pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
pNtkFrames->pName = Extra_UtilStrsav(Buffer);
// create new latches (or their initial values) and remember them in the new latches
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 99ed5636..ac46501c 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -78,7 +78,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
return NULL;
// start the network
- pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+ pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
pNtk->pName = Extra_UtilStrsav(pNamePo);
// make sure the new manager has enough inputs
Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index cb1d2a38..e3bb764d 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -66,7 +66,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
if ( Abc_NtkIsNetlist(pNtk) )
{
fprintf( pFile, " net = %5d", Abc_NtkNetNum(pNtk) );
- fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
+ fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
+ fprintf( pFile, " box = %5d", Abc_NtkBoxNum(pNtk) );
}
else if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
{
@@ -83,7 +84,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
else
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
- if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
+ if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) || Abc_NtkIsNetlist(pNtk) )
{
}
else if ( Abc_NtkHasSop(pNtk) )
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 61bc8b09..03073075 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -676,7 +676,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
int i;
assert( Abc_NtkIsStrash(pNtk) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav( "temp" );
// map the constant nodes
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 86f13884..02bfca17 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -436,6 +436,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
int clk1 = clock(), clk;
int fOrderCiVarsFirst = 0;
int nLevelsMax = Abc_AigGetLevelNum(pNtk);
+ int RetValue = 0;
assert( Abc_NtkIsStrash(pNtk) );
@@ -481,7 +482,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
}
// add the trivial clause
if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
- return 0;
+ goto Quits;
}
// add the clauses
@@ -515,7 +516,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
}
// add the clauses
if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
- return 0;
+ goto Quits;
}
else
{
@@ -537,12 +538,12 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
{
if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
// if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
- return 0;
+ goto Quits;
}
else
{
if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
- return 0;
+ goto Quits;
}
}
// add the variables to the J-frontier
@@ -597,11 +598,13 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
Asat_SolverSetFactors( pSat, Vec_IntReleaseArray(vLevels) );
Vec_IntFree( vLevels );
*/
+ RetValue = 1;
+Quits :
// delete
Vec_IntFree( vVars );
Vec_PtrFree( vNodes );
Vec_PtrFree( vSuper );
- return 1;
+ return RetValue;
}
/**Function*************************************************************
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index c69aeabf..c54ea33c 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -250,7 +250,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
Abc_Obj_t * pFanin;
int i;
assert( Abc_ObjIsNode(pNodeOld) );
- assert( Abc_NtkIsAigLogic(pNodeOld->pNtk) );
+ assert( Abc_NtkHasAig(pNodeOld->pNtk) && !Abc_NtkIsStrash(pNodeOld->pNtk) );
// get the local AIG manager and the local root node
pMan = pNodeOld->pNtk->pManFunc;
pRoot = pNodeOld->pData;
@@ -317,7 +317,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
// get the cutoff level
LevelCut = ABC_MAX( 0, Abc_AigGetLevelNum(pNtk) - nLevels );
// start the network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
// create PIs below the cut and nodes above the cut
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index b5306bea..156d9b3d 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -284,7 +284,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
int i;
// start the new network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
pNtkNew->pName = Extra_UtilStrsav( "exdc" );
pNtkNew->pSpec = NULL;
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index 58d9f64e..50baa285 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -514,7 +514,7 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
if ( vCorresp )
Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL );
// start the new network
- pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
if ( fShortNames )
{
pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName);
@@ -719,7 +719,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
assert( Abc_NtkIsStrash(pNtk) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
pNtkNew->pName = Extra_UtilStrsav("exdc");
pNtkNew->pSpec = NULL;
diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c
index 29b5d3a6..339d64d1 100644
--- a/src/base/abci/abcVanImp.c
+++ b/src/base/abci/abcVanImp.c
@@ -877,7 +877,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
assert( Abc_NtkIsStrash(pNtk) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
pNtkNew->pName = Extra_UtilStrsav( "exdc" );
pNtkNew->pSpec = NULL;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-10 22:35:46 +0000