Skip to content

Commit 3c5ab7a

Browse files
Natasha Yogananda Jeppudanielsn
Natasha Yogananda Jeppu
authored andcommitted
Store clause counter value from satcheck_minisat instead of storing the clause itself
Add comment to explain solver_clause_num + 1 in solver hardness, change <int> to <size_t>
1 parent 1cb2d40 commit 3c5ab7a

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed

src/solvers/solver_hardness.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,8 @@ void solver_hardnesst::register_clause(
108108
std::cout << "0\n";
109109
#endif
110110

111+
// The clause_counter is incremented after the call to register_clause.
112+
// Here we add 1 to solver_clause_num to incorporate this increment.
111113
current_hardness.clause_set.push_back(solver_clause_num + 1);
112114
std::sort(
113115
current_hardness.clause_set.begin(), current_hardness.clause_set.end());

src/solvers/solver_hardness.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ struct solver_hardnesst
5050
size_t clauses = 0;
5151
size_t literals = 0;
5252
std::unordered_set<size_t> variables = {};
53-
std::vector<int> clause_set = {};
53+
std::vector<size_t> clause_set = {};
5454

5555
sat_hardnesst &operator+=(const sat_hardnesst &other);
5656
};

0 commit comments

Comments
 (0)