OR-Tools  8.2
DratProofHandler

Detailed Description

Definition at line 40 of file drat_proof_handler.h.

Public Member Functions

 DratProofHandler ()
 
 DratProofHandler (bool in_binary_format, File *output, bool check=false)
 
 ~DratProofHandler ()
 
void ApplyMapping (const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
 
void SetNumVariables (int num_variables)
 
void AddOneVariable ()
 
void AddProblemClause (absl::Span< const Literal > clause)
 
void AddClause (absl::Span< const Literal > clause)
 
void DeleteClause (absl::Span< const Literal > clause)
 
DratChecker::Status Check (double max_time_in_seconds)
 

Constructor & Destructor Documentation

◆ DratProofHandler() [1/2]

Definition at line 26 of file drat_proof_handler.cc.

◆ DratProofHandler() [2/2]

DratProofHandler ( bool  in_binary_format,
File output,
bool  check = false 
)

Definition at line 29 of file drat_proof_handler.cc.

◆ ~DratProofHandler()

~DratProofHandler ( )
inline

Definition at line 49 of file drat_proof_handler.h.

Member Function Documentation

◆ AddClause()

void AddClause ( absl::Span< const Literal clause)

Definition at line 72 of file drat_proof_handler.cc.

◆ AddOneVariable()

void AddOneVariable ( )

Definition at line 62 of file drat_proof_handler.cc.

◆ AddProblemClause()

void AddProblemClause ( absl::Span< const Literal clause)

Definition at line 66 of file drat_proof_handler.cc.

◆ ApplyMapping()

void ApplyMapping ( const absl::StrongVector< BooleanVariable, BooleanVariable > &  mapping)

Definition at line 38 of file drat_proof_handler.cc.

◆ Check()

DratChecker::Status Check ( double  max_time_in_seconds)

Definition at line 92 of file drat_proof_handler.cc.

◆ DeleteClause()

void DeleteClause ( absl::Span< const Literal clause)

Definition at line 82 of file drat_proof_handler.cc.

◆ SetNumVariables()

void SetNumVariables ( int  num_variables)

Definition at line 55 of file drat_proof_handler.cc.


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