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

Detailed Description

Definition at line 1718 of file clause.cc.

Public Member Functions

 LratEquivalenceHelper (BinaryImplicationGraph *graph)
void NewComponent (absl::Span< const int32_t > component)
bool FixAllLiteralsInComponent (LiteralIndex fixed_literal, bool all_true)
void ProcessSingletonComponent ()
void ProcessComponent (LiteralIndex representative)
void ProcessUnsatComponent (Literal literal, Literal representative)
void ComputeImplicationChain (Literal a, Literal b, util_intops::StrongVector< LiteralIndex, LiteralIndex > &parents, std::vector< ClauseId > &clause_ids)

Constructor & Destructor Documentation

◆ LratEquivalenceHelper()

operations_research::sat::LratEquivalenceHelper::LratEquivalenceHelper ( BinaryImplicationGraph * graph)
inlineexplicit

Definition at line 1720 of file clause.cc.

Member Function Documentation

◆ ComputeImplicationChain()

void operations_research::sat::LratEquivalenceHelper::ComputeImplicationChain ( Literal a,
Literal b,
util_intops::StrongVector< LiteralIndex, LiteralIndex > & parents,
std::vector< ClauseId > & clause_ids )
inline

Definition at line 1873 of file clause.cc.

◆ FixAllLiteralsInComponent()

bool operations_research::sat::LratEquivalenceHelper::FixAllLiteralsInComponent ( LiteralIndex fixed_literal,
bool all_true )
inline

Definition at line 1747 of file clause.cc.

◆ NewComponent()

void operations_research::sat::LratEquivalenceHelper::NewComponent ( absl::Span< const int32_t > component)
inline

Definition at line 1732 of file clause.cc.

◆ ProcessComponent()

void operations_research::sat::LratEquivalenceHelper::ProcessComponent ( LiteralIndex representative)
inline

Definition at line 1797 of file clause.cc.

◆ ProcessSingletonComponent()

void operations_research::sat::LratEquivalenceHelper::ProcessSingletonComponent ( )
inline

Definition at line 1774 of file clause.cc.

◆ ProcessUnsatComponent()

void operations_research::sat::LratEquivalenceHelper::ProcessUnsatComponent ( Literal literal,
Literal representative )
inline

Definition at line 1853 of file clause.cc.

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