Skip to content

A
abc
Commit c05aa7a8 by Alan Mishchenko
Options

Adding CEC command &splitprove.

parent 4875dfcb
Showing with 4 additions and 4 deletions
src/proof/cec/cecSplit.c
...@@ -426,7 +426,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in ...@@ -426,7 +426,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
// get the last AIG // get the last AIG
Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack ); Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
// determine cofactoring variable // determine cofactoring variable
int Depth = pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0; int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0);
int iVar = Gia_SplitCofVar( pLast, LookAhead ); int iVar = Gia_SplitCofVar( pLast, LookAhead );
// cofactor // cofactor
Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 ); Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 );
...@@ -441,7 +441,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in ...@@ -441,7 +441,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs ); status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
if ( status == 1 ) if ( status == 1 )
Progress += 1.0 / pow(2, Depth + 1); Progress += 1.0 / pow(2, Depth);
if ( fVerbose ) if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
if ( status == 0 ) // SAT if ( status == 0 ) // SAT
...@@ -468,7 +468,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in ...@@ -468,7 +468,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs ); status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
if ( status == 1 ) if ( status == 1 )
Progress += 1.0 / pow(2, Depth + 1); Progress += 1.0 / pow(2, Depth);
if ( fVerbose ) if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
if ( status == 0 ) // SAT if ( status == 0 ) // SAT
...@@ -568,7 +568,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int ...@@ -568,7 +568,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int
pCnf = Cec_GiaDeriveGiaRemapped( p ); pCnf = Cec_GiaDeriveGiaRemapped( p );
status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs ); status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
if ( fVerbose ) if ( fVerbose && status != -1 )
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
if ( status == 0 ) if ( status == 0 )
{ {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment