operations_research::sat::ClauseManager Member List

This is the complete list of members for operations_research::sat::ClauseManager, including all inherited members.

AddClause(ClauseId id, absl::Span< const Literal > literals, Trail *trail, int lbd)	operations_research::sat::ClauseManager
AddClause(absl::Span< const Literal > literals)	operations_research::sat::ClauseManager
AddRemovableClause(ClauseId id, absl::Span< const Literal > literals, Trail *trail, int lbd)	operations_research::sat::ClauseManager
AllClausesInCreationOrder() const	operations_research::sat::ClauseManager	inline
AppendClauseIdsFixing(absl::Span< const Literal > literals, std::vector< ClauseId > *clause_ids, LiteralIndex decision=kNoLiteralIndex, std::optional< absl::FunctionRef< ClauseId(int, int)> > root_literals={})	operations_research::sat::ClauseManager
Attach(SatClause *clause, Trail *trail)	operations_research::sat::ClauseManager
AttachAllClauses()	operations_research::sat::ClauseManager
ChangeLbdIfBetter(SatClause *clause, int new_lbd)	operations_research::sat::ClauseManager
ClauseIsUsedAsReason(SatClause *clause) const	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
DeletionCounters() const	operations_research::sat::ClauseManager	inline
DetachAllClauses()	operations_research::sat::ClauseManager
EnsureNewClauseIndexInitialized()	operations_research::sat::ClauseManager	inline
GetClauseId(const SatClause *clause) const	operations_research::sat::ClauseManager	inline
InprocessingAddClause(absl::Span< const Literal > new_clause)	operations_research::sat::ClauseManager
InprocessingAddUnitClause(ClauseId unit_clause_id, Literal true_literal)	operations_research::sat::ClauseManager
InprocessingFixLiteral(Literal true_literal, absl::Span< const ClauseId > clause_ids={})	operations_research::sat::ClauseManager
InprocessingRewriteClause(SatClause *clause, absl::Span< const Literal > new_clause, absl::Span< const ClauseId > clause_ids={})	operations_research::sat::ClauseManager
IsEmpty() const	operations_research::sat::SatPropagator	inlinevirtual
IsRemovable(SatClause *const clause) const	operations_research::sat::ClauseManager	inline
KeepClauseForever(SatClause *const clause)	operations_research::sat::ClauseManager	inline
LastNClauses(int n)	operations_research::sat::ClauseManager	inline
LazyDelete(SatClause *clause, DeletionSourceForStat source)	operations_research::sat::ClauseManager
LbdOrZeroIfNotRemovable(SatClause *const clause) const	operations_research::sat::ClauseManager	inline
literal_size() const	operations_research::sat::ClauseManager	inline
mutable_clauses_info()	operations_research::sat::ClauseManager	inline
name() const	operations_research::sat::SatPropagator	inline
name_	operations_research::sat::SatPropagator	protected
NextClauseToMinimize()	operations_research::sat::ClauseManager
NextClauseToProbe()	operations_research::sat::ClauseManager
NextNewClauseToMinimize()	operations_research::sat::ClauseManager
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_lbd_promotions() const	operations_research::sat::ClauseManager	inline
num_removable_clauses() const	operations_research::sat::ClauseManager	inline
num_watched_clauses() const	operations_research::sat::ClauseManager	inline
NumToMinimizeIndexResets() 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
ReasonClauseId(Literal literal) const	operations_research::sat::ClauseManager
ReasonClauseOrNull(BooleanVariable var) const	operations_research::sat::ClauseManager
Reimply(Trail *trail, int old_trail_index) final	operations_research::sat::ClauseManager	virtual
RemoveFixedLiteralsAndTestIfTrue(SatClause *clause)	operations_research::sat::ClauseManager
RescaleClauseActivities(double scaling_factor)	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, ClauseId id, absl::Span< const Literal >)> add_clause_callback)	operations_research::sat::ClauseManager	inline
SetClauseId(const SatClause *clause, ClauseId id)	operations_research::sat::ClauseManager	inline
SetPropagatorId(int id)	operations_research::sat::SatPropagator	inline
TakeAddClauseCallback()	operations_research::sat::ClauseManager	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