diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-25 18:08:48 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-25 18:08:48 -0800 |
commit | d2db956a618fd9be1915a6c66b063c894e540fee (patch) | |
tree | 0b2df03a20bfccd0b2d1eab44cfd456a1070c244 /src/aig | |
parent | 0f594b78fae6f45cee463fe47e6f2c0fb33abaf2 (diff) | |
download | abc-d2db956a618fd9be1915a6c66b063c894e540fee.tar.gz abc-d2db956a618fd9be1915a6c66b063c894e540fee.tar.bz2 abc-d2db956a618fd9be1915a6c66b063c894e540fee.zip |
Started experiments with a new solver.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/cnf/cnfMan.c | 121 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
-rw-r--r-- | src/aig/fra/fraCec.c | 277 | ||||
-rw-r--r-- | src/aig/gia/giaAig.c | 4 | ||||
-rw-r--r-- | src/aig/int/intContain.c | 4 | ||||
-rw-r--r-- | src/aig/ivy/ivyFraig.c | 4 | ||||
-rw-r--r-- | src/aig/saig/saigGlaPba.c | 12 |
7 files changed, 332 insertions, 92 deletions
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 837ca2c2..85311229 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -20,6 +20,7 @@ #include "cnf.h" #include "satSolver.h" +#include "satSolver2.h" #include "zlib.h" ABC_NAMESPACE_IMPL_START @@ -416,6 +417,98 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) /**Function************************************************************* + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ) +{ + sat_solver2 * pSat; + int i, f, status; + assert( nFrames > 0 ); + pSat = sat_solver2_new(); + sat_solver2_setnvars( pSat, p->nVars * nFrames ); + for ( i = 0; i < p->nClauses; i++ ) + { + if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + { + sat_solver2_delete( pSat ); + return NULL; + } + } + if ( nFrames > 1 ) + { + Aig_Obj_t * pObjLo, * pObjLi; + int nLitsAll, * pLits, Lits[2]; + nLitsAll = 2 * p->nVars; + pLits = p->pClauses[0]; + for ( f = 1; f < nFrames; f++ ) + { + // add equality of register inputs/outputs for different timeframes + Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i ) + { + Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 ); + Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 ); + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver2_delete( pSat ); + return NULL; + } + Lits[0]++; + Lits[1]--; + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver2_delete( pSat ); + return NULL; + } + } + // add clauses for the next timeframe + for ( i = 0; i < p->nLiterals; i++ ) + pLits[i] += nLitsAll; + for ( i = 0; i < p->nClauses; i++ ) + { + if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) ) + { + sat_solver2_delete( pSat ); + return NULL; + } + } + } + // return literals to their original state + nLitsAll = (f-1) * nLitsAll; + for ( i = 0; i < p->nLiterals; i++ ) + pLits[i] -= nLitsAll; + } + if ( fInit ) + { + Aig_Obj_t * pObjLo; + int Lits[1]; + Aig_ManForEachLoSeq( p->pMan, pObjLo, i ) + { + Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 ); + if ( !sat_solver2_addclause( pSat, Lits, Lits + 1 ) ) + { + sat_solver2_delete( pSat ); + return NULL; + } + } + } + status = sat_solver2_simplify(pSat); + if ( status == 0 ) + { + sat_solver2_delete( pSat ); + return NULL; + } + return pSat; +} + +/**Function************************************************************* + Synopsis [Adds the OR-clause.] Description [] @@ -453,6 +546,34 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) SeeAlso [] ***********************************************************************/ +int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf ) +{ + sat_solver2 * pSat = (sat_solver2 *)p; + Aig_Obj_t * pObj; + int i, * pLits; + pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) ); + Aig_ManForEachPo( pCnf->pMan, pObj, i ) + pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) ) + { + ABC_FREE( pLits ); + return 0; + } + ABC_FREE( pLits ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds the OR-clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) { sat_solver * pSat = (sat_solver *)p; diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index a0073ca1..ea362bdf 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -286,7 +286,7 @@ static inline int Fra_ImpCreate( int Left, int Right ) //////////////////////////////////////////////////////////////////////// /*=== fraCec.c ========================================================*/ -extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); +extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose ); extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose ); /*=== fraClass.c ========================================================*/ diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 037e6c70..1c36ea62 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -20,6 +20,7 @@ #include "fra.h" #include "cnf.h" +#include "satSolver2.h" ABC_NAMESPACE_IMPL_START @@ -43,111 +44,223 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) +int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose ) { - sat_solver * pSat; - Cnf_Dat_t * pCnf; - int status, RetValue, clk = clock(); - Vec_Int_t * vCiIds; + if ( fNewSolver ) + { + extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit ); + extern int Cnf_DataWriteOrClause2( void * pSat, Cnf_Dat_t * pCnf ); - assert( Aig_ManRegNum(pMan) == 0 ); - pMan->pData = NULL; + sat_solver2 * pSat; + Cnf_Dat_t * pCnf; + int status, RetValue, clk = clock(); + Vec_Int_t * vCiIds; - // derive CNF - pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); -// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); + assert( Aig_ManRegNum(pMan) == 0 ); + pMan->pData = NULL; - if ( fFlipBits ) - Cnf_DataTranformPolarity( pCnf, 0 ); + // derive CNF + pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); + // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); - // convert into SAT solver - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - if ( pSat == NULL ) - { + if ( fFlipBits ) + Cnf_DataTranformPolarity( pCnf, 0 ); + + // convert into SAT solver + pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + return 1; + } + + + if ( fAndOuts ) + { + // assert each output independently + if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) ) + { + sat_solver2_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + else + { + // add the OR clause for the outputs + if ( !Cnf_DataWriteOrClause2( pSat, pCnf ) ) + { + sat_solver2_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); Cnf_DataFree( pCnf ); - return 1; - } - if ( fAndOuts ) - { - // assert each output independently - if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) ) + printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) ); + ABC_PRT( "Time", clock() - clk ); + + // simplify the problem + clk = clock(); + status = sat_solver2_simplify(pSat); + printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) ); + ABC_PRT( "Time", clock() - clk ); + if ( status == 0 ) { - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); + Vec_IntFree( vCiIds ); + sat_solver2_delete( pSat ); + // printf( "The problem is UNSATISFIABLE after simplification.\n" ); return 1; } + + // solve the miter + clk = clock(); + if ( fVerbose ) + pSat->verbosity = 1; + status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status == l_Undef ) + { + // printf( "The problem timed out.\n" ); + RetValue = -1; + } + else if ( status == l_True ) + { + // printf( "The problem is SATISFIABLE.\n" ); + RetValue = 0; + } + else if ( status == l_False ) + { + // printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = 1; + } + else + assert( 0 ); + + // Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts ); + // Abc_PrintTime( 1, "Solving time", clock() - clk ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + } + // free the sat_solver2 +// if ( fVerbose ) + Sat_Solver2PrintStats( stdout, pSat ); + //sat_solver2_store_write( pSat, "trace.cnf" ); + //sat_solver2_store_free( pSat ); + sat_solver2_delete( pSat ); + Vec_IntFree( vCiIds ); + return RetValue; } else { - // add the OR clause for the outputs - if ( !Cnf_DataWriteOrClause( pSat, pCnf ) ) + sat_solver * pSat; + Cnf_Dat_t * pCnf; + int status, RetValue, clk = clock(); + Vec_Int_t * vCiIds; + + assert( Aig_ManRegNum(pMan) == 0 ); + pMan->pData = NULL; + + // derive CNF + pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); + // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); + + if ( fFlipBits ) + Cnf_DataTranformPolarity( pCnf, 0 ); + + // convert into SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) { - sat_solver_delete( pSat ); Cnf_DataFree( pCnf ); return 1; } - } - vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); - Cnf_DataFree( pCnf ); -// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// ABC_PRT( "Time", clock() - clk ); + if ( fAndOuts ) + { + // assert each output independently + if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) ) + { + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + else + { + // add the OR clause for the outputs + if ( !Cnf_DataWriteOrClause( pSat, pCnf ) ) + { + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); + Cnf_DataFree( pCnf ); - // simplify the problem - clk = clock(); - status = sat_solver_simplify(pSat); -// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// ABC_PRT( "Time", clock() - clk ); - if ( status == 0 ) - { - Vec_IntFree( vCiIds ); - sat_solver_delete( pSat ); -// printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return 1; - } - // solve the miter - clk = clock(); - if ( fVerbose ) - pSat->verbosity = 1; - status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( status == l_Undef ) - { -// printf( "The problem timed out.\n" ); - RetValue = -1; - } - else if ( status == l_True ) - { -// printf( "The problem is SATISFIABLE.\n" ); - RetValue = 0; - } - else if ( status == l_False ) - { -// printf( "The problem is UNSATISFIABLE.\n" ); - RetValue = 1; - } - else - assert( 0 ); + // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); + // ABC_PRT( "Time", clock() - clk ); + + // simplify the problem + clk = clock(); + status = sat_solver_simplify(pSat); + // printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); + // ABC_PRT( "Time", clock() - clk ); + if ( status == 0 ) + { + Vec_IntFree( vCiIds ); + sat_solver_delete( pSat ); + // printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return 1; + } -// Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts ); -// Abc_PrintTime( 1, "Solving time", clock() - clk ); + // solve the miter + clk = clock(); + if ( fVerbose ) + pSat->verbosity = 1; + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status == l_Undef ) + { + // printf( "The problem timed out.\n" ); + RetValue = -1; + } + else if ( status == l_True ) + { + // printf( "The problem is SATISFIABLE.\n" ); + RetValue = 0; + } + else if ( status == l_False ) + { + // printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = 1; + } + else + assert( 0 ); + + // Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts ); + // Abc_PrintTime( 1, "Solving time", clock() - clk ); - // if the problem is SAT, get the counterexample - if ( status == l_True ) - { - pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + } + // free the sat_solver +// if ( fVerbose ) + Sat_SolverPrintStats( stdout, pSat ); + //sat_solver_store_write( pSat, "trace.cnf" ); + //sat_solver_store_free( pSat ); + sat_solver_delete( pSat ); + Vec_IntFree( vCiIds ); + return RetValue; } - // free the sat_solver - if ( fVerbose ) - Sat_SolverPrintStats( stdout, pSat ); -//sat_solver_store_write( pSat, "trace.cnf" ); -//sat_solver_store_free( pSat ); - sat_solver_delete( pSat ); - Vec_IntFree( vCiIds ); - return RetValue; } /**Function************************************************************* @@ -187,7 +300,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ) // if SAT only, solve without iteration clk = clock(); - RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0 ); + RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 ); if ( fVerbose ) { printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) ); @@ -255,7 +368,7 @@ ABC_PRT( "Time", clock() - clk ); if ( RetValue == -1 ) { clk = clock(); - RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0 ); + RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0, 0 ); if ( fVerbose ) { printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 221593a1..00148451 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -568,11 +568,11 @@ void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbo ***********************************************************************/ int Gia_ManSolveSat( Gia_Man_t * p ) { -// extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); +// extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose ); Aig_Man_t * pNew; int RetValue, clk = clock(); pNew = Gia_ManToAig( p, 0 ); - RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0 ); + RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0, 0 ); if ( RetValue == 0 ) { Gia_Obj_t * pObj; diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c index 4cc8577e..d4af0ae8 100644 --- a/src/aig/int/intContain.c +++ b/src/aig/int/intContain.c @@ -57,7 +57,7 @@ int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); RetValue = Fra_FraigMiterStatus( pAigTemp ); Aig_ManStop( pAigTemp ); -// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 ); } assert( RetValue != -1 ); Aig_ManStop( pMiter ); @@ -88,7 +88,7 @@ int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ) pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); RetValue = Fra_FraigMiterStatus( pAigTemp ); Aig_ManStop( pAigTemp ); -// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 ); } assert( RetValue != -1 ); Aig_ManStop( pMiter ); diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index 87209ca3..b53805b4 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -2907,14 +2907,14 @@ printf( "***************\n" ); ***********************************************************************/ int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit ) { - extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); + extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose ); Vec_Int_t * vLeaves; Aig_Man_t * pMan; Aig_Obj_t * pObj; int i, RetValue; vLeaves = Vec_IntAlloc( 100 ); pMan = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves ); - RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 1 ); + RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 1 ); if ( RetValue == 0 ) { int Counter = 0; diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index 50f6fce8..5834db76 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -558,6 +558,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in Aig_Gla2Man_t * p; Vec_Int_t * vCore, * vResult; int nTimeToStop = time(NULL) + TimeLimit; + int clk, clk2 = clock(); assert( Saig_ManPoNum(pAig) == 1 ); Abc_Clock(0,1); @@ -570,6 +571,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in } // start the solver + clk = clock(); Abc_Clock(1,1); p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose ); if ( !Aig_Gla2CreateSatSolver( p ) ) @@ -579,13 +581,15 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in return NULL; } sat_solver_set_random( p->pSat, fSkipRand ); - p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; +// p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; + p->timePre += clock() - clk; // set runtime limit if ( TimeLimit ) sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); // compute UNSAT core + clk = clock(); Abc_Clock(1,1); vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL ); if ( vCore == NULL ) @@ -593,8 +597,10 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in Aig_Gla2ManStop( p ); return NULL; } - p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; - p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC; +// p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; +// p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC; + p->timeSat += clock() - clk; + p->timeTotal += clock() - clk2; // print stats if ( fVerbose ) |