Updates to arithmetic verification.

3 files changed, 77 insertions, 3 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index dc6c679a..3bc97e6b 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1242,6 +1242,8 @@ extern Gia_Man_t *         Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
 extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
 extern Gia_Man_t *         Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
 extern Gia_Man_t *         Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis );
+extern Gia_Man_t *         Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
+extern Gia_Man_t *         Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
 extern Gia_Man_t *         Gia_ManDupOneHot( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupLevelized( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index cdb6a208..b0ba3472 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3046,6 +3046,71 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim
     return pNew;
 
 }
+void Gia_ManDupAndConesLimit_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+    if ( ~pObj->Value )
+        return;
+    if ( !Gia_ObjIsAnd(pObj) || Gia_ObjLevel(p, pObj) < Level )
+    {
+        pObj->Value = Gia_ManAppendCi( pNew );
+        //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+        return;
+    }
+    Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level );
+    Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+}
+Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
+{
+    Gia_Man_t * pNew;
+    int i;
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManLevelNum( p );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManDupAndConesLimit_rec( pNew, p, pAnds[i], Level );
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
+    return pNew;
+}
+
+void Gia_ManDupAndConesLimit2_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+    if ( ~pObj->Value )
+        return;
+    if ( !Gia_ObjIsAnd(pObj) || Level <= 0 )
+    {
+        pObj->Value = Gia_ManAppendCi( pNew );
+        //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+        return;
+    }
+    Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level-1 );
+    Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level-1 );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
+}
+Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
+{
+    Gia_Man_t * pNew;
+    int i;
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManDupAndConesLimit2_rec( pNew, p, pAnds[i], Level );
+    for ( i = 0; i < nAnds; i++ )
+        Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
+    return pNew;
+
+}
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index 4dd85aab..4deebd7a 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -1014,16 +1014,23 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_In
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds )
+Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds, Vec_Int_t * vBold )
 {
-    Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
+    Vec_Bit_t * vIsBold = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i, Entry;
+    if ( vBold )
+        Vec_IntForEachEntry( vBold, Entry, i )
+            Vec_BitWriteEntry( vIsBold, Entry, 1 );
     for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
     {
         if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 )
             continue;
+        if ( Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+4)) )
+            continue;
         Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i );
         Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i );
     }
+    Vec_BitFree( vIsBold );
     return vMapAdds;
 }
 Vec_Int_t * Gia_ShowMapXors( Gia_Man_t * p, Vec_Int_t * vXors )
@@ -1105,7 +1112,7 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v
 ***********************************************************************/
 void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
 {
-    Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds );
+    Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds, vBold );
     Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors );
     Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors );
     Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder );