Google OR-Tools v9.15
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research::sat::DratChecker Class Reference

Detailed Description

Definition at line 45 of file drat_checker.h.

#include <drat_checker.h>

Public Types

enum  Status { UNKNOWN , VALID , INVALID }

Public Member Functions

 DratChecker ()
 ~DratChecker ()=default
int num_variables () const
void AddProblemClause (absl::Span< const Literal > clause)
void AddInferredClause (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 operations_research::sat::DratChecker::Status
Enumerator
UNKNOWN 
VALID 
INVALID 

Definition at line 80 of file drat_checker.h.

Constructor & Destructor Documentation

◆ DratChecker()

operations_research::sat::DratChecker::DratChecker ( )

Definition at line 61 of file drat_checker.cc.

◆ ~DratChecker()

operations_research::sat::DratChecker::~DratChecker ( )
default

Member Function Documentation

◆ AddInferredClause()

void operations_research::sat::DratChecker::AddInferredClause ( absl::Span< const Literal > clause)

Definition at line 84 of file drat_checker.cc.

◆ AddProblemClause()

void operations_research::sat::DratChecker::AddProblemClause ( absl::Span< const Literal > clause)

Definition at line 70 of file drat_checker.cc.

◆ Check()

DratChecker::Status operations_research::sat::DratChecker::Check ( double max_time_in_seconds)

Definition at line 160 of file drat_checker.cc.

◆ DeleteClause()

void operations_research::sat::DratChecker::DeleteClause ( absl::Span< const Literal > clause)

Definition at line 130 of file drat_checker.cc.

◆ GetOptimizedProof()

std::vector< std::vector< Literal > > operations_research::sat::DratChecker::GetOptimizedProof ( ) const

Definition at line 233 of file drat_checker.cc.

◆ GetUnsatSubProblem()

std::vector< std::vector< Literal > > operations_research::sat::DratChecker::GetUnsatSubProblem ( ) const

Definition at line 229 of file drat_checker.cc.

◆ num_variables()

int operations_research::sat::DratChecker::num_variables ( ) const
inline

Definition at line 52 of file drat_checker.h.

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