Extending TT-based ISOP to handle ISFs.

src/bool/kit/kit.h

@@ -566,6 +566,7 @@ extern Kit_Edge_t      Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEd
 extern Kit_Edge_t      Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type );
 extern unsigned        Kit_GraphToTruth( Kit_Graph_t * pGraph );
 extern Kit_Graph_t *   Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
+extern Kit_Graph_t *   Kit_TruthToGraph2( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory );
 extern int             Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
 /*=== kitHop.c ==========================================================*/
 //extern int             Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
@@ -574,6 +575,7 @@ extern int             Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t
 //extern Hop_Obj_t *     Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
 /*=== kitIsop.c ==========================================================*/
 extern int             Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
+extern int             Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth );
 extern void            Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
 extern void            Kit_TruthIsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl );
 /*=== kitPla.c ==========================================================*/

src/bool/kit/kitGraph.c

@@ -371,6 +371,34 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
 
 /**Function*************************************************************
 
+  Synopsis    [Derives the factored form from the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Kit_Graph_t * Kit_TruthToGraph2( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )
+{
+    Kit_Graph_t * pGraph;
+    int RetValue;
+    // derive SOP
+    RetValue = Kit_TruthIsop2( pTruth0, pTruth1, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
+    if ( RetValue == -1 )
+        return NULL;
+    if ( Vec_IntSize(vMemory) > (1<<16) )
+        return NULL;
+//    printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
+    assert( RetValue == 0 || RetValue == 1 );
+    // derive factored form
+    pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
+    return pGraph;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives the maximum depth from the leaf to the root.]
 
   Description []

src/bool/kit/kitHop.c

@@ -100,6 +100,30 @@ int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t *
     Kit_GraphFree( pGraph );
     return iLit;
 }
+int Kit_TruthToGia2( Gia_Man_t * pMan, unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash )
+{
+    int iLit;
+    Kit_Graph_t * pGraph;
+    // transform truth table into the decomposition tree
+    if ( vMemory == NULL )
+    {
+        vMemory = Vec_IntAlloc( 0 );
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+        Vec_IntFree( vMemory );
+    }
+    else
+        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
+    if ( pGraph == NULL )
+    {
+        printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
+        Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
+        Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
+    }
+    // derive the AIG for the decomposition tree
+    iLit = Kit_GraphToGia( pMan, pGraph, vLeaves, fHash );
+    Kit_GraphFree( pGraph );
+    return iLit;
+}
 
 /**Function*************************************************************
 

src/bool/kit/kitIsop.c

@@ -52,6 +52,76 @@ static unsigned   Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, K
   SeeAlso     []
 
 ***********************************************************************/
+int Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth )
+{
+    Kit_Sop_t cRes, * pcRes = &cRes;
+    Kit_Sop_t cRes2, * pcRes2 = &cRes2;
+    unsigned * pResult;
+    int RetValue = 0;
+    assert( nVars >= 0 && nVars <= 16 );
+    // prepare memory manager
+    Vec_IntClear( vMemory );
+    Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
+    // compute ISOP for the direct polarity
+    Kit_TruthNot( puTruth0, puTruth0, nVars );
+    pResult = Kit_TruthIsop_rec( puTruth1, puTruth0, nVars, pcRes, vMemory );
+    Kit_TruthNot( puTruth0, puTruth0, nVars );
+    if ( pcRes->nCubes == -1 )
+    {
+        vMemory->nSize = -1;
+        return -1;
+    }
+    assert( Kit_TruthIsImply( puTruth1, pResult, nVars ) );
+    Kit_TruthNot( puTruth0, puTruth0, nVars );
+    assert( Kit_TruthIsImply( pResult, puTruth0, nVars ) );
+    Kit_TruthNot( puTruth0, puTruth0, nVars );
+    if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
+    {
+        vMemory->pArray[0] = 0;
+        Vec_IntShrink( vMemory, pcRes->nCubes );
+        return 0;
+    }
+    if ( fTryBoth )
+    {
+        // compute ISOP for the complemented polarity
+        Kit_TruthNot( puTruth1, puTruth1, nVars );
+        pResult = Kit_TruthIsop_rec( puTruth0, puTruth1, nVars, pcRes2, vMemory );
+        Kit_TruthNot( puTruth1, puTruth1, nVars );
+        if ( pcRes2->nCubes >= 0 )
+        {
+            assert( Kit_TruthIsImply( puTruth0, pResult, nVars ) );
+            Kit_TruthNot( puTruth1, puTruth1, nVars );
+            assert( Kit_TruthIsImply( pResult, puTruth1, nVars ) );
+            Kit_TruthNot( puTruth1, puTruth1, nVars );
+            if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) )
+            {
+                RetValue = 1;
+                pcRes = pcRes2;
+            }
+        }
+    }
+//    printf( "%d ", vMemory->nSize );
+    // move the cover representation to the beginning of the memory buffer
+    memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
+    Vec_IntShrink( vMemory, pcRes->nCubes );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes ISOP from TT.]
+
+  Description [Returns the cover in vMemory. Uses the rest of array in vMemory
+  as an intermediate memory storage. Returns the cover with -1 cubes, if the
+  the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of
+  intermediate data).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth )
 {
     Kit_Sop_t cRes, * pcRes = &cRes;