Classes | |
| class | Clasp::Assignment |
| Stores assignment related information. More... | |
| struct | Clasp::CCMinRecursive |
| class | Clasp::ClauseHead |
| (Abstract) base class for clause types. More... | |
| class | Clasp::ClauseInfo |
| struct | Clasp::ClauseRep |
| Primitive representation of a clause. More... | |
| struct | Clasp::ClauseWatch |
| struct | Clasp::CoreStats |
| A struct for holding core statistics used by a solver. More... | |
| struct | Clasp::ExtendedStats |
| A struct for holding (optional) extra statistics. More... | |
| struct | Clasp::GenericWatch |
| Represents a generic watch in a Solver. More... | |
| struct | Clasp::ImpliedList |
| A type for storing ImpliedLiteral objects. More... | |
| struct | Clasp::ImpliedLiteral |
| Stores information about a literal that is implied on an earlier level than the current decision level. More... | |
| struct | Clasp::JumpStats |
| A struct for holding (optional) jump statistics. More... | |
| struct | Clasp::QueueImpl |
| struct | Clasp::ReasonStore32 |
| struct | Clasp::ReasonStore64 |
| Type for storing reasons for variable assignments together with additional data. More... | |
| class | Clasp::SatPreprocessor |
| Base class for preprocessors working on clauses only. More... | |
| class | Clasp::SmallClauseAlloc |
| Allocator for small (at most 32-byte) clauses. More... | |
| class | Clasp::SolveAlgorithm |
| Interface for complex solve algorithms. More... | |
| struct | Clasp::SolveParams |
| Parameter-Object for grouping solve-related options. More... | |
| class | Clasp::Solver |
| clasp's Solver class. More... | |
| struct | Clasp::SolverStats |
| A struct for aggregating statistics maintained in a solver object. More... | |
| struct | Clasp::SumQueue |
| struct | Clasp::ValueSet |
| A set of configurable values for a variable. More... | |
Defines | |
| #define | CLASP_STAT_ACCU(m, k, a, accu) accu; |
| #define | CLASP_STAT_DEFINE(m, k, a, accu) m |
| #define | CLASP_STAT_GET(m, k, a, accu) if (std::strcmp(key, k) == 0) { return double( (a) ); } |
| #define | CLASP_STAT_KEY(m, k, a, accu) k "\0" |
| #define | NO_ARG |
Typedefs | |
| typedef bk_lib::left_right_sequence < ClauseWatch, GenericWatch, 0 > | Clasp::WatchList |
| Watch list type. | |
Functions | |
| void | Clasp::SolverStats::addCpuTime (double t) |
| void | Clasp::SolverStats::addDeleted (uint32 num) |
| void | Clasp::SolverStats::addDistributed (uint32 lbd, ConstraintType t) |
| void | Clasp::SolverStats::addDomChoice (uint32 num=1) |
| void | Clasp::SolverStats::addIntegrated (uint32 num=1) |
| void | Clasp::SolverStats::addIntegratedAsserting (uint32 receivedDL, uint32 jumpDL) |
| void | Clasp::SolverStats::addLearnt (uint32 size, ConstraintType t) |
| void | Clasp::SolverStats::addModel (uint32 decisionLevel) |
| void | Clasp::SolverStats::addPath (const LitVec::size_type &sz) |
| void | Clasp::SolverStats::addSplit (uint32 num=1) |
| void | Clasp::SolverStats::addTest (bool partial) |
| bool | Clasp::isRevLit (const Solver &s, Literal p, uint32 maxL) |
| bool | Clasp::matchStatPath (const char *&x, const char *path, std::size_t len) |
| bool | Clasp::matchStatPath (const char *&x, const char *path) |
| double | Clasp::percent (uint64 x, uint64 y) |
| double | Clasp::ratio (uint64 x, uint64 y) |
| void | Clasp::releaseVec (WatchList &w) |
| void | Clasp::SolverStats::removeIntegrated (uint32 num=1) |
| template<class C > | |
| void | Clasp::simplifyDB (Solver &s, C &db, bool shuffle) |
| void | Clasp::SolverStats::updateJumps (uint32 dl, uint32 uipLevel, uint32 bLevel, uint32 lbd) |
| #define CLASP_STAT_ACCU | ( | m, | |
| k, | |||
| a, | |||
| accu | |||
| ) | accu; |
Definition at line 60 of file solver_types.h.
| #define CLASP_STAT_DEFINE | ( | m, | |
| k, | |||
| a, | |||
| accu | |||
| ) | m |
Definition at line 61 of file solver_types.h.
| #define CLASP_STAT_GET | ( | m, | |
| k, | |||
| a, | |||
| accu | |||
| ) | if (std::strcmp(key, k) == 0) { return double( (a) ); } |
Definition at line 62 of file solver_types.h.
| #define CLASP_STAT_KEY | ( | m, | |
| k, | |||
| a, | |||
| accu | |||
| ) | k "\0" |
Definition at line 63 of file solver_types.h.
| #define NO_ARG |
Definition at line 64 of file solver_types.h.
| typedef bk_lib::left_right_sequence<ClauseWatch, GenericWatch, 0> Clasp::WatchList |
Watch list type.
Definition at line 570 of file solver_types.h.
| void Clasp::SolverStats::addCpuTime | ( | double | t | ) | [inline] |
Definition at line 336 of file solver_types.h.
| void Clasp::SolverStats::addDeleted | ( | uint32 | num | ) | [inline] |
Definition at line 332 of file solver_types.h.
| void Clasp::SolverStats::addDistributed | ( | uint32 | lbd, |
| ConstraintType | t | ||
| ) | [inline] |
Definition at line 333 of file solver_types.h.
| void Clasp::SolverStats::addDomChoice | ( | uint32 | num = 1 | ) | [inline] |
Definition at line 341 of file solver_types.h.
| void Clasp::SolverStats::addIntegrated | ( | uint32 | num = 1 | ) | [inline] |
Definition at line 334 of file solver_types.h.
| void Clasp::SolverStats::addIntegratedAsserting | ( | uint32 | receivedDL, |
| uint32 | jumpDL | ||
| ) | [inline] |
Definition at line 342 of file solver_types.h.
| void Clasp::SolverStats::addLearnt | ( | uint32 | size, |
| ConstraintType | t | ||
| ) | [inline] |
Definition at line 331 of file solver_types.h.
| void Clasp::SolverStats::addModel | ( | uint32 | decisionLevel | ) | [inline] |
Definition at line 340 of file solver_types.h.
| void Clasp::SolverStats::addPath | ( | const LitVec::size_type & | sz | ) | [inline] |
Definition at line 338 of file solver_types.h.
| void Clasp::SolverStats::addSplit | ( | uint32 | num = 1 | ) | [inline] |
Definition at line 337 of file solver_types.h.
| void Clasp::SolverStats::addTest | ( | bool | partial | ) | [inline] |
Definition at line 339 of file solver_types.h.
| bool Clasp::isRevLit | ( | const Solver & | s, |
| Literal | p, | ||
| uint32 | maxL | ||
| ) | [inline] |
| bool Clasp::matchStatPath | ( | const char *& | x, |
| const char * | path, | ||
| std::size_t | len | ||
| ) | [inline] |
Definition at line 53 of file solver_types.h.
| bool Clasp::matchStatPath | ( | const char *& | x, |
| const char * | path | ||
| ) | [inline] |
Definition at line 56 of file solver_types.h.
| double Clasp::percent | ( | uint64 | x, |
| uint64 | y | ||
| ) | [inline] |
Definition at line 51 of file solver_types.h.
| double Clasp::ratio | ( | uint64 | x, |
| uint64 | y | ||
| ) | [inline] |
Definition at line 47 of file solver_types.h.
| void Clasp::releaseVec | ( | WatchList & | w | ) | [inline] |
Definition at line 571 of file solver_types.h.
| void Clasp::SolverStats::removeIntegrated | ( | uint32 | num = 1 | ) | [inline] |
Definition at line 335 of file solver_types.h.
| void Clasp::simplifyDB | ( | Solver & | s, |
| C & | db, | ||
| bool | shuffle | ||
| ) |
| void Clasp::SolverStats::updateJumps | ( | uint32 | dl, |
| uint32 | uipLevel, | ||
| uint32 | bLevel, | ||
| uint32 | lbd | ||
| ) | [inline] |
Definition at line 345 of file solver_types.h.