Added new command 'outdec'.

5 files changed, 317 insertions, 0 deletions

diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index a83ac5e2..c98fb860 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -11,6 +11,7 @@ SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigInd.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigMiter.c \
+    src/aig/saig/saigOutDec.c \
     src/aig/saig/saigPba.c \
     src/aig/saig/saigPhase.c \
     src/aig/saig/saigRetFwd.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index c21ac625..af4d904e 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -169,6 +169,8 @@ extern Aig_Man_t *       Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * p
 extern int               Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
 extern int               Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
 extern int               Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose );
+/*=== saigOutdec.c ==========================================================*/
+extern Aig_Man_t *       Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose );
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
diff --git a/src/aig/saig/saigOutDec.c b/src/aig/saig/saigOutDec.c
new file mode 100644
index 00000000..d8cc591e
--- /dev/null
+++ b/src/aig/saig/saigOutDec.c
@@ -0,0 +1,205 @@
+/**CFile****************************************************************
+
+  FileName    [saigOutDec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Output cone decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigOutDec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the property output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_ManFindPrimes( Aig_Man_t * pAig, int nLits, int fVerbose )
+{
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj0, * pObj1, * pRoot, * pMiter;
+    Vec_Ptr_t * vPrimes, * vNodes;
+    Vec_Int_t * vCube, * vMarks;
+    int i0, i1, m, RetValue, Lits[10];
+    int fCompl0, fCompl1, nNodes1, nNodes2;
+    assert( nLits == 1 || nLits == 2 );
+    assert( nLits < 10 );
+
+    // create SAT solver
+    pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) ); 
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+
+    // collect nodes in the property output cone
+    pMiter = Aig_ManPo( pAig, 0 );
+    pRoot  = Aig_ObjFanin0( pMiter );
+    vNodes = Aig_ManDfsNodes( pAig, &pRoot, 1 );
+    // sort nodes by level and remove the last few
+ 
+    // try single nodes
+    vPrimes = Vec_PtrAlloc( 100 );
+    // create assumptions
+    vMarks = Vec_IntStart( Vec_PtrSize(vNodes) );
+    Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pMiter)], 1 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj0, i0 )
+    if ( pObj0 != pRoot )
+    {
+        // create assumptions
+        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj0)], pObj0->fPhase );
+        // solve the problem
+        RetValue = sat_solver_solve( pSat, Lits, Lits+2, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        if ( RetValue == l_False )
+        {
+            vCube = Vec_IntAlloc( 1 );
+            Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj0), pObj0->fPhase) );
+            Vec_PtrPush( vPrimes, vCube );
+            if ( fVerbose )
+            printf( "Adding prime %d%c\n", Aig_ObjId(pObj0),  pObj0->fPhase?'-':'+' );
+            Vec_IntWriteEntry( vMarks, i0, 1 );
+        }
+    }
+    nNodes1 = Vec_PtrSize(vPrimes);
+    if ( nLits > 1 )
+    {
+        // try adding second literal
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj0, i0 )
+        if ( pObj0 != pRoot )
+        Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pObj1, i1, i0+1 )
+        if ( pObj1 != pRoot )
+        {
+            if ( Vec_IntEntry(vMarks,i0) || Vec_IntEntry(vMarks,i1) )
+                continue;
+            for ( m = 0; m < 3; m++ )
+            {
+                fCompl0 =  m & 1;
+                fCompl1 = (m >> 1) & 1;
+                // create assumptions
+                Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj0)], fCompl0 ^ pObj0->fPhase );
+                Lits[2] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj1)], fCompl1 ^ pObj1->fPhase );
+                // solve the problem
+                RetValue = sat_solver_solve( pSat, Lits, Lits+3, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+                if ( RetValue == l_False )
+                {
+                    vCube = Vec_IntAlloc( 2 );
+                    Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj0), fCompl0 ^ pObj0->fPhase) );
+                    Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj1), fCompl1 ^ pObj1->fPhase) );
+                    Vec_PtrPush( vPrimes, vCube );
+                    if ( fVerbose )
+                    printf( "Adding prime %d%c %d%c\n", 
+                        Aig_ObjId(pObj0), (fCompl0 ^ pObj0->fPhase)?'-':'+', 
+                        Aig_ObjId(pObj1), (fCompl1 ^ pObj1->fPhase)?'-':'+' );
+                    break;
+                }
+            }
+        }
+    }
+    nNodes2 = Vec_PtrSize(vPrimes) - nNodes1;
+
+    printf( "Property cone size = %6d    1-lit primes = %5d    2-lit primes = %5d\n", 
+        Vec_PtrSize(vNodes), nNodes1, nNodes2 );
+
+    // clean up
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vMarks );
+    return vPrimes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the property output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose )
+{
+    Aig_Man_t * pAigNew = NULL;
+    Aig_Obj_t * pObj, * pMiter;
+    Vec_Ptr_t * vPrimes;
+    Vec_Int_t * vCube;
+    int i, k, Lit;
+
+    // compute primes of the comb output function
+    vPrimes = Saig_ManFindPrimes( pAig, nLits, fVerbose );
+
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+    pAigNew->nConstrs = pAig->nConstrs;
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // create variables for PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pAigNew );
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create original POs of the circuit
+    Saig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    // create prime POs of the circuit
+    if ( vPrimes )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPrimes, vCube, k )
+    {
+        pMiter = Aig_ManConst1( pAigNew );
+        Vec_IntForEachEntry( vCube, Lit, i )
+        {
+            pObj = Aig_NotCond( Aig_ObjCopy(Aig_ManObj(pAig, Aig_Lit2Var(Lit))), Aig_LitIsCompl(Lit) );
+            pMiter = Aig_And( pAigNew, pMiter, pObj );
+        }
+        Aig_ObjCreatePo( pAigNew, pMiter );
+    }
+    // transfer to register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+
+    Vec_VecFreeP( (Vec_Vec_t **)&vPrimes );
+    return pAigNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 13411203..15d29df2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -160,6 +160,7 @@ static int Abc_CommandCover                  ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandDouble                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInter                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBb2Wb                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOutdec                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandQuaVar                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -579,6 +580,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "double",        Abc_CommandDouble,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "inter",         Abc_CommandInter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "bb2wb",         Abc_CommandBb2Wb,            0 );
+    Cmd_CommandAdd( pAbc, "Various",      "outdec",        Abc_CommandOutdec,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 //    Cmd_CommandAdd( pAbc, "Various",      "qbf_solve",     Abc_CommandTest,               0 );
 
@@ -8419,6 +8421,82 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandOutdec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Abc_NtkDarOutdec( Abc_Ntk_t * pNtk, int nLits, int fVerbose );
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Abc_Ntk_t * pNtkRes;
+    int c, nLits = 1;
+    int fVerbose = 0;
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Lvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLits = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLits < 1 || nLits > 2 ) 
+            {
+                printf( "Currently, command \"outdec\" works for 1-lit and 2-lit primes only.\n" );
+                goto usage;
+            }
+            break;
+        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_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "Only works for strashed networks.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDarOutdec( pNtk, nLits, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        Abc_Print( -1, "Command has failed.\n" );
+        return 0;
+    }
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: outdec [-Lvh]\n" );
+    Abc_Print( -2, "\t         performs prime decomposition of the first output\n" );
+    Abc_Print( -2, "\t-L num : the number of literals in the primes [default = %d]\n", nLits );
+    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_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
@@ -8577,6 +8655,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 }
 */
+
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 34306fd8..c113d856 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3843,6 +3843,36 @@ void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, in
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarOutdec( Abc_Ntk_t * pNtk, int nLits, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Saig_ManDecPropertyOutput( pTemp = pMan, nLits, fVerbose );
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;