summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/cnf/cnfMan.c121
-rw-r--r--src/aig/fra/fra.h2
-rw-r--r--src/aig/fra/fraCec.c277
-rw-r--r--src/aig/gia/giaAig.c4
-rw-r--r--src/aig/int/intContain.c4
-rw-r--r--src/aig/ivy/ivyFraig.c4
-rw-r--r--src/aig/saig/saigGlaPba.c12
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 )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 18:32:22 +0000