diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-04-05 10:03:05 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-05 10:03:05 -0700 |
commit | d663720936b0b873c917fc3fce9999f069bea0f1 (patch) | |
tree | e53e80666f4f8b512a41c9f29830bf5239c94a09 /src/prop | |
parent | 7de51f8f53db83ebbc871a4d437c382b6ef8d2ba (diff) |
SatClauseSetHashFunction (#2916)
* SatClauseHashFunction
Added to the same file as SatLiteralHashFunction.
* clang-format
Thanks Andres!
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/sat_solver_types.h | 16 |
1 files changed, 16 insertions, 0 deletions
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. |