Information about a variable assignment. More...

Detailed Description

Information about a variable assignment.

Definition at line 242 of file sat_base.h.

#include <sat_base.h>

Public Member Functions
std::string	DebugString () const

Public Attributes
uint32_t	level: 28
uint32_t	type: 4
int32_t	trail_index
	The index of this assignment in the trail.

Member Function Documentation

std::string operations_research::sat::AssignmentInfo::DebugString ( ) const

inline

Definition at line 265 of file sat_base.h.

uint32_t operations_research::sat::AssignmentInfo::level

The decision level at which this assignment was made. This starts at 0 and increases each time the solver takes a search decision.

Todo: (user): We may be able to get rid of that for faster enqueues. Most of the code only need to know if this is 0 or the highest level, and for the LBD computation, the literal of the conflict are already ordered by level, so we could do it fairly efficiently.

Todo: (user): We currently don't support more than 2^28 decision levels. That should be enough for most practical problem, but we should fail properly if this limit is reached.

Definition at line 254 of file sat_base.h.

int32_t operations_research::sat::AssignmentInfo::trail_index

The index of this assignment in the trail.

Definition at line 263 of file sat_base.h.

uint32_t operations_research::sat::AssignmentInfo::type

mutable

The type of assignment (see AssignmentType below).

Note(user): We currently don't support more than 16 types of assignment. This is checked in RegisterPropagator().

Definition at line 260 of file sat_base.h.

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