New command 'expand' to expand SOPs against the offset.

4 files changed, 266 insertions, 1 deletions

diff --git a/abclib.dsp b/abclib.dsp
index ae631513..58688983 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1863,6 +1863,10 @@ SOURCE=.\src\sat\bmc\bmcEco.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcExpand.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcFault.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 302b8553..94de213b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -158,6 +158,7 @@ static int Abc_CommandBidec                  ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandOrder                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCubes                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExpand                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSplitSop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReach                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -793,6 +794,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "order",         Abc_CommandOrder,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "cubes",         Abc_CommandCubes,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "expand",        Abc_CommandExpand,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "splitsop",      Abc_CommandSplitSop,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "reach",         Abc_CommandReach,            0 );
@@ -8990,7 +8992,7 @@ usage:
     Abc_Print( -2, "usage: cubes [-xh]\n" );
     Abc_Print( -2, "\t        converts the current network into a network derived by creating\n" );
     Abc_Print( -2, "\t        a separate node for each product and sum in the local SOPs\n" );
-    Abc_Print( -2, "\t-v    : toggle using XOR instead of OR [default = %s]\n", fXor? "yes": "no" );
+    Abc_Print( -2, "\t-x    : toggle using XOR instead of OR [default = %s]\n", fXor? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -9006,6 +9008,90 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandExpand( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkExpandCubes( Abc_Ntk_t * pNtk, Gia_Man_t * pGia, int fVerbose );
+    Abc_Ntk_t * pStrash, * pNtk2, * pNtk = Abc_FrameReadNtk(pAbc);
+    Gia_Man_t * pGia; int c, fVerbose;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsSopLogic(pNtk) )
+    {
+        Abc_Print( -1, "Only a SOP logic network can be transformed into cubes.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLevel(pNtk) > 1 )
+    {
+        Abc_Print( -1, "The number of logic levels is more than 1 (collapse the network and try again).\n" );
+        return 1;
+    }
+    // read the offset representation
+    if ( argc != globalUtilOptind + 1 )
+    {
+        Abc_Print( 0, "Using the complement of the current network as its offset.\n" );
+        pNtk2 = Abc_NtkDup( pNtk );
+    }
+    else
+    {
+        char * FileName = argv[globalUtilOptind];
+        pNtk2 = Io_Read( FileName, Io_ReadFileType(FileName), 1, 0 );
+        if ( pNtk2 == NULL )
+        {
+            Abc_Print( -1, "Failed to read the current network from file \"%s\".\n", FileName );
+            return 1;
+        }
+    }
+    // strash the network
+    pStrash = Abc_NtkStrash( pNtk2, 0, 1, 0 );
+    Abc_NtkDelete( pNtk2 );
+    // convert it into an AIG
+    pGia = Abc_NtkClpGia( pStrash );
+    //Gia_AigerWrite( pGia, "aig_dump.aig", 0, 0 );
+    Abc_NtkDelete( pStrash );
+    // get the new network
+    Abc_NtkExpandCubes( pNtk, pGia, fVerbose );
+    Gia_ManStop( pGia );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: expand [-vh] <file>\n" );
+    Abc_Print( -2, "\t        expands cubes against the offset\n" );
+    Abc_Print( -2, "\t-v    : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "\tfile  : (optional) representation of on-set plus dc-set\n");
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSplitSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Abc_Ntk_t * Abc_NtkSplitSop( Abc_Ntk_t * pNtk, int nCubesMax, int fVerbose );
diff --git a/src/sat/bmc/bmcExpand.c b/src/sat/bmc/bmcExpand.c
new file mode 100644
index 00000000..f3ec999e
--- /dev/null
+++ b/src/sat/bmc/bmcExpand.c
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+  FileName    [bmcExpand.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Expanding cubes against the offset.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcExpand.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "base/abc/abc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// iterator thought the cubes
+#define Bmc_SopForEachCube( pSop, nVars, pCube )  for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
+
+extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Expands cubes against the offset given as an AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjExpandCubesTry( Vec_Str_t * vSop, sat_solver * pSat, Vec_Int_t * vVars )
+{
+    extern int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit );
+
+    char * pCube, * pSop = Vec_StrArray(vSop);
+    int nCubes = Abc_SopGetCubeNum(pSop);
+    int nVars = Abc_SopGetVarNum(pSop);
+
+    Vec_Int_t * vLits = Vec_IntAlloc( nVars );
+    Vec_Int_t * vTemp = Vec_IntAlloc( nVars );
+
+    assert( nVars == Vec_IntSize(vVars) );
+    assert( Vec_StrSize(vSop) == nCubes * (nVars + 3) + 1 );
+    Bmc_SopForEachCube( pSop, nVars, pCube )
+    {
+        int k, Entry;
+        // collect literals and clean cube
+        Vec_IntFill( vLits, nVars, -1 );
+        for ( k = 0; k < nVars; k++ )
+        {
+            if ( pCube[k] == '-' )
+                continue;
+            Vec_IntWriteEntry( vLits, k, Abc_Var2Lit(Vec_IntEntry(vVars, k), pCube[k] == '0') );
+            pCube[k] = '-';
+        }
+        // expand cube
+        Bmc_CollapseExpandRound( pSat, NULL, vLits, NULL, vTemp, 0, 0, -1 );
+        // insert literals
+        Vec_IntForEachEntry( vLits, Entry, k )
+            if ( Entry != -1 )
+                pCube[k] = '1' - Abc_LitIsCompl(Entry);
+    }
+
+    Vec_IntFree( vLits );
+    Vec_IntFree( vTemp );
+    return nCubes;
+}
+int Abc_ObjExpandCubes( Vec_Str_t * vSop, Gia_Man_t * p, int nVars )
+{
+    extern int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars );
+
+    int fReverse = 0;
+    Vec_Int_t * vVars = Vec_IntAlloc( nVars );
+    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    int v, n, iLit, status, nCubesNew, iCiVarBeg = sat_solver_nvars(pSat) - nVars;
+
+    // check that on-set/off-set is sat
+    int iOutVar = 1;
+    for ( n = 0; n < 2; n++ )
+    {
+        iLit  = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1   n=1 => F=0
+        status = sat_solver_solve( pSat, &iLit, &iLit + 1, 0, 0, 0, 0 );
+        if ( status == l_False )
+        {
+            Vec_StrClear( vSop );
+            Vec_StrPrintStr( vSop, n ? " 1\n" : " 0\n" );
+            Vec_StrPush( vSop, '\0' );
+            return 1;
+        }
+    }
+
+    // add literals to the solver
+    iLit  = Abc_Var2Lit( iOutVar, 1 ); 
+    status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
+    assert( status );
+
+    // collect variables
+    if ( fReverse )
+        for ( v = nVars - 1; v >= 0; v-- )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+    else
+        for ( v = 0; v < nVars; v++ )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+
+    nCubesNew = Abc_ObjExpandCubesTry( vSop, pSat, vVars );
+
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Vec_IntFree( vVars );
+    if ( nCubesNew > 1 )
+        Bmc_CollapseIrredundantFull( vSop, nCubesNew, nVars );
+    return 0;
+}
+void Abc_NtkExpandCubes( Abc_Ntk_t * pNtk, Gia_Man_t * pGia, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Abc_Obj_t * pObj; int i;
+    Vec_Str_t * vSop = Vec_StrAlloc( 1000 );
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    assert( Abc_NtkCiNum(pNtk) == Gia_ManCiNum(pGia) );
+    assert( Abc_NtkCoNum(pNtk) == Gia_ManCoNum(pGia) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pObj = Abc_ObjFanin0(pObj);
+        if ( !Abc_ObjIsNode(pObj) || Abc_ObjFaninNum(pObj) == 0 )
+            continue;
+        assert( Abc_ObjFaninNum(pObj) == Gia_ManCiNum(pGia) );
+
+        Vec_StrClear( vSop );
+        Vec_StrAppend( vSop, (char *)pObj->pData );
+        Vec_StrPush( vSop, '\0' );
+
+        pNew = Gia_ManDupCones( pGia, &i, 1, 0 );
+        assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pGia) );
+        if ( Abc_ObjExpandCubes( vSop, pNew, Abc_ObjFaninNum(pObj) ) )
+            Vec_IntClear( &pObj->vFanins );
+        Gia_ManStop( pNew );
+
+        pObj->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, Vec_StrArray(vSop) );
+    }
+    Vec_StrFree( vSop );
+    Abc_NtkSortSops( pNtk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 6d09b15c..e1777df8 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -13,6 +13,7 @@ SRC +=    src/sat/bmc/bmcBCore.c \
     src/sat/bmc/bmcChain.c \
     src/sat/bmc/bmcClp.c \
     src/sat/bmc/bmcEco.c \
+    src/sat/bmc/bmcExpand.c \
     src/sat/bmc/bmcFault.c \
     src/sat/bmc/bmcFx.c \
     src/sat/bmc/bmcICheck.c \