OR-Tools  8.2
LiteralWatchers

Detailed Description

Definition at line 160 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 LiteralReason (const Trail &trail, int trail_index) const final
 
SatClauseReasonClause (int trail_index) const
 
bool AddClause (absl::Span< const Literal > literals, Trail *trail)
 
bool AddClause (absl::Span< const Literal > literals)
 
SatClauseAddRemovableClause (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 num_clauses () const
 
const std::vector< SatClause * > & AllClausesInCreationOrder () const
 
bool IsRemovable (SatClause *const clause) const
 
int64 num_removable_clauses () const
 
absl::flat_hash_map< SatClause *, ClauseInfo > * mutable_clauses_info ()
 
int64 num_inspected_clauses () const
 
int64 num_inspected_clause_literals () const
 
int64 literal_size () const
 
int64 num_watched_clauses () const
 
void SetDratProofHandler (DratProofHandler *drat_proof_handler)
 
SatClauseNextClauseToMinimize ()
 
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)
 
SatClauseInprocessingAddClause (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
 

Protected Attributes

const std::string name_
 
int propagator_id_
 
int propagation_trail_index_
 

Constructor & Destructor Documentation

◆ LiteralWatchers()

LiteralWatchers ( Model model)
explicit

Definition at line 53 of file clause.cc.

◆ ~LiteralWatchers()

~LiteralWatchers ( )
override

Definition at line 64 of file clause.cc.

Member Function Documentation

◆ AddClause() [1/2]

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

Definition at line 201 of file clause.cc.

◆ AddClause() [2/2]

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

Definition at line 205 of file clause.cc.

◆ AddRemovableClause()

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

Definition at line 212 of file clause.cc.

◆ AllClausesInCreationOrder()

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

Definition at line 211 of file clause.h.

◆ Attach()

void Attach ( SatClause clause,
Trail trail 
)

Definition at line 274 of file clause.cc.

◆ AttachAllClauses()

void AttachAllClauses ( )

Definition at line 322 of file clause.cc.

◆ CleanUpWatchers()

void CleanUpWatchers ( )

Definition at line 441 of file clause.cc.

◆ DeleteRemovedClauses()

void DeleteRemovedClauses ( )

Definition at line 454 of file clause.cc.

◆ Detach()

void Detach ( SatClause clause)

Definition at line 301 of file clause.cc.

◆ DetachAllClauses()

void DetachAllClauses ( )

Definition at line 311 of file clause.cc.

◆ InprocessingAddClause()

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

Definition at line 415 of file clause.cc.

◆ InprocessingFixLiteral()

bool InprocessingFixLiteral ( Literal  true_literal)

Definition at line 339 of file clause.cc.

◆ InprocessingRemoveClause()

void InprocessingRemoveClause ( SatClause clause)

Definition at line 358 of file clause.cc.

◆ InprocessingRewriteClause()

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

Definition at line 367 of file clause.cc.

◆ IsRemovable()

bool IsRemovable ( SatClause *const  clause) const
inline

Definition at line 219 of file clause.h.

◆ LazyDetach()

void LazyDetach ( SatClause clause)

Definition at line 294 of file clause.cc.

◆ literal_size()

int64 literal_size ( ) const
inline

Definition at line 234 of file clause.h.

◆ mutable_clauses_info()

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

Definition at line 223 of file clause.h.

◆ NextClauseToMinimize()

SatClause * NextClauseToMinimize ( )
inline

Definition at line 246 of file clause.h.

◆ num_clauses()

int64 num_clauses ( ) const
inline

Definition at line 210 of file clause.h.

◆ num_inspected_clause_literals()

int64 num_inspected_clause_literals ( ) const
inline

Definition at line 229 of file clause.h.

◆ num_inspected_clauses()

int64 num_inspected_clauses ( ) const
inline

Definition at line 228 of file clause.h.

◆ num_removable_clauses()

int64 num_removable_clauses ( ) const
inline

Definition at line 222 of file clause.h.

◆ num_watched_clauses()

int64 num_watched_clauses ( ) const
inline

Definition at line 237 of file clause.h.

◆ Propagate()

bool Propagate ( Trail trail)
finalvirtual

Implements SatPropagator.

Definition at line 183 of file clause.cc.

◆ PropagatePreconditionsAreSatisfied()

bool PropagatePreconditionsAreSatisfied ( const Trail trail) const
inlineinherited

Definition at line 517 of file sat_base.h.

◆ PropagationIsDone()

bool PropagationIsDone ( const Trail trail) const
inlineinherited

Definition at line 500 of file sat_base.h.

◆ PropagatorId()

int PropagatorId ( ) const
inlineinherited

Definition at line 453 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 192 of file clause.cc.

◆ ReasonClause()

SatClause * ReasonClause ( int  trail_index) const

Definition at line 197 of file clause.cc.

◆ ResetToMinimizeIndex()

void ResetToMinimizeIndex ( )
inline

Definition at line 257 of file clause.h.

◆ Resize()

void Resize ( int  num_variables)

Definition at line 69 of file clause.cc.

◆ SetDratProofHandler()

void SetDratProofHandler ( DratProofHandler drat_proof_handler)
inline

Definition at line 239 of file clause.h.

◆ SetPropagatorId()

void SetPropagatorId ( int  id)
inlineinherited

Definition at line 452 of file sat_base.h.

◆ Untrail()

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

◆ WatcherListOnFalse()

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

Definition at line 312 of file clause.h.

Member Data Documentation

◆ name_

const std::string name_
protectedinherited

Definition at line 505 of file sat_base.h.

◆ propagation_trail_index_

int propagation_trail_index_
protectedinherited

Definition at line 507 of file sat_base.h.

◆ propagator_id_

int propagator_id_
protectedinherited

Definition at line 506 of file sat_base.h.


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