Google OR-Tools v9.15
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research::sat::UniqueClauseStream Class Reference

Detailed Description

Definition at line 775 of file synchronization.h.

#include <synchronization.h>

Public Member Functions

 UniqueClauseStream ()
 UniqueClauseStream (const UniqueClauseStream &)=delete
 UniqueClauseStream (UniqueClauseStream &&)=default
bool Add (absl::Span< const int > clause, int lbd=2)
bool BlockClause (absl::Span< const int > clause)
CompactVectorVector< int > NextBatch ()
void ClearFingerprints ()
int NumLiteralsOfSize (int size) const
int NumBufferedLiterals () const
int lbd_threshold () const
void set_lbd_threshold (int lbd_threshold)

Static Public Member Functions

static size_t HashClause (absl::Span< const int > clause, size_t hash_seed=0)

Static Public Attributes

static constexpr int kMinClauseSize = 3
static constexpr int kMaxClauseSize = 32
static constexpr int kMinLbd = 2
static constexpr int kMaxLbd = 5
static constexpr int kMaxLiteralsPerBatch = 4096 / sizeof(int)

Constructor & Destructor Documentation

◆ UniqueClauseStream() [1/3]

operations_research::sat::UniqueClauseStream::UniqueClauseStream ( )

Definition at line 1220 of file synchronization.cc.

◆ UniqueClauseStream() [2/3]

operations_research::sat::UniqueClauseStream::UniqueClauseStream ( const UniqueClauseStream & )
delete

◆ UniqueClauseStream() [3/3]

operations_research::sat::UniqueClauseStream::UniqueClauseStream ( UniqueClauseStream && )
default

Member Function Documentation

◆ Add()

bool operations_research::sat::UniqueClauseStream::Add ( absl::Span< const int > clause,
int lbd = 2 )

Definition at line 1227 of file synchronization.cc.

◆ BlockClause()

bool operations_research::sat::UniqueClauseStream::BlockClause ( absl::Span< const int > clause)

Definition at line 1248 of file synchronization.cc.

◆ ClearFingerprints()

void operations_research::sat::UniqueClauseStream::ClearFingerprints ( )
inline

Definition at line 805 of file synchronization.h.

◆ HashClause()

size_t operations_research::sat::UniqueClauseStream::HashClause ( absl::Span< const int > clause,
size_t hash_seed = 0 )
static

Definition at line 1301 of file synchronization.cc.

◆ lbd_threshold()

int operations_research::sat::UniqueClauseStream::lbd_threshold ( ) const
inline

Definition at line 815 of file synchronization.h.

◆ NextBatch()

CompactVectorVector< int > operations_research::sat::UniqueClauseStream::NextBatch ( )

Definition at line 1256 of file synchronization.cc.

◆ NumBufferedLiterals()

int operations_research::sat::UniqueClauseStream::NumBufferedLiterals ( ) const

Definition at line 1293 of file synchronization.cc.

◆ NumLiteralsOfSize()

int operations_research::sat::UniqueClauseStream::NumLiteralsOfSize ( int size) const

Definition at line 1324 of file synchronization.cc.

◆ set_lbd_threshold()

void operations_research::sat::UniqueClauseStream::set_lbd_threshold ( int lbd_threshold)
inline

Definition at line 816 of file synchronization.h.

Member Data Documentation

◆ kMaxClauseSize

int operations_research::sat::UniqueClauseStream::kMaxClauseSize = 32
staticconstexpr

Definition at line 778 of file synchronization.h.

◆ kMaxLbd

int operations_research::sat::UniqueClauseStream::kMaxLbd = 5
staticconstexpr

Definition at line 780 of file synchronization.h.

◆ kMaxLiteralsPerBatch

int operations_research::sat::UniqueClauseStream::kMaxLiteralsPerBatch = 4096 / sizeof(int)
staticconstexpr

Definition at line 782 of file synchronization.h.

◆ kMinClauseSize

int operations_research::sat::UniqueClauseStream::kMinClauseSize = 3
staticconstexpr

Definition at line 777 of file synchronization.h.

◆ kMinLbd

int operations_research::sat::UniqueClauseStream::kMinLbd = 2
staticconstexpr

Definition at line 779 of file synchronization.h.

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