diff options
Diffstat (limited to 'src/proof/ssw/sswSat.c')
-rw-r--r-- | src/proof/ssw/sswSat.c | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/proof/ssw/sswSat.c b/src/proof/ssw/sswSat.c index e5971a64..59ed6945 100644 --- a/src/proof/ssw/sswSat.c +++ b/src/proof/ssw/sswSat.c @@ -46,7 +46,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int nBTLimit = p->pPars->nBTLimit; int pLits[3], nLits, RetValue, RetValue1; - clock_t clk;//, status; + abctime clk;//, status; p->nSatCalls++; p->pMSat->nSolverCalls++; @@ -80,13 +80,13 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) assert( RetValue != 0 ); } -clk = clock(); +clk = Abc_Clock(); RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); -p->timeSat += clock() - clk; +p->timeSat += Abc_Clock() - clk; if ( RetValue1 == l_False ) { -p->timeSatUnsat += clock() - clk; +p->timeSatUnsat += Abc_Clock() - clk; if ( nLits == 2 ) { pLits[0] = lit_neg( pLits[0] ); @@ -105,13 +105,13 @@ p->timeSatUnsat += clock() - clk; } else if ( RetValue1 == l_True ) { -p->timeSatSat += clock() - clk; +p->timeSatSat += Abc_Clock() - clk; p->nSatCallsSat++; return 0; } else // if ( RetValue1 == l_Undef ) { -p->timeSatUndec += clock() - clk; +p->timeSatUndec += Abc_Clock() - clk; p->nSatFailsReal++; return -1; } @@ -142,13 +142,13 @@ p->timeSatUndec += clock() - clk; assert( RetValue != 0 ); } -clk = clock(); +clk = Abc_Clock(); RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); -p->timeSat += clock() - clk; +p->timeSat += Abc_Clock() - clk; if ( RetValue1 == l_False ) { -p->timeSatUnsat += clock() - clk; +p->timeSatUnsat += Abc_Clock() - clk; if ( nLits == 2 ) { pLits[0] = lit_neg( pLits[0] ); @@ -167,13 +167,13 @@ p->timeSatUnsat += clock() - clk; } else if ( RetValue1 == l_True ) { -p->timeSatSat += clock() - clk; +p->timeSatSat += Abc_Clock() - clk; p->nSatCallsSat++; return 0; } else // if ( RetValue1 == l_Undef ) { -p->timeSatUndec += clock() - clk; +p->timeSatUndec += Abc_Clock() - clk; p->nSatFailsReal++; return -1; } |