Class Literal

Class Documentation

class Literal

Reference class storing information on each literal (i.e., both positive and negative0. The primary information this tracks is:

  • binary_links_ - Represents variables linked by binary clauses
  • Watch List - Clauses associated with the two watch literals principle

Public Functions

void increaseActivity(unsigned u = 1)

Increase the literal’s supplied literals activity score by the specified amount.

Parameters
  • u: Amount to increase the literals activity score by. This should generally be a positive number.

void resetActivity()

Resets the literals activity score which represents how frequently it appears in a clause.

void removeWatchLinkTo(ClauseOfs clause_ofs)

Parameters
  • clause_ofs:

void replaceWatchLinkTo(ClauseOfs clause_ofs, ClauseOfs replace_ofs)
void addWatchLinkTo(ClauseIndex clause_ofs)

Associates the clause to be monitored with this literal.

Parameters
  • clause_ofs: Clause to be monitored

void addBinLinkTo(LiteralID lit)

Creates a link between the implicit literal and the explicitly supplied literal. This implies the two literals are in the same binary clause.

Parameters
  • lit: Other literal to be linked to.

void resetWatchList()

Resets the binary watch list for a literal. It removes all binary links from the literal to all binary clauses.

It does put the sentinel clause onto the stack.

bool hasBinaryLinkTo(LiteralID lit)

Checks if the implicit literal has a link to the explicitly supplied literal.

Return
true if the two literals appear in the same binary clause.
Parameters
  • lit: Other literal to check for a binary clause linkage to.

bool hasBinaryLinks()

Checks if the literal is associated with any binary links.

Return
True if there is at least one binary link.

Public Members

std::vector<LiteralID> binary_links_ = std::vector<LiteralID>(1, NOT_A_LIT )
std::vector<ClauseOfs> watch_list_ = std::vector<ClauseOfs>(1, NOT_A_CLAUSE )

List of watch clauses for the two watch literals paradigm.

float activity_score_ = 0.0f