Solver Class Referenceabstract
Inheritance diagram for Solver:
[legend]
Collaboration diagram for Solver:
[legend]

## Classes

struct | Work
| A single work item. More...
struct | State
| The solver state. More...
struct | Trail
| A trail item. More...

## Public Member Functions

bool | Pop ()
void | UndoOne ()
bool | AddWork (Work &&work)
| Solver (pkgCache &Cache)
bool | Assume (Lit lit, const Clause *reason=nullptr)
bool | Enqueue (Lit lit, const Clause *reason=nullptr)
bool | Solve ()
virtual std::string | WhyStr (Var reason) const
virtual std::string | LongWhyStr (Var var, bool assignment, const Clause *rclause, std::string prefix, std::unordered_set< Var > &seen) const
| Print a long reason string.

## Protected Types

using | level_type = unsigned int
template<typename T>
using | heap = std::vector<T>

## Protected Member Functions

constexpr State & | operator[] (const pkgCache::Package *P) noexcept
constexpr const State & | operator[] (const pkgCache::Package *P) const noexcept
constexpr State & | operator[] (const pkgCache::Version *V) noexcept
constexpr const State & | operator[] (const pkgCache::Version *V) const noexcept
constexpr State & | operator[] (Var r) noexcept
constexpr const State & | operator[] (Var r) const noexcept
constexpr std::vector< const Clause * > & | watches (Lit lit) noexcept
virtual void | Discover (Var var)=0
bool | Propagate ()
bool | Propagate (const Clause *clause, Lit lit)
level_type | decisionLevel ()
constexpr Var | bestReason (Clause const *clause, Var var) const noexcept
constexpr LiftedBool | value (Lit lit) const noexcept

## Protected Attributes

pkgCache & | cache
std::unique_ptr< State > | rootState
ContiguousCacheMap< pkgCache::Package, State > | pkgStates
ContiguousCacheMap< pkgCache::Version, State > | verStates
heap< Work > | work
std::vector< Trail > | trail
| Trail of assignments done, and clauses solved.
std::vector< level_type > | trailLim {}
| Separator indices for different decision levels in trail.
std::queue< Var > | propQ
time_t | startTime {}
std::string | version {_config->Find("APT::Solver", "3.0")}
| Various configuration options.
int | debug {_config->FindI("Debug::APT::Solver")}
int | Timeout {_config->FindI("APT::Solver::Timeout", 10)}

## Member Function Documentation

## Enqueue()

bool Enqueue | ( | Lit | lit,
|  | const Clause * | reason = nullptr )

nodiscard

Todo
  Adjust call to bestReason to use lit

References LongWhyStr(), and trail.

Referenced by DependencySolver::FromDepCache(), and Pop().

## LongWhyStr()

std::string LongWhyStr | ( | Var | var,
|  | bool | assignment,
|  | const Clause * | rclause,
|  | std::string | prefix,
|  | std::unordered_set< Var > & | seen ) const

virtual

Print a long reason string.

Print a reason as to why rclause implies assignment for the variable var.

Parameters

  var | The variable to print the reason for
  assignment | The assumed assignment to print the reason for (may be different from actual assignment if rclause is specified)
  rclause | The clause that caused this variable to be marked (or would be marked)
  prefix | A prefix, for indentation purposes, as this is recursive
  seen | A set of seen objects such that the output does not repeat itself (not for safety, it is acyclic)

References LongWhyStr().

Referenced by Enqueue(), DependencySolver::InternalCliWhy(), and LongWhyStr().

## Pop()

bool Pop | ( |  | ) |

nodiscard

Todo
  There should be a reason!

References Enqueue(), trail, trailLim, and UndoOne().

## UndoOne()

void UndoOne | ( |  | ) |

Todo
  Add the undo handling here once we have watchers.

References trail.

Referenced by Pop().

## Member Data Documentation

## trail

std::vector<Trail> trail

protected

Trail of assignments done, and clauses solved.

Record past assignments and solved clauses such that we can revert them when backtracking.

Referenced by Enqueue(), Pop(), and UndoOne().

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

- apt-pkg/solver3.h
- apt-pkg/solver3.cc