Added support for constraints in AIGER (bug fix).

3 files changed, 72 insertions, 34 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index cd14deb4..2a8e6664 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -650,6 +650,7 @@ extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose );
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
+extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
 extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index a78ddf81..f4979470 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -569,7 +569,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
 Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck )
 {
     Gia_Man_t * pNew, * pTemp;
-    Vec_Int_t * vLits = NULL;
+    Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
     Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
     int iObj, iNode0, iNode1;
     int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
@@ -625,6 +625,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
     }
 
     // create the AND gates
+    Gia_ManHashAlloc( pNew );
     for ( i = 0; i < nAnds; i++ )
     {
         uLit = ((i + 1 + nInputs + nLatches) << 1);
@@ -635,8 +636,9 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
         assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
 //        Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
-        Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
+        Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
     }
+    Gia_ManHashStop( pNew );
 
     // remember the place where symbols begin
     pSymbols = pCur;
@@ -680,6 +682,17 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         Vec_IntFree( vLits );
     }
 
+    // create the POs
+    for ( i = 0; i < nOutputs; i++ )
+        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
+    for ( i = 0; i < nLatches; i++ )
+        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
+    Vec_IntFree( vDrivers );
+
+    // create the latches
+    Gia_ManSetRegNum( pNew, nLatches );
+
+
     // check if there are other types of information to read
     pCur = pSymbols;
     if ( (char *)pCur + 1 < pContents + nFileSize && *pCur == 'c' )
@@ -838,54 +851,33 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
             if ( !fBreakUsed )
             {
                 nInvars = nConstr = 0;
+                vPoTypes = Vec_IntStart( Gia_ManPoNum(pNew) );
                 Vec_IntForEachEntry( vPoNames, Entry, i )
                 {
                     if ( Entry == ~0 )
                         continue;
                     if ( strncmp( pContents+Entry, "constraint:", 11 ) == 0 )
+                    {
+                        Vec_IntWriteEntry( vPoTypes, i, 1 );
                         nConstr++;
+                    }
                     if ( strncmp( pContents+Entry, "invariant:", 10 ) == 0 )
+                    {
+                        Vec_IntWriteEntry( vPoTypes, i, 2 );
                         nInvars++;
+                    }
                 }
-
-                // move constraints forward in the PO list
-                if ( nConstr || nInvars )
-                {
-                    int k = nLatches;
-                    Vec_Int_t * vDriversCopy = Vec_IntDup( vDrivers );
-                    Vec_IntForEachEntry( vPoNames, Entry, i )
-                        if ( Entry == ~0 || (strncmp( pContents+Entry, "constraint:", 11 ) != 0 && strncmp( pContents+Entry, "invariant:", 10 ) != 0) )
-                            Vec_IntWriteEntry( vDrivers, k++, Vec_IntEntry(vDriversCopy, nLatches + i) );
-                    Vec_IntForEachEntry( vPoNames, Entry, i )
-                        if ( Entry != ~0 && strncmp( pContents+Entry, "constraint:", 11 ) == 0 )
-                            Vec_IntWriteEntry( vDrivers, k++, Vec_IntEntry(vDriversCopy, nLatches + i) ^ 1 ); // flip polarity!!!
-                    // update the PO count
-                    nOutputs -= nInvars;
-                    assert( k == nLatches + nOutputs );
-                    Vec_IntFree( vDriversCopy );
-                    // mark constraints
-                    pNew->nConstrs = nConstr;
-                }
-
                 if ( nConstr )
                     fprintf( stdout, "Recognized and added %d constraints.\n", nConstr );
                 if ( nInvars )
                     fprintf( stdout, "Recognized and skipped %d invariants.\n", nInvars );
+                if ( nConstr == 0 && nInvars == 0 )
+                    Vec_IntFreeP( &vPoTypes );
             }
             Vec_IntFree( vPoNames );
         }
     }
 
-    // create the POs
-    for ( i = 0; i < nOutputs; i++ )
-        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
-    for ( i = 0; i < nLatches; i++ )
-        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
-    Vec_IntFree( vDrivers );
-
-    // create the latches
-    Gia_ManSetRegNum( pNew, nLatches );
-
     // skipping the comments
     Vec_IntFree( vNodes );
 /*
@@ -897,6 +889,13 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         return NULL;
     }
 */
+    // clean the PO drivers
+    if ( vPoTypes )
+    {
+        pNew = Gia_ManDupWithConstraints( pTemp = pNew, vPoTypes );
+        Gia_ManStop( pTemp );
+        Vec_IntFreeP( &vPoTypes );
+    }
 
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 62586103..d3a4ccc8 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -948,13 +948,13 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
     Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     // dup second AIG
     Gia_ManConst0(p2)->Value = 0;
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManPi(p2, i)->Value = Gia_ObjFanin0Copy(pObj);
     Gia_ManForEachAnd( p2, pObj, i )
-        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     Gia_ManForEachCo( p2, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManHashStop( pNew );
@@ -1466,6 +1466,44 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting first PIs, then nodes, then POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i, nConstr = 0;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        if ( Vec_IntEntry(vPoTypes, i) == 0 ) // regular PO
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        if ( Vec_IntEntry(vPoTypes, i) == 1 ) // constraint (should be complemented!)
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ^ 1 ), nConstr++;
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+//    Gia_ManDupRemapEquiv( pNew, p );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew->nConstrs = nConstr;
+    assert( Gia_ManIsNormalized(pNew) );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////