operations_research::sat::ClauseWithOneMissingHasher Class Reference

Class to help detects clauses that differ on a single literal. More...

#include <presolve_util.h>

Public Member Functions
	ClauseWithOneMissingHasher (absl::BitGenRef random)
void	RegisterClause (int c, absl::Span< const int > clause)
	We use the proto encoding of literals here.
uint64_t	HashWithout (int c, int ref) const
uint64_t	HashOfNegatedLiterals (absl::Span< const int > literals)
	Returns a hash of the negation of all the given literals.

Detailed Description

Class to help detects clauses that differ on a single literal.

Definition at line 294 of file presolve_util.h.

Constructor & Destructor Documentation

ClauseWithOneMissingHasher()

operations_research::sat::ClauseWithOneMissingHasher::ClauseWithOneMissingHasher ( absl::BitGenRef random )

inlineexplicit

Definition at line 296 of file presolve_util.h.

Member Function Documentation

HashOfNegatedLiterals()

uint64_t operations_research::sat::ClauseWithOneMissingHasher::HashOfNegatedLiterals

(

absl::Span< const int >

literals

)

Returns a hash of the negation of all the given literals.

We use random value for a literal hash.

Definition at line 674 of file presolve_util.cc.

HashWithout()

uint64_t operations_research::sat::ClauseWithOneMissingHasher::HashWithout ( int c, int ref ) const

inline

Returns a hash of the clause with index c and literal ref removed. This assumes that ref was part of the clause. Work in O(1).

Definition at line 304 of file presolve_util.h.

RegisterClause()

void operations_research::sat::ClauseWithOneMissingHasher::RegisterClause	(	int	c,
		absl::Span< const int >	clause )

We use the proto encoding of literals here.

We use random value for a literal hash.

Definition at line 658 of file presolve_util.cc.

---

The documentation for this class was generated from the following files:

• ortools/sat/presolve_util.h
• ortools/sat/presolve_util.cc