AddClause(absl::Span< const Literal > literals, Trail *trail, int lbd) | operations_research::sat::ClauseManager | |
AddClause(absl::Span< const Literal > literals) | operations_research::sat::ClauseManager | |
AddRemovableClause(absl::Span< const Literal > literals, Trail *trail, int lbd) | operations_research::sat::ClauseManager | |
AllClausesInCreationOrder() const | operations_research::sat::ClauseManager | inline |
Attach(SatClause *clause, Trail *trail) | operations_research::sat::ClauseManager | |
AttachAllClauses() | operations_research::sat::ClauseManager | |
ClauseManager(Model *model) | operations_research::sat::ClauseManager | explicit |
ClauseManager(const ClauseManager &)=delete | operations_research::sat::ClauseManager | |
CleanUpWatchers() | operations_research::sat::ClauseManager | |
DeleteRemovedClauses() | operations_research::sat::ClauseManager | |
Detach(SatClause *clause) | operations_research::sat::ClauseManager | |
DetachAllClauses() | operations_research::sat::ClauseManager | |
InprocessingAddClause(absl::Span< const Literal > new_clause) | operations_research::sat::ClauseManager | |
InprocessingFixLiteral(Literal true_literal) | operations_research::sat::ClauseManager | |
InprocessingRemoveClause(SatClause *clause) | operations_research::sat::ClauseManager | |
InprocessingRewriteClause(SatClause *clause, absl::Span< const Literal > new_clause) | operations_research::sat::ClauseManager | |
IsEmpty() const | operations_research::sat::SatPropagator | inlinevirtual |
IsRemovable(SatClause *const clause) const | operations_research::sat::ClauseManager | inline |
LazyDetach(SatClause *clause) | operations_research::sat::ClauseManager | |
literal_size() const | operations_research::sat::ClauseManager | inline |
mutable_clauses_info() | operations_research::sat::ClauseManager | inline |
name_ | operations_research::sat::SatPropagator | protected |
NextClauseToMinimize() | operations_research::sat::ClauseManager | inline |
NextClauseToProbe() | operations_research::sat::ClauseManager | inline |
num_clauses() const | operations_research::sat::ClauseManager | inline |
num_inspected_clause_literals() const | operations_research::sat::ClauseManager | inline |
num_inspected_clauses() const | operations_research::sat::ClauseManager | inline |
num_removable_clauses() const | operations_research::sat::ClauseManager | inline |
num_watched_clauses() const | operations_research::sat::ClauseManager | inline |
operator=(const ClauseManager &)=delete | operations_research::sat::ClauseManager | |
operations_research::sat::SatPropagator::operator=(const SatPropagator &)=delete | operations_research::sat::SatPropagator | |
Propagate(Trail *trail) final | operations_research::sat::ClauseManager | virtual |
PropagatePreconditionsAreSatisfied(const Trail &trail) const | operations_research::sat::SatPropagator | inline |
propagation_trail_index_ | operations_research::sat::SatPropagator | protected |
PropagationIsDone(const Trail &trail) const | operations_research::sat::SatPropagator | inline |
propagator_id_ | operations_research::sat::SatPropagator | protected |
PropagatorId() const | operations_research::sat::SatPropagator | inline |
Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final | operations_research::sat::ClauseManager | virtual |
ReasonClause(int trail_index) const | operations_research::sat::ClauseManager | |
ResetToMinimizeIndex() | operations_research::sat::ClauseManager | inline |
ResetToProbeIndex() | operations_research::sat::ClauseManager | inline |
Resize(int num_variables) | operations_research::sat::ClauseManager | |
SatPropagator(const std::string &name) | operations_research::sat::SatPropagator | inlineexplicit |
SatPropagator(const SatPropagator &)=delete | operations_research::sat::SatPropagator | |
SetAddClauseCallback(absl::AnyInvocable< void(int lbd, absl::Span< const Literal >)> add_clause_callback) | operations_research::sat::ClauseManager | inline |
SetDratProofHandler(DratProofHandler *drat_proof_handler) | operations_research::sat::ClauseManager | inline |
SetPropagatorId(int id) | operations_research::sat::SatPropagator | inline |
Untrail(const Trail &, int trail_index) | operations_research::sat::SatPropagator | inlinevirtual |
WatcherListOnFalse(Literal false_literal) const | operations_research::sat::ClauseManager | inline |
~ClauseManager() override | operations_research::sat::ClauseManager | |
~SatPropagator()=default | operations_research::sat::SatPropagator | virtual |