Make sure a ReferenceStat is set to values of the correct type (#6430)

This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index e517b8f74a8b66ce43d152e3cdaad8df323919f7..e7d9086bc35fb86c1c0392a48258f845a2d57dc2 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -1412,9 +1412,9 @@ bool Solver::withinBudget(Resource r) const
   d_notify->safePoint(r);
 
   return !asynch_interrupt &&
-         (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
+         (conflict_budget < 0 || conflicts < conflict_budget) &&
          (propagation_budget < 0 ||
-          propagations < (uint64_t)propagation_budget);
+          propagations < propagation_budget);
 }
 
 }  // namespace BVMinisat

diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index d2423a71a25455583217b3c747929de831122d1e..7c08c3bcf6170655972d7d4992dec699522a69a8 100644 (file)
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -235,8 +235,8 @@ public:
 
  // Statistics: (read-only member variable)
  //
- uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
- uint64_t dec_vars, clauses_literals, learnts_literals, max_literals,
+ int64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+ int64_t dec_vars, clauses_literals, learnts_literals, max_literals,
      tot_literals;
 
  // Bitvector Propagations

diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index b103243d32bd2c4f36245a9de3e67ec2807ebc29..ec6ed375a3b5df98ff9b509ee60a945d482d4f54 100644 (file)
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -114,7 +114,7 @@ class SimpSolver : public Solver {
     //
     int     merges;
     int     asymm_lits;
-    int     eliminated_vars;
+    int64_t eliminated_vars;
     //    cvc5::TimerStat total_eliminate_time;
 
    protected:

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ea30c12e92c556a507cc4887ae278088f7419f7c..40274489b77d104258ff6f7bbd06c2e9ddf63d35 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -2383,10 +2383,8 @@ inline bool Solver::withinBudget(Resource r) const
   d_proxy->spendResource(r);
 
   bool within_budget =
-      !asynch_interrupt
-      && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget)
-      && (propagation_budget < 0
-          || propagations < (uint64_t)propagation_budget);
+      !asynch_interrupt && (conflict_budget < 0 || conflicts < conflict_budget)
+      && (propagation_budget < 0 || propagations < propagation_budget);
   return within_budget;
 }
 

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index f85dc0d242959604261994e3aace6bbda40ee892..cd3f38c9efee3937becfcb86b582b0f755f68522 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -351,9 +351,9 @@ public:
 
  // Statistics: (read-only member variable)
  //
- uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts,
+ int64_t solves, starts, decisions, rnd_decisions, propagations, conflicts,
      resources_consumed;
- uint64_t dec_vars, clauses_literals, learnts_literals, max_literals,
+ int64_t dec_vars, clauses_literals, learnts_literals, max_literals,
      tot_literals;
 
 protected:

diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h
index 93d7e3e2ad8067c928938a10c1b7e0197205fc62..4821dda601741e4842da1dcebbeb067ecfbb0103 100644 (file)
--- a/src/util/statistics_stats.h
+++ b/src/util/statistics_stats.h
@@ -122,8 +122,10 @@ class ReferenceStat
   /** Value stored for this statistic */
   using stat_type = StatisticReferenceValue<T>;
   /** Reset the reference to point to `t`. */
-  void set(const T& t)
+  template <typename TT>
+  void set(const TT& t)
   {
+    static_assert(std::is_same_v<T, TT>, "Incorrect type for ReferenceStat");
     if constexpr (Configuration::isStatisticsBuild())
     {
       d_data->d_value = &t;