diff options
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abcPrint.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcProve.c | 4 | ||||
| -rw-r--r-- | src/base/abci/abcSat.c | 10 |
3 files changed, 14 insertions, 2 deletions
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index d7b270bf..2aad721b 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -50,6 +50,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) { int Num, Num2; +// Abc_NtkDetectMatching( pNtk ); +// return; fprintf( pFile, "%-13s:", pNtk->pName ); fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) ); diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index c0e904bf..23315223 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -140,8 +140,9 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) if ( RetValue >= 0 ) break; } - } + } +/* // try to prove it using brute force SAT if ( RetValue < 0 && pParams->fUseBdds ) { @@ -161,6 +162,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) pNtk = pNtkTemp; Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose ); } +*/ if ( RetValue < 0 ) { diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 9348231b..06376eed 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -422,7 +422,15 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) pNode->pCopy = (Abc_Obj_t *)vNodes->nSize; Vec_PtrPush( vNodes, pNode ); Abc_NtkClauseTriv( pSat, pNode, vVars ); - +/* + // add the PI variables first + Abc_NtkForEachCi( pNtk, pNode, i ) + { + pNode->fMarkA = 1; + pNode->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pNode ); + } +*/ // collect the nodes that need clauses and top-level assignments Abc_NtkForEachCo( pNtk, pNode, i ) { |