OR-Tools  9.6
Classes | Public Member Functions | Protected Attributes | List of all members
LiteralWatchers

Detailed Description

Definition at line 163 of file clause.h.

Classes

struct  Watcher
 

Public Member Functions

 LiteralWatchers (Model *model)
 
 ~LiteralWatchers () override
 
void Resize (int num_variables)
 
bool Propagate (Trail *trail) final
 
absl::Span< const Literal > Reason (const Trail &trail, int trail_index) const final
 
SatClause * ReasonClause (int trail_index) const
 
bool AddClause (absl::Span< const Literal > literals, Trail *trail)
 
bool AddClause (absl::Span< const Literal > literals)
 
SatClause * AddRemovableClause (const std::vector< Literal > &literals, Trail *trail)
 
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
 
int64_t num_inspected_clause_literals () const
 
int64_t literal_size () const
 
int64_t num_watched_clauses () const
 
void SetDratProofHandler (DratProofHandler *drat_proof_handler)
 
SatClause * NextClauseToMinimize ()
 
void ResetToMinimizeIndex ()
 
void DetachAllClauses ()
 
void AttachAllClauses ()
 
void InprocessingRemoveClause (SatClause *clause)
 
ABSL_MUST_USE_RESULT bool InprocessingFixLiteral (Literal true_literal)
 
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 SetPropagatorId (int id)
 
int PropagatorId () const
 
virtual void Untrail (const Trail &trail, int trail_index)
 
bool PropagatePreconditionsAreSatisfied (const Trail &trail) const
 
bool PropagationIsDone (const Trail &trail) const
 
virtual bool IsEmpty () const
 

Protected Attributes

const std::string name_
 
int propagator_id_
 
int propagation_trail_index_
 

Constructor & Destructor Documentation

◆ LiteralWatchers()

LiteralWatchers ( Model *  model)
explicit

Definition at line 71 of file clause.cc.

◆ ~LiteralWatchers()

~LiteralWatchers ( )
override

Definition at line 82 of file clause.cc.

Member Function Documentation

◆ AddClause() [1/2]

bool AddClause ( absl::Span< const Literal >  literals)

Definition at line 219 of file clause.cc.

◆ AddClause() [2/2]

bool AddClause ( absl::Span< const Literal >  literals,
Trail *  trail 
)

Definition at line 223 of file clause.cc.

◆ AddRemovableClause()

SatClause * AddRemovableClause ( const std::vector< Literal > &  literals,
Trail *  trail 
)

Definition at line 230 of file clause.cc.

◆ AllClausesInCreationOrder()

const std::vector<SatClause*>& AllClausesInCreationOrder ( ) const
inline

Definition at line 214 of file clause.h.

◆ Attach()

void Attach ( SatClause *  clause,
Trail *  trail 
)

Definition at line 292 of file clause.cc.

◆ AttachAllClauses()

void AttachAllClauses ( )

Definition at line 340 of file clause.cc.

◆ CleanUpWatchers()

void CleanUpWatchers ( )

Definition at line 459 of file clause.cc.

◆ DeleteRemovedClauses()

void DeleteRemovedClauses ( )

Definition at line 472 of file clause.cc.

◆ Detach()

void Detach ( SatClause *  clause)

Definition at line 319 of file clause.cc.

◆ DetachAllClauses()

void DetachAllClauses ( )

Definition at line 329 of file clause.cc.

◆ InprocessingAddClause()

SatClause * InprocessingAddClause ( absl::Span< const Literal >  new_clause)

Definition at line 433 of file clause.cc.

◆ InprocessingFixLiteral()

bool InprocessingFixLiteral ( Literal  true_literal)

Definition at line 357 of file clause.cc.

◆ InprocessingRemoveClause()

void InprocessingRemoveClause ( SatClause *  clause)

Definition at line 376 of file clause.cc.

◆ InprocessingRewriteClause()

bool InprocessingRewriteClause ( SatClause *  clause,
absl::Span< const Literal >  new_clause 
)

Definition at line 385 of file clause.cc.

◆ IsEmpty()

virtual bool IsEmpty ( ) const
inlinevirtualinherited

Reimplemented in PbConstraints, and BinaryImplicationGraph.

Definition at line 538 of file sat_base.h.

◆ IsRemovable()

bool IsRemovable ( SatClause *const  clause) const
inline

Definition at line 222 of file clause.h.

◆ LazyDetach()

void LazyDetach ( SatClause *  clause)

Definition at line 312 of file clause.cc.

◆ literal_size()

int64_t literal_size ( ) const
inline

Definition at line 237 of file clause.h.

◆ mutable_clauses_info()

absl::flat_hash_map<SatClause*, ClauseInfo>* mutable_clauses_info ( )
inline

Definition at line 226 of file clause.h.

◆ NextClauseToMinimize()

SatClause* NextClauseToMinimize ( )
inline

Definition at line 249 of file clause.h.

◆ num_clauses()

int64_t num_clauses ( ) const
inline

Definition at line 213 of file clause.h.

◆ num_inspected_clause_literals()

int64_t num_inspected_clause_literals ( ) const
inline

Definition at line 232 of file clause.h.

◆ num_inspected_clauses()

int64_t num_inspected_clauses ( ) const
inline

Definition at line 231 of file clause.h.

◆ num_removable_clauses()

int64_t num_removable_clauses ( ) const
inline

Definition at line 225 of file clause.h.

◆ num_watched_clauses()

int64_t num_watched_clauses ( ) const
inline

Definition at line 240 of file clause.h.

◆ Propagate()

bool Propagate ( Trail *  trail)
finalvirtual

Implements SatPropagator.

Definition at line 201 of file clause.cc.

◆ PropagatePreconditionsAreSatisfied()

bool PropagatePreconditionsAreSatisfied ( const Trail &  trail) const
inlineinherited

Definition at line 553 of file sat_base.h.

◆ PropagationIsDone()

bool PropagationIsDone ( const Trail &  trail) const
inlineinherited

Definition at line 530 of file sat_base.h.

◆ PropagatorId()

int PropagatorId ( ) const
inlineinherited

Definition at line 483 of file sat_base.h.

◆ Reason()

absl::Span< const Literal > Reason ( const Trail &  trail,
int  trail_index 
) const
finalvirtual

Reimplemented from SatPropagator.

Definition at line 210 of file clause.cc.

◆ ReasonClause()

SatClause * ReasonClause ( int  trail_index) const

Definition at line 215 of file clause.cc.

◆ ResetToMinimizeIndex()

void ResetToMinimizeIndex ( )
inline

Definition at line 260 of file clause.h.

◆ Resize()

void Resize ( int  num_variables)

Definition at line 87 of file clause.cc.

◆ SetDratProofHandler()

void SetDratProofHandler ( DratProofHandler *  drat_proof_handler)
inline

Definition at line 242 of file clause.h.

◆ SetPropagatorId()

void SetPropagatorId ( int  id)
inlineinherited

Definition at line 482 of file sat_base.h.

◆ Untrail()

virtual void Untrail ( const Trail &  trail,
int  trail_index 
)
inlinevirtualinherited

Reimplemented in SymmetryPropagator, PrecedencesPropagator, PbConstraints, EnforcementPropagator, GenericLiteralWatcher, and IntegerTrail.

Definition at line 505 of file sat_base.h.

◆ WatcherListOnFalse()

const std::vector<Watcher>& WatcherListOnFalse ( Literal  false_literal) const
inline

Definition at line 315 of file clause.h.

Member Data Documentation

◆ name_

const std::string name_
protectedinherited

Definition at line 541 of file sat_base.h.

◆ propagation_trail_index_

int propagation_trail_index_
protectedinherited

Definition at line 543 of file sat_base.h.

◆ propagator_id_

int propagator_id_
protectedinherited

Definition at line 542 of file sat_base.h.

The documentation for this class was generated from the following files: