summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaDup.c2
-rw-r--r--src/aig/gia/giaIso.c145
-rw-r--r--src/aig/saig/saigIso.c15
-rw-r--r--src/base/abci/abc.c58
-rw-r--r--src/base/abci/abcSweep.c2
-rw-r--r--src/proof/ssw/sswSemi.c2
6 files changed, 202 insertions, 22 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 342332cd..577a0180 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1762,7 +1762,7 @@ void Gia_ManDupCones_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vLeaves,
Gia_ManDupCones_rec( p, Gia_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
Vec_PtrPush( vNodes, pObj );
}
- else if ( Gia_ObjIsPo(p, pObj) )
+ else if ( Gia_ObjIsCo(pObj) )
Gia_ManDupCones_rec( p, Gia_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
else if ( Gia_ObjIsRo(p, pObj) )
Vec_PtrPush( vRoots, Gia_ObjRoToRi(p, pObj) );
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index 3ff8ee2f..71733ee9 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -21,7 +21,7 @@
#include "gia.h"
ABC_NAMESPACE_IMPL_START
-
+
#define ISO_MASK 0xFF
static int s_256Primes[ISO_MASK+1] =
@@ -458,11 +458,68 @@ void Gia_IsoSort( Gia_IsoMan_t * p )
SeeAlso []
***********************************************************************/
-void Gia_IsoTest( Gia_Man_t * pGia )
+Vec_Ptr_t * Gia_IsoCollectCos( Gia_IsoMan_t * p, int fVerbose )
+{
+ Vec_Ptr_t * vGroups;
+ Vec_Int_t * vLevel;
+ Gia_Obj_t * pObj;
+ int i, k, iBegin, nSize;
+
+ // add singletons
+ vGroups = Vec_PtrAlloc( 1000 );
+ Gia_ManForEachPo( p->pGia, pObj, i )
+ if ( p->pUniques[Gia_ObjId(p->pGia, pObj)] > 0 )
+ {
+ vLevel = Vec_IntAlloc( 1 );
+ Vec_IntPush( vLevel, i );
+ Vec_PtrPush( vGroups, vLevel );
+ }
+
+ // add groups
+ Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
+ {
+ for ( k = 0; k < nSize; k++ )
+ {
+ pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
+ if ( Gia_ObjIsPo(p->pGia, pObj) )
+ break;
+ }
+ if ( k == nSize )
+ continue;
+ vLevel = Vec_IntAlloc( 8 );
+ for ( k = 0; k < nSize; k++ )
+ {
+ pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
+ if ( Gia_ObjIsPo(p->pGia, pObj) )
+ Vec_IntPush( vLevel, Gia_ObjCioId(pObj) );
+ }
+ Vec_PtrPush( vGroups, vLevel );
+ }
+ // canonicize order
+ Vec_PtrForEachEntry( Vec_Int_t *, vGroups, vLevel, i )
+ Vec_IntSort( vLevel, 0 );
+ Vec_VecSortByFirstInt( (Vec_Vec_t *)vGroups, 0 );
+// Vec_VecFree( (Vec_Vec_t *)vGroups );
+// return NULL;
+ return vGroups;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fVerbose )
{
- int fVerbose = 1;
- int nIterMax = 50;
+ Vec_Ptr_t * vEquivs;
Gia_IsoMan_t * p;
+ int nIterMax = 1000;
int i, clk = clock(), clkTotal = clock();
Gia_ManCleanValue( pGia );
@@ -470,9 +527,9 @@ void Gia_IsoTest( Gia_Man_t * pGia )
Gia_IsoPrepare( p );
Gia_IsoAssignUnique( p );
p->timeStart = clock() - clk;
-
// Gia_IsoPrintClasses( p );
- Gia_IsoPrint( p, 0, clock() - clkTotal );
+ if ( fVerbose )
+ Gia_IsoPrint( p, 0, clock() - clkTotal );
for ( i = 0; i < nIterMax; i++ )
{
clk = clock();
@@ -484,11 +541,11 @@ void Gia_IsoTest( Gia_Man_t * pGia )
p->timeRefine += clock() - clk;
// Gia_IsoPrintClasses( p );
- Gia_IsoPrint( p, i+1, clock() - clkTotal );
+ if ( fVerbose )
+ Gia_IsoPrint( p, i+1, clock() - clkTotal );
if ( p->nSingles == 0 )
break;
}
-
if ( fVerbose )
{
p->timeTotal = clock() - clkTotal;
@@ -501,11 +558,81 @@ void Gia_IsoTest( Gia_Man_t * pGia )
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
-
+ vEquivs = Gia_IsoCollectCos( p, fVerbose );
Gia_IsoManStop( p );
+ return vEquivs;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
+{
+ Gia_Man_t * pPart;
+ Vec_Ptr_t * vEquivs;
+ Vec_Int_t * vRemain, * vLevel;
+ int i, clk = clock();
+ // create equivalences
+ vEquivs = Gia_IsoDeriveEquivPos( pGia, fVerbose );
+ // collect the first ones
+ vRemain = Vec_IntAlloc( 100 );
+ Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
+ Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) );
+ // derive the resulting AIG
+ pPart = Gia_ManDupCones( pGia, Vec_IntArray(vRemain), Vec_IntSize(vRemain) );
+ Vec_IntFree( vRemain );
+ // report the results
+ printf( "Reduced %d outputs to %d outputs. ", Gia_ManPoNum(pGia), Gia_ManPoNum(pPart) );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ if ( fVerbose )
+ {
+ printf( "Nontrivial classes:\n" );
+ Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
+ }
+ if ( pvPosEquivs )
+ *pvPosEquivs = vEquivs;
+ else
+ Vec_VecFree( (Vec_Vec_t *)vEquivs );
+// Gia_ManStopP( &pPart );
+ return pPart;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_IsoTest( Gia_Man_t * pGia, int fVerbose )
+{
+ Vec_Ptr_t * vEquivs;
+ int clk = clock();
+ vEquivs = Gia_IsoDeriveEquivPos( pGia, fVerbose );
+ printf( "Reduced %d outputs to %d. ", Gia_ManPoNum(pGia), Vec_PtrSize(vEquivs) );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ if ( fVerbose )
+ {
+ printf( "Nontrivial classes:\n" );
+ Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
+ }
+ Vec_VecFree( (Vec_Vec_t *)vEquivs );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
index 95d0cdae..c3d1af9d 100644
--- a/src/aig/saig/saigIso.c
+++ b/src/aig/saig/saigIso.c
@@ -428,6 +428,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
Vec_Str_t * vStr, * vPrev;
int i, nPos, nUnique = 0, clk = clock();
int clkDup = 0, clkAig = 0, clkIso = 0, clk2;
+ *pvPosEquivs = NULL;
// derive AIG for each PO
nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
@@ -521,13 +522,6 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
// return (Vec_Vec_t *)vClasses;
// Vec_VecFree( (Vec_Vec_t *)vClasses );
*pvPosEquivs = vClasses;
- if ( fVerbose && vClasses )
- {
- printf( "Non-trivial equivalence clases of primary outputs:\n" );
- Vec_VecPrintInt( (Vec_Vec_t *)vClasses, 1 );
- }
-
-// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
return pPart;
}
@@ -570,7 +564,12 @@ Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int f
pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
Abc_PrintTime( 1, "Time", clock() - clk );
-// Aig_ManStop( pPart );
+ if ( fVerbose && *pvPosEquivs )
+ {
+ printf( "Nontrivial classes:\n" );
+ Vec_VecPrintInt( (Vec_Vec_t *)*pvPosEquivs, 1 );
+ }
+// Aig_ManStopP( &pPart );
return pPart;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 15e314db..c9640db0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -352,6 +352,7 @@ static int Abc_CommandAbc9ReachP ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -782,6 +783,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&reachn", Abc_CommandAbc9ReachN, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reachy", Abc_CommandAbc9ReachY, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
Cmd_CommandAdd( pAbc, "Liveness", "l2s", Abc_CommandAbcLivenessToSafety, 0 );
@@ -27835,6 +27837,58 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
+
+ Gia_Man_t * pAig;
+ Vec_Ptr_t * vPosEquivs;
+ 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_CommandAbc9Iso(): There is no AIG.\n" );
+ return 1;
+ }
+ pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, fVerbose );
+ // update the internal storage of PO equivalences
+ Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
+ // update the AIG
+ Abc_CommandUpdate9( pAbc, pAig );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &iso [-vh]\n" );
+ Abc_Print( -2, "\t removes POs with isomorphic sequential COI\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_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{
// Gia_Man_t * pTemp = NULL;
@@ -27843,7 +27897,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
// extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
// extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose );
- extern void Gia_IsoTest( Gia_Man_t * p );
+ extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -27882,7 +27936,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManSuppSizeTest( pAbc->pGia );
// Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 );
- Gia_IsoTest( pAbc->pGia );
+ Gia_IsoTest( pAbc->pGia, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &test [-svh]\n" );
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index a898f26c..a5649794 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -177,7 +177,7 @@ void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
/**Function*************************************************************
- Synopsis [Collects equivalence classses of node in the network.]
+ Synopsis [Collects equivalence classes of node in the network.]
Description []
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index 74305adf..ec50ab50 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -6,7 +6,7 @@
PackageName [Inductive prover with constraints.]
- Synopsis [Semiformal for equivalence clases.]
+ Synopsis [Semiformal for equivalence classes.]
Author [Alan Mishchenko]
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 01:33:29 +0000