Updates to arithmetic verification.

2 files changed, 35 insertions, 0 deletions

diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index f09b8783..d952518f 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1692,6 +1692,24 @@ static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Ve
     }
     return Vec_IntSize(vArr);
 }
+static inline int Vec_IntTwoFindCommonReverse( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
+{
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    Vec_IntClear( vArr );
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++;
+        else if ( *pBeg1 > *pBeg2 )
+            pBeg1++;
+        else 
+            pBeg2++;
+    }
+    return Vec_IntSize(vArr);
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index e4e92503..8180e984 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -303,6 +303,23 @@ static inline Vec_Int_t * Vec_WecPushLevel( Vec_Wec_t * p )
     ++p->nSize;
     return Vec_WecEntryLast( p );
 }
+static inline Vec_Int_t * Vec_WecInsertLevel( Vec_Wec_t * p, int i )
+{
+    Vec_Int_t * pTemp;
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_WecGrow( p, 16 );
+        else
+            Vec_WecGrow( p, 2 * p->nCap );
+    }
+    ++p->nSize;
+    assert( i >= 0 && i < p->nSize );
+    for ( pTemp = p->pArray + p->nSize - 2; pTemp >= p->pArray + i; pTemp-- )
+        pTemp[1] = pTemp[0];
+    Vec_IntZero( p->pArray + i );
+    return p->pArray + i;
+}
 
 /**Function*************************************************************