Solver::Trail Struct Reference

A trail item. More...

`#include <apt-pkg/solver3.h>`

Collaboration diagram for Solver::Trail:
[legend]

## Public Attributes

Var | assigned
| A variable that got assigned True or False. May be reset to Undefined on backtracking.
std::optional< Work > | work
| A work item (a clause) that was solved. Needs to be put back on the work heap on backtracking.

## Detailed Description

A trail item.

In MiniSAT, a trail item is an assigned literal. However, we store an assigned variable instead, since the assignment is still recorded when we need to access the trail; there does not appear to be a substantial value in recording the sign here; but it produces a risk for a disagreement between the actual state and the sign recorded in the trail.

In addition to MiniSAT's trail, we also need to keep a trail of solved Work items; that is clauses that were being solved, as when undoing the trail, we need to mark those clauses active again by putting them back on the work heap.

The documentation for this struct was generated from the following file:

- apt-pkg/solver3.h