summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/bool/kit/kit.h2
-rw-r--r--src/bool/kit/kitGraph.c28
-rw-r--r--src/bool/kit/kitHop.c24
-rw-r--r--src/bool/kit/kitIsop.c70
4 files changed, 124 insertions, 0 deletions
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index 15b27fad..6889aa32 100644
--- a/src/bool/kit/kit.h
+++ b/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 ==========================================================*/
diff --git a/src/bool/kit/kitGraph.c b/src/bool/kit/kitGraph.c
index 08dabc7e..2ee135e2 100644
--- a/src/bool/kit/kitGraph.c
+++ b/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 []
diff --git a/src/bool/kit/kitHop.c b/src/bool/kit/kitHop.c
index a159a05a..4ac82ac9 100644
--- a/src/bool/kit/kitHop.c
+++ b/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*************************************************************
diff --git a/src/bool/kit/kitIsop.c b/src/bool/kit/kitIsop.c
index 506da2e5..828ef1de 100644
--- a/src/bool/kit/kitIsop.c
+++ b/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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 22:24:16 +0000