From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 5 Apr 2019 17:03:05 +0000 (-0700)
Subject: SatClauseSetHashFunction (#2916)
X-Git-Tag: cvc5-1.0.0~4191
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d663720936b0b873c917fc3fce9999f069bea0f1;p=cvc5.git

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 68fd04b1f..f1fd6233e 100644
--- 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.