SatClauseSetHashFunction (#2916)

* SatClauseHashFunction

Added to the same file as SatLiteralHashFunction.

* clang-format

Thanks Andres!

diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 68fd04b1fd10e8f05e5e39350b6c1552276dc0fa..f1fd6233e0abedf856b342911cce97943f462894 100644 (file)
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -26,6 +26,7 @@
 
 #include <sstream>
 #include <string>
+#include <unordered_set>
 #include <vector>
 
 namespace CVC4 {
@@ -167,6 +168,21 @@ struct SatLiteralHashFunction {
  */
 typedef std::vector<SatLiteral> SatClause;
 
+struct SatClauseSetHashFunction
+{
+  inline size_t operator()(
+      const std::unordered_set<SatLiteral, SatLiteralHashFunction>& clause)
+      const
+  {
+    size_t acc = 0;
+    for (const auto& l : clause)
+    {
+      acc ^= l.hash();
+    }
+    return acc;
+  }
+};
+
 /**
  * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
  * so that the SAT solver can (or should) remove them when the lifespan is over.