![]() |
OR-Tools
8.2
|
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) |
DratProofHandler | ( | ) |
Definition at line 26 of file drat_proof_handler.cc.
DratProofHandler | ( | bool | in_binary_format, |
File * | output, | ||
bool | check = false |
||
) |
Definition at line 29 of file drat_proof_handler.cc.
|
inline |
Definition at line 49 of file drat_proof_handler.h.
void AddClause | ( | absl::Span< const Literal > | clause | ) |
Definition at line 72 of file drat_proof_handler.cc.
void AddOneVariable | ( | ) |
Definition at line 62 of file drat_proof_handler.cc.
void AddProblemClause | ( | absl::Span< const Literal > | clause | ) |
Definition at line 66 of file drat_proof_handler.cc.
void ApplyMapping | ( | const absl::StrongVector< BooleanVariable, BooleanVariable > & | mapping | ) |
Definition at line 38 of file drat_proof_handler.cc.
DratChecker::Status Check | ( | double | max_time_in_seconds | ) |
Definition at line 92 of file drat_proof_handler.cc.
void DeleteClause | ( | absl::Span< const Literal > | clause | ) |
Definition at line 82 of file drat_proof_handler.cc.
void SetNumVariables | ( | int | num_variables | ) |
Definition at line 55 of file drat_proof_handler.cc.