Improve sbva_lib memory management

davidmisiak · Aug 4, 2023 · ff2ffdf · ff2ffdf
1 parent 7eee714
commit ff2ffdf
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 15 deletions.
diff --git a/external/SBVA/sbva_lib.cc b/external/SBVA/sbva_lib.cc
@@ -76,7 +76,7 @@ class Formula {
 public:
     Formula() { adj_deleted = 0; }
 
-    void read_cnf(vector<vector<int>> cnf) {
+    void read_cnf(const vector<vector<int>> &cnf) {
         ClauseCache cache;
 
         int curr_clause = 0;
@@ -91,7 +91,7 @@ class Formula {
             }
         }
         clauses = vector<Clause>(num_clauses);
-        clauses.reserve(num_clauses * 10);
+        // clauses.reserve(num_clauses * 10);
         lit_to_clauses = vector<vector<int>>(num_vars * 2);
         lit_count_adjust = vector<int>(num_vars * 2);
         adjacency_matrix_width = num_vars * 4;
@@ -258,19 +258,19 @@ class Formula {
         vector<int> matched_clauses_swap = vector<int>();
         vector<int> matched_clauses_id = vector<int>();
         vector<int> matched_clauses_id_swap = vector<int>();
-        matched_lits.reserve(10000);
-        matched_clauses.reserve(10000);
-        matched_clauses_swap.reserve(10000);
-        matched_clauses_id.reserve(10000);
-        matched_clauses_id_swap.reserve(10000);
+        // matched_lits.reserve(10000);
+        // matched_clauses.reserve(10000);
+        // matched_clauses_swap.reserve(10000);
+        // matched_clauses_id.reserve(10000);
+        // matched_clauses_id_swap.reserve(10000);
 
         // Track the index of the matched clauses from every literal that is added to matched_lits.
         vector<tuple<int, int>> clauses_to_remove = vector<tuple<int, int>>();
-        clauses_to_remove.reserve(10000);
+        // clauses_to_remove.reserve(10000);
 
         // Used for computing clause differences
         vector<int> diff = vector<int>();
-        diff.reserve(10000);
+        // diff.reserve(10000);
 
         // Keep track of the matrix of swaps that we can perform.
         // Each entry is of the form (literal, <clause index>, <index in matched_clauses>)
@@ -308,15 +308,15 @@ class Formula {
         //              (C v E)  (C v F)  (C v H)
         //
         vector<tuple<int, int, int>> matched_entries = vector<tuple<int, int, int>>();
-        matched_entries.reserve(10000);
+        // matched_entries.reserve(10000);
 
         // Keep a list of the literals that are matched so we can sort and count later.
         vector<int> matched_entries_lits = vector<int>();
-        matched_entries_lits.reserve(10000);
+        // matched_entries_lits.reserve(10000);
 
         // Used for priority queue updates.
         unordered_set<int> lits_to_update;
-        lits_to_update.reserve(10000);
+        // lits_to_update.reserve(10000);
 
         // Track number of replacements (new auxiliary variables).
         int num_replacements = 0;
@@ -636,7 +636,7 @@ class Formula {
     map<int, int> tmp_heuristic_cache_full;
 };
 
-pair<int, vector<vector<int>>> runBVA(vector<vector<int>> cnf, int max_seconds) {
+pair<int, vector<vector<int>>> runBVA(const vector<vector<int>> &cnf, int max_seconds) {
     end_time = nullptr;
     if (max_seconds) {
         end_time = make_unique<std::chrono::high_resolution_clock::time_point>(

diff --git a/src/solvers/sat/sbva_wrapper.cpp b/src/solvers/sat/sbva_wrapper.cpp
@@ -9,8 +9,8 @@
 #include "solvers/sat/sat_utils.hpp"
 #include "solvers/sat/sat_wrapper.hpp"
 
-extern std::pair<int, std::vector<std::vector<int>>> runBVA(std::vector<std::vector<int>> cnf,
-                                                            int max_seconds);
+extern std::pair<int, std::vector<std::vector<int>>> runBVA(
+        const std::vector<std::vector<int>>& cnf, int max_seconds);
 
 void SbvaWrapper::run(std::unique_ptr<SatWrapper>& sat_wrapper, int max_seconds) {
     // convert sat_utils::Clause to DIMACS input for SBVA