summaryrefslogtreecommitdiffstats
path: root/src/aig/kit/kitFactor.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/kit/kitFactor.c')
-rw-r--r--src/aig/kit/kitFactor.c339
1 files changed, 339 insertions, 0 deletions
diff --git a/src/aig/kit/kitFactor.c b/src/aig/kit/kitFactor.c
new file mode 100644
index 00000000..e3288342
--- /dev/null
+++ b/src/aig/kit/kitFactor.c
@@ -0,0 +1,339 @@
+/**CFile****************************************************************
+
+ FileName [kitFactor.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Computation kit.]
+
+ Synopsis [Algebraic factoring.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Dec 6, 2006.]
+
+ Revision [$Id: kitFactor.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// factoring fails if intermediate memory usage exceed this limit
+#define KIT_FACTOR_MEM_LIMIT (1<<16)
+
+static Kit_Edge_t Kit_SopFactor_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory );
+static Kit_Edge_t Kit_SopFactorLF_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, Kit_Sop_t * cSimple, int nLits, Vec_Int_t * vMemory );
+static Kit_Edge_t Kit_SopFactorTrivial( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits );
+static Kit_Edge_t Kit_SopFactorTrivialCube( Kit_Graph_t * pFForm, unsigned uCube, int nLits );
+
+extern int Kit_SopFactorVerify( Vec_Int_t * cSop, Kit_Graph_t * pFForm, int nVars );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Factors the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory )
+{
+ Kit_Sop_t Sop, * cSop = &Sop;
+ Kit_Graph_t * pFForm;
+ Kit_Edge_t eRoot;
+// int nCubes;
+
+ // works for up to 15 variables because divisin procedure
+ // used the last bit for marking the cubes going to the remainder
+ assert( nVars < 16 );
+
+ // check for trivial functions
+ if ( Vec_IntSize(vCover) == 0 )
+ return Kit_GraphCreateConst0();
+ if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 )
+ return Kit_GraphCreateConst1();
+
+ // prepare memory manager
+// Vec_IntClear( vMemory );
+ Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );
+
+ // perform CST
+ Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST
+
+ // start the factored form
+ pFForm = Kit_GraphCreate( nVars );
+ // factor the cover
+ eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
+ // finalize the factored form
+ Kit_GraphSetRoot( pFForm, eRoot );
+ if ( fCompl )
+ Kit_GraphComplement( pFForm );
+
+ // verify the factored form
+// nCubes = Vec_IntSize(vCover);
+// Vec_IntShrink( vCover, nCubes );
+// if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
+// printf( "Verification has failed.\n" );
+ return pFForm;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursive factoring procedure.]
+
+ Description [For the pseudo-code, see Hachtel/Somenzi,
+ Logic synthesis and verification algorithms, Kluwer, 1996, p. 432.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_Edge_t Kit_SopFactor_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory )
+{
+ Kit_Sop_t Div, Quo, Rem, Com;
+ Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem, * cCom = &Com;
+ Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
+
+ // make sure the cover contains some cubes
+ assert( Kit_SopCubeNum(cSop) > 0 );
+
+ // get the divisor
+ if ( !Kit_SopDivisor(cDiv, cSop, nLits, vMemory) )
+ return Kit_SopFactorTrivial( pFForm, cSop, nLits );
+
+ // divide the cover by the divisor
+ Kit_SopDivideInternal( cSop, cDiv, cQuo, cRem, vMemory );
+
+ // check the trivial case
+ assert( Kit_SopCubeNum(cQuo) > 0 );
+ if ( Kit_SopCubeNum(cQuo) == 1 )
+ return Kit_SopFactorLF_rec( pFForm, cSop, cQuo, nLits, vMemory );
+
+ // make the quotient cube free
+ Kit_SopMakeCubeFree( cQuo );
+
+ // divide the cover by the quotient
+ Kit_SopDivideInternal( cSop, cQuo, cDiv, cRem, vMemory );
+
+ // check the trivial case
+ if ( Kit_SopIsCubeFree( cDiv ) )
+ {
+ eNodeDiv = Kit_SopFactor_rec( pFForm, cDiv, nLits, vMemory );
+ eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
+ eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+ if ( Kit_SopCubeNum(cRem) == 0 )
+ return eNodeAnd;
+ eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
+ return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
+ }
+
+ // get the common cube
+ Kit_SopCommonCubeCover( cCom, cDiv, vMemory );
+
+ // solve the simple problem
+ return Kit_SopFactorLF_rec( pFForm, cSop, cCom, nLits, vMemory );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Internal recursive factoring procedure for the leaf case.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_Edge_t Kit_SopFactorLF_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, Kit_Sop_t * cSimple, int nLits, Vec_Int_t * vMemory )
+{
+ Kit_Sop_t Div, Quo, Rem;
+ Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem;
+ Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
+ assert( Kit_SopCubeNum(cSimple) == 1 );
+ // get the most often occurring literal
+ Kit_SopBestLiteralCover( cDiv, cSop, Kit_SopCube(cSimple, 0), nLits, vMemory );
+ // divide the cover by the literal
+ Kit_SopDivideByCube( cSop, cDiv, cQuo, cRem, vMemory );
+ // get the node pointer for the literal
+ eNodeDiv = Kit_SopFactorTrivialCube( pFForm, Kit_SopCube(cDiv, 0), nLits );
+ // factor the quotient and remainder
+ eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
+ eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+ if ( Kit_SopCubeNum(cRem) == 0 )
+ return eNodeAnd;
+ eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
+ return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Factoring cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_Edge_t Kit_SopFactorTrivialCube_rec( Kit_Graph_t * pFForm, unsigned uCube, int nStart, int nFinish )
+{
+ Kit_Edge_t eNode1, eNode2;
+ int i, iLit = -1, nLits, nLits1, nLits2;
+ assert( uCube );
+ // count the number of literals in this interval
+ nLits = 0;
+ for ( i = nStart; i < nFinish; i++ )
+ if ( Kit_CubeHasLit(uCube, i) )
+ {
+ iLit = i;
+ nLits++;
+ }
+ assert( iLit != -1 );
+ // quit if there is only one literal
+ if ( nLits == 1 )
+ return Kit_EdgeCreate( iLit/2, iLit%2 ); // CST
+ // split the literals into two parts
+ nLits1 = nLits/2;
+ nLits2 = nLits - nLits1;
+// nLits2 = nLits/2;
+// nLits1 = nLits - nLits2;
+ // find the splitting point
+ nLits = 0;
+ for ( i = nStart; i < nFinish; i++ )
+ if ( Kit_CubeHasLit(uCube, i) )
+ {
+ if ( nLits == nLits1 )
+ break;
+ nLits++;
+ }
+ // recursively construct the tree for the parts
+ eNode1 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, nStart, i );
+ eNode2 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, i, nFinish );
+ return Kit_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Factoring cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_Edge_t Kit_SopFactorTrivialCube( Kit_Graph_t * pFForm, unsigned uCube, int nLits )
+{
+ return Kit_SopFactorTrivialCube_rec( pFForm, uCube, 0, nLits );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Factoring SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_Edge_t Kit_SopFactorTrivial_rec( Kit_Graph_t * pFForm, unsigned * pCubes, int nCubes, int nLits )
+{
+ Kit_Edge_t eNode1, eNode2;
+ int nCubes1, nCubes2;
+ if ( nCubes == 1 )
+ return Kit_SopFactorTrivialCube_rec( pFForm, pCubes[0], 0, nLits );
+ // split the cubes into two parts
+ nCubes1 = nCubes/2;
+ nCubes2 = nCubes - nCubes1;
+// nCubes2 = nCubes/2;
+// nCubes1 = nCubes - nCubes2;
+ // recursively construct the tree for the parts
+ eNode1 = Kit_SopFactorTrivial_rec( pFForm, pCubes, nCubes1, nLits );
+ eNode2 = Kit_SopFactorTrivial_rec( pFForm, pCubes + nCubes1, nCubes2, nLits );
+ return Kit_GraphAddNodeOr( pFForm, eNode1, eNode2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Factoring the cover, which has no algebraic divisors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_Edge_t Kit_SopFactorTrivial( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits )
+{
+ return Kit_SopFactorTrivial_rec( pFForm, cSop->pCubes, cSop->nCubes, nLits );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Testing procedure for the factoring code.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_FactorTest( unsigned * pTruth, int nVars )
+{
+ Vec_Int_t * vCover, * vMemory;
+ Kit_Graph_t * pGraph;
+// unsigned uTruthRes;
+ int RetValue;
+
+ // derive SOP
+ vCover = Vec_IntAlloc( 0 );
+ RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 );
+ assert( RetValue == 0 );
+
+ // derive factored form
+ vMemory = Vec_IntAlloc( 0 );
+ pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
+/*
+ // derive truth table
+ assert( nVars <= 5 );
+ uTruthRes = Kit_GraphToTruth( pGraph );
+ if ( uTruthRes != pTruth[0] )
+ printf( "Verification failed!" );
+*/
+ printf( "Vars = %2d. Cubes = %3d. FFNodes = %3d. FF_memory = %3d.\n",
+ nVars, Vec_IntSize(vCover), Kit_GraphNodeNum(pGraph), Vec_IntSize(vMemory) );
+
+ Vec_IntFree( vMemory );
+ Vec_IntFree( vCover );
+ Kit_GraphFree( pGraph );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+