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()

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