From 9521d1345b364eeb99498dfc0df329375d0ea669 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 28 Oct 2015 13:44:29 -0700
Subject: Improvements to 'satclp'.

---
 src/aig/gia/gia.h     |  1 +
 src/aig/gia/giaUtil.c | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+)

(limited to 'src/aig/gia')

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6b801b9e..4ad3e39a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1452,6 +1452,7 @@ extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t **
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
 extern int                 Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
+extern int                 Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp );
 extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index ae32b91e..ff44eecf 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1141,6 +1141,47 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
     return ConeSize1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of internal nodes in the MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_NodeCollect_rec( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pNode) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pNode);
+    if ( Gia_ObjRefNum(p, pNode) || Gia_ObjIsCi(pNode) )
+    {
+        Vec_IntPush( vSupp, Gia_ObjId(p, pNode) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pNode) );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
+}
+int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
+{
+    int ConeSize1, ConeSize2;
+    assert( !Gia_IsComplement(pNode) );
+    assert( Gia_ObjIsAnd(pNode) );
+    Vec_IntClear( vSupp );
+    Gia_ManIncrementTravId( p );
+    ConeSize1 = Gia_NodeDeref_rec( p, pNode );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
+    Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
+    ConeSize2 = Gia_NodeRef_rec( p, pNode );
+    assert( ConeSize1 == ConeSize2 );
+    assert( ConeSize1 >= 0 );
+    return ConeSize1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if AIG has dangling nodes.]
-- 
cgit v1.2.3