summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp4
-rw-r--r--src/aig/gia/gia.h6
-rw-r--r--src/aig/gia/giaDup.c2
-rw-r--r--src/aig/gia/giaEquiv.c142
-rw-r--r--src/aig/gia/giaMan.c2
-rw-r--r--src/base/abc/abcFunc.c11
-rw-r--r--src/base/abci/abc.c79
-rw-r--r--src/base/abci/abcDress3.c259
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/proof/cec/cec.h1
-rw-r--r--src/proof/cec/cecCore.c10
-rw-r--r--src/proof/cec/cecInt.h2
-rw-r--r--src/proof/cec/cecSolve.c12
13 files changed, 518 insertions, 13 deletions
diff --git a/abclib.dsp b/abclib.dsp
index e1fbe7f3..f2dbc1b3 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -263,6 +263,10 @@ SOURCE=.\src\base\abci\abcDress2.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\abci\abcDress3.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\abci\abcDsd.c
# End Source File
# Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f2baf7e0..3d2d84ae 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -175,6 +175,8 @@ struct Gia_Man_t_
Vec_Int_t * vUserFfIds; // numbers assigned to FFs by the user
Vec_Int_t * vCiNumsOrig; // original CI names
Vec_Int_t * vCoNumsOrig; // original CO names
+ Vec_Int_t * vIdsOrig; // original object IDs
+ Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent
Vec_Int_t * vCofVars; // cofactoring variables
Vec_Vec_t * vClockDoms; // clock domains
Vec_Flt_t * vTiming; // arrival/required/slack
@@ -1241,6 +1243,10 @@ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p );
/*=== giaEquiv.c ==========================================================*/
+extern void Gia_ManOrigIdsInit( Gia_Man_t * p );
+extern void Gia_ManOrigIdsStart( Gia_Man_t * p );
+extern void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew );
+extern Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs );
extern void Gia_ManEquivFixOutputPairs( Gia_Man_t * p );
extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
extern int * Gia_ManDeriveNexts( Gia_Man_t * p );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b5fd393e..7ced54a4 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1383,7 +1383,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew->nConstrs = p->nConstrs;
if ( p->pCexSeq )
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index d383ce41..584be4cd 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -34,6 +34,143 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
+ Synopsis [Manipulating original IDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManOrigIdsInit( Gia_Man_t * p )
+{
+ Vec_IntFreeP( &p->vIdsOrig );
+ p->vIdsOrig = Vec_IntStartNatural( Gia_ManObjNum(p) );
+}
+void Gia_ManOrigIdsStart( Gia_Man_t * p )
+{
+ Vec_IntFreeP( &p->vIdsOrig );
+ p->vIdsOrig = Vec_IntStartFull( Gia_ManObjNum(p) );
+}
+void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew )
+{
+ Gia_Obj_t * pObj; int i;
+ if ( p->vIdsOrig == NULL )
+ return;
+ Gia_ManOrigIdsStart( pNew );
+ Vec_IntWriteEntry( pNew->vIdsOrig, 0, 0 );
+ Gia_ManForEachObj1( p, pObj, i )
+ if ( ~pObj->Value && Abc_Lit2Var(pObj->Value) && Vec_IntEntry(p->vIdsOrig, i) != -1 && Vec_IntEntry(pNew->vIdsOrig, Abc_Lit2Var(pObj->Value)) == -1 )
+ Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pObj->Value), Vec_IntEntry(p->vIdsOrig, i) );
+ Gia_ManForEachObj( pNew, pObj, i )
+ assert( Vec_IntEntry(pNew->vIdsOrig, i) >= 0 );
+}
+// input is a set of equivalent node pairs in any order
+// output is the mapping of each node into the equiv node with the smallest ID
+void Gia_ManOrigIdsRemapPairsInsert( Vec_Int_t * vMap, int One, int Two )
+{
+ int Smo = One < Two ? One : Two;
+ int Big = One < Two ? Two : One;
+ assert( Smo != Big );
+ if ( Vec_IntEntry(vMap, Big) == -1 )
+ Vec_IntWriteEntry( vMap, Big, Smo );
+ else
+ Gia_ManOrigIdsRemapPairsInsert( vMap, Smo, Vec_IntEntry(vMap, Big) );
+}
+int Gia_ManOrigIdsRemapPairsExtract( Vec_Int_t * vMap, int One )
+{
+ if ( Vec_IntEntry(vMap, One) == -1 )
+ return One;
+ return Gia_ManOrigIdsRemapPairsExtract( vMap, Vec_IntEntry(vMap, One) );
+}
+Vec_Int_t * Gia_ManOrigIdsRemapPairs( Vec_Int_t * vEquivPairs, int nObjs )
+{
+ Vec_Int_t * vMapResult;
+ Vec_Int_t * vMap2Smaller;
+ int i, One, Two;
+ // map bigger into smaller one
+ vMap2Smaller = Vec_IntStartFull( nObjs );
+ Vec_IntForEachEntryDouble( vEquivPairs, One, Two, i )
+ Gia_ManOrigIdsRemapPairsInsert( vMap2Smaller, One, Two );
+ // collect results in the topo order
+ vMapResult = Vec_IntStartFull( nObjs );
+ Vec_IntForEachEntry( vMap2Smaller, One, i )
+ if ( One >= 0 )
+ Vec_IntWriteEntry( vMapResult, i, Gia_ManOrigIdsRemapPairsExtract(vMap2Smaller, One) );
+ Vec_IntFree( vMap2Smaller );
+ return vMapResult;
+}
+// remap the AIG using the equivalent pairs proved
+// returns the reduced AIG and the equivalence classes of the original AIG
+Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs )
+{
+ Gia_Man_t * pNew = NULL;
+ Gia_Obj_t * pObj, * pRepr; int i;
+ Vec_Int_t * vMap = Gia_ManOrigIdsRemapPairs( vPairs, Gia_ManObjNum(p) );
+ Gia_ManSetPhase( p );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ Gia_ManFillValue(p);
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( Vec_IntEntry(vMap, i) == -1 )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else
+ {
+ pRepr = Gia_ManObj( p, Vec_IntEntry(vMap, i) );
+ pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
+ }
+ }
+ Gia_ManHashStop( pNew );
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Vec_IntFree( vMap );
+ // compute equivalences
+ assert( !p->pReprs && !p->pNexts );
+ p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ Gia_ObjSetRepr( p, i, GIA_VOID );
+ Gia_ManFillValue(pNew);
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ int iRepr = Abc_Lit2Var(pObj->Value);
+ if ( iRepr == 0 )
+ {
+ Gia_ObjSetRepr( p, i, 0 );
+ continue;
+ }
+ pRepr = Gia_ManObj( pNew, iRepr );
+ if ( !~pRepr->Value ) // first time
+ {
+ pRepr->Value = i;
+ continue;
+ }
+ // add equivalence
+ Gia_ObjSetRepr( p, i, pRepr->Value );
+ }
+ p->pNexts = Gia_ManDeriveNexts( p );
+ return pNew;
+}
+Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs )
+{
+ Gia_Man_t * pTemp, * pNew = Gia_ManOrigIdsReduce( p, vPairs );
+ Gia_ManPrintStats( p, NULL );
+ Gia_ManPrintStats( pNew, NULL );
+ //Gia_ManStop( pNew );
+ // cleanup the resulting one
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if AIG is not in the required topo order.]
Description []
@@ -460,7 +597,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS
Gia_ManForEachCo( p, pObj, i )
Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
@@ -641,6 +778,7 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
if ( pNew == NULL )
return NULL;
+ Gia_ManOrigIdsRemap( p, pNew );
if ( fMiterPairs )
Gia_ManEquivFixOutputPairs( pNew );
if ( fSeq )
@@ -649,9 +787,11 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
Gia_ManCombMarkUsed( pNew );
Gia_ManEquivUpdatePointers( p, pNew );
pFinal = Gia_ManDupMarked( pNew );
+ Gia_ManOrigIdsRemap( pNew, pFinal );
Gia_ManEquivDeriveReprs( p, pNew, pFinal );
Gia_ManStop( pNew );
pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
+ Gia_ManOrigIdsRemap( pNew, pFinal );
Gia_ManStop( pNew );
return pFinal;
}
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index d9e878a7..9ccab495 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -93,6 +93,8 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_FltFreeP( &p->vTiming );
Vec_VecFreeP( &p->vClockDoms );
Vec_IntFreeP( &p->vCofVars );
+ Vec_IntFreeP( &p->vIdsOrig );
+ Vec_IntFreeP( &p->vIdsEquiv );
Vec_IntFreeP( &p->vLutConfigs );
Vec_IntFreeP( &p->vEdgeDelay );
Vec_IntFreeP( &p->vEdgeDelayR );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index b44a272a..5d0261d7 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -980,7 +980,7 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
Vec_Int_t * vMapping = NULL;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode, * pFanin;
- int i, k, nObjs;
+ int i, k, nObjs, iGiaObj;
assert( Abc_NtkIsAigLogic(p) );
pHopMan = (Hop_Man_t *)p->pManFunc;
// create new manager
@@ -1016,15 +1016,14 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
{
assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
Abc_ConvertAigToGia( pNew, pHopObj );
- if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(pHopObj->iData))) )
- continue;
- if ( vMapping && !Vec_IntEntry(vMapping, Abc_Lit2Var(pHopObj->iData)) )
+ iGiaObj = Abc_Lit2Var( pHopObj->iData );
+ if ( vMapping && Gia_ObjIsAnd(Gia_ManObj(pNew, iGiaObj)) && !Vec_IntEntry(vMapping, iGiaObj) )
{
- Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pHopObj->iData), Vec_IntSize(vMapping) );
+ Vec_IntWriteEntry( vMapping, iGiaObj, Vec_IntSize(vMapping) );
Vec_IntPush( vMapping, Abc_ObjFaninNum(pNode) );
Abc_ObjForEachFanin( pNode, pFanin, k )
Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->iTemp) );
- Vec_IntPush( vMapping, Abc_Lit2Var(pHopObj->iData) );
+ Vec_IntPush( vMapping, iGiaObj );
}
}
pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ebd6c368..f19f8449 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -233,6 +233,7 @@ static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDumpEquiv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStart3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStop3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -869,6 +870,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_clean", Abc_CommandFraigClean, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "dress", Abc_CommandFraigDress, 1 );
+ Cmd_CommandAdd( pAbc, "Fraiging", "dump_equiv", Abc_CommandDumpEquiv, 0 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_start3", Abc_CommandRecStart3, 0 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_stop3", Abc_CommandRecStop3, 0 );
@@ -14812,6 +14814,81 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose );
+ FILE * pFile = NULL;
+ Abc_Ntk_t * pNtks[2] = {NULL};
+ char * pFileName[2], * pFileNameOut;
+ int c, nConfs = 1000, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfs < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc != globalUtilOptind + 3 )
+ {
+ Abc_Print( -1, "Expecting three file names on the command line.\n" );
+ goto usage;
+ }
+ pFileName[0] = argv[globalUtilOptind];
+ pFileName[1] = argv[globalUtilOptind+1];
+ pFileNameOut = argv[globalUtilOptind+2];
+ for ( c = 0; c < 2; c++ )
+ {
+ pNtks[c] = Io_Read( pFileName[c], Io_ReadFileType(pFileName[c]), 1, 0 );
+ if ( pNtks[c] == NULL )
+ goto usage;
+ Abc_NtkToAig( pNtks[c] );
+ }
+ Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fVerbose );
+ Abc_NtkDelete( pNtks[0] );
+ Abc_NtkDelete( pNtks[1] );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: dump_equiv [-C num] [-vh] <file1.blif> <file2.blif> <file_dump_equiv.txt>\n" );
+ Abc_Print( -2, "\t computes equivalence classes of nodes in <file1> and <file2>\n" );
+ Abc_Print( -2, "\t-C num : the maximum number of conflicts at each node [default = %d]\n", nConfs );
+ Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\t<file1> : first network whose nodes are considered\n" );
+ Abc_Print( -2, "\t<file2> : second network whose nodes are considered\n" );
+ Abc_Print( -2, "\t<file_dump_equiv> : text file with node equivalence classes\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * FileName, * pTemp;
@@ -27022,7 +27099,7 @@ usage:
Abc_Print( -2, "\t converts the current network into GIA and moves it to the &-space\n" );
Abc_Print( -2, "\t (if the network is a sequential logic network, normalizes the flops\n" );
Abc_Print( -2, "\t to have const-0 initial values, equivalent to \"undc; st; zero\")\n" );
- Abc_Print( -2, "\t-c : toggles allowing simple GIA to be improved [default = %s]\n", fGiaSimple? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-m : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" );
Abc_Print( -2, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c
new file mode 100644
index 00000000..ee7eb8e3
--- /dev/null
+++ b/src/base/abci/abcDress3.c
@@ -0,0 +1,259 @@
+/**CFile****************************************************************
+
+ FileName [abcDress3.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Transfers names from one netlist to the other.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcDress3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/io/ioAbc.h"
+#include "proof/cec/cec.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Compute equivalence classes of nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
+{
+ Gia_Man_t * pTemp;
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+ Cec_ManFraSetDefaultParams( pPars );
+ pPars->fUseOrigIds = 1;
+ pPars->fSatSweeping = 1;
+ pPars->nBTLimit = nConfs;
+ pPars->fVerbose = fVerbose;
+ pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
+ Gia_ManStop( pTemp );
+ pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
+ Gia_ManStop( pTemp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Add logic from pNtk to the AIG manager p.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
+{
+ extern int Abc_ConvertAigToGia( Gia_Man_t * p, Hop_Obj_t * pRoot );
+ Hop_Man_t * pHopMan;
+ Hop_Obj_t * pHopObj;
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pNode, * pFanin;
+ int i, k;
+ assert( Abc_NtkIsAigLogic(pNtk) );
+ pHopMan = (Hop_Man_t *)pNtk->pManFunc;
+ Hop_ManConst1(pHopMan)->iData = 1;
+ // image primary inputs
+ Abc_NtkCleanCopy( pNtk );
+ Abc_NtkForEachCi( pNtk, pNode, i )
+ pNode->iTemp = Gia_ManCiLit(p, i);
+ // iterate through nodes used in the mapping
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
+ {
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ Hop_ManPi(pHopMan, k)->iData = pFanin->iTemp;
+ pHopObj = Hop_Regular( (Hop_Obj_t *)pNode->pData );
+ assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
+ if ( Hop_DagSize(pHopObj) > 0 )
+ Abc_ConvertAigToGia( p, pHopObj );
+ pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
+ }
+ Vec_PtrFree( vNodes );
+ // create primary outputs
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ Gia_ManAppendCo( p, Abc_ObjFanin0(pNode)->iTemp );
+}
+Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+ Gia_Man_t * p;
+ Gia_Obj_t * pObj;
+ Abc_Obj_t * pNode;
+ int i;
+ assert( Abc_NtkIsAigLogic(pNtk1) );
+ assert( Abc_NtkIsAigLogic(pNtk2) );
+ // create new manager
+ p = Gia_ManStart( 10000 );
+ p->pName = Abc_UtilStrsav( Abc_NtkName(pNtk1) );
+ p->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk1) );
+ Abc_NtkForEachCi( pNtk1, pNode, i )
+ Gia_ManAppendCi(p);
+ // add logic
+ Gia_ManHashAlloc( p );
+ Abc_NtkAigToGiaOne( p, pNtk1 );
+ Abc_NtkAigToGiaOne( p, pNtk2 );
+ Gia_ManHashStop( p );
+ // add extra POs to dangling nodes
+ Gia_ManCreateValueRefs( p );
+ Gia_ManForEachAnd( p, pObj, i )
+ if ( pObj->Value == 0 )
+ Gia_ManAppendCo( p, Abc_Var2Lit(i, 0) );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect equivalence class information.]
+
+ Description [Each class is represented as follows:
+ <num_entries><entry1><entry2>...<entryN>
+ where <entry> is nodeId with 1-bit for complement and 1-bit for network.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_NtkCollectAddOne( int iNtk, int iObj, int iGiaLit, Gia_Man_t * pGia, Vec_Int_t * vGia2Cla, Vec_Int_t * vNexts[2] )
+{
+ int iRepr = Gia_ObjReprSelf( pGia, Abc_Lit2Var(iGiaLit) );
+ int Compl = Abc_LitIsCompl(iGiaLit) ^ Gia_ObjPhase(Gia_ManObj(pGia, iRepr)) ^ Gia_ObjPhase(Gia_ManObj(pGia, Abc_Lit2Var(iGiaLit)));
+ int Added = Abc_Var2Lit( Abc_Var2Lit(iObj, Compl), iNtk );
+ int Entry = Vec_IntEntry( vGia2Cla, iRepr );
+ Vec_IntWriteEntry( vNexts[iNtk], iObj, Entry );
+ Vec_IntWriteEntry( vGia2Cla, iRepr, Added );
+}
+Vec_Int_t * Abc_NtkCollectEquivClasses( Abc_Ntk_t * pNtks[2], Gia_Man_t * pGia )
+{
+ Vec_Int_t * vClass = Vec_IntAlloc( 100 );
+ Vec_Int_t * vClasses = Vec_IntAlloc( 1000 );
+ Vec_Int_t * vGia2Cla = Vec_IntStartFull( Gia_ManObjNum(pGia) ); // mapping objId into classId
+ Vec_Int_t * vNexts[2] = { Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[0])), Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[1])) };
+ Abc_Obj_t * pObj;
+ int n, i, k, Entry, fCompl;
+ Abc_NtkForEachCi( pNtks[0], pObj, i )
+ Abc_NtkCollectAddOne( 0, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
+ for ( n = 0; n < 2; n++ )
+ Abc_NtkForEachNode( pNtks[n], pObj, i )
+ Abc_NtkCollectAddOne( n, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
+ Vec_IntForEachEntry( vGia2Cla, Entry, i )
+ {
+ Vec_IntClear( vClass );
+ for ( ; Entry >= 0; Entry = Vec_IntEntry(vNexts[Entry&1], Entry>>2) )
+ Vec_IntPush( vClass, Entry );
+ if ( Vec_IntSize(vClass) < 2 )
+ continue;
+ Vec_IntReverseOrder( vClass );
+ fCompl = 2 & Vec_IntEntry( vClass, 0 );
+ Vec_IntForEachEntry( vClass, Entry, k )
+ Vec_IntWriteEntry( vClass, k, Entry ^ fCompl );
+ Vec_IntPush( vClasses, Vec_IntSize(vClass) );
+ Vec_IntAppend( vClasses, vClass );
+ }
+ Vec_IntFree( vGia2Cla );
+ Vec_IntFree( vNexts[0] );
+ Vec_IntFree( vNexts[1] );
+ Vec_IntFree( vClass );
+ return vClasses;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write the output file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * pNtks[2] )
+{
+ int i, c, k, Entry;
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL ) { printf( "Cannot open file %s for writing.\n", pFileName ); return; }
+ fprintf( pFile, "# Node equivalences computed by ABC for networks \"%s\" and \"%s\" on %s\n\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), Extra_TimeStamp() );
+ for ( i = c = 0; i < Vec_IntSize(vClasses); c++, i += 1 + Vec_IntEntry(vClasses, i) )
+ {
+ Vec_IntForEachEntryStartStop( vClasses, Entry, k, i + 1, i + 1 + Vec_IntEntry(vClasses, i) )
+ {
+ Abc_Ntk_t * pNtk = pNtks[Entry & 1];
+ char * pObjName = Abc_ObjName( Abc_NtkObj(pNtk, Entry>>2) );
+ fprintf( pFile, "%d:%s:%s%s\n", c+1, Abc_NtkName(pNtk), (Entry&2) ? "NOT:":"", pObjName );
+ }
+ fprintf( pFile, "\n" );
+ }
+ fclose( pFile );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Compute and dump equivalent name classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose )
+{
+ //abctime clk = Abc_Clock();
+ Vec_Int_t * vClasses;
+ // derive shared AIG for the two networks
+ Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1] );
+ if ( fVerbose )
+ printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
+ // compute equivalences in this AIG
+ Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose );
+ //if ( fVerbose )
+ // Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
+ if ( fVerbose )
+ Gia_ManPrintStats( pGia, NULL );
+ // collect equivalence class information
+ vClasses = Abc_NtkCollectEquivClasses( pNtks, pGia );
+ Gia_ManStop( pGia );
+ // dump information into the output file
+ Abc_NtkDumpEquivFile( pFileName, vClasses, pNtks );
+ Vec_IntFree( vClasses );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 492fc62a..b97f526f 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -15,6 +15,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDetect.c \
src/base/abci/abcDress.c \
src/base/abci/abcDress2.c \
+ src/base/abci/abcDress3.c \
src/base/abci/abcDsd.c \
src/base/abci/abcExact.c \
src/base/abci/abcExtract.c \
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index a0b92b52..e8b243d3 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -108,6 +108,7 @@ struct Cec_ParFra_t_
int fColorDiff; // miter with separate outputs
int fSatSweeping; // enable SAT sweeping
int fRunCSat; // enable another solver
+ int fUseOrigIds; // enable recording of original IDs
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
int iOutFail; // the failed output
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index c9e9f67a..ed5c4ab7 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -236,7 +236,7 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
Gia_Man_t * pNew;
Cec_ManPat_t * pPat;
pPat = Cec_ManPatStart();
- Cec_ManSatSolve( pPat, pAig, pPars );
+ Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL );
// pNew = Gia_ManDupDfsSkip( pAig );
pNew = Gia_ManDup( pAig );
Cec_ManPatStop( pPat );
@@ -351,6 +351,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
pIni = Gia_ManDup(pAig);
pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
+ if ( pPars->fUseOrigIds )
+ {
+ Gia_ManOrigIdsInit( pIni );
+ Vec_IntFreeP( &pAig->vIdsEquiv );
+ pAig->vIdsEquiv = Vec_IntAlloc( 1000 );
+ }
// prepare the managers
// SAT sweeping
@@ -429,7 +435,7 @@ clk = Abc_Clock();
if ( pPars->fRunCSat )
Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
else
- Cec_ManSatSolve( pPat, pSrm, pParsSat );
+ Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv );
p->timeSat += Abc_Clock() - clk;
if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
{
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index ef1dd983..d93e5e86 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -201,7 +201,7 @@ extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== cecSolve.c ============================================================*/
extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
-extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs );
extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index e3db0b93..f75914e4 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -673,7 +673,7 @@ p->timeSatUndec += Abc_Clock() - clk;
SeeAlso []
***********************************************************************/
-void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
{
Bar_Progress_t * pProgress = NULL;
Cec_ManSat_t * p;
@@ -706,6 +706,16 @@ clk2 = Abc_Clock();
status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
pObj->fMark0 = (status == 0);
pObj->fMark1 = (status == 1);
+ if ( status == 1 && vIdsOrig )
+ {
+ int iObj1 = Vec_IntEntry(vMiterPairs, 2*i);
+ int iObj2 = Vec_IntEntry(vMiterPairs, 2*i+1);
+ int OrigId1 = Vec_IntEntry(vIdsOrig, iObj1);
+ int OrigId2 = Vec_IntEntry(vIdsOrig, iObj2);
+ assert( OrigId1 >= 0 && OrigId2 >= 0 );
+ Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 );
+ }
+
/*
if ( status == -1 )
{
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 11:13:05 +0000