OR-Tools  8.2
DratChecker

Detailed Description

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
 

Member Enumeration Documentation

◆ Status

enum Status
Enumerator
UNKNOWN 
VALID 
INVALID 

Definition at line 76 of file drat_checker.h.

Constructor & Destructor Documentation

◆ DratChecker()

Definition at line 47 of file drat_checker.cc.

◆ ~DratChecker()

~DratChecker ( )
inline

Definition at line 43 of file drat_checker.h.

Member Function Documentation

◆ AddInferedClause()

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

Definition at line 69 of file drat_checker.cc.

◆ AddProblemClause()

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

Definition at line 56 of file drat_checker.cc.

◆ Check()

DratChecker::Status Check ( double  max_time_in_seconds)

Definition at line 139 of file drat_checker.cc.

◆ DeleteClause()

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

Definition at line 111 of file drat_checker.cc.

◆ GetOptimizedProof()

std::vector< std::vector< Literal > > GetOptimizedProof ( ) const

Definition at line 212 of file drat_checker.cc.

◆ GetUnsatSubProblem()

std::vector< std::vector< Literal > > GetUnsatSubProblem ( ) const

Definition at line 208 of file drat_checker.cc.

◆ num_variables()

int num_variables ( ) const
inline

Definition at line 47 of file drat_checker.h.


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