luke/abc
1
0
Fork 0
mirror of https://github.com/YosysHQ/abc.git synced 2026-08-22 14:06:36 +02:00
Code Issues Packages Projects Releases Wiki Activity

Version abc50908

Browse Source
This commit is contained in:
Alan Mishchenko
2005-09-08 08:01:00 -07:00
parent 1260d20cc0
commit eb4cdcdcb4
60 changed files with 1105 additions and 173501 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/base/abc/abc.h
+14 -9
View File
@@ -147,10 +147,10 @@ struct Abc_Ntk_t_
Vec_Ptr_t * vCos; // the array of combinational outputs (POs followed by latches)
Vec_Ptr_t * vLats; // the array of latches (or the cutset in the sequential network)
// the stats about the number of living objects
int nObjs; // the number of living objs
int nNets; // the number of living nets
int nNodes; // the number of living nodes
int nLatches; // the number of latches
int nObjs; // the number of live objs
int nNets; // the number of live nets
int nNodes; // the number of live nodes
int nLatches; // the number of live latches
int nPis; // the number of primary inputs
int nPos; // the number of primary outputs
// the functionality manager
@@ -167,6 +167,8 @@ struct Abc_Ntk_t_
Vec_Int_t * vLevelsR; // level in the reverse topological order
// support information
Vec_Ptr_t * vSupps;
// the satisfiable assignment of the miter
int * pModel;
// the external don't-care if given
Abc_Ntk_t * pExdc; // the EXDC network
// miscellaneous data members
@@ -401,7 +403,7 @@ extern Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Ab
extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew );
extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
@@ -414,6 +416,7 @@ extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
/*=== abcCheck.c ==========================================================*/
extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk );
extern bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
extern bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
/*=== abcCollapse.c ==========================================================*/
@@ -427,6 +430,7 @@ extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
extern int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk );
@@ -440,6 +444,7 @@ extern void Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t
extern void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
/*=== abcFraig.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes );
extern void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes );
extern Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk );
extern int Abc_NtkFraigStore( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkFraigRestore();
@@ -470,9 +475,6 @@ extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial );
/*=== abcObj.c ==========================================================*/
extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_ObjRecycle( Abc_Obj_t * pObj );
extern void Abc_ObjAdd( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
extern Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
@@ -560,12 +562,13 @@ extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t *
extern int Abc_NodeMffcSize( Abc_Obj_t * pNode );
extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode );
extern int Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
extern Vec_Ptr_t * Abc_NodeMffcCollect( Abc_Obj_t * pNode );
/*=== abcRenode.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple );
extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
/*=== abcSat.c ==========================================================*/
extern bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose );
extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose );
extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
/*=== abcSeq.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
@@ -660,6 +663,8 @@ extern int Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_O
extern int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
extern Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
extern void Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
src/base/abc/abcAig.c
+20 -14
View File
@@ -83,7 +83,7 @@ static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_O
static void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis );
static void Abc_AigResize( Abc_Aig_t * pMan );
// incremental AIG procedures
static void Abc_AigReplace_int( Abc_Aig_t * pMan );
static void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel );
static void Abc_AigDelete_int( Abc_Aig_t * pMan );
static void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan );
static void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan );
@@ -655,7 +655,7 @@ Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
SeeAlso []
***********************************************************************/
void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel )
{
assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 );
assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 );
@@ -663,9 +663,12 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
Vec_PtrPush( pMan->vStackReplaceOld, pOld );
Vec_PtrPush( pMan->vStackReplaceNew, pNew );
while ( Vec_PtrSize(pMan->vStackReplaceOld) )
Abc_AigReplace_int( pMan );
Abc_AigUpdateLevel_int( pMan );
Abc_AigUpdateLevelR_int( pMan );
Abc_AigReplace_int( pMan, fUpdateLevel );
if ( fUpdateLevel )
{
Abc_AigUpdateLevel_int( pMan );
Abc_AigUpdateLevelR_int( pMan );
}
}
/**Function*************************************************************
@@ -679,7 +682,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
SeeAlso []
***********************************************************************/
void Abc_AigReplace_int( Abc_Aig_t * pMan )
void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel )
{
Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew, * pFanoutFanout;
int k, v, iFanin;
@@ -736,14 +739,17 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );
// schedule the updated fanout for updating direct level
assert( pFanout->fMarkA == 0 );
pFanout->fMarkA = 1;
Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
// schedule the updated fanout for updating reverse level
assert( pFanout->fMarkB == 0 );
pFanout->fMarkB = 1;
Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
if ( fUpdateLevel )
{
// schedule the updated fanout for updating direct level
assert( pFanout->fMarkA == 0 );
pFanout->fMarkA = 1;
Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
// schedule the updated fanout for updating reverse level
assert( pFanout->fMarkB == 0 );
pFanout->fMarkB = 1;
Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
}
// the fanout has changed, update EXOR status of its fanouts
Abc_ObjForEachFanout( pFanout, pFanoutFanout, v )
src/base/abc/abcCheck.c
-1
View File
@@ -25,7 +25,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
static bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk );
static bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk );
static bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk );
src/base/abc/abcDfs.c
+63
View File
@@ -27,6 +27,7 @@
static void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
static void Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
static void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
static void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
static void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels );
static int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode );
static bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode );
@@ -206,6 +207,68 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
}
/**Function*************************************************************
Synopsis [Returns the set of CI nodes in the support of the given nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes )
{
Vec_Ptr_t * vNodes;
int i;
// set the traversal ID
Abc_NtkIncrementTravId( pNtk );
// start the array of nodes
vNodes = Vec_PtrAlloc( 100 );
// go through the PO nodes and call for each of them
for ( i = 0; i < nNodes; i++ )
if ( Abc_ObjIsCo(ppNodes[i]) )
Abc_NtkNodeSupport_rec( Abc_ObjFanin0(ppNodes[i]), vNodes );
else
Abc_NtkNodeSupport_rec( ppNodes[i], vNodes );
return vNodes;
}
/**Function*************************************************************
Synopsis [Performs DFS for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
{
Abc_Obj_t * pFanin;
int i;
assert( !Abc_ObjIsNet(pNode) );
// if this node is already visited, skip
if ( Abc_NodeIsTravIdCurrent( pNode ) )
return;
// mark the node as visited
Abc_NodeSetTravIdCurrent( pNode );
// collect the CI
if ( Abc_ObjIsCi(pNode) )
{
Vec_PtrPush( vNodes, pNode );
return;
}
assert( Abc_ObjIsNode( pNode ) );
// visit the transitive fanin of the node
Abc_ObjForEachFanin( pNode, pFanin, i )
Abc_NtkNodeSupport_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
}
/**Function*************************************************************
Synopsis [Returns the DFS ordered array of logic nodes.]
src/base/abc/abcInt.h
+11
View File
@@ -29,6 +29,8 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define ABC_NUM_STEPS 10
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -37,6 +39,15 @@
/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== abcObj.c ==========================================================*/
extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_ObjRecycle( Abc_Obj_t * pObj );
extern void Abc_ObjAdd( Abc_Obj_t * pObj );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abc/abcNtk.c
+7 -4
View File
@@ -19,6 +19,7 @@
***********************************************************************/
#include "abc.h"
#include "abcInt.h"
#include "main.h"
#include "mio.h"
@@ -26,8 +27,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define ABC_NUM_STEPS 10
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -400,7 +399,10 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t *
pFinal = Abc_AigConst1( pNtkNew->pManFunc );
Vec_PtrForEachEntry( vRoots, pObj, i )
{
pOther = pObj->pCopy;
if ( Abc_ObjIsCo(pObj) )
pOther = Abc_ObjFanin0(pObj)->pCopy;
else
pOther = pObj->pCopy;
if ( Vec_IntEntry(vValues, i) == 0 )
pOther = Abc_ObjNot(pOther);
pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther );
@@ -477,7 +479,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// free large fanout arrays
if ( pObj->vFanouts.nCap * 4 > LargePiece )
FREE( pObj->vFanouts.pArray );
// check that the other things are okay
// these flags should be always zero
// if this is not true, something is wrong somewhere
assert( pObj->fMarkA == 0 );
assert( pObj->fMarkB == 0 );
assert( pObj->fMarkC == 0 );
src/base/abc/abcObj.c
+7
View File
@@ -19,6 +19,7 @@
***********************************************************************/
#include "abc.h"
#include "abcInt.h"
#include "main.h"
#include "mio.h"
@@ -66,7 +67,13 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
void Abc_ObjRecycle( Abc_Obj_t * pObj )
{
Abc_Ntk_t * pNtk = pObj->pNtk;
int LargePiece = (4 << ABC_NUM_STEPS);
// free large fanout arrays
if ( pObj->vFanouts.nCap * 4 > LargePiece )
FREE( pObj->vFanouts.pArray );
// clean the memory to make deleted object distinct from the live one
memset( pObj, 0, sizeof(Abc_Obj_t) );
// recycle the object
Extra_MmFixedEntryRecycle( pNtk->pMmObj, (char *)pObj );
}
src/base/abc/abcRefs.c
+70
View File
@@ -26,6 +26,7 @@
static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes );
static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference );
static int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -106,6 +107,42 @@ int Abc_NodeMffcLabel( Abc_Obj_t * pNode )
return nConeSize1;
}
/**Function*************************************************************
Synopsis [Returns the MFFC size.]
Description [Profiling shows that this procedure runs the same as
the above one, not faster.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
{
Abc_Obj_t * pTemp;
int nConeSize, i;
assert( !Abc_ObjIsComplement( pNode ) );
assert( Abc_ObjIsNode( pNode ) );
if ( Abc_ObjFaninNum(pNode) == 0 )
return 0;
Vec_PtrClear( vNodes );
nConeSize = Abc_NodeDeref( pNode, vNodes );
// label the nodes with the current ID and ref their children
Vec_PtrForEachEntry( vNodes, pTemp, i )
{
Abc_NodeSetTravIdCurrent( pTemp );
if ( Abc_ObjIsCi(pTemp) )
continue;
Abc_ObjFanin0(pTemp)->vFanouts.nSize++;
Abc_ObjFanin1(pTemp)->vFanouts.nSize++;
}
return nConeSize;
}
/**Function*************************************************************
Synopsis [Collects the nodes in MFFC in the topological order.]
@@ -180,6 +217,39 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t
return Counter;
}
/**Function*************************************************************
Synopsis [References/references the node and returns MFFC size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
{
Abc_Obj_t * pNode0, * pNode1;
int Counter;
// collect visited nodes
Vec_PtrPush( vNodes, pNode );
// skip the CI
if ( Abc_ObjIsCi(pNode) )
return 0;
// process the internal node
pNode0 = Abc_ObjFanin0(pNode);
pNode1 = Abc_ObjFanin1(pNode);
assert( pNode0->vFanouts.nSize > 0 );
assert( pNode1->vFanouts.nSize > 0 );
Counter = 1;
if ( --pNode0->vFanouts.nSize == 0 )
Counter += Abc_NodeDeref( pNode0, vNodes );
if ( --pNode1->vFanouts.nSize == 0 )
Counter += Abc_NodeDeref( pNode1, vNodes );
return Counter;
}
/**Function*************************************************************
Synopsis [References/references the node and returns MFFC size.]
src/base/abc/abcUtil.c
+95
View File
@@ -883,6 +883,101 @@ Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk )
return vNodes;
}
/**Function*************************************************************
Synopsis [Returns the array of CI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vCiIds;
Abc_Obj_t * pObj;
int i;
vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
Vec_IntPush( vCiIds, pObj->Id );
return vCiIds;
}
/**Function*************************************************************
Synopsis [Puts the nodes into the DFS order and reassign their IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vNodes;
Vec_Ptr_t * vObjsNew;
Abc_Obj_t * pNode, * pTemp;
Abc_Obj_t * pConst1 = NULL, * pReset = NULL;
int i, k;
// start the array of objects with new IDs
vObjsNew = Vec_PtrAlloc( pNtk->nObjs );
// put constant nodes (if present) first
if ( Abc_NtkIsStrash(pNtk) )
{
pConst1 = Abc_AigConst1(pNtk->pManFunc);
pConst1->Id = Vec_PtrSize( vObjsNew );
Vec_PtrPush( vObjsNew, pConst1 );
pReset = Abc_AigReset(pNtk->pManFunc);
pReset->Id = Vec_PtrSize( vObjsNew );
Vec_PtrPush( vObjsNew, pReset );
}
// put PI nodes next
Abc_NtkForEachPi( pNtk, pNode, i )
{
pNode->Id = Vec_PtrSize( vObjsNew );
Vec_PtrPush( vObjsNew, pNode );
}
// put PO nodes next
Abc_NtkForEachPo( pNtk, pNode, i )
{
pNode->Id = Vec_PtrSize( vObjsNew );
Vec_PtrPush( vObjsNew, pNode );
}
// put latches next
Abc_NtkForEachLatch( pNtk, pNode, i )
{
pNode->Id = Vec_PtrSize( vObjsNew );
Vec_PtrPush( vObjsNew, pNode );
}
// finally, internal nodes in the DFS order
vNodes = Abc_NtkDfs( pNtk, 1 );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( pNode == pReset || pNode == pConst1 )
continue;
pNode->Id = Vec_PtrSize( vObjsNew );
Vec_PtrPush( vObjsNew, pNode );
}
Vec_PtrFree( vNodes );
assert( Vec_PtrSize(vObjsNew) == pNtk->nObjs );
// update the fanin/fanout arrays
Abc_NtkForEachObj( pNtk, pNode, i )
{
Abc_ObjForEachFanin( pNode, pTemp, k )
pNode->vFanins.pArray[k].iFan = pTemp->Id;
Abc_ObjForEachFanout( pNode, pTemp, k )
pNode->vFanouts.pArray[k].iFan = pTemp->Id;
}
// replace the array of objs
Vec_PtrFree( pNtk->vObjs );
pNtk->vObjs = vObjsNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
src/base/abci/abc.c
+107 -43
View File
@@ -1672,26 +1672,31 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
bool fUpdateLevel;
bool fPrecompute;
bool fUseZeros;
bool fVerbose;
// external functions
extern void Rwr_Precompute();
extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose );
extern void Rwr_Precompute();
extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fPrecompute = 0;
fUseZeros = 0;
fVerbose = 0;
fUpdateLevel = 0;
fPrecompute = 0;
fUseZeros = 0;
fVerbose = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "xzvh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "lxzvh" ) ) != EOF )
{
switch ( c )
{
case 'l':
fUpdateLevel ^= 1;
break;
case 'x':
fPrecompute ^= 1;
break;
@@ -1731,7 +1736,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
if ( !Abc_NtkRewrite( pNtk, fUseZeros, fVerbose ) )
if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose ) )
{
fprintf( pErr, "Rewriting has failed.\n" );
return 1;
@@ -1739,8 +1744,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: rewrite [-zvh]\n" );
fprintf( pErr, "usage: rewrite [-lzvh]\n" );
fprintf( pErr, "\t performs technology-independent rewriting of the AIG\n" );
fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -1765,10 +1771,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int nNodeSizeMax;
int nConeSizeMax;
bool fUpdateLevel;
bool fUseZeros;
bool fUseDcs;
bool fVerbose;
extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose );
extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -1777,11 +1784,12 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nNodeSizeMax = 10;
nConeSizeMax = 16;
fUpdateLevel = 0;
fUseZeros = 0;
fUseDcs = 0;
fVerbose = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "NCzdvh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "NClzdvh" ) ) != EOF )
{
switch ( c )
{
@@ -1807,6 +1815,9 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConeSizeMax < 0 )
goto usage;
break;
case 'l':
fUpdateLevel ^= 1;
break;
case 'z':
fUseZeros ^= 1;
break;
@@ -1846,7 +1857,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUseZeros, fUseDcs, fVerbose ) )
if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ) )
{
fprintf( pErr, "Refactoring has failed.\n" );
return 1;
@@ -1854,10 +1865,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: refactor [-N num] [-C num] [-zdvh]\n" );
fprintf( pErr, "usage: refactor [-N num] [-C num] [-lzdvh]\n" );
fprintf( pErr, "\t performs technology-independent refactoring of the AIG\n" );
fprintf( pErr, "\t-N num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );
fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax );
fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
fprintf( pErr, "\t-d : toggle using don't-cares [default = %s]\n", fUseDcs? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
@@ -2291,7 +2303,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int RetValue;
int fVerbose;
int nSeconds;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -2299,11 +2313,23 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fVerbose = 0;
nSeconds = 20;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "Tvh" ) ) != EOF )
{
switch ( c )
{
case 'T':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nSeconds = atoi(argv[util_optind]);
util_optind++;
if ( nSeconds < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
@@ -2323,7 +2349,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
return 0;
}
}
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
@@ -2334,15 +2360,19 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkIsSopLogic(pNtk) )
Abc_NtkSopToBdd(pNtk);
if ( Abc_NtkMiterSat( pNtk, fVerbose ) )
printf( "The miter is satisfiable.\n" );
RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
if ( RetValue == -1 )
printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "The miter is SATISFIABLE.\n" );
else
printf( "The miter is unsatisfiable.\n" );
printf( "The miter is UNSATISFIABLE.\n" );
return 0;
usage:
fprintf( pErr, "usage: sat [-vh]\n" );
fprintf( pErr, "usage: sat [-T num] [-vh]\n" );
fprintf( pErr, "\t solves the miter\n" );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -2863,6 +2893,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fAllNodes = 0;
memset( pParams, 0, sizeof(Fraig_Params_t) );
pParams->nPatsRand = 2048; // the number of words of random simulation info
pParams->nPatsDyna = 2048; // the number of words of dynamic simulation info
pParams->nBTLimit = 99; // the max number of backtracks to perform
@@ -2879,7 +2910,6 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
switch ( c )
{
case 'R':
if ( util_optind >= argc )
{
@@ -3913,9 +3943,10 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fSat;
int fVerbose;
int nSeconds;
extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose );
extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds );
extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
pNtk = Abc_FrameReadNet(pAbc);
@@ -3923,13 +3954,25 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fSat = 0;
fVerbose = 0;
fSat = 0;
fVerbose = 0;
nSeconds = 20;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "svh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "Tsvh" ) ) != EOF )
{
switch ( c )
{
case 'T':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nSeconds = atoi(argv[util_optind]);
util_optind++;
if ( nSeconds < 0 )
goto usage;
break;
case 's':
fSat ^= 1;
break;
@@ -3948,24 +3991,25 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform equivalence checking
if ( fSat )
Abc_NtkCecSat( pNtk1, pNtk2 );
Abc_NtkCecSat( pNtk1, pNtk2, nSeconds );
else
Abc_NtkCecFraig( pNtk1, pNtk2, fVerbose );
Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
return 0;
usage:
fprintf( pErr, "usage: cec [-svh] <file1> <file2>\n" );
fprintf( pErr, "\t performs combinational equivalence checking\n" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
fprintf( pErr, "\t if no files are given, uses the current network and its spec\n");
fprintf( pErr, "\t if one file is given, uses the current network and the file\n");
fprintf( pErr, "usage: cec [-T num] [-svh] <file1> <file2>\n" );
fprintf( pErr, "\t performs combinational equivalence checking\n" );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
fprintf( pErr, "\t if no files are given, uses the current network and its spec\n");
fprintf( pErr, "\t if one file is given, uses the current network and the file\n");
return 1;
}
@@ -3989,10 +4033,12 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
int nArgcNew;
int c;
int fSat;
int fVerbose;
int nFrames;
int nSeconds;
extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames );
extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames );
extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames );
extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
pNtk = Abc_FrameReadNet(pAbc);
@@ -4000,10 +4046,12 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames = 3;
fSat = 0;
fSat = 0;
fVerbose = 0;
nFrames = 3;
nSeconds = 20;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "Fsh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "FTsvh" ) ) != EOF )
{
switch ( c )
{
@@ -4018,6 +4066,20 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFrames < 0 )
goto usage;
break;
case 'T':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nSeconds = atoi(argv[util_optind]);
util_optind++;
if ( nSeconds < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 's':
fSat ^= 1;
break;
@@ -4033,20 +4095,22 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform equivalence checking
if ( fSat )
Abc_NtkSecSat( pNtk1, pNtk2, nFrames );
Abc_NtkSecSat( pNtk1, pNtk2, nSeconds, nFrames );
else
Abc_NtkSecFraig( pNtk1, pNtk2, nFrames );
Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
return 0;
usage:
fprintf( pErr, "usage: sec [-sh] [-F num] <file1> <file2>\n" );
fprintf( pErr, "usage: sec [-F num] [-T num] [-svh] <file1> <file2>\n" );
fprintf( pErr, "\t performs bounded sequential equivalence checking\n" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
fprintf( pErr, "\t if no files are given, uses the current network and its spec\n");
src/base/abci/abcBalance.c
+21 -10
View File
@@ -25,8 +25,8 @@
////////////////////////////////////////////////////////////////////////
static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate );
static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, bool fDuplicate );
static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int fDuplicate );
static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate );
static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate );
static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate );
////////////////////////////////////////////////////////////////////////
@@ -86,7 +86,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
// set the level of PIs of AIG according to the arrival times of the old network
Abc_NtkSetNodeLevelsArrival( pNtk );
// allocate temporary storage for supergates
vStorage = Vec_VecStart( Abc_AigGetLevelNum(pNtk) + 1 );
vStorage = Vec_VecStart( 10 );
// perform balancing of POs
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
@@ -94,7 +94,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
Extra_ProgressBarUpdate( pProgress, i, NULL );
// strash the driver node
pDriver = Abc_ObjFanin0(pNode);
Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, fDuplicate );
Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate );
}
Extra_ProgressBarStop( pProgress );
Vec_VecFree( vStorage );
@@ -111,7 +111,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, bool fDuplicate )
Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate )
{
Abc_Aig_t * pMan = pNtkNew->pManFunc;
Abc_Obj_t * pNodeNew, * pNode1, * pNode2;
@@ -123,7 +123,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
return pNodeOld->pCopy;
assert( Abc_ObjIsNode(pNodeOld) );
// get the implication supergate
vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, fDuplicate );
vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate );
if ( vSuper->nSize == 0 )
{ // it means that the supergate contains two nodes in the opposite polarity
pNodeOld->pCopy = Abc_ObjNot(Abc_AigConst1(pMan));
@@ -132,9 +132,11 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
// for each old node, derive the new well-balanced node
for ( i = 0; i < vSuper->nSize; i++ )
{
pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, fDuplicate );
pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate );
vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) );
}
if ( vSuper->nSize < 2 )
printf( "BUG!\n" );
// sort the new nodes by level in the decreasing order
Vec_PtrSort( vSuper, Abc_NodeCompareLevelsDecrease );
// balance the nodes
@@ -149,6 +151,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
assert( pNodeOld->pCopy == NULL );
// mark the old node with the new node
pNodeOld->pCopy = vSuper->pArray[0];
vSuper->nSize = 0;
return pNodeOld->pCopy;
}
@@ -165,17 +168,25 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int fDuplicate )
Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate )
{
Vec_Ptr_t * vNodes;
int RetValue, i;
assert( !Abc_ObjIsComplement(pNode) );
vNodes = Vec_VecEntry( vStorage, pNode->Level );
// extend the storage
if ( Vec_VecSize( vStorage ) <= Level )
Vec_VecPush( vStorage, Level, 0 );
// get the temporary array of nodes
vNodes = Vec_VecEntry( vStorage, Level );
Vec_PtrClear( vNodes );
// collect the nodes in the implication supergate
RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate );
assert( vNodes->nSize > 0 );
assert( vNodes->nSize > 1 );
// unmark the visited nodes
for ( i = 0; i < vNodes->nSize; i++ )
Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0;
// if we found the node and its complement in the same implication supergate,
// return empty set of nodes (meaning that we should use constant-0 node)
if ( RetValue == -1 )
vNodes->nSize = 0;
return vNodes;
src/base/abci/abcFraig.c
+5 -5
View File
@@ -26,7 +26,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
@@ -83,13 +82,14 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
SeeAlso []
***********************************************************************/
Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes )
void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
{
Fraig_Man_t * pMan;
ProgressBar * pProgress;
Fraig_Node_t * pNodeFraig;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode, * pConst1, * pReset;
int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
int i;
assert( Abc_NtkIsStrash(pNtk) );
@@ -106,11 +106,11 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
// perform strashing
vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
if ( !pParams->fInternal )
if ( !fInternal )
pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( !pParams->fInternal )
if ( !fInternal )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pNode == pConst1 )
pNodeFraig = Fraig_ManReadConst1(pMan);
@@ -123,7 +123,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
assert( pNode->pCopy == NULL );
pNode->pCopy = (Abc_Obj_t *)pNodeFraig;
}
if ( !pParams->fInternal )
if ( !fInternal )
Extra_ProgressBarStop( pProgress );
Vec_PtrFree( vNodes );
src/base/abci/abcMiter.c
+5 -5
View File
@@ -372,8 +372,8 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
Synopsis [Checks the status of the miter.]
Description [Return 1 if the miter is sat for at least one output.
Return 0 if the miter is unsat for all its outputs. Returns -1 if the
Description [Return 0 if the miter is sat for at least one output.
Return 1 if the miter is unsat for all its outputs. Returns -1 if the
miter is undecided for some outputs.]
SideEffects []
@@ -396,15 +396,15 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
{
// if the miter is constant 1, return immediately
printf( "MITER IS CONSTANT 1!\n" );
return 1;
return 0;
}
}
// if the miter is undecided (or satisfiable), return immediately
else
return -1;
}
// return 0, meaning all outputs are constant zero
return 0;
// return 1, meaning all outputs are constant zero
return 1;
}
/**Function*************************************************************
src/base/abci/abcRefactor.c
+19 -8
View File
@@ -58,7 +58,7 @@ struct Abc_ManRef_t_
static void Abc_NtkManRefPrintStats( Abc_ManRef_t * p );
static Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose );
static void Abc_NtkManRefStop( Abc_ManRef_t * p );
static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose );
static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -80,7 +80,7 @@ static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec
SeeAlso []
***********************************************************************/
int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose )
int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
{
ProgressBar * pProgress;
Abc_ManRef_t * pManRef;
@@ -98,7 +98,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
pManRef->vLeaves = Abc_NtkManCutReadCutLarge( pManCut );
Abc_NtkStartReverseLevels( pNtk );
// compute the reverse levels if level update is requested
if ( fUpdateLevel )
Abc_NtkStartReverseLevels( pNtk );
// resynthesize each node once
nNodes = Abc_NtkObjNumMax(pNtk);
@@ -121,13 +123,13 @@ clk = clock();
pManRef->timeCut += clock() - clk;
// evaluate this cut
clk = clock();
pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUseZeros, fUseDcs, fVerbose );
pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
pManRef->timeRes += clock() - clk;
if ( pFForm == NULL )
continue;
// acceptable replacement found, update the graph
clk = clock();
Dec_GraphUpdateNetwork( pNode, pFForm, pManRef->nLastGain );
Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
pManRef->timeNtk += clock() - clk;
Dec_GraphFree( pFForm );
}
@@ -140,7 +142,13 @@ pManRef->timeTotal = clock() - clkStart;
// delete the managers
Abc_NtkManCutStop( pManCut );
Abc_NtkManRefStop( pManRef );
Abc_NtkStopReverseLevels( pNtk );
// put the nodes into the DFS order and reassign their IDs
Abc_NtkReassignIds( pNtk );
// fix the levels
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );
else
Abc_NtkGetLevelNum( pNtk );
// check
if ( !Abc_NtkCheck( pNtk ) )
{
@@ -161,7 +169,7 @@ pManRef->timeTotal = clock() - clkStart;
SeeAlso []
***********************************************************************/
Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose )
Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
{
int fVeryVerbose = 0;
Abc_Obj_t * pFanin;
@@ -169,6 +177,9 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
DdNode * bNodeFunc;
int nNodesSaved, nNodesAdded, i, clk;
char * pSop;
int Required;
Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
p->nNodesConsidered++;
@@ -239,7 +250,7 @@ p->timeFact += clock() - clk;
// detect how many new nodes will be added (while taking into account reused nodes)
clk = clock();
nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Abc_NodeReadRequiredLevel(pNode) );
nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Required );
p->timeEval += clock() - clk;
// quit if there is no improvement
if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !fUseZeros )
src/base/abci/abcRenode.c
+1 -1
View File
@@ -486,7 +486,7 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
Abc_ObjFanin1(pNode)->fMarkA == 0 )
nMuxes++;
}
printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
// printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
}
/**Function*************************************************************
src/base/abci/abcRewrite.c
+15 -5
View File
@@ -50,7 +50,7 @@ static void Abc_NodePrintCuts( Abc_Obj_t * pNode );
SeeAlso []
***********************************************************************/
int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose )
{
int fDrop = 0;
ProgressBar * pProgress;
@@ -67,7 +67,9 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
pManRwr = Rwr_ManStart( 0 );
if ( pManRwr == NULL )
return 0;
Abc_NtkStartReverseLevels( pNtk );
// compute the reverse levels if level update is requested
if ( fUpdateLevel )
Abc_NtkStartReverseLevels( pNtk );
// start the cut manager
clk = clock();
pManCut = Abc_NtkStartCutManForRewrite( pNtk, fDrop );
@@ -90,14 +92,16 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
if ( Abc_ObjFanoutNum(pNode) > 1000 )
continue;
// for each cut, try to resynthesize it
nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros );
nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros );
if ( nGain > 0 || nGain == 0 && fUseZeros )
{
Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr);
int fCompl = Rwr_ManReadCompl(pManRwr);
// complement the FF if needed
if ( fCompl ) Dec_GraphComplement( pGraph );
Dec_GraphUpdateNetwork( pNode, pGraph, nGain );
clk = clock();
Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
if ( fCompl ) Dec_GraphComplement( pGraph );
}
}
@@ -110,7 +114,13 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
Rwr_ManStop( pManRwr );
Cut_ManStop( pManCut );
pNtk->pManCut = NULL;
Abc_NtkStopReverseLevels( pNtk );
// put the nodes into the DFS order and reassign their IDs
Abc_NtkReassignIds( pNtk );
// fix the levels
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );
else
Abc_NtkGetLevelNum( pNtk );
// check
if ( !Abc_NtkCheck( pNtk ) )
{
src/base/abci/abcSat.c
+35 -16
View File
@@ -35,18 +35,18 @@ static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t *
Synopsis [Attempts to solve the miter using an internal SAT solver.]
Description [Returns 1 if the miter is SAT.]
Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
{
solver * pSat;
lbool status;
int clk;
int RetValue, clk;
assert( Abc_NtkIsBddLogic(pNtk) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
@@ -57,20 +57,18 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
// load clauses into the solver
clk = clock();
pSat = Abc_NtkMiterSatCreate( pNtk );
// printf( "Created SAT problem with %d variable and %d clauses. ",
// solver_nvars(pSat), solver_nclauses(pSat) );
// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
// simplify the problem
clk = clock();
status = solver_simplify(pSat);
// printf( "Simplified the problem to %d variables and %d clauses. ",
// solver_nvars(pSat), solver_nclauses(pSat) );
// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
if ( status == l_False )
{
solver_delete( pSat );
printf( "The problem is UNSAT after simplification.\n" );
printf( "The problem is UNSATISFIABLE after simplification.\n" );
return 0;
}
@@ -78,17 +76,38 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
clk = clock();
if ( fVerbose )
pSat->verbosity = 1;
status = solver_solve( pSat, NULL, NULL );
// if ( fVerbose )
// {
printf( "The problem is %5s. ", (status == l_True)? "SAT" : "UNSAT" );
PRT( "SAT solver time", clock() - clk );
// }
status = solver_solve( pSat, NULL, NULL, nSeconds );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
RetValue = -1;
}
else if ( status == l_True )
{
// printf( "The problem is SATISFIABLE.\n" );
RetValue = 0;
}
else if ( status == l_False )
{
// printf( "The problem is UNSATISFIABLE.\n" );
RetValue = 1;
}
else
assert( 0 );
// PRT( "SAT solver time", clock() - clk );
// if the problem is SAT, get the counterexample
if ( status == l_True )
{
Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
Vec_IntFree( vCiIds );
}
// free the solver
solver_delete( pSat );
return status == l_True;
return RetValue;
}
/**Function*************************************************************
Synopsis [Sets up the SAT solver.]
src/base/abci/abcSweep.c
-2
View File
@@ -25,8 +25,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
static stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
static void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
src/base/abci/abcVerify.c
+214 -46
View File
@@ -25,6 +25,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk );
static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -40,7 +44,7 @@
SeeAlso []
***********************************************************************/
void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
{
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pCnf;
@@ -54,13 +58,17 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 1 )
if ( RetValue == 0 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel );
return;
}
if ( RetValue == 0 )
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
@@ -77,10 +85,16 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
}
// solve the CNF using the SAT solver
if ( Abc_NtkMiterSat( pCnf, 0 ) )
RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 );
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT after SAT.\n" );
else
printf( "Networks are equivalent after SAT.\n" );
if ( pCnf->pModel )
Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel );
FREE( pCnf->pModel );
Abc_NtkDelete( pCnf );
}
@@ -96,11 +110,11 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
SeeAlso []
***********************************************************************/
void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
{
Fraig_Params_t Params;
Fraig_Man_t * pMan;
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pFraig;
int RetValue;
// get the miter of the two networks
@@ -111,13 +125,17 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 1 )
if ( RetValue == 0 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel );
return;
}
if ( RetValue == 0 )
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
@@ -127,21 +145,27 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
// convert the miter into a FRAIG
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
pFraig = Abc_NtkFraig( pMiter, &Params, 0 );
Abc_NtkDelete( pMiter );
if ( pFraig == NULL )
{
printf( "Fraiging has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pFraig );
Abc_NtkDelete( pFraig );
if ( RetValue == 0 )
{
Params.nSeconds = nSeconds;
pMan = Abc_NtkToFraig( pMiter, &Params, 0 );
Fraig_ManProveMiter( pMan );
// analyze the result
RetValue = Fraig_ManCheckMiter( pMan );
// report the result
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
else if ( RetValue == 1 )
printf( "Networks are equivalent after fraiging.\n" );
return;
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) );
}
printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
else assert( 0 );
// delete the fraig manager
Fraig_ManFree( pMan );
// delete the miter
Abc_NtkDelete( pMiter );
}
/**Function*************************************************************
@@ -155,7 +179,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
SeeAlso []
***********************************************************************/
void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames )
{
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pFrames;
@@ -170,13 +194,13 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 1 )
if ( RetValue == 0 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
return;
}
if ( RetValue == 0 )
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
@@ -192,13 +216,13 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
return;
}
RetValue = Abc_NtkMiterIsConstant( pFrames );
if ( RetValue == 1 )
if ( RetValue == 0 )
{
Abc_NtkDelete( pFrames );
printf( "Networks are NOT EQUIVALENT after framing.\n" );
return;
}
if ( RetValue == 0 )
if ( RetValue == 1 )
{
Abc_NtkDelete( pFrames );
printf( "Networks are equivalent after framing.\n" );
@@ -215,7 +239,10 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
}
// solve the CNF using the SAT solver
if ( Abc_NtkMiterSat( pCnf, 0 ) )
RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 );
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT after SAT.\n" );
else
printf( "Networks are equivalent after SAT.\n" );
@@ -233,11 +260,11 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
SeeAlso []
***********************************************************************/
void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose )
{
Fraig_Params_t Params;
Fraig_Man_t * pMan;
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pFraig;
Abc_Ntk_t * pFrames;
int RetValue;
@@ -249,13 +276,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 1 )
if ( RetValue == 0 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
return;
}
if ( RetValue == 0 )
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
@@ -271,13 +298,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
return;
}
RetValue = Abc_NtkMiterIsConstant( pFrames );
if ( RetValue == 1 )
if ( RetValue == 0 )
{
Abc_NtkDelete( pFrames );
printf( "Networks are NOT EQUIVALENT after framing.\n" );
return;
}
if ( RetValue == 0 )
if ( RetValue == 1 )
{
Abc_NtkDelete( pFrames );
printf( "Networks are equivalent after framing.\n" );
@@ -286,23 +313,164 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
// convert the miter into a FRAIG
Fraig_ParamsSetDefault( &Params );
pFraig = Abc_NtkFraig( pFrames, &Params, 0 );
Abc_NtkDelete( pFrames );
if ( pFraig == NULL )
{
printf( "Fraiging has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pFraig );
Abc_NtkDelete( pFraig );
if ( RetValue == 0 )
{
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
pMan = Abc_NtkToFraig( pFrames, &Params, 0 );
Fraig_ManProveMiter( pMan );
// analyze the result
RetValue = Fraig_ManCheckMiter( pMan );
// report the result
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
else if ( RetValue == 1 )
printf( "Networks are equivalent after fraiging.\n" );
return;
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
// Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) );
}
printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
else assert( 0 );
// delete the fraig manager
Fraig_ManFree( pMan );
// delete the miter
Abc_NtkDelete( pFrames );
}
/**Function*************************************************************
Synopsis [Reports mismatch between the two networks.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int * pValues1, * pValues2;
int nMisses, nPrinted, i, iNode = -1;
assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
// get the CO values under this model
pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
// count the mismatches
nMisses = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
nMisses += (int)( pValues1[i] != pValues2[i] );
printf( "Verification failed for %d outputs: ", nMisses );
// print the first 3 outputs
nPrinted = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
if ( pValues1[i] != pValues2[i] )
{
if ( iNode == -1 )
iNode = i;
printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
if ( ++nPrinted == 3 )
break;
}
if ( nPrinted != nMisses )
printf( " ..." );
printf( "\n" );
// report mismatch for the first output
if ( iNode >= 0 )
{
printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n",
Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] );
printf( "Input pattern: " );
// collect PIs in the cone
pNode = Abc_NtkCo(pNtk1,iNode);
vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
// set the PI numbers
Abc_NtkForEachCi( pNtk1, pNode, i )
pNode->pCopy = (void*)i;
// print the model
Vec_PtrForEachEntry( vNodes, pNode, i )
{
assert( Abc_ObjIsCi(pNode) );
printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] );
}
printf( "\n" );
Vec_PtrFree( vNodes );
}
free( pValues1 );
free( pValues2 );
}
/**Function*************************************************************
Synopsis [Returns a dummy pattern full of zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk )
{
int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
return pModel;
}
/**Function*************************************************************
Synopsis [Returns the PO values under the given input pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int * pValues, Value0, Value1, i;
int fStrashed = 0;
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash(pNtk, 0, 0);
fStrashed = 1;
}
// increment the trav ID
Abc_NtkIncrementTravId( pNtk );
// set the CI values
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (void *)pModel[i];
// simulate in the topological order
vNodes = Abc_NtkDfs( pNtk, 1 );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_NodeIsConst(pNode) )
pNode->pCopy = NULL;
else
{
Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
pNode->pCopy = (void *)(Value0 & Value1);
}
}
Vec_PtrFree( vNodes );
// fill the output values
pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
if ( fStrashed )
Abc_NtkDelete( pNtk );
return pValues;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
src/base/abcs/abcSeq.c
+1 -1
View File
@@ -112,7 +112,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
if ( Abc_ObjIsCi(pFaninNew) || !Abc_NodeIsConst(pFaninNew) )
continue;
pConst = Abc_ObjNotCond( Abc_AigConst1(pManNew), Abc_ObjFaninC0(pLatch) );
Abc_AigReplace( pManNew, pLatch, pConst );
Abc_AigReplace( pManNew, pLatch, pConst, 0 );
fChange = 1;
Counter++;
}
src/base/main/main.c
+63 -2
View File
@@ -20,6 +20,9 @@
#include "mainInt.h"
// this line should be included in the library project
#define _LIB
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -30,6 +33,8 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s);
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
#ifndef _LIB
/**Function*************************************************************
Synopsis [The main() procedure.]
@@ -64,8 +69,8 @@ int main( int argc, char * argv[] )
fInitRead = 0;
fFinalWrite = 0;
sInFile = sOutFile = NULL;
sprintf( sReadCmd, "read_blif_mv" );
sprintf( sWriteCmd, "write_blif_mv" );
sprintf( sReadCmd, "read" );
sprintf( sWriteCmd, "write" );
util_getopt_reset();
while ((c = util_getopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
@@ -226,6 +231,62 @@ usage:
return 1;
}
#endif
/**Function*************************************************************
Synopsis [Initialization procedure for the library project.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_Start()
{
Abc_Frame_t * pAbc;
// added to detect memory leaks:
#ifdef _DEBUG
_CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
#endif
// get global frame (singleton pattern)
// will be initialized on first call
pAbc = Abc_FrameGetGlobalFrame();
// source the resource file
Abc_UtilsSource( pAbc );
}
/**Function*************************************************************
Synopsis [Deallocation procedure for the library project.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_Stop()
{
Abc_Frame_t * pAbc;
int fStatus = 0;
// if the memory should be freed, quit packages
if ( fStatus == -2 )
{
pAbc = Abc_FrameGetGlobalFrame();
// perform uninitializations
Abc_FrameEnd( pAbc );
// stop the framework
Abc_FrameDeallocate( pAbc );
}
}
/**Function********************************************************************
src/base/main/main.h
+5 -1
View File
@@ -73,7 +73,11 @@ typedef struct Abc_Frame_t_ Abc_Frame_t;
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/*=== mvFrame.c ===========================================================*/
/*=== main.c ===========================================================*/
extern void Abc_Start();
extern void Abc_Stop();
/*=== mainFrame.c ===========================================================*/
extern Abc_Ntk_t * Abc_FrameReadNet( Abc_Frame_t * p );
extern FILE * Abc_FrameReadOut( Abc_Frame_t * p );
extern FILE * Abc_FrameReadErr( Abc_Frame_t * p );
src/opt/dec/dec.h
+1 -1
View File
@@ -97,7 +97,7 @@ struct Dec_Man_t_
/*=== decAbc.c ========================================================*/
extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph );
extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain );
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
/*=== decFactor.c ========================================================*/
extern Dec_Graph_t * Dec_Factor( char * pSop );
/*=== decMan.c ========================================================*/
src/opt/dec/decAbc.c
+3 -3
View File
@@ -126,7 +126,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) )
LevelNew = (int)Abc_ObjRegular(pAnd1)->Level;
LevelOld = (int)Abc_ObjRegular(pAnd)->Level;
assert( LevelNew == LevelOld );
// assert( LevelNew == LevelOld );
}
if ( LevelNew > LevelMax )
return -1;
@@ -148,7 +148,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
SeeAlso []
***********************************************************************/
void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain )
void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain )
{
Abc_Obj_t * pRootNew;
Abc_Ntk_t * pNtk = pRoot->pNtk;
@@ -157,7 +157,7 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain
// create the new structure of nodes
pRootNew = Dec_GraphToNetwork( pNtk->pManFunc, pGraph );
// remove the old nodes
Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew );
Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
// compare the gains
nNodesNew = Abc_NtkNodeNum(pNtk);
assert( nGain <= nNodesOld - nNodesNew );
src/opt/rwr/rwr.h
+7 -2
View File
@@ -49,6 +49,7 @@ struct Rwr_Man_t_
char * pPhases; // canonical phases
char * pPerms; // canonical permutations
unsigned char * pMap; // mapping of functions into class numbers
unsigned short * pMapInv; // mapping of classes into functions
char * pPractical; // practical NPN classes
char ** pPerms4; // four-var permutations
// node space
@@ -63,10 +64,11 @@ struct Rwr_Man_t_
int nClasses; // the number of NN classes
// the result of resynthesis
int fCompl; // indicates if the output of FF should be complemented
void * pGraph; // the decomposition tree (temporary)
void * pGraph; // the decomposition tree (temporary)
Vec_Ptr_t * vFanins; // the fanins array (temporary)
Vec_Ptr_t * vFaninsCur; // the fanins array (temporary)
Vec_Int_t * vLevNums; // the array of levels (temporary)
Vec_Ptr_t * vNodesTemp; // the nodes in MFFC (temporary)
// node statistics
int nNodesConsidered;
int nNodesRewritten;
@@ -80,6 +82,8 @@ struct Rwr_Man_t_
int timeCut;
int timeRes;
int timeEval;
int timeMffc;
int timeUpdate;
int timeTotal;
};
@@ -114,7 +118,7 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_N
/*=== rwrDec.c ========================================================*/
extern void Rwr_ManPreprocess( Rwr_Man_t * p );
/*=== rwrEva.c ========================================================*/
extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros );
extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros );
/*=== rwrLib.c ========================================================*/
extern void Rwr_ManPrecompute( Rwr_Man_t * p );
extern Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute );
@@ -128,6 +132,7 @@ extern void Rwr_ManPrintStats( Rwr_Man_t * p );
extern void * Rwr_ManReadDecs( Rwr_Man_t * p );
extern int Rwr_ManReadCompl( Rwr_Man_t * p );
extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
extern void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time );
extern void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time );
/*=== rwrPrint.c ========================================================*/
extern void Rwr_ManPrint( Rwr_Man_t * p );
src/opt/rwr/rwrDec.c
+3
View File
@@ -49,6 +49,8 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
Rwr_Node_t * pNode;
int i, k;
// put the nodes into the structure
p->pMapInv = ALLOC( unsigned short, 222 );
memset( p->pMapInv, 0, sizeof(unsigned short) * 222 );
p->vClasses = Vec_VecStart( 222 );
for ( i = 0; i < p->nFuncs; i++ )
{
@@ -60,6 +62,7 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
assert( pNode->uTruth == p->pTable[i]->uTruth );
assert( p->pMap[pNode->uTruth] >= 0 && p->pMap[pNode->uTruth] < 222 );
Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
p->pMapInv[ p->pMap[pNode->uTruth] ] = p->puCanons[pNode->uTruth];
}
}
// compute decomposition forms for each node and verify them
src/opt/rwr/rwrEva.c
+4 -2
View File
@@ -49,7 +49,7 @@ static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_
SeeAlso []
***********************************************************************/
int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros )
int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros )
{
int fVeryVerbose = 0;
Dec_Graph_t * pGraph;
@@ -63,7 +63,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
p->nNodesConsidered++;
// get the required times
Required = Abc_NodeReadRequiredLevel( pNode );
Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
// get the node's cuts
clk = clock();
pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode );
@@ -98,6 +98,7 @@ clk = clock();
}
p->nCutsGood++;
clk2 = clock();
// mark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Abc_ObjRegular(pFanin)->vFanouts.nSize++;
@@ -107,6 +108,7 @@ clk = clock();
// unmark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Abc_ObjRegular(pFanin)->vFanouts.nSize--;
p->timeMffc += clock() - clk2;
// evaluate the cut
clk2 = clock();
src/opt/rwr/rwrMan.c
+23 -2
View File
@@ -75,6 +75,7 @@ clk = clock();
p->vLevNums = Vec_IntAlloc( 50 );
p->vFanins = Vec_PtrAlloc( 50 );
p->vFaninsCur = Vec_PtrAlloc( 50 );
p->vNodesTemp = Vec_PtrAlloc( 50 );
if ( fPrecompute )
{ // precompute subgraphs
Rwr_ManPrecompute( p );
@@ -112,11 +113,13 @@ void Rwr_ManStop( Rwr_Man_t * p )
Dec_GraphFree( (Dec_Graph_t *)pNode->pNext );
}
if ( p->vClasses ) Vec_VecFree( p->vClasses );
Vec_PtrFree( p->vNodesTemp );
Vec_PtrFree( p->vForest );
Vec_IntFree( p->vLevNums );
Vec_PtrFree( p->vFanins );
Vec_PtrFree( p->vFaninsCur );
Extra_MmFixedStop( p->pMmNode, 0 );
FREE( p->pMapInv );
free( p->pTable );
free( p->pPractical );
free( p->pPerms4 );
@@ -151,14 +154,16 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
PRT( "Start ", p->timeStart );
PRT( "Cuts ", p->timeCut );
PRT( "Resynthesis ", p->timeRes );
PRT( " Mffc ", p->timeMffc );
PRT( " Eval ", p->timeEval );
PRT( "Update ", p->timeUpdate );
PRT( "TOTAL ", p->timeTotal );
/*
printf( "The scores are : " );
printf( "The scores are:\n" );
for ( i = 0; i < 222; i++ )
if ( p->nScores[i] > 0 )
printf( "%d=%d ", i, p->nScores[i] );
printf( "%3d = %8d canon = %5d\n", i, p->nScores[i], p->pMapInv[i] );
printf( "\n" );
*/
}
@@ -211,6 +216,22 @@ void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time )
p->timeCut += Time;
}
/**Function*************************************************************
Synopsis [Stops the resynthesis manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time )
{
p->timeUpdate += Time;
}
/**Function*************************************************************
Synopsis [Stops the resynthesis manager.]
src/opt/rwr/rwrPrint.c
+29 -2
View File
@@ -77,6 +77,33 @@ void Rwr_GetBushVolume( Rwr_Man_t * p, int Entry, int * pVolume, int * pnFuncs )
*pnFuncs = nFuncs;
}
/**Function*************************************************************
Synopsis [Adds the node to the end of the list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Rwr_GetBushSumOfVolumes( Rwr_Man_t * p, int Entry )
{
Rwr_Node_t * pNode;
int Volume, VolumeTotal = 0;
for ( pNode = p->pTable[Entry]; pNode; pNode = pNode->pNext )
{
if ( pNode->uTruth != p->puCanons[pNode->uTruth] )
continue;
Volume = 0;
Rwr_ManIncTravId( p );
Rwr_Trav2_rec( p, pNode, &Volume );
VolumeTotal += Volume;
}
return VolumeTotal;
}
/**Function*************************************************************
Synopsis [Prints one rwr node.]
@@ -219,9 +246,9 @@ void Rwr_ManPrint( Rwr_Man_t * p )
continue;
if ( i != p->puCanons[i] )
continue;
fprintf( pFile, "\nClass %3d. Func %6d. ", p->pMap[i], Counter++ );
fprintf( pFile, "\nClass %3d. Func %6d. ", p->pMap[i], Counter++ );
Rwr_GetBushVolume( p, i, &Volume, &nFuncs );
fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
fprintf( pFile, "Roots = %3d. Vol = %3d. Sum = %3d. ", nFuncs, Volume, Rwr_GetBushSumOfVolumes(p, i) );
uTruth = i;
Extra_PrintBinary( pFile, &uTruth, 16 );
fprintf( pFile, "\n" );
src/opt/sim/simSupp.c
+1 -2
View File
@@ -35,8 +35,6 @@ static void Sim_UtilAssignFromFifo( Sim_Man_t * p );
static void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters );
static int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output );
extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -469,6 +467,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
// transform the miter into a fraig
Fraig_ParamsSetDefault( &Params );
Params.nSeconds = ABC_INFINITY;
Params.fInternal = 1;
clk = clock();
pMan = Abc_NtkToFraig( pMiter, &Params, 0 );
src/opt/sim/simSymSat.c
+2 -2
View File
@@ -26,8 +26,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -145,6 +144,7 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned *
Params.fInternal = 1;
Params.nPatsRand = 512;
Params.nPatsDyna = 512;
Params.nSeconds = ABC_INFINITY;
clk = clock();
pMan = Abc_NtkToFraig( pMiter, &Params, 0 );
src/sat/asat/added.c
+24
View File
@@ -119,6 +119,30 @@ void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
fprintf( pFile, "\n" );
}
/**Function*************************************************************
Synopsis [Returns a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * solver_get_model( solver * p, int * pVars, int nVars )
{
int * pModel;
int i;
pModel = ALLOC( int, nVars );
for ( i = 0; i < nVars; i++ )
{
assert( pVars[i] >= 0 && pVars[i] < p->size );
pModel[i] = (int)(p->model.ptr[pVars[i]] == (void *)l_True);
}
return pModel;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/asat/solver.c
+7 -2
View File
@@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <stdio.h>
#include <assert.h>
#include <math.h>
#include <time.h>
#include "solver.h"
@@ -1055,13 +1056,14 @@ bool solver_simplify(solver* s)
}
bool solver_solve(solver* s, lit* begin, lit* end)
int solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
{
double nof_conflicts = 100;
double nof_learnts = solver_nclauses(s) / 3;
lbool status = l_Undef;
lbool* values = s->assigns;
lit* i;
int timeStart = clock();
for (i = begin; i < end; i++)
if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
@@ -1096,12 +1098,15 @@ bool solver_solve(solver* s, lit* begin, lit* end)
status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
nof_conflicts *= 1.5;
nof_learnts *= 1.1;
// if the runtime limit is exceeded, quit the restart loop
if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC )
break;
}
if (s->verbosity >= 1)
printf("==============================================================================\n");
solver_canceluntil(s,0);
return status != l_False;
return status;
}
src/sat/asat/solver.h
+2 -1
View File
@@ -69,7 +69,8 @@ extern void solver_delete(solver* s);
extern bool solver_addclause(solver* s, lit* begin, lit* end);
extern bool solver_simplify(solver* s);
extern bool solver_solve(solver* s, lit* begin, lit* end);
extern int solver_solve(solver* s, lit* begin, lit* end, int nSeconds);
extern int * solver_get_model( solver * p, int * pVars, int nVars );
extern int solver_nvars(solver* s);
extern int solver_nclauses(solver* s);
src/sat/csat/csat_apis.c
+76 -36
View File
@@ -24,6 +24,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define ABC_DEFAULT_TIMEOUT 60 // 60 seconds
struct CSAT_ManagerStruct_t
{
// information about the problem
@@ -33,7 +35,8 @@ struct CSAT_ManagerStruct_t
Abc_Ntk_t * pTarget; // the AIG representing the target
char * pDumpFileName; // the name of the file to dump the target network
// solving parameters
int mode; // 0 = baseline; 1 = resource-aware fraiging
int mode; // 0 = brute-force SAT; 1 = resource-aware FRAIG
int nSeconds; // time limit for pure SAT solving
Fraig_Params_t Params; // the set of parameters to call FRAIG package
// information about the target
int nog; // the numbers of gates in the target
@@ -44,11 +47,9 @@ struct CSAT_ManagerStruct_t
};
static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
static void CSAT_TargetResFree( CSAT_Target_ResultT * p );
static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode );
// some external procedures
extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
////////////////////////////////////////////////////////////////////////
@@ -77,6 +78,7 @@ CSAT_Manager CSAT_InitManager()
mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
mng->vNodes = Vec_PtrAlloc( 100 );
mng->vValues = Vec_IntAlloc( 100 );
mng->nSeconds = ABC_DEFAULT_TIMEOUT;
return mng;
}
@@ -107,7 +109,7 @@ void CSAT_QuitManager( CSAT_Manager mng )
Synopsis [Sets solver options for learning.]
Description [0 = baseline; 1 = resource-aware solving.]
Description [0 = brute-force SAT; 1 = resource-aware FRAIG.]
SideEffects []
@@ -118,11 +120,11 @@ void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
{
mng->mode = option;
if ( option == 0 )
printf( "CSAT_SetSolveOption: Setting baseline solving mode.\n" );
printf( "CSAT_SetSolveOption: Setting brute-force SAT mode.\n" );
else if ( option == 1 )
printf( "CSAT_SetSolveOption: Setting resource-aware solving mode.\n" );
printf( "CSAT_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
else
printf( "CSAT_SetSolveOption: Unknown option.\n" );
printf( "CSAT_SetSolveOption: Unknown solving mode.\n" );
}
@@ -280,7 +282,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
assert( Abc_NtkLatchNum(pNtk) == 0 );
// make sure everything is okay with the network structure
if ( !Abc_NtkCheckRead( pNtk ) )
if ( !Abc_NtkDoCheck( pNtk ) )
{
printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
return 0;
@@ -311,7 +313,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
***********************************************************************/
void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
{
printf( "CSAT_SetTimeLimit: The resource limit is not implemented (warning).\n" );
mng->nSeconds = runtime;
}
/**Function*************************************************************
@@ -458,7 +460,8 @@ void CSAT_SolveInit( CSAT_Manager mng )
memset( pParams, 0, sizeof(Fraig_Params_t) );
pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info
pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info
pParams->nBTLimit = 99; // the max number of backtracks to perform at a node
pParams->nBTLimit = 10; // the max number of backtracks to perform at a node
pParams->nSeconds = mng->nSeconds; // the time out for the final proof
pParams->fFuncRed = mng->mode; // performs only one level hashing
pParams->fFeedBack = 1; // enables solver feedback
pParams->fDist1Pats = 1; // enables distance-1 patterns
@@ -498,6 +501,7 @@ void CSAT_AnalyzeTargets( CSAT_Manager mng )
enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
{
Fraig_Man_t * pMan;
Abc_Ntk_t * pCnf;
int * pModel;
int RetValue, i;
@@ -505,34 +509,68 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
if ( mng->pTarget == NULL )
{ printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; }
// transform the target into a fraig
pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 );
Fraig_ManProveMiter( pMan );
// optimizations of the target go here
// for example, to enable one pass of rewriting, uncomment this line
// Abc_NtkRewrite( mng->pTarget, 0, 1, 0 );
// analyze the result
mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
RetValue = Fraig_ManCheckMiter( pMan );
if ( RetValue == -1 )
mng->pResult->status = UNDETERMINED;
else if ( RetValue == 1 )
mng->pResult->status = UNSATISFIABLE;
else if ( RetValue == 0 )
if ( mng->mode == 0 ) // brute-force SAT
{
mng->pResult->status = SATISFIABLE;
pModel = Fraig_ManReadModel( pMan );
assert( pModel != NULL );
// create the array of PI names and values
for ( i = 0; i < mng->pResult->no_sig; i++ )
// transfor the AIG into a logic network for efficient CNF construction
pCnf = Abc_NtkRenode( mng->pTarget, 0, 100, 1, 0, 0 );
RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 );
// analyze the result
mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
if ( RetValue == -1 )
mng->pResult->status = UNDETERMINED;
else if ( RetValue == 1 )
mng->pResult->status = UNSATISFIABLE;
else if ( RetValue == 0 )
{
mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
mng->pResult->values[i] = pModel[i];
mng->pResult->status = SATISFIABLE;
// create the array of PI names and values
for ( i = 0; i < mng->pResult->no_sig; i++ )
{
mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
mng->pResult->values[i] = pCnf->pModel[i];
}
FREE( mng->pTarget->pModel );
}
else assert( 0 );
Abc_NtkDelete( pCnf );
}
else
else if ( mng->mode == 1 ) // resource-aware fraiging
{
// transform the target into a fraig
pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 );
Fraig_ManProveMiter( pMan );
RetValue = Fraig_ManCheckMiter( pMan );
// analyze the result
mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
if ( RetValue == -1 )
mng->pResult->status = UNDETERMINED;
else if ( RetValue == 1 )
mng->pResult->status = UNSATISFIABLE;
else if ( RetValue == 0 )
{
mng->pResult->status = SATISFIABLE;
pModel = Fraig_ManReadModel( pMan );
assert( pModel != NULL );
// create the array of PI names and values
for ( i = 0; i < mng->pResult->no_sig; i++ )
{
mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
mng->pResult->values[i] = pModel[i];
}
}
else assert( 0 );
// delete the fraig manager
Fraig_ManFree( pMan );
}
else
assert( 0 );
// delete the fraig manager
Fraig_ManFree( pMan );
// delete the target
Abc_NtkDelete( mng->pTarget );
mng->pTarget = NULL;
@@ -558,9 +596,9 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
/**Function*************************************************************
Synopsis [Dumps the target AIG into the BENCH file.]
Synopsis [Dumps the original network into the BENCH file.]
Description []
Description [This procedure should be modified to dump the target.]
SideEffects []
@@ -569,11 +607,13 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
***********************************************************************/
void CSAT_Dump_Bench_File( CSAT_Manager mng )
{
Abc_Ntk_t * pNtkTemp;
Abc_Ntk_t * pNtkTemp, * pNtkAig;
char * pFileName;
// derive the netlist
pNtkTemp = Abc_NtkLogicToNetlistBench( mng->pTarget );
pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0 );
pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig );
Abc_NtkDelete( pNtkAig );
if ( pNtkTemp == NULL )
{ printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
src/sat/csat/csat_apis.h
+4
View File
@@ -167,6 +167,10 @@ extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
extern void CSAT_Dump_Bench_File(CSAT_Manager mng);
// ADDED PROCEDURES:
extern void CSAT_QuitManager( CSAT_Manager mng );
extern void CSAT_TargetResFree( CSAT_Target_ResultT * p );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/fraig/fraig.h
+3 -2
View File
@@ -43,6 +43,7 @@ struct Fraig_ParamsStruct_t_
int nPatsRand; // the number of words of random simulation info
int nPatsDyna; // the number of words of dynamic simulation info
int nBTLimit; // the max number of backtracks to perform
int nSeconds; // the timeout for the final proof
int fFuncRed; // performs only one level hashing
int fFeedBack; // enables solver feedback
int fDist1Pats; // enables distance-1 patterns
@@ -162,8 +163,8 @@ extern int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pO
extern int Fraig_CountLevels( Fraig_Man_t * pMan );
/*=== fraigSat.c =============================================================*/
extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit );
extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
extern void Fraig_ManProveMiter( Fraig_Man_t * p );
extern int Fraig_ManCheckMiter( Fraig_Man_t * p );
src/sat/fraig/fraigCanon.c
+1 -1
View File
@@ -167,7 +167,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
// there is another node which looks the same according to simulation
// use SAT to resolve the ambiguity
if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit ) )
if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
{
// set the node to be equivalent with this node
// to prevent loops, only set if the old node is not in the TFI of the new node
src/sat/fraig/fraigInt.h
+1
View File
@@ -143,6 +143,7 @@ struct Fraig_ManStruct_t_
int nWordsRand; // the number of words of random simulation info
int nWordsDyna; // the number of words of dynamic simulation info
int nBTLimit; // the max number of backtracks to perform
int nSeconds; // the runtime limit for the miter proof
int fFuncRed; // performs only one level hashing
int fFeedBack; // enables solver feedback
int fDist1Pats; // enables solver feedback
src/sat/fraig/fraigMan.c
+2
View File
@@ -46,6 +46,7 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info
pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
pParams->nBTLimit = 99; // the max number of backtracks to perform
pParams->nSeconds = 20; // the max number of seconds to solve the miter
pParams->fFuncRed = 1; // performs only one level hashing
pParams->fFeedBack = 1; // enables solver feedback
pParams->fDist1Pats = 1; // enables distance-1 patterns
@@ -100,6 +101,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand ); // the number of words of random simulation info
p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna ); // the number of patterns for dynamic simulation info
p->nBTLimit = pParams->nBTLimit; // -1 means infinite backtrack limit
p->nSeconds = pParams->nSeconds; // the timeout for the final miter
p->fFuncRed = pParams->fFuncRed; // enables functional reduction (otherwise, only one-level hashing is performed)
p->fFeedBack = pParams->fFeedBack; // enables solver feedback (the use of counter-examples in simulation)
p->fDist1Pats = pParams->fDist1Pats; // enables solver feedback (the use of counter-examples in simulation)
src/sat/fraig/fraigSat.c
+7 -7
View File
@@ -56,13 +56,13 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i );
SeeAlso []
***********************************************************************/
int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit )
{
if ( pNode1 == pNode2 )
return 1;
if ( pNode1 == Fraig_Not(pNode2) )
return 0;
return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit );
return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
}
/**Function*************************************************************
@@ -95,7 +95,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
// skip nodes that are different according to simulation
if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
continue;
if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1 ) )
if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
{
if ( Fraig_IsComplement(p->vOutputs->pArray[i]) )
p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
@@ -160,7 +160,7 @@ int Fraig_ManCheckMiter( Fraig_Man_t * p )
SeeAlso []
***********************************************************************/
int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit )
{
int RetValue, RetValue1, i, fComp, clk;
int fVerbose = 0;
@@ -227,7 +227,7 @@ if ( fVerbose )
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
// run the solver
clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
if ( RetValue1 == MSAT_FALSE )
@@ -286,7 +286,7 @@ p->time3 += clock() - clk;
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
// run the solver
clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
if ( RetValue1 == MSAT_FALSE )
{
@@ -411,7 +411,7 @@ if ( fVerbose )
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
// run the solver
clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
p->timeSat += clock() - clk;
if ( RetValue1 == MSAT_FALSE )
src/sat/msat/msat.h
+1 -1
View File
@@ -79,7 +79,7 @@ extern bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p
extern bool Msat_SolverAddVar( Msat_Solver_t * p );
extern bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
extern bool Msat_SolverSimplifyDB( Msat_Solver_t * p );
extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit );
extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
// printing stats, assignments, and clauses
extern void Msat_SolverPrintStats( Msat_Solver_t * p );
extern void Msat_SolverPrintAssignment( Msat_Solver_t * p );
src/sat/msat/msatSolverCore.c
+5 -1
View File
@@ -131,11 +131,12 @@ void Msat_SolverPrintStats( Msat_Solver_t * p )
SeeAlso []
***********************************************************************/
bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit )
bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
{
Msat_SearchParams_t Params = { 0.95, 0.999 };
double nConflictsLimit, nLearnedLimit;
Msat_Type_t Status;
int timeStart = clock();
int64 nConflictsOld = p->Stats.nConflicts;
int64 nDecisionsOld = p->Stats.nDecisions;
@@ -174,6 +175,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
// if the limit on the number of backtracks is given, quit the restart loop
if ( nBackTrackLimit > 0 )
break;
// if the runtime limit is exceeded, quit the restart loop
if ( clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
break;
}
Msat_SolverCancelUntil( p, 0 );
p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;