|
| | ClauseManager (Model *model) |
| | --— ClauseManager --—
|
| |
| | ClauseManager (const ClauseManager &)=delete |
| | This type is neither copyable nor movable.
|
| |
| ClauseManager & | operator= (const ClauseManager &)=delete |
| |
| | ~ClauseManager () override |
| |
| void | Resize (int num_variables) |
| | Must be called before adding clauses referring to such variables.
|
| |
| bool | Propagate (Trail *trail) final |
| | SatPropagator API.
|
| |
| absl::Span< const Literal > | Reason (const Trail &trail, int trail_index, int64_t conflict_id) const final |
| |
| SatClause * | ReasonClause (int trail_index) const |
| |
| bool | AddClause (absl::Span< const Literal > literals, Trail *trail, int lbd) |
| | Adds a new clause and perform initial propagation for this clause only.
|
| |
| bool | AddClause (absl::Span< const Literal > literals) |
| |
| SatClause * | AddRemovableClause (absl::Span< const Literal > literals, Trail *trail, int lbd) |
| |
| void | LazyDetach (SatClause *clause) |
| |
| void | CleanUpWatchers () |
| |
| void | Detach (SatClause *clause) |
| |
| 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 () |
| |
| int64_t | num_inspected_clauses () const |
| | Total number of clauses inspected during calls to PropagateOnFalse().
|
| |
| int64_t | num_inspected_clause_literals () const |
| |
| int64_t | literal_size () const |
| | The number of different literals (always twice the number of variables).
|
| |
| int64_t | num_watched_clauses () const |
| | Number of clauses currently watched.
|
| |
| void | SetDratProofHandler (DratProofHandler *drat_proof_handler) |
| |
| SatClause * | NextClauseToMinimize () |
| |
| SatClause * | NextClauseToProbe () |
| |
| void | ResetToProbeIndex () |
| | Restart the scans.
|
| |
| void | ResetToMinimizeIndex () |
| |
| void | DetachAllClauses () |
| |
| void | AttachAllClauses () |
| |
| void | InprocessingRemoveClause (SatClause *clause) |
| | These must only be called between [Detach/Attach]AllClauses() calls.
|
| |
| ABSL_MUST_USE_RESULT bool | InprocessingFixLiteral (Literal true_literal) |
| | This one do not need the clause to be detached.
|
| |
| ABSL_MUST_USE_RESULT bool | InprocessingRewriteClause (SatClause *clause, absl::Span< const Literal > new_clause) |
| |
| SatClause * | InprocessingAddClause (absl::Span< const Literal > new_clause) |
| |
| const std::vector< Watcher > & | WatcherListOnFalse (Literal false_literal) const |
| |
| void | SetAddClauseCallback (absl::AnyInvocable< void(int lbd, absl::Span< const Literal >)> add_clause_callback) |
| |
| | SatPropagator (const std::string &name) |
| |
| | SatPropagator (const SatPropagator &)=delete |
| | This type is neither copyable nor movable.
|
| |
| SatPropagator & | operator= (const SatPropagator &)=delete |
| |
| virtual | ~SatPropagator ()=default |
| |
| void | SetPropagatorId (int id) |
| | Sets/Gets this propagator unique id.
|
| |
| int | PropagatorId () const |
| |
| virtual void | Untrail (const Trail &, int trail_index) |
| |
| bool | PropagatePreconditionsAreSatisfied (const Trail &trail) const |
| | ######################## Implementations below ########################
|
| |
| bool | PropagationIsDone (const Trail &trail) const |
| | Returns true iff all the trail was inspected by this propagator.
|
| |
| virtual bool | IsEmpty () const |
| |
Stores the 2-watched literals data structure. See http://www.cs.berkeley.edu/~necula/autded/lecture24-sat.pdf for detail.
This class is also responsible for owning the clause memory and all related information.
Definition at line 159 of file clause.h.
| void operations_research::sat::ClauseManager::DetachAllClauses |
( |
| ) |
|
During an inprocessing phase, it is easier to detach all clause first, then simplify and then reattach them. Note however that during these two calls, it is not possible to use the solver unit-progation.
Important: When reattach is called, we assume that none of their literal are fixed, so we don't do any special checks.
These functions can be called multiple-time and do the right things. This way before doing something, you can call the corresponding function and be sure to be in a good state. I.e. always AttachAllClauses() before propagation and DetachAllClauses() before going to do an inprocessing pass that might transform them.
This is easy, and this allows to reset memory if some watcher lists where really long at some point.
Definition at line 332 of file clause.cc.
| absl::Span< const Literal > operations_research::sat::ClauseManager::Reason |
( |
const Trail & | , |
|
|
int | , |
|
|
int64_t | ) const |
|
finalvirtual |
Explains why the literal at given trail_index was propagated by returning a reason for this propagation. This will only be called for literals that are on the trail and were propagated by this class.
The interpretation is that because all the literals of a reason were assigned to false, we could deduce the assignment of the given variable.
The returned Span has to be valid until the literal is untrailed. A client can use trail_.GetEmptyVectorToStoreReason() if it doesn't have a memory location that already contains the reason.
If conlict id is positive, then this is called during first UIP resolution and we will backtrack over this literal right away, so we don't need to have a span that survive more than once.
Reimplemented from operations_research::sat::SatPropagator.
Definition at line 210 of file clause.cc.
Public Member Functions inherited from operations_research::sat::SatPropagator
1.12.0