operations_research::sat::SatClause Class Reference

Detailed Description

Definition at line 55 of file clause.h.

#include <clause.h>

Public Member Functions
void	operator delete (void *p)
int	size () const
bool	empty () const
int	IsRemoved () const
const Literal *	begin () const
const Literal *	end () const
Literal	FirstLiteral () const
Literal	SecondLiteral () const
Literal	PropagatedLiteral () const
absl::Span< const Literal >	PropagationReason () const
absl::Span< const Literal >	AsSpan () const
bool	IsSatisfied (const VariablesAssignment &assignment) const
std::string	DebugString () const

Static Public Member Functions
static SatClause *	Create (absl::Span< const Literal > literals)

Friends
class	ClauseManager

Member Function Documentation

AsSpan()

absl::Span< const Literal > operations_research::sat::SatClause::AsSpan ( ) const

inline

Definition at line 100 of file clause.h.

begin()

const Literal * operations_research::sat::SatClause::begin ( ) const

inline

Definition at line 79 of file clause.h.

Create()

SatClause * operations_research::sat::SatClause::Create ( absl::Span< const Literal > literals )

static

Definition at line 3590 of file clause.cc.

DebugString()

std::string operations_research::sat::SatClause::DebugString

(

)

const

Definition at line 3634 of file clause.cc.

empty()

bool operations_research::sat::SatClause::empty ( ) const

inline

Definition at line 70 of file clause.h.

end()

const Literal * operations_research::sat::SatClause::end ( ) const

inline

Definition at line 80 of file clause.h.

FirstLiteral()

Literal operations_research::sat::SatClause::FirstLiteral ( ) const

inline

Definition at line 84 of file clause.h.

IsRemoved()

int operations_research::sat::SatClause::IsRemoved ( ) const

inline

Definition at line 76 of file clause.h.

IsSatisfied()

bool operations_research::sat::SatClause::IsSatisfied

(

const VariablesAssignment &

assignment

)

const

Definition at line 3627 of file clause.cc.

operator delete()

void operations_research::sat::SatClause::operator delete ( void * p )

inline

Definition at line 64 of file clause.h.

PropagatedLiteral()

Literal operations_research::sat::SatClause::PropagatedLiteral ( ) const

inline

Definition at line 90 of file clause.h.

PropagationReason()

absl::Span< const Literal > operations_research::sat::SatClause::PropagationReason ( ) const

inline

Definition at line 95 of file clause.h.

SecondLiteral()

Literal operations_research::sat::SatClause::SecondLiteral ( ) const

inline

Definition at line 85 of file clause.h.

size()

int operations_research::sat::SatClause::size ( ) const

inline

Definition at line 69 of file clause.h.

Friends And Related Symbol Documentation

ClauseManager

friend class ClauseManager

friend

Definition at line 114 of file clause.h.

---

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

• ortools/sat/clause.h
• ortools/sat/clause.cc