Detailed Description

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)

Constructor & Destructor Documentation

◆ DratProofHandler() [1/2]

DratProofHandler ( )

Definition at line 26 of file drat_proof_handler.cc.

◆ DratProofHandler() [2/2]

DratProofHandler	(	bool	in_binary_format,
		File *	output,
		bool	check = `false`
	)

Definition at line 29 of file drat_proof_handler.cc.

◆ ~DratProofHandler()

~DratProofHandler ( )

inline

Definition at line 49 of file drat_proof_handler.h.

Member Function Documentation

◆ AddClause()

void AddClause ( absl::Span< const Literal > clause )

Definition at line 72 of file drat_proof_handler.cc.

◆ AddOneVariable()

void AddOneVariable ( )

Definition at line 62 of file drat_proof_handler.cc.

◆ AddProblemClause()

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

Definition at line 66 of file drat_proof_handler.cc.

◆ ApplyMapping()

void ApplyMapping ( const absl::StrongVector< BooleanVariable, BooleanVariable > & mapping )

Definition at line 38 of file drat_proof_handler.cc.

◆ Check()

DratChecker::Status Check ( double max_time_in_seconds )

Definition at line 92 of file drat_proof_handler.cc.

◆ DeleteClause()

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

Definition at line 82 of file drat_proof_handler.cc.

◆ SetNumVariables()

void SetNumVariables ( int num_variables )

Definition at line 55 of file drat_proof_handler.cc.

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