operations_research::sat::LratChecker Class Reference

Detailed Description

Definition at line 38 of file lrat_checker.h.

#include <lrat_checker.h>

Classes
struct	RatIds

Public Member Functions
	LratChecker (Model *model)
	LratChecker (SharedStatistics *stats)
bool	AddProblemClause (ClauseId id, absl::Span< const Literal > clause)
*Either clause and the r resolvant_id clause have two pairs of *Or all the r unit_ids clauses must become unit and eventually empty bool	AddInferredClause (ClauseId id, absl::Span< const Literal > clause, absl::Span< const ClauseId > unit_ids, absl::Span< const RatIds > rat={})
void	DeleteClauses (absl::Span< const ClauseId > clause_ids)
bool	Valid () const
bool	Check ()
void	AddStats () const
std::string_view	error_message () const
absl::Span< const Literal >	GetClauseForDebug (ClauseId id) const

Constructor & Destructor Documentation

LratChecker() [1/2]

operations_research::sat::LratChecker::LratChecker ( Model * model )

inlineexplicit

Definition at line 40 of file lrat_checker.h.

LratChecker() [2/2]

operations_research::sat::LratChecker::LratChecker ( SharedStatistics * stats )

inlineexplicit

Definition at line 42 of file lrat_checker.h.

Member Function Documentation

AddInferredClause()

bool operations_research::sat::LratChecker::AddInferredClause	(	ClauseId	id,
		absl::Span< const Literal >	clause,
		absl::Span< const ClauseId >	unit_ids,
		absl::Span< const RatIds >	rat = {} )

Definition at line 59 of file lrat_checker.cc.

AddProblemClause()

bool operations_research::sat::LratChecker::AddProblemClause	(	ClauseId	id,
		absl::Span< const Literal >	clause )

Definition at line 52 of file lrat_checker.cc.

AddStats()

void operations_research::sat::LratChecker::AddStats

(

)

const

Definition at line 34 of file lrat_checker.cc.

Check()

bool operations_research::sat::LratChecker::Check ( )

inline

Definition at line 104 of file lrat_checker.h.

DeleteClauses()

void operations_research::sat::LratChecker::DeleteClauses

(

absl::Span< const ClauseId >

clause_ids

)

Definition at line 68 of file lrat_checker.cc.

error_message()

std::string_view operations_research::sat::LratChecker::error_message ( ) const

inline

Definition at line 115 of file lrat_checker.h.

GetClauseForDebug()

absl::Span< const Literal > operations_research::sat::LratChecker::GetClauseForDebug ( ClauseId id ) const

inline

Definition at line 118 of file lrat_checker.h.

Valid()

bool operations_research::sat::LratChecker::Valid ( ) const

inline

Definition at line 100 of file lrat_checker.h.

---

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

• ortools/sat/lrat_checker.h
• ortools/sat/lrat_checker.cc