Detailed Description

Definition at line 368 of file sat_base.h.

#include <sat_base.h>

Public Member Functions
	EnqueueHelper (Literal trail_ptr, AssignmentInfo current_info, AssignmentInfo info_ptr, VariablesAssignment assignment, util_intops::StrongVector< BooleanVariable, ClauseId > *clause_ids)
void	EnqueueAtLevel (Literal true_literal, int level)
void	EnqueueWithUnitReason (Literal true_literal, ClauseId clause_id)
bool	LiteralIsTrue (Literal literal) const
bool	LiteralIsFalse (Literal literal) const

Constructor & Destructor Documentation

operations_research::sat::Trail::EnqueueHelper::EnqueueHelper	(	Literal *	trail_ptr,
		AssignmentInfo *	current_info,
		AssignmentInfo *	info_ptr,
		VariablesAssignment *	assignment,
		util_intops::StrongVector< BooleanVariable, ClauseId > *	clause_ids )

inline

Definition at line 370 of file sat_base.h.

void operations_research::sat::Trail::EnqueueHelper::EnqueueAtLevel	(	Literal	true_literal,
		int	level )

inline

Definition at line 380 of file sat_base.h.

void operations_research::sat::Trail::EnqueueHelper::EnqueueWithUnitReason	(	Literal	true_literal,
		ClauseId	clause_id )

inline

Definition at line 388 of file sat_base.h.

bool operations_research::sat::Trail::EnqueueHelper::LiteralIsFalse ( Literal literal ) const

inline

Definition at line 407 of file sat_base.h.

bool operations_research::sat::Trail::EnqueueHelper::LiteralIsTrue ( Literal literal ) const

inline

Definition at line 404 of file sat_base.h.

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