summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-06-04 15:08:58 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-06-04 15:08:58 -0700
commit9c4bf6e11d61b9af1645e896ae238ddf87579f99 (patch)
tree5507a9320277b76a1e69fa6b13e8d29018f89e29 /src
parentb844433a0d326a25aac9b439779e339e0c5303fd (diff)
downloadabc-9c4bf6e11d61b9af1645e896ae238ddf87579f99.tar.gz
abc-9c4bf6e11d61b9af1645e896ae238ddf87579f99.tar.bz2
abc-9c4bf6e11d61b9af1645e896ae238ddf87579f99.zip
Adding CEC command &splitprove.
Diffstat (limited to 'src')
-rw-r--r--src/proof/cec/cecSplit.c10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 3e2b70a6..f8bc6b07 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -217,7 +217,6 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
***********************************************************************/
int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead )
{
- abctime clk = Abc_Clock();
Gia_Man_t * pPart;
int * pOrder = Gia_PermuteSpecialOrder( p );
int Cost0, Cost1, CostBest = ABC_INFINITY;
@@ -250,7 +249,6 @@ int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead )
}
ABC_FREE( pOrder );
assert( iBest >= 0 );
-// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return iBest;
}
@@ -499,6 +497,7 @@ typedef struct Par_ThData_t_
{
Gia_Man_t * p;
Cnf_Dat_t * pCnf;
+ int iThread;
int nTimeOut;
int fWorking;
int Result;
@@ -549,12 +548,12 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
if ( status == 0 )
{
- printf( "The problem is SAT.\n" );
+ printf( "The problem is SAT without cofactoring.\n" );
return 0;
}
if ( status == 1 )
{
- printf( "The problem is UNSAT.\n" );
+ printf( "The problem is UNSAT without cofactoring.\n" );
return 1;
}
assert( status == -1 );
@@ -570,6 +569,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
{
ThData[i].p = NULL;
ThData[i].pCnf = NULL;
+ ThData[i].iThread = i;
ThData[i].nTimeOut = nTimeOut;
ThData[i].fWorking = 0;
ThData[i].Result = -1;
@@ -595,7 +595,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
Gia_Man_t * pLast = ThData[i].p;
int Depth = Vec_IntSize(pLast->vCofVars);
if ( fVerbose )
- Cec_GiaSplitPrint( nIter, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal );
+ Cec_GiaSplitPrint( i, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal );
if ( ThData[i].Result == 0 ) // SAT
{
RetValue = 0;