From 06ba3d3e6ceee78cf52c024ac56287e924b00af3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 17 Apr 2013 22:18:43 -0700 Subject: Adding command &filter_equiv to filter candidate equivalence classes using indexes of disproved POs after handling SRM as a multi-output miter. --- src/aig/gia/giaEquiv.c | 142 ++++++++++++++++++++++++++++++++++------------ src/base/abci/abc.c | 50 +++++++++++++++- src/base/main/main.h | 1 + src/base/main/mainFrame.c | 3 + src/base/main/mainInt.h | 1 + src/python/pyabc.i | 22 +++++++ 6 files changed, 183 insertions(+), 36 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index c7d4d5c7..a2cde10c 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -724,7 +724,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide ) +static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap ) { Gia_Obj_t * pRepr; unsigned iLitNew; @@ -740,7 +740,11 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t if ( vTrace ) Vec_IntPush( vTrace, 1 ); if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) ) + { + if ( vMap ) + Vec_IntPush( vMap, Gia_ObjId(p, pObj) ); Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); + } } else { @@ -751,29 +755,6 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t pObj->Value = iLitNew; } -/**Function************************************************************* - - Synopsis [Returns 1 if AIG has dangling nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManHasNoEquivs( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj; - int i; - if ( p->pReprs == NULL ) - return 1; - Gia_ManForEachObj( p, pObj, i ) - if ( Gia_ObjReprObj(p, i) != NULL ) - break; - return i == Gia_ManObjNum(p); -} - /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] @@ -785,15 +766,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide ) +void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap ) { if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap ); } /**Function************************************************************* @@ -807,7 +788,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace ) +Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMap ) { Vec_Int_t * vXorLits; Gia_Man_t * pNew, * pTemp; @@ -830,9 +811,9 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace ) Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManForEachRo( p, pObj, i ) - Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL, vMap ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL, vMap ); Gia_ManForEachPo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Vec_IntForEachEntry( vXorLits, iLitNew, i ) @@ -883,7 +864,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int if ( fSkipSome ) { vGuide = Vec_IntAlloc( 100 ); - pTemp = Gia_ManSpecReduceTrace( p, vGuide ); + pTemp = Gia_ManSpecReduceTrace( p, vGuide, NULL ); Gia_ManStop( pTemp ); assert( Vec_IntSize(vGuide) == Gia_ManEquivCountLitsAll(p) ); vTrace = Vec_IntAlloc( 100 ); @@ -901,9 +882,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManForEachRo( p, pObj, i ) - Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL ); if ( !fSynthesis ) { Gia_ManForEachPo( p, pObj, i ) @@ -1212,7 +1193,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb if ( fSkipSome ) { Vec_Int_t * vTrace = Vec_IntAlloc( 100 ); - pTemp = Gia_ManSpecReduceTrace( p, vTrace ); + pTemp = Gia_ManSpecReduceTrace( p, vTrace, NULL ); Gia_ManStop( pTemp ); assert( Vec_IntSize(vTrace) == nLitsAll ); // count the number of non-zero entries @@ -1277,6 +1258,74 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb Gia_ManStop( pMiter ); } +/**Function************************************************************* + + Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose ) +{ + Gia_Man_t * pSrm; + Vec_Int_t * vTrace, * vMap; + int i, iObjId, Entry, Prev = -1; + // check if there are equivalences + if ( p->pReprs == NULL || p->pNexts == NULL ) + { + Abc_Print( 1, "Gia_ManEquivFilter(): Equivalence classes are not defined.\n" ); + return; + } + // check if PO indexes are available + if ( vPoIds == NULL ) + { + Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs is not available.\n" ); + return; + } + if ( Vec_IntSize(vPoIds) == 0 ) + return; + // create SRM with mapping into POs + vMap = Vec_IntAlloc( 1000 ); + vTrace = Vec_IntAlloc( 1000 ); + pSrm = Gia_ManSpecReduceTrace( p, vTrace, vMap ); + // the resulting array (vMap) maps PO indexes of the SRM into object IDs + assert( Vec_IntSize(vMap) == Gia_ManPoNum(pSrm) ); + Vec_IntFree( vTrace ); + Gia_ManStop( pSrm ); + // check if disproved POs satisfy the range + Vec_IntSort( vPoIds, 0 ); + Vec_IntForEachEntry( vPoIds, Entry, i ) + { + if ( Entry < 0 || Entry >= Gia_ManPoNum(p) ) + { + Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains PO index (%d),\n", Entry ); + Abc_Print( 1, "which does not fit into the range of available PO indexes of the SRM: [%d; %d].\n", Entry, 0, Vec_IntSize(vMap)-1 ); + Vec_IntFree( vMap ); + return; + } + if ( Prev == Entry ) + { + Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains at least one duplicate entry (%d),\n", Entry ); + Vec_IntFree( vMap ); + return; + } + Prev = Entry; + } + // perform the reduction of the equivalence classes + Vec_IntForEachEntry( vPoIds, Entry, i ) + { + iObjId = Vec_IntEntry( vMap, Entry ); + Gia_ObjUnsetRepr( p, iObjId ); +// Gia_ObjSetNext( p, iObjId, 0 ); + } + ABC_FREE( p->pNexts ); + p->pNexts = Gia_ManDeriveNexts( p ); +} + /**Function************************************************************* Synopsis [Transforms equiv classes by setting a good representative.] @@ -1642,6 +1691,29 @@ ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START +/**Function************************************************************* + + Synopsis [Returns 1 if AIG has dangling nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManHasNoEquivs( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + if ( p->pReprs == NULL ) + return 1; + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjReprObj(p, i) != NULL ) + break; + return i == Gia_ManObjNum(p); +} + /**Function************************************************************* Synopsis [Implements iteration during speculation.] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1d8bc34c..af1c8ecf 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -354,6 +354,7 @@ static int Abc_CommandAbc9Srm2 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Filter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9EquivFilter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Verify ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -849,6 +850,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&filter", Abc_CommandAbc9Filter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reduce", Abc_CommandAbc9Reduce, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&equiv_filter", Abc_CommandAbc9EquivFilter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&verify", Abc_CommandAbc9Verify, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sweep", Abc_CommandAbc9Sweep, 0 ); @@ -27518,7 +27520,7 @@ int Abc_CommandAbc9EquivMark( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Reduce(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9EquivMark(): There is no AIG.\n" ); return 1; } if ( argc != globalUtilOptind + 1 ) @@ -27547,6 +27549,52 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9EquivFilter( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose ); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9EquivFilter(): There is no AIG.\n" ); + return 1; + } + Gia_ManEquivFilter( pAbc->pGia, pAbc->vAbcObjIds, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &equiv_filter [-vh]\n" ); + Abc_Print( -2, "\t filters equivalence candidates after disproving some SRM outputs\n" ); + Abc_Print( -2, "\t (the array of disproved outputs should be given as pAbc->vAbcObjIds)\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/main/main.h b/src/base/main/main.h index 4257d623..34678479 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -116,6 +116,7 @@ extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p ); extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ); +extern ABC_DLL Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadCexRegNum( Abc_Frame_t * p ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 8c3344ff..a525afb6 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -65,6 +65,7 @@ int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFr Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; } Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; } Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; } +Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ) { return s_GlobalFrame->vAbcObjIds; } int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; } int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; } @@ -142,6 +143,7 @@ Abc_Frame_t * Abc_FrameAllocate() p->fBatchMode = 0; // networks to be used by choice p->vStore = Vec_PtrAlloc( 16 ); + p->vAbcObjIds = Vec_IntAlloc( 0 ); // initialize decomposition manager // define_cube_size(20); // set_espresso_flags(); @@ -172,6 +174,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) // undefine_cube_size(); Rwt_ManGlobalStop(); // Ivy_TruthManStop(); + if ( p->vAbcObjIds) Vec_IntFree( p->vAbcObjIds ); if ( p->vCexVec ) Vec_PtrFreeFree( p->vCexVec ); if ( p->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs ); if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL ); diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 9813061e..2d5bf4c8 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -101,6 +101,7 @@ struct Abc_Frame_t_ Abc_Cex_t * pCex2; // copy of the above Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs + Vec_Int_t * vAbcObjIds; // object IDs int Status; // the status of verification problem (proved=1, disproved=0, undecided=-1) int nFrames; // the number of time frames completed by BMC Vec_Ptr_t * vPlugInComBinPairs; // pairs of command and its binary name diff --git a/src/python/pyabc.i b/src/python/pyabc.i index 907dec84..e071a74a 100644 --- a/src/python/pyabc.i +++ b/src/python/pyabc.i @@ -320,6 +320,20 @@ PyObject* eq_classes() return eq_classes; } +void _pyabc_array_clear() +{ + Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame(); + Vec_Int_t *vObjIds = Abc_FrameReadObjIds(pAbc); + Vec_IntClear( vObjIds ); +} + +void _pyabc_array_push(int i) +{ + Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame(); + Vec_Int_t *vObjIds = Abc_FrameReadObjIds(pAbc); + Vec_IntPush( vObjIds, i ); +} + static PyObject* pyabc_internal_python_command_callback = 0; void pyabc_internal_set_command_callback( PyObject* callback ) @@ -644,6 +658,9 @@ int _cex_get_frame(Abc_Cex_t* pCex); PyObject* eq_classes(); +void _pyabc_array_clear(); +void _pyabc_array_push(int i); + void pyabc_internal_set_command_callback( PyObject* callback ); void pyabc_internal_register_command( char * sGroup, char * sName, int fChanges ); @@ -1168,4 +1185,9 @@ def cmd_python(cmd_args): add_abc_command(cmd_python, "Python", "python", 0) +def create_abc_array(List): + _pyabc_array_clear() + for ObjId in List: + _pyabc_array_push(ObjId) + %} -- cgit v1.2.3