operations_research::sat::LratWriter Class Reference

Detailed Description

Definition at line 45 of file lrat_proof_handler.h.

#include <lrat_proof_handler.h>

Public Member Functions
	LratWriter (std::string_view filename)
	~LratWriter ()
std::string_view	filename () const
void	AddImportedClause (ClauseId id, absl::Span< const Literal > clause)
void	AddInferredClause (ClauseId id, absl::Span< const Literal > clause, absl::Span< const ClauseId > unit_ids, absl::Span< const LratChecker::RatIds > rat, bool exported=false)
void	ExportClause (ClauseId id, absl::Span< const Literal > clause)
void	DeleteClause (ClauseId id)

Constructor & Destructor Documentation

LratWriter()

operations_research::sat::LratWriter::LratWriter ( std::string_view filename )

explicit

Definition at line 64 of file lrat_proof_handler.cc.

~LratWriter()

operations_research::sat::LratWriter::~LratWriter

(

)

Definition at line 73 of file lrat_proof_handler.cc.

Member Function Documentation

AddImportedClause()

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

Definition at line 78 of file lrat_proof_handler.cc.

AddInferredClause()

void operations_research::sat::LratWriter::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 90 of file lrat_proof_handler.cc.

DeleteClause()

void operations_research::sat::LratWriter::DeleteClause

(

ClauseId

id

)

Definition at line 127 of file lrat_proof_handler.cc.

ExportClause()

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

Definition at line 116 of file lrat_proof_handler.cc.

filename()

std::string_view operations_research::sat::LratWriter::filename ( ) const

inline

Definition at line 50 of file lrat_proof_handler.h.

---

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

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