Modified structural constraint extraction (unfold -s) to work for multi-output testcases.

1 files changed, 241 insertions, 162 deletions

diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c
index 6c258505..682c46cf 100644
--- a/src/aig/saig/saigConstr.c
+++ b/src/aig/saig/saigConstr.c
@@ -26,169 +26,53 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
+/*
+    Property holds iff it is const 0.
+    Constraint holds iff it is const 0.
+
+    The following structure is used for folding constraints:
+    - the output of OR gate is 0 as long as all constraints hold
+    - as soon as one constraint fail, the property output becomes 0 forever
+      because the flop becomes 1 and it stays 1 forever
+
+
+       property output
+
+             |
+          |-----|
+          | and |
+          |-----|
+           |   |
+           |  / \
+           | /inv\
+           | -----
+       ____|   |_________________________
+       |             |                  |
+      / \       -----------             |   
+     /   \      |   or    |             |
+    /     \     -----------             |
+   / logic \     |   |   |              |
+  /  cone   \    |   |   |              |
+ /___________\   |   |   |              |
+                 |   | ------           |   
+                 |   | |flop| (init=0)  |
+                 |   | ------           |
+                 |   |   |              |
+                 |   |   |______________| 
+                 |   |
+                 c1  c2 
+*/
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG while unfolding constraints.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
-{
-    Vec_Ptr_t * vOuts, * vCons;
-    Aig_Man_t * pAigNew;
-    Aig_Obj_t * pMiter, * pObj;
-    int i, RetValue;
-    RetValue = Saig_ManDetectConstr( pAig, &vOuts, &vCons );
-    if ( RetValue == 0 )
-    {
-        Vec_PtrFreeP( &vOuts );
-        Vec_PtrFreeP( &vCons );
-        return Aig_ManDupDfs( pAig );
-    }
-    // start the new manager
-    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
-    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
-    // create variables for PIs
-    Aig_ManForEachCi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreateCi( pAigNew );
-    // add internal nodes of this frame
-    Aig_ManForEachNode( pAig, pObj, i )
-        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    // AND the outputs
-    pMiter = Aig_ManConst1( pAigNew );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, i )
-        pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) );
-    Aig_ObjCreateCo( pAigNew, pMiter );
-    // add constraints
-    pAigNew->nConstrs = Vec_PtrSize(vCons);
-    Vec_PtrForEachEntry( Aig_Obj_t *, vCons, pObj, i )
-        Aig_ObjCreateCo( pAigNew, Aig_ObjRealCopy(pObj) );
-    // transfer to register outputs
-    Saig_ManForEachLi( pAig, pObj, i )
-        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
-    Vec_PtrFreeP( &vOuts );
-    Vec_PtrFreeP( &vCons );
-
-    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
-    Aig_ManCleanup( pAigNew );
-    Aig_ManSeqCleanup( pAigNew );
-    return pAigNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the AIG while folding in the constraints.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * vConstrs )
-{
-    Aig_Man_t * pAigNew;
-    Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
-    int Entry, i;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    // start the new manager
-    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
-    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
-    // create variables for PIs
-    Aig_ManForEachCi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreateCi( pAigNew );
-    // add internal nodes of this frame
-    Aig_ManForEachNode( pAig, pObj, i )
-        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-
-    // OR the constraint outputs
-    pMiter = Aig_ManConst0( pAigNew );
-    Vec_IntForEachEntry( vConstrs, Entry, i )
-    {
-        assert( Entry > 0 && Entry < Saig_ManPoNum(pAig) );
-        pObj = Aig_ManCo( pAig, Entry );
-        pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
-    }
-    // create additional flop
-    pFlopOut = Aig_ObjCreateCi( pAigNew );
-    pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
-
-    // create primary output
-    Saig_ManForEachPo( pAig, pObj, i )
-    {
-        pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
-        Aig_ObjCreateCo( pAigNew, pMiter );
-    }
-
-    // transfer to register outputs
-    Saig_ManForEachLi( pAig, pObj, i )
-        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
-    // create additional flop 
-    Aig_ObjCreateCo( pAigNew, pFlopIn );
-
-    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
-    Aig_ManCleanup( pAigNew );
-    Aig_ManSeqCleanup( pAigNew );
-    return pAigNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Tests the above two procedures.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManFoldConstrTest( Aig_Man_t * pAig )
-{
-    Aig_Man_t * pAig1, * pAig2;
-    Vec_Int_t * vConstrs;
-    // unfold constraints
-    pAig1 = Saig_ManDupUnfoldConstrs( pAig );
-    // create the constraint list
-    vConstrs = Vec_IntStartNatural( Saig_ManPoNum(pAig1) );
-    Vec_IntRemove( vConstrs, 0 );
-    // fold constraints back
-    pAig2 = Saig_ManDupFoldConstrs( pAig1, vConstrs );
-    Vec_IntFree( vConstrs );
-    // compare the two AIGs
-    Ioa_WriteAiger( pAig2, "test.aig", 0, 0 );
-    Aig_ManStop( pAig1 );
-    Aig_ManStop( pAig2 );
-}
-
-
-
-
-/**Function*************************************************************
-
   Synopsis    [Collects the supergate.]
 
   Description []
@@ -271,19 +155,15 @@ Vec_Ptr_t * Saig_ManDetectConstrCheckCont( Vec_Ptr_t * vSuper, Vec_Ptr_t * vSupe
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons )
+int Saig_ManDetectConstr( Aig_Man_t * p, int iOut, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons )
 {
     Vec_Ptr_t * vSuper, * vSuper2 = NULL, * vUnique;
     Aig_Obj_t * pObj, * pObj2, * pFlop;
     int i, nFlops, RetValue;
+    assert( iOut >= 0 && iOut < Saig_ManPoNum(p) );
     *pvOuts = NULL;
     *pvCons = NULL;
-    if ( Saig_ManPoNum(p) != 1 )
-    {
-        printf( "The number of POs is other than 1.\n" );
-        return 0;
-    }
-    pObj = Aig_ObjChild0( Aig_ManCo(p, 0) );
+    pObj = Aig_ObjChild0( Aig_ManCo(p, iOut) );
     if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) )
     {
         printf( "The output is not an AND.\n" );
@@ -346,8 +226,8 @@ int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCon
     }
     // vUnique contains unique entries
     // vSuper2 contains the supergate
-    printf( "Structural analysis found %d original properties and %d constraints.\n", 
-        Vec_PtrSize(vUnique), Vec_PtrSize(vSuper2) );
+    printf( "Output %d : Structural analysis found %d original properties and %d constraints.\n", 
+        iOut, Vec_PtrSize(vUnique), Vec_PtrSize(vSuper2) );
     // remember the number of constraints
     RetValue = Vec_PtrSize(vSuper2);
     // make the AND of properties 
@@ -361,6 +241,205 @@ int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCon
 
 /**Function*************************************************************
 
+  Synopsis    [Procedure used for sorting nodes by ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManDupCompare( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
+{
+    int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while unfolding constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
+{
+    Vec_Ptr_t * vOutsAll, * vConsAll;
+    Vec_Ptr_t * vOuts, * vCons, * vCons0;
+    Aig_Man_t * pAigNew;
+    Aig_Obj_t * pMiter, * pObj;
+    int i, k, RetValue;
+    // detect constraints for each output
+    vOutsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+    vConsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        RetValue = Saig_ManDetectConstr( pAig, i, &vOuts, &vCons );
+        if ( RetValue == 0 )
+        {
+            Vec_PtrFreeP( &vOuts );
+            Vec_PtrFreeP( &vCons );
+            Vec_VecFree( (Vec_Vec_t *)vOutsAll );
+            Vec_VecFree( (Vec_Vec_t *)vConsAll );
+            return Aig_ManDupDfs( pAig );
+        }
+        Vec_PtrSort( vOuts, Saig_ManDupCompare );
+        Vec_PtrSort( vCons, Saig_ManDupCompare );
+        Vec_PtrPush( vOutsAll, vOuts );
+        Vec_PtrPush( vConsAll, vCons );
+    }
+    // check if constraints are compatible
+    vCons0 = (Vec_Ptr_t *)Vec_PtrEntry( vConsAll, 0 );
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
+        if ( !Vec_PtrEqual(vCons0, vCons) )
+            break;
+    if ( i < Vec_PtrSize(vConsAll) )
+    {
+        printf( "Collected constraints are not compatible.\n" );
+        Vec_VecFree( (Vec_Vec_t *)vOutsAll );
+        Vec_VecFree( (Vec_Vec_t *)vConsAll );
+        return Aig_ManDupDfs( pAig );
+    }
+
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // create variables for PIs
+    Aig_ManForEachCi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( pAigNew );
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // transform each output
+    Vec_PtrForEachEntry( Vec_Ptr_t *, vOutsAll, vOuts, i )
+    {
+        // AND the outputs
+        pMiter = Aig_ManConst1( pAigNew );
+        Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, k )
+            pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) );
+        Aig_ObjCreateCo( pAigNew, pMiter );
+    }
+    // add constraints
+    pAigNew->nConstrs = Vec_PtrSize(vCons0);
+    Vec_PtrForEachEntry( Aig_Obj_t *, vCons0, pObj, i )
+        Aig_ObjCreateCo( pAigNew, Aig_ObjRealCopy(pObj) );
+    // transfer to register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
+//    Vec_PtrFreeP( &vOuts );
+//    Vec_PtrFreeP( &vCons );
+    Vec_VecFree( (Vec_Vec_t *)vOutsAll );
+    Vec_VecFree( (Vec_Vec_t *)vConsAll );
+
+    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSeqCleanup( pAigNew );
+    return pAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while folding in the constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * vConstrs )
+{
+    Aig_Man_t * pAigNew;
+    Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
+    int Entry, i;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // create variables for PIs
+    Aig_ManForEachCi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( pAigNew );
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+
+    // OR the constraint outputs
+    pMiter = Aig_ManConst0( pAigNew );
+    Vec_IntForEachEntry( vConstrs, Entry, i )
+    {
+        assert( Entry > 0 && Entry < Saig_ManPoNum(pAig) );
+        pObj = Aig_ManCo( pAig, Entry );
+        pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
+    }
+    // create additional flop
+    pFlopOut = Aig_ObjCreateCi( pAigNew );
+    pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
+
+    // create primary output
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
+        Aig_ObjCreateCo( pAigNew, pMiter );
+    }
+
+    // transfer to register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    // create additional flop 
+    Aig_ObjCreateCo( pAigNew, pFlopIn );
+
+    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSeqCleanup( pAigNew );
+    return pAigNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Tests the above two procedures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManFoldConstrTest( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pAig1, * pAig2;
+    Vec_Int_t * vConstrs;
+    // unfold constraints
+    pAig1 = Saig_ManDupUnfoldConstrs( pAig );
+    // create the constraint list
+    vConstrs = Vec_IntStartNatural( Saig_ManPoNum(pAig1) );
+    Vec_IntRemove( vConstrs, 0 );
+    // fold constraints back
+    pAig2 = Saig_ManDupFoldConstrs( pAig1, vConstrs );
+    Vec_IntFree( vConstrs );
+    // compare the two AIGs
+    Ioa_WriteAiger( pAig2, "test.aig", 0, 0 );
+    Aig_ManStop( pAig1 );
+    Aig_ManStop( pAig2 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Experiment with the above procedure.]
 
   Description []
@@ -373,7 +452,7 @@ int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCon
 int Saig_ManDetectConstrTest( Aig_Man_t * p )
 {
     Vec_Ptr_t * vOuts, * vCons;
-    int RetValue = Saig_ManDetectConstr( p, &vOuts, &vCons );
+    int RetValue = Saig_ManDetectConstr( p, 0, &vOuts, &vCons );
     Vec_PtrFreeP( &vOuts );
     Vec_PtrFreeP( &vCons );
     return RetValue;