![]() |
OR-Tools
8.2
|
Definition at line 40 of file drat_checker.h.
Public Types | |
enum | Status { UNKNOWN , VALID , INVALID } |
Public Member Functions | |
DratChecker () | |
~DratChecker () | |
int | num_variables () const |
void | AddProblemClause (absl::Span< const Literal > clause) |
void | AddInferedClause (absl::Span< const Literal > clause) |
void | DeleteClause (absl::Span< const Literal > clause) |
Status | Check (double max_time_in_seconds) |
std::vector< std::vector< Literal > > | GetUnsatSubProblem () const |
std::vector< std::vector< Literal > > | GetOptimizedProof () const |
enum Status |
Enumerator | |
---|---|
UNKNOWN | |
VALID | |
INVALID |
Definition at line 76 of file drat_checker.h.
DratChecker | ( | ) |
Definition at line 47 of file drat_checker.cc.
|
inline |
Definition at line 43 of file drat_checker.h.
void AddInferedClause | ( | absl::Span< const Literal > | clause | ) |
Definition at line 69 of file drat_checker.cc.
void AddProblemClause | ( | absl::Span< const Literal > | clause | ) |
Definition at line 56 of file drat_checker.cc.
DratChecker::Status Check | ( | double | max_time_in_seconds | ) |
Definition at line 139 of file drat_checker.cc.
void DeleteClause | ( | absl::Span< const Literal > | clause | ) |
Definition at line 111 of file drat_checker.cc.
std::vector< std::vector< Literal > > GetOptimizedProof | ( | ) | const |
Definition at line 212 of file drat_checker.cc.
std::vector< std::vector< Literal > > GetUnsatSubProblem | ( | ) | const |
Definition at line 208 of file drat_checker.cc.
|
inline |
Definition at line 47 of file drat_checker.h.