Updates for the new BMC engine.

2 files changed, 91 insertions, 40 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 19f87767..f4c89526 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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_CommandAbc9MultiProve         ( 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_CommandAbc9CexCut             ( 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 )
     Cmd_CommandAdd( pAbc, "ABC9",         "&popart",       Abc_CommandAbc9PoPart,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   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",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -31774,7 +31776,6 @@ usage:
 ***********************************************************************/
 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;
     Bmc_AndPar_t Pars, * pPars = &Pars;
     memset( pPars, 0, sizeof(Bmc_AndPar_t) );
@@ -31836,10 +31837,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     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;
     }
-//    Bmc_PerformBmc( pAbc->pGia, pPars );
     Gia_ManBmcPerform( pAbc->pGia, pPars );
     return 0;
 
@@ -31867,6 +31867,55 @@ usage:
   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 )
 {
     return -1;
diff --git a/src/sat/bmc/bmcLoad.c b/src/sat/bmc/bmcLoad.c
index 757188ee..31bbc789 100644
--- a/src/sat/bmc/bmcLoad.c
+++ b/src/sat/bmc/bmcLoad.c
@@ -28,8 +28,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Bmc_Lad_t_ Bmc_Lad_t;  
-struct Bmc_Lad_t_
+typedef struct Bmc_Load_t_ Bmc_Load_t;  
+struct Bmc_Load_t_
 {
     Bmc_AndPar_t *   pPars;     // parameters
     Gia_Man_t *      pGia;      // unrolled AIG
@@ -57,7 +57,7 @@ struct Bmc_Lad_t_
   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 );
     if ( pObj->Value == 0 )
@@ -68,9 +68,9 @@ int Bmc_LadGetSatVar( Bmc_Lad_t * p, int Id )
     }
     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);
     Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vSat2Id, iVar) );
     p->nCallBacks1++;
@@ -82,32 +82,32 @@ int Bmc_LadAddCnf( void * pMan, int iLit )
     Lits[0] = Abc_LitNot(iLit);
     if ( Abc_LitIsCompl(iLit) )
     {
-        Lits[1] = Abc_Var2Lit( Bmc_LadGetSatVar(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[1] = Abc_Var2Lit( Bmc_LoadGetSatVar(p, Gia_ObjFaninId0p(p->pGia, pObj)), !Gia_ObjFaninC0(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 );
         pObj->fMark1 = 1;
     }
     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 );
-        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 );
         pObj->fMark0 = 1;
     }
     p->nCallBacks2++;
     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 );
     if ( Gia_ObjIsAnd(pObj) && !(pObj->fMark0 && pObj->fMark1) )
     {
-        Bmc_LadAddCnf( p, Abc_Var2Lit(iVar, 0) );
-        Bmc_LadAddCnf( p, Abc_Var2Lit(iVar, 1) );
-        Bmc_LadAddCnf_rec( p, Gia_ObjFaninId0(pObj, Id) );
-        Bmc_LadAddCnf_rec( p, Gia_ObjFaninId1(pObj, Id) );
+        Bmc_LoadAddCnf( p, Abc_Var2Lit(iVar, 0) );
+        Bmc_LoadAddCnf( p, Abc_Var2Lit(iVar, 1) );
+        Bmc_LoadAddCnf_rec( p, Gia_ObjFaninId0(pObj, Id) );
+        Bmc_LoadAddCnf_rec( p, Gia_ObjFaninId1(pObj, Id) );
     }
     return iVar;
 }
@@ -123,30 +123,24 @@ int Bmc_LadAddCnf_rec( Bmc_Lad_t * p, int Id )
   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;
     Gia_ManSetPhase( pGia );
     Gia_ManCleanValue( pGia );
     Gia_ManCreateRefs( pGia );
-    p = ABC_CALLOC( Bmc_Lad_t, 1 );
-    p->pPars     = pPars;
+    p = ABC_CALLOC( Bmc_Load_t, 1 );
     p->pGia      = pGia;
     p->pSat      = sat_solver_new();
     p->vSat2Id   = Vec_IntAlloc( 1000 );
     Vec_IntPush( p->vSat2Id, 0 );
     // 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 );
-    // add callback for CNF loading
-    if ( pPars->fLoadCnf )
-        p->pSat->pCnfMan  = p;
-    if ( pPars->fLoadCnf )
-        p->pSat->pCnfFunc = Bmc_LadAddCnf;
     return p;
 }
-void Bmc_LadStop( Bmc_Lad_t * p )
+void Bmc_LoadStop( Bmc_Load_t * p )
 {
     Vec_IntFree( p->vSat2Id );
     sat_solver_delete( p->pSat );
@@ -164,28 +158,36 @@ void Bmc_LadStop( Bmc_Lad_t * p )
   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;
-    Bmc_Lad_t * p;
+    int nConfLimit = 0;
+    Bmc_Load_t * p;
     Gia_Obj_t * pObj;
     int i, status, Lit;
     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 )
     {
-        if ( pPars->fLoadCnf )
-            Lit = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) );
+        if ( fLoadCnf )
+            Lit = Abc_Var2Lit( Bmc_LoadGetSatVar(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) );
         else
-            Lit = Abc_Var2Lit( Bmc_LadAddCnf_rec(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) );
-        if ( pPars->fVerbose )
+            Lit = Abc_Var2Lit( Bmc_LoadAddCnf_rec(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) );
+        if ( fVerbose )
         {
             printf( "Frame%4d :  ", i );
             printf( "Vars = %6d  ", Vec_IntSize(p->vSat2Id) );
             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 );
-        if ( pPars->fVerbose )
+        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 ( fVerbose )
         {
             printf( "Conf = %6d  ", sat_solver_nconflicts(p->pSat) );
             if ( status == l_False )
@@ -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 );
-    Bmc_LadStop( p );
+    Bmc_LoadStop( p );
 }
 
 ////////////////////////////////////////////////////////////////////////