/**CFile****************************************************************
FileName [bmcBCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Performs recording of BMC core.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcBCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satStore.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Collect pivot variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Bmc_ManBCoreReadPivots( char * pName )
{
int Num;
Vec_Int_t * vPivots = Vec_IntAlloc( 100 );
FILE * pFile = fopen( pName, "r" );
while ( fscanf( pFile, "%d", &Num ) == 1 )
Vec_IntPush( vPivots, Num );
fclose( pFile );
return vPivots;
}
Vec_Int_t * Bmc_ManBCoreCollectPivots( Gia_Man_t * p, char * pName, Vec_Int_t * vVarMap )
{
Gia_Obj_t * pObj;
int i, iVar, iFrame;
Vec_Int_t * vPivots = Vec_IntAlloc( 100 );
Vec_Int_t * vVars = Bmc_ManBCoreReadPivots( pName );
Gia_ManForEachObj( p, pObj, i )
pObj->fMark0 = 0;
Vec_IntForEachEntry( vVars, iVar, i )
if ( iVar > 0 && iVar < Gia_ManObjNum(p) )
Gia_ManObj( p, iVar )->fMark0 = 1;
else
printf( "Cannot find object with Id %d in the given AIG.\n", iVar );
Vec_IntForEachEntryDouble( vVarMap, iVar, iFrame, i )
if ( Gia_ManObj( p, iVar )->fMark0 )
Vec_IntPush( vPivots, Abc_Lit2Var(i) );
Gia_ManForEachObj( p, pObj, i )
pObj->fMark0 = 0;
Vec_IntFree( vVars );
return vPivots;
}
/**Function*************************************************************
Synopsis [Collect (Id; Frame) pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Bmc_ManBCoreAssignVar( Gia_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vNodes )
{
pObj->Value = Abc_Lit2Var(Vec_IntSize(vNodes));
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
Vec_IntPush( vNodes, f );
// printf( "Obj %3d Frame %3d ---> Var %3d ", Gia_ObjId(p, pObj), f, pObj->Value );
// Gia_ObjPrint( p, pObj );
}
void Bmc_ManBCoreCollect_rec( Gia_Man_t * p, int Id, int f, Vec_Int_t * vNodes, Vec_Int_t * vRootsNew )
{
Gia_Obj_t * pObj;
if ( Gia_ObjIsTravIdCurrentId(p, Id) )
return;
Gia_ObjSetTravIdCurrentId(p, Id);
pObj = Gia_ManObj( p, Id );
Bmc_ManBCoreAssignVar( p, pObj, f, vNodes );
if ( Gia_ObjIsPi(p, pObj) )
return;
if ( Gia_ObjIsRo(p, pObj) )
{
Vec_IntPush( vRootsNew, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId0p(p, pObj), f, vNodes, vRootsNew );
Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId1p(p, pObj), f, vNodes, vRootsNew );
}
Vec_Int_t * Bmc_ManBCoreCollect( Gia_Man_t * p, int iFrame, int iOut, sat_solver * pSat )
{
Gia_Obj_t * pObj;
int f, i, iObj, nNodesOld;
Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
Vec_Int_t * vRoots2 = Vec_IntAlloc( 100 );
assert( iFrame >= 0 && iOut >= 0 );
// add first variables
Vec_IntPush( vNodes, -1 );
Vec_IntPush( vNodes, -1 );
Bmc_ManBCoreAssignVar( p, Gia_ManPo(p, iOut), iFrame, vNodes );
// start with root node
Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManPo(p, iOut)) );
// iterate through time frames
for ( f = iFrame; f >= 0; f-- )
{
Gia_ManIncrementTravId( p );
// add constant node
Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
Bmc_ManBCoreAssignVar( p, Gia_ManConst0(p), f, vNodes );
sat_solver_add_const( pSat, Gia_ManConst0(p)->Value, 1 );
// collect nodes in this timeframe
Vec_IntClear( vRoots2 );
nNodesOld = Vec_IntSize(vNodes);
Gia_ManForEachObjVec( vRoots, p, pObj, i )
Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId0p(p, pObj), f, vNodes, vRoots2 );
if ( f == iFrame )
{
// add the final clause
pObj = Gia_ManPo(p, iOut);
assert( pObj->Value == 1 );
assert( Gia_ObjFanin0(pObj)->Value == 3 );
// sat_solver_add_const( pSat, Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
sat_solver_add_constraint( pSat, Gia_ObjFanin0(pObj)->Value, pObj->Value, Gia_ObjFaninC0(pObj) );
}
else
{
// connect current RIs to previous ROs
Gia_ManForEachObjVec( vRoots, p, pObj, i )
sat_solver_add_buffer( pSat, pObj->Value, Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
}
Gia_ManForEachObjVec( vRoots2, p, pObj, i )
pObj->Value = Gia_ObjRiToRo(p, pObj)->Value;
// add nodes of this timeframe
Vec_IntForEachEntryStart( vNodes, iObj, i, nNodesOld )
{
pObj = Gia_ManObj(p, iObj); i++;
if ( Gia_ObjIsCi(pObj) )
continue;
assert( Gia_ObjIsAnd(pObj) );
sat_solver_add_and( pSat, pObj->Value, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
}
// collect constant node
ABC_SWAP( Vec_Int_t *, vRoots, vRoots2 );
}
// add constraint variables for the init state
Gia_ManForEachObjVec( vRoots, p, pObj, i )
{
sat_solver_add_constraint( pSat, pObj->Value, Abc_Lit2Var(Vec_IntSize(vNodes)), 1 );
pObj = Gia_ObjRiToRo(p, pObj);
Bmc_ManBCoreAssignVar( p, pObj, -1, vNodes );
}
Vec_IntFree( vRoots );
Vec_IntFree( vRoots2 );
return vNodes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars )
{
clock_t clk = clock();
Intp_Man_t * pManProof;
Vec_Int_t * vVarMap, * vCore;
sat_solver * pSat;
FILE * pFile;
void * pSatCnf;
int RetValue;
// create SAT solver
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
sat_solver_setnvars( pSat, 1000 );
sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
vVarMap = Bmc_ManBCoreCollect( p, pPars->iFrame, pPars->iOutput, pSat );
sat_solver_store_mark_roots( pSat );
// create pivot variables
if ( pPars->pFilePivots )
{
Vec_Int_t * vPivots = Bmc_ManBCoreCollectPivots(p, pPars->pFilePivots, vVarMap);
sat_solver_set_pivot_variables( pSat, Vec_IntArray(vPivots), Vec_IntSize(vPivots) );
Vec_IntReleaseArray( vPivots );
Vec_IntFree( vPivots );
}
// solve the problem
RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_Undef )
{
Vec_IntFree( vVarMap );
sat_solver_delete( pSat );
printf( "Timeout of conflict limit is reached.\n" );
return;
}
if ( RetValue == l_True )
{
Vec_IntFree( vVarMap );
sat_solver_delete( pSat );
printf( "The BMC problem is SAT.\n" );
return;
}
if ( pPars->fVerbose )
{
printf( "SAT solver returned UNSAT after %7d conflicts. ", (int)pSat->stats.conflicts );
Abc_PrintTime( 1, "Time", clock() - clk );
}
assert( RetValue == l_False );
pSatCnf = sat_solver_store_release( pSat );
// Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" );
// derive the UNSAT core
clk = clock();
pManProof = Intp_ManAlloc();
vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 1, pPars->fVerbose );
Intp_ManFree( pManProof );
if ( pPars->fVerbose )
{
printf( "UNSAT core contains %d (out of %d) learned clauses. ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
// write the problem
Vec_IntSort( vCore, 0 );
pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout;
Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap );
if ( pFile != stdout )
fclose( pFile );
// cleanup
Sto_ManFree( (Sto_Man_t *)pSatCnf );
Vec_IntFree( vVarMap );
Vec_IntFree( vCore );
sat_solver_delete( pSat );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END