Definition at line 180 of file clause.h.
|
| | ClauseManager (Model *model) |
| | ClauseManager (const ClauseManager &)=delete |
| ClauseManager & | operator= (const ClauseManager &)=delete |
| | ~ClauseManager () override |
| void | Resize (int num_variables) |
| bool | Propagate (Trail *trail) final |
| absl::Span< const Literal > | Reason (const Trail &trail, int trail_index, int64_t conflict_id) const final |
| void | Reimply (Trail *trail, int old_trail_index) final |
| SatClause * | ReasonClause (int trail_index) const |
| SatClause * | ReasonClauseOrNull (BooleanVariable var) const |
| bool | ClauseIsUsedAsReason (SatClause *clause) const |
| bool | AddClause (ClauseId id, absl::Span< const Literal > literals, Trail *trail, int lbd) |
| bool | AddClause (absl::Span< const Literal > literals) |
| SatClause * | AddRemovableClause (ClauseId id, absl::Span< const Literal > literals, Trail *trail, int lbd) |
| absl::Span< const int64_t > | DeletionCounters () const |
| void | LazyDelete (SatClause *clause, DeletionSourceForStat source) |
| void | CleanUpWatchers () |
| void | Attach (SatClause *clause, Trail *trail) |
| void | DeleteRemovedClauses () |
| int64_t | num_clauses () const |
| const std::vector< SatClause * > & | AllClausesInCreationOrder () const |
| bool | IsRemovable (SatClause *const clause) const |
| int64_t | num_removable_clauses () const |
| absl::flat_hash_map< SatClause *, ClauseInfo > * | mutable_clauses_info () |
| int | LbdOrZeroIfNotRemovable (SatClause *const clause) const |
| void | KeepClauseForever (SatClause *const clause) |
| void | RescaleClauseActivities (double scaling_factor) |
| void | ChangeLbdIfBetter (SatClause *clause, int new_lbd) |
| int64_t | num_inspected_clauses () const |
| int64_t | num_inspected_clause_literals () const |
| int64_t | literal_size () const |
| int64_t | num_watched_clauses () const |
| int64_t | num_lbd_promotions () const |
| ClauseId | GetClauseId (const SatClause *clause) const |
| void | SetClauseId (const SatClause *clause, ClauseId id) |
| SatClause * | NextNewClauseToMinimize () |
| SatClause * | NextClauseToMinimize () |
| SatClause * | NextClauseToProbe () |
| absl::Span< SatClause * > | LastNClauses (int n) |
| void | ResetToProbeIndex () |
| int64_t | NumToMinimizeIndexResets () const |
| void | EnsureNewClauseIndexInitialized () |
| void | DetachAllClauses () |
| void | AttachAllClauses () |
| ABSL_MUST_USE_RESULT bool | InprocessingRewriteClause (SatClause *clause, absl::Span< const Literal > new_clause, absl::Span< const ClauseId > clause_ids={}) |
| bool | RemoveFixedLiteralsAndTestIfTrue (SatClause *clause) |
| ABSL_MUST_USE_RESULT bool | InprocessingAddUnitClause (ClauseId unit_clause_id, Literal true_literal) |
| ABSL_MUST_USE_RESULT bool | InprocessingFixLiteral (Literal true_literal, absl::Span< const ClauseId > clause_ids={}) |
| SatClause * | InprocessingAddClause (absl::Span< const Literal > new_clause) |
| const std::vector< Watcher > & | WatcherListOnFalse (Literal false_literal) const |
| void | SetAddClauseCallback (absl::AnyInvocable< void(int lbd, ClauseId id, absl::Span< const Literal >)> add_clause_callback) |
| absl::AnyInvocable< void(int lbd, ClauseId id, absl::Span< const Literal >)> | TakeAddClauseCallback () |
| ClauseId | ReasonClauseId (Literal literal) const |
| void | AppendClauseIdsFixing (absl::Span< const Literal > literals, std::vector< ClauseId > *clause_ids, LiteralIndex decision=kNoLiteralIndex, std::optional< absl::FunctionRef< ClauseId(int, int)> > root_literals={}) |
| | SatPropagator (const std::string &name) |
| | SatPropagator (const SatPropagator &)=delete |
| SatPropagator & | operator= (const SatPropagator &)=delete |
| virtual | ~SatPropagator ()=default |
| void | SetPropagatorId (int id) |
| int | PropagatorId () const |
| virtual void | Untrail (const Trail &, int trail_index) |
| bool | PropagatePreconditionsAreSatisfied (const Trail &trail) const |
| bool | PropagationIsDone (const Trail &trail) const |
| const std::string & | name () const |
| virtual bool | IsEmpty () const |
1.15.0