luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding CEC command &splitprove.

This commit is contained in:
Alan Mishchenko 2014-06-04 15:00:38 -07:00
parent f2818ddb83
commit b844433a0d
6 changed files with 366 additions and 82 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -4219,6 +4219,10 @@ SOURCE=.\src\proof\cec\cecSolve.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSplit.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSweep.c
# End Source File
# Begin Source File

1
src/aig/gia/gia.h
View File

@ -1015,6 +1015,7 @@ extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes );
extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value );
extern Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar );
extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );

94
src/aig/gia/giaDup.c
View File

@ -1237,6 +1237,100 @@ Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
return pNew;
}
/**Function*************************************************************
Synopsis [Existentially quantified given variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
assert( Gia_ManPoNum(p) == 1 );
assert( Gia_ManRegNum(p) == 0 );
Gia_ManFillValue( p );
// find the cofactoring variable
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManHashAlloc( pNew );
// compute negative cofactor
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
// compute the positive cofactor
Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// create OR gate
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Existentially quantifies the given variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupExist2( Gia_Man_t * p, int iVar )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManFillValue( p );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// first part
Gia_ManPi( p, iVar )->Value = 0; // modification!
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
// second part
Gia_ManPi( p, iVar )->Value = 1; // modification!
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = ~0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
// combination
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew->nConstrs = p->nConstrs;
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order while putting CIs first.]

22
src/base/abci/abc.c
View File

@ -32876,13 +32876,24 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose );
int c, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0;
extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose );
int c, nProcs = 1, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "TILvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PTILvh" ) ) != EOF )
{
switch ( c )
{
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" );
goto usage;
}
nProcs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nProcs <= 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
@ -32938,12 +32949,13 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" );
return 1;
}
Cec_GiaSplitTest( pAbc->pGia, nTimeOut, nIterMax, LookAhead, fVerbose );
Cec_GiaSplitTest( pAbc->pGia, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &splitprove [-TIL num] [-vh]\n" );
Abc_Print( -2, "usage: &splitprove [-PTIL num] [-vh]\n" );
Abc_Print( -2, "\t proves CEC problem by case-splitting\n" );
Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs );
Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIterMax );
Abc_Print( -2, "\t-L num : maximum look-ahead during cofactoring [default = %d]\n", LookAhead );

279
src/proof/cec/cecSplit.c
View File

@ -21,10 +21,21 @@
#include <math.h>
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
//#include "bdd/cudd/cuddInt.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "misc/util/utilTruth.h"
//#include "bdd/cudd/cuddInt.h"
//#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
//#endif
ABC_NAMESPACE_IMPL_START
@ -222,12 +233,20 @@ int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead )
Cost1 = Gia_ManAndNum(pPart);
Gia_ManStop( pPart );
if ( CostBest > Cost0 + Cost1 )
CostBest = Cost0 + Cost1, iBest = pOrder[i];
/*
pPart = Gia_ManDupExist( p, pOrder[i] );
printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d %6d -> %6d\n",
i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
Cost0, Cost1, Cost0+Cost1, Gia_ManAndNum(p), Gia_ManAndNum(pPart) );
Gia_ManStop( pPart );
*/
// printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d\n",
// i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
// Cost0, Cost1, Cost0+Cost1 );
if ( CostBest > Cost0 + Cost1 )
CostBest = Cost0 + Cost1, iBest = pOrder[i];
}
ABC_FREE( pOrder );
assert( iBest >= 0 );
@ -255,27 +274,40 @@ static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p )
Aig_ManStop( pAig );
return pCnf;
}
static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, int nTimeOut )
static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut )
{
sat_solver * pSat;
Cnf_Dat_t * pCnf;
int i;
pCnf = Cec_GiaDeriveGiaRemapped( p );
int i, fDerive = (pCnf == NULL);
if ( pCnf == NULL )
pCnf = Cec_GiaDeriveGiaRemapped( p );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
{
// the problem is UNSAT
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
return NULL;
}
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
Cnf_DataFree( pCnf );
if ( fDerive )
Cnf_DataFree( pCnf );
return pSat;
}
static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
static inline int Cnf_GiaSolveOne( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs )
{
sat_solver * pSat = Cec_GiaDeriveSolver( p, nTimeOut );
int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
*pnVars = sat_solver_nvars( pSat );
*pnConfs = sat_solver_nconflicts( pSat );
int status;
sat_solver * pSat = Cec_GiaDeriveSolver( p, pCnf, nTimeOut );
if ( pSat == NULL )
{
*pnVars = 0;
*pnConfs = 0;
return 1;
}
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
*pnVars = sat_solver_nvars( pSat );
*pnConfs = sat_solver_nconflicts( pSat );
sat_solver_delete( pSat );
if ( status == l_Undef )
return -1;
@ -299,9 +331,9 @@ static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, in
}
*/
}
static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs )
{
int status = Cnf_GiaSolveOne( p, nTimeOut, fVerbose, pnVars, pnConfs );
int status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, pnVars, pnConfs );
if ( status == -1 )
{
Vec_PtrPush( vStack, p );
@ -333,13 +365,13 @@ static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
SeeAlso []
***********************************************************************/
void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUnsat, double Prog, abctime clk )
void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fStatus, double Prog, abctime clk )
{
printf( "%6d : ", nIter );
printf( "Depth =%3d ", Depth );
printf( "SatVar =%7d ", nVars );
printf( "SatConf =%7d ", nConfs );
printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" );
printf( "%s ", fStatus ? (fStatus == 1 ? "UNSAT " : "UNDECIDED") : "SAT " );
printf( "Progress = %.10f ", Prog );
Abc_PrintTime( 1, "Time", clk );
//ABC_PRTr( "Time", Abc_Clock()-clk );
@ -366,9 +398,9 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
{
abctime clk, clkTotal = Abc_Clock();
abctime clkTotal = Abc_Clock();
Gia_Man_t * pPart0, * pPart1, * pLast;
Vec_Ptr_t * vStack;
int nSatVars, nSatConfs, fSatUnsat;
@ -381,13 +413,12 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
p->vCofVars = Vec_IntAlloc( 100 );
// start with the current problem
vStack = Vec_PtrAlloc( 1000 );
clk = Abc_Clock();
if ( !Cnf_GiaCheckOne(vStack, p, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
if ( !Cnf_GiaCheckOne(vStack, p, NULL, nTimeOut, &nSatVars, &nSatConfs) )
RetValue = 0;
else
{
if ( fVerbose )
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, 0, 0, Abc_Clock() - clk );
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, -1, Progress, Abc_Clock() - clkTotal );
for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
{
// get the last AIG
@ -403,8 +434,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
Vec_IntPush( pPart0->vCofVars, Abc_Var2Lit(iVar, 1) );
// check this AIG
fSatUnsat = Vec_PtrSize(vStack);
clk = Abc_Clock();
if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
if ( !Cnf_GiaCheckOne(vStack, pPart0, NULL, nTimeOut, &nSatVars, &nSatConfs) )
{
Gia_ManStop( pLast );
RetValue = 0;
@ -414,7 +444,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
if ( fSatUnsat )
Progress += 1.0 / pow(2, Depth + 1);
if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat?1:-1, Progress, Abc_Clock() - clkTotal );
// cofactor
pPart1 = Gia_ManDupCofactor( pLast, iVar, 1 );
// create variable
@ -424,8 +454,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
Gia_ManStop( pLast );
// check this AIG
fSatUnsat = Vec_PtrSize(vStack);
clk = Abc_Clock();
if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
if ( !Cnf_GiaCheckOne(vStack, pPart1, NULL, nTimeOut, &nSatVars, &nSatConfs) )
{
RetValue = 0;
break;
@ -434,7 +463,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
if ( fSatUnsat )
Progress += 1.0 / pow(2, Depth + 1);
if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat?1:-1, Progress, Abc_Clock() - clkTotal );
if ( nIterMax && Vec_PtrSize(vStack) >= nIterMax )
break;
}
@ -454,6 +483,198 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#define PAR_THR_MAX 100
typedef struct Par_ThData_t_
{
Gia_Man_t * p;
Cnf_Dat_t * pCnf;
int nTimeOut;
int fWorking;
int Result;
int nVars;
int nConfs;
} Par_ThData_t;
void * Cec_GiaSplitWorkerThread( void * pArg )
{
Par_ThData_t * pThData = (Par_ThData_t *)pArg;
volatile int * pPlace = &pThData->fWorking;
while ( 1 )
{
while ( *pPlace == 0 );
assert( pThData->fWorking );
if ( pThData->p == NULL )
{
pthread_exit( NULL );
assert( 0 );
return NULL;
}
pThData->Result = Cnf_GiaSolveOne( pThData->p, pThData->pCnf, pThData->nTimeOut, &pThData->nVars, &pThData->nConfs );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
{
abctime clkTotal = Abc_Clock();
Par_ThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
Vec_Ptr_t * vStack;
double Progress = 0;
int i, status, nSatVars, nSatConfs;
int nIter = 0, RetValue = -1, fWorkToDo = 1;
if ( fVerbose )
printf( "Solving CEC problem by cofactoring with the following parameters:\n" );
if ( fVerbose )
printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
if ( nProcs == 1 )
return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
// subtract manager thread
nProcs--;
assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
// check the problem
status = Cnf_GiaSolveOne( p, NULL, nTimeOut, &nSatVars, &nSatConfs );
if ( fVerbose )
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
if ( status == 0 )
{
printf( "The problem is SAT.\n" );
return 0;
}
if ( status == 1 )
{
printf( "The problem is UNSAT.\n" );
return 1;
}
assert( status == -1 );
// create local copy
p = Gia_ManDup( p );
vStack = Vec_PtrAlloc( 1000 );
Vec_PtrPush( vStack, p );
// start cofactored variables
assert( p->vCofVars == NULL );
p->vCofVars = Vec_IntAlloc( 100 );
// start threads
for ( i = 0; i < nProcs; i++ )
{
ThData[i].p = NULL;
ThData[i].pCnf = NULL;
ThData[i].nTimeOut = nTimeOut;
ThData[i].fWorking = 0;
ThData[i].Result = -1;
ThData[i].nVars = -1;
ThData[i].nConfs = -1;
status = pthread_create( WorkerThread + i, NULL,Cec_GiaSplitWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
}
// look at the threads
while ( fWorkToDo )
{
fWorkToDo = (int)(Vec_PtrSize(vStack) > 0);
for ( i = 0; i < nProcs; i++ )
{
// check if this thread is working
if ( ThData[i].fWorking )
{
fWorkToDo = 1;
continue;
}
// check if this thread has recently finished
if ( ThData[i].p != NULL )
{
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 );
if ( ThData[i].Result == 0 ) // SAT
{
RetValue = 0;
goto finish;
}
if ( ThData[i].Result == -1 ) // UNDEC
{
// determine cofactoring variable
int iVar = Gia_SplitCofVar2( pLast, LookAhead );
// cofactor
Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 );
pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
Vec_PtrPush( vStack, pPart );
// cofactor
pPart = Gia_ManDupCofactor( pLast, iVar, 1 );
pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
Vec_PtrPush( vStack, pPart );
// keep working
fWorkToDo = 1;
nIter++;
}
else
Progress += 1.0 / pow(2, Depth);
Gia_ManStopP( &ThData[i].p );
if ( ThData[i].pCnf == NULL )
continue;
Cnf_DataFree( ThData[i].pCnf );
ThData[i].pCnf = NULL;
}
if ( Vec_PtrSize(vStack) == 0 )
continue;
// start a new thread
assert( ThData[i].p == NULL );
ThData[i].p = Vec_PtrPop( vStack );
ThData[i].pCnf = Cec_GiaDeriveGiaRemapped( ThData[i].p );
ThData[i].fWorking = 1;
}
if ( nIterMax && nIter >= nIterMax )
break;
}
if ( !fWorkToDo )
RetValue = 1;
finish:
// wait till threads finish
for ( i = 0; i < nProcs; i++ )
if ( ThData[i].fWorking )
i = 0;
// stop threads
for ( i = 0; i < nProcs; i++ )
{
assert( !ThData[i].fWorking );
// cleanup
Gia_ManStopP( &ThData[i].p );
if ( ThData[i].pCnf == NULL )
continue;
Cnf_DataFree( ThData[i].pCnf );
ThData[i].pCnf = NULL;
// stop
ThData[i].p = NULL;
ThData[i].fWorking = 1;
}
// finish
Cec_GiaSplitClean( vStack );
if ( RetValue == 0 )
printf( "Problem is SAT " );
else if ( RetValue == 1 )
printf( "Problem is UNSAT " );
else if ( RetValue == -1 )
printf( "Problem is UNDECIDED " );
else assert( 0 );
printf( "after %d case-splits. ", nIter );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

48
src/sat/bmc/bmcCexDepth.c
View File

@ -35,54 +35,6 @@ extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Existentially quantified given variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
assert( Gia_ManPoNum(p) == 1 );
assert( Gia_ManRegNum(p) == 0 );
Gia_ManFillValue( p );
// find the cofactoring variable
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManHashAlloc( pNew );
// compute negative cofactor
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
// compute the positive cofactor
Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// create OR gate
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, pObj->Value, Gia_ObjFanin0Copy(pObj)) );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Performs targe enlargement of the given size.]