Definition at line 160 of file clause.h.
◆ LiteralWatchers()
◆ ~LiteralWatchers()
◆ AddClause() [1/2]
bool AddClause |
( |
absl::Span< const Literal > |
literals | ) |
|
◆ AddClause() [2/2]
bool AddClause |
( |
absl::Span< const Literal > |
literals, |
|
|
Trail * |
trail |
|
) |
| |
◆ AddRemovableClause()
◆ AllClausesInCreationOrder()
const std::vector<SatClause*>& AllClausesInCreationOrder |
( |
| ) |
const |
|
inline |
◆ Attach()
◆ AttachAllClauses()
void AttachAllClauses |
( |
| ) |
|
◆ CleanUpWatchers()
◆ DeleteRemovedClauses()
void DeleteRemovedClauses |
( |
| ) |
|
◆ Detach()
◆ DetachAllClauses()
void DetachAllClauses |
( |
| ) |
|
◆ InprocessingAddClause()
◆ InprocessingFixLiteral()
bool InprocessingFixLiteral |
( |
Literal |
true_literal | ) |
|
◆ InprocessingRemoveClause()
void InprocessingRemoveClause |
( |
SatClause * |
clause | ) |
|
◆ InprocessingRewriteClause()
bool InprocessingRewriteClause |
( |
SatClause * |
clause, |
|
|
absl::Span< const Literal > |
new_clause |
|
) |
| |
◆ IsRemovable()
bool IsRemovable |
( |
SatClause *const |
clause | ) |
const |
|
inline |
◆ LazyDetach()
◆ literal_size()
int64 literal_size |
( |
| ) |
const |
|
inline |
◆ mutable_clauses_info()
◆ NextClauseToMinimize()
◆ num_clauses()
int64 num_clauses |
( |
| ) |
const |
|
inline |
◆ num_inspected_clause_literals()
int64 num_inspected_clause_literals |
( |
| ) |
const |
|
inline |
◆ num_inspected_clauses()
int64 num_inspected_clauses |
( |
| ) |
const |
|
inline |
◆ num_removable_clauses()
int64 num_removable_clauses |
( |
| ) |
const |
|
inline |
◆ num_watched_clauses()
int64 num_watched_clauses |
( |
| ) |
const |
|
inline |
◆ Propagate()
bool Propagate |
( |
Trail * |
trail | ) |
|
|
finalvirtual |
◆ PropagatePreconditionsAreSatisfied()
bool PropagatePreconditionsAreSatisfied |
( |
const Trail & |
trail | ) |
const |
|
inlineinherited |
◆ PropagationIsDone()
bool PropagationIsDone |
( |
const Trail & |
trail | ) |
const |
|
inlineinherited |
◆ PropagatorId()
int PropagatorId |
( |
| ) |
const |
|
inlineinherited |
◆ Reason()
absl::Span< const Literal > Reason |
( |
const Trail & |
trail, |
|
|
int |
trail_index |
|
) |
| const |
|
finalvirtual |
◆ ReasonClause()
SatClause * ReasonClause |
( |
int |
trail_index | ) |
const |
◆ ResetToMinimizeIndex()
void ResetToMinimizeIndex |
( |
| ) |
|
|
inline |
◆ Resize()
void Resize |
( |
int |
num_variables | ) |
|
◆ SetDratProofHandler()
◆ SetPropagatorId()
void SetPropagatorId |
( |
int |
id | ) |
|
|
inlineinherited |
◆ Untrail()
virtual void Untrail |
( |
const Trail & |
trail, |
|
|
int |
trail_index |
|
) |
| |
|
inlinevirtualinherited |
◆ WatcherListOnFalse()
const std::vector<Watcher>& WatcherListOnFalse |
( |
Literal |
false_literal | ) |
const |
|
inline |
◆ name_
◆ propagation_trail_index_
int propagation_trail_index_ |
|
protectedinherited |
◆ propagator_id_
The documentation for this class was generated from the following files: