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>

Remove sorting of clause set keeping performance in mind

Add additional utility to map program lines to clauses in --dimacs output

clang format

Author: Natasha Yogananda Jeppu

regression/solver-hardness/solver-hardness-simple/test.desc

@@ -5,7 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$
 ^VERIFICATION FAILED$
-^Valid JSON File$
-\"SAT_hardness\": \{(\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+)\}
+\"SAT_hardness\":\{(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\}
 --
 ^warning: ignoring

src/solvers/solver_hardness.h

@@ -106,8 +106,10 @@ struct solver_hardnesst
   /// Called e.g. from the `satcheck_minisat2::lcnf`, this function adds the
   ///   complexity statistics from the last SAT query to the `current_ssa_key`.
   /// \param bv: the clause (vector of literals)
-  /// \param solver_clause_num: clause counter value passed from
-  /// `satcheck_minisat2::lcnf`
+  /// \param cnf: processed clause
+  /// \param cnf_clause_index: index of clause in dimacs output
+  /// \param register_cnf: negation of boolean variable tracking if the clause
+  /// can be eliminated
   void register_clause(
     const bvt &bv,
     const bvt &cnf,