Skip to content

A
abc
Commit d4c70cb6 by Alan Mishchenko
Options

Updates for the new BMC engine.

parent 2fa9645b
Showing with 91 additions and 40 deletions
src/base/abci/abc.c
...@@ -393,6 +393,7 @@ static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, cha ...@@ -393,6 +393,7 @@ static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -948,6 +949,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -948,6 +949,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
...@@ -31774,7 +31776,6 @@ usage: ...@@ -31774,7 +31776,6 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
// extern void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars );
int c; int c;
Bmc_AndPar_t Pars, * pPars = &Pars; Bmc_AndPar_t Pars, * pPars = &Pars;
memset( pPars, 0, sizeof(Bmc_AndPar_t) ); memset( pPars, 0, sizeof(Bmc_AndPar_t) );
...@@ -31836,10 +31837,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -31836,10 +31837,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( pAbc->pGia == NULL ) if ( pAbc->pGia == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9Rpm(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9Bmc(): There is no AIG.\n" );
return 0; return 0;
} }
// Bmc_PerformBmc( pAbc->pGia, pPars );
Gia_ManBmcPerform( pAbc->pGia, pPars ); Gia_ManBmcPerform( pAbc->pGia, pPars );
return 0; return 0;
...@@ -31867,6 +31867,55 @@ usage: ...@@ -31867,6 +31867,55 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9SatTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Bmc_LoadTest( Gia_Man_t * pGia, int fLoadCnf, int fVerbose );
int c, fLoadCnf = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
{
switch ( c )
{
case 'c':
fLoadCnf ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SatTest(): There is no AIG.\n" );
return 0;
}
Bmc_LoadTest( pAbc->pGia, fLoadCnf, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &sattest [-cvh]\n" );
Abc_Print( -2, "\t performs testing of dynamic CNF loading\n" );
Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", fLoadCnf? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
return -1; return -1;
src/sat/bmc/bmcLoad.c
...@@ -28,8 +28,8 @@ ABC_NAMESPACE_IMPL_START ...@@ -28,8 +28,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Bmc_Lad_t_ Bmc_Lad_t; typedef struct Bmc_Load_t_ Bmc_Load_t;
struct Bmc_Lad_t_ struct Bmc_Load_t_
{ {
Bmc_AndPar_t * pPars; // parameters Bmc_AndPar_t * pPars; // parameters
Gia_Man_t * pGia; // unrolled AIG Gia_Man_t * pGia; // unrolled AIG
...@@ -57,7 +57,7 @@ struct Bmc_Lad_t_ ...@@ -57,7 +57,7 @@ struct Bmc_Lad_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Bmc_LadGetSatVar( Bmc_Lad_t * p, int Id ) int Bmc_LoadGetSatVar( Bmc_Load_t * p, int Id )
{ {
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Id ); Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Id );
if ( pObj->Value == 0 ) if ( pObj->Value == 0 )
...@@ -68,9 +68,9 @@ int Bmc_LadGetSatVar( Bmc_Lad_t * p, int Id ) ...@@ -68,9 +68,9 @@ int Bmc_LadGetSatVar( Bmc_Lad_t * p, int Id )
} }
return pObj->Value; return pObj->Value;
} }
int Bmc_LadAddCnf( void * pMan, int iLit ) int Bmc_LoadAddCnf( void * pMan, int iLit )
{ {
Bmc_Lad_t * p = (Bmc_Lad_t *)pMan; Bmc_Load_t * p = (Bmc_Load_t *)pMan;
int Lits[3], iVar = Abc_Lit2Var(iLit); int Lits[3], iVar = Abc_Lit2Var(iLit);
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vSat2Id, iVar) ); Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vSat2Id, iVar) );
p->nCallBacks1++; p->nCallBacks1++;
...@@ -82,32 +82,32 @@ int Bmc_LadAddCnf( void * pMan, int iLit ) ...@@ -82,32 +82,32 @@ int Bmc_LadAddCnf( void * pMan, int iLit )
Lits[0] = Abc_LitNot(iLit); Lits[0] = Abc_LitNot(iLit);
if ( Abc_LitIsCompl(iLit) ) if ( Abc_LitIsCompl(iLit) )
{ {
Lits[1] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId0p(p->pGia, pObj)), !Gia_ObjFaninC0(pObj) ); Lits[1] = Abc_Var2Lit( Bmc_LoadGetSatVar(p, Gia_ObjFaninId0p(p->pGia, pObj)), !Gia_ObjFaninC0(pObj) );
Lits[2] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId1p(p->pGia, pObj)), !Gia_ObjFaninC1(pObj) ); Lits[2] = Abc_Var2Lit( Bmc_LoadGetSatVar(p, Gia_ObjFaninId1p(p->pGia, pObj)), !Gia_ObjFaninC1(pObj) );
sat_solver_clause_new( p->pSat, Lits, Lits + 3, 0 ); sat_solver_clause_new( p->pSat, Lits, Lits + 3, 0 );
pObj->fMark1 = 1; pObj->fMark1 = 1;
} }
else else
{ {
Lits[1] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId0p(p->pGia, pObj)), Gia_ObjFaninC0(pObj) ); Lits[1] = Abc_Var2Lit( Bmc_LoadGetSatVar(p, Gia_ObjFaninId0p(p->pGia, pObj)), Gia_ObjFaninC0(pObj) );
sat_solver_clause_new( p->pSat, Lits, Lits + 2, 0 ); sat_solver_clause_new( p->pSat, Lits, Lits + 2, 0 );
Lits[1] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId1p(p->pGia, pObj)), Gia_ObjFaninC1(pObj) ); Lits[1] = Abc_Var2Lit( Bmc_LoadGetSatVar(p, Gia_ObjFaninId1p(p->pGia, pObj)), Gia_ObjFaninC1(pObj) );
sat_solver_clause_new( p->pSat, Lits, Lits + 2, 0 ); sat_solver_clause_new( p->pSat, Lits, Lits + 2, 0 );
pObj->fMark0 = 1; pObj->fMark0 = 1;
} }
p->nCallBacks2++; p->nCallBacks2++;
return 1; return 1;
} }
int Bmc_LadAddCnf_rec( Bmc_Lad_t * p, int Id ) int Bmc_LoadAddCnf_rec( Bmc_Load_t * p, int Id )
{ {
int iVar = Bmc_LadGetSatVar( p, Id ); int iVar = Bmc_LoadGetSatVar( p, Id );
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Id ); Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Id );
if ( Gia_ObjIsAnd(pObj) && !(pObj->fMark0 && pObj->fMark1) ) if ( Gia_ObjIsAnd(pObj) && !(pObj->fMark0 && pObj->fMark1) )
{ {
Bmc_LadAddCnf( p, Abc_Var2Lit(iVar, 0) ); Bmc_LoadAddCnf( p, Abc_Var2Lit(iVar, 0) );
Bmc_LadAddCnf( p, Abc_Var2Lit(iVar, 1) ); Bmc_LoadAddCnf( p, Abc_Var2Lit(iVar, 1) );
Bmc_LadAddCnf_rec( p, Gia_ObjFaninId0(pObj, Id) ); Bmc_LoadAddCnf_rec( p, Gia_ObjFaninId0(pObj, Id) );
Bmc_LadAddCnf_rec( p, Gia_ObjFaninId1(pObj, Id) ); Bmc_LoadAddCnf_rec( p, Gia_ObjFaninId1(pObj, Id) );
} }
return iVar; return iVar;
} }
...@@ -123,30 +123,24 @@ int Bmc_LadAddCnf_rec( Bmc_Lad_t * p, int Id ) ...@@ -123,30 +123,24 @@ int Bmc_LadAddCnf_rec( Bmc_Lad_t * p, int Id )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Bmc_Lad_t * Bmc_LadStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) Bmc_Load_t * Bmc_LoadStart( Gia_Man_t * pGia )
{ {
Bmc_Lad_t * p; Bmc_Load_t * p;
int Lit; int Lit;
Gia_ManSetPhase( pGia ); Gia_ManSetPhase( pGia );
Gia_ManCleanValue( pGia ); Gia_ManCleanValue( pGia );
Gia_ManCreateRefs( pGia ); Gia_ManCreateRefs( pGia );
p = ABC_CALLOC( Bmc_Lad_t, 1 ); p = ABC_CALLOC( Bmc_Load_t, 1 );
p->pPars = pPars;
p->pGia = pGia; p->pGia = pGia;
p->pSat = sat_solver_new(); p->pSat = sat_solver_new();
p->vSat2Id = Vec_IntAlloc( 1000 ); p->vSat2Id = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vSat2Id, 0 ); Vec_IntPush( p->vSat2Id, 0 );
// create constant node // create constant node
Lit = Abc_Var2Lit( Bmc_LadGetSatVar(p, 0), 1 ); Lit = Abc_Var2Lit( Bmc_LoadGetSatVar(p, 0), 1 );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
// add callback for CNF loading
if ( pPars->fLoadCnf )
p->pSat->pCnfMan = p;
if ( pPars->fLoadCnf )
p->pSat->pCnfFunc = Bmc_LadAddCnf;
return p; return p;
} }
void Bmc_LadStop( Bmc_Lad_t * p ) void Bmc_LoadStop( Bmc_Load_t * p )
{ {
Vec_IntFree( p->vSat2Id ); Vec_IntFree( p->vSat2Id );
sat_solver_delete( p->pSat ); sat_solver_delete( p->pSat );
...@@ -164,28 +158,36 @@ void Bmc_LadStop( Bmc_Lad_t * p ) ...@@ -164,28 +158,36 @@ void Bmc_LadStop( Bmc_Lad_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) void Bmc_LoadTest( Gia_Man_t * pGia, int fLoadCnf, int fVerbose )
{ {
// int nConfLimit = 0; int nConfLimit = 0;
Bmc_Lad_t * p; Bmc_Load_t * p;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i, status, Lit; int i, status, Lit;
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
p = Bmc_LadStart( pGia, pPars ); // create the loading manager
p = Bmc_LoadStart( pGia );
// add callback for CNF loading
if ( fLoadCnf )
{
p->pSat->pCnfMan = p;
p->pSat->pCnfFunc = Bmc_LoadAddCnf;
}
// solve SAT problem for each PO
Gia_ManForEachPo( pGia, pObj, i ) Gia_ManForEachPo( pGia, pObj, i )
{ {
if ( pPars->fLoadCnf ) if ( fLoadCnf )
Lit = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) ); Lit = Abc_Var2Lit( Bmc_LoadGetSatVar(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) );
else else
Lit = Abc_Var2Lit( Bmc_LadAddCnf_rec(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) ); Lit = Abc_Var2Lit( Bmc_LoadAddCnf_rec(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) );
if ( pPars->fVerbose ) if ( fVerbose )
{ {
printf( "Frame%4d : ", i ); printf( "Frame%4d : ", i );
printf( "Vars = %6d ", Vec_IntSize(p->vSat2Id) ); printf( "Vars = %6d ", Vec_IntSize(p->vSat2Id) );
printf( "Clas = %6d ", sat_solver_nclauses(p->pSat) ); printf( "Clas = %6d ", sat_solver_nclauses(p->pSat) );
} }
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( pPars->fVerbose ) if ( fVerbose )
{ {
printf( "Conf = %6d ", sat_solver_nconflicts(p->pSat) ); printf( "Conf = %6d ", sat_solver_nconflicts(p->pSat) );
if ( status == l_False ) if ( status == l_False )
...@@ -198,7 +200,7 @@ void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -198,7 +200,7 @@ void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
} }
} }
printf( "Callbacks = %d. Loadings = %d.\n", p->nCallBacks1, p->nCallBacks2 ); printf( "Callbacks = %d. Loadings = %d.\n", p->nCallBacks1, p->nCallBacks2 );
Bmc_LadStop( p ); Bmc_LoadStop( p );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
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