Definition at line 233 of file sat_base.h.
◆ Trail() [1/2]
◆ Trail() [2/2]
◆ Assignment()
◆ AssignmentType()
◆ ChangeReason()
void ChangeReason |
( |
int |
trail_index, |
|
|
int |
propagator_id |
|
) |
| |
|
inline |
◆ CurrentDecisionLevel()
int CurrentDecisionLevel |
( |
| ) |
const |
|
inline |
◆ DebugString()
std::string DebugString |
( |
| ) |
|
|
inline |
◆ Dequeue()
◆ Enqueue()
void Enqueue |
( |
Literal |
true_literal, |
|
|
int |
propagator_id |
|
) |
| |
|
inline |
◆ EnqueueSearchDecision()
void EnqueueSearchDecision |
( |
Literal |
true_literal | ) |
|
|
inline |
◆ EnqueueWithSameReasonAs()
void EnqueueWithSameReasonAs |
( |
Literal |
true_literal, |
|
|
BooleanVariable |
reference_var |
|
) |
| |
|
inline |
◆ EnqueueWithStoredReason()
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason |
( |
Literal |
true_literal | ) |
|
|
inline |
◆ EnqueueWithUnitReason()
void EnqueueWithUnitReason |
( |
Literal |
true_literal | ) |
|
|
inline |
◆ FailingClause()
absl::Span<const Literal> FailingClause |
( |
| ) |
const |
|
inline |
◆ FailingSatClause()
◆ GetEmptyVectorToStoreReason() [1/2]
std::vector<Literal>* GetEmptyVectorToStoreReason |
( |
| ) |
const |
|
inline |
◆ GetEmptyVectorToStoreReason() [2/2]
std::vector<Literal>* GetEmptyVectorToStoreReason |
( |
int |
trail_index | ) |
const |
|
inline |
◆ Index()
◆ Info()
◆ MutableConflict()
std::vector<Literal>* MutableConflict |
( |
| ) |
|
|
inline |
◆ NumberOfEnqueues()
int64 NumberOfEnqueues |
( |
| ) |
const |
|
inline |
◆ NumVariables()
int NumVariables |
( |
| ) |
const |
|
inline |
◆ operator[]()
const Literal& operator[] |
( |
int |
index | ) |
const |
|
inline |
◆ Reason()
absl::Span< const Literal > Reason |
( |
BooleanVariable |
var | ) |
const |
|
inline |
◆ ReferenceVarWithSameReason()
BooleanVariable ReferenceVarWithSameReason |
( |
BooleanVariable |
var | ) |
const |
|
inline |
◆ RegisterPropagator()
◆ Resize()
void Resize |
( |
int |
num_variables | ) |
|
|
inline |
◆ SetDecisionLevel()
void SetDecisionLevel |
( |
int |
level | ) |
|
|
inline |
◆ SetFailingSatClause()
void SetFailingSatClause |
( |
SatClause * |
clause | ) |
|
|
inline |
◆ Untrail()
void Untrail |
( |
int |
target_trail_index | ) |
|
|
inline |
The documentation for this class was generated from the following file: