summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaEquiv.c7
-rw-r--r--src/aig/gia/giaSweep.c2
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/proof/ssc/sscCore.c4
5 files changed, 16 insertions, 13 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 48f0c215..ed38806e 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -891,7 +891,7 @@ extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p );
extern int Gia_ManEquivCountClasses( Gia_Man_t * p );
extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
-extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
+extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose );
extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 3067f956..d795856a 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -414,7 +414,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose )
+Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@@ -445,7 +445,8 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
return NULL;
}
*/
- Gia_ManSetPhase( p );
+ if ( !fSkipPhase )
+ Gia_ManSetPhase( p );
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
@@ -637,7 +638,7 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
{
Gia_Man_t * pNew, * pFinal;
- pNew = Gia_ManEquivReduce( p, 0, 0, 0 );
+ pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
if ( pNew == NULL )
return NULL;
if ( fMiterPairs )
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 994aedc1..4517bb7b 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -288,7 +288,7 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
if ( p->pManTime == NULL )
{
Gia_ManFraigSweepPerform( p, pPars );
- pNew = Gia_ManEquivReduce( p, 1, 0, 0 );
+ pNew = Gia_ManEquivReduce( p, 1, 0, 0, 0 );
if ( pNew == NULL )
return Gia_ManDup(p);
return pNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d7e36cfa..ec8e9e76 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27365,7 +27365,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( fSynthesis )
{
- pTemp = Gia_ManEquivReduce( pAbc->pGia, 1, fDualOut, fVerbose );
+ pTemp = Gia_ManEquivReduce( pAbc->pGia, 1, fDualOut, 0, fVerbose );
if ( pTemp )
{
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
@@ -27612,7 +27612,7 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( fUseAll )
{
- pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, fVerbose );
+ pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, 0, fVerbose );
pTemp = Gia_ManSeqStructSweep( pTemp2 = pTemp, 1, 1, 0 );
Gia_ManStop( pTemp2 );
}
@@ -31601,7 +31601,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{
-// Gia_Man_t * pTemp = NULL;
+ Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0;
int fSwitch = 0;
// extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
@@ -31614,9 +31614,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Unr_ManTest( Gia_Man_t * pGia );
// extern void Mig_ManTest( Gia_Man_t * pGia );
// extern int Gia_ManVerify( Gia_Man_t * pGia );
-// extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
// extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
// extern void Gia_ManCollectSeqTest( Gia_Man_t * p );
+ extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -31668,10 +31668,10 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Unr_ManTest( pAbc->pGia );
// Mig_ManTest( pAbc->pGia );
// Gia_ManVerifyWithBoxes( pAbc->pGia );
-// pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
-// pTemp = Gia_ManOptimizeRing( pAbc->pGia );
-// Abc_FrameUpdateGia( pAbc, pTemp );
// Gia_ManCollectSeqTest( pAbc->pGia );
+// pTemp = Gia_ManOptimizeRing( pAbc->pGia );
+ pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
+ Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &test [-svh]\n" );
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index 43d0e250..1a57a47c 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -298,6 +298,7 @@ clk = clock();
{
p->nSatCallsUnsat++;
pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
+ Gia_ObjSetProved( pAig, i );
}
else if ( status == l_True )
{
@@ -329,9 +330,10 @@ clk = clock();
p->timeSimSat += clock() - clk;
}
// Gia_ManEquivPrintClasses( pAig, 1, 0 );
+// Gia_ManPrint( pAig );
// generate the resulting AIG
- pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
+ pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 );
if ( pResult == NULL )
{
printf( "There is no equivalences.\n" );
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 00:45:17 +0000