diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 14:23:49 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 14:23:49 -0800 |
| commit | bab4c1ddfc3e7bb88d649daed8bd412a98850cf9 (patch) | |
| tree | f46fe175c353513ce100c20db8b62642f45a4f5e /src/proof/cec | |
| parent | cc840d8bd83775f911bc373aa3284d518dc050d0 (diff) | |
| download | abc-bab4c1ddfc3e7bb88d649daed8bd412a98850cf9.tar.gz abc-bab4c1ddfc3e7bb88d649daed8bd412a98850cf9.tar.bz2 abc-bab4c1ddfc3e7bb88d649daed8bd412a98850cf9.zip | |
Upgrading the SAT solvers.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cecSatG2.c | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index e9783b57..acdf097d 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1366,7 +1366,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords ); //Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i ) // Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) ); - pCex = sat_solver_read_cex( p->pSat ); + pCex = NULL;//sat_solver_read_cex( p->pSat ); Vec_IntClear( p->vPat ); if ( pCex == NULL ) { @@ -1461,8 +1461,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p Gia_Obj_t * pObj, * pRepr; int i, fSimulate = 1; if ( pPars->fVerbose ) - printf( "Simulate %d words in %d rounds. Easy SAT with %d tries. SAT with %d confs. Recycle after %d SAT calls.\n", - pPars->nWords, pPars->nRounds, pPars->nGenIters, pPars->nBTLimit, pPars->nCallsRecycle ); + printf( "Solver type = %d. Simulate %d words in %d rounds. SAT with %d confs. Recycle after %d SAT calls.\n", + pPars->jType, pPars->nWords, pPars->nRounds, pPars->nBTLimit, pPars->nCallsRecycle ); // this is currently needed to have a correct mapping Gia_ManForEachCi( p, pObj, i ) @@ -1498,7 +1498,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p Cec4_ManSimulate( p, pMan ); if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected goto finalize; - if ( i % (pPars->nRounds / 5) == 0 && pPars->fVerbose ) + if ( i && i % (pPars->nRounds / 5) == 0 && pPars->fVerbose ) Cec4_ManPrintStats( p, pPars, pMan, 1 ); } @@ -1510,9 +1510,11 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p Cec4_ManSimulate( p, pMan ); if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected goto finalize; - if ( pPars->fVerbose ) + if ( i && i % 5 == 0 && pPars->fVerbose ) Cec4_ManPrintStats( p, pPars, pMan, 1 ); } + if ( i && i % 5 && pPars->fVerbose ) + Cec4_ManPrintStats( p, pPars, pMan, 1 ); p->iPatsPi = 0; pMan->nSatSat = 0; |