Fixing memory being used too much

msoos · Jul 8, 2024 · ffcf4e0 · ffcf4e0
1 parent b735c94
commit ffcf4e0
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 5 deletions.
diff --git a/scripts/build_scripts b/scripts/build_scripts
diff --git a/src/clauseallocator.cpp b/src/clauseallocator.cpp
@@ -198,7 +198,7 @@ ClOffset ClauseAllocator::move_cl(
     ClOffset* newDataStart
     , ClOffset*& new_ptr
     , Clause* old
-) const {
+) {
     uint64_t bytesNeeded = sizeof(Clause) + old->size()*sizeof(Lit);
     uint64_t sizeNeeded = bytesNeeded/sizeof(BASE_DATA_TYPE) + (bool)(bytesNeeded % sizeof(BASE_DATA_TYPE));
     memcpy(new_ptr, old, sizeNeeded*sizeof(BASE_DATA_TYPE));
@@ -209,6 +209,7 @@ ClOffset ClauseAllocator::move_cl(
     (*old)[1] = Lit::toLit((new_offset>>32) & 0xFFFFFFFF);
     #endif
     old->reloced = true;
+    new_sz_while_moving += sizeNeeded;
 
     new_ptr += sizeNeeded;
     return new_offset;
@@ -265,6 +266,7 @@ void ClauseAllocator::consolidate(
         return;
     }
     const double my_time = cpuTime();
+    new_sz_while_moving = 0;
 
     //Pointers that will be moved along
     BASE_DATA_TYPE * const newDataStart = (BASE_DATA_TYPE*)malloc(currentlyUsedSize*sizeof(BASE_DATA_TYPE));
@@ -308,7 +310,7 @@ void ClauseAllocator::consolidate(
     const uint64_t old_size = size;
     size = new_ptr-newDataStart;
     capacity = currentlyUsedSize;
-    currentlyUsedSize = size;
+    currentlyUsedSize = new_sz_while_moving;
     free(dataStart);
     dataStart = newDataStart;
 

diff --git a/src/clauseallocator.h b/src/clauseallocator.h
@@ -100,8 +100,9 @@ class ClauseAllocator {
             ClOffset* newDataStart
             , ClOffset*& new_ptr
             , Clause* old
-        ) const;
+        );
 
+        uint32_t new_sz_while_moving;
         BASE_DATA_TYPE* dataStart; ///<Stack starts at these positions
         uint64_t size; ///<The number of BASE_DATA_TYPE datapieces currently used in each stack
         /**

diff --git a/utils/minisat b/utils/minisat