summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaEquiv.c142
-rw-r--r--src/base/abci/abc.c50
-rw-r--r--src/base/main/main.h1
-rw-r--r--src/base/main/mainFrame.c3
-rw-r--r--src/base/main/mainInt.h1
-rw-r--r--src/python/pyabc.i22
6 files changed, 183 insertions, 36 deletions
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
{
@@ -753,29 +757,6 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
/**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.]
Description []
@@ -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
@@ -1279,6 +1260,74 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
/**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.]
Description []
@@ -1644,6 +1693,29 @@ 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.]
Description []
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 )
@@ -27558,6 +27560,52 @@ usage:
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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
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)
+
%}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 14:13:07 +0000