summaryrefslogtreecommitdiffstats
path: root/src/aig/aig/aigFact.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/aig/aigFact.c')
-rw-r--r--src/aig/aig/aigFact.c272
1 files changed, 272 insertions, 0 deletions
diff --git a/src/aig/aig/aigFact.c b/src/aig/aig/aigFact.c
new file mode 100644
index 00000000..7004618a
--- /dev/null
+++ b/src/aig/aig/aigFact.c
@@ -0,0 +1,272 @@
+/**CFile****************************************************************
+
+ FileName [aigFactor.c]
+
+ SystemName []
+
+ PackageName []
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation []
+
+ Date [Ver. 1.0. Started - April 17, 2009.]
+
+ Revision [$Id: aigFactor.c,v 1.00 2009/04/17 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Detects multi-input AND gate rooted at this node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManFindImplications_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vImplics )
+{
+ if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) )
+ {
+ Vec_PtrPushUnique( vImplics, pObj );
+ return;
+ }
+ Aig_ManFindImplications_rec( Aig_ObjChild0(pObj), vImplics );
+ Aig_ManFindImplications_rec( Aig_ObjChild1(pObj), vImplics );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the nodes whose values are implied by pNode.]
+
+ Description [Attention! Both pNode and results can be complemented!
+ Also important: Currently, this procedure only does backward propagation.
+ In general, it may find more implications if forward propagation is enabled.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManFindImplications( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+ Vec_Ptr_t * vImplics;
+ vImplics = Vec_PtrAlloc( 100 );
+ Aig_ManFindImplications_rec( pNode, vImplics );
+ return vImplics;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManFindConeOverlap_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+ if ( Aig_ObjIsTravIdPrevious( p, pNode ) )
+ return 1;
+ if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
+ return 0;
+ Aig_ObjSetTravIdCurrent( p, pNode );
+ if ( Aig_ObjIsPi(pNode) )
+ return 0;
+ if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin0(pNode) ) )
+ return 1;
+ if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin1(pNode) ) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManFindConeOverlap( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode )
+{
+ Aig_Obj_t * pTemp;
+ int i;
+ assert( !Aig_IsComplement(pNode) );
+ assert( !Aig_ObjIsConst1(pNode) );
+ Aig_ManIncrementTravId( p );
+ Vec_PtrForEachEntry( vImplics, pTemp, i )
+ Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
+ Aig_ManIncrementTravId( p );
+ return Aig_ManFindConeOverlap_rec( p, pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDeriveNewCone_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+ if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
+ return pNode->pData;
+ Aig_ObjSetTravIdCurrent( p, pNode );
+ if ( Aig_ObjIsPi(pNode) )
+ return pNode->pData = pNode;
+ Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin0(pNode) );
+ Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin1(pNode) );
+ return pNode->pData = Aig_And( p, Aig_ObjChild0Copy(pNode), Aig_ObjChild1Copy(pNode) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the cone of the node overlaps with the vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDeriveNewCone( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode )
+{
+ Aig_Obj_t * pTemp;
+ int i;
+ assert( !Aig_IsComplement(pNode) );
+ assert( !Aig_ObjIsConst1(pNode) );
+ Aig_ManIncrementTravId( p );
+ Vec_PtrForEachEntry( vImplics, pTemp, i )
+ {
+ Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
+ Aig_Regular(pTemp)->pData = Aig_NotCond( Aig_ManConst1(p), Aig_IsComplement(pTemp) );
+ }
+ return Aig_ManDeriveNewCone_rec( p, pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns algebraic factoring of B in terms of A.]
+
+ Description [Returns internal node C (an AND gate) that is equal to B
+ under assignment A = 'Value', or NULL if there is no such node C. ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManFactorAlgebraic_int( Aig_Man_t * p, Aig_Obj_t * pPoA, Aig_Obj_t * pPoB, int Value )
+{
+ Aig_Obj_t * pNodeA, * pNodeC;
+ Vec_Ptr_t * vImplics;
+ int RetValue;
+ if ( Aig_ObjIsConst1(Aig_ObjFanin0(pPoA)) || Aig_ObjIsConst1(Aig_ObjFanin0(pPoB)) )
+ return NULL;
+ if ( Aig_ObjIsPi(Aig_ObjFanin0(pPoB)) )
+ return NULL;
+ // get the internal node representing function of A under assignment A = 'Value'
+ pNodeA = Aig_ObjChild0( pPoA );
+ pNodeA = Aig_NotCond( pNodeA, Value==0 );
+ // find implications of this signal (nodes whose value is fixed under assignment A = 'Value')
+ vImplics = Aig_ManFindImplications( p, pNodeA );
+ // check if the TFI cone of B overlaps with the implied nodes
+ RetValue = Aig_ManFindConeOverlap( p, vImplics, Aig_ObjFanin0(pPoB) );
+ if ( RetValue == 0 ) // no overlap
+ {
+ Vec_PtrFree( vImplics );
+ return NULL;
+ }
+ // there is overlap - derive node representing value of B under assignment A = 'Value'
+ pNodeC = Aig_ManDeriveNewCone( p, vImplics, Aig_ObjFanin0(pPoB) );
+ pNodeC = Aig_NotCond( pNodeC, Aig_ObjFaninC0(pPoB) );
+ Vec_PtrFree( vImplics );
+ return pNodeC;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns algebraic factoring of B in terms of A.]
+
+ Description [Returns internal node C (an AND gate) that is equal to B
+ under assignment A = 'Value', or NULL if there is no such node C. ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManFactorAlgebraic( Aig_Man_t * p, int iPoA, int iPoB, int Value )
+{
+ assert( iPoA >= 0 && iPoA < Aig_ManPoNum(p) );
+ assert( iPoB >= 0 && iPoB < Aig_ManPoNum(p) );
+ assert( Value == 0 || Value == 1 );
+ return Aig_ManFactorAlgebraic_int( p, Aig_ManPo(p, iPoA), Aig_ManPo(p, iPoB), Value );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Testing procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManFactorAlgebraicTest( Aig_Man_t * p )
+{
+ int iPoA = 0;
+ int iPoB = 1;
+ int Value = 0;
+ Aig_Obj_t * pRes;
+// Aig_Obj_t * pObj;
+// int i;
+ pRes = Aig_ManFactorAlgebraic( p, iPoA, iPoB, Value );
+ Aig_ManShow( p, 0, NULL );
+ Aig_ObjPrint( p, pRes );
+ printf( "\n" );
+/*
+ printf( "Results:\n" );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ printf( "Object = %d.\n", i );
+ Aig_ObjPrint( p, pObj );
+ printf( "\n" );
+ Aig_ObjPrint( p, pObj->pData );
+ printf( "\n" );
+ }
+*/
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 21:32:11 +0000