summaryrefslogtreecommitdiffstats
path: root/src/misc/vec/vecSet.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-13 16:31:12 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-13 16:31:12 -0700
commit3fb103dadced1d5cd392c5447d87c3599f8754c6 (patch)
tree88f5fd8409da789d2a1812fa98cb7c9e4d9591e4 /src/misc/vec/vecSet.h
parentda525b2a23802ed168f8528811f704b7c19708d0 (diff)
downloadabc-3fb103dadced1d5cd392c5447d87c3599f8754c6.tar.gz
abc-3fb103dadced1d5cd392c5447d87c3599f8754c6.tar.bz2
abc-3fb103dadced1d5cd392c5447d87c3599f8754c6.zip
Debugging a proof error.
Diffstat (limited to 'src/misc/vec/vecSet.h')
-rw-r--r--src/misc/vec/vecSet.h19
1 files changed, 19 insertions, 0 deletions
diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h
index 5f8df449..7e5c6c62 100644
--- a/src/misc/vec/vecSet.h
+++ b/src/misc/vec/vecSet.h
@@ -156,6 +156,25 @@ static inline void Vec_SetRestart( Vec_Set_t * p )
/**Function*************************************************************
+ Synopsis [Returns memory in bytes occupied by the vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline double Vec_ReportMemory( Vec_Set_t * p )
+{
+ double Mem = sizeof(Vec_Set_t);
+ Mem += p->nPagesAlloc * sizeof(void *);
+ Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage);
+ return Mem;
+}
+
+/**Function*************************************************************
+
Synopsis [Freeing vector.]
Description []