operations_research::sat::LratProofHandler Class Reference

Detailed Description

Definition at line 140 of file lrat_proof_handler.h.

#include <lrat_proof_handler.h>

Public Member Functions
bool	lrat_check_enabled () const
bool	lrat_output_enabled () const
bool	drat_check_enabled () const
bool	drat_output_enabled () const
int64_t	num_assumed_clauses () const
bool	AddProblemClause (ClauseId id, absl::Span< const Literal > clause)
void	EndProblemClauses ()
bool	AddInferredClause (ClauseId id, absl::Span< const Literal > clause, absl::Span< const ClauseId > unit_ids, bool exported=false)
bool	AddInferredClause (ClauseId id, absl::Span< const Literal > clause, absl::Span< const ClauseId > unit_ids, absl::Span< const LratChecker::RatIds > rat, bool exported=false)
ClauseId	AddAndProveInferredClauseByEnumeration (absl::Span< const Literal > new_clause, absl::Span< const ClauseId > ids_for_proof, const CompactVectorVector< int, Literal > &clauses_for_proof)
bool	AddImportedClause (ClauseId id, absl::Span< const Literal > clause)
bool	AddAssumedClause (ClauseId id, absl::Span< const Literal > clause)
bool	ExportClause (ClauseId id, absl::Span< const Literal > clause)
void	PinClause (ClauseId id, absl::Span< const Literal > clause)
void	UnpinClause (ClauseId id)
void	DeleteClause (ClauseId id, absl::Span< const Literal > clause)
DratChecker::Status	Valid () const
DratChecker::Status	Check ()
void	Close (bool model_is_unsat)
absl::Span< const Literal >	GetLratClauseForDebug (ClauseId id) const

Static Public Member Functions
static std::unique_ptr< LratProofHandler >	MaybeCreate (Model *model)
static std::unique_ptr< LratProofHandler >	MaybeCreate (const SatParameters &params, ClauseIdGenerator *id_generator, SharedLratProofStatus *proof_status, SharedStatistics *stats)

Member Function Documentation

AddAndProveInferredClauseByEnumeration()

ClauseId operations_research::sat::LratProofHandler::AddAndProveInferredClauseByEnumeration	(	absl::Span< const Literal >	new_clause,
		absl::Span< const ClauseId >	ids_for_proof,
		const CompactVectorVector< int, Literal > &	clauses_for_proof )

Definition at line 738 of file lrat_proof_handler.cc.

AddAssumedClause()

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

Definition at line 613 of file lrat_proof_handler.cc.

AddImportedClause()

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

Definition at line 595 of file lrat_proof_handler.cc.

AddInferredClause() [1/2]

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

Definition at line 563 of file lrat_proof_handler.cc.

AddInferredClause() [2/2]

bool operations_research::sat::LratProofHandler::AddInferredClause ( ClauseId id, absl::Span< const Literal > clause, absl::Span< const ClauseId > unit_ids, bool exported = false )

inline

Definition at line 162 of file lrat_proof_handler.h.

AddProblemClause()

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

Definition at line 532 of file lrat_proof_handler.cc.

Check()

DratChecker::Status operations_research::sat::LratProofHandler::Check

(

)

Definition at line 696 of file lrat_proof_handler.cc.

Close()

void operations_research::sat::LratProofHandler::Close

(

bool

model_is_unsat

)

Definition at line 722 of file lrat_proof_handler.cc.

DeleteClause()

void operations_research::sat::LratProofHandler::DeleteClause	(	ClauseId	id,
		absl::Span< const Literal >	clause )

Definition at line 664 of file lrat_proof_handler.cc.

drat_check_enabled()

bool operations_research::sat::LratProofHandler::drat_check_enabled ( ) const

inline

Definition at line 149 of file lrat_proof_handler.h.

drat_output_enabled()

bool operations_research::sat::LratProofHandler::drat_output_enabled ( ) const

inline

Definition at line 150 of file lrat_proof_handler.h.

EndProblemClauses()

void operations_research::sat::LratProofHandler::EndProblemClauses

(

)

Definition at line 553 of file lrat_proof_handler.cc.

ExportClause()

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

Definition at line 634 of file lrat_proof_handler.cc.

GetLratClauseForDebug()

absl::Span< const Literal > operations_research::sat::LratProofHandler::GetLratClauseForDebug ( ClauseId id ) const

inline

Definition at line 232 of file lrat_proof_handler.h.

lrat_check_enabled()

bool operations_research::sat::LratProofHandler::lrat_check_enabled ( ) const

inline

Definition at line 147 of file lrat_proof_handler.h.

lrat_output_enabled()

bool operations_research::sat::LratProofHandler::lrat_output_enabled ( ) const

inline

Definition at line 148 of file lrat_proof_handler.h.

MaybeCreate() [1/2]

std::unique_ptr< LratProofHandler > operations_research::sat::LratProofHandler::MaybeCreate ( const SatParameters & params, ClauseIdGenerator * id_generator, SharedLratProofStatus * proof_status, SharedStatistics * stats )

static

Definition at line 494 of file lrat_proof_handler.cc.

MaybeCreate() [2/2]

std::unique_ptr< LratProofHandler > operations_research::sat::LratProofHandler::MaybeCreate ( Model * model )

static

Definition at line 487 of file lrat_proof_handler.cc.

num_assumed_clauses()

int64_t operations_research::sat::LratProofHandler::num_assumed_clauses ( ) const

inline

Definition at line 152 of file lrat_proof_handler.h.

PinClause()

void operations_research::sat::LratProofHandler::PinClause	(	ClauseId	id,
		absl::Span< const Literal >	clause )

Definition at line 644 of file lrat_proof_handler.cc.

UnpinClause()

void operations_research::sat::LratProofHandler::UnpinClause

(

ClauseId

id

)

Definition at line 655 of file lrat_proof_handler.cc.

Valid()

DratChecker::Status operations_research::sat::LratProofHandler::Valid

(

)

const

Definition at line 686 of file lrat_proof_handler.cc.

---

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

• ortools/sat/lrat_proof_handler.h
• ortools/sat/lrat_proof_handler.cc